awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.AbelLimit
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
linarith : 1 - ‖z‖ = 0 → 1 - ‖z‖ - 0 + (‖z‖ - 1) = 0
⊢ 1 - ‖z‖ ≠ 0

Tactic:
linarith only [zn]
-- Module: Mathlib.Analysis.Complex.AbelLimit
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
linarith : M = 0 → -1 + (M - 0) + (1 - M) = 0
⊢ M ≠ 0

Tactic:
linarith only [hM]
-- Module: Mathlib.Analysis.Complex.AbelLimit
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
rw : ε / 4 / M * M * (1 - ‖z‖) / (1 - ‖z‖) = ε / 4
rw₁ : ε / 4 / M * M = ε / 4
rw₂ rw₃ : ε / 4 = ε / 4
⊢ M * (1 - ‖z‖) * (ε / 4 / M) / (1 - ‖z‖) = ε / 4

Tactic:
rw [← mul_rotate, mul_div_cancel_right₀ _ (by linarith only [zn]),
          div_mul_cancel₀ _ (by linarith only [hM])]

Premises used: div_mul_cancel₀, mul_div_cancel_right₀, mul_rotate
-- Module: Mathlib.Analysis.Complex.AbelLimit
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
⊢ ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4

Tactic:
have S₂ : ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i < ε / 4 :=
    calc
      _ ≤ ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ε / 4 / M * ‖z‖ ^ i := by
        gcongr with i hi
        have := hB₁ (i + 1) (by linarith only [(mem_Ico.mp hi).1])
        rw [norm_sub_rev] at this
        exact this.le
      _ = ‖1 - z‖ * (ε / 4 / M) * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖z‖ ^ i := by
        rw [← mul_sum, ← mul_assoc]
      _ ≤ ‖1 - z‖ * (ε / 4 / M) * ∑' i, ‖z‖ ^ i := by
        gcongr
        exact Summable.sum_le_tsum _ (fun _ _ ↦ by positivity)
          (summable_geometric_of_lt_one (by positivity) zn)
      _ = ‖1 - z‖ * (ε / 4 / M) / (1 - ‖z‖) := by
        rw [tsum_geometric_of_lt_one (by positivity) zn, ← div_eq_mul_inv]
      _ < M * (1 - ‖z‖) * (ε / 4 / M) / (1 - ‖z‖) := by gcongr
      _ = _ := by
        rw [← mul_rotate, mul_div_cancel_right₀ _ (by linarith only [zn]),
          div_mul_cancel₀ _ (by linarith only [hM])]
-- Module: Mathlib.Analysis.Complex.AbelLimit
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
⊢ ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i + ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i <
    ε / 4 + ε / 4

Tactic:
add_lt_add S₁ S₂

Premises used: add_lt_add
-- Module: Mathlib.Analysis.Complex.AbelLimit
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
h₁ : ε / 2 = ε / 4 + ε / 4
⊢ ‖1 - z‖ * ∑ i ∈ range B₁, ‖l - s (i + 1)‖ * ‖z‖ ^ i + ‖1 - z‖ * ∑ i ∈ Ico B₁ (max B₁ B₂), ‖l - s (i + 1)‖ * ‖z‖ ^ i <
    ε / 2

Tactic:
convert! add_lt_add S₁ S₂ using 1

Premises used: add_lt_add
-- Module: Mathlib.Analysis.Complex.AbelLimit
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
linarith₁₅ : ε / 4 + ε / 4 < ε / 2 → 1 * ε + 1 * ε - 2 * ε = 0
⊢ ε / 2 = ε / 4 + ε / 4

Tactic:
linarith only
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
s : ℝ
hs : 0 < s
⊢ Tendsto (fun (z : ℂ) ↦ ∑' (n : ℕ), f n * z ^ n) (𝓝[stolzCone s] 1) (𝓝 l)

Tactic:
(tendsto_tsum_powerSeries_nhdsWithin_stolzSet h).mono_left
    (nhdsWithin_stolzCone_le_nhdsWithin_stolzSet hs).choose_spec

Premises used: Exists.choose_spec, Filter.Tendsto.mono_left, Complex.nhdsWithin_stolzCone_le_nhdsWithin_stolzSet, Complex.tendsto_tsum_powerSeries_nhdsWithin_stolzSet
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
⊢ Tendsto (fun (z : ℂ) ↦ ∑' (n : ℕ), f n * z ^ n) (Filter.map ofReal (𝓝[<] 1)) (𝓝 l)

Tactic:
(tendsto_tsum_powerSeries_nhdsWithin_stolzSet (M := 2) h).mono_left
    (nhdsWithin_lt_le_nhdsWithin_stolzSet one_lt_two)

Premises used: Complex.nhdsWithin_lt_le_nhdsWithin_stolzSet, one_lt_two, Filter.Tendsto.mono_left, Complex.tendsto_tsum_powerSeries_nhdsWithin_stolzSet
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℝ
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
⊢ Filter.map ofReal (𝓝 l) ≤ 𝓝 (↑l : ℂ)

Tactic:
have m : (𝓝 l).map ofReal ≤ 𝓝 ↑l := ofRealCLM.continuous.tendsto l
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℝ
l : ℝ
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
m : Filter.map ofReal (𝓝 l) ≤ 𝓝 (↑l : ℂ)
⊢ Tendsto (α := ℕ) (ofReal ∘ fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 (↑l : ℂ))

Tactic:
replace h := (tendsto_map.comp h).mono_right m
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℝ
l : ℝ
m : Filter.map ofReal (𝓝 l) ≤ 𝓝 (↑l : ℂ)
h : Tendsto (α := ℕ) (ofReal ∘ fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 (↑l : ℂ))
⊢ Tendsto (fun (x : ℕ) ↦ (↑(∑ i ∈ range x, f i) : ℂ)) atTop (𝓝 (↑l : ℂ))

Tactic:
rw [Function.comp_def] at h

Premises used: Function.comp_def
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℝ
l : ℝ
m : Filter.map ofReal (𝓝 l) ≤ 𝓝 (↑l : ℂ)
h : Tendsto (fun (x : ℕ) ↦ (↑(∑ i ∈ range x, f i) : ℂ)) atTop (𝓝 (↑l : ℂ))
⊢ Tendsto (fun (x : ℕ) ↦ ∑ i ∈ range x, (↑(f i) : ℂ)) atTop (𝓝 (↑l : ℂ))

Tactic:
push_cast at h
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℝ
l : ℝ
m : Filter.map ofReal (𝓝 l) ≤ 𝓝 (↑l : ℂ)
h : Tendsto (fun (x : ℕ) ↦ ∑ i ∈ range x, (↑(f i) : ℂ)) atTop (𝓝 (↑l : ℂ))
⊢ Tendsto (fun (z : ℂ) ↦ ∑' (n : ℕ), (↑(f n) : ℂ) * z ^ n) (Filter.map ofReal (𝓝[<] 1)) (𝓝 (↑l : ℂ))

Tactic:
replace h := Complex.tendsto_tsum_powerSeries_nhdsWithin_lt h
-- Module: Mathlib.Analysis.Complex.AbelLimit
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 (z : ℂ) ↦ ∑' (n : ℕ), (↑(f n) : ℂ) * z ^ n) ∘ ofReal) (𝓝[<] 1) (𝓝 (↑l : ℂ))

Tactic:
rw [tendsto_map'_iff] at h

Premises used: Filter.tendsto_map'_iff
-- Module: Mathlib.Analysis.Complex.AbelLimit
Goal:
f : ℕ → ℝ
l : ℝ
m : Filter.map ofReal (𝓝 l) ≤ 𝓝 (↑l : ℂ)
h : Tendsto ((fun (z : ℂ) ↦ ∑' (n : ℕ), (↑(f n) : ℂ) * z ^ n) ∘ ofReal) (𝓝[<] 1) (𝓝 (↑l : ℂ))
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 < ε
⊢ Tendsto (fun (x : ℝ) ↦ ∑' (n : ℕ), f n * x ^ n) (𝓝[<] 1) (𝓝 l)

Tactic:
rw [Metric.tendsto_nhdsWithin_nhds] at h ⊢

Premises used: Metric.tendsto_nhdsWithin_nhds
-- Module: Mathlib.Analysis.Complex.AbelLimit
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 (((fun (z : ℂ) ↦ ∑' (n : ℕ), (↑(f n) : ℂ) * z ^ n) ∘ ofReal) x) (↑l : ℂ) < ε

Tactic:
h
-- Module: Mathlib.Analysis.Complex.AbelLimit
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 : ℂ) < ε
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 : ℂ)
⊢ ∀ ε > 0,
    ∃ δ > 0, ∀ ⦃x : ℝ⦄, Membership.mem (γ := Set ℝ) (Set.Iio 1) x → dist x 1 < δ → dist (∑' (n : ℕ), f n * x ^ n) l < ε

Tactic:
convert! h
-- Module: Mathlib.Analysis.Complex.AbelLimit
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
h₁ : ‖∑' (n : ℕ), f n * a_1 ^ n - l‖ = ‖∑' (n : ℕ), (↑(f n) : ℂ) * (↑a_1 : ℂ) ^ n - (↑l : ℂ)‖
⊢ dist (∑' (n : ℕ), f n * a_1 ^ n) l = dist (((fun (z : ℂ) ↦ ∑' (n : ℕ), (↑(f n) : ℂ) * z ^ n) ∘ ofReal) a_1) (↑l : ℂ)

Tactic:
simp_rw [Function.comp_apply, dist_eq_norm]

Premises used: dist_eq_norm, Function.comp_apply
-- Module: Mathlib.Analysis.Complex.AbelLimit
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
h₁ h₂ h₃ h₄ : ‖∑' (n : ℕ), f n * a_1 ^ n - l‖ = ‖∑' (n : ℕ), f n * a_1 ^ n - l‖
⊢ ‖∑' (n : ℕ), f n * a_1 ^ n - l‖ = ‖∑' (n : ℕ), (↑(f n) : ℂ) * (↑a_1 : ℂ) ^ n - (↑l : ℂ)‖

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (closedBall z (dist w z)) z
⊢ let r := dist w z;
  DiffContOnCl ℂ f (ball z r)

Tactic:
set r : ℝ := dist w z

Premises used: Dist.dist
-- Module: Mathlib.Analysis.Complex.AbsMax
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
f : ℂ → F
z w : ℂ
hd : DiffContOnCl ℂ f (ball z (dist w z))
hz : IsMaxOn (norm ∘ f) (closedBall z (dist w z)) z
hd₁ :
  let r := dist w z;
  DiffContOnCl ℂ f (ball z r)
⊢ let r := dist w z;
  IsMaxOn (norm ∘ f) (closedBall z r) z

Tactic:
set r : ℝ := dist w z

Premises used: Dist.dist
-- Module: Mathlib.Analysis.Complex.AbsMax
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
⊢ w ∈ closedBall z r

Tactic:
have hw : w ∈ closedBall z r := mem_closedBall.2 le_rfl
-- Module: Mathlib.Analysis.Complex.AbsMax
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‖

Tactic:
(isMaxOn_iff.1 hz _ hw).antisymm (not_lt.1 ?_)

Premises used: LE.le.antisymm, isMaxOn_iff, not_lt, Iff.mp
-- Module: Mathlib.Analysis.Complex.AbsMax
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
refine : ¬(norm ∘ f) w < (norm ∘ f) z
⊢ ‖f w‖ = ‖f z‖

Tactic:
refine (isMaxOn_iff.1 hz _ hw).antisymm (not_lt.1 ?_)

Premises used: LE.le.antisymm, isMaxOn_iff, not_lt, Iff.mp
-- Module: Mathlib.Analysis.Complex.AbsMax
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‖
⊢ 0 < r

Tactic:
have hr : 0 < r := dist_pos.2 (ne_of_apply_ne (norm ∘ f) hw_lt.ne)
-- Module: Mathlib.Analysis.Complex.AbsMax
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

Tactic:
this.ne ?_

Premises used: LT.lt.ne
-- Module: Mathlib.Analysis.Complex.AbsMax
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‖
refine : norm.{v} (E := F) (∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ) = 2 * π * ‖f z‖
⊢ False

Tactic:
refine this.ne ?_

Premises used: LT.lt.ne
-- Module: Mathlib.Analysis.Complex.AbsMax
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‖
⊢ ∮ (ζ : ℂ) 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)
-- Module: Mathlib.Analysis.Complex.AbsMax
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‖
A : ∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ = (2 * (↑π : ℂ) * I) • f z
⊢ norm.{v} (E := F) (∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ) = 2 * π * ‖f z‖

Tactic:
simp [A, norm_smul, Real.pi_pos.le]

Premises used: norm_smul, Real.pi_pos, LT.lt.le
-- Module: Mathlib.Analysis.Complex.AbsMax
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
suffices : norm.{v} (E := F) (∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ) < 2 * π * ‖f z‖
⊢ False

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]
-- Module: Mathlib.Analysis.Complex.AbsMax
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‖
rwa₁ rwa₂ rwa₃ 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‖
⊢ norm.{v} (E := F) (∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ) < 2 * π * ‖f z‖

Tactic:
rwa [mul_assoc, mul_div_cancel₀ _ hr.ne'] at this

Premises used: mul_assoc, mul_div_cancel₀, LT.lt.ne'
-- Module: Mathlib.Analysis.Complex.AbsMax
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
suffices : 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:
suffices ‖∮ ζ in C(z, r), (ζ - z)⁻¹ • f ζ‖ < 2 * π * r * (‖f z‖ / r) by
    rwa [mul_assoc, mul_div_cancel₀ _ hr.ne'] at this
-- Module: Mathlib.Analysis.Complex.AbsMax
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
⊢ sphere z r ⊆ closedBall z r

Tactic:
have hsub : sphere z r ⊆ closedBall z r := sphere_subset_closedBall
-- Module: Mathlib.Analysis.Complex.AbsMax
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)

Tactic:
circleIntegral.norm_integral_lt_of_norm_le_const_of_lt hr ?_ ?_ ⟨w, rfl, ?_⟩

Premises used: circleIntegral.norm_integral_lt_of_norm_le_const_of_lt, And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.Complex.AbsMax
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
refine_3 : ‖(w - z)⁻¹ • f w‖ < ‖f z‖ / r
⊢ norm.{v} (E := F) (∮ (ζ : ℂ) in C(z, r), (ζ - z)⁻¹ • f ζ) < 2 * π * r * (‖f z‖ / r)

Tactic:
refine circleIntegral.norm_integral_lt_of_norm_le_const_of_lt hr ?_ ?_ ⟨w, rfl, ?_⟩

Premises used: circleIntegral.norm_integral_lt_of_norm_le_const_of_lt, And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.Complex.AbsMax
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)

Tactic:
((continuousOn_id.sub continuousOn_const).inv₀ ?_).smul (hd.continuousOn_ball.mono hsub)

Premises used: ContinuousOn.sub, continuousOn_const, DiffContOnCl.continuousOn_ball, ContinuousOn.smul, ContinuousOn.inv₀, ContinuousOn.mono, continuousOn_id
-- Module: Mathlib.Analysis.Complex.AbsMax
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 : ∀ x ∈ sphere z r, _root_.id x - z ≠ 0
⊢ ContinuousOn.{0, v} (Y := F) (fun (ζ : ℂ) ↦ (ζ - z)⁻¹ • f ζ) (sphere z r)

Tactic:
refine ((continuousOn_id.sub continuousOn_const).inv₀ ?_).smul (hd.continuousOn_ball.mono hsub)

Premises used: ContinuousOn.sub, continuousOn_const, DiffContOnCl.continuousOn_ball, ContinuousOn.smul, ContinuousOn.inv₀, ContinuousOn.mono, continuousOn_id
-- Module: Mathlib.Analysis.Complex.AbsMax
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
⊢ ∀ x ∈ sphere z r, _root_.id x - z ≠ 0

Tactic:
fun ζ hζ => sub_ne_zero.2 (ne_of_mem_sphere hζ hr.ne')

Premises used: Iff.mpr, Metric.ne_of_mem_sphere, sub_ne_zero, LT.lt.ne'