awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (hypothesis)
Goal:
a : ℂ
this :
  Eq (α := FormalMultilinearSeries ℂ ℂ ℂ) (binomialSeries ℂ a : FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦
        HDiv.hDiv (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0) (↑n ! : ℂ) :
      FormalMultilinearSeries ℂ ℂ ℂ)
z : ℂ
hz : Membership.mem (γ := Set ℂ) (Metric.eball 0 1) z
⊢ norm (E := ℂ) ((fun (x : ℂ) ↦ x) z) < 1
have hz₁ : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) z
Tactic: rw [← ENNReal.ofReal_one, Metric.eball_ofReal] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a : ℂ
this :
  Eq (α := FormalMultilinearSeries ℂ ℂ ℂ) (binomialSeries ℂ a : FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦
        HDiv.hDiv (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0) (↑n ! : ℂ) :
      FormalMultilinearSeries ℂ ℂ ℂ)
⊢ 1 ≤
    FormalMultilinearSeries.radius (𝕜 := ℂ) (E := ℂ) (F := ℂ)
      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦
        HDiv.hDiv (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0) (↑n ! : ℂ))
have convert_8 : 1 ≤ FormalMultilinearSeries.radius (binomialSeries ℂ a)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a : ℂ
⊢ HasFPowerSeriesOnBall (fun (x : ℂ) ↦ (1 + x) ^ a) (binomialSeries ℂ a) 0 1
have suffices : Eq (α := FormalMultilinearSeries ℂ ℂ ℂ) (binomialSeries ℂ a : FormalMultilinearSeries ℂ ℂ ℂ)
  (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦
      HDiv.hDiv (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0) (↑n ! : ℂ) :
    FormalMultilinearSeries ℂ ℂ ℂ)
Tactic: suffices (binomialSeries ℂ a = FormalMultilinearSeries.ofScalars ℂ
      fun n ↦ iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0 / n !) by
    convert! AnalyticOn.hasFPowerSeriesOnSubball _ _ _
    · norm_num
    · -- TODO: use `fun_prop` for this subgoal
      apply AnalyticOn.cpow (analyticOn_const.add analyticOn_id) analyticOn_const
      intro z hz
      apply Complex.mem_slitPlane_of_norm_lt_one
      rw [← ENNReal.ofReal_one, Metric.eball_ofReal] at hz
      simpa using hz
    · rw [← this]
      exact binomialSeries_radius_ge_one
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a : ℂ
⊢ Eq (α := FormalMultilinearSeries ℂ ℂ ℂ) (binomialSeries ℂ a : FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦
        HDiv.hDiv (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0) (↑n ! : ℂ) :
      FormalMultilinearSeries ℂ ℂ ℂ)
have simp : Eq (α := ℕ → ℂ) (fun (x : ℕ) ↦ Ring.choose a x) fun (n : ℕ) ↦
  HDiv.hDiv (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0) (↑n ! : ℂ)
Tactic: simp only [binomialSeries, FormalMultilinearSeries.ofScalars_series_eq_iff]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a : ℂ
⊢ Eq (α := ℕ → ℂ) (fun (x : ℕ) ↦ Ring.choose a x) fun (n : ℕ) ↦
    HDiv.hDiv (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0) (↑n ! : ℂ)
have h : ∀ (n : ℕ), Ring.choose a n = HDiv.hDiv (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0) (↑n ! : ℂ)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a : ℂ
n : ℕ
⊢ Ring.choose a n = HDiv.hDiv (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0) (↑n ! : ℂ)
have h : Polynomial.smeval (descPochhammer ℤ n) a = iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0
Tactic: rw [eq_div_iff_mul_eq (by simp [Nat.factorial_ne_zero]), ← nsmul_eq_mul',
    ← Ring.descPochhammer_eq_factorial_smul_choose]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (hypothesis)
Goal:
a : ℂ
n : ℕ
B : Set ℂ := Metric.ball 0 1
this :
  Set.EqOn (β := ℂ) (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) B
⊢ Polynomial.smeval (descPochhammer ℤ n) a = iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0
have this₁ : Eq (α := ℂ) (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B 0)
  ((fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) 0)
Tactic: specialize this (show 0 ∈ _ by simp [B])
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (hypothesis)
Goal:
a : ℂ
n : ℕ
B : Set ℂ := Metric.ball 0 1
this :
  Eq (α := ℂ) (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B 0)
    ((fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) 0)
⊢ Polynomial.smeval (descPochhammer ℤ n) a = iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0
have this₁ : Eq (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0)
  ((fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) 0)
Tactic: rw [iteratedDerivWithin_of_isOpen Metric.isOpen_ball (by simp)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a : ℂ
n : ℕ
B : Set ℂ := Metric.ball 0 1
this :
  Eq (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0)
    ((fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) 0)
⊢ Polynomial.smeval (descPochhammer ℤ n) a = iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0
have symm : iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0 = Polynomial.smeval (descPochhammer ℤ n) a
Tactic: symm
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a : ℂ
n : ℕ
B : Set ℂ := Metric.ball 0 1
⊢ Polynomial.smeval (descPochhammer ℤ n) a = iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0
have h : Set.EqOn (β := ℂ) (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B)
  (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) B
Tactic: suffices Set.EqOn (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B)
      (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - n)) B by
    specialize this (show 0 ∈ _ by simp [B])
    rw [iteratedDerivWithin_of_isOpen Metric.isOpen_ball (by simp)] at this
    symm
    simpa using this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a : ℂ
B : Set ℂ := Metric.ball 0 1
n : ℕ
ih :
  Set.EqOn (β := ℂ) (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) B
⊢ Eq (α := (x : ℂ) → ℂ) (iteratedDerivWithin (n + 1) (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B)
have h : ∀ (z : ℂ),
  Eq (α := ℂ) (iteratedDerivWithin (n + 1) (fun (x : ℂ) ↦ (1 + x) ^ a) B z)
    (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B z)
Tactic: ext z
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a : ℂ
B : Set ℂ := Metric.ball 0 1
n : ℕ
ih :
  Set.EqOn (β := ℂ) (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) B
z : ℂ
⊢ Eq (α := ℂ) (iteratedDerivWithin (n + 1) (fun (x : ℂ) ↦ (1 + x) ^ a) B z)
    (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B z)
have h : Eq (α := ℂ) (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B z)
  (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B z)
Tactic: rw [iteratedDerivWithin_succ]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (hypothesis)
Goal:
a : ℂ
B : Set ℂ := Metric.ball 0 1
n : ℕ
ih :
  Set.EqOn (β := ℂ) (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) B
⊢ Set.EqOn (β := ℂ) (iteratedDerivWithin (n + 1) (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ (n + 1)) a * (1 + x) ^ (a - (↑(n + 1) : ℂ))) B
have this : Eq (α := (x : ℂ) → ℂ) (iteratedDerivWithin (n + 1) (fun (x : ℂ) ↦ (1 + x) ^ a) B)
  (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B)
Tactic: have : iteratedDerivWithin (n + 1) (fun (x : ℂ) ↦ (1 + x) ^ a) B =
        derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B := by
      ext z
      rw [iteratedDerivWithin_succ]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a : ℂ
B : Set ℂ := Metric.ball 0 1
n : ℕ
ih :
  Set.EqOn (β := ℂ) (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) B
this :
  Eq (α := (x : ℂ) → ℂ) (iteratedDerivWithin (n + 1) (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B)
⊢ Set.EqOn (β := ℂ) (iteratedDerivWithin (n + 1) (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ (n + 1)) a * (1 + x) ^ (a - (↑(n + 1) : ℂ))) B
have h : Set.EqOn (β := ℂ) (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B)
  (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ (n + 1)) a * (1 + x) ^ (a - (↑(n + 1) : ℂ))) B
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a : ℂ
B : Set ℂ := Metric.ball 0 1
n : ℕ
ih :
  Set.EqOn (β := ℂ) (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) B
this :
  Eq (α := (x : ℂ) → ℂ) (iteratedDerivWithin (n + 1) (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B)
z : ℂ
hz : z ∈ B
⊢ Eq (α := ℂ) (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B z)
    (derivWithin (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) B z)
have rw : Eq (α := ℂ)
  (derivWithin (fun (x : ℂ) ↦ (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) x) B
    z)
  (derivWithin (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) B z)
Tactic: rw [derivWithin_congr (fun _ hz ↦ ih hz) (ih hz)]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (hypothesis)
Goal:
a : ℂ
B : Set ℂ := Metric.ball 0 1
n : ℕ
ih :
  Set.EqOn (β := ℂ) (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) B
this :
  Eq (α := (x : ℂ) → ℂ) (iteratedDerivWithin (n + 1) (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B)
⊢ Set.EqOn (β := ℂ) (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B)
    (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ (n + 1)) a * (1 + x) ^ (a - (↑(n + 1) : ℂ))) B
have this₁ : Set.EqOn (β := ℂ) (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B)
  (derivWithin (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) B) B
Tactic: have : Set.EqOn (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B)
        (derivWithin (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n)) B) B := by
      intro z hz
      rw [derivWithin_congr (fun _ hz ↦ ih hz) (ih hz)]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a : ℂ
B : Set ℂ := Metric.ball 0 1
n : ℕ
ih :
  Set.EqOn (β := ℂ) (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) B
this_1 :
  Eq (α := (x : ℂ) → ℂ) (iteratedDerivWithin (n + 1) (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B)
this :
  Set.EqOn (β := ℂ) (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B)
    (derivWithin (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) B) B
⊢ Set.EqOn (β := ℂ) (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B)
    (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ (n + 1)) a * (1 + x) ^ (a - (↑(n + 1) : ℂ))) B
have h : Set.EqOn (β := ℂ) (derivWithin (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) B)
  (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ (n + 1)) a * (1 + x) ^ (a - (↑(n + 1) : ℂ))) B
Tactic: apply Set.EqOn.trans this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a : ℂ
B : Set ℂ := Metric.ball 0 1
n : ℕ
ih :
  Set.EqOn (β := ℂ) (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) B
this_1 :
  Eq (α := (x : ℂ) → ℂ) (iteratedDerivWithin (n + 1) (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B)
this :
  Set.EqOn (β := ℂ) (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B)
    (derivWithin (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) B) B
z : ℂ
hz : z ∈ B
⊢ Eq (α := ℂ) (derivWithin (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) B z)
    ((fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ (n + 1)) a * (1 + x) ^ (a - (↑(n + 1) : ℂ))) z)
have h : Polynomial.smeval (descPochhammer ℤ n) a * deriv (fun (x : ℂ) ↦ (1 + x) ^ (a - (↑n : ℂ))) z =
  Polynomial.smeval (descPochhammer ℤ (n + 1)) a * (1 + z) ^ (a - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
Tactic: simp only [Nat.cast_add, Nat.cast_one, B, derivWithin_of_isOpen Metric.isOpen_ball hz,
      deriv_const_mul_field']
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a : ℂ
B : Set ℂ := Metric.ball 0 1
n : ℕ
ih :
  Set.EqOn (β := ℂ) (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) B
this_1 :
  Eq (α := (x : ℂ) → ℂ) (iteratedDerivWithin (n + 1) (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B)
this :
  Set.EqOn (β := ℂ) (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B)
    (derivWithin (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) B) B
z : ℂ
hz : z ∈ B
⊢ Polynomial.smeval (descPochhammer ℤ n) a * deriv (fun (x : ℂ) ↦ (1 + x) ^ (a - (↑n : ℂ))) z =
    Polynomial.smeval (descPochhammer ℤ (n + 1)) a * (1 + z) ^ (a - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
have h : Polynomial.smeval (descPochhammer ℤ n) a * (a - (↑n : ℂ)) * (1 + z) ^ (a - (↑n : ℂ) - 1) =
  Polynomial.smeval (descPochhammer ℤ (n + 1)) a * (1 + z) ^ (a - (↑n : ℂ) - 1)
Tactic: rw [_root_.deriv_cpow_const (by fun_prop), deriv_const_add_id, mul_one,
      show a - (n + 1) = a - n - 1 by ring, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a : ℂ
B : Set ℂ := Metric.ball 0 1
n : ℕ
ih :
  Set.EqOn (β := ℂ) (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) B
this_1 :
  Eq (α := (x : ℂ) → ℂ) (iteratedDerivWithin (n + 1) (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B)
this :
  Set.EqOn (β := ℂ) (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B)
    (derivWithin (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) B) B
z : ℂ
hz : z ∈ B
h :
  Polynomial.smeval (descPochhammer ℤ n) a * (a - (↑n : ℂ)) * (1 + z) ^ (a - (↑n : ℂ) - 1) =
    Polynomial.smeval (descPochhammer ℤ (n + 1)) a * (1 + z) ^ (a - (↑n : ℂ) - 1)
⊢ Polynomial.smeval (descPochhammer ℤ n) a * deriv (fun (x : ℂ) ↦ (1 + x) ^ (a - (↑n : ℂ))) z =
    Polynomial.smeval (descPochhammer ℤ (n + 1)) a * (1 + z) ^ (a - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
have h₁ : 1 + z ∈ slitPlane
Tactic: rw [_root_.deriv_cpow_const (by fun_prop), deriv_const_add_id, mul_one,
      show a - (n + 1) = a - n - 1 by ring, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a : ℂ
B : Set ℂ := Metric.ball 0 1
n : ℕ
ih :
  Set.EqOn (β := ℂ) (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) B
this_1 :
  Eq (α := (x : ℂ) → ℂ) (iteratedDerivWithin (n + 1) (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B)
this :
  Set.EqOn (β := ℂ) (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B)
    (derivWithin (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) B) B
z : ℂ
hz : z ∈ B
⊢ Polynomial.smeval (descPochhammer ℤ n) a * (a - (↑n : ℂ)) * (1 + z) ^ (a - (↑n : ℂ) - 1) =
    Polynomial.smeval (descPochhammer ℤ (n + 1)) a * (1 + z) ^ (a - (↑n : ℂ) - 1)
have h : Polynomial.smeval (descPochhammer ℤ n) a * (a - (↑n : ℂ)) = Polynomial.smeval (descPochhammer ℤ (n + 1)) a
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a : ℂ
B : Set ℂ := Metric.ball 0 1
n : ℕ
ih :
  Set.EqOn (β := ℂ) (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) B
this_1 :
  Eq (α := (x : ℂ) → ℂ) (iteratedDerivWithin (n + 1) (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B)
this :
  Set.EqOn (β := ℂ) (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B)
    (derivWithin (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) B) B
z : ℂ
hz : z ∈ B
⊢ 1 + z ∈ slitPlane
have h : ‖z‖ < 1
Tactic: apply Complex.mem_slitPlane_of_norm_lt_one
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a : ℂ
n : ℕ
B : Set ℂ := Metric.ball 0 1
⊢ Set.EqOn (β := ℂ) (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) B
have h : Set.EqOn (β := ℂ) (iteratedDerivWithin 0 (fun (x : ℂ) ↦ (1 + x) ^ a) B)
  (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ 0) a * (1 + x) ^ (a - (↑0 : ℂ))) B
Tactic: induction n with
  | zero => simp [Set.EqOn]
  | succ n ih =>
    have : iteratedDerivWithin (n + 1) (fun (x : ℂ) ↦ (1 + x) ^ a) B =
        derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B := by
      ext z
      rw [iteratedDerivWithin_succ]
    rw [this]
    have : Set.EqOn (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B)
        (derivWithin (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n)) B) B := by
      intro z hz
      rw [derivWithin_congr (fun _ hz ↦ ih hz) (ih hz)]
    apply Set.EqOn.trans this
    intro z hz
    simp only [Nat.cast_add, Nat.cast_one, B, derivWithin_of_isOpen Metric.isOpen_ball hz,
      deriv_const_mul_field']
    rw [_root_.deriv_cpow_const (by fun_prop), deriv_const_add_id, mul_one,
      show a - (n + 1) = a - n - 1 by ring, ← mul_assoc]
    · congr
      simp [descPochhammer_succ_right, Polynomial.smeval_mul, Polynomial.smeval_natCast]
    · apply Complex.mem_slitPlane_of_norm_lt_one
      simpa [B] using hz
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a : ℂ
n : ℕ
B : Set ℂ := Metric.ball 0 1
h :
  Set.EqOn (β := ℂ) (iteratedDerivWithin 0 (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ 0) a * (1 + x) ^ (a - (↑0 : ℂ))) B
⊢ Set.EqOn (β := ℂ) (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) B
have h₁ : ∀ (n : ℕ)
  (ih :
    Set.EqOn (β := ℂ) (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B)
      (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) B),
  Set.EqOn (β := ℂ) (iteratedDerivWithin (n + 1) (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ (n + 1)) a * (1 + x) ^ (a - (↑(n + 1) : ℂ))) B
Tactic: induction n with
  | zero => simp [Set.EqOn]
  | succ n ih =>
    have : iteratedDerivWithin (n + 1) (fun (x : ℂ) ↦ (1 + x) ^ a) B =
        derivWithin (iteratedDerivWithin n (fun x ↦ (1 + x) ^ a) B) B := by
      ext z
      rw [iteratedDerivWithin_succ]
    rw [this]
    have : Set.EqOn (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B)
        (derivWithin (fun x ↦ (descPochhammer ℤ n).smeval a * (1 + x) ^ (a - ↑n)) B) B := by
      intro z hz
      rw [derivWithin_congr (fun _ hz ↦ ih hz) (ih hz)]
    apply Set.EqOn.trans this
    intro z hz
    simp only [Nat.cast_add, Nat.cast_one, B, derivWithin_of_isOpen Metric.isOpen_ball hz,
      deriv_const_mul_field']
    rw [_root_.deriv_cpow_const (by fun_prop), deriv_const_add_id, mul_one,
      show a - (n + 1) = a - n - 1 by ring, ← mul_assoc]
    · congr
      simp [descPochhammer_succ_right, Polynomial.smeval_mul, Polynomial.smeval_natCast]
    · apply Complex.mem_slitPlane_of_norm_lt_one
      simpa [B] using hz
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a : ℂ
⊢ Eq (α := FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.compContinuousLinearMap (binomialSeries ℂ (-a) : FormalMultilinearSeries ℂ ℂ ℂ) (-1) :
      FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ Ring.choose (a + (↑n : ℂ) - 1) n : FormalMultilinearSeries ℂ ℂ ℂ)
have h : ∀ (n : ℕ),
  Eq (α := ℂ)
    ((FormalMultilinearSeries.compContinuousLinearMap (binomialSeries ℂ (-a) : FormalMultilinearSeries ℂ ℂ ℂ) (-1) n :
          (a : (i : Fin n) → ℂ) → ℂ)
        fun (x : Fin n) ↦ 1 :
      ℂ)
    ((FormalMultilinearSeries.ofScalars ℂ (fun (n : ℕ) ↦ Ring.choose (a + (↑n : ℂ) - 1) n) n :
          (a : (i : Fin n) → ℂ) → ℂ)
        fun (x : Fin n) ↦ 1 :
      ℂ)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (hypothesis)
Goal:
a : ℂ
⊢ HasFPowerSeriesOnBall (𝕜 := ℂ) (F := ℂ) (fun (x : ℂ) ↦ 1 / (1 - x) ^ a)
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ Ring.choose (a + (↑n : ℂ) - 1) n) 0 1
have H : Eq (α := FormalMultilinearSeries ℂ ℂ ℂ)
  (FormalMultilinearSeries.compContinuousLinearMap (binomialSeries ℂ (-a) : FormalMultilinearSeries ℂ ℂ ℂ) (-1) :
    FormalMultilinearSeries ℂ ℂ ℂ)
  (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ Ring.choose (a + (↑n : ℂ) - 1) n : FormalMultilinearSeries ℂ ℂ ℂ)
Tactic: have H : ((binomialSeries ℂ (-a)).compContinuousLinearMap (-1)) =
      .ofScalars ℂ fun n ↦ Ring.choose (a + n - 1) n := by
    ext n; simp [FormalMultilinearSeries.compContinuousLinearMap, binomialSeries, Ring.choose_neg,
      Units.smul_def, ← pow_add, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (hypothesis)
Goal:
a : ℂ
H :
  Eq (α := FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.compContinuousLinearMap (binomialSeries ℂ (-a) : FormalMultilinearSeries ℂ ℂ ℂ) (-1) :
      FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ Ring.choose (a + (↑n : ℂ) - 1) n : FormalMultilinearSeries ℂ ℂ ℂ)
⊢ HasFPowerSeriesOnBall (𝕜 := ℂ) (F := ℂ) (fun (x : ℂ) ↦ 1 / (1 - x) ^ a)
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ Ring.choose (a + (↑n : ℂ) - 1) n) 0 1
have this : HasFPowerSeriesOnBall (fun (x : ℂ) ↦ (1 + x) ^ (-a)) (binomialSeries ℂ (-a)) (-0) 1
Tactic: have : HasFPowerSeriesOnBall (fun x ↦ (1 + x) ^ (-a)) (binomialSeries ℂ (-a : ℂ)) (-0) 1 := by
    simpa using one_add_cpow_hasFPowerSeriesOnBall_zero
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a : ℕ
⊢ HasFPowerSeriesOnBall (𝕜 := ℂ) (F := ℂ) (fun (x : ℂ) ↦ 1 / (1 - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (↑((a + n).choose a) : ℂ)) 0 1
have h : ∀ (z : ℂ), (1 - z) ^ (a + 1) = (1 - z) ^ HAdd.hAdd (α := ℂ) (↑a : ℂ) 1
Tactic: convert! one_div_one_sub_cpow_hasFPowerSeriesOnBall_zero (a + 1) using 3 with z n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a : ℕ
h : ∀ (z : ℂ), (1 - z) ^ (a + 1) = (1 - z) ^ HAdd.hAdd (α := ℂ) (↑a : ℂ) 1
⊢ HasFPowerSeriesOnBall (𝕜 := ℂ) (F := ℂ) (fun (x : ℂ) ↦ 1 / (1 - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ (↑((a + n).choose a) : ℂ)) 0 1
have h₁ : ∀ (n : ℕ), (↑((a + n).choose a) : ℂ) = Ring.choose (HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 + (↑n : ℂ) - 1) n
Tactic: convert! one_div_one_sub_cpow_hasFPowerSeriesOnBall_zero (a + 1) using 3 with z n