author paulson Tue, 02 Nov 2021 17:01:47 +0000 changeset 75049 2d9d02beaf96 parent 75048 4c508826fee8 child 75056 74f044c3e590
simplified some ugly proofs
```--- a/src/HOL/Topological_Spaces.thy	Tue Nov 02 16:01:25 2021 +0100
+++ b/src/HOL/Topological_Spaces.thy	Tue Nov 02 17:01:47 2021 +0000
@@ -567,12 +567,7 @@

lemma (in topological_space) at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}"
unfolding trivial_limit_def eventually_at_topological
-  apply safe
-   apply (case_tac "S = {a}")
-    apply simp
-   apply fast
-  apply fast
-  done
+  by (metis UNIV_I empty_iff is_singletonE is_singletonI' singleton_iff)

lemma (in perfect_space) at_neq_bot [simp]: "at a \<noteq> bot"
@@ -1574,15 +1569,11 @@
show "x \<in> (\<Inter>i\<le>n. A i)" "\<And>n. open (\<Inter>i\<le>n. A i)" for n
using * by auto
-    show "nhds x = (INF n. principal (\<Inter>i\<le>n. A i))"
-      using *
+    with * show "nhds x = (INF n. principal (\<Inter>i\<le>n. A i))"
unfolding nhds_def
-      apply -
-      apply (rule INF_eq)
-       apply simp_all
+      apply (intro INF_eq)
apply fastforce
-      apply (intro exI [of _ "\<Inter>i\<le>n. A i" for n] conjI open_INT)
-         apply auto
+      apply blast
done
qed
qed
@@ -2487,24 +2478,12 @@
and Q: "\<And>I'. finite I' \<Longrightarrow> I' \<subseteq> I \<Longrightarrow> (s \<inter> (\<Inter>i\<in>I'. f i) \<noteq> {})"
shows "s \<inter> (\<Inter>i\<in>I. f i) \<noteq> {}"
proof -
-  note \<open>compact s\<close>
-  moreover from P have "\<forall>i \<in> f ` I. closed i"
+  from P have "\<forall>i \<in> f ` I. closed i"
by blast
moreover have "\<forall>A. finite A \<and> A \<subseteq> f ` I \<longrightarrow> (s \<inter> (\<Inter>A) \<noteq> {})"
-    apply rule
-    apply rule
-    apply (erule conjE)
-  proof -
-    fix A :: "'a set set"
-    assume "finite A" and "A \<subseteq> f ` I"
-    then obtain B where "B \<subseteq> I" and "finite B" and "A = f ` B"
-      using finite_subset_image [of A f I] by blast
-    with Q [of B] show "s \<inter> \<Inter>A \<noteq> {}"
-      by simp
-  qed
-  ultimately have "s \<inter> (\<Inter>(f ` I)) \<noteq> {}"
-    by (metis compact_imp_fip)
-  then show ?thesis by simp
+    by (metis Q finite_subset_image)
+  ultimately show "s \<inter> (\<Inter>(f ` I)) \<noteq> {}"
+    by (metis \<open>compact s\<close> compact_imp_fip)
qed

end```