Update version to lean4:v4.29.0-rc6

README.md

@@ -91,4 +91,4 @@ set_option trace.aesop true in
 -- Print compiler IR, such as to see how well inlining worked:
 set_option trace.compiler.ir.result true in
 def ...
-```
+```

Ray/Analytic/Analytic.lean

@@ -43,11 +43,16 @@ public lemma AnalyticWithinAt.analyticAt {f : E → F} {s : Set E} {x : E}
   obtain ⟨p, r, fp⟩ := fa
   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
-  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])
+    {r_le := by exact le_trans (min_le_left _ _) fp.r_le
+     r_pos := by exact lt_min fp.r_pos (ENNReal.ofReal_pos.mpr e0)
+     hasSum := fun {y} yr ↦ ?_}⟩
+  rw [Metric.mem_eball, edist_zero_right] at yr
+  have yr' : ‖y‖ₑ < r := lt_of_lt_of_le yr (min_le_left _ _)
+  have ye : ‖y‖ < e := by
+    have ye' : ‖y‖ₑ < ENNReal.ofReal e := lt_of_lt_of_le yr (min_le_right _ _)
+    rwa [ENNReal.lt_ofReal_iff_toReal_lt enorm_ne_top, toReal_enorm] at ye'
+  exact fp.hasSum (.inr (es (by simpa [Metric.mem_ball, dist_eq_norm, sub_eq_add_neg, add_assoc]
+    using ye))) (by simpa [Metric.mem_eball, edist_zero_right] using yr')
 
 /-- Extract `AnalyticAt` from `ContDiffOn 𝕜 ω` if we have a neighborhood -/
 public lemma ContDiffOn.analyticAt {f : E → F} {s : Set E} (fa : ContDiffOn 𝕜 ω f s) {x : E}
@@ -59,11 +64,9 @@ 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 : 𝕜} :
+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
+  simpa using fa.div_const
 
 public lemma AnalyticAt.dslope {f : 𝕜 → E} {c x : 𝕜} (fa : AnalyticAt 𝕜 f x) :
     AnalyticAt 𝕜 (dslope f c) x := by
@@ -175,6 +178,7 @@ lemma FormalMultilinearSeries.unshift_coeff_zero (p : FormalMultilinearSeries 
     (p.unshift' c).coeff 0 = c := by
   simp only [FormalMultilinearSeries.coeff, FormalMultilinearSeries.unshift',
     FormalMultilinearSeries.unshift, continuousMultilinearCurryFin0_symm_apply]
+  exact ContinuousMultilinearMap.uncurry0_apply 𝕜 c 1
 
 @[simp]
 lemma FormalMultilinearSeries.unshift_coeff_succ (p : FormalMultilinearSeries 𝕜 𝕜 E) (c : E)
@@ -215,7 +219,7 @@ lemma FormalMultilinearSeries.unshift_radius' (p : FormalMultilinearSeries 𝕜
   · refine iSup₂_le ?_; intro r k; refine iSup_le ?_; intro h
     refine le_trans ?_ (le_iSup₂ r (k * ↑r⁻¹))
     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, le_zero_iff]
+    by_cases r0 : r = 0; · simp [r0]
     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
     simp only [NNReal.coe_inv]
@@ -278,7 +282,10 @@ 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
+    by_contra h
+    push_neg at h
+    exact pnz (FormalMultilinearSeries.ext h)
   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 ⊢
@@ -390,7 +397,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
+        exact lt_of_le_of_lt m tr
       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

@@ -106,15 +106,12 @@ lemma continuousOn_cauchy_integral (i : Holo f μ s c r) :
   set g : X → ℝ → E := fun x t ↦ deriv (circleMap c r) t • (circleMap c r t - c)⁻¹ ^ n •
       (circleMap c r t - c)⁻¹ • f x (circleMap c r t)
   have ic : ContinuousOn (fun p : X × ℝ ↦ g p.1 p.2) (s ×ˢ univ) := by
-    simp only [g, deriv_circleMap, circleMap_sub_center, circleMap_zero_inv, smul_smul]
-    apply ContinuousOn.smul
-    · fun_prop
-    · have e : (fun p : X × ℝ ↦ f p.1 (circleMap c r p.2)) =
-        uncurry f ∘ fun p : X × ℝ ↦ (p.1, circleMap c r p.2) := rfl
-      rw [e]
-      refine i.fc.comp (by fun_prop) ?_
-      intro p ⟨ps, _⟩
-      simp [circleMap, ps]
+    simp only [g, circleMap_sub_center, circleMap_zero_inv, smul_smul]
+    refine ContinuousOn.smul (ContinuousOn.mul (((contDiff_circleMap c r :
+      ContDiff ℝ 2 (circleMap c r)).continuous_deriv (by norm_num)).comp_continuousOn
+      continuousOn_snd) (by fun_prop)) ?_
+    exact i.fc.comp (by fun_prop : ContinuousOn (fun p : X × ℝ ↦ (p.1, circleMap c r p.2))
+      (s ×ˢ univ)) fun p hp ↦ by simpa [circleMap] using hp
   apply MeasureTheory.continuousOn_of_dominated (bound := fun _ ↦ r * ((r ^ n)⁻¹ * (r⁻¹ * i.C)))
   · intro x xs
     apply Continuous.aestronglyMeasurable
@@ -187,10 +184,13 @@ theorem hasFPowerSeriesOnBall_integral (i : Holo f μ s c r) :
     have e : EqOn (fun x ↦ f x (c + y)) (fun x ↦ ∑' n, a x n) s :=
       fun x xs ↦ (hs x xs).tsum_eq.symm
     rw [setIntegral_congr_fun i.sm e]
-    simp only [series, ContinuousMultilinearMap.integral_apply i.integrableOn_cauchyPowerSeries]
-    apply MeasureTheory.hasSum_integral_of_summable_integral_norm
+    have hseries : (fun n ↦ (i.series n) fun _ ↦ y) = fun n ↦ ∫ x in s, a x n ∂μ := by
+      funext n; exact ContinuousMultilinearMap.integral_apply (μ := μ.restrict s)
+        (φ_int := i.integrableOn_cauchyPowerSeries (n := n)) (m := fun _ ↦ y)
+    rw [hseries]; 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
+    · rw [Metric.eball_coe] at ym
+      simp only [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 simp [Metric.eball_coe, r']
   rw [e]
   exact i.hasFPowerSeriesOnBall_integral.analyticOnNhd
 

Ray/Analytic/Products.lean

@@ -56,7 +56,7 @@ public theorem product_pow' {f : ℕ → ℂ} {p : ℕ} (h : ProdExists f) :
 theorem product_cons {a g : ℂ} {f : ℕ → ℂ} (h : HasProd f g) :
     HasProd (Stream'.cons a f) (a * g) := by
   rw [HasProd] at h ⊢
-  have ha := Filter.Tendsto.comp (Continuous.tendsto (continuous_mul_left a) g) h
+  have ha := Filter.Tendsto.comp (Continuous.tendsto (continuous_const_mul 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

Ray/Analytic/Series.lean

@@ -70,7 +70,7 @@ theorem CNonpos.degenerate {f : ℕ → ℂ → G} {s : Set ℂ} {c a : ℝ} (c0
 theorem sum_cons {a g : G} {f : ℕ → G} (h : HasSum f g) :
     HasSum (Stream'.cons a f) (a + g) := by
   rw [HasSum] at h ⊢
-  have ha := Filter.Tendsto.comp (Continuous.tendsto (continuous_add_left a) g) h
+  have ha := Filter.Tendsto.comp (Continuous.tendsto (continuous_const_add 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

Ray/Analytic/Uniform.lean

@@ -56,7 +56,7 @@ theorem cauchy_bound {f : ℂ → E} {c : ℂ} {r : ℝ≥0} {d : ℝ≥0} {w :
     _ = π * ‖π‖⁻¹ * (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 field_simp; norm_cast; field_simp; simp
+    _ = wr := by simpa [mul_assoc] using congrArg (fun t : ℝ => t * wr) (mul_inv_cancel₀ (by exact_mod_cast rp.ne' : (↑r : ℝ) ≠ 0))
 
 theorem circleIntegral_sub {f g : ℂ → E} {c : ℂ} {r : ℝ} (fi : CircleIntegrable f c r)
     (gi : CircleIntegrable g c r) :
@@ -69,11 +69,8 @@ theorem circleIntegral_sub {f g : ℂ → E} {c : ℂ} {r : ℝ} (fi : CircleInt
   generalize hfg : (fun θ : ℝ ↦ deriv (circleMap c r) θ • (f - g) (circleMap c r θ)) = fgc
   have hs : fc - gc = fgc := by
     rw [← hf, ← hg, ← hfg]; funext
-    simp only [deriv_circleMap, Pi.sub_apply, smul_sub]
-  rw [← hs]; clear hfg hs fgc; symm
-  have fci := CircleIntegrable.out fi; rw [hf] at fci
-  have gci := CircleIntegrable.out gi; rw [hg] at gci
-  exact intervalIntegral.integral_sub fci gci
+    simp only [Pi.sub_apply, smul_sub]
+  simpa only [Pi.sub_apply, smul_sub] using (intervalIntegral.integral_sub fi.out gi.out).symm
 
 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]
@@ -158,7 +155,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 +167,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

Ray/Dynamics/BottcherNearM.lean

@@ -524,8 +524,8 @@ public theorem Super.bottcherNear_mfderiv_ne_zero (s : Super f d a) (c : ℂ) :
     exact ContinuousLinearMap.smulRight_ne_zero ContinuousLinearMap.one_ne_zero (by norm_num)
   · have u : (fun z : S ↦ extChartAt I a z - extChartAt I a a) =
         extChartAt I a - fun _ : S ↦ extChartAt I a a := rfl
-    rw [u, mfderiv_sub, mfderiv_const, sub_zero]
-    · exact extChartAt_mderiv_ne_zero a
+    rw [u, mfderiv_sub, mfderiv_const]
+    · exact fun h ↦ extChartAt_mderiv_ne_zero a (sub_eq_zero.mp h)
     · exact (contMDiffAt_extChartAt' (mem_chart_source _ a)).mdifferentiableAt one_ne_zero
     · apply mdifferentiableAt_const
 

Ray/Dynamics/Grow.lean

@@ -204,13 +204,14 @@ theorem eqn_noncritical {x : ℂ × ℂ} (e : ∀ᶠ y in 𝓝 x, Eqn s n r y) (
     ((continuousAt_const.prodMk continuousAt_id).eventually e).mp
       (.of_forall fun _ e ↦ e.eqn)
   rw [mfderiv_eq_fderiv, loc.fderiv_eq] at x0
-  have d := (differentiableAt_pow (𝕜 := ℂ) (x := x) (d ^ n)).hasFDerivAt.hasDerivAt.deriv
+  have hd := (differentiableAt_pow (𝕜 := ℂ) (x := x) (d ^ n)).hasFDerivAt.hasDerivAt.deriv
   apply_fun (fun x ↦ x 1) at x0
-  rw [x0] at d
-  replace d := Eq.trans d (ContinuousLinearMap.zero_apply _)
+  rw [x0] at hd
+  have dz : deriv (fun x ↦ x ^ d ^ n) x = 0 := by
+    exact Eq.trans hd (show ((0 : ℂ →L[ℂ] ℂ) 1) = (0 : ℂ) from rfl)
   simp only [differentiableAt_fun_id, deriv_fun_pow, Nat.cast_pow, deriv_id'', mul_one, mul_eq_zero,
-    pow_eq_zero_iff', Nat.cast_eq_zero, s.d0, ne_eq, false_and, false_or] at d
-  exact d.1
+    pow_eq_zero_iff', Nat.cast_eq_zero, s.d0, ne_eq, false_and, false_or] at dz
+  exact dz.1
 
 /-- `p < 1` for any `p` in `Grow` -/
 theorem Grow.p1 (g : Grow s c p n r) : p < 1 := by

Ray/Dynamics/Multiple.lean

@@ -77,8 +77,8 @@ theorem SuperAt.not_local_inj {f : ℂ → ℂ} {d : ℕ} (s : SuperAt f d) :
     have d0 : mfderiv I I (fun z : ℂ ↦ z) 0 ≠ 0 := id_mderiv_ne_zero
     rw [(Filter.EventuallyEq.symm ib).mfderiv_eq] at d0
     rw [←Function.comp_def, mfderiv_comp 0 _ ba.differentiableAt.mdifferentiableAt] at d0
-    simp only [Ne, mderiv_comp_eq_zero_iff, nc, or_false] at d0
-    rw [bottcherNear_zero] at d0; exact d0
+    rw [bottcherNear_zero] at d0
+    exact fun h => d0 (by rw [h, ContinuousLinearMap.zero_comp]; rfl)
     rw [bottcherNear_zero]; exact ia.mdifferentiableAt (by decide)
   rcases exist_root_of_unity s.d2 with ⟨a, a1, ad⟩
   refine ⟨fun z ↦ i (a * bottcherNear f d z), ?_, ?_, ?_⟩
@@ -193,7 +193,9 @@ public theorem not_local_inj_of_mfderiv_zero {f : S → T} {c : S} (fa : ContMDi
       mfderiv_comp _ ((contMDiffAt_extChartAt' _).mdifferentiableAt one_ne_zero) _,
       mfderiv_comp _ fd (((contMDiffOn_extChartAt_symm _).contMDiffAt
       (extChartAt_target_mem_nhds' _)).mdifferentiableAt one_ne_zero),
-      PartialEquiv.left_inv, df, ContinuousLinearMap.zero_comp, ContinuousLinearMap.comp_zero]
+      PartialEquiv.left_inv, df, ContinuousLinearMap.zero_comp]
+    · simpa using (ContinuousLinearMap.comp_zero
+        (mfderiv I I (extChartAt I (f c)) ((f ∘ (extChartAt I c).symm) (extChartAt I c c))))
     · apply mem_extChartAt_source
     · apply mem_extChartAt_target
     · simp

Ray/Dynamics/Ray.lean

@@ -175,6 +175,7 @@ theorem Super.ray_noncritical_zero (s : Super f d a) [OnePreimage s] (c : ℂ) :
   have hr : MDifferentiableAt I I (s.ray c) 0 :=
     (s.ray_mAnalytic (s.mem_ext c)).along_snd.mdifferentiableAt (by decide)
   rw [mfderiv_comp 0 hb hr, h, ContinuousLinearMap.comp_zero]
+  rfl
 
 -- `s.ray` is noncritical everywhere in `s.ext`
 public theorem Super.ray_noncritical (s : Super f d a) [OnePreimage s] (post : (c, x) ∈ s.ext) :
@@ -186,19 +187,22 @@ public theorem Super.ray_noncritical (s : Super f d a) [OnePreimage s] (post : (
       (continuousAt_const.prodMk continuousAt_id).eventually (s.ray_eqn_iter' post)
     rw [e.mfderiv_eq]; contrapose x0
     rw [mfderiv_eq_fderiv] at x0
-    have d := (differentiableAt_pow (x := x) (d ^ n)).hasFDerivAt.hasDerivAt.deriv
+    have hd := (differentiableAt_pow (x := x) (d ^ n)).hasFDerivAt.hasDerivAt.deriv
     apply_fun (fun x ↦ x 1) at x0
-    rw [x0] at d
-    replace d := Eq.trans d (ContinuousLinearMap.zero_apply _)
+    rw [x0] at hd
+    have hd0 : deriv (fun y ↦ y ^ d ^ n) x = 0 := by
+      exact hd.trans rfl
     simp only [differentiableAt_fun_id, deriv_fun_pow, Nat.cast_pow, deriv_id'', mul_one,
-      mul_eq_zero, pow_eq_zero_iff', Nat.cast_eq_zero, s.d0, ne_eq, false_and, false_or] at d
-    exact d.1
+      mul_eq_zero, pow_eq_zero_iff', Nat.cast_eq_zero, s.d0, ne_eq, false_and, false_or] at hd0
+    exact hd0.1
   have d := mfderiv_comp x
       ((s.bottcherNearIter_mAnalytic (s.ray_near post)).along_snd.mdifferentiableAt (by decide))
       ((s.ray_mAnalytic post).along_snd.mdifferentiableAt (by decide))
   simp only [Function.comp_def, n] at d h
-  simp only [d, Ne, mderiv_comp_eq_zero_iff, not_or] at h
-  exact h.2
+  intro hx
+  apply h
+  rw [d, hx, ContinuousLinearMap.comp_zero]
+  rfl
 
 /-- `s.ray` is nontrivial, since it is noncritical at 0 and `s.ext` is connected -/
 public theorem Super.ray_nontrivial (s : Super f d a) [OnePreimage s] (post : (c, x) ∈ s.ext) :
@@ -288,10 +292,14 @@ public theorem Super.ray_inj (s : Super f d a) [OnePreimage s] {x0 x1 : ℂ} :
     refine ((continuousAt_const.prodMk (Complex.continuous_ofReal.continuousAt.mul
         continuousAt_const)).eventually
         (eqn_unique e0 er ?_ (mul_ne_zero t0 x00))).mp (.of_forall fun u e ↦ ?_)
-    · simp only [← hr]; rw [xe]; exact e
+    · rw [← hr]
+      change s.ray c (↑t * x0) = s.ray c (x1 / x0 * (↑t * x0))
+      rw [xe]
+      simpa [u] using e
     · rw [← hr] at e; simp only [uncurry] at e
-      rw [← mul_assoc, mul_comm _ (u:ℂ), mul_assoc, div_mul_cancel₀ _ x00] at e
-      exact e
+      have xeu : x1 / x0 * (↑u * x0) = ↑u * x1 := by
+        rw [← mul_assoc, mul_comm _ (u : ℂ), mul_assoc, div_mul_cancel₀ _ x00]
+      simpa [xeu] using e
   · intro t ⟨m, e⟩; simp only [mem_closure_iff_frequently] at e ⊢
     have rc : ∀ {x : ℂ}, (c, x) ∈ s.ext → ContinuousAt (fun t : ℝ ↦ s.ray c (↑t * x)) t :=
       fun {x} p ↦