Bump to Lean v4.33.0 / Mathlib v4.33.0

.gitignore

@@ -1 +1,2 @@
 .lake
+*.log

Ray/Analytic/Analytic.lean

@@ -44,7 +44,7 @@ public lemma AnalyticWithinAt.analyticAt {f : E → F} {s : Set E} {x : E}
   obtain ⟨e, e0, es⟩ := Metric.mem_nhds_iff.mp xs
   refine ⟨p, min r (.ofReal e),
     {r_le := by simp [fp.r_le], r_pos := by simp [fp.r_pos, e0], hasSum := fun {y} yr ↦ ?_}⟩
-  simp only [EMetric.mem_ball, edist_zero_right, lt_inf_iff] at yr
+  simp only [Metric.mem_eball, edist_zero_right, lt_inf_iff] at yr
   obtain ⟨yr, ye⟩ := yr
   simp only [← ofReal_norm, ENNReal.ofReal_lt_ofReal_iff e0] at ye
   exact fp.hasSum (.inr (es (by simp [ye]))) (by simp [yr])
@@ -59,12 +59,6 @@ public lemma ContDiffOn.analyticOnNhd {f : E → F} {s : Set E} (fa : ContDiffOn
     (os : IsOpen s) : AnalyticOnNhd 𝕜 f s :=
   fun x xs ↦ (fa x xs).analyticWithinAt.analyticAt (os.mem_nhds xs)
 
-public lemma AnalyticAt.div_const {f : E → 𝕜} {c : E} (fa : AnalyticAt 𝕜 f c) {w : 𝕜} :
-    AnalyticAt 𝕜 (fun z ↦ f z / w) c := by
-  by_cases w0 : w = 0
-  · simp only [w0, div_zero, analyticAt_const]
-  · exact fa.div analyticAt_const w0
-
 public lemma AnalyticAt.dslope {f : 𝕜 → E} {c x : 𝕜} (fa : AnalyticAt 𝕜 f x) :
     AnalyticAt 𝕜 (dslope f c) x := by
   by_cases e : x = c
@@ -100,7 +94,7 @@ public theorem orderAt_eq_zero {f : 𝕜 → E} {c : 𝕜} (f0 : f c ≠ 0) : or
   · rcases fp with ⟨p, fp⟩; rw [fp.orderAt_unique]; rw [← fp.coeff_zero 1] at f0
     rw [FormalMultilinearSeries.order_eq_zero_iff']; right
     contrapose f0
-    simp only [f0, ContinuousMultilinearMap.zero_apply]
+    simp only [f0, _root_.zero_apply]
   · simp [orderAt, fp]
 
 /-- `orderAt = 0` means either `f = 0` or `f c ≠ 0` -/
@@ -143,13 +137,12 @@ public theorem AnalyticAt.leading_approx {f : 𝕜 → E} {c : 𝕜} (fa : Analy
   simp_rw [← fp.orderAt_unique, hd] at e
   apply Asymptotics.IsLittleO.of_isBigOWith; intro k kp
   rw [Asymptotics.isBigOWith_iff]
-  apply e.mp
   have dc : ContinuousAt ((Function.swap _root_.dslope c)^[d] f) c :=
     (fp.has_fpower_series_iterate_dslope_fslope d).analyticAt.continuousAt
   rcases Metric.continuousAt_iff.mp dc k kp with ⟨r, rp, rh⟩
   rw [ha'] at rh
   generalize hg : (Function.swap _root_.dslope c)^[d] f = g; rw [hg] at rh
-  rw [Metric.eventually_nhds_iff]; use r, rp; intro y yr fe; rw [fe]
+  rw [Metric.eventually_nhds_iff]; use r, rp; intro y yr; rw [e y, hg]
   specialize rh yr; rw [dist_eq_norm] at rh
   calc ‖(y - c) ^ d • g y - (y - c) ^ d • a‖
     _ = ‖(y - c) ^ d‖ * ‖g y - a‖ := by rw [←smul_sub, norm_smul]
@@ -174,7 +167,8 @@ def FormalMultilinearSeries.unshift' (p : FormalMultilinearSeries 𝕜 𝕜 E) (
 lemma FormalMultilinearSeries.unshift_coeff_zero (p : FormalMultilinearSeries 𝕜 𝕜 E) (c : E) :
     (p.unshift' c).coeff 0 = c := by
   simp only [FormalMultilinearSeries.coeff, FormalMultilinearSeries.unshift',
-    FormalMultilinearSeries.unshift, continuousMultilinearCurryFin0_symm_apply]
+    FormalMultilinearSeries.unshift, continuousMultilinearCurryFin0_symm_apply,
+    ContinuousMultilinearMap.uncurry0_apply]
 
 @[simp]
 lemma FormalMultilinearSeries.unshift_coeff_succ (p : FormalMultilinearSeries 𝕜 𝕜 E) (c : E)
@@ -190,7 +184,7 @@ def FormalMultilinearSeries.unshiftIter (p : FormalMultilinearSeries 𝕜 𝕜 E
 lemma FormalMultilinearSeries.unshiftIter_coeff (p : FormalMultilinearSeries 𝕜 𝕜 E) (n : ℕ)
     (i : ℕ) : (p.unshiftIter n).coeff i = if i < n then 0 else p.coeff (i - n) := by
   revert i; induction' n with n h
-  · simp only [FormalMultilinearSeries.unshiftIter, Function.iterate_zero, id_eq, not_lt_zero',
+  · simp only [FormalMultilinearSeries.unshiftIter, Function.iterate_zero, id_eq, not_lt_zero,
     tsub_zero, if_false, forall_const]
   · simp_rw [FormalMultilinearSeries.unshiftIter] at h
     simp only [FormalMultilinearSeries.unshiftIter, Function.iterate_succ', Function.comp]
@@ -278,7 +272,7 @@ public theorem AnalyticAt.monomial_mul_orderAt {f : 𝕜 → E} {c : 𝕜} (fa :
   have pnz : p ≠ 0 := by
     contrapose fnz
     simpa only [HasFPowerSeriesAt.locally_zero_iff fp, Filter.not_frequently, not_not]
-  have pe : ∃ i, p i ≠ 0 := by rw [Function.ne_iff] at pnz; exact pnz
+  have pe : ∃ i, p i ≠ 0 := by contrapose! pnz; exact FormalMultilinearSeries.ext pnz
   have pne : ∃ i, (p.unshiftIter n) i ≠ 0 := by
     rcases pe with ⟨i, pi⟩; use n + i
     simp only [FormalMultilinearSeries.ne_zero_iff_coeff_ne_zero] at pi ⊢
@@ -290,7 +284,7 @@ public theorem AnalyticAt.monomial_mul_orderAt {f : 𝕜 → E} {c : 𝕜} (fa :
   · have s := Nat.find_spec pe
     simp only [← p.coeff_eq_zero, Ne] at s
     simp only [p.unshiftIter_coeff, ← FormalMultilinearSeries.coeff_eq_zero, s, Ne,
-      add_lt_iff_neg_left, not_lt_zero', add_tsub_cancel_left, if_false, not_false_iff]
+      add_lt_iff_neg_left, not_lt_zero, add_tsub_cancel_left, if_false, not_false_iff]
   · intro m mp; simp [← FormalMultilinearSeries.coeff_eq_zero, p.unshiftIter_coeff]; intro mn
     generalize ha : m - n = a; have hm : m = n + a := by rw [← ha, add_comm, Nat.sub_add_cancel mn]
     simp only [hm, add_lt_add_iff_left, Nat.lt_find_iff, not_not] at mp
@@ -340,8 +334,10 @@ public theorem AnalyticAt.deriv2 [CompleteSpace 𝕜] {f : E → 𝕜 → 𝕜}
 /-- Scaling commutes with power series -/
 theorem HasFPowerSeriesAt.const_fun_smul {f : 𝕜 → E} {c a : 𝕜} {p : FormalMultilinearSeries 𝕜 𝕜 E}
     (fp : HasFPowerSeriesAt f p c) : HasFPowerSeriesAt (fun z ↦ a • f z) (fun n ↦ a • p n) c := by
+  show HasFPowerSeriesAt (fun z ↦ a • f z) (a • p) c
   rw [hasFPowerSeriesAt_iff] at fp ⊢; refine fp.mp (.of_forall fun z h ↦ ?_)
-  simp only [FormalMultilinearSeries.coeff, ContinuousMultilinearMap.smul_apply, smul_comm _ a]
+  simp only [FormalMultilinearSeries.coeff, FormalMultilinearSeries.smul_apply,
+    _root_.smul_apply, smul_comm _ a]
   exact h.const_smul a
 
 /-- Nonzero scaling does not change analyticitiy -/
@@ -390,7 +386,7 @@ public theorem leadingCoeff_const_smul {f : 𝕜 → E} {c a : 𝕜} :
     simp only [Function.iterate_succ_apply', h, hg]
     funext x; simp only [Function.swap]
     by_cases cx : x = c
-    · simp only [cx, dslope_same, Pi.smul_apply, Pi.smul_def, deriv_fun_const_smul']
+    · simp only [cx, dslope_same, Pi.smul_apply, Pi.smul_def, deriv_fun_const_smul_field]
     · simp only [dslope_of_ne _ cx, Pi.smul_apply, slope, vsub_eq_sub, ← smul_sub, smul_comm _ a]
   simp only [e, Pi.smul_apply]
 

Ray/Analytic/ConjConj.lean

@@ -41,7 +41,7 @@ lemma HasFPowerSeriesOnBall.conj_conj (fa : HasFPowerSeriesOnBall f p (conj z) r
   r_pos := fa.r_pos
   hasSum := by
     intro y m
-    simp only [EMetric.mem_ball, edist_zero_right] at m
+    simp only [Metric.mem_eball, edist_zero_right] at m
     simpa only [FormalMultilinearSeries.conj_conj, ContinuousMultilinearMap.conj_conj_apply, map_add,
       conjCLM_apply] using conjCLM.hasSum (@fa.hasSum (conj y) (by simpa))
 

Ray/Analytic/Holomorphic.lean

@@ -71,31 +71,31 @@ public theorem contDiffAt_iff_analytic_at2 {E : Type} {f : ℂ × ℂ → E} {x
 /-- If `f` is analytic in an open ball, it has a power series over that ball -/
 public lemma analyticOnNhd_ball_iff_hasFPowerSeriesOnBall {f : ℂ → E} {c : ℂ} {r : ℝ≥0∞}
     (r0 : 0 < r) :
-    AnalyticOnNhd ℂ f (EMetric.ball c r) ↔
+    AnalyticOnNhd ℂ f (Metric.eball c r) ↔
       ∃ p : FormalMultilinearSeries ℂ ℂ E, HasFPowerSeriesOnBall f p c r := by
   constructor
   · intro a
-    obtain ⟨p,s,hs⟩ := a c (by simp only [EMetric.mem_ball, edist_self, r0])
+    obtain ⟨p,s,hs⟩ := a c (by simp only [Metric.mem_eball, edist_self, r0])
     have grow : ∀ t : ℝ≥0, 0 < t → t < r → HasFPowerSeriesOnBall f p c t := by
       intro t t0 tr
       have d : DifferentiableOn ℂ f (closedBall c t) := by
         apply (a.mono ?_).differentiableOn
         intro x m
-        simp only [Metric.mem_closedBall, dist_le_coe, EMetric.mem_ball,
+        simp only [Metric.mem_closedBall, dist_le_coe, Metric.mem_eball,
           ← ENNReal.coe_le_coe, ← edist_nndist] at m ⊢
         order
       have ht := d.hasFPowerSeriesOnBall t0
       exact hs.hasFPowerSeriesAt.eq_formalMultilinearSeries ht.hasFPowerSeriesAt ▸ ht
     refine ⟨p, ?_, r0, ?_⟩
     · exact ENNReal.le_of_forall_pos_nnreal_lt fun t t0 tr ↦ (grow t t0 tr).r_le
     · intro y yr
-      simp only [EMetric.mem_ball, edist_zero_right] at yr
+      simp only [Metric.mem_eball, edist_zero_right] at yr
       obtain ⟨t,yt,tr⟩ := ENNReal.lt_iff_exists_nnreal_btwn.mp yr
       have t0 : 0 < t := by
         simp only [enorm_eq_nnnorm, ENNReal.coe_lt_coe] at yt
         exact pos_of_gt yt
       refine (grow t t0 tr).hasSum ?_
-      simp only [Metric.emetric_ball_nnreal, Metric.mem_ball, dist_zero_right]
+      simp only [Metric.eball_coe, Metric.mem_ball, dist_zero_right]
       simpa only [← ofReal_norm, ENNReal.ofReal_lt_coe_iff, norm_nonneg] using yt
   · intro ⟨p,a⟩
     exact a.analyticOnNhd

Ray/Analytic/Integral.lean

@@ -190,7 +190,7 @@ theorem hasFPowerSeriesOnBall_integral (i : Holo f μ s c r) :
     simp only [series, ContinuousMultilinearMap.integral_apply i.integrableOn_cauchyPowerSeries]
     apply MeasureTheory.hasSum_integral_of_summable_integral_norm
     · exact fun _ ↦ i.integrableOn_cauchyPowerSeries_apply
-    · simp only [Metric.emetric_ball_nnreal, Metric.mem_ball, dist_zero_right] at ym
+    · simp only [Metric.eball_coe, Metric.mem_ball, dist_zero_right] at ym
       exact i.summable_cauchyPowerSeries_apply ym
 
 end Holo
@@ -205,7 +205,7 @@ theorem AnalyticOnNhd.integral_ball {r : ℝ} (fc : ContinuousOn (uncurry f) (s
     (μs : μ s ≠ ⊤ := by finiteness) : AnalyticOnNhd ℂ (fun z ↦ ∫ x in s, f x z ∂μ) (ball c r) := by
   set r' : ℝ≥0 := ⟨r, r0.le⟩
   set i : Holo f μ s c r' := ⟨r0, sc, μs, fc, fd⟩
-  have e : ball c r = EMetric.ball c r' := by simp [r']
+  have e : ball c r = Metric.eball c r' := by rw [Metric.eball_coe]; rfl
   rw [e]
   exact i.hasFPowerSeriesOnBall_integral.analyticOnNhd
 

Ray/Analytic/Products.lean

@@ -52,36 +52,51 @@ public theorem product_pow' {f : ℕ → ℂ} {p : ℕ} (h : ProdExists f) :
     tprod f ^ p = tprod fun n ↦ f n ^ p := by
   rcases h with ⟨g, h⟩; rw [HasProd.tprod_eq h]; rw [HasProd.tprod_eq _]; exact product_pow p h
 
-/-- Adding one more term to a product multiplies by it -/
-theorem product_cons {a g : ℂ} {f : ℕ → ℂ} (h : HasProd f g) :
-    HasProd (Stream'.cons a f) (a * g) := by
+/-- Adding one more term to a product multiplies by it, `Stream'.get` version to keep terms
+    type-correct at low transparency -/
+theorem product_cons_get {a t : ℂ} {q : Stream' ℂ} (h : HasProd q.get t) :
+    HasProd (Stream'.cons a q).get (a * t) := by
   rw [HasProd] at h ⊢
-  have ha := Filter.Tendsto.comp (Continuous.tendsto (continuous_mul_left a) g) h
-  have s : ((fun z ↦ a * z) ∘ fun N : Finset ℕ ↦ N.prod f) =
-      (fun N : Finset ℕ ↦ N.prod (Stream'.cons a f)) ∘ push := by
-    apply funext; intro N; simp; exact push_prod
+  have ha := Filter.Tendsto.comp (Continuous.tendsto (continuous_const_mul a) t) h
+  have s : ((fun z ↦ a * z) ∘ fun N : Finset ℕ ↦ N.prod q.get) =
+      (fun N : Finset ℕ ↦ N.prod (Stream'.cons a q).get) ∘ push := by
+    apply funext; intro N
+    simp only [Function.comp_apply]
+    exact push_prod_get
   rw [s] at ha
   exact tendsto_comp_push.mp ha
 
+/-- Adding one more term to a product multiplies by it -/
+theorem product_cons {a g : ℂ} {f : ℕ → ℂ} (h : HasProd f g) :
+    HasProd (Stream'.cons a f) (a * g) :=
+  product_cons_get (q := f) h
+
 /-- Adding one more term to a product multiplies by it (`tprod` version) -/
 theorem product_cons' {a : ℂ} {f : ℕ → ℂ} (h : ProdExists f) :
     tprod (Stream'.cons a f) = a * tprod f := by
-  rcases h with ⟨g, h⟩; rw [HasProd.tprod_eq h]; rw [HasProd.tprod_eq _]; exact product_cons h
+  rcases h with ⟨g, h⟩; rw [HasProd.tprod_eq h]; exact HasProd.tprod_eq (product_cons h)
 
-/-- Dropping a nonzero term divides by it -/
-theorem product_drop {f : ℕ → ℂ} {g : ℂ} (f0 : f 0 ≠ 0) (h : HasProd f g) :
-    HasProd (fun n ↦ f (n + 1)) (g / f 0) := by
-  have c := @product_cons (f 0)⁻¹ _ _ h
+/-- Dropping a nonzero term divides by it, `Stream'.get` version -/
+theorem product_drop_get {q : Stream' ℂ} {t : ℂ} (q0 : q.head ≠ 0) (h : HasProd q.get t) :
+    HasProd q.tail.get (t / q.head) := by
+  have c := product_cons_get (a := q.head⁻¹) h
   rw [HasProd]
   rw [inv_mul_eq_div, HasProd, SummationFilter.unconditional_filter, ← tendsto_comp_push,
     ← tendsto_comp_push] at c
-  have s : ((fun N : Finset ℕ ↦ N.prod fun n ↦ (Stream'.cons (f 0)⁻¹ f) n) ∘ push) ∘ push =
-      fun N : Finset ℕ ↦ N.prod fun n ↦ f (n + 1) := by
-    clear c h g; apply funext; intro N; simp
-    nth_rw 2 [← Stream'.eta f]
-    simp only [←push_prod, Stream'.head, Stream'.tail, Stream'.get, ←mul_assoc, inv_mul_cancel₀ f0,
-      one_mul]
-  rw [s] at c; assumption
+  have s : ((fun N : Finset ℕ ↦ N.prod (Stream'.cons q.head⁻¹ q).get) ∘ push) ∘ push =
+      fun N : Finset ℕ ↦ N.prod q.tail.get := by
+    apply funext; intro N
+    simp only [Function.comp_apply]
+    have e1 := push_prod_get (a := q.head⁻¹) (g := q) (N := push N)
+    have e2 := push_prod_get (a := q.head) (g := q.tail) (N := N)
+    rw [Stream'.eta q] at e2
+    rw [← e1, ← e2, ← mul_assoc, inv_mul_cancel₀ q0, one_mul]
+  rw [s] at c; exact c
+
+/-- Dropping a nonzero term divides by it -/
+theorem product_drop {f : ℕ → ℂ} {g : ℂ} (f0 : f 0 ≠ 0) (h : HasProd f g) :
+    HasProd (fun n ↦ f (n + 1)) (g / f 0) :=
+  product_drop_get (q := f) f0 h
 
 /-- Dropping a nonzero term divides by it (`tprod` version) -/
 theorem product_drop' {f : ℕ → ℂ} (f0 : f 0 ≠ 0) (h : ProdExists f) :

Ray/Analytic/Series.lean

@@ -66,36 +66,35 @@ theorem CNonpos.degenerate {f : ℕ → ℂ → G} {s : Set ℂ} {c a : ℝ} (c0
   have ca : c * a ^ n ≤ 0 := mul_nonpos_iff.mpr (Or.inr ⟨c0, by bound⟩)
   exact norm_eq_zero.mp (le_antisymm (le_trans hf ca) (norm_nonneg _))
 
-/-- Adding one more term to a sum adds it -/
-theorem sum_cons {a g : G} {f : ℕ → G} (h : HasSum f g) :
-    HasSum (Stream'.cons a f) (a + g) := by
+/-- Adding one more term to a sum adds it, `Stream'.get` version to keep terms type-correct
+    at low transparency -/
+theorem sum_cons_get {a t : G} {q : Stream' G} (h : HasSum q.get t) :
+    HasSum (Stream'.cons a q).get (a + t) := by
   rw [HasSum] at h ⊢
-  have ha := Filter.Tendsto.comp (Continuous.tendsto (continuous_add_left a) g) h
-  have s : ((fun z ↦ a + z) ∘ fun N : Finset ℕ ↦ N.sum f) =
-      (fun N : Finset ℕ ↦ N.sum (Stream'.cons a f)) ∘ push := by
-    apply funext; intro N; simp; exact push_sum
+  have ha := Filter.Tendsto.comp (Continuous.tendsto (continuous_const_add a) t) h
+  have s : ((fun z ↦ a + z) ∘ fun N : Finset ℕ ↦ N.sum q.get) =
+      (fun N : Finset ℕ ↦ N.sum (Stream'.cons a q).get) ∘ push := by
+    apply funext; intro N
+    simp only [Function.comp_apply]
+    exact push_sum_get
   rw [s] at ha
   exact tendsto_comp_push.mp ha
 
+/-- Adding one more term to a sum adds it -/
+theorem sum_cons {a g : G} {f : ℕ → G} (h : HasSum f g) :
+    HasSum (Stream'.cons a f) (a + g) :=
+  sum_cons_get (q := f) h
+
 /-- Adding one more term to a sum adds it (`tprod` version) -/
 lemma sum_cons' {a : G} {f : ℕ → G} (h : Summable f) :
     tsum (Stream'.cons a f) = a + tsum f := by
-  rcases h with ⟨g, h⟩; rw [HasSum.tsum_eq h]; rw [HasSum.tsum_eq _]; exact sum_cons h
+  rcases h with ⟨g, h⟩; rw [HasSum.tsum_eq h]; exact HasSum.tsum_eq (sum_cons h)
 
 /-- Dropping the first term subtracts it -/
 public lemma sum_drop {f : ℕ → G} {g : G} (h : HasSum f g) :
     HasSum (fun n ↦ f (n + 1)) (g - f 0) := by
-  have c := sum_cons (a := -f 0) h
-  rw [HasSum]
-  rw [neg_add_eq_sub, HasSum, SummationFilter.unconditional_filter, ← tendsto_comp_push,
-    ← tendsto_comp_push] at c
-  have s : ((fun N : Finset ℕ ↦ N.sum fun n ↦ (Stream'.cons (-f 0) f) n) ∘ push) ∘ push =
-      fun N : Finset ℕ ↦ N.sum fun n ↦ f (n + 1) := by
-    clear c h g; apply funext; intro N; simp
-    nth_rw 2 [← Stream'.eta f]
-    simp only [←push_sum, Stream'.head, Stream'.tail, Stream'.get]
-    abel
-  rw [s] at c; assumption
+  rw [hasSum_nat_add_iff (f := f) 1]
+  simpa using h
 
 /-- Dropping the first term subtracts it (`tsum` version) -/
 public lemma tsum_drop {f : ℕ → G} (h : Summable f) :
@@ -153,7 +152,7 @@ theorem uniformVanishing_to_tendsto_uniformly_on {f : ℕ → ℂ → G} {s : Se
 theorem fast_series_converge_uniformly_on {f : ℕ → ℂ → G} {s : Set ℂ} {c a : ℝ} (a0 : 0 ≤ a)
     (a1 : a < 1) (hf : ∀ n z, z ∈ s → ‖f n z‖ ≤ c * a ^ n) : HasUniformSum f (tsumOn f) s := by
   by_cases c0 : c ≤ 0
-  · have fz := CNonpos.degenerate c0 a0 hf; simp only at fz
+  · have fz := CNonpos.degenerate c0 a0 hf
     rw [HasUniformSum, Metric.tendstoUniformlyOn_iff]
     intro e ep; refine .of_forall ?_; intro n z zs
     rw [tsumOn]
@@ -187,7 +186,6 @@ theorem fast_series_converge_at {f : ℕ → G} {c a : ℝ} (a0 : 0 ≤ a) (a1 :
   set g : ℕ → ℂ → G := fun n _ ↦ f n
   have hg : ∀ n z, z ∈ s → ‖g n z‖ ≤ c * a ^ n := fun n z _ ↦ hf n
   have u := fast_series_converge_uniformly_on a0 a1 hg
-  simp at u
   rw [HasUniformSum] at u
   rw [tendstoUniformlyOn_singleton_iff_tendsto] at u
   apply HasSum.summable; assumption

Ray/Analytic/Uniform.lean

@@ -26,7 +26,7 @@ theorem analyticOn_small_cball {f : ℂ → E} {z : ℂ} {r : ℝ≥0} (h : Anal
   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
+    rw [ball]; simp only [dist_lt_coe, Set.mem_ofPred_eq]; exact lt_of_le_of_lt hx sr
   exact h x hb
 
 theorem cauchy_bound {f : ℂ → E} {c : ℂ} {r : ℝ≥0} {d : ℝ≥0} {w : ℂ} {n : ℕ} (rp : r > 0)
@@ -77,7 +77,7 @@ theorem circleIntegral_sub {f g : ℂ → E} {c : ℂ} {r : ℝ} (fi : CircleInt
 
 theorem circleMap_nz {c : ℂ} {r : ℝ≥0} {θ : ℝ} (rp : r > 0) : circleMap c r θ - c ≠ 0 := by
   simp only [circleMap_sub_center, Ne, circleMap_eq_center_iff, NNReal.coe_eq_zero]
-  intro h; rw [h] at rp; simp only [gt_iff_lt, not_lt_zero'] at rp
+  intro h; rw [h] at rp; simp only [gt_iff_lt, not_lt_zero] at rp
 
 theorem cauchy_is_circleIntegrable {f : ℂ → E} {c : ℂ} {r : ℝ≥0} (n : ℕ) (w : ℂ) (rp : r > 0)
     (h : ContinuousOn f (closedBall c r)) :
@@ -158,7 +158,7 @@ theorem analyticOn_ball_radius {f : ℂ → E} {z : ℂ} {r : ℝ≥0} (rp : r >
     rw [← pp] at hp'
     refine hp'.r_le
   · intro y yr
-    rw [EMetric.ball, Set.mem_setOf] at yr
+    rw [Metric.mem_eball] at yr
     rcases exists_between yr with ⟨t, t0, t1⟩
     have t1' : t.toNNReal < r := by
       rw [← WithTop.coe_lt_coe]; exact lt_of_le_of_lt ENNReal.coe_toNNReal_le_self t1
@@ -170,7 +170,7 @@ theorem analyticOn_ball_radius {f : ℂ → E} {z : ℂ} {r : ℝ≥0} (rp : r >
       HasFPowerSeriesAt.eq_formalMultilinearSeries ⟨↑(r / 2), ph⟩ ⟨t.toNNReal, hp'⟩
     rw [← pp] at hp'
     refine hp'.hasSum ?_
-    rw [EMetric.ball, Set.mem_setOf]
+    rw [Metric.mem_eball]
     calc edist y 0
       _ < t := t0
       _ = ↑t.toNNReal := (ENNReal.coe_toNNReal <| ne_top_of_lt t1).symm