awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Liouville (hypothesis)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hp : ∀ (z : ℂ) (hz : z ∈ sphere c R), ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
⊢ ‖iteratedDeriv n f c‖ ≤ (↑n.factorial : ℝ) * C / R ^ n
have hq : iteratedDeriv n f c =
  n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)
Tactic: have hq : iteratedDeriv n f c = n.factorial • (2 * π * I)⁻¹ •
    ∮ z in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z := by
    have : (2 * π * I / n.factorial) ≠ 0 := by simp [Nat.factorial_ne_zero]
    rw [← inv_smul_smul₀ this (iteratedDeriv n f c), inv_div, div_eq_inv_mul, mul_comm,
      ← nsmul_eq_mul, smul_assoc]
    simp [← DiffContOnCl.circleIntegral_one_div_sub_center_pow_smul hR n hf]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Liouville (goal)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hp : ∀ (z : ℂ) (hz : z ∈ sphere c R), ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
hq :
  iteratedDeriv n f c =
    n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)
⊢ ‖iteratedDeriv n f c‖ =
    ‖n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)‖
have rw : ‖n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)‖ =
  ‖n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)‖
Tactic: rw [hq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Liouville (goal)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hp : ∀ (z : ℂ) (hz : z ∈ sphere c R), ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
hq :
  iteratedDeriv n f c =
    n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)
⊢ ‖n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)‖ ≤
    (↑n.factorial : ℝ) * (R * (C / R ^ (n + 1)))
have rw : ‖HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)‖ ≤ R * (C / R ^ (n + 1))
Tactic: rw [RCLike.norm_nsmul (K := ℂ), nsmul_eq_mul, mul_le_mul_iff_right₀ (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Liouville (goal)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hp : ∀ (z : ℂ) (hz : z ∈ sphere c R), ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
hq :
  iteratedDeriv n f c =
    n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)
⊢ ‖iteratedDeriv n f c‖ ≤ (↑n.factorial : ℝ) * C / R ^ n
have n₁ : ‖iteratedDeriv n f c‖ =
  ‖n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)‖
Tactic: calc
    ‖iteratedDeriv n f c‖ = ‖n.factorial • (2 * π * I)⁻¹ •
      ∮ z in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z‖ := by rw [hq]
    _ ≤ n.factorial * (R * (C / (R ^ (n + 1)))) := by
      rw [RCLike.norm_nsmul (K := ℂ), nsmul_eq_mul, mul_le_mul_iff_right₀ (by positivity)]
      exact circleIntegral.norm_two_pi_i_inv_smul_integral_le_of_norm_le_const hR.le hp
    _ = n.factorial * C / R ^ n := by
      grind
-- Lean 4 proof step from Mathlib.Analysis.Complex.Liouville (goal)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hp : ∀ (z : ℂ) (hz : z ∈ sphere c R), ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
hq :
  iteratedDeriv n f c =
    n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)
n₁ :
  ‖iteratedDeriv n f c‖ =
    ‖n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)‖
⊢ ‖iteratedDeriv n f c‖ ≤ (↑n.factorial : ℝ) * C / R ^ n
have n₂ : ‖n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)‖ ≤
  (↑n.factorial : ℝ) * (R * (C / R ^ (n + 1)))
Tactic: calc
    ‖iteratedDeriv n f c‖ = ‖n.factorial • (2 * π * I)⁻¹ •
      ∮ z in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z‖ := by rw [hq]
    _ ≤ n.factorial * (R * (C / (R ^ (n + 1)))) := by
      rw [RCLike.norm_nsmul (K := ℂ), nsmul_eq_mul, mul_le_mul_iff_right₀ (by positivity)]
      exact circleIntegral.norm_two_pi_i_inv_smul_integral_le_of_norm_le_const hR.le hp
    _ = n.factorial * C / R ^ n := by
      grind
-- Lean 4 proof step from Mathlib.Analysis.Complex.Liouville (goal)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hp : ∀ (z : ℂ) (hz : z ∈ sphere c R), ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
hq :
  iteratedDeriv n f c =
    n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)
n₁ :
  ‖iteratedDeriv n f c‖ =
    ‖n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)‖
n₂ :
  ‖n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)‖ ≤
    (↑n.factorial : ℝ) * (R * (C / R ^ (n + 1)))
⊢ ‖iteratedDeriv n f c‖ ≤ (↑n.factorial : ℝ) * C / R ^ n
have n₃ : (↑n.factorial : ℝ) * (R * (C / R ^ (n + 1))) = (↑n.factorial : ℝ) * C / R ^ n
Tactic: calc
    ‖iteratedDeriv n f c‖ = ‖n.factorial • (2 * π * I)⁻¹ •
      ∮ z in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z‖ := by rw [hq]
    _ ≤ n.factorial * (R * (C / (R ^ (n + 1)))) := by
      rw [RCLike.norm_nsmul (K := ℂ), nsmul_eq_mul, mul_le_mul_iff_right₀ (by positivity)]
      exact circleIntegral.norm_two_pi_i_inv_smul_integral_le_of_norm_le_const hR.le hp
    _ = n.factorial * C / R ^ n := by
      grind
-- Lean 4 proof step from Mathlib.Analysis.Complex.Liouville (hypothesis)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
⊢ ‖deriv f c‖ ≤ C / R
have this : HasDerivAt (F := F̂) ((⇑e : (a : F) → F̂) ∘ f : ℂ → F̂) ((e : (a : F) → F̂) (deriv f c) : F̂) c
Tactic: have : HasDerivAt (e ∘ f) (e (deriv f c)) c :=
    e.hasFDerivAt.comp_hasDerivAt c
      (hd.differentiableAt isOpen_ball <| mem_ball_self hR).hasDerivAt
-- Lean 4 proof step from Mathlib.Analysis.Complex.Liouville (goal)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
this : HasDerivAt (F := F̂) ((⇑e : (a : F) → F̂) ∘ f : ℂ → F̂) ((e : (a : F) → F̂) (deriv f c) : F̂) c
⊢ ‖deriv f c‖ = norm (E := F̂) (deriv ((⇑e : (a : F) → F̂) ∘ f) c)
have rw : ‖deriv f c‖ = norm (E := F̂) ((e : (a : F) → F̂) (deriv f c) : F̂)
Tactic: rw [this.deriv]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Liouville (goal)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
this : HasDerivAt (F := F̂) ((⇑e : (a : F) → F̂) ∘ f : ℂ → F̂) ((e : (a : F) → F̂) (deriv f c) : F̂) c
⊢ ‖deriv f c‖ ≤ C / R
have f₁ : ‖deriv f c‖ = norm (E := F̂) (deriv ((⇑e : (a : F) → F̂) ∘ f) c)
Tactic: calc
    ‖deriv f c‖ = ‖deriv (e ∘ f) c‖ := by
      rw [this.deriv]
      exact (UniformSpace.Completion.norm_coe _).symm
    _ ≤ C / R :=
      norm_deriv_le_aux hR (e.differentiable.comp_diffContOnCl hd) fun z hz =>
        (UniformSpace.Completion.norm_coe _).trans_le (hC z hz)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Liouville (goal)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
z w : ℂ
⊢ f z = f w
have suffices : ∀ (c : ℂ), deriv f c = 0
Tactic: suffices ∀ c, deriv f c = 0 from is_const_of_deriv_eq_zero hf this z w
-- Lean 4 proof step from Mathlib.Analysis.Complex.Liouville (goal)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
c : ℂ
⊢ ∃ C > 0, ∀ (z : ℂ), ‖f z‖ ≤ C
have rcases : ∀ (C : ℝ) (hC : ∀ x ∈ range f, ‖x‖ ≤ C), ∃ C > 0, ∀ (z : ℂ), ‖f z‖ ≤ C
Tactic: rcases isBounded_iff_forall_norm_le.1 hb with ⟨C, hC⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.Liouville (goal)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
c : ℂ
⊢ deriv f c = 0
have obtain : ∀ (C : ℝ) (C₀ : C > 0) (hC : ∀ (z : ℂ), ‖f z‖ ≤ C), deriv f c = 0
Tactic: obtain ⟨C, C₀, hC⟩ : ∃ C > (0 : ℝ), ∀ z, ‖f z‖ ≤ C := by
    rcases isBounded_iff_forall_norm_le.1 hb with ⟨C, hC⟩
    exact
      ⟨max C 1, lt_max_iff.2 (Or.inr zero_lt_one), fun z =>
        (hC (f z) (mem_range_self _)).trans (le_max_left _ _)⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.Liouville (goal)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
c : ℂ
C : ℝ
C₀ : C > 0
hC : ∀ (z : ℂ), ‖f z‖ ≤ C
⊢ deriv f c = 0
have refine : ∀ (ε : ℝ) (ε₀ : 0 < ε), ‖deriv f c‖ ≤ ε
Tactic: refine norm_le_zero_iff.1 (le_of_forall_gt_imp_ge_of_dense fun ε ε₀ => ?_)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Liouville (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
z w : E
g : ℂ → F := f ∘ fun (t : ℂ) ↦ t • (w - z) + z
⊢ f z = f w
have suffices : g 0 = g 1
Tactic: suffices g 0 = g 1 by simpa [g]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Liouville (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
z w : E
g : ℂ → F := f ∘ fun (t : ℂ) ↦ t • (w - z) + z
⊢ g 0 = g 1
have hf₁ : Differentiable ℂ g
Tactic: apply liouville_theorem_aux
-- Lean 4 proof step from Mathlib.Analysis.Complex.Liouville (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
f : E → F
hf : Differentiable ℂ f
hb : Bornology.IsBounded (range f)
z w : E
g : ℂ → F := f ∘ fun (t : ℂ) ↦ t • (w - z) + z
hf₁ : Differentiable ℂ g
⊢ g 0 = g 1
have hb₁ : Bornology.IsBounded (range g)
Tactic: apply liouville_theorem_aux
-- Lean 4 proof step from Mathlib.Analysis.Complex.Liouville (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
inst_4 : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
⊢ Bornology.IsBounded (range f)
have obtain : ∀ (s : Set E) (hs : s ∈ cocompact E) (hs_bdd : Bornology.IsBounded (f '' s)), Bornology.IsBounded (range f)
Tactic: obtain ⟨s, hs, hs_bdd⟩ := Metric.exists_isBounded_image_of_tendsto hb
-- Lean 4 proof step from Mathlib.Analysis.Complex.Liouville (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
inst_4 : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
s : Set E
hs : s ∈ cocompact E
hs_bdd : Bornology.IsBounded (f '' s)
⊢ Bornology.IsBounded (range f)
have obtain : ∀ (t : Set E) (ht : IsCompact t) (hts : tᶜ ⊆ s), Bornology.IsBounded (range f)
Tactic: obtain ⟨t, ht, hts⟩ := mem_cocompact.mp hs
-- Lean 4 proof step from Mathlib.Analysis.Complex.Liouville (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
inst_4 : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
s : Set E
hs : s ∈ cocompact E
hs_bdd : Bornology.IsBounded (f '' s)
t : Set E
ht : IsCompact t
hts : tᶜ ⊆ s
⊢ Bornology.IsBounded (range f)
have apply : range f ⊆ f '' t ∪ f '' s
Tactic: apply ht.image hf.continuous |>.isBounded.union hs_bdd |>.subset
-- Lean 4 proof step from Mathlib.Analysis.Complex.Liouville (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
inst_4 : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
⊢ f = const E c
have h_bdd : Bornology.IsBounded (range f)
Tactic: have h_bdd : Bornology.IsBounded (Set.range f) := by
    obtain ⟨s, hs, hs_bdd⟩ := Metric.exists_isBounded_image_of_tendsto hb
    obtain ⟨t, ht, hts⟩ := mem_cocompact.mp hs
    apply ht.image hf.continuous |>.isBounded.union hs_bdd |>.subset
    simpa [Set.image_union, Set.image_univ] using Set.image_mono <| calc
      Set.univ = t ∪ tᶜ := t.union_compl_self.symm
      _        ⊆ t ∪ s  := by gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Liouville (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
inst_4 : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
h_bdd : Bornology.IsBounded (range f)
⊢ f = const E c
have obtain : ∀ (c' : F) (hc' : f = const E c'), f = const E c
Tactic: obtain ⟨c', hc'⟩ := hf.exists_eq_const_of_bounded h_bdd
-- Lean 4 proof step from Mathlib.Analysis.Complex.Liouville (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
F : Type v
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℂ F
inst_4 : Nontrivial E
f : E → F
hf : Differentiable ℂ f
c : F
hb : Tendsto f (cocompact E) (𝓝 c)
h_bdd : Bornology.IsBounded (range f)
c' : F
hc' : f = const E c'
⊢ f = const E c
have h : c = c'
Tactic: convert! hc'
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M
⊢ 0 ≤ M
have obtain : ∀ (w : ℂ) (hw : w ∈ sphere z r), 0 ≤ M
Tactic: obtain ⟨w, hw⟩ : (sphere z r).Nonempty := NormedSpace.sphere_nonempty.mpr hr.le
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M
⊢ ‖cderiv r f z‖ ≤ M / r
have hM : 0 ≤ M
Tactic: have hM : 0 ≤ M := by
    obtain ⟨w, hw⟩ : (sphere z r).Nonempty := NormedSpace.sphere_nonempty.mpr hr.le
    exact (norm_nonneg _).trans (hf w hw)
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M
hM : 0 ≤ M
w : ℂ
hw : w ∈ sphere z r
⊢ ‖(HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • f w‖ ≤ M / HPow.hPow (β := ℕ) r 2
have hw₁ : ‖w - z‖ = r
Tactic: simp only [mem_sphere_iff_norm] at hw hf
Cleared hypotheses: hf, hw
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M
hM : 0 ≤ M
w : ℂ
hw : w ∈ sphere z r
hw₁ : ‖w - z‖ = r
⊢ ‖(HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • f w‖ ≤ M / HPow.hPow (β := ℕ) r 2
have hf₁ : ∀ (w : ℂ), ‖w - z‖ = r → ‖f w‖ ≤ M
Tactic: simp only [mem_sphere_iff_norm] at hw hf
Cleared hypotheses: hf, hw
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hM : 0 ≤ M
w : ℂ
hw : ‖w - z‖ = r
hf : ∀ (w : ℂ), ‖w - z‖ = r → ‖f w‖ ≤ M
⊢ ‖(HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • f w‖ ≤ M / HPow.hPow (β := ℕ) r 2
have simp : ‖f w‖ / HPow.hPow (β := ℕ) r 2 ≤ M / HPow.hPow (β := ℕ) r 2
Tactic: simp only [norm_smul, inv_mul_eq_div, hw, norm_inv, norm_pow]
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M
hM : 0 ≤ M
⊢ ‖cderiv r f z‖ ≤ M / r
have h1 : ∀ w ∈ sphere z r, ‖(HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • f w‖ ≤ M / HPow.hPow (β := ℕ) r 2
Tactic: have h1 : ∀ w ∈ sphere z r, ‖((w - z) ^ 2)⁻¹ • f w‖ ≤ M / r ^ 2 := by
    intro w hw
    simp only [mem_sphere_iff_norm] at hw hf
    simp only [norm_smul, inv_mul_eq_div, hw, norm_inv, norm_pow]
    exact div_le_div₀ hM (hf w hw) (sq_pos_of_pos hr) le_rfl
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M
hM : 0 ≤ M
h1 : ∀ w ∈ sphere z r, ‖(HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • f w‖ ≤ M / HPow.hPow (β := ℕ) r 2
⊢ ‖cderiv r f z‖ ≤ M / r
have h2 : norm.{u_1} (E := E) (∮ (z_1 : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (z_1 - z) 2)⁻¹ • f z_1) ≤
  2 * π * r * (M / HPow.hPow (β := ℕ) r 2)
Tactic: have h2 := circleIntegral.norm_integral_le_of_norm_le_const hr.le h1
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M
hM : 0 ≤ M
h1 : ∀ w ∈ sphere z r, ‖(HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • f w‖ ≤ M / HPow.hPow (β := ℕ) r 2
h2 :
  norm.{u_1} (E := E) (∮ (z_1 : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (z_1 - z) 2)⁻¹ • f z_1) ≤
    2 * π * r * (M / HPow.hPow (β := ℕ) r 2)
⊢ ‖cderiv r f z‖ ≤ M / r
have simp : ‖(2 * (↑π : ℂ) * I)⁻¹‖ * norm.{u_1} (E := E) (∮ (w : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • f w) ≤ M / r
Tactic: simp only [cderiv, norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M
hM : 0 ≤ M
h1 : ∀ w ∈ sphere z r, ‖(HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • f w‖ ≤ M / HPow.hPow (β := ℕ) r 2
h2 :
  norm.{u_1} (E := E) (∮ (z_1 : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (z_1 - z) 2)⁻¹ • f z_1) ≤
    2 * π * r * (M / HPow.hPow (β := ℕ) r 2)
⊢ ‖(2 * (↑π : ℂ) * I)⁻¹‖ * norm.{u_1} (E := E) (∮ (w : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • f w) ≤ M / r
have refine : ‖(2 * (↑π : ℂ) * I)⁻¹‖ * (2 * π * r * (M / HPow.hPow (β := ℕ) r 2)) = M / r
Tactic: refine (mul_le_mul le_rfl h2 (norm_nonneg _) (norm_nonneg _)).trans (le_of_eq ?_)
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
r : ℝ
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
⊢ ContinuousOn (Y := ℂ) (fun (w : ℂ) ↦ (HPow.hPow (β := ℕ) (w - z) 2)⁻¹) (sphere z r)
have refine : ∀ (w : ℂ) (hw : w ∈ sphere z r) (h : HPow.hPow (β := ℕ) (w - z) 2 = 0), 0 = r
Tactic: refine ((continuous_id'.sub continuous_const).pow 2).continuousOn.inv₀ fun w hw h => hr.ne ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
r : ℝ
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
w : ℂ
hw : w ∈ sphere z r
h : HPow.hPow (β := ℕ) (w - z) 2 = 0
⊢ 0 = r
have rwa : ∀ (hw : ‖w - z‖ = r) (h : HPow.hPow (β := ℕ) (w - z) 2 = 0), 0 = r
Tactic: rwa [mem_sphere_iff_norm, sq_eq_zero_iff.mp h, norm_zero] at hw
Cleared hypotheses: hw, h
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
r : ℝ
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
w : ℂ
hw : w ∈ sphere z r
h : HPow.hPow (β := ℕ) (w - z) 2 = 0
rwa : ∀ (hw : ‖w - z‖ = r) (h : HPow.hPow (β := ℕ) (w - z) 2 = 0), 0 = r
⊢ 0 = r
have rwa₁ : ∀ (hw : norm (E := ℂ) 0 = r) (h : HPow.hPow (β := ℕ) (w - z) 2 = 0), 0 = r
Tactic: rwa [mem_sphere_iff_norm, sq_eq_zero_iff.mp h, norm_zero] at hw
Cleared hypotheses: hw, h
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
r : ℝ
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
w : ℂ
hw : w ∈ sphere z r
h : HPow.hPow (β := ℕ) (w - z) 2 = 0
rwa : ∀ (hw : ‖w - z‖ = r) (h : HPow.hPow (β := ℕ) (w - z) 2 = 0), 0 = r
rwa₁ : ∀ (hw : norm (E := ℂ) 0 = r) (h : HPow.hPow (β := ℕ) (w - z) 2 = 0), 0 = r
⊢ 0 = r
have rwa₂ : ∀ (hw : 0 = r) (h : HPow.hPow (β := ℕ) (w - z) 2 = 0), 0 = r
Tactic: rwa [mem_sphere_iff_norm, sq_eq_zero_iff.mp h, norm_zero] at hw
Cleared hypotheses: hw, h
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
r : ℝ
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
⊢ cderiv r (f - g) z = cderiv r f z - cderiv r g z
have h1 : ContinuousOn (Y := ℂ) (fun (w : ℂ) ↦ (HPow.hPow (β := ℕ) (w - z) 2)⁻¹) (sphere z r)
Tactic: have h1 : ContinuousOn (fun w : ℂ => ((w - z) ^ 2)⁻¹) (sphere z r) := by
    refine ((continuous_id'.sub continuous_const).pow 2).continuousOn.inv₀ fun w hw h => hr.ne ?_
    rwa [mem_sphere_iff_norm, sq_eq_zero_iff.mp h, norm_zero] at hw
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
r : ℝ
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
h1 : ContinuousOn (Y := ℂ) (fun (w : ℂ) ↦ (HPow.hPow (β := ℕ) (w - z) 2)⁻¹) (sphere z r)
⊢ cderiv r (f - g) z = cderiv r f z - cderiv r g z
have simp_rw : HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (w : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • (f - g) w) =
  (2 * (↑π : ℂ) * I)⁻¹ •
    HSub.hSub (α := E) (∮ (w : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • f w)
      (∮ (w : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • g w)
Tactic: simp_rw [cderiv, ← smul_sub]
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
r : ℝ
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
h1 : ContinuousOn (Y := ℂ) (fun (w : ℂ) ↦ (HPow.hPow (β := ℕ) (w - z) 2)⁻¹) (sphere z r)
⊢ HSMul.hSMul (β := E) (2 * (↑π : ℂ) * I)⁻¹ (∮ (w : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • (f - g) w) =
    (2 * (↑π : ℂ) * I)⁻¹ •
      HSub.hSub (α := E) (∮ (w : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • f w)
        (∮ (w : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • g w)
have e_a : ∮ (w : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • (f - g) w =
  HSub.hSub (α := E) (∮ (w : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • f w)
    (∮ (w : ℂ) in C(z, r), (HPow.hPow (β := ℕ) (w - z) 2)⁻¹ • g w)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.LocallyUniformLimit (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
M r : ℝ
f : ℂ → E
hr : 0 < r
hfM : ∀ w ∈ sphere z r, ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
⊢ ∃ L < M, ∀ w ∈ sphere z r, ‖f w‖ ≤ L
have e1 : (sphere z r).Nonempty
Tactic: have e1 : (sphere z r).Nonempty := NormedSpace.sphere_nonempty.mpr hr.le