awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (hypothesis)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn : Asymptotics.IsLittleO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 c) (fun (x : E) ↦ f x - f c) fun (w : E) ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : Eq (α := ℂ) ((g : (a : F) → ℂ) (f z - f c) : ℂ) ((↑‖f z - f c‖ : ℂ) : ℂ)
h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E)
hmaps_line : MapsTo (α := ℂ) (⇑(lineMap c z) : (a : ℂ) → E) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
hdiff : DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)
have hn₁ : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 0) (fun (x : ℂ) ↦ h x - h 0) fun (w : ℂ) ↦ (w - 0) ^ n
Tactic: have hn : (h · - h 0) =o[𝓝 0] (fun w ↦ (w - 0) ^ n) := by
    simp only [h, ← map_sub, Function.comp_apply, sub_zero]
    refine (g.isBigO_comp _ _).trans_isLittleO ?_
    rw [← lineMap_apply_zero (k := ℂ) c z] at hn
    refine hn.comp_tendsto ?_ |>.trans_isBigO ?_
    · exact Continuous.tendsto (by fun_prop) 0
    · simpa [Function.comp_def, ← dist_eq_norm_sub, mul_pow, mul_comm]
        using (Asymptotics.isBigO_refl (· ^ n) (𝓝 (0 : ℂ))).norm_left.const_mul_left _
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (hypothesis)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn_1 : Asymptotics.IsLittleO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 c) (fun (x : E) ↦ f x - f c) fun (w : E) ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : Eq (α := ℂ) ((g : (a : F) → ℂ) (f z - f c) : ℂ) ((↑‖f z - f c‖ : ℂ) : ℂ)
h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E)
hmaps_line : MapsTo (α := ℂ) (⇑(lineMap c z) : (a : ℂ) → E) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
hdiff : DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 0) (fun (x : ℂ) ↦ h x - h 0) fun (w : ℂ) ↦ (w - 0) ^ n
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)
have hmem : Membership.mem (γ := Set ℂ) (ball 0 (R₁ / dist z c)) 1
Tactic: have hmem : 1 ∈ ball (0 : ℂ) (R₁ / dist z c) := by
    simpa [lt_div_iff₀, hne]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (hypothesis)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
c z : E
R₁ R₂ : ℝ
n : ℕ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hn_1 : Asymptotics.IsLittleO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 c) (fun (x : E) ↦ f x - f c) fun (w : E) ↦ ‖w - c‖ ^ n
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 ≤ R₂
hfne : f z ≠ f c
hne : z ≠ c
g : StrongDual ℂ F
hg : ‖g‖ = 1
hgf : Eq (α := ℂ) ((g : (a : F) → ℂ) (f z - f c) : ℂ) ((↑‖f z - f c‖ : ℂ) : ℂ)
h : ℂ → ℂ := (⇑g : (a : F) → ℂ) ∘ f ∘ (⇑(lineMap c z) : (a : ℂ) → E)
hmaps_line : MapsTo (α := ℂ) (⇑(lineMap c z) : (a : ℂ) → E) (ball 0 (R₁ / dist z c)) (ball c R₁)
hmaps : MapsTo h (ball 0 (R₁ / dist z c)) (closedBall (h 0) R₂)
hdiff : DifferentiableOn ℂ h (ball 0 (R₁ / dist z c))
hn : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝 0) (fun (x : ℂ) ↦ h x - h 0) fun (w : ℂ) ↦ (w - 0) ^ n
hmem : Membership.mem (γ := Set ℂ) (ball 0 (R₁ / dist z c)) 1
⊢ dist (f z) (f c) ≤ R₂ * (dist z c / R₁) ^ (n + 1)
have hgf₁ : HSub.hSub (α := ℂ) (β := ℂ) ((g : (a : F) → ℂ) (f z) : ℂ) ((g : (a : F) → ℂ) (f c) : ℂ) = (↑‖f z - f c‖ : ℂ)
Tactic: rw [map_sub] at hgf
Cleared hypotheses: hgf, h, hmaps_line, hmaps, hdiff, hn, hmem
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
R₁ R₂ : ℝ
f : E → F
c z : E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
⊢ dist (f z) (f c) ≤ R₂ / R₁ * dist z c
have refine_1 : Asymptotics.IsLittleO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 c) (fun (x : E) ↦ f x - f c) fun (w : E) ↦
  HPow.hPow (β := ℕ) ‖w - c‖ 0
Tactic: refine dist_le_mul_div_pow_of_mapsTo_ball_of_isLittleO (n := 0) hd h_maps ?_ hz |>.trans_eq ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
R₁ R₂ : ℝ
f : E → F
c z : E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
refine_1 :
  Asymptotics.IsLittleO.{u_1, u_2, 0} (E := F) (F := ℝ) (𝓝 c) (fun (x : E) ↦ f x - f c) fun (w : E) ↦
    HPow.hPow (β := ℕ) ‖w - c‖ 0
⊢ dist (f z) (f c) ≤ R₂ / R₁ * dist z c
have refine_2 : R₂ * (dist z c / R₁) ^ HAdd.hAdd (α := ℕ) 0 1 = R₂ / R₁ * dist z c
Tactic: refine dist_le_mul_div_pow_of_mapsTo_ball_of_isLittleO (n := 0) hd h_maps ?_ hz |>.trans_eq ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (hypothesis)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
R₁ R₂ : ℝ
f : E → F
c : E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h₀ : 0 < R₁
⊢ norm (E := E →L[ℂ] F) (fderiv ℂ f c) ≤ R₂ / R₁
have this : 0 ≤ R₂
Tactic: have : 0 ≤ R₂ := nonempty_closedBall.mp <| h_maps.nonempty <| nonempty_ball.mpr h₀
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
R₁ R₂ : ℝ
f : E → F
c : E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h₀ : 0 < R₁
this : 0 ≤ R₂
⊢ norm (E := E →L[ℂ] F) (fderiv ℂ f c) ≤ R₂ / R₁
have refine : ∀ᶠ (x : E) in 𝓝 c, ‖f x - f c‖ ≤ R₂ / R₁ * ‖x - c‖
Tactic: refine norm_fderiv_le_of_lip' _ (by positivity) ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
R₁ R₂ : ℝ
f : E → F
c : E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h₀ : 0 < R₁
this : 0 ≤ R₂
⊢ ∀ᶠ (x : E) in 𝓝 c, ‖f x - f c‖ ≤ R₂ / R₁ * ‖x - c‖
have h : ∀ (z : E) (hz : z ∈ ball c R₁), ‖f z - f c‖ ≤ R₂ / R₁ * ‖z - c‖
Tactic: filter_upwards [ball_mem_nhds _ h₀] with z hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h₀ : 0 < R₁
⊢ ‖deriv f c‖ ≤ R₂ / R₁
have rw : norm (E := ℂ →L[ℂ] E) (fderiv ℂ f c) ≤ R₂ / R₁
Tactic: rw [norm_deriv_eq_norm_fderiv]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
have inl : ∀ (hd : DifferentiableOn ℂ f (ball z R₁)) (h_maps : MapsTo f (ball z R₁) (closedBall (f z) R₂)) (hz : z ∈ ball z R₁),
  ‖dslope f z z‖ ≤ R₂ / R₁
Tactic: rcases eq_or_ne z c with rfl | hne
Cleared hypotheses: c, hd, h_maps, hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
inl :
  ∀ (hd : DifferentiableOn ℂ f (ball z R₁)) (h_maps : MapsTo f (ball z R₁) (closedBall (f z) R₂)) (hz : z ∈ ball z R₁),
    ‖dslope f z z‖ ≤ R₂ / R₁
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
have inr : ∀ (hne : z ≠ c), ‖dslope f c z‖ ≤ R₂ / R₁
Tactic: rcases eq_or_ne z c with rfl | hne
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
hne : z ≠ c
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
have inr : dist (f z) (f c) ≤ R₂ / R₁ * dist z c
Tactic: rw [dslope_of_ne _ hne, slope_def_module, norm_smul, norm_inv, ← dist_eq_norm_sub,
      ← dist_eq_norm_sub, ← div_eq_inv_mul, div_le_iff₀]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
hz : z ∈ ball c R₁
hne : z ≠ c
inr : dist (f z) (f c) ≤ R₂ / R₁ * dist z c
⊢ ‖dslope f c z‖ ≤ R₂ / R₁
have inr₁ : 0 < dist z c
Tactic: rw [dslope_of_ne _ hne, slope_def_module, norm_smul, norm_inv, ← dist_eq_norm_sub,
      ← dist_eq_norm_sub, ← div_eq_inv_mul, div_le_iff₀]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst_2 : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope ((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
⊢ f z = (fun (z : ℂ) ↦ f c + (z - c) • dslope f c z₀) z
have h_R₁ : 0 < R₁
Tactic: have h_R₁ : 0 < R₁ := nonempty_ball.mp ⟨_, h_z₀⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst_2 : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope ((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
⊢ g = (⇑e : (a : E) → UniformSpace.Completion E) ∘ dslope f c
have h : ∀ (w : ℂ), g w = ((⇑e : (a : E) → UniformSpace.Completion E) ∘ dslope f c) w
Tactic: ext w
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst_2 : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope ((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
w : ℂ
⊢ Eq (α := UniformSpace.Completion E) (dslope ((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) c w)
    (((⇑e : (a : E) → UniformSpace.Completion E) ∘ dslope f c) w)
have h : c = w → DifferentiableAt ℂ f c
Tactic: rw [e.dslope_comp, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst_2 : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope ((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
⊢ f z = (fun (z : ℂ) ↦ f c + (z - c) • dslope f c z₀) z
have hg' : g = (⇑e : (a : E) → UniformSpace.Completion E) ∘ dslope f c
Tactic: have hg' : g = e ∘ dslope f c := by
    ext w
    simp only [g]
    rw [e.dslope_comp, Function.comp_apply]
    rintro rfl
    exact hd.differentiableAt <| ball_mem_nhds _ h_R₁
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst_2 : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope ((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
hg' : g = (⇑e : (a : E) → UniformSpace.Completion E) ∘ dslope f c
⊢ f z = (fun (z : ℂ) ↦ f c + (z - c) • dslope f c z₀) z
have g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁
Tactic: have g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁ := fun z hz =>
    norm_dslope_le_div_of_mapsTo_ball (e.differentiable.comp_differentiableOn hd)
      (fun w hw ↦ by simpa [e] using h_maps hw) hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst_2 : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope ((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
hg' : g = (⇑e : (a : E) → UniformSpace.Completion E) ∘ dslope f c
g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁
⊢ f z = (fun (z : ℂ) ↦ f c + (z - c) • dslope f c z₀) z
have g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀
Tactic: have g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀ :=
    isMaxOn_iff.mpr fun z hz => by simpa [h_eq, hg', e] using g_le_div z hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst_2 : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope ((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
hg' : g = (⇑e : (a : E) → UniformSpace.Completion E) ∘ dslope f c
g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁
g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀
⊢ f z = (fun (z : ℂ) ↦ f c + (z - c) • dslope f c z₀) z
have g_diff : DifferentiableOn ℂ g (ball c R₁)
Tactic: have g_diff : DifferentiableOn ℂ g (ball c R₁) :=
    (differentiableOn_dslope (isOpen_ball.mem_nhds (mem_ball_self h_R₁))).mpr
      (e.differentiable.comp_differentiableOn hd)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst_2 : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope ((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
hg' : g = (⇑e : (a : E) → UniformSpace.Completion E) ∘ dslope f c
g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁
g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀
g_diff : DifferentiableOn ℂ g (ball c R₁)
⊢ f z = (fun (z : ℂ) ↦ f c + (z - c) • dslope f c z₀) z
have heq : ‖dslope f c z‖ = ‖dslope f c z₀‖
Tactic: have heq : ‖dslope f c z‖ = ‖dslope f c z₀‖ := by
    simpa [hg', e] using norm_eqOn_of_isPreconnected_of_isMaxOn (convex_ball c R₁).isPreconnected
      isOpen_ball g_diff h_z₀ g_max hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst_2 : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope ((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
hg' : g = (⇑e : (a : E) → UniformSpace.Completion E) ∘ dslope f c
g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁
g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀
g_diff : DifferentiableOn ℂ g (ball c R₁)
heq : ‖dslope f c z‖ = ‖dslope f c z₀‖
⊢ f z = (fun (z : ℂ) ↦ f c + (z - c) • dslope f c z₀) z
have heq_add : ‖dslope f c z + dslope f c z₀‖ = ‖dslope f c z₀ + dslope f c z₀‖
Tactic: have heq_add : ‖dslope f c z + dslope f c z₀‖ = ‖dslope f c z₀ + dslope f c z₀‖ := by
    simpa [hg', e, ← UniformSpace.Completion.coe_add]
      using norm_eqOn_of_isPreconnected_of_isMaxOn (convex_ball c R₁).isPreconnected
        isOpen_ball (g_diff.add_const (g z₀)) h_z₀ g_max.norm_add_self hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.Schwarz (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst_2 : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (closedBall (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
e : E →L[ℂ] UniformSpace.Completion E := UniformSpace.Completion.toComplL
g : ℂ → UniformSpace.Completion E := dslope ((⇑e : (a : E) → UniformSpace.Completion E) ∘ f) c
z : ℂ
hz : z ∈ ball c R₁
h_R₁ : 0 < R₁
hg' : g = (⇑e : (a : E) → UniformSpace.Completion E) ∘ dslope f c
g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁
g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀
g_diff : DifferentiableOn ℂ g (ball c R₁)
heq : ‖dslope f c z‖ = ‖dslope f c z₀‖
heq_add : ‖dslope f c z + dslope f c z₀‖ = ‖dslope f c z₀ + dslope f c z₀‖
⊢ f z = (fun (z : ℂ) ↦ f c + (z - c) • dslope f c z₀) z
have this : dslope f c z = dslope f c z₀
Tactic: have : dslope f c z = dslope f c z₀ := eq_of_norm_eq_of_norm_add_eq heq <| by
    simp only [heq, SameRay.rfl.norm_add, heq_add]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Spectrum (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : IsScalarTower ℂ A A
inst_3 : SMulCommClass ℂ A A
a : A
⊢ QuasispectrumRestricts (R := ℝ) (S := ℂ) a (⇑Complex.reCLM : (a : ℂ) → ℝ) ↔ ∀ x ∈ σₙ ℂ a, x = (↑x.re : ℂ)
have rw : SpectrumRestricts (R := ℝ) (S := ℂ) (A := Unitization ℂ A) (↑a : Unitization ℂ A) (⇑Complex.reCLM : (a : ℂ) → ℝ) ↔
  ∀ x ∈ σₙ ℂ a, x = (↑x.re : ℂ)
Tactic: rw [quasispectrumRestricts_iff_spectrumRestricts_inr,
    Unitization.quasispectrum_eq_spectrum_inr' _ ℂ, SpectrumRestricts.real_iff]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Spectrum (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : IsScalarTower ℂ A A
inst_3 : SMulCommClass ℂ A A
a : A
rw :
  SpectrumRestricts (R := ℝ) (S := ℂ) (A := Unitization ℂ A) (↑a : Unitization ℂ A) (⇑Complex.reCLM : (a : ℂ) → ℝ) ↔
    ∀ x ∈ σₙ ℂ a, x = (↑x.re : ℂ)
⊢ QuasispectrumRestricts (R := ℝ) (S := ℂ) a (⇑Complex.reCLM : (a : ℂ) → ℝ) ↔ ∀ x ∈ σₙ ℂ a, x = (↑x.re : ℂ)
have rw₁ : SpectrumRestricts (R := ℝ) (S := ℂ) (A := Unitization ℂ A) (↑a : Unitization ℂ A) (⇑Complex.reCLM : (a : ℂ) → ℝ) ↔
  ∀ x ∈ spectrum ℂ (A := Unitization ℂ A) (↑a : Unitization ℂ A), x = (↑x.re : ℂ)
Tactic: rw [quasispectrumRestricts_iff_spectrumRestricts_inr,
    Unitization.quasispectrum_eq_spectrum_inr' _ ℂ, SpectrumRestricts.real_iff]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Spectrum (goal)
Goal:
A : Type u_1
inst : NonUnitalRing A
inst_1 : Module ℂ A
inst_2 : IsScalarTower ℂ A A
inst_3 : SMulCommClass ℂ A A
a : A
rw :
  SpectrumRestricts (R := ℝ) (S := ℂ) (A := Unitization ℂ A) (↑a : Unitization ℂ A) (⇑Complex.reCLM : (a : ℂ) → ℝ) ↔
    ∀ x ∈ σₙ ℂ a, x = (↑x.re : ℂ)
rw₁ :
  SpectrumRestricts (R := ℝ) (S := ℂ) (A := Unitization ℂ A) (↑a : Unitization ℂ A) (⇑Complex.reCLM : (a : ℂ) → ℝ) ↔
    ∀ x ∈ spectrum ℂ (A := Unitization ℂ A) (↑a : Unitization ℂ A), x = (↑x.re : ℂ)
⊢ QuasispectrumRestricts (R := ℝ) (S := ℂ) a (⇑Complex.reCLM : (a : ℂ) → ℝ) ↔ ∀ x ∈ σₙ ℂ a, x = (↑x.re : ℂ)
have rw₂ : (∀ x ∈ spectrum ℂ (A := Unitization ℂ A) (↑a : Unitization ℂ A), x = (↑x.re : ℂ)) ↔
  ∀ x ∈ spectrum ℂ (A := Unitization ℂ A) (↑a : Unitization ℂ A), x = (↑x.re : ℂ)
Tactic: rw [quasispectrumRestricts_iff_spectrumRestricts_inr,
    Unitization.quasispectrum_eq_spectrum_inr' _ ℂ, SpectrumRestricts.real_iff]
-- Lean 4 proof step from Mathlib.Analysis.Complex.SqrtDeriv (goal)
Goal:
z : ℂ
hz : z ∈ slitPlane
⊢ 2⁻¹ * z ^ HSub.hSub (α := ℂ) 2⁻¹ 1 = z ^ (-1 / 2) / 2
have rw : 2⁻¹ * z ^ (-1 / 2) = z ^ (-1 / 2) / 2
Tactic: rw [show (2 : ℂ)⁻¹ - 1 = -1 / 2 by norm_num, mul_comm, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.Complex.SqrtDeriv (goal)
Goal:
z : ℂ
hz : z ∈ slitPlane
rw : 2⁻¹ * z ^ (-1 / 2) = z ^ (-1 / 2) / 2
⊢ 2⁻¹ * z ^ HSub.hSub (α := ℂ) 2⁻¹ 1 = z ^ (-1 / 2) / 2
have rw₁ : z ^ (-1 / 2) * 2⁻¹ = z ^ (-1 / 2) / 2
Tactic: rw [show (2 : ℂ)⁻¹ - 1 = -1 / 2 by norm_num, mul_comm, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.Complex.SqrtDeriv (goal)
Goal:
z : ℂ
hz : z ∈ slitPlane
rw : 2⁻¹ * z ^ (-1 / 2) = z ^ (-1 / 2) / 2
rw₁ : z ^ (-1 / 2) * 2⁻¹ = z ^ (-1 / 2) / 2
⊢ 2⁻¹ * z ^ HSub.hSub (α := ℂ) 2⁻¹ 1 = z ^ (-1 / 2) / 2
have rw₂ : z ^ (-1 / 2) / 2 = z ^ (-1 / 2) / 2
Tactic: rw [show (2 : ℂ)⁻¹ - 1 = -1 / 2 by norm_num, mul_comm, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.Complex.SummableUniformlyOn (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ι → ℂ → E
s : Set ℂ
hs : IsOpen s
h : SummableLocallyUniformlyOn f s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt ℂ (f n) r
⊢ DifferentiableOn.{0, 0, u_2} ℂ (F := E) (fun (z : ℂ) ↦ ∑' (n : ι), f n z) s
have obtain : ∀ (g : ℂ → E) (hg : HasSumLocallyUniformlyOn f g s),
  DifferentiableOn.{0, 0, u_2} ℂ (F := E) (fun (z : ℂ) ↦ ∑' (n : ι), f n z) s
Tactic: obtain ⟨g, hg⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.SummableUniformlyOn (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ι → ℂ → E
s : Set ℂ
hs : IsOpen s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt ℂ (f n) r
g : ℂ → E
hg : HasSumLocallyUniformlyOn f g s
⊢ DifferentiableOn.{0, 0, u_2} ℂ (F := E) (fun (z : ℂ) ↦ ∑' (n : ι), f n z) s
have refine_2 : ∀ (hc : DifferentiableOn ℂ g s), DifferentiableOn.{0, 0, u_2} ℂ (F := E) (fun (z : ℂ) ↦ ∑' (n : ι), f n z) s
Tactic: have hc := (hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn.mp hg).differentiableOn ?_ hs
-- Lean 4 proof step from Mathlib.Analysis.Complex.SummableUniformlyOn (goal)
Goal:
ι : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
f : ι → ℂ → E
s : Set ℂ
hs : IsOpen s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt ℂ (f n) r
g : ℂ → E
hg : HasSumLocallyUniformlyOn f g s
refine_2 : ∀ (hc : DifferentiableOn ℂ g s), DifferentiableOn.{0, 0, u_2} ℂ (F := E) (fun (z : ℂ) ↦ ∑' (n : ι), f n z) s
⊢ DifferentiableOn.{0, 0, u_2} ℂ (F := E) (fun (z : ℂ) ↦ ∑' (n : ι), f n z) s
have refine_1 : ∀ᶠ (n : Finset ι) in Filter.atTop, DifferentiableOn.{0, 0, u_2} ℂ (F := E) (fun (x2 : ℂ) ↦ ∑ i ∈ n, f i x2) s
Tactic: have hc := (hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn.mp hg).differentiableOn ?_ hs