awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a : ℕ
z : ℂ
⊢ (1 - z) ^ (a + 1) = (1 - z) ^ HAdd.hAdd (α := ℂ) (↑a : ℂ) 1
have h : (1 - z) ^ (a + 1) = (1 - z) ^ (a + 1)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a n : ℕ
⊢ (↑((a + n).choose a) : ℂ) = Ring.choose (HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 + (↑n : ℂ) - 1) n
have h : Ring.choose (HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 + (↑n : ℂ) - 1) n = (↑((a + n).choose a) : ℂ)
Tactic: rw [eq_comm, add_right_comm, add_sub_cancel_right, ← Nat.cast_add,
      Ring.choose_natCast, Nat.choose_symm_add]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a n : ℕ
h : Ring.choose (HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 + (↑n : ℂ) - 1) n = (↑((a + n).choose a) : ℂ)
⊢ (↑((a + n).choose a) : ℂ) = Ring.choose (HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 + (↑n : ℂ) - 1) n
have h₁ : Ring.choose (HAdd.hAdd (α := ℂ) (↑a : ℂ) (↑n : ℂ) + 1 - 1) n = (↑((a + n).choose a) : ℂ)
Tactic: rw [eq_comm, add_right_comm, add_sub_cancel_right, ← Nat.cast_add,
      Ring.choose_natCast, Nat.choose_symm_add]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a n : ℕ
h : Ring.choose (HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 + (↑n : ℂ) - 1) n = (↑((a + n).choose a) : ℂ)
h₁ : Ring.choose (HAdd.hAdd (α := ℂ) (↑a : ℂ) (↑n : ℂ) + 1 - 1) n = (↑((a + n).choose a) : ℂ)
⊢ (↑((a + n).choose a) : ℂ) = Ring.choose (HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 + (↑n : ℂ) - 1) n
have h₂ : Ring.choose (HAdd.hAdd (α := ℂ) (↑a : ℂ) (↑n : ℂ)) n = (↑((a + n).choose a) : ℂ)
Tactic: rw [eq_comm, add_right_comm, add_sub_cancel_right, ← Nat.cast_add,
      Ring.choose_natCast, Nat.choose_symm_add]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a n : ℕ
h : Ring.choose (HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 + (↑n : ℂ) - 1) n = (↑((a + n).choose a) : ℂ)
h₁ : Ring.choose (HAdd.hAdd (α := ℂ) (↑a : ℂ) (↑n : ℂ) + 1 - 1) n = (↑((a + n).choose a) : ℂ)
h₂ : Ring.choose (HAdd.hAdd (α := ℂ) (↑a : ℂ) (↑n : ℂ)) n = (↑((a + n).choose a) : ℂ)
⊢ (↑((a + n).choose a) : ℂ) = Ring.choose (HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 + (↑n : ℂ) - 1) n
have h₃ : Eq (α := ℂ) (Ring.choose (↑(a + n) : ℂ) n) (↑((a + n).choose a) : ℂ)
Tactic: rw [eq_comm, add_right_comm, add_sub_cancel_right, ← Nat.cast_add,
      Ring.choose_natCast, Nat.choose_symm_add]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a n : ℕ
h : Ring.choose (HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 + (↑n : ℂ) - 1) n = (↑((a + n).choose a) : ℂ)
h₁ : Ring.choose (HAdd.hAdd (α := ℂ) (↑a : ℂ) (↑n : ℂ) + 1 - 1) n = (↑((a + n).choose a) : ℂ)
h₂ : Ring.choose (HAdd.hAdd (α := ℂ) (↑a : ℂ) (↑n : ℂ)) n = (↑((a + n).choose a) : ℂ)
h₃ : Eq (α := ℂ) (Ring.choose (↑(a + n) : ℂ) n) (↑((a + n).choose a) : ℂ)
⊢ (↑((a + n).choose a) : ℂ) = Ring.choose (HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 + (↑n : ℂ) - 1) n
have h₄ : Eq (α := ℂ) (↑((a + n).choose n) : ℂ) (↑((a + n).choose a) : ℂ)
Tactic: rw [eq_comm, add_right_comm, add_sub_cancel_right, ← Nat.cast_add,
      Ring.choose_natCast, Nat.choose_symm_add]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a n : ℕ
h : Ring.choose (HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 + (↑n : ℂ) - 1) n = (↑((a + n).choose a) : ℂ)
h₁ : Ring.choose (HAdd.hAdd (α := ℂ) (↑a : ℂ) (↑n : ℂ) + 1 - 1) n = (↑((a + n).choose a) : ℂ)
h₂ : Ring.choose (HAdd.hAdd (α := ℂ) (↑a : ℂ) (↑n : ℂ)) n = (↑((a + n).choose a) : ℂ)
h₃ : Eq (α := ℂ) (Ring.choose (↑(a + n) : ℂ) n) (↑((a + n).choose a) : ℂ)
h₄ : Eq (α := ℂ) (↑((a + n).choose n) : ℂ) (↑((a + n).choose a) : ℂ)
⊢ (↑((a + n).choose a) : ℂ) = Ring.choose (HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 + (↑n : ℂ) - 1) n
have h₅ : Eq (α := ℂ) (↑((a + n).choose n) : ℂ) (↑((a + n).choose n) : ℂ)
Tactic: rw [eq_comm, add_right_comm, add_sub_cancel_right, ← Nat.cast_add,
      Ring.choose_natCast, Nat.choose_symm_add]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (hypothesis)
Goal:
a : ℕ
z : ℂ
hz : z ≠ 0
⊢ HasFPowerSeriesOnBall (𝕜 := ℂ) (F := ℂ) (fun (x : ℂ) ↦ 1 / (z - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (z ^ (n + a + 1))⁻¹ * (↑((a + n).choose a) : ℂ)) 0 ‖z‖ₑ
have this : HasFPowerSeriesOnBall (𝕜 := ℂ) (F := ℂ) (fun (x : ℂ) ↦ 1 / (1 - x) ^ (a + 1))
  (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (↑((a + n).choose a) : ℂ)) 0 1
Tactic: have := one_div_one_sub_pow_hasFPowerSeriesOnBall_zero a
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (hypothesis)
Goal:
a : ℕ
z : ℂ
hz : z ≠ 0
this :
  HasFPowerSeriesOnBall (𝕜 := ℂ) (F := ℂ) (fun (x : ℂ) ↦ 1 / (1 - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (↑((a + n).choose a) : ℂ)) 0 1
⊢ HasFPowerSeriesOnBall (𝕜 := ℂ) (F := ℂ) (fun (x : ℂ) ↦ 1 / (z - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (z ^ (n + a + 1))⁻¹ * (↑((a + n).choose a) : ℂ)) 0 ‖z‖ₑ
have this₁ : HasFPowerSeriesOnBall (𝕜 := ℂ) (E := ℂ) (F := ℂ) (fun (x : ℂ) ↦ 1 / (1 - x) ^ (a + 1))
  (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (↑((a + n).choose a) : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ)
  ((HSMul.hSMul (β := ℂ →L[ℂ] ℂ) z⁻¹ 1 : (a : ℂ) → ℂ) 0 : ℂ) 1
Tactic: rw [← map_zero (z⁻¹ • 1 : ℂ →L[ℂ] ℂ)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (hypothesis)
Goal:
a : ℕ
z : ℂ
hz : z ≠ 0
this :
  HasFPowerSeriesOnBall (𝕜 := ℂ) (E := ℂ) (F := ℂ) (fun (x : ℂ) ↦ 1 / (1 - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (↑((a + n).choose a) : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ)
    ((HSMul.hSMul (β := ℂ →L[ℂ] ℂ) z⁻¹ 1 : (a : ℂ) → ℂ) 0 : ℂ) 1
⊢ HasFPowerSeriesOnBall (𝕜 := ℂ) (F := ℂ) (fun (x : ℂ) ↦ 1 / (z - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (z ^ (n + a + 1))⁻¹ * (↑((a + n).choose a) : ℂ)) 0 ‖z‖ₑ
have this₁ : HasFPowerSeriesOnBall ((fun (x : ℂ) ↦ 1 / (1 - x) ^ (a + 1)) ∘ (⇑(HSMul.hSMul (β := ℂ →L[ℂ] ℂ) z⁻¹ 1) : (a : ℂ) → ℂ))
  (FormalMultilinearSeries.compContinuousLinearMap
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (↑((a + n).choose a) : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ)
    (HSMul.hSMul (β := ℂ →L[ℂ] ℂ) z⁻¹ 1))
  0 (1 / ‖HSMul.hSMul (β := ℂ →L[ℂ] ℂ) z⁻¹ 1‖ₑ)
Tactic: have := this.compContinuousLinearMap
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (hypothesis)
Goal:
a : ℕ
z : ℂ
hz : z ≠ 0
this_1 :
  HasFPowerSeriesOnBall (𝕜 := ℂ) (E := ℂ) (F := ℂ) (fun (x : ℂ) ↦ 1 / (1 - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (↑((a + n).choose a) : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ)
    ((HSMul.hSMul (β := ℂ →L[ℂ] ℂ) z⁻¹ 1 : (a : ℂ) → ℂ) 0 : ℂ) 1
this :
  HasFPowerSeriesOnBall ((fun (x : ℂ) ↦ 1 / (1 - x) ^ (a + 1)) ∘ (⇑(HSMul.hSMul (β := ℂ →L[ℂ] ℂ) z⁻¹ 1) : (a : ℂ) → ℂ))
    (FormalMultilinearSeries.compContinuousLinearMap
      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (↑((a + n).choose a) : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ)
      (HSMul.hSMul (β := ℂ →L[ℂ] ℂ) z⁻¹ 1))
    0 (1 / ‖HSMul.hSMul (β := ℂ →L[ℂ] ℂ) z⁻¹ 1‖ₑ)
⊢ HasFPowerSeriesOnBall (𝕜 := ℂ) (F := ℂ) (fun (x : ℂ) ↦ 1 / (z - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (z ^ (n + a + 1))⁻¹ * (↑((a + n).choose a) : ℂ)) 0 ‖z‖ₑ
have H : 1 / ‖HSMul.hSMul (β := ℂ →L[ℂ] ℂ) z⁻¹ 1‖ₑ = ‖z‖ₑ
Tactic: have H : 1 / ‖(z⁻¹ • 1 : ℂ →L[ℂ] ℂ)‖ₑ = ‖z‖ₑ := by simp [enorm_smul, enorm_inv, hz]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (hypothesis)
Goal:
a : ℕ
z : ℂ
hz : z ≠ 0
this_1 :
  HasFPowerSeriesOnBall (𝕜 := ℂ) (E := ℂ) (F := ℂ) (fun (x : ℂ) ↦ 1 / (1 - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (↑((a + n).choose a) : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ)
    ((HSMul.hSMul (β := ℂ →L[ℂ] ℂ) z⁻¹ 1 : (a : ℂ) → ℂ) 0 : ℂ) 1
this :
  HasFPowerSeriesOnBall ((fun (x : ℂ) ↦ 1 / (1 - x) ^ (a + 1)) ∘ (⇑(HSMul.hSMul (β := ℂ →L[ℂ] ℂ) z⁻¹ 1) : (a : ℂ) → ℂ))
    (FormalMultilinearSeries.compContinuousLinearMap
      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (↑((a + n).choose a) : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ)
      (HSMul.hSMul (β := ℂ →L[ℂ] ℂ) z⁻¹ 1))
    0 (1 / ‖HSMul.hSMul (β := ℂ →L[ℂ] ℂ) z⁻¹ 1‖ₑ)
H : 1 / ‖HSMul.hSMul (β := ℂ →L[ℂ] ℂ) z⁻¹ 1‖ₑ = ‖z‖ₑ
⊢ HasFPowerSeriesOnBall (𝕜 := ℂ) (F := ℂ) (fun (x : ℂ) ↦ 1 / (z - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (z ^ (n + a + 1))⁻¹ * (↑((a + n).choose a) : ℂ)) 0 ‖z‖ₑ
have this₁ : HasFPowerSeriesOnBall (fun (x : ℂ) ↦ ((1 - HSMul.hSMul (β := (a : ℂ) → ℂ) z⁻¹ (⇑1 : (a : ℂ) → ℂ) x) ^ (a + 1))⁻¹)
  (FormalMultilinearSeries.compContinuousLinearMap
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (↑((a + n).choose a) : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ)
    (HSMul.hSMul (β := ℂ →L[ℂ] ℂ) z⁻¹ 1))
  0 ‖z‖ₑ
Tactic: simp only [one_div, ContinuousLinearMap.coe_smul', H, Function.comp_def] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a : ℕ
z : ℂ
hz : z ≠ 0
this_1 :
  HasFPowerSeriesOnBall (𝕜 := ℂ) (E := ℂ) (F := ℂ) (fun (x : ℂ) ↦ 1 / (1 - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (↑((a + n).choose a) : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ)
    ((HSMul.hSMul (β := ℂ →L[ℂ] ℂ) z⁻¹ 1 : (a : ℂ) → ℂ) 0 : ℂ) 1
H : 1 / ‖HSMul.hSMul (β := ℂ →L[ℂ] ℂ) z⁻¹ 1‖ₑ = ‖z‖ₑ
this :
  HasFPowerSeriesOnBall (fun (x : ℂ) ↦ ((1 - HSMul.hSMul (β := (a : ℂ) → ℂ) z⁻¹ (⇑1 : (a : ℂ) → ℂ) x) ^ (a + 1))⁻¹)
    (FormalMultilinearSeries.compContinuousLinearMap
      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (↑((a + n).choose a) : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ)
      (HSMul.hSMul (β := ℂ →L[ℂ] ℂ) z⁻¹ 1))
    0 ‖z‖ₑ
⊢ HasFPowerSeriesOnBall (𝕜 := ℂ) (F := ℂ) (fun (x : ℂ) ↦ 1 / (z - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (z ^ (n + a + 1))⁻¹ * (↑((a + n).choose a) : ℂ)) 0 ‖z‖ₑ
have h : (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (z ^ (n + a + 1))⁻¹ * (↑((a + n).choose a) : ℂ)) =
  HSMul.hSMul (β := FormalMultilinearSeries ℂ ℂ ℂ) (z ^ (a + 1))⁻¹
    (FormalMultilinearSeries.compContinuousLinearMap
        (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (↑((a + n).choose a) : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ)
        (HSMul.hSMul (β := ℂ →L[ℂ] ℂ) z⁻¹ 1) :
      FormalMultilinearSeries ℂ ℂ ℂ)
Tactic: convert! (this.const_smul (c := (z ^ (a + 1))⁻¹)).congr ?_ using 2
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a : ℕ
z : ℂ
hz : z ≠ 0
this_1 :
  HasFPowerSeriesOnBall (𝕜 := ℂ) (E := ℂ) (F := ℂ) (fun (x : ℂ) ↦ 1 / (1 - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (↑((a + n).choose a) : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ)
    ((HSMul.hSMul (β := ℂ →L[ℂ] ℂ) z⁻¹ 1 : (a : ℂ) → ℂ) 0 : ℂ) 1
H : 1 / ‖HSMul.hSMul (β := ℂ →L[ℂ] ℂ) z⁻¹ 1‖ₑ = ‖z‖ₑ
this :
  HasFPowerSeriesOnBall (fun (x : ℂ) ↦ ((1 - HSMul.hSMul (β := (a : ℂ) → ℂ) z⁻¹ (⇑1 : (a : ℂ) → ℂ) x) ^ (a + 1))⁻¹)
    (FormalMultilinearSeries.compContinuousLinearMap
      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (↑((a + n).choose a) : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ)
      (HSMul.hSMul (β := ℂ →L[ℂ] ℂ) z⁻¹ 1))
    0 ‖z‖ₑ
h :
  (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (z ^ (n + a + 1))⁻¹ * (↑((a + n).choose a) : ℂ)) =
    HSMul.hSMul (β := FormalMultilinearSeries ℂ ℂ ℂ) (z ^ (a + 1))⁻¹
      (FormalMultilinearSeries.compContinuousLinearMap
          (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (↑((a + n).choose a) : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ)
          (HSMul.hSMul (β := ℂ →L[ℂ] ℂ) z⁻¹ 1) :
        FormalMultilinearSeries ℂ ℂ ℂ)
⊢ HasFPowerSeriesOnBall (𝕜 := ℂ) (F := ℂ) (fun (x : ℂ) ↦ 1 / (z - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (z ^ (n + a + 1))⁻¹ * (↑((a + n).choose a) : ℂ)) 0 ‖z‖ₑ
have convert_2 : Set.EqOn
  (HSMul.hSMul (β := ℂ → ℂ) (z ^ (a + 1))⁻¹ fun (x : ℂ) ↦
    ((1 - HSMul.hSMul (β := (a : ℂ) → ℂ) z⁻¹ (⇑1 : (a : ℂ) → ℂ) x) ^ (a + 1))⁻¹)
  (fun (x : ℂ) ↦ 1 / (z - x) ^ (a + 1)) (Metric.eball 0 ‖z‖ₑ)
Tactic: convert! (this.const_smul (c := (z ^ (a + 1))⁻¹)).congr ?_ using 2
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a : ℕ
z : ℂ
hz : z ≠ 0
this_1 :
  HasFPowerSeriesOnBall (𝕜 := ℂ) (E := ℂ) (F := ℂ) (fun (x : ℂ) ↦ 1 / (1 - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (↑((a + n).choose a) : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ)
    ((HSMul.hSMul (β := ℂ →L[ℂ] ℂ) z⁻¹ 1 : (a : ℂ) → ℂ) 0 : ℂ) 1
H : 1 / ‖HSMul.hSMul (β := ℂ →L[ℂ] ℂ) z⁻¹ 1‖ₑ = ‖z‖ₑ
this :
  HasFPowerSeriesOnBall (fun (x : ℂ) ↦ ((1 - HSMul.hSMul (β := (a : ℂ) → ℂ) z⁻¹ (⇑1 : (a : ℂ) → ℂ) x) ^ (a + 1))⁻¹)
    (FormalMultilinearSeries.compContinuousLinearMap
      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (↑((a + n).choose a) : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ)
      (HSMul.hSMul (β := ℂ →L[ℂ] ℂ) z⁻¹ 1))
    0 ‖z‖ₑ
⊢ (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (z ^ (n + a + 1))⁻¹ * (↑((a + n).choose a) : ℂ)) =
    HSMul.hSMul (β := FormalMultilinearSeries ℂ ℂ ℂ) (z ^ (a + 1))⁻¹
      (FormalMultilinearSeries.compContinuousLinearMap
          (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (↑((a + n).choose a) : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ)
          (HSMul.hSMul (β := ℂ →L[ℂ] ℂ) z⁻¹ 1) :
        FormalMultilinearSeries ℂ ℂ ℂ)
have h : ∀ (n : ℕ),
  Eq (α := ℂ)
    ((FormalMultilinearSeries.ofScalars ℂ (fun (n : ℕ) ↦ (z ^ (n + a + 1))⁻¹ * (↑((a + n).choose a) : ℂ)) n :
          (a : (i : Fin n) → ℂ) → ℂ)
        fun (x : Fin n) ↦ 1 :
      ℂ)
    ((HSMul.hSMul (β := FormalMultilinearSeries ℂ ℂ ℂ) (z ^ (a + 1))⁻¹
            (FormalMultilinearSeries.compContinuousLinearMap
                (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (↑((a + n).choose a) : ℂ) :
                  FormalMultilinearSeries ℂ ℂ ℂ)
                (HSMul.hSMul (β := ℂ →L[ℂ] ℂ) z⁻¹ 1) :
              FormalMultilinearSeries ℂ ℂ ℂ)
            n :
          (a : (i : Fin n) → ℂ) → ℂ)
        fun (x : Fin n) ↦ 1 :
      ℂ)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a b : ℂ
⊢ HasFPowerSeriesOnBall (𝕜 := ℂ) (F := ℂ) (fun (x : ℂ) ↦ (b - a) / (1 - x) + a / HPow.hPow (β := ℕ) (1 - x) 2)
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ a * (↑n : ℂ) + b) 0 1
have h : ∀ (x : ℂ),
  (b - a) / (1 - x) + a / HPow.hPow (β := ℕ) (1 - x) 2 =
    ((HSMul.hSMul (β := ℂ → ℂ) (b - a) fun (x : ℂ) ↦ 1 / (1 - x)) +
        HSMul.hSMul (β := ℂ → ℂ) a fun (x : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (1 - x) 2)
      x
Tactic: convert!
    (one_div_one_sub_hasFPowerSeriesOnBall_zero.const_smul (c := b - a)).add
      (one_div_one_sub_sq_hasFPowerSeriesOnBall_zero.const_smul (c := a)) using 2
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a b : ℂ
h :
  ∀ (x : ℂ),
    (b - a) / (1 - x) + a / HPow.hPow (β := ℕ) (1 - x) 2 =
      ((HSMul.hSMul (β := ℂ → ℂ) (b - a) fun (x : ℂ) ↦ 1 / (1 - x)) +
          HSMul.hSMul (β := ℂ → ℂ) a fun (x : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (1 - x) 2)
        x
⊢ HasFPowerSeriesOnBall (𝕜 := ℂ) (F := ℂ) (fun (x : ℂ) ↦ (b - a) / (1 - x) + a / HPow.hPow (β := ℕ) (1 - x) 2)
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ a * (↑n : ℂ) + b) 0 1
have h₁ : (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ a * (↑n : ℂ) + b) =
  HSMul.hSMul (β := FormalMultilinearSeries ℂ ℂ ℂ) (b - a)
      (FormalMultilinearSeries.ofScalars ℂ 1 : FormalMultilinearSeries ℂ ℂ ℂ) +
    HSMul.hSMul (β := FormalMultilinearSeries ℂ ℂ ℂ) a
      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 : FormalMultilinearSeries ℂ ℂ ℂ)
Tactic: convert!
    (one_div_one_sub_hasFPowerSeriesOnBall_zero.const_smul (c := b - a)).add
      (one_div_one_sub_sq_hasFPowerSeriesOnBall_zero.const_smul (c := a)) using 2
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a b : ℂ
⊢ (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ a * (↑n : ℂ) + b) =
    HSMul.hSMul (β := FormalMultilinearSeries ℂ ℂ ℂ) (b - a)
        (FormalMultilinearSeries.ofScalars ℂ 1 : FormalMultilinearSeries ℂ ℂ ℂ) +
      HSMul.hSMul (β := FormalMultilinearSeries ℂ ℂ ℂ) a
        (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 :
          FormalMultilinearSeries ℂ ℂ ℂ)
have h : ∀ (n : ℕ),
  Eq (α := ℂ)
    ((FormalMultilinearSeries.ofScalars ℂ (fun (n : ℕ) ↦ a * (↑n : ℂ) + b) n : (a : (i : Fin n) → ℂ) → ℂ)
        fun (x : Fin n) ↦ 1 :
      ℂ)
    (((HSMul.hSMul (β := FormalMultilinearSeries ℂ ℂ ℂ) (b - a)
                (FormalMultilinearSeries.ofScalars ℂ 1 : FormalMultilinearSeries ℂ ℂ ℂ) +
              HSMul.hSMul (β := FormalMultilinearSeries ℂ ℂ ℂ) a
                (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 :
                  FormalMultilinearSeries ℂ ℂ ℂ))
            n :
          (a : (i : Fin n) → ℂ) → ℂ)
        fun (x : Fin n) ↦ 1 :
      ℂ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a b : ℂ
n : ℕ
⊢ Eq (α := ℂ)
    ((FormalMultilinearSeries.ofScalars ℂ (fun (n : ℕ) ↦ a * (↑n : ℂ) + b) n : (a : (i : Fin n) → ℂ) → ℂ)
        fun (x : Fin n) ↦ 1 :
      ℂ)
    (((HSMul.hSMul (β := FormalMultilinearSeries ℂ ℂ ℂ) (b - a)
                (FormalMultilinearSeries.ofScalars ℂ 1 : FormalMultilinearSeries ℂ ℂ ℂ) +
              HSMul.hSMul (β := FormalMultilinearSeries ℂ ℂ ℂ) a
                (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 :
                  FormalMultilinearSeries ℂ ℂ ℂ))
            n :
          (a : (i : Fin n) → ℂ) → ℂ)
        fun (x : Fin n) ↦ 1 :
      ℂ)
have h : a * (↑n : ℂ) + b = b - a + a * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
w x : ℂ
hw : w ≠ x
⊢ HasFPowerSeriesOnBall (𝕜 := ℂ) (F := ℂ) (fun (z : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (z - w) 2 - 1 / HPow.hPow (β := ℕ) w 2)
    (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
      HSub.hSub (β := ℂ) (HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HPow.hPow (β := ℤ) (w - x) (-(↑(i + 2) : ℤ)))
        (Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) w (-2)) 0 : ℂ))
    x ‖w - x‖ₑ
have rw : HasFPowerSeriesOnBall
  (HSub.hSub (α := (i : ℂ) → ℂ) (fun (z : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (z - w) 2) fun (z : ℂ) ↦
    1 / HPow.hPow (β := ℕ) w 2)
  (HSub.hSub (α := FormalMultilinearSeries ℂ ℂ ℂ) (β := FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
        HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HPow.hPow (β := ℤ) (w - x) (-(↑(i + 2) : ℤ)) :
      FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
        Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) w (-2)) 0 :
      FormalMultilinearSeries ℂ ℂ ℂ))
  x ‖w - x‖ₑ
Tactic: rw [← Pi.sub_def, ← Pi.sub_def, FormalMultilinearSeries.ofScalars_sub]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
w x : ℂ
hw : w ≠ x
⊢ HasFPowerSeriesOnBall
    (HSub.hSub (α := (i : ℂ) → ℂ) (fun (z : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (z - w) 2) fun (z : ℂ) ↦
      1 / HPow.hPow (β := ℕ) w 2)
    (HSub.hSub (α := FormalMultilinearSeries ℂ ℂ ℂ) (β := FormalMultilinearSeries ℂ ℂ ℂ)
      (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
          HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HPow.hPow (β := ℤ) (w - x) (-(↑(i + 2) : ℤ)) :
        FormalMultilinearSeries ℂ ℂ ℂ)
      (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
          Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) w (-2)) 0 :
        FormalMultilinearSeries ℂ ℂ ℂ))
    x ‖w - x‖ₑ
have refine_1 : HasFPowerSeriesOnBall (𝕜 := ℂ) (F := ℂ) (fun (z : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (z - w) 2)
  (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
    HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HPow.hPow (β := ℤ) (w - x) (-(↑(i + 2) : ℤ)))
  x ‖w - x‖ₑ
Tactic: refine .sub ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
w x : ℂ
hw : w ≠ x
refine_1 :
  HasFPowerSeriesOnBall (𝕜 := ℂ) (F := ℂ) (fun (z : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (z - w) 2)
    (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
      HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HPow.hPow (β := ℤ) (w - x) (-(↑(i + 2) : ℤ)))
    x ‖w - x‖ₑ
⊢ HasFPowerSeriesOnBall
    (HSub.hSub (α := (i : ℂ) → ℂ) (fun (z : ℂ) ↦ 1 / HPow.hPow (β := ℕ) (z - w) 2) fun (z : ℂ) ↦
      1 / HPow.hPow (β := ℕ) w 2)
    (HSub.hSub (α := FormalMultilinearSeries ℂ ℂ ℂ) (β := FormalMultilinearSeries ℂ ℂ ℂ)
      (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
          HAdd.hAdd (α := ℂ) (↑i : ℂ) 1 * HPow.hPow (β := ℤ) (w - x) (-(↑(i + 2) : ℤ)) :
        FormalMultilinearSeries ℂ ℂ ℂ)
      (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
          Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) w (-2)) 0 :
        FormalMultilinearSeries ℂ ℂ ℂ))
    x ‖w - x‖ₑ
have refine_2 : HasFPowerSeriesOnBall (𝕜 := ℂ) (F := ℂ) (fun (z : ℂ) ↦ 1 / HPow.hPow (β := ℕ) w 2)
  (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) w (-2)) 0)
  x ‖w - x‖ₑ
Tactic: refine .sub ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
w x : ℂ
hw : w ≠ x
⊢ HasFPowerSeriesOnBall (𝕜 := ℂ) (F := ℂ) (fun (z : ℂ) ↦ 1 / HPow.hPow (β := ℕ) w 2)
    (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
      Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) w (-2)) 0)
    x ‖w - x‖ₑ
have h : Eq (α := FormalMultilinearSeries ℂ ℂ ℂ)
  (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
      Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) w (-2)) 0 :
    FormalMultilinearSeries ℂ ℂ ℂ)
  (constFormalMultilinearSeries ℂ ℂ (1 / HPow.hPow (β := ℕ) w 2) : FormalMultilinearSeries ℂ ℂ ℂ)
Tactic: convert! hasFPowerSeriesOnBall_const.mono _ le_top
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
w x : ℂ
hw : w ≠ x
h :
  Eq (α := FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
        Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) w (-2)) 0 :
      FormalMultilinearSeries ℂ ℂ ℂ)
    (constFormalMultilinearSeries ℂ ℂ (1 / HPow.hPow (β := ℕ) w 2) : FormalMultilinearSeries ℂ ℂ ℂ)
⊢ HasFPowerSeriesOnBall (𝕜 := ℂ) (F := ℂ) (fun (z : ℂ) ↦ 1 / HPow.hPow (β := ℕ) w 2)
    (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
      Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) w (-2)) 0)
    x ‖w - x‖ₑ
have refine_2 : 0 < ‖w - x‖ₑ
Tactic: convert! hasFPowerSeriesOnBall_const.mono _ le_top
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
w x : ℂ
hw : w ≠ x
⊢ Eq (α := FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
        Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) w (-2)) 0 :
      FormalMultilinearSeries ℂ ℂ ℂ)
    (constFormalMultilinearSeries ℂ ℂ (1 / HPow.hPow (β := ℕ) w 2) : FormalMultilinearSeries ℂ ℂ ℂ)
have h : Eq (α := ℂ)
  ((FormalMultilinearSeries.ofScalars ℂ
          (fun (i : ℕ) ↦ Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) w (-2)) 0) 0 :
        (a : (i : Fin 0) → ℂ) → ℂ)
      fun (x : Fin 0) ↦ 1 :
    ℂ)
  ((constFormalMultilinearSeries ℂ ℂ (1 / HPow.hPow (β := ℕ) w 2) 0 : (a : (i : Fin 0) → ℂ) → ℂ) fun (x : Fin 0) ↦ 1 :
    ℂ)
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
w x : ℂ
hw : w ≠ x
h :
  Eq (α := ℂ)
    ((FormalMultilinearSeries.ofScalars ℂ
            (fun (i : ℕ) ↦ Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) w (-2)) 0) 0 :
          (a : (i : Fin 0) → ℂ) → ℂ)
        fun (x : Fin 0) ↦ 1 :
      ℂ)
    ((constFormalMultilinearSeries ℂ ℂ (1 / HPow.hPow (β := ℕ) w 2) 0 : (a : (i : Fin 0) → ℂ) → ℂ) fun (x : Fin 0) ↦ 1 :
      ℂ)
⊢ Eq (α := FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.ofScalars ℂ fun (i : ℕ) ↦
        Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) w (-2)) 0 :
      FormalMultilinearSeries ℂ ℂ ℂ)
    (constFormalMultilinearSeries ℂ ℂ (1 / HPow.hPow (β := ℕ) w 2) : FormalMultilinearSeries ℂ ℂ ℂ)
have h₁ : ∀ (n : ℕ),
  Eq (α := ℂ)
    ((FormalMultilinearSeries.ofScalars ℂ
            (fun (i : ℕ) ↦ Nat.casesOn (motive := fun (x : ℕ) ↦ ℂ) i (HPow.hPow (β := ℤ) w (-2)) 0) (n + 1) :
          (a : (i : Fin (n + 1)) → ℂ) → ℂ)
        fun (x : Fin (n + 1)) ↦ 1 :
      ℂ)
    ((constFormalMultilinearSeries ℂ ℂ (1 / HPow.hPow (β := ℕ) w 2) (n + 1) : (a : (i : Fin (n + 1)) → ℂ) → ℂ)
        fun (x : Fin (n + 1)) ↦ 1 :
      ℂ)
Tactic: ext (_ | _)