Fix ChartedSpace.lean

Ray.lean

@@ -11,6 +11,7 @@ import Ray.Dynamics.Multibrot.Postcritical
 import Ray.Dynamics.Ray
 import Ray.Hartogs.Hartogs
 import Ray.Hartogs.Osgood
+import Ray.Misc.ChartedSpace
 import Ray.Render.Grid
 import Ray.Render.Mandelbrot
 import Ray.Render.Image

Ray/Misc/ChartedSpace.lean

@@ -26,22 +26,21 @@ theorem ChartedSpace.t1Space [T1Space A] : T1Space M where
         simp only [mem_diff, mem_singleton_iff, mem_inter_iff, mem_preimage]; constructor
         intro ⟨zm, zx⟩; use zm, PartialEquiv.map_source _ zm, (PartialEquiv.injOn _).ne zm xm zx
         intro ⟨zm, _, zx⟩; use zm, ((PartialEquiv.injOn _).ne_iff zm xm).mp zx
-      use t; refine ⟨_, _, _⟩
-      simp only [mem_diff, mem_singleton_iff, eq_self_iff_true, not_true, and_false_iff,
-        not_false_iff]
-      rw [e]
-      apply (chartAt A y).continuousOn.isOpen_inter_preimage (_root_.chartAt _ _).open_source
-      exact IsOpen.sdiff (_root_.chartAt _ _).open_target isClosed_singleton
-      rw [e]
-      simp only [mem_inter_iff, mem_chart_source, true_and_iff, mem_preimage, mem_diff,
-        mem_chart_target, mem_singleton_iff]
-      exact (PartialEquiv.injOn _).ne (mem_chart_source A y) xm m
-    · use(chartAt A y).source, xm, (chartAt A y).open_source, mem_chart_source A y
+      refine ⟨t, ?_, ?_, ?_⟩
+      · simp only [mem_diff, mem_singleton_iff, not_true_eq_false, and_false, not_false_eq_true, t]
+      · rw [e]
+        apply (chartAt A y).continuousOn.isOpen_inter_preimage (_root_.chartAt _ _).open_source
+        exact IsOpen.sdiff (_root_.chartAt _ _).open_target isClosed_singleton
+      · rw [e]
+        simp only [preimage_diff, mem_inter_iff, mem_chart_source, mem_diff, mem_preimage,
+          PartialHomeomorph.map_source, mem_singleton_iff, true_and]
+        exact (PartialEquiv.injOn _).ne (mem_chart_source A y) xm m
+    · use (chartAt A y).source, xm, (chartAt A y).open_source, mem_chart_source A y
 
 /-- Charted spaces are regular if `A` is regular and locally compact and `M` is `T2`.
     This is a weird set of assumptions, but I don't know how to prove T2 naturally. -/
 theorem ChartedSpace.regularSpace [T2Space M] [LocallyCompactSpace A] : RegularSpace M := by
-  apply RegularSpace.ofExistsMemNhdsIsClosedSubset; intro x s n
+  apply RegularSpace.of_exists_mem_nhds_isClosed_subset; intro x s n
   set t := (chartAt A x).target ∩ (chartAt A x).symm ⁻¹' ((chartAt A x).source ∩ s)
   have cn : (chartAt A x).source ∈ 𝓝 x :=
     (chartAt A x).open_source.mem_nhds (mem_chart_source A x)
@@ -50,13 +49,13 @@ theorem ChartedSpace.regularSpace [T2Space M] [LocallyCompactSpace A] : RegularS
     apply ((chartAt A x).continuousAt_symm (mem_chart_target _ _)).preimage_mem_nhds
     rw [(chartAt A x).left_inv (mem_chart_source _ _)]; exact Filter.inter_mem cn n
   rcases local_compact_nhds tn with ⟨u, un, ut, uc⟩
-  refine ⟨(chartAt A x).symm '' u, _, _, _⟩
+  refine ⟨(chartAt A x).symm '' u, ?_, ?_, ?_⟩
   · convert (chartAt A x).symm.image_mem_nhds _ un
     rw [(chartAt A x).left_inv (mem_chart_source _ _)]
     rw [PartialHomeomorph.symm_source]; exact mem_chart_target _ _
   · have c : IsCompact ((chartAt A x).symm '' u) :=
       uc.image_of_continuousOn ((chartAt A x).continuousOn_symm.mono
-        (_root_.trans ut (inter_subset_left _ _)))
+        (_root_.trans ut inter_subset_left))
     exact c.isClosed
   · intro y m; rcases(mem_image _ _ _).mp m with ⟨z, zu, zy⟩; rw [← zy]
     rcases ut zu with ⟨_, m1⟩; simp only [mem_preimage] at m1; exact m1.2