Bump mathlib

Author: vbeffara

RMT4.lean

@@ -101,9 +101,8 @@ lemma 𝓘_nonempty [good_domain U] : (𝓘 U).Nonempty := by
     have f_eq_comp := (good_domain.is_open.eventually_mem hz₀).mono g_sqf
     have dg_nonzero : deriv g z₀ ≠ 0 := by
       have e3 := e2.differentiableAt.deriv_eq_deriv_pow_div_pow zero_lt_two f_eq_comp (f_noz hz₀)
-      simp [e3, deriv_sub_const]
+      simp [e3, deriv_sub_const, f]
       intro h
-      norm_num at h
       have := g_sqf hz₀
       rw [Pi.pow_apply, h, zero_pow two_ne_zero] at this
       cases f_noz hz₀ this

RMT4/Bunch.lean

@@ -49,8 +49,8 @@ lemma eventuallyEq (hi : a ∈ B.S i) (hj : a ∈ B.S j) (h : B i a = B j a) :
 lemma tile_inter {s₁ s₂ : Set α} (hi₁ : i₁ ∈ B.idx z) (hi₂ : i₂ ∈ B.idx z) (hi : i ∈ B.idx z)
     (h₁ : s₁ ∈ 𝓝 z.1) (h₂ : s₂ ∈ 𝓝 z.1) :
     ∃ s ∈ 𝓝 z.1, B.tile i s ⊆ B.tile i₁ s₁ ∩ B.tile i₂ s₂ := by
-  suffices : ∀ᶠ b in 𝓝 z.1, (b, B i b) ∈ B.tile i₁ s₁ ∩ B.tile i₂ s₂
-  · simpa only [eventually_iff_exists_mem, ← subset_iff_forall] using this
+  suffices h : ∀ᶠ b in 𝓝 z.1, (b, B i b) ∈ B.tile i₁ s₁ ∩ B.tile i₂ s₂
+    by simpa only [eventually_iff_exists_mem, ← subset_iff_forall] using h
   have l1 := eventuallyEq hi₁.1 hi.1 (hi₁.2.trans hi.2.symm)
   have l2 := eventuallyEq hi₂.1 hi.1 (hi₂.2.trans hi.2.symm)
   filter_upwards [h₁, h₂, l1, l2] with b e1 e2 e3 e4
@@ -120,7 +120,11 @@ theorem nhd_is_nhd (a : space B) (s : Set (space B)) (hs : s ∈ nhd a) :
     · simp only [nhd, h, dite_false] ; simp
     · simp [hs]
 
-lemma nhds_eq_nhd : 𝓝 z = nhd z := nhds_mkOfNhds _ _ pure_le nhd_is_nhd
+lemma nhds_eq_nhd : 𝓝 z = nhd z := by
+  refine nhds_mkOfNhds _ _ pure_le ?_
+  intro a s hs
+  obtain ⟨t, h1, _, h3⟩ := nhd_is_nhd a s hs -- TODO simplify `nhd_is_nhd`
+  apply eventually_of_mem h1 h3
 
 lemma mem_nhds_tfae (h : Nonempty (B.idx z)) : List.TFAE [
       s ∈ 𝓝 z,

RMT4/Covering.lean

@@ -121,8 +121,8 @@ lemma nhd_from_eq_nhd {z : covering Λ} (h : ↑z.1 ∈ Λ.S x) : nhd_from x z =
 lemma nhd_eq_toBunch_nhd : nhd = Λ.toBunch.nhd := by
   ext ⟨a, b⟩ s
   have : Nonempty (Λ.toBunch.idx (a, b)) := by
-    simp [toBunch, Bunch.idx, FF]
-    refine ⟨a.1, a.prop, Λ.mem a, b, by ring⟩
+    dsimp [toBunch, Bunch.idx, FF]
+    exact ⟨(a, b), Λ.mem a, by ring⟩
   simp only [Bunch.nhd, this, dite_true, IsBasis.mem_filter_iff]
   constructor
   · intro h

RMT4/Glue.lean

@@ -103,8 +103,8 @@ lemma Continuous.Iic_extend' (hf : Continuous f) : Continuous (IicExtend f) :=
 lemma continuous_glue_Iic (hf : Continuous f) (hg : Continuous g)
     (h : f ⟨a, le_rfl⟩ = g ⟨a, ⟨inf_le_left, le_sup_left⟩⟩) : Continuous (glue_Iic f g) := by
   rw [glue_Iic_eq]
-  suffices : Continuous fun t => if t ≤ a then IicExtend f t else IccExtend inf_le_sup g t
-  · exact this.comp continuous_subtype_val
+  suffices h : Continuous fun t => if t ≤ a then IicExtend f t else IccExtend inf_le_sup g t
+    by exact h.comp continuous_subtype_val
   refine hf.Iic_extend'.if_le hg.Icc_extend' continuous_id continuous_const ?_
   rintro x rfl ; simpa [IccExtend_of_mem] using h
 

RMT4/Lift.lean

@@ -3,6 +3,7 @@ import Mathlib.Analysis.Convex.Segment
 import Mathlib.Topology.Covering
 import Mathlib.Topology.LocallyConstant.Basic
 import RMT4.Glue
+import Mathlib
 
 open Set Topology Metric unitInterval Filter ContinuousMap
 
@@ -29,6 +30,25 @@ instance : Zero (Iic t) := ⟨0, nonneg'⟩
 def reachable (f : E → X) (γ : C(I, X)) (A : E) (t : I) : Prop :=
   ∃ Γ : C(Iic t, E), Γ 0 = A ∧ ∀ s, f (Γ s) = γ s
 
+def reachable' (f : E → X) (γ : C(I, X)) (A : E) (t : I) : Prop :=
+  ∃ Γ : C(I, E), Γ 0 = A ∧ ∀ s ≤ t, f (Γ s) = γ s
+
+example : reachable f γ A t ↔ reachable' f γ A t := by
+  constructor
+  · rintro ⟨Γ, h1, h2⟩
+    refine ⟨⟨IicExtend Γ, ?_⟩, ?_, ?_⟩
+    · apply Continuous.comp Γ.2
+      apply Continuous.subtype_mk
+      apply continuous_const.min continuous_id
+    · simp [IicExtend, projIic, min, ← h1]
+      congr
+      simp [inf_eq_right, t.2.1]
+    · intro s hs
+      specialize h2 ⟨s, hs⟩
+      simp at h2
+      simp [← h2, IicExtend, projIic, min_eq_right hs]
+  · sorry
+
 lemma reachable_zero (hγ : γ 0 = f A) : reachable f γ A 0 := by
   refine ⟨⟨λ _ => A, continuous_const⟩, rfl, ?_⟩
   intro ⟨s, (hs : s ≤ 0)⟩ ; simp [le_antisymm hs s.2.1, hγ]
@@ -42,7 +62,7 @@ lemma reachable_extend {T : Trivialization (f ⁻¹' {γ t}) f} (h : MapsTo γ (
   have l1 : f (Γ T₁) = γ t₁ := h2 T₁
   have l2 : Γ T₁ ∈ T.source := T.mem_source.2 <| l1 ▸ h left_mem_uIcc
   refine ⟨trans_Iic Γ δ ?_, trans_Iic_of_le nonneg', λ s => ?_⟩
-  · simpa only [ContinuousMap.coe_mk, ← l1, ← T.proj_toFun _ l2] using (T.left_inv' l2).symm
+  · simpa only [T₁, δ, ContinuousMap.coe_mk, ← l1, ← T.proj_toFun _ l2] using (T.left_inv' l2).symm
   · by_cases H : s ≤ t₁ <;> simp only [trans_Iic, glue_Iic, ContinuousMap.coe_mk, H, dite_true, h2]
     have l5 : γ s ∈ T.baseSet := h ⟨inf_le_left.trans (not_le.1 H).le, le_trans s.2 le_sup_right⟩
     have l6 {z} : (γ s, z) ∈ T.target := T.mem_target.2 l5
@@ -74,11 +94,13 @@ theorem Lift (hf : IsCoveringMap f) (hγ : γ 0 = f A) : ∃! Γ : C(I, E), Γ 0
   have l2 : IsClopen {t | reachable f γ A t} := isClopen_iff_nhds.2 (λ t => reachable_nhds_iff hf)
   let ⟨Γ, h1, h2⟩ := ((isClopen_iff.1 l2).resolve_left <| Nonempty.ne_empty l1).symm ▸ mem_univ 1
   let Γ₁ : C(I, E) := ⟨IicExtend Γ, Γ.2.Iic_extend'⟩
-  have l3 : Γ₁ 0 = A := by simpa [IicExtend, projIic] using h1
+  have l3 : Γ₁ 0 = A := by simpa [Γ₁, IicExtend, projIic] using h1
   have l4 : f ∘ Γ₁ = γ := by
     ext1 s
     simp only [IicExtend, coe_mk, Function.comp_apply, projIic]
     convert h2 ⟨s, s.2.2⟩
+    simp [Γ₁, IicExtend, projIic]
+    congr
     simpa using s.2.2
   refine ⟨Γ₁, ⟨l3, l4⟩, ?_⟩
   intro Γ₂ ⟨hh1, hh2⟩
@@ -151,7 +173,7 @@ theorem HLL (hp : IsCoveringMap p) (f₀ : C(Y, X)) (F : C(Y × I, X)) (hF : ∀
     ext ⟨y, t⟩
     let Hy : C(I, E) := ⟨λ t => H (y, t), sorry⟩
     have h4 : (p ∘ fun t => H (y, t)) = fun t => F (y, t) := sorry
-    simp [← hG2 y Hy ⟨hH2 y, h4⟩]
+    simp [← hG2 y Hy ⟨hH2 y, h4⟩, Hy]
 
 -- theorem HomLift (hf : IsCoveringMap f) (h0 : γ (0, 0) = f e) :
 --     ∃ Γ : C(I × I, E), Γ (0, 0) = e ∧ f ∘ Γ = γ := by

RMT4/Primitive.lean

@@ -64,7 +64,7 @@ lemma DifferentiableOn.exists_primitive (f_holo : DifferentiableOn ℂ f U)
   have φ_diff {t} (ht : t ∈ I) : DifferentiableOn ℂ (λ w => φ w t) U :=
     f_holo.comp differentiable_bary.differentiableOn (λ z hz => hU.bary hz ht)
   have φ_derz {z} (hz : z ∈ U) {t} (ht : t ∈ I) : HasDerivAt (λ x => φ x t) (ψ z t) z := by
-    convert (f_deri (hU.bary hz ht)).comp z hasDerivAt_bary' ; simp ; ring
+    convert (f_deri (hU.bary hz ht)).comp z hasDerivAt_bary' ; simp [ψ] ; ring
   have φ_dert {t} (ht : t ∈ I) : HasDerivAt (φ z) ((z - z₀) * _root_.deriv f ((1 - t) • z₀ + t • z)) t := by
     convert (f_deri (hU.bary hz ht)).comp t has_deriv_at_bary using 1 ; ring
   have ψ_cont : ContinuousOn (ψ z) I :=
@@ -91,7 +91,7 @@ lemma DifferentiableOn.exists_primitive (f_holo : DifferentiableOn ℂ f U)
         rw [(φ_derz (K_subs hw) ht).deriv]
         have f_bary := hC _ ((K_conv.starConvex hz₀).bary hw ht)
         have ht' : |t| ≤ 1 := by { rw [abs_le] ; constructor <;> linarith [ht.1, ht.2] }
-        simpa [abs_eq_self.2 C_nonneg] using mul_le_mul ht' f_bary (by simp) (by simp)
+        simpa [ψ, abs_eq_self.2 C_nonneg] using mul_le_mul ht' f_bary (by simp) (by simp)
 
     apply has_deriv_at_integral_of_continuous_of_lip zero_le_one δ_pos
     · exact eventually_of_mem (hU'.mem_nhds hz) (λ _ => φ_cont)
@@ -107,22 +107,22 @@ lemma DifferentiableOn.exists_primitive (f_holo : DifferentiableOn ℂ f U)
     have g_dert : ∀ t ∈ Ioo (0:ℝ) 1, HasDerivAt g (h t) t := by
       rintro t ht
       convert (hasDerivAt_id t).smul (φ_dert (Ioo_subset_Icc_self ht)) using 1
-      simp [add_comm] ; ring
+      simp [ψ, h, add_comm] ; ring
     have h_intg : IntervalIntegrable h volume (0:ℝ) 1 := by
       apply ContinuousOn.intervalIntegrable
-      simp only [Interval, min_eq_left, zero_le_one, max_eq_right]
+      simp only [h, Interval, min_eq_left, zero_le_one, max_eq_right]
       convert (φ_cont hz).add (continuousOn_const.mul ψ_cont) ; simp
 
     convert ← integral_eq_sub_of_hasDerivAt_of_le zero_le_one g_cont g_dert h_intg using 1
-    · simp only
+    · simp only [ψ, h]
       rw [intervalIntegral.integral_add]
       · simp
       · apply ContinuousOn.intervalIntegrable ; convert φ_cont hz ; simp [Interval]
       · apply ContinuousOn.intervalIntegrable
         refine continuousOn_const.mul ?_
         convert ψ_cont
         simp
-    · simp [detail.φ]
+    · simp [g, φ, detail.φ]
 
   have : HasDerivAt (primitive f z₀)
       ((∫ t in (0:ℝ)..1, φ z t) + (z - z₀) * ∫ t in (0:ℝ)..1, ψ z t) z := by

RMT4/cindex.lean

@@ -180,7 +180,6 @@ lemma exists_cindex_eq_order (hp : HasFPowerSeriesAt f p z₀) :
       exact hr.2
     rw [circleIntegral.integral_congr hr.1.le this]
     simp [circleIntegral]
-    exact intervalIntegral.integral_zero
 
 lemma cindex_eventually_eq_order (hp : HasFPowerSeriesAt f p z₀) :
     ∀ᶠ r in 𝓝[>] 0, cindex z₀ r f = p.order := by

RMT4/deriv_inj.lean

@@ -14,13 +14,13 @@ lemma crucial (hU : IsOpen U) (hcr : closedBall c r ⊆ U) (hz₀ : z₀ ∈ bal
   have h2 : ∀ z ∈ closedBall c r, g z ≠ 0 := by
     rintro z hz
     by_cases h : z = z₀
-    case pos => simp [dslope, h, Function.update, hf'z₀]
-    case neg => simp [dslope, h, Function.update, slope, sub_ne_zero.2 h, hfz₀, hfz z hz h]
+    case pos => simp [g, dslope, h, Function.update, hf'z₀]
+    case neg => simp [g, dslope, h, Function.update, slope, sub_ne_zero.2 h, hfz₀, hfz z hz h]
   have h10 : ∀ z ∈ sphere c r, z - z₀ ≠ 0 :=
     λ z hz => sub_ne_zero.2 (sphere_disjoint_ball.ne_of_mem hz hz₀)
-  suffices : cindex c r f = ((2 * Real.pi * I)⁻¹ * ∮ z in C(c, r), (z - z₀)⁻¹) + cindex c r g
-  · rw [this, integral_sub_inv_of_mem_ball hz₀, cindex_eq_zero hU hr hcr h1 h2]
-    field_simp [two_ne_zero, Real.pi_ne_zero, I_ne_zero]
+  suffices this : cindex c r f = ((2 * Real.pi * I)⁻¹ * ∮ z in C(c, r), (z - z₀)⁻¹) + cindex c r g
+    by rw [this, integral_sub_inv_of_mem_ball hz₀, cindex_eq_zero hU hr hcr h1 h2]
+       field_simp [two_ne_zero, Real.pi_ne_zero, I_ne_zero]
   have h6 : ∀ z ∈ sphere c r, deriv f z / f z = (z - z₀)⁻¹ + deriv g z / g z := by
     rintro z hz
     have h3 : ∀ z ∈ U, f z = (z - z₀) * g z :=

RMT4/etape2.lean

@@ -70,7 +70,7 @@ lemma non_injective_schwarz {f : ℂ → ℂ} (f_diff : DifferentiableOn ℂ f 
   let g := φ u_in_𝔻 ∘ f
   have g_diff : DifferentiableOn ℂ g 𝔻 := (φ u_in_𝔻).is_diff.comp f_diff f_img
   have g_maps : MapsTo g 𝔻 𝔻 := (φ u_in_𝔻).maps_to.comp f_img
-  have g_0_eq_0 : g 0 = 0 := by simp [φ]
+  have g_0_eq_0 : g 0 = 0 := by simp [g, φ]
   by_cases h : ‖deriv g 0‖ = 1
   case pos =>
     have g_lin : EqOn g (λ (z : ℂ) => z • deriv g 0) (ball 0 1) := by
@@ -123,22 +123,22 @@ lemma step_2 (hz₀ : z₀ ∈ U) (f : embedding U 𝔻) (hf : f '' U ⊂ 𝔻)
   have φᵤf_ne_zero : ∀ z ∈ U, φᵤf z ≠ 0 := λ z z_in_U hz => by
     refine u_not_in_f_U ⟨z, z_in_U, ?_⟩
     apply φᵤ.is_inj (f.maps_to z_in_U) u_in_𝔻
-    dsimp at hz
+    dsimp [φᵤf] at hz
     rw [hz]
-    simp [φ]
+    simp [φᵤ, φ]
   obtain ⟨g, hg⟩ := φᵤf.sqrt' φᵤf_ne_zero
   let v : ℂ := g z₀
   have v_in_𝔻 : v ∈ 𝔻 := g.maps_to hz₀
   let h : embedding U 𝔻 := (φ v_in_𝔻).comp g
-  have h_z₀_eq_0 : h z₀ = 0 := by simp [φ]
+  have h_z₀_eq_0 : h z₀ = 0 := by simp [h, φ]
   let σ : ℂ → ℂ := λ z => z ^ 2
   let ψ : ℂ → ℂ := φ (neg_in_𝔻 u_in_𝔻) ∘ σ ∘ φ (neg_in_𝔻 v_in_𝔻)
   have f_eq_ψ_h : EqOn f (ψ ∘ h) U := λ z hz => by
     have e1 := φ_inv v_in_𝔻 (g.maps_to hz)
     have e2 := hg hz
     have e3 := φ_inv u_in_𝔻 (f.maps_to hz)
-    dsimp at e2
-    simp [e1, ← e2, e3]
+    dsimp [φᵤf] at e2
+    simp [ψ, σ, h, e1, ← e2, e3]
   have ψ_is_diff : DifferentiableOn ℂ ψ 𝔻 := by
     refine (φ (neg_in_𝔻 u_in_𝔻)).is_diff.comp ?_ ?_
     · apply DifferentiableOn.comp
@@ -152,7 +152,7 @@ lemma step_2 (hz₀ : z₀ ∈ U) (f : embedding U 𝔻) (hf : f '' U ⊂ 𝔻)
         exact (φ (neg_in_𝔻 v_in_𝔻)).maps_to
     · refine MapsTo.comp ?_ (φ (neg_in_𝔻 v_in_𝔻)).maps_to
       intros z hz
-      simpa [𝔻] using hz
+      simpa [σ, 𝔻] using hz
   have deriv_eq_mul : deriv f z₀ = deriv ψ 0 * deriv h z₀ := by
     have e1 : U ∈ 𝓝 z₀ := good_domain.is_open.mem_nhds hz₀
     have e2 : 𝔻 ∈ 𝓝 (0 : ℂ) := ball_mem_nhds _ zero_lt_one
@@ -166,12 +166,13 @@ lemma step_2 (hz₀ : z₀ ∈ U) (f : embedding U 𝔻) (hf : f '' U ⊂ 𝔻)
   · exact norm_pos_iff.2 (embedding.deriv_ne_zero good_domain.is_open hz₀)
   · apply non_injective_schwarz ψ_is_diff
     · refine λ z hz => (φ (neg_in_𝔻 u_in_𝔻)).maps_to (mem_𝔻_iff.mpr ?_)
-      simpa using mem_𝔻_iff.mp ((φ (neg_in_𝔻 v_in_𝔻)).maps_to hz)
+      simpa [σ] using mem_𝔻_iff.mp ((φ (neg_in_𝔻 v_in_𝔻)).maps_to hz)
     · simp only [InjOn, not_forall, exists_prop]
       have e1 : (2⁻¹ : ℂ) ∈ 𝔻 := by apply mem_𝔻_iff.mpr; norm_num
       have e2 : (-2⁻¹ : ℂ) ∈ 𝔻 := neg_in_𝔻 e1
       refine ⟨φ v_in_𝔻 2⁻¹, (φ v_in_𝔻).maps_to e1, φ v_in_𝔻 (-2⁻¹), (φ v_in_𝔻).maps_to e2, ?_, ?_⟩
-      · simp [φ_inv v_in_𝔻 e1, φ_inv v_in_𝔻 e2]
+      · unfold_let
+        simp [φ_inv v_in_𝔻 e1, φ_inv v_in_𝔻 e2]
       · intro h
         have := (φ v_in_𝔻).is_inj e1 e2 h
         norm_num at this

RMT4/has_sqrt.lean

@@ -23,7 +23,7 @@ lemma EqOn_zero_of_deriv_eq_zero (hU : IsOpen U) (hU' : IsPreconnected U) {f : 
   refine eventually_nhds_iff.2 ⟨r, hr, λ z hz => ?_⟩
   rw [Pi.zero_apply, ← hfz₀]
   suffices h : ∀ z ∈ ball z₀ r, fderivWithin ℂ f (ball z₀ r) z = 0
-  { exact (convex_ball z₀ r).is_const_of_fderivWithin_eq_zero (hf.mono hrU) h hz (mem_ball_self hr) }
+    by exact (convex_ball z₀ r).is_const_of_fderivWithin_eq_zero (hf.mono hrU) h hz (mem_ball_self hr)
   rintro w hw
   have : UniqueDiffWithinAt ℂ (ball z₀ r) w := isOpen_ball.uniqueDiffWithinAt hw
   rw [fderivWithin_eq_fderiv this (hf.differentiableAt (hU.mem_nhds (hrU hw)))]
@@ -34,8 +34,8 @@ lemma EqOn_of_deriv_eq_zero (hU : IsOpen U) (hU' : IsPreconnected U) {f : ℂ 
     (hf : DifferentiableOn ℂ f U) (hf' : EqOn (deriv f) 0 U) (hz₀ : z₀ ∈ U) :
     EqOn f (λ _ => f z₀) U := by
   set g := λ z => f z - f z₀
-  have h2 : EqOn (deriv g) 0 U := λ z hz => by simp [deriv_sub_const, hf' hz]
-  have h3 : g z₀ = 0 := by simp
+  have h2 : EqOn (deriv g) 0 U := λ z hz => by rw [deriv_sub_const, hf' hz]
+  have h3 : g z₀ = 0 := by simp [g]
   have := EqOn_zero_of_deriv_eq_zero hU hU' (hf.sub_const _) h2 hz₀ h3
   exact λ z hz => sub_eq_zero.1 (this hz)
 
@@ -70,15 +70,16 @@ lemma has_primitives.has_logs (hp : has_primitives U) (hU : IsOpen U) (hU' : IsP
     have e4 : DifferentiableOn ℂ (exp ∘ g) U := differentiable_exp.comp_differentiableOn h3
     have e1 : DifferentiableOn ℂ h U := hf.div e4 (λ z _ => exp_ne_zero _)
     refine ⟨g, h3, ?_⟩
-    suffices : EqOn h (λ _ => 1) U
-    · exact λ z hz => eq_of_div_eq_one (this hz)
-    have : 1 = h z₀ := by simp [exp_log, hfz z₀ hz₀]
+    suffices h : EqOn h (λ _ => 1) U
+      by exact λ z hz => eq_of_div_eq_one (h hz)
+    have : 1 = h z₀ := by unfold_let ; simp [exp_log, hfz z₀ hz₀]
     rw [this]
     refine EqOn_of_deriv_eq_zero hU hU' e1 (λ z hz => ?_) hz₀
     have f0 : U ∈ 𝓝 z := hU.mem_nhds hz
     dsimp
+    unfold_let
     rw [Pi.div_def, deriv_div (hf.differentiableAt f0) (e4.differentiableAt f0) (exp_ne_zero _)]
     rw [deriv.scomp z differentiableAt_exp (h3.differentiableAt f0)]
-    have e5 : deriv g z = deriv lf z := by simp
+    have e5 : deriv g z = deriv lf z := by unfold_let ; simp
     field_simp [exp_ne_zero, hlf2 hz, hfz z hz, e5]
     ring

RMT4/hurwitz.lean

@@ -403,9 +403,9 @@ theorem hurwitz_inj [NeBot p]
   have hg : TendstoLocallyUniformlyOn G g p U :=
     hurwitz4 hf (uniformContinuous_id.sub uniformContinuous_const)
   have hgx : g x = 0 := sub_self _
-  have hgy : g y = 0 := by simp [hfxy]
-  suffices : ∀ z ∈ U, g z = 0
-  · exact ⟨f x, by simpa [sub_eq_zero] using this⟩
+  have hgy : g y = 0 := by simp [g, hfxy]
+  suffices this : ∀ z ∈ U, g z = 0
+    by exact ⟨f x, by simpa [sub_eq_zero, g] using this⟩
   --
   contrapose hi; simp only [not_frequently, InjOn, not_forall]
   have h1 : DifferentiableOn ℂ g U := hg.differentiableOn hG hU

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "f1cae6351cf7010d504e6652f05e8aa2da0dd4cb",
+   "rev": "ff9850c4726f6b9fb8d8e96980c3fcb2900be8bd",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "190ec9abbc4cd43b1b6a1401722c0b54418a98b0",
+   "rev": "fd760831487e6835944e7eeed505522c9dd47563",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "1f200b89e635064ba6f614ae82c7aced0b28d929",
+   "rev": "056ca0fa8f5585539d0b940f532d9750c3a2270f",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,10 +31,10 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "f5b2b6ff817890d85ffd8ed47637e36fcac544a6",
+   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.28",
+   "inputRev": "v0.0.30",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "9618fa9d33d128679a5e376a9ffd3c9440b088f4",
+   "rev": "64d082eeaad1a8e6bbb7c23b7a16b85a1715a02f",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,12 +58,21 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "998cfc8bbcf09a654986ea0e26373c1f7d1bd6eb",
+   "rev": "16003723509e6a2d8517dac98e096e3b3ca6b1de",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
    "inherited": false,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/PatrickMassot/checkdecls.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "2ee81a0269048010900117b675876a1d8db5883c",
+   "name": "checkdecls",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": false,
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/xubaiw/CMark.lean",
    "type": "git",
    "subDir": null,
@@ -99,15 +108,6 @@
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/PatrickMassot/checkdecls.git",
-   "type": "git",
-   "subDir": null,
-   "rev": "2ee81a0269048010900117b675876a1d8db5883c",
-   "name": "checkdecls",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": null,
-   "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "rMT4",
  "lakeDir": ".lake"}