awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
g : (z : ℂ) → ℂ := fun (z : ℂ) ↦ ∑' (n : ℕ), f n * z ^ n
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖
z : ℂ
zn : ‖z‖ < 1
zm : ‖1 - z‖ < M * (1 - ‖z‖)
zd : ‖z - 1‖ < ε / 4 / (F + 1)
B₂ : ℕ
hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
S₁ : ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
S₂ : ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
linarith : ε / 2 < ε / 4 + ε / 4 → 2 / 2 = 1
linarith₁ : ε / 2 < ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 2 2 = 4
linarith₂ : ε / 2 < ε / 4 + ε / 4 → 4 / 4 = 1
linarith₃ : ε / 2 < ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₄ : ε / 2 < ε / 4 + ε / 4 → 4 / 4 = 1
linarith₅ : ε / 2 < ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₆ : ε / 2 < ε / 4 + ε / 4 → GT.gt (α := ℝ) 4 0
linarith₇ : ε / 2 < ε / 4 + ε / 4 → 2 * ε - (1 * ε + 1 * ε) = 0
linarith₈ : ε / 4 + ε / 4 < ε / 2 → 4 / 4 = 1
linarith₉ : ε / 4 + ε / 4 < ε / 2 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₁₀ : ε / 4 + ε / 4 < ε / 2 → 4 / 4 = 1
linarith₁₁ : ε / 4 + ε / 4 < ε / 2 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₁₂ : ε / 4 + ε / 4 < ε / 2 → 2 / 2 = 1
⊢ ε / 2 = ε / 4 + ε / 4
have linarith₁₃ : ε / 4 + ε / 4 < ε / 2 → HMul.hMul (α := ℝ) 2 2 = 4
Tactic: linarith only
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
g : (z : ℂ) → ℂ := fun (z : ℂ) ↦ ∑' (n : ℕ), f n * z ^ n
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖
z : ℂ
zn : ‖z‖ < 1
zm : ‖1 - z‖ < M * (1 - ‖z‖)
zd : ‖z - 1‖ < ε / 4 / (F + 1)
B₂ : ℕ
hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
S₁ : ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
S₂ : ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
linarith : ε / 2 < ε / 4 + ε / 4 → 2 / 2 = 1
linarith₁ : ε / 2 < ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 2 2 = 4
linarith₂ : ε / 2 < ε / 4 + ε / 4 → 4 / 4 = 1
linarith₃ : ε / 2 < ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₄ : ε / 2 < ε / 4 + ε / 4 → 4 / 4 = 1
linarith₅ : ε / 2 < ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₆ : ε / 2 < ε / 4 + ε / 4 → GT.gt (α := ℝ) 4 0
linarith₇ : ε / 2 < ε / 4 + ε / 4 → 2 * ε - (1 * ε + 1 * ε) = 0
linarith₈ : ε / 4 + ε / 4 < ε / 2 → 4 / 4 = 1
linarith₉ : ε / 4 + ε / 4 < ε / 2 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₁₀ : ε / 4 + ε / 4 < ε / 2 → 4 / 4 = 1
linarith₁₁ : ε / 4 + ε / 4 < ε / 2 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₁₂ : ε / 4 + ε / 4 < ε / 2 → 2 / 2 = 1
linarith₁₃ : ε / 4 + ε / 4 < ε / 2 → HMul.hMul (α := ℝ) 2 2 = 4
⊢ ε / 2 = ε / 4 + ε / 4
have linarith₁₄ : ε / 4 + ε / 4 < ε / 2 → GT.gt (α := ℝ) 4 0
Tactic: linarith only
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
M : ℝ
hM : 1 < M
s : (n : ℕ) → ℂ := fun (n : ℕ) ↦ ∑ i ∈ range n, f i
g : (z : ℂ) → ℂ := fun (z : ℂ) ↦ ∑' (n : ℕ), f n * z ^ n
ε : ℝ
εpos : ε > 0
B₁ : ℕ
hB₁ : ∀ n ≥ B₁, ‖∑ i ∈ range n, f i - l‖ < ε / 4 / M
F : ℝ := ∑ i ∈ range B₁, ‖l - s (i + 1)‖
z : ℂ
zn : ‖z‖ < 1
zm : ‖1 - z‖ < M * (1 - ‖z‖)
zd : ‖z - 1‖ < ε / 4 / (F + 1)
B₂ : ℕ
hB₂ : ‖l - ∑' (n : ℕ), f n * z ^ n - (1 - z) * ∑ i ∈ range (max B₁ B₂), (l - ∑ j ∈ range (i + 1), f j) * z ^ i‖ < ε / 2
S₁ : ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
S₂ : ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4
linarith : ε / 2 < ε / 4 + ε / 4 → 2 / 2 = 1
linarith₁ : ε / 2 < ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 2 2 = 4
linarith₂ : ε / 2 < ε / 4 + ε / 4 → 4 / 4 = 1
linarith₃ : ε / 2 < ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₄ : ε / 2 < ε / 4 + ε / 4 → 4 / 4 = 1
linarith₅ : ε / 2 < ε / 4 + ε / 4 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₆ : ε / 2 < ε / 4 + ε / 4 → GT.gt (α := ℝ) 4 0
linarith₇ : ε / 2 < ε / 4 + ε / 4 → 2 * ε - (1 * ε + 1 * ε) = 0
linarith₈ : ε / 4 + ε / 4 < ε / 2 → 4 / 4 = 1
linarith₉ : ε / 4 + ε / 4 < ε / 2 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₁₀ : ε / 4 + ε / 4 < ε / 2 → 4 / 4 = 1
linarith₁₁ : ε / 4 + ε / 4 < ε / 2 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₁₂ : ε / 4 + ε / 4 < ε / 2 → 2 / 2 = 1
linarith₁₃ : ε / 4 + ε / 4 < ε / 2 → HMul.hMul (α := ℝ) 2 2 = 4
linarith₁₄ : ε / 4 + ε / 4 < ε / 2 → GT.gt (α := ℝ) 4 0
⊢ ε / 2 = ε / 4 + ε / 4
have linarith₁₅ : ε / 4 + ε / 4 < ε / 2 → 1 * ε + 1 * ε - 2 * ε = 0
Tactic: linarith only
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (hypothesis)
Goal:
f : ℕ → ℝ
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
⊢ Tendsto (fun (x : ℝ) ↦ ∑' (n : ℕ), f n * x ^ n) (𝓝[<] 1) (𝓝 l)
have m : Filter.map ofReal (𝓝 l) ≤ 𝓝 (↑l : ℂ)
Tactic: have m : (𝓝 l).map ofReal ≤ 𝓝 ↑l := ofRealCLM.continuous.tendsto l
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (hypothesis)
Goal:
f : ℕ → ℝ
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
m : Filter.map ofReal (𝓝 l) ≤ 𝓝 (↑l : ℂ)
⊢ Tendsto (fun (x : ℝ) ↦ ∑' (n : ℕ), f n * x ^ n) (𝓝[<] 1) (𝓝 l)
have h₁ : Tendsto (α := ℕ) (ofReal ∘ fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 (↑l : ℂ))
Tactic: replace h := (tendsto_map.comp h).mono_right m
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (hypothesis)
Goal:
f : ℕ → ℝ
l : ℝ
m : Filter.map ofReal (𝓝 l) ≤ 𝓝 (↑l : ℂ)
h : Tendsto (α := ℕ) (ofReal ∘ fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 (↑l : ℂ))
⊢ Tendsto (fun (x : ℝ) ↦ ∑' (n : ℕ), f n * x ^ n) (𝓝[<] 1) (𝓝 l)
have h₁ : Tendsto (fun (x : ℕ) ↦ (↑(∑ i ∈ range x, f i) : ℂ)) atTop (𝓝 (↑l : ℂ))
Tactic: rw [Function.comp_def] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (hypothesis)
Goal:
f : ℕ → ℝ
l : ℝ
m : Filter.map ofReal (𝓝 l) ≤ 𝓝 (↑l : ℂ)
h : Tendsto (fun (x : ℕ) ↦ (↑(∑ i ∈ range x, f i) : ℂ)) atTop (𝓝 (↑l : ℂ))
⊢ Tendsto (fun (x : ℝ) ↦ ∑' (n : ℕ), f n * x ^ n) (𝓝[<] 1) (𝓝 l)
have h₁ : Tendsto (fun (x : ℕ) ↦ ∑ i ∈ range x, (↑(f i) : ℂ)) atTop (𝓝 (↑l : ℂ))
Tactic: push_cast at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (hypothesis)
Goal:
f : ℕ → ℝ
l : ℝ
m : Filter.map ofReal (𝓝 l) ≤ 𝓝 (↑l : ℂ)
h : Tendsto (fun (x : ℕ) ↦ ∑ i ∈ range x, (↑(f i) : ℂ)) atTop (𝓝 (↑l : ℂ))
⊢ Tendsto (fun (x : ℝ) ↦ ∑' (n : ℕ), f n * x ^ n) (𝓝[<] 1) (𝓝 l)
have h₁ : Tendsto (fun (z : ℂ) ↦ ∑' (n : ℕ), (↑(f n) : ℂ) * z ^ n) (Filter.map ofReal (𝓝[<] 1)) (𝓝 (↑l : ℂ))
Tactic: replace h := Complex.tendsto_tsum_powerSeries_nhdsWithin_lt h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (hypothesis)
Goal:
f : ℕ → ℝ
l : ℝ
m : Filter.map ofReal (𝓝 l) ≤ 𝓝 (↑l : ℂ)
h : Tendsto (fun (z : ℂ) ↦ ∑' (n : ℕ), (↑(f n) : ℂ) * z ^ n) (Filter.map ofReal (𝓝[<] 1)) (𝓝 (↑l : ℂ))
⊢ Tendsto (fun (x : ℝ) ↦ ∑' (n : ℕ), f n * x ^ n) (𝓝[<] 1) (𝓝 l)
have h₁ : Tendsto ((fun (z : ℂ) ↦ ∑' (n : ℕ), (↑(f n) : ℂ) * z ^ n) ∘ ofReal) (𝓝[<] 1) (𝓝 (↑l : ℂ))
Tactic: rw [tendsto_map'_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
f : ℕ → ℝ
l : ℝ
m : Filter.map ofReal (𝓝 l) ≤ 𝓝 (↑l : ℂ)
h : Tendsto ((fun (z : ℂ) ↦ ∑' (n : ℕ), (↑(f n) : ℂ) * z ^ n) ∘ ofReal) (𝓝[<] 1) (𝓝 (↑l : ℂ))
⊢ Tendsto (fun (x : ℝ) ↦ ∑' (n : ℕ), f n * x ^ n) (𝓝[<] 1) (𝓝 l)
have rw : ∀
  (h :
    ∀ ε > 0,
      ∃ δ > 0,
        ∀ ⦃x : ℝ⦄,
          Membership.mem (γ := Set ℝ) (Set.Iio 1) x →
            dist x 1 < δ → dist (((fun (z : ℂ) ↦ ∑' (n : ℕ), (↑(f n) : ℂ) * z ^ n) ∘ ofReal) x) (↑l : ℂ) < ε),
  ∀ ε > 0,
    ∃ δ > 0, ∀ ⦃x : ℝ⦄, Membership.mem (γ := Set ℝ) (Set.Iio 1) x → dist x 1 < δ → dist (∑' (n : ℕ), f n * x ^ n) l < ε
Tactic: rw [Metric.tendsto_nhdsWithin_nhds] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
f : ℕ → ℝ
l : ℝ
m : Filter.map ofReal (𝓝 l) ≤ 𝓝 (↑l : ℂ)
h :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ ⦃x : ℝ⦄,
        Membership.mem (γ := Set ℝ) (Set.Iio 1) x →
          dist x 1 < δ → dist (((fun (z : ℂ) ↦ ∑' (n : ℕ), (↑(f n) : ℂ) * z ^ n) ∘ ofReal) x) (↑l : ℂ) < ε
⊢ ∀ ε > 0,
    ∃ δ > 0, ∀ ⦃x : ℝ⦄, Membership.mem (γ := Set ℝ) (Set.Iio 1) x → dist x 1 < δ → dist (∑' (n : ℕ), f n * x ^ n) l < ε
have h₁ : ∀ a > 0,
  ∀ (x a : ℝ),
    Membership.mem (γ := Set ℝ) (Set.Iio 1) a →
      dist a 1 < x →
        dist (∑' (n : ℕ), f n * a ^ n) l = dist (((fun (z : ℂ) ↦ ∑' (n : ℕ), (↑(f n) : ℂ) * z ^ n) ∘ ofReal) a) (↑l : ℂ)
Tactic: convert! h
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
f : ℕ → ℝ
l : ℝ
m : Filter.map ofReal (𝓝 l) ≤ 𝓝 (↑l : ℂ)
h :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ ⦃x : ℝ⦄,
        Membership.mem (γ := Set ℝ) (Set.Iio 1) x →
          dist x 1 < δ → dist (((fun (z : ℂ) ↦ ∑' (n : ℕ), (↑(f n) : ℂ) * z ^ n) ∘ ofReal) x) (↑l : ℂ) < ε
a : ℝ
h_1 : a > 0
x a_1 : ℝ
h_2 : Membership.mem (γ := Set ℝ) (Set.Iio 1) a_1
h_3 : dist a_1 1 < x
⊢ dist (∑' (n : ℕ), f n * a_1 ^ n) l = dist (((fun (z : ℂ) ↦ ∑' (n : ℕ), (↑(f n) : ℂ) * z ^ n) ∘ ofReal) a_1) (↑l : ℂ)
have h₁ : ‖∑' (n : ℕ), f n * a_1 ^ n - l‖ = ‖∑' (n : ℕ), (↑(f n) : ℂ) * (↑a_1 : ℂ) ^ n - (↑l : ℂ)‖
Tactic: simp_rw [Function.comp_apply, dist_eq_norm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbelLimit (goal)
Goal:
f : ℕ → ℝ
l : ℝ
m : Filter.map ofReal (𝓝 l) ≤ 𝓝 (↑l : ℂ)
h :
  ∀ ε > 0,
    ∃ δ > 0,
      ∀ ⦃x : ℝ⦄,
        Membership.mem (γ := Set ℝ) (Set.Iio 1) x →
          dist x 1 < δ → dist (((fun (z : ℂ) ↦ ∑' (n : ℕ), (↑(f n) : ℂ) * z ^ n) ∘ ofReal) x) (↑l : ℂ) < ε
a : ℝ
h_1 : a > 0
x a_1 : ℝ
h_2 : Membership.mem (γ := Set ℝ) (Set.Iio 1) a_1
h_3 : dist a_1 1 < x
⊢ ‖∑' (n : ℕ), f n * a_1 ^ n - l‖ = ‖∑' (n : ℕ), (↑(f n) : ℂ) * (↑a_1 : ℂ) ^ n - (↑l : ℂ)‖
have h₁ : ‖∑' (n : ℕ), f n * a_1 ^ n - l‖ = ‖∑' (n : ℕ), f n * a_1 ^ n - l‖
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
⊢ ‖f w‖ = ‖f z‖
have hw : w ∈ closedBall z r
Tactic: have hw : w ∈ closedBall z r := mem_closedBall.2 le_rfl
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
⊢ ‖f w‖ = ‖f z‖
have refine : ¬(norm ∘ f) w < (norm ∘ f) z
Tactic: refine (isMaxOn_iff.1 hz _ hw).antisymm (not_lt.1 ?_)
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
⊢ False
have hr : 0 < r
Tactic: have hr : 0 < r := dist_pos.2 (ne_of_apply_ne (norm ∘ f) hw_lt.ne)
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
this : norm.{v} (E := F) (∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ) < 2 * π * ‖f z‖
⊢ False
have refine : norm.{v} (E := F) (∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ) = 2 * π * ‖f z‖
Tactic: refine this.ne ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
this : norm.{v} (E := F) (∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ) < 2 * π * ‖f z‖
⊢ norm.{v} (E := F) (∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ) = 2 * π * ‖f z‖
have A : ∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ = (2 * (↑π : ℂ) * I) • f z
Tactic: have A : (∮ ζ in C(z, r), (ζ - z)⁻¹ • f ζ) = (2 * π * I : ℂ) • f z :=
      hd.circleIntegral_sub_inv_smul (mem_ball_self hr)
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
⊢ False
have suffices : norm.{v} (E := F) (∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ) < 2 * π * ‖f z‖
Tactic: suffices ‖∮ ζ in C(z, r), (ζ - z)⁻¹ • f ζ‖ < 2 * π * ‖f z‖ by
    refine this.ne ?_
    have A : (∮ ζ in C(z, r), (ζ - z)⁻¹ • f ζ) = (2 * π * I : ℂ) • f z :=
      hd.circleIntegral_sub_inv_smul (mem_ball_self hr)
    simp [A, norm_smul, Real.pi_pos.le]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
this : norm.{v} (E := F) (∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ) < 2 * π * r * (‖f z‖ / r)
⊢ norm.{v} (E := F) (∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ) < 2 * π * ‖f z‖
have rwa : ∀ (this : norm.{v} (E := F) (∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ) < 2 * π * (r * (‖f z‖ / r))),
  norm.{v} (E := F) (∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ) < 2 * π * ‖f z‖
Tactic: rwa [mul_assoc, mul_div_cancel₀ _ hr.ne'] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
this : norm.{v} (E := F) (∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ) < 2 * π * r * (‖f z‖ / r)
rwa :
  ∀ (this : norm.{v} (E := F) (∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ) < 2 * π * (r * (‖f z‖ / r))),
    norm.{v} (E := F) (∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ) < 2 * π * ‖f z‖
⊢ norm.{v} (E := F) (∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ) < 2 * π * ‖f z‖
have rwa₁ : ∀ (this : norm.{v} (E := F) (∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ) < 2 * π * ‖f z‖),
  norm.{v} (E := F) (∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ) < 2 * π * ‖f z‖
Tactic: rwa [mul_assoc, mul_div_cancel₀ _ hr.ne'] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
⊢ norm.{v} (E := F) (∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ) < 2 * π * ‖f z‖
have suffices : norm.{v} (E := F) (∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ) < 2 * π * r * (‖f z‖ / r)
Tactic: suffices ‖∮ ζ in C(z, r), (ζ - z)⁻¹ • f ζ‖ < 2 * π * r * (‖f z‖ / r) by
    rwa [mul_assoc, mul_div_cancel₀ _ hr.ne'] at this
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
⊢ norm.{v} (E := F) (∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ) < 2 * π * r * (‖f z‖ / r)
have hsub : sphere z r ⊆ closedBall z r
Tactic: have hsub : sphere z r ⊆ closedBall z r := sphere_subset_closedBall
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
hsub : sphere z r ⊆ closedBall z r
⊢ norm.{v} (E := F) (∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ) < 2 * π * r * (‖f z‖ / r)
have refine_1 : ContinuousOn.{0, v} (Y := F) (fun (ζ : ℂ) ↦ (ζ - z)⁻¹ • f ζ) (sphere z r)
Tactic: refine circleIntegral.norm_integral_lt_of_norm_le_const_of_lt hr ?_ ?_ ⟨w, rfl, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
hsub : sphere z r ⊆ closedBall z r
refine_1 : ContinuousOn.{0, v} (Y := F) (fun (ζ : ℂ) ↦ (ζ - z)⁻¹ • f ζ) (sphere z r)
⊢ norm.{v} (E := F) (∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ) < 2 * π * r * (‖f z‖ / r)
have refine_2 : ∀ z_1 ∈ sphere z r, ‖(z_1 - z)⁻¹ • f z_1‖ ≤ ‖f z‖ / r
Tactic: refine circleIntegral.norm_integral_lt_of_norm_le_const_of_lt hr ?_ ?_ ⟨w, rfl, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
hsub : sphere z r ⊆ closedBall z r
refine_1 : ContinuousOn.{0, v} (Y := F) (fun (ζ : ℂ) ↦ (ζ - z)⁻¹ • f ζ) (sphere z r)
refine_2 : ∀ z_1 ∈ sphere z r, ‖(z_1 - z)⁻¹ • f z_1‖ ≤ ‖f z‖ / r
⊢ norm.{v} (E := F) (∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ) < 2 * π * r * (‖f z‖ / r)
have refine_3 : ‖(w - z)⁻¹ • f w‖ < ‖f z‖ / r
Tactic: refine circleIntegral.norm_integral_lt_of_norm_le_const_of_lt hr ?_ ?_ ⟨w, rfl, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
hsub : sphere z r ⊆ closedBall z r
⊢ ContinuousOn.{0, v} (Y := F) (fun (ζ : ℂ) ↦ (ζ - z)⁻¹ • f ζ) (sphere z r)
have refine_1 : ∀ x ∈ sphere z r, _root_.id x - z ≠ 0
Tactic: refine ((continuousOn_id.sub continuousOn_const).inv₀ ?_).smul (hd.continuousOn_ball.mono hsub)
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
hsub : sphere z r ⊆ closedBall z r
ζ : ℂ
hζ : ζ ∈ sphere z r
⊢ ‖(ζ - z)⁻¹ • f ζ‖ ≤ ‖f z‖ / r
have refine_2 : ‖f ζ‖ ≤ ‖f z‖
Tactic: rw [le_div_iff₀ hr, norm_smul, norm_inv, mem_sphere_iff_norm.1 hζ, mul_comm,
      mul_inv_cancel_left₀ hr.ne']
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
f : ℂ → F
z w : ℂ
r : ℝ := dist w z
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (closedBall z r) z
hw : w ∈ closedBall z r
hw_lt : ‖f w‖ < ‖f z‖
hr : 0 < r
hsub : sphere z r ⊆ closedBall z r
⊢ ‖(w - z)⁻¹ • f w‖ < ‖f z‖ / r
have refine_3 : ‖f w‖ / dist w z < ‖f z‖ / r
Tactic: rw [norm_smul, norm_inv, ← div_eq_inv_mul, ← dist_eq_norm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (closedBall z (dist w z)) z
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
⊢ ‖f w‖ = ‖f z‖
have he : ∀ (x : F), norm (E := F̂) ((e : (a : F) → F̂) x : F̂) = ‖x‖
Tactic: have he : ∀ x, ‖e x‖ = ‖x‖ := UniformSpace.Completion.norm_coe
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (closedBall z (dist w z)) z
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
he : ∀ (x : F), norm (E := F̂) ((e : (a : F) → F̂) x : F̂) = ‖x‖
⊢ ‖f w‖ = ‖f z‖
have hz₁ : IsMaxOn (Function.comp (β := F̂) norm ((⇑e : (a : F) → F̂) ∘ f)) (closedBall z (dist w z)) z
Tactic: replace hz : IsMaxOn (norm ∘ e ∘ f) (closedBall z (dist w z)) z := by
    simpa only [IsMaxOn, Function.comp_def, he] using hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
r : ℝ
hr : dist w z = r
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
⊢ ‖f w‖ = ‖f z‖
have hd₁ : DiffContOnCl ℂ f (ball z (dist w z))
Tactic: subst r
Cleared hypotheses: r, hr, hd, hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
r : ℝ
hr : dist w z = r
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
hd₁ : DiffContOnCl ℂ f (ball z (dist w z))
⊢ ‖f w‖ = ‖f z‖
have hz₁ : IsMaxOn (norm ∘ f) (ball z (dist w z)) z
Tactic: subst r
Cleared hypotheses: r, hr, hd, hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (ball z (dist w z)) z
⊢ ‖f w‖ = ‖f z‖
have inl : ∀ (hd : DiffContOnCl ℂ f (ball w (dist w w))) (hz : IsMaxOn (norm ∘ f) (ball w (dist w w)) w), ‖f w‖ = ‖f w‖
Tactic: rcases eq_or_ne w z with (rfl | hne)
Cleared hypotheses: z, hd, hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (goal)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (ball z (dist w z)) z
inl : ∀ (hd : DiffContOnCl ℂ f (ball w (dist w w))) (hz : IsMaxOn (norm ∘ f) (ball w (dist w w)) w), ‖f w‖ = ‖f w‖
⊢ ‖f w‖ = ‖f z‖
have inr : ∀ (hne : w ≠ z), ‖f w‖ = ‖f z‖
Tactic: rcases eq_or_ne w z with (rfl | hne)
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (ball z (dist w z)) z
hne : w ≠ z
⊢ ‖f w‖ = ‖f z‖
have hne₁ : dist w z ≠ 0
Tactic: rw [← dist_ne_zero] at hne
Cleared hypotheses: hne
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (hypothesis)
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
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : w ∈ closedBall z r
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w
have hw₁ : dist z w ≤ r
Tactic: rw [mem_closedBall, dist_comm] at hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.Analysis.Complex.AbsMax (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
z : E
r : ℝ
hd : DiffContOnCl ℂ f (ball z r)
hz : IsMaxOn (norm ∘ f) (ball z r) z
w : E
hw : dist z w ≤ r
⊢ (norm ∘ f) w = Function.const E ‖f z‖ w
have inl : ∀ (hw : dist z z ≤ r), (norm ∘ f) z = Function.const E ‖f z‖ z
Tactic: rcases eq_or_ne z w with (rfl | hne)
Cleared hypotheses: w, hw