Update lean and mathlib

Ray/Analytic/Analytic.lean

@@ -279,7 +279,7 @@ theorem AnalyticAt.monomial_mul_leadingCoeff {f : 𝕜 → E} {c : 𝕜} (fa : A
 theorem AnalyticAt.fderiv [CompleteSpace F] {f : E → F} {c : E} (fa : AnalyticAt 𝕜 f c) :
     AnalyticAt 𝕜 (fderiv 𝕜 f) c := by
   rcases Metric.isOpen_iff.mp (isOpen_analyticAt 𝕜 f) _ fa with ⟨r, rp, fa⟩
-  exact AnalyticOn.fderiv fa _ (Metric.mem_ball_self rp)
+  exact AnalyticOnNhd.fderiv fa _ (Metric.mem_ball_self rp)
 
 /-- `deriv` is analytic -/
 theorem AnalyticAt.deriv {f : 𝕜 → 𝕜} {c : 𝕜} (fa : AnalyticAt 𝕜 f c) [CompleteSpace 𝕜] :

Ray/Analytic/Holomorphic.lean

@@ -34,7 +34,7 @@ variable {F : Type} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F]
 /-- `f : ℂ × ℂ → E` is differentiable iff it is analytic -/
 theorem differentiable_iff_analytic2 {E : Type} {f : ℂ × ℂ → E} {s : Set (ℂ × ℂ)}
     [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (o : IsOpen s) :
-    DifferentiableOn ℂ f s ↔ AnalyticOn ℂ f s := by
+    DifferentiableOn ℂ f s ↔ AnalyticOnNhd ℂ f s := by
   constructor
   · intro d; apply osgood o d.continuousOn
     · intro z0 z1 zs

Ray/Analytic/HolomorphicUpstream.lean

@@ -29,23 +29,23 @@ variable {G : Type} [NormedAddCommGroup G] [NormedSpace ℂ G]
 
 /-- A function is analytic at `z` iff it's differentiable on a surrounding open set -/
 theorem analyticOn_iff_differentiableOn {f : ℂ → E} {s : Set ℂ} (o : IsOpen s) :
-    AnalyticOn ℂ f s ↔ DifferentiableOn ℂ f s := by
+    AnalyticOnNhd ℂ f s ↔ DifferentiableOn ℂ f s := by
   constructor
-  · exact AnalyticOn.differentiableOn
+  · exact AnalyticOnNhd.differentiableOn
   · intro d z zs
     exact DifferentiableOn.analyticAt d (o.mem_nhds zs)
 
 /-- A function is entire iff it's differentiable everywhere -/
 theorem analyticOn_univ_iff_differentiable {f : ℂ → E} :
-    AnalyticOn ℂ f univ ↔ Differentiable ℂ f := by
+    AnalyticOnNhd ℂ f univ ↔ Differentiable ℂ f := by
   simp only [←  differentiableOn_univ]
   exact analyticOn_iff_differentiableOn isOpen_univ
 
 /-- A function is analytic at `z` iff it's differentiable on near `z` -/
 theorem analyticAt_iff_eventually_differentiableAt {f : ℂ → E} {c : ℂ} :
     AnalyticAt ℂ f c ↔ ∀ᶠ z in 𝓝 c, DifferentiableAt ℂ f z := by
   constructor
-  · intro fa; rcases fa.exists_ball_analyticOn with ⟨r, rp, fa⟩
+  · intro fa; rcases fa.exists_ball_analyticOnNhd with ⟨r, rp, fa⟩
     exact fa.differentiableOn.eventually_differentiableAt (Metric.ball_mem_nhds _ rp)
   · intro d; rcases Metric.eventually_nhds_iff.mp d with ⟨r, rp, d⟩
     have dr : DifferentiableOn ℂ f (ball c r) := by
@@ -54,12 +54,12 @@ theorem analyticAt_iff_eventually_differentiableAt {f : ℂ → E} {c : ℂ} :
     exact dr _ (Metric.mem_ball_self rp)
 
 /-- `exp` is entire -/
-theorem AnalyticOn.exp : AnalyticOn ℂ exp univ := by
+theorem AnalyticOnNhd.exp : AnalyticOnNhd ℂ exp univ := by
   rw [analyticOn_univ_iff_differentiable]; exact Complex.differentiable_exp
 
 /-- `exp` is analytic at any point -/
 theorem AnalyticAt.exp {z : ℂ} : AnalyticAt ℂ exp z :=
-  AnalyticOn.exp z (Set.mem_univ _)
+  AnalyticOnNhd.exp z (Set.mem_univ _)
 
 /-- `log` is analytic away from nonpositive reals -/
 theorem analyticAt_log {c : ℂ} (m : c ∈ Complex.slitPlane) : AnalyticAt ℂ log c := by
@@ -74,8 +74,8 @@ theorem AnalyticAt.log {f : G → ℂ} {c : G} (fa : AnalyticAt ℂ f c) (m : f
   (analyticAt_log m).comp fa
 
 /-- `log` is analytic away from nonpositive reals -/
-theorem AnalyticOn.log {f : G → ℂ} {s : Set G} (fs : AnalyticOn ℂ f s)
-    (m : ∀ z ∈ s, f z ∈ Complex.slitPlane) : AnalyticOn ℂ (fun z ↦ log (f z)) s :=
+theorem AnalyticOnNhd.log {f : G → ℂ} {s : Set G} (fs : AnalyticOnNhd ℂ f s)
+    (m : ∀ z ∈ s, f z ∈ Complex.slitPlane) : AnalyticOnNhd ℂ (fun z ↦ log (f z)) s :=
   fun z n ↦ (analyticAt_log (m z n)).comp (fs z n)
 
 /-- `f z ^ g z` is analytic if `f z` is not a nonpositive real -/

Ray/Analytic/Products.lean

@@ -54,9 +54,9 @@ theorem HasProdOn.tprodOn_eq {f : ℕ → ℂ → ℂ} {g : ℂ → ℂ} {s : Se
     For now, we require the constant to be `≤ 1/2` so that we can take logs without
     care, and get nonzero results. -/
 theorem fast_products_converge {f : ℕ → ℂ → ℂ} {s : Set ℂ} {a c : ℝ} (o : IsOpen s)
-    (c12 : c ≤ 1 / 2) (a0 : a ≥ 0) (a1 : a < 1) (h : ∀ n, AnalyticOn ℂ (f n) s)
+    (c12 : c ≤ 1 / 2) (a0 : a ≥ 0) (a1 : a < 1) (h : ∀ n, AnalyticOnNhd ℂ (f n) s)
     (hf : ∀ n z, z ∈ s → abs (f n z - 1) ≤ c * a ^ n) :
-    ∃ g : ℂ → ℂ, HasProdOn f g s ∧ AnalyticOn ℂ g s ∧ ∀ z, z ∈ s → g z ≠ 0 := by
+    ∃ g : ℂ → ℂ, HasProdOn f g s ∧ AnalyticOnNhd ℂ g s ∧ ∀ z, z ∈ s → g z ≠ 0 := by
   set fl := fun n z ↦ log (f n z)
   have near1 : ∀ n z, z ∈ s → abs (f n z - 1) ≤ 1 / 2 := by
     intro n z zs
@@ -69,7 +69,7 @@ theorem fast_products_converge {f : ℕ → ℂ → ℂ} {s : Set ℂ} {a c : 
   have expfl : ∀ n z, z ∈ s → exp (fl n z) = f n z := by
     intro n z zs; refine Complex.exp_log ?_
     exact near_one_avoids_zero (near1' n z zs)
-  have hl : ∀ n, AnalyticOn ℂ (fl n) s := fun n ↦
+  have hl : ∀ n, AnalyticOnNhd ℂ (fl n) s := fun n ↦
     (h n).log (fun z m ↦ mem_slitPlane_of_near_one (near1' n z m))
     --fun n ↦ log_analytic_near_one o (h n) (near1' n)
   set c2 := 2 * c
@@ -98,9 +98,9 @@ theorem fast_products_converge {f : ℕ → ℂ → ℂ} {s : Set ℂ} {a c : 
 
 /-- Same as above, but converge to `tprodOn` -/
 theorem fast_products_converge' {f : ℕ → ℂ → ℂ} {s : Set ℂ} {c a : ℝ} (o : IsOpen s)
-    (c12 : c ≤ 1 / 2) (a0 : 0 ≤ a) (a1 : a < 1) (h : ∀ n, AnalyticOn ℂ (f n) s)
+    (c12 : c ≤ 1 / 2) (a0 : 0 ≤ a) (a1 : a < 1) (h : ∀ n, AnalyticOnNhd ℂ (f n) s)
     (hf : ∀ n z, z ∈ s → abs (f n z - 1) ≤ c * a ^ n) :
-    ProdExistsOn f s ∧ AnalyticOn ℂ (tprodOn f) s ∧ ∀ z, z ∈ s → tprodOn f z ≠ 0 := by
+    ProdExistsOn f s ∧ AnalyticOnNhd ℂ (tprodOn f) s ∧ ∀ z, z ∈ s → tprodOn f z ≠ 0 := by
   rcases fast_products_converge o c12 a0 a1 h hf with ⟨g, gp, ga, g0⟩
   refine ⟨?_, ?_, ?_⟩
   · exact fun z zs ↦ ⟨g z, gp z zs⟩

Ray/Analytic/Series.lean

@@ -153,10 +153,10 @@ theorem fast_series_converge_at {f : ℕ → ℂ} {c a : ℝ} (a0 : 0 ≤ a) (a1
 
 /-- Analytic series that converge exponentially converge to analytic functions -/
 theorem fast_series_converge {f : ℕ → ℂ → ℂ} {s : Set ℂ} {c a : ℝ} (o : IsOpen s) (a0 : 0 ≤ a)
-    (a1 : a < 1) (h : ∀ n, AnalyticOn ℂ (f n) s) (hf : ∀ n z, z ∈ s → abs (f n z) ≤ c * a ^ n) :
-    ∃ g : ℂ → ℂ, AnalyticOn ℂ g s ∧ HasSumOn f g s := by
+    (a1 : a < 1) (h : ∀ n, AnalyticOnNhd ℂ (f n) s) (hf : ∀ n z, z ∈ s → abs (f n z) ≤ c * a ^ n) :
+    ∃ g : ℂ → ℂ, AnalyticOnNhd ℂ g s ∧ HasSumOn f g s := by
   use tsumOn f; constructor
-  · exact uniform_analytic_lim o (fun N ↦ N.analyticOn_sum fun _ _ ↦ h _)
+  · exact uniform_analytic_lim o (fun N ↦ N.analyticOnNhd_sum fun _ _ ↦ h _)
       (fast_series_converge_uniformly_on a0 a1 hf)
   · exact fun z zs ↦ Summable.hasSum (fast_series_converge_at a0 a1 fun n ↦ hf n z zs)
 

Ray/Analytic/Uniform.lean

@@ -28,28 +28,28 @@ open scoped Real NNReal Topology
 noncomputable section
 
 theorem cauchy_on_cball_radius {f : ℂ → ℂ} {z : ℂ} {r : ℝ≥0} (rp : r > 0)
-    (h : AnalyticOn ℂ f (closedBall z r)) :
+    (h : AnalyticOnNhd ℂ f (closedBall z r)) :
     HasFPowerSeriesOnBall f (cauchyPowerSeries f z r) z r := by
   have hd : DifferentiableOn ℂ f (closedBall z r) := by
     intro x H; exact AnalyticAt.differentiableWithinAt (h x H)
   set p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries f z r
   exact DifferentiableOn.hasFPowerSeriesOnBall hd rp
 
 theorem analyticOn_cball_radius {f : ℂ → ℂ} {z : ℂ} {r : ℝ≥0} (rp : r > 0)
-    (h : AnalyticOn ℂ f (closedBall z r)) :
+    (h : AnalyticOnNhd ℂ f (closedBall z r)) :
     ∃ p : FormalMultilinearSeries ℂ ℂ ℂ, HasFPowerSeriesOnBall f p z r :=
   ⟨cauchyPowerSeries f z r, cauchy_on_cball_radius rp h⟩
 
-theorem analyticOn_small_cball {f : ℂ → ℂ} {z : ℂ} {r : ℝ≥0} (h : AnalyticOn ℂ f (ball z r))
-    (s : ℝ≥0) (sr : s < r) : AnalyticOn ℂ f (closedBall z s) := by
+theorem analyticOn_small_cball {f : ℂ → ℂ} {z : ℂ} {r : ℝ≥0} (h : AnalyticOnNhd ℂ f (ball z r))
+    (s : ℝ≥0) (sr : s < r) : AnalyticOnNhd ℂ f (closedBall z s) := by
   intro x hx
   rw [closedBall] at hx; simp at hx
   have hb : x ∈ ball z r := by
     rw [ball]; simp only [dist_lt_coe, Set.mem_setOf_eq]; exact lt_of_le_of_lt hx sr
   exact h x hb
 
 theorem analyticOn_ball_radius {f : ℂ → ℂ} {z : ℂ} {r : ℝ≥0} (rp : r > 0)
-    (h : AnalyticOn ℂ f (ball z r)) :
+    (h : AnalyticOnNhd ℂ f (ball z r)) :
     ∃ p : FormalMultilinearSeries ℂ ℂ ℂ, HasFPowerSeriesOnBall f p z r := by
   have h0 := analyticOn_small_cball h (r / 2) (NNReal.half_lt_self <| rp.ne')
   rcases analyticOn_cball_radius (half_pos rp) h0 with ⟨p, ph⟩
@@ -184,20 +184,20 @@ theorem cauchy_dist {f g : ℂ → ℂ} {c : ℂ} {r : ℝ≥0} {d : ℝ≥0} (n
 
 /-- Uniform limits of analytic functions are analytic -/
 theorem uniform_analytic_lim {I : Type} [Lattice I] [Nonempty I] {f : I → ℂ → ℂ} {g : ℂ → ℂ}
-    {s : Set ℂ} (o : IsOpen s) (h : ∀ n, AnalyticOn ℂ (f n) s)
-    (u : TendstoUniformlyOn f g atTop s) : AnalyticOn ℂ g s := by
+    {s : Set ℂ} (o : IsOpen s) (h : ∀ n, AnalyticOnNhd ℂ (f n) s)
+    (u : TendstoUniformlyOn f g atTop s) : AnalyticOnNhd ℂ g s := by
   intro c hc
   rcases Metric.nhds_basis_closedBall.mem_iff.mp (o.mem_nhds hc) with ⟨r, rp, cb⟩
   lift r to ℝ≥0 using rp.le
   simp only [NNReal.coe_pos] at rp
-  have hb : ∀ n, AnalyticOn ℂ (f n) (closedBall c r) := fun n ↦ (h n).mono cb
+  have hb : ∀ n, AnalyticOnNhd ℂ (f n) (closedBall c r) := fun n ↦ (h n).mono cb
   set pr := fun n ↦ cauchyPowerSeries (f n) c r
   have hpf : ∀ n, HasFPowerSeriesOnBall (f n) (pr n) c r := by
     intro n
     have cs := cauchy_on_cball_radius rp (hb n)
     have pn : pr n = cauchyPowerSeries (f n) c r := rfl
     rw [← pn] at cs; exact cs
-  have cfs : ∀ n, ContinuousOn (f n) s := fun n ↦ AnalyticOn.continuousOn (h n)
+  have cfs : ∀ n, ContinuousOn (f n) s := fun n ↦ AnalyticOnNhd.continuousOn (h n)
   have cf : ∀ n, ContinuousOn (f n) (closedBall c r) := fun n ↦ ContinuousOn.mono (cfs n) cb
   have cg : ContinuousOn g (closedBall c r) :=
     ContinuousOn.mono (TendstoUniformlyOn.continuousOn u (.of_forall cfs)) cb

Ray/AnalyticManifold/AnalyticManifold.lean

@@ -62,14 +62,14 @@ lemma ModelWithCorners.prod_apply' {E H E' H' : Type*} [NormedAddCommGroup E] [N
     This lemma helps when proving particular spaces are analytic manifolds. -/
 theorem extChartAt_self_analytic {E : Type} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
     {M : Type} [TopologicalSpace M] (f : PartialHomeomorph M E) :
-    AnalyticOn 𝕜 (𝓘(𝕜, E) ∘ (f.symm.trans f) ∘ ⇑𝓘(𝕜, E).symm)
+    AnalyticOnNhd 𝕜 (𝓘(𝕜, E) ∘ (f.symm.trans f) ∘ ⇑𝓘(𝕜, E).symm)
       (𝓘(𝕜, E) '' (f.symm.trans f).toPartialEquiv.source) := by
-  apply AnalyticOn.congr (f := fun z ↦ z)
+  apply AnalyticOnNhd.congr (f := fun z ↦ z)
   · simp only [modelWithCornersSelf_coe, id_eq, image_id', PartialHomeomorph.trans_toPartialEquiv,
       PartialHomeomorph.symm_toPartialEquiv, PartialEquiv.trans_source, PartialEquiv.symm_source,
       PartialHomeomorph.coe_coe_symm]
     exact f.isOpen_inter_preimage_symm f.open_source
-  · exact analyticOn_id _
+  · exact analyticOnNhd_id
   · intro x m
     simp only [modelWithCornersSelf_coe, id, image_id', PartialHomeomorph.trans_toPartialEquiv,
       PartialHomeomorph.symm_toPartialEquiv, PartialEquiv.trans_source, PartialEquiv.symm_source,
@@ -172,7 +172,7 @@ theorem mAnalyticAt_fst [I.Boundaryless] [J.Boundaryless] {x : M × N} :
     MAnalyticAt (I.prod J) I (fun p : M × N ↦ p.fst) x := by
   rw [mAnalyticAt_iff]
   use continuousAt_fst
-  refine ((analyticAt_fst _).congr ?_).analyticWithinAt
+  refine (analyticAt_fst.congr ?_).analyticWithinAt
   filter_upwards [((isOpen_extChartAt_target _ x).eventually_mem (mem_extChartAt_target _ _))]
   intro y m
   rw [extChartAt_prod] at m
@@ -185,7 +185,7 @@ theorem mAnalyticAt_snd [I.Boundaryless] [J.Boundaryless] {x : M × N} :
     MAnalyticAt (I.prod J) J (fun p : M × N ↦ p.snd) x := by
   rw [mAnalyticAt_iff]
   use continuousAt_snd
-  refine ((analyticAt_snd _).congr ?_).analyticWithinAt
+  refine (analyticAt_snd.congr ?_).analyticWithinAt
   filter_upwards [((isOpen_extChartAt_target _ x).eventually_mem (mem_extChartAt_target _ _))]
   intro y m
   rw [extChartAt_prod] at m
@@ -326,7 +326,7 @@ theorem MAnalytic.prod {f : O → M} {g : O → N} (fh : MAnalytic K I f) (gh :
 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 ?_ ?_
+  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
@@ -337,8 +337,6 @@ theorem mAnalyticAt_id {x : M} : MAnalyticAt I I (fun x ↦ x) x := by
 theorem mAnalytic_id : MAnalytic I I fun x : M ↦ x :=
   fun _ ↦ mAnalyticAt_id
 
-variable [CompleteSpace E] [CompleteSpace F]
-
 /-- MAnalytic functions compose -/
 theorem MAnalyticAt.comp {f : N → M} {g : O → N} {x : O}
     (fh : MAnalyticAt J I f (g x)) (gh : MAnalyticAt K J g x) :
@@ -453,27 +451,27 @@ theorem MAnalyticAt.add [CompleteSpace G] {f g : O → F} {x : O}
     MAnalyticAt K (modelWithCornersSelf 𝕜 F) (fun x ↦ f x + g x) x := by
   have e : (fun x ↦ f x + g x) = (fun p : F × F ↦ p.1 + p.2) ∘ fun x ↦ (f x, g x) := rfl
   rw [e]
-  exact (((analyticAt_fst _).add (analyticAt_snd _)).mAnalyticAt _ _).comp (fa.prod ga)
+  exact ((analyticAt_fst.add analyticAt_snd).mAnalyticAt _ _).comp (fa.prod ga)
 
 /-- Subtraction is analytic -/
 theorem MAnalyticAt.sub [CompleteSpace G] {f g : O → F} {x : O}
     (fa : MAnalyticAt K (modelWithCornersSelf 𝕜 F) f x)
     (ga : MAnalyticAt K (modelWithCornersSelf 𝕜 F) g x) :
     MAnalyticAt K (modelWithCornersSelf 𝕜 F) (fun x ↦ f x - g x) x :=
-  (((analyticAt_fst _).sub (analyticAt_snd _)).mAnalyticAt _ _).comp (fa.prod ga)
+  ((analyticAt_fst.sub analyticAt_snd).mAnalyticAt _ _).comp (fa.prod ga)
 
 /-- Multiplication is analytic -/
 theorem MAnalyticAt.mul [CompleteSpace 𝕜] [CompleteSpace G] {f g : O → 𝕜} {x : O}
     (fa : MAnalyticAt K (modelWithCornersSelf 𝕜 𝕜) f x)
     (ga : MAnalyticAt K (modelWithCornersSelf 𝕜 𝕜) g x) :
     MAnalyticAt K (modelWithCornersSelf 𝕜 𝕜) (fun x ↦ f x * g x) x :=
-  (((analyticAt_fst _).mul (analyticAt_snd _)).mAnalyticAt _ _).comp (fa.prod ga)
+  ((analyticAt_fst.mul analyticAt_snd).mAnalyticAt _ _).comp (fa.prod ga)
 
 /-- Inverse is analytic away from zeros -/
 theorem MAnalyticAt.inv [CompleteSpace 𝕜] [CompleteSpace G] {f : O → 𝕜} {x : O}
     (fa : MAnalyticAt K (modelWithCornersSelf 𝕜 𝕜) f x) (f0 : f x ≠ 0) :
     MAnalyticAt K (modelWithCornersSelf 𝕜 𝕜) (fun x ↦ (f x)⁻¹) x :=
-  (((analyticAt_id _ _).inv f0).mAnalyticAt _ _).comp fa
+  ((analyticAt_id.inv f0).mAnalyticAt _ _).comp fa
 
 /-- Division is analytic away from denominator zeros -/
 theorem MAnalyticAt.div [CompleteSpace 𝕜] [CompleteSpace G] {f g : O → 𝕜} {x : O}
@@ -487,7 +485,7 @@ theorem MAnalyticAt.pow [CompleteSpace 𝕜] [CompleteSpace G] {f : O → 𝕜}
     (fa : MAnalyticAt K (modelWithCornersSelf 𝕜 𝕜) f x) {n : ℕ} :
     MAnalyticAt K (modelWithCornersSelf 𝕜 𝕜) (fun x ↦ f x ^ n) x := by
   have e : (fun x ↦ f x ^ n) = (fun z : 𝕜 ↦ z ^ n) ∘ f := rfl
-  rw [e]; exact (((analyticAt_id _ _).pow _).mAnalyticAt _ _).comp fa
+  rw [e]; exact ((analyticAt_id.pow _).mAnalyticAt _ _).comp fa
 
 /-- Complex powers `f x ^ g x` are analytic if `f x` avoids the negative real axis  -/
 theorem MAnalyticAt.cpow {E A M : Type} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
@@ -498,14 +496,16 @@ theorem MAnalyticAt.cpow {E A M : Type} [NormedAddCommGroup E] [NormedSpace ℂ
     MAnalyticAt I (modelWithCornersSelf ℂ ℂ) (fun x ↦ f x ^ g x) x := by
   have e : (fun x ↦ f x ^ g x) = (fun p : ℂ × ℂ ↦ p.1 ^ p.2) ∘ fun x ↦ (f x, g x) := rfl
   rw [e]
-  refine (((analyticAt_fst _).cpow (analyticAt_snd _) ?_).mAnalyticAt _ _).comp (fa.prod ga)
+  refine ((analyticAt_fst.cpow analyticAt_snd ?_).mAnalyticAt _ _).comp (fa.prod ga)
   exact a
 
 /-- Iterated analytic functions are analytic -/
 theorem MAnalytic.iter {f : M → M} (fa : MAnalytic I I f) (n : ℕ) : MAnalytic I I f^[n] := by
   induction' n with n h; simp only [Function.iterate_zero]; exact mAnalytic_id
   simp only [Function.iterate_succ']; exact fa.comp h
 
+variable [CompleteSpace E] [CompleteSpace F]
+
 /-- If we're analytic at a point, we're locally analytic.
 This is true even with boundary, but for now we prove only the `Boundaryless` case. -/
 theorem MAnalyticAt.eventually [I.Boundaryless] [J.Boundaryless] [AnalyticManifold I M]

Ray/AnalyticManifold/Inverse.lean

@@ -62,7 +62,7 @@ theorem Cinv.fa' (i : Cinv f c z) : AnalyticAt ℂ i.f' (c, i.z') := by
   simp only [mAnalyticAt_iff_of_boundaryless, uncurry, extChartAt_prod, Function.comp,
     PartialEquiv.prod_coe_symm, PartialEquiv.prod_coe] at fa
   exact fa.2
-theorem Cinv.ha (i : Cinv f c z) : AnalyticAt ℂ i.h (c, i.z') := (analyticAt_fst _).prod i.fa'
+theorem Cinv.ha (i : Cinv f c z) : AnalyticAt ℂ i.h (c, i.z') := analyticAt_fst.prod i.fa'
 
 /-- The key nonzero derivative: `d(f c z)/dz` -/
 @[nolint unusedArguments]