Update lean, mathlib, and interval

Ray.lean

@@ -16,5 +16,3 @@ import Ray.Render.Mandelbrot
 import Ray.Render.Image
 import Ray.Render.Iterate
 import Ray.Render.Potential
-import Ray.Tactic.Bound
-import Ray.Tactic.BoundTests

Ray/Analytic/Analytic.lean

@@ -6,7 +6,6 @@ import Mathlib.Analysis.Analytic.IsolatedZeros
 import Mathlib.Analysis.Calculus.FormalMultilinearSeries
 import Mathlib.Data.Finset.Basic
 import Mathlib.Data.Real.Basic
-import Mathlib.Data.Real.NNReal
 import Mathlib.Data.Set.Basic
 import Mathlib.Data.Stream.Defs
 import Mathlib.Topology.Basic
@@ -19,18 +18,16 @@ import Ray.Misc.Topology
 -/
 
 open Classical
-open Filter (atTop eventually_of_forall)
+open Filter (atTop)
 open Function (curry uncurry)
 open Metric (ball closedBall sphere isOpen_ball)
 open Set (univ)
 open scoped Real NNReal ENNReal Topology
 noncomputable section
 
 variable {𝕜 : Type} [NontriviallyNormedField 𝕜]
-variable {E : Type} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
-variable {F : Type} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F]
-variable {G : Type} [NormedAddCommGroup G] [NormedSpace 𝕜 G] [CompleteSpace G]
-variable {H : Type} [NormedAddCommGroup H] [NormedSpace 𝕜 H] [CompleteSpace H]
+variable {E : Type} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+variable {F : Type} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
 
 /-- The order of a zero at a point.
     We define this in terms of the function alone so that expressions involving order can
@@ -176,7 +173,7 @@ lemma FormalMultilinearSeries.unshift_radius' (p : FormalMultilinearSeries 𝕜
     have h := fun n ↦ mul_le_mul_of_nonneg_right (h (n + 1)) (NNReal.coe_nonneg r⁻¹)
     by_cases r0 : r = 0; · simp only [r0, ENNReal.coe_zero, ENNReal.iSup_zero_eq_zero, le_zero_iff]
     simp only [pow_succ, ←mul_assoc _ _ (r:ℝ), mul_assoc _ (r:ℝ) _,
-      mul_inv_cancel (NNReal.coe_ne_zero.mpr r0), NNReal.coe_inv, mul_one, p.unshift_norm'] at h
+      mul_inv_cancel₀ (NNReal.coe_ne_zero.mpr r0), NNReal.coe_inv, mul_one, p.unshift_norm'] at h
     simp only [NNReal.coe_inv]
     convert le_iSup _ h; rfl
   · refine iSup₂_le ?_; intro r k; refine iSup_le ?_; intro h
@@ -279,7 +276,7 @@ theorem AnalyticAt.monomial_mul_leadingCoeff {f : 𝕜 → E} {c : 𝕜} (fa : A
     rw [e, h]
 
 /-- `fderiv` is analytic -/
-theorem AnalyticAt.fderiv {f : E → F} {c : E} (fa : AnalyticAt 𝕜 f c) :
+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)
@@ -298,7 +295,7 @@ theorem AnalyticAt.deriv2 [CompleteSpace 𝕜] {f : E → 𝕜 → 𝕜} {c : E
     AnalyticAt 𝕜 (fun x : E × 𝕜 ↦ _root_.deriv (f x.1) x.2) c := by
   set p : (E × 𝕜 →L[𝕜] 𝕜) →L[𝕜] 𝕜 := ContinuousLinearMap.apply 𝕜 𝕜 (0, 1)
   have e : ∀ᶠ x : E × 𝕜 in 𝓝 c, _root_.deriv (f x.1) x.2 = p (_root_.fderiv 𝕜 (uncurry f) x) := by
-    refine fa.eventually_analyticAt.mp (eventually_of_forall ?_)
+    refine fa.eventually_analyticAt.mp (.of_forall ?_)
     intro ⟨x, y⟩ fa; simp only [← fderiv_deriv]
     have e : f x = uncurry f ∘ fun y ↦ (x, y) := rfl
     rw [e]; rw [fderiv.comp]
@@ -314,7 +311,7 @@ theorem AnalyticAt.deriv2 [CompleteSpace 𝕜] {f : E → 𝕜 → 𝕜} {c : E
 /-- Scaling commutes with power series -/
 theorem HasFPowerSeriesAt.const_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
-  rw [hasFPowerSeriesAt_iff] at fp ⊢; refine fp.mp (eventually_of_forall fun z h ↦ ?_)
+  rw [hasFPowerSeriesAt_iff] at fp ⊢; refine fp.mp (.of_forall fun z h ↦ ?_)
   simp only [FormalMultilinearSeries.coeff, ContinuousMultilinearMap.smul_apply, smul_comm _ a]
   exact h.const_smul a
 
@@ -324,7 +321,7 @@ theorem analyticAt_iff_const_smul {f : 𝕜 → E} {c a : 𝕜} (a0 : a ≠ 0) :
   constructor
   · intro ⟨p, fp⟩
     have e : f = fun z ↦ a⁻¹ • a • f z := by
-      funext; simp only [← smul_assoc, smul_eq_mul, inv_mul_cancel a0, one_smul]
+      funext; simp only [← smul_assoc, smul_eq_mul, inv_mul_cancel₀ a0, one_smul]
     rw [e]; exact ⟨_, fp.const_smul⟩
   · intro ⟨p, fp⟩; exact ⟨_, fp.const_smul⟩
 
@@ -347,7 +344,7 @@ theorem leadingCoeff.zero {c : 𝕜} : leadingCoeff (fun _ : 𝕜 ↦ (0 : E)) c
   induction' n with n h; simp only [Function.iterate_zero_apply]
   simp only [Function.iterate_succ_apply]; convert h
   simp only [Function.swap, dslope, deriv_const]
-  funext; simp only [slope_fun_def, vsub_eq_sub, sub_zero, smul_zero, Function.update_apply]
+  simp only [slope_fun_def, vsub_eq_sub, sub_zero, smul_zero, Function.update_apply]
   split_ifs; rfl; rfl
 
 /-- `leadingCoeff` has linear scaling -/

Ray/Analytic/Holomorphic.lean

@@ -7,7 +7,6 @@ import Mathlib.Analysis.Complex.CauchyIntegral
 import Mathlib.Data.Complex.Basic
 import Mathlib.Data.Finset.Basic
 import Mathlib.Data.Real.Basic
-import Mathlib.Data.Real.NNReal
 import Mathlib.Data.Real.Pi.Bounds
 import Mathlib.Data.Set.Basic
 import Mathlib.Topology.Basic

Ray/Analytic/HolomorphicUpstream.lean

@@ -8,7 +8,6 @@ import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
 import Mathlib.Data.Complex.Basic
 import Mathlib.Data.Finset.Basic
 import Mathlib.Data.Real.Basic
-import Mathlib.Data.Real.NNReal
 import Mathlib.Data.Real.Pi.Bounds
 import Mathlib.Data.Set.Basic
 import Mathlib.Topology.Basic
@@ -26,6 +25,7 @@ noncomputable section
 
 variable {E : Type} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
 variable {F : Type} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F]
+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) :
@@ -69,21 +69,21 @@ theorem analyticAt_log {c : ℂ} (m : c ∈ Complex.slitPlane) : AnalyticAt ℂ
   exact differentiableAt_id.clog m
 
 /-- `log` is analytic away from nonpositive reals -/
-theorem AnalyticAt.log {f : E → ℂ} {c : E} (fa : AnalyticAt ℂ f c) (m : f c ∈ Complex.slitPlane) :
+theorem AnalyticAt.log {f : G → ℂ} {c : G} (fa : AnalyticAt ℂ f c) (m : f c ∈ Complex.slitPlane) :
     AnalyticAt ℂ (fun z ↦ log (f z)) c :=
   (analyticAt_log m).comp fa
 
 /-- `log` is analytic away from nonpositive reals -/
-theorem AnalyticOn.log {f : E → ℂ} {s : Set E} (fs : AnalyticOn ℂ f s)
+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 :=
   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 -/
-theorem AnalyticAt.cpow {f g : E → ℂ} {c : E} (fa : AnalyticAt ℂ f c) (ga : AnalyticAt ℂ g c)
+theorem AnalyticAt.cpow {f g : G → ℂ} {c : G} (fa : AnalyticAt ℂ f c) (ga : AnalyticAt ℂ g c)
     (m : f c ∈ Complex.slitPlane) : AnalyticAt ℂ (fun z ↦ f z ^ g z) c := by
   have fc : f c ≠ 0 := Complex.slitPlane_ne_zero m
   have e : (fun z ↦ f z ^ g z) =ᶠ[𝓝 c] fun z ↦ Complex.exp (Complex.log (f z) * g z) := by
-    refine (fa.continuousAt.eventually_ne fc).mp (Filter.eventually_of_forall ?_)
+    refine (fa.continuousAt.eventually_ne fc).mp (.of_forall ?_)
     intro z fz; simp only [fz, Complex.cpow_def, if_false]
   rw [analyticAt_congr e]
   exact AnalyticAt.exp.comp ((fa.log m).mul ga)

Ray/Analytic/Products.lean

@@ -13,7 +13,6 @@ import Ray.Misc.Bounds
 import Ray.Misc.Finset
 import Ray.Analytic.Holomorphic
 import Ray.Analytic.Series
-import Ray.Tactic.Bound
 
 /-!
 ## Infinite products of analytic functions
@@ -86,7 +85,7 @@ theorem fast_products_converge {f : ℕ → ℂ → ℂ} {s : Set ℂ} {a c : 
   generalize hg : (fun z ↦ exp (gl z)) = g
   use g; refine ⟨?_, ?_, ?_⟩
   · intro z zs
-    specialize us z zs; simp at us
+    specialize us z zs
     have comp :
       Filter.Tendsto (exp ∘ fun N : Finset ℕ ↦ N.sum fun n ↦ fl n z) atTop (𝓝 (exp (gl z))) :=
       Filter.Tendsto.comp (Continuous.tendsto Complex.continuous_exp _) us
@@ -145,7 +144,7 @@ theorem product_drop {f : ℕ → ℂ} {g : ℂ} (f0 : f 0 ≠ 0) (h : HasProd f
       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,
+    simp only [←push_prod, Stream'.head, Stream'.tail, Stream'.get, ←mul_assoc, inv_mul_cancel₀ f0,
       one_mul]
   rw [s] at c; assumption
 

Ray/Analytic/Series.lean

@@ -1,7 +1,6 @@
 import Mathlib.Analysis.Analytic.Basic
 import Mathlib.Data.Complex.Basic
 import Mathlib.Data.Real.Basic
-import Mathlib.Data.Real.NNReal
 import Mathlib.Data.Real.Pi.Bounds
 import Mathlib.Data.Set.Basic
 import Mathlib.Data.Stream.Init
@@ -10,7 +9,6 @@ import Mathlib.Topology.UniformSpace.UniformConvergence
 import Ray.Analytic.Analytic
 import Ray.Analytic.Uniform
 import Ray.Misc.Bounds
-import Ray.Tactic.Bound
 
 /-!
 ## Infinite series of analytic functions
@@ -115,7 +113,7 @@ theorem fast_series_converge_uniformly_on {f : ℕ → ℂ → ℂ} {s : Set ℂ
   by_cases c0 : c ≤ 0
   · have fz := CNonpos.degenerate c0 a0 hf; simp only at fz
     rw [HasUniformSum, Metric.tendstoUniformlyOn_iff]
-    intro e ep; apply Filter.eventually_of_forall; intro n z zs
+    intro e ep; refine .of_forall ?_; intro n z zs
     rw [tsumOn]
     simp_rw [fz _ z zs]
     simp only [tsum_zero, Finset.sum_const_zero, dist_zero_left, Complex.norm_eq_abs,
@@ -137,7 +135,7 @@ theorem fast_series_converge_uniformly_on {f : ℕ → ℂ → ℂ} {s : Set ℂ
       _ ≤ t * (c * (1 - a)⁻¹) := by bound
       _ = (1 - a) / c * (e / 2) * (c * (1 - a)⁻¹) := rfl
       _ = (1 - a) * (1 - a)⁻¹ * (c / c) * (e / 2) := by ring
-      _ = 1 * 1 * (e / 2) := by rw [mul_inv_cancel a1p.ne', div_self c0.ne']
+      _ = 1 * 1 * (e / 2) := by rw [mul_inv_cancel₀ a1p.ne', div_self c0.ne']
       _ = e / 2 := by ring
       _ < e := by linarith
 

Ray/Analytic/Uniform.lean

@@ -3,7 +3,6 @@ import Mathlib.Analysis.Complex.CauchyIntegral
 import Mathlib.Analysis.Complex.ReImTopology
 import Mathlib.Data.Complex.Basic
 import Mathlib.Data.Real.Basic
-import Mathlib.Data.Real.NNReal
 import Mathlib.Data.Real.Pi.Bounds
 import Mathlib.Data.Set.Basic
 import Mathlib.MeasureTheory.Integral.IntervalIntegral
@@ -14,7 +13,6 @@ import Mathlib.Topology.UniformSpace.UniformConvergence
 import Ray.Analytic.Analytic
 import Ray.Misc.Bounds
 import Ray.Misc.Topology
-import Ray.Tactic.Bound
 
 /-!
 ## Convergent sequences of analytic functions
@@ -116,9 +114,8 @@ theorem cauchy_bound {f : ℂ → ℂ} {c : ℂ} {r : ℝ≥0} {d : ℝ≥0} {w
     _ ≤ |π|⁻¹ * 2⁻¹ * (2 * π * r * (wr * r⁻¹)) := by bound
     _ = π * |π|⁻¹ * (r * r⁻¹) * wr := by ring
     _ = π * π⁻¹ * (r * r⁻¹) * wr := by rw [p3]
-    _ = 1 * (r * r⁻¹) * wr := by rw [mul_inv_cancel Real.pi_ne_zero]
-    _ = wr := by
-      rw [NNReal.coe_inv, mul_inv_cancel (NNReal.coe_ne_zero.mpr rp.ne'), one_mul, one_mul]
+    _ = 1 * (r * r⁻¹) * wr := by rw [mul_inv_cancel₀ Real.pi_ne_zero]
+    _ = wr := by field_simp
 
 theorem circleIntegral_sub {f g : ℂ → ℂ} {c : ℂ} {r : ℝ} (fi : CircleIntegrable f c r)
     (gi : CircleIntegrable g c r) :
@@ -203,7 +200,7 @@ theorem uniform_analytic_lim {I : Type} [Lattice I] [Nonempty I] {f : I → ℂ
   have cfs : ∀ n, ContinuousOn (f n) s := fun n ↦ AnalyticOn.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 (Filter.eventually_of_forall cfs)) cb
+    ContinuousOn.mono (TendstoUniformlyOn.continuousOn u (.of_forall cfs)) cb
   clear h hb hc o cfs
   set p := cauchyPowerSeries g c r
   refine
@@ -255,7 +252,7 @@ theorem uniform_analytic_lim {I : Type} [Lattice I] [Nonempty I] {f : I → ℂ
         _ ≤ (1 - a)⁻¹ * d := by bound
         _ = (1 - a)⁻¹ * ((1 - a) * (e / 4)) := by rw [← d4]
         _ = (1 - a) * (1 - a)⁻¹ * (e / 4) := by ring
-        _ = 1 * (e / 4) := by rw [mul_inv_cancel a1p.ne']
+        _ = 1 * (e / 4) := by rw [mul_inv_cancel₀ a1p.ne']
         _ = e / 4 := by ring
   generalize hMp : M.sum (fun k : ℕ ↦ p k fun _ ↦ y) = Mp; rw [hMp] at dppr
   generalize hMpr : M.sum (fun k ↦ pr n k fun _ ↦ y) = Mpr; rw [hMpr] at dpf dppr