lake update

Ray/Analytic/Analytic.lean

@@ -182,7 +182,7 @@ lemma FormalMultilinearSeries.unshift_radius' (p : FormalMultilinearSeries 𝕜
       intro n; induction' n with n _
       · simp only [FormalMultilinearSeries.unshift_coeff_zero,
           FormalMultilinearSeries.norm_apply_eq_norm_coef, pow_zero, mul_one, le_max_iff, le_refl,
-          true_or_iff]
+          true_or]
       · simp only [FormalMultilinearSeries.norm_apply_eq_norm_coef] at h
         simp only [FormalMultilinearSeries.unshift_coeff_succ, pow_succ, ← mul_assoc,
           FormalMultilinearSeries.norm_apply_eq_norm_coef, le_max_iff]
@@ -331,7 +331,7 @@ theorem orderAt_const_smul {f : 𝕜 → E} {c a : 𝕜} (a0 : a ≠ 0) :
   by_cases fa : AnalyticAt 𝕜 f c
   · rcases fa with ⟨p, fp⟩
     have e : ∀ n, a • p n ≠ 0 ↔ p n ≠ 0 := fun n ↦ by
-      simp only [a0, Ne, smul_eq_zero, false_or_iff]
+      simp only [a0, Ne, smul_eq_zero, false_or]
     simp only [fp.orderAt_unique, fp.const_smul.orderAt_unique, FormalMultilinearSeries.order, e]
   · have ga := fa; rw [← analyticAt_iff_const_smul a0] at ga
     simp only [orderAt, fa, ga]; rw [dif_neg, dif_neg]

Ray/Analytic/Within.lean

@@ -27,21 +27,26 @@ lemma AnalyticWithinAt.congr_set {f : E → F} {s t : Set E} {x : E} (hf : Analy
     r_pos := by bound
     hasSum := by
       intro y m n
-      simp only [EMetric.mem_ball, lt_min_iff, edist_lt_ofReal, dist_zero_right] at m n ⊢
-      exact hp.hasSum (by simpa only [mem_def, dist_self_add_left, n.1, @st (x + y)]) n.2
-    continuousWithinAt := by
-      have e : 𝓝[s] x = 𝓝[t] x := nhdsWithin_eq_iff_eventuallyEq.mpr hst
-      simpa only [ContinuousWithinAt, e] using hp.continuousWithinAt }⟩
+      apply hp.hasSum
+      simp only [mem_insert_iff, add_right_eq_self, EMetric.mem_ball, lt_min_iff, edist_lt_ofReal,
+        dist_zero_right] at m n ⊢
+      rcases m with m | m
+      · exact .inl m
+      · specialize @st (x + y) _
+        · simpa only [dist_self_add_left] using n.1
+        · simp only [eq_iff_iff] at st
+          exact Or.inr (st.mpr m)
+      · simp only [EMetric.mem_ball, lt_min_iff, edist_lt_ofReal, dist_zero_right] at n ⊢
+        exact n.2 }⟩
 
 /-- Analyticity within is open (within the set) -/
 lemma AnalyticWithinAt.eventually_analyticWithinAt [CompleteSpace F] {f : E → F} {s : Set E} {x : E}
     (hf : AnalyticWithinAt 𝕜 f s x) : ∀ᶠ y in 𝓝[s] x, AnalyticWithinAt 𝕜 f s y := by
-  obtain ⟨_, g, fg, ga⟩ := analyticWithinAt_iff_exists_analyticAt.mp hf
+  obtain ⟨g, fg, ga⟩ := analyticWithinAt_iff_exists_analyticAt.mp hf
   simp only [Filter.EventuallyEq, eventually_nhdsWithin_iff] at fg ⊢
   filter_upwards [fg.eventually_nhds, ga.eventually_analyticAt]
   intro z fg ga zs
-  refine analyticWithinAt_iff_exists_analyticAt.mpr ⟨?_, g, ?_, ga⟩
-  · refine ga.continuousAt.continuousWithinAt.congr_of_eventuallyEq ?_ (fg.self_of_nhds zs)
-    rw [← eventually_nhdsWithin_iff] at fg
-    exact fg
-  · simpa only [Filter.EventuallyEq, eventually_nhdsWithin_iff]
+  refine analyticWithinAt_iff_exists_analyticAt.mpr ⟨g, ?_, ga⟩
+  rw [← eventually_nhdsWithin_iff] at fg
+  refine fg.filter_mono (nhdsWithin_mono _ ?_)
+  simp only [zs, insert_eq_of_mem, subset_insert]

Ray/AnalyticManifold/AnalyticManifold.lean

@@ -161,7 +161,7 @@ theorem MAnalyticOn.continuousOn {f : M → N} {s : Set M} (h : MAnalyticOn I J
 /-- Constants are analytic -/
 theorem mAnalyticAt_const {x : M} {c : N} : MAnalyticAt I J (fun _ ↦ c) x := by
   rw [mAnalyticAt_iff]; use continuousAt_const
-  simp only [Prod.fst_comp_mk, Function.comp]
+  simp only [Prod.fst_comp_mk, Function.comp_def]
   exact analyticAt_const.analyticWithinAt
 
 /-- Constants are analytic -/
@@ -304,9 +304,39 @@ theorem MAnalyticAt.congr [CompleteSpace F] {f g : M → N} {x : M} (fa : MAnaly
     refine Filter.EventuallyEq.fun_comp ?_ (_root_.extChartAt J (g x))
     have t := (continuousAt_extChartAt_symm I x).tendsto
     rw [PartialEquiv.left_inv _ (mem_extChartAt_source I x)] at t
-    exact e.comp_tendsto (t.mono_left nhdsWithin_le_nhds)
+    exact (e.comp_tendsto (t.mono_left nhdsWithin_le_nhds)).symm
   · simp only [e.self_of_nhds, Function.comp, PartialEquiv.left_inv _ (mem_extChartAt_source _ _)]
 
+/-- `MAnalyticAt` for `x ↦ (f x, g x)` -/
+theorem MAnalyticAt.prod {f : O → M} {g : O → N} {x : O}
+    (fh : MAnalyticAt K I f x) (gh : MAnalyticAt K J g x) :
+    MAnalyticAt K (I.prod J) (fun x ↦ (f x, g x)) x := by
+  rw [mAnalyticAt_iff] at fh gh ⊢; use fh.1.prod gh.1
+  refine (fh.2.prod gh.2).congr_of_eventuallyEq ?_ ?_
+  simp only [eventuallyEq_nhdsWithin_iff]
+  refine .of_forall fun y _ ↦ ?_
+  simp only [extChartAt_prod, Function.comp, PartialEquiv.prod_coe]
+  simp only [mfld_simps]
+
+/-- `MAnalytic` for `x ↦ (f x, g x)` -/
+theorem MAnalytic.prod {f : O → M} {g : O → N} (fh : MAnalytic K I f) (gh : MAnalytic K J g) :
+    MAnalytic K (I.prod J) fun x ↦ (f x, g x) := fun x ↦ (fh x).prod (gh x)
+
+/-- `id` is analytic -/
+theorem mAnalyticAt_id {x : M} : MAnalyticAt I I (fun x ↦ x) x := by
+  rw [mAnalyticAt_iff]
+  use continuousAt_id
+  refine (analyticAt_id _ _).analyticWithinAt.congr_of_eventuallyEq ?_ ?_
+  · simp only [mfld_simps, Filter.EventuallyEq, id, ← I.map_nhds_eq, Filter.eventually_map]
+    filter_upwards [(chartAt A x).open_target.eventually_mem (mem_chart_target _ _)]
+    intro y m
+    simp only [(chartAt A x).right_inv m]
+  · simp only [mfld_simps]
+
+/-- `id` is analytic -/
+theorem mAnalytic_id : MAnalytic I I fun x : M ↦ x :=
+  fun _ ↦ mAnalyticAt_id
+
 variable [CompleteSpace E] [CompleteSpace F]
 
 /-- MAnalytic functions compose -/
@@ -347,28 +377,13 @@ theorem MAnalyticAt.comp_of_eq {f : N → M} {g : O → N} {x : O} {y : N}
     MAnalyticAt K I (fun x ↦ f (g x)) x := by
   rw [← e] at fh; exact fh.comp gh
 
-/-- `MAnalyticAt` for `x ↦ (f x, g x)` -/
-theorem MAnalyticAt.prod {f : O → M} {g : O → N} {x : O}
-    (fh : MAnalyticAt K I f x) (gh : MAnalyticAt K J g x) :
-    MAnalyticAt K (I.prod J) (fun x ↦ (f x, g x)) x := by
-  rw [mAnalyticAt_iff] at fh gh ⊢; use fh.1.prod gh.1
-  refine (fh.2.prod gh.2).congr_of_eventuallyEq ?_ ?_
-  simp only [eventuallyEq_nhdsWithin_iff]
-  refine .of_forall fun y _ ↦ ?_
-  simp only [extChartAt_prod, Function.comp, PartialEquiv.prod_coe]
-  simp only [mfld_simps]
-
 /-- `MAnalyticAt.comp` for a function of two arguments -/
 theorem MAnalyticAt.comp₂ [CompleteSpace H] {h : N × M → P} {f : O → N}
     {g : O → M} {x : O}
     (ha : MAnalyticAt (J.prod I) L h (f x, g x)) (fa : MAnalyticAt K J f x)
     (ga : MAnalyticAt K I g x) : MAnalyticAt K L (fun x ↦ h (f x, g x)) x :=
   ha.comp (g := fun x ↦ (f x, g x)) (fa.prod ga)
 
-/-- `MAnalytic` for `x ↦ (f x, g x)` -/
-theorem MAnalytic.prod {f : O → M} {g : O → N} (fh : MAnalytic K I f) (gh : MAnalytic K J g) :
-    MAnalytic K (I.prod J) fun x ↦ (f x, g x) := fun x ↦ (fh x).prod (gh x)
-
 /-- `MAnalyticAt.comp₂`, with a separate argument for point equality -/
 theorem MAnalyticAt.comp₂_of_eq [CompleteSpace H] {h : N × M → P} {f : O → N}
     {g : O → M} {x : O} {y : N × M} (ha : MAnalyticAt (J.prod I) L h y) (fa : MAnalyticAt K J f x)
@@ -407,21 +422,6 @@ theorem MAnalyticAt.analyticAt (I : ModelWithCorners 𝕜 E A) [I.Boundaryless]
     MAnalyticAt I J f x → AnalyticAt 𝕜 f x :=
   (analyticAt_iff_mAnalyticAt _ _).mpr
 
-/-- `id` is analytic -/
-theorem mAnalyticAt_id {x : M} : MAnalyticAt I I (fun x ↦ x) x := by
-  rw [mAnalyticAt_iff]
-  use continuousAt_id
-  refine (analyticAt_id _ _).analyticWithinAt.congr_of_eventuallyEq ?_ ?_
-  · simp only [mfld_simps, Filter.EventuallyEq, id, ← I.map_nhds_eq, Filter.eventually_map]
-    filter_upwards [(chartAt A x).open_target.eventually_mem (mem_chart_target _ _)]
-    intro y m
-    simp only [(chartAt A x).right_inv m]
-  · simp only [mfld_simps]
-
-/-- `id` is analytic -/
-theorem mAnalytic_id : MAnalytic I I fun x : M ↦ x :=
-  fun _ ↦ mAnalyticAt_id
-
 /-- Curried analytic functions are analytic in the first coordinate -/
 theorem MAnalyticAt.along_fst [CompleteSpace G] [CompleteSpace H] [AnalyticManifold I M]
     {f : M → O → P} {x : M} {y : O} (fa : MAnalyticAt (I.prod K) L (uncurry f) (x, y)) :
@@ -521,10 +521,11 @@ theorem MAnalyticAt.eventually [I.Boundaryless] [J.Boundaryless] [AnalyticManifo
   clear a
   have h' := (MAnalyticAt.extChartAt_symm (PartialEquiv.map_source _ fm.self_of_nhds)).comp_of_eq
       (h.comp (MAnalyticAt.extChartAt m)) ?_
-  · apply h'.congr; clear h h'
+  · apply h'.congr
+    clear h h'
     apply ((isOpen_extChartAt_source I x).eventually_mem m).mp
     refine fm.mp (.of_forall fun z mf m ↦ ?_)
-    simp only [PartialEquiv.left_inv _ m, PartialEquiv.left_inv _ mf]
+    simp only [PartialEquiv.left_inv _ m, PartialEquiv.left_inv _ mf, Function.comp_def]
   · simp only [Function.comp, PartialEquiv.left_inv _ m]
 
 /-- The domain of analyticity is open -/

Ray/AnalyticManifold/GlobalInverse.lean

@@ -120,7 +120,7 @@ theorem weak_global_complex_inverse_fun_open {f : S → T} [Nonempty S] {s : Set
   rcases global_complex_inverse_fun_open fa' nc' inj' (isOpen_univ.prod so) with ⟨g, ga, gf⟩
   use g 0; constructor
   · intro z ⟨w, m⟩; refine (ga ⟨0, z⟩ ⟨⟨0, w⟩, ⟨mem_univ _, m.1⟩, ?_⟩).along_snd
-    simp only [Prod.ext_iff, eq_self_iff_true, true_and_iff]; exact m.2
+    simp only [Prod.ext_iff, eq_self_iff_true, true_and]; exact m.2
   · intro z m; exact gf ⟨0, z⟩ ⟨mem_univ _, m⟩
 
 /-- The global 1D inverse function theorem (open case): if `f : S → T` is injective on an

Ray/AnalyticManifold/Inverse.lean

@@ -213,11 +213,11 @@ theorem Cinv.left_inv (i : Cinv f c z) : ∀ᶠ x : ℂ × S in 𝓝 (c, z), i.g
     exact (continuousOn_extChartAt _ _).isOpen_inter_preimage (isOpen_extChartAt_source _ _)
       i.he.open_source
   have m : (c, z) ∈ t := by
-    simp only [mem_inter_iff, mem_preimage, mem_extChartAt_source, true_and_iff, ← ht]
+    simp only [mem_inter_iff, mem_preimage, mem_extChartAt_source, true_and, ← ht]
     exact ContDiffAt.mem_toPartialHomeomorph_source i.ha.contDiffAt i.has_dhe le_top
   apply Filter.eventuallyEq_of_mem (o.mem_nhds m); intro x m
   simp only [mem_inter_iff, mem_preimage, extChartAt_prod, extChartAt_eq_refl, ← ht,
-    PartialEquiv.prod_source, PartialEquiv.refl_source, mem_prod_eq, mem_univ, true_and_iff,
+    PartialEquiv.prod_source, PartialEquiv.refl_source, mem_prod_eq, mem_univ, true_and,
     PartialEquiv.prod_coe, PartialEquiv.refl_coe, id] at m
   have inv := i.he.left_inv m.2
   simp only [Cinv.g]
@@ -249,7 +249,7 @@ theorem Cinv.right_inv (i : Cinv f c z) :
       simp only [Cinv.h, Cinv.z', Cinv.f', PartialEquiv.left_inv _ (mem_extChartAt_source _ _)]
     rw [e] at m; exact m
   have m : (c, f c z) ∈ t := by
-    simp only [m', mem_inter_iff, mem_preimage, mem_extChartAt_source, true_and_iff, ← ht,
+    simp only [m', mem_inter_iff, mem_preimage, mem_extChartAt_source, true_and, ← ht,
       extChartAt_prod, PartialEquiv.prod_coe, extChartAt_eq_refl, PartialEquiv.refl_coe, id,
       PartialEquiv.prod_source, prod_mk_mem_set_prod_eq, PartialEquiv.refl_source, mem_univ]
   have fm : ∀ᶠ x : ℂ × T in 𝓝 (c, f c z),
@@ -273,7 +273,7 @@ theorem Cinv.right_inv (i : Cinv f c z) :
   refine fm.mp (Filter.eventually_of_mem (o.mem_nhds m) ?_)
   intro x m mf
   simp only [mem_inter_iff, mem_preimage, extChartAt_prod, extChartAt_eq_refl,
-    PartialEquiv.prod_source, PartialEquiv.refl_source, mem_prod_eq, mem_univ, true_and_iff,
+    PartialEquiv.prod_source, PartialEquiv.refl_source, mem_prod_eq, mem_univ, true_and,
     PartialEquiv.prod_coe, PartialEquiv.refl_coe, id, ← ht] at m
   have inv := i.he.right_inv m.2
   simp only [Cinv.g]

Ray/AnalyticManifold/Nonseparating.lean

@@ -33,15 +33,15 @@ theorem Nonseparating.univ_prod [LocallyConnectedSpace X] {t : Set Y} (n : Nonse
     Nonseparating ((univ : Set X) ×ˢ t) := by
   have e : ((univ : Set X) ×ˢ t)ᶜ = univ ×ˢ tᶜ := by
     apply Set.ext; intro ⟨a, x⟩; rw [mem_compl_iff]
-    simp only [prod_mk_mem_set_prod_eq, mem_univ, mem_compl_iff, true_and_iff]
+    simp only [prod_mk_mem_set_prod_eq, mem_univ, mem_compl_iff, true_and]
   constructor; · rw [e]; exact dense_univ.prod n.dense
-  · intro ⟨a, x⟩ u m un; simp only [mem_prod_eq, mem_univ, true_and_iff] at m
+  · intro ⟨a, x⟩ u m un; simp only [mem_prod_eq, mem_univ, true_and] at m
     rcases mem_nhds_prod_iff.mp un with ⟨u0, n0, u1, n1, uu⟩
     rcases n.loc x u1 m n1 with ⟨c1, cs1, cn1, cp1⟩
     rcases locallyConnectedSpace_iff_open_connected_subsets.mp (by infer_instance) a u0 n0 with
       ⟨c0, cs0, co0, cm0, cc0⟩
     use c0 ×ˢ c1; refine ⟨?_, ?_, ?_⟩
-    · intro ⟨b, y⟩ m'; simp only [mem_prod_eq, mem_diff, mem_univ, true_and_iff] at m' ⊢
+    · intro ⟨b, y⟩ m'; simp only [mem_prod_eq, mem_diff, mem_univ, true_and] at m' ⊢
       refine ⟨?_, (cs1 m'.2).2⟩; apply uu; use cs0 m'.1, (cs1 m'.2).1
     · rw [e, nhdsWithin_prod_eq, nhdsWithin_univ]; exact Filter.prod_mem_prod (co0.mem_nhds cm0) cn1
     · exact cc0.isPreconnected.prod cp1
@@ -61,17 +61,17 @@ theorem Nonseparating.complexManifold {t : Set S}
           (isOpen_extChartAt_target I z) uo
       have vn : v.Nonempty := by
         use extChartAt I z z
-        simp only [mem_inter_iff, mem_extChartAt_target, true_and_iff, mem_preimage,
+        simp only [mem_inter_iff, mem_extChartAt_target, true_and, mem_preimage,
           PartialEquiv.left_inv _ (mem_extChartAt_source I z), m, ← hv]
       rcases dense_iff_inter_open.mp (h z).dense v vo vn with ⟨y, m⟩
       use(extChartAt I z).symm y
       simp only [mem_inter_iff, mem_preimage, mem_compl_iff, not_and, ← hv] at m
       rcases m with ⟨⟨ym, yu⟩, yt⟩
-      simp only [mem_inter_iff, ym, yu, true_and_iff, mem_compl_iff]; exact yt ym
+      simp only [mem_inter_iff, ym, yu, true_and, mem_compl_iff]; exact yt ym
     loc := by
       intro z u zt un
       have m : extChartAt I z z ∈ (extChartAt I z).target ∩ (extChartAt I z).symm ⁻¹' t := by
-        simp only [mem_inter_iff, mem_extChartAt_target I z, true_and_iff, mem_preimage,
+        simp only [mem_inter_iff, mem_extChartAt_target I z, true_and, mem_preimage,
           PartialEquiv.left_inv _ (mem_extChartAt_source I z), zt]
       have n : (extChartAt I z).target ∩ (extChartAt I z).symm ⁻¹' u ∈ 𝓝 (extChartAt I z z) := by
         apply Filter.inter_mem
@@ -88,7 +88,7 @@ theorem Nonseparating.complexManifold {t : Set S}
       use(extChartAt I z).source ∩ extChartAt I z ⁻¹' c; refine ⟨?_, ?_, ?_⟩
       · intro x xm; simp only [mem_inter_iff, mem_preimage] at xm; rcases xm with ⟨xz, xc⟩
         replace xc := cs xc
-        simp only [mem_diff, mem_inter_iff, mem_preimage, PartialEquiv.map_source _ xz, true_and_iff,
+        simp only [mem_diff, mem_inter_iff, mem_preimage, PartialEquiv.map_source _ xz, true_and,
           PartialEquiv.left_inv _ xz] at xc
         exact xc
       · rw [e]; convert Filter.image_mem_map cn
@@ -104,7 +104,7 @@ theorem Nonseparating.complexManifold {t : Set S}
           simp only [PartialEquiv.left_inv _ xz, xt, PartialEquiv.map_source _ xz, not_false_iff,
             and_self_iff, eq_self_iff_true]
         · intro ⟨⟨y, ⟨⟨yz, yt⟩, yx⟩⟩, _⟩
-          simp only [← yx, yt, PartialEquiv.map_target _ yz, not_false_iff, true_and_iff]
+          simp only [← yx, yt, PartialEquiv.map_target _ yz, not_false_iff, true_and]
       · rw [e]; apply cp.image; apply (continuousOn_extChartAt_symm I z).mono
         exact _root_.trans cs (_root_.trans diff_subset inter_subset_left) }
 
@@ -124,11 +124,11 @@ theorem IsPreconnected.open_diff {s t : Set X} (sc : IsPreconnected s) (so : IsO
       exact (o.eventually_mem xu).mp (.of_forall fun q m ↦ subset_union_left m)
     by_cases xt : x ∉ t
     · contrapose xu; clear xu
-      simp only [mem_union, mem_setOf, xt, false_and_iff, and_false_iff, or_false_iff, ← hf] at m
+      simp only [mem_union, mem_setOf, xt, false_and, and_false, or_false, ← hf] at m
       simp only [not_not]; exact m
     simp only [not_not] at xt
     have n := m
-    simp only [mem_union, xt, xu, false_or_iff, true_and_iff, mem_setOf,
+    simp only [mem_union, xt, xu, false_or, true_and, mem_setOf,
       eventually_nhdsWithin_iff, ← hf] at n
     refine (so.eventually_mem n.1).mp (n.2.eventually_nhds.mp (.of_forall fun y n m ↦ ?_))
     by_cases yt : y ∈ t
@@ -148,7 +148,7 @@ theorem IsPreconnected.open_diff {s t : Set X} (sc : IsPreconnected s) (so : IsO
     exact subset_union_right (mem m xt cn cv)
   have fdiff : ∀ {u}, f u \ t ⊆ u := by
     intro u x m; simp only [mem_diff, mem_union, mem_setOf, ← hf] at m
-    simp only [m.2, false_and_iff, and_false_iff, or_false_iff, not_false_iff, and_true_iff] at m
+    simp only [m.2, false_and, and_false, or_false, not_false_iff, and_true] at m
     exact m
   have fnon : ∀ {x u}, IsOpen u → x ∈ f u → ∀ᶠ y in 𝓝[tᶜ] x, y ∈ u := by
     intro x u o m; simp only [mem_union, mem_setOf, ← hf] at m
@@ -181,15 +181,15 @@ theorem IsPreconnected.ball_diff_center {a : ℂ} {r : ℝ} : IsPreconnected (ba
       (fun p : ℝ × ℝ ↦ a + p.1 * Complex.exp (p.2 * Complex.I)) '' Ioo 0 r ×ˢ univ := by
     apply Set.ext; intro z
     simp only [mem_diff, mem_ball, Complex.dist_eq, mem_singleton_iff, mem_image, Prod.exists,
-      mem_prod_eq, mem_Ioo, mem_univ, and_true_iff]
+      mem_prod_eq, mem_Ioo, mem_univ, and_true]
     constructor
     · intro ⟨zr, za⟩; use abs (z - a), Complex.arg (z - a)
       simp only [AbsoluteValue.pos_iff, Ne, Complex.abs_mul_exp_arg_mul_I,
-        add_sub_cancel, eq_self_iff_true, sub_eq_zero, za, zr, not_false_iff, and_true_iff]
+        add_sub_cancel, eq_self_iff_true, sub_eq_zero, za, zr, not_false_iff, and_true]
     · intro ⟨s, t, ⟨s0, sr⟩, e⟩
       simp only [← e, add_sub_cancel_left, Complex.abs.map_mul, Complex.abs_ofReal, abs_of_pos s0,
-        Complex.abs_exp_ofReal_mul_I, mul_one, sr, true_and_iff, add_right_eq_self, mul_eq_zero,
-        Complex.exp_ne_zero, or_false_iff, Complex.ofReal_eq_zero]
+        Complex.abs_exp_ofReal_mul_I, mul_one, sr, true_and, add_right_eq_self, mul_eq_zero,
+        Complex.exp_ne_zero, or_false, Complex.ofReal_eq_zero]
       exact s0.ne'
   rw [e]; apply IsPreconnected.image; exact isPreconnected_Ioo.prod isPreconnected_univ
   apply Continuous.continuousOn; continuity
@@ -204,8 +204,8 @@ theorem Complex.nonseparating_singleton (a : ℂ) : Nonseparating ({a} : Set ℂ
       rcases Metric.isOpen_iff.mp uo a m with ⟨r, rp, rs⟩
       use a + r / 2
       simp only [mem_inter_iff, mem_compl_iff, mem_singleton_iff, add_right_eq_self,
-        div_eq_zero_iff, Complex.ofReal_eq_zero, one_ne_zero, or_false_iff,
-        rp.ne', not_false_iff, and_true_iff, false_or, two_ne_zero]
+        div_eq_zero_iff, Complex.ofReal_eq_zero, one_ne_zero, or_false,
+        rp.ne', not_false_iff, and_true, false_or, two_ne_zero]
       apply rs
       simp only [mem_ball, dist_self_add_left, Complex.norm_eq_abs, map_div₀, Complex.abs_ofReal,
         Complex.abs_two, abs_of_pos rp, half_lt_self rp]
@@ -220,7 +220,7 @@ theorem AnalyticManifold.nonseparating_singleton (a : S) : Nonseparating ({a} :
   apply Nonseparating.complexManifold; intro z
   by_cases az : a ∈ (extChartAt I z).source
   · convert Complex.nonseparating_singleton (extChartAt I z a)
-    simp only [eq_singleton_iff_unique_mem, mem_inter_iff, PartialEquiv.map_source _ az, true_and_iff,
+    simp only [eq_singleton_iff_unique_mem, mem_inter_iff, PartialEquiv.map_source _ az, true_and,
       mem_preimage, mem_singleton_iff, PartialEquiv.left_inv _ az, eq_self_iff_true]
     intro x ⟨m, e⟩; simp only [← e, PartialEquiv.right_inv _ m]
   · convert Nonseparating.empty
@@ -239,5 +239,5 @@ theorem IsPreconnected.open_diff_line {s : Set (ℂ × S)} (sc : IsPreconnected
   apply IsPreconnected.open_diff sc so
   have e : {p : ℂ × S | p.2 = a} = univ ×ˢ {a} := by
     apply Set.ext; intro ⟨c, z⟩
-    simp only [mem_prod_eq, mem_setOf, mem_univ, true_and_iff, mem_singleton_iff]
+    simp only [mem_prod_eq, mem_setOf, mem_univ, true_and, mem_singleton_iff]
   rw [e]; exact Nonseparating.univ_prod (AnalyticManifold.nonseparating_singleton _)