awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℂ
simp :
  Eq (α := ℕ → ℂ) (fun (x : ℕ) ↦ Ring.choose a x) fun (n : ℕ) ↦
    HDiv.hDiv (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0) (↑n ! : ℂ)
⊢ Eq (α := FormalMultilinearSeries ℂ ℂ ℂ) (binomialSeries ℂ a : FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦
        HDiv.hDiv (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0) (↑n ! : ℂ) :
      FormalMultilinearSeries ℂ ℂ ℂ)

Tactic:
simp only [binomialSeries, FormalMultilinearSeries.ofScalars_series_eq_iff]

Premises used: FormalMultilinearSeries.ofScalars_series_eq_iff, binomialSeries
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℂ
h : ∀ (n : ℕ), Ring.choose a n = HDiv.hDiv (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0) (↑n ! : ℂ)
⊢ Eq (α := ℕ → ℂ) (fun (x : ℕ) ↦ Ring.choose a x) fun (n : ℕ) ↦
    HDiv.hDiv (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0) (↑n ! : ℂ)

Tactic:
ext n
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℂ
n : ℕ
⊢ Ne (α := ℂ) (↑n ! : ℂ) 0

Tactic:
simp [Nat.factorial_ne_zero]

Premises used: Nat.factorial_ne_zero
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℂ
n : ℕ
h : Polynomial.smeval (descPochhammer ℤ n) a = iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0
⊢ Ring.choose a n = HDiv.hDiv (α := ℂ) (iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0) (↑n ! : ℂ)

Tactic:
rw [eq_div_iff_mul_eq (by simp [Nat.factorial_ne_zero]), ← nsmul_eq_mul',
    ← Ring.descPochhammer_eq_factorial_smul_choose]

Premises used: nsmul_eq_mul', eq_div_iff_mul_eq, Ring.descPochhammer_eq_factorial_smul_choose
-- Module: Mathlib.Analysis.Analytic.Binomial
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
⊢ 0 ∈ B

Tactic:
simp [B]
-- Module: Mathlib.Analysis.Analytic.Binomial
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
⊢ 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])
-- Module: Mathlib.Analysis.Analytic.Binomial
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)
⊢ Membership.mem (γ := Set ℂ) (Metric.ball 0 1) 0

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Binomial
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)
⊢ 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

Premises used: Metric.isOpen_ball, iteratedDerivWithin_of_isOpen
-- Module: Mathlib.Analysis.Analytic.Binomial
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)
symm : iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0 = Polynomial.smeval (descPochhammer ℤ n) a
⊢ Polynomial.smeval (descPochhammer ℤ n) a = iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0

Tactic:
symm
-- Module: Mathlib.Analysis.Analytic.Binomial
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)
⊢ iteratedDeriv n (fun (x : ℂ) ↦ (1 + x) ^ a) 0 = Polynomial.smeval (descPochhammer ℤ n) a

Tactic:
simpa using this
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℂ
n : ℕ
B : Set ℂ := Metric.ball 0 1
h :
  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

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
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℂ
B : Set ℂ := Metric.ball 0 1
⊢ Set.EqOn (β := ℂ) (iteratedDerivWithin 0 (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ 0) a * (1 + x) ^ (a - (↑0 : ℂ))) B

Tactic:
simp [Set.EqOn]

Premises used: Set.EqOn
-- Module: Mathlib.Analysis.Analytic.Binomial
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
h :
  ∀ (z : ℂ),
    Eq (α := ℂ) (iteratedDerivWithin (n + 1) (fun (x : ℂ) ↦ (1 + x) ^ a) B z)
      (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B z)
⊢ Eq (α := (x : ℂ) → ℂ) (iteratedDerivWithin (n + 1) (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B)

Tactic:
ext z
-- Module: Mathlib.Analysis.Analytic.Binomial
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 : ℂ
h h₁ :
  Eq (α := ℂ) (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B z)
    (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B z)
⊢ Eq (α := ℂ) (iteratedDerivWithin (n + 1) (fun (x : ℂ) ↦ (1 + x) ^ a) B z)
    (derivWithin (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B) B z)

Tactic:
rw [iteratedDerivWithin_succ]

Premises used: iteratedDerivWithin_succ
-- Module: Mathlib.Analysis.Analytic.Binomial
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)

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]
-- Module: Mathlib.Analysis.Analytic.Binomial
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)
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
⊢ 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:
rw [this]
-- Module: Mathlib.Analysis.Analytic.Binomial
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
rw 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)
⊢ 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)

Tactic:
rw [derivWithin_congr (fun _ hz ↦ ih hz) (ih hz)]

Premises used: derivWithin_congr
-- Module: Mathlib.Analysis.Analytic.Binomial
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)
    (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)]
-- Module: Mathlib.Analysis.Analytic.Binomial
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
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
⊢ 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:
apply Set.EqOn.trans this

Premises used: Set.EqOn.trans
-- Module: Mathlib.Analysis.Analytic.Binomial
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 * deriv (fun (x : ℂ) ↦ (1 + x) ^ (a - (↑n : ℂ))) z =
    Polynomial.smeval (descPochhammer ℤ (n + 1)) a * (1 + z) ^ (a - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1)
⊢ 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)

Tactic:
simp only [Nat.cast_add, Nat.cast_one, B, derivWithin_of_isOpen Metric.isOpen_ball hz,
      deriv_const_mul_field']

Premises used: deriv_const_mul_field', Nat.cast_add, Metric.isOpen_ball, derivWithin_of_isOpen, Nat.cast_one
-- Module: Mathlib.Analysis.Analytic.Binomial
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
⊢ DifferentiableAt ℂ (HAdd.hAdd (α := ℂ) 1) z

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Analytic.Binomial
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
⊢ a - HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 = a - (↑n : ℂ) - 1

Tactic:
ring
-- Module: Mathlib.Analysis.Analytic.Binomial
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)
h₁ : 1 + z ∈ slitPlane
⊢ 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:
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]

Premises used: deriv_cpow_const, deriv_const_add_id, mul_assoc, mul_one
-- Module: Mathlib.Analysis.Analytic.Binomial
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 : ℂ)) = Polynomial.smeval (descPochhammer ℤ (n + 1)) a
⊢ Polynomial.smeval (descPochhammer ℤ n) a * (a - (↑n : ℂ)) * (1 + z) ^ (a - (↑n : ℂ) - 1) =
    Polynomial.smeval (descPochhammer ℤ (n + 1)) a * (1 + z) ^ (a - (↑n : ℂ) - 1)

Tactic:
congr
-- Module: Mathlib.Analysis.Analytic.Binomial
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 : ℂ)) = Polynomial.smeval (descPochhammer ℤ (n + 1)) a

Tactic:
simp [descPochhammer_succ_right, Polynomial.smeval_mul, Polynomial.smeval_natCast]

Premises used: descPochhammer_succ_right, Polynomial.smeval_natCast, Polynomial.smeval_mul
-- Module: Mathlib.Analysis.Analytic.Binomial
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 : ‖z‖ < 1
⊢ 1 + z ∈ slitPlane

Tactic:
apply Complex.mem_slitPlane_of_norm_lt_one

Premises used: Complex.mem_slitPlane_of_norm_lt_one
-- Module: Mathlib.Analysis.Analytic.Binomial
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
⊢ ‖z‖ < 1

Tactic:
simpa [B] using hz
-- Module: Mathlib.Analysis.Analytic.Binomial
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
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
⊢ Set.EqOn (β := ℂ) (iteratedDerivWithin n (fun (x : ℂ) ↦ (1 + x) ^ a) B)
    (fun (x : ℂ) ↦ Polynomial.smeval (descPochhammer ℤ n) a * (1 + x) ^ (a - (↑n : ℂ))) 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

Premises used: deriv_cpow_const, deriv_const_add_id, mul_assoc, deriv_const_mul_field', descPochhammer_succ_right, Polynomial.smeval_natCast, Polynomial.smeval_mul, Set.EqOn, Nat.cast_add, Complex.mem_slitPlane_of_norm_lt_one, mul_one, Nat.cast_one
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℂ
⊢ HasFPowerSeriesAt (fun (x : ℂ) ↦ (1 + x) ^ a) (binomialSeries ℂ a) 0

Tactic:
one_add_cpow_hasFPowerSeriesOnBall_zero.hasFPowerSeriesAt

Premises used: HasFPowerSeriesOnBall.hasFPowerSeriesAt, Complex.one_add_cpow_hasFPowerSeriesOnBall_zero
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℂ
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 :
        ℂ)
⊢ Eq (α := FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.compContinuousLinearMap (binomialSeries ℂ (-a) : FormalMultilinearSeries ℂ ℂ ℂ) (-1) :
      FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ Ring.choose (a + (↑n : ℂ) - 1) n : FormalMultilinearSeries ℂ ℂ ℂ)

Tactic:
ext n
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℂ
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:
simp [FormalMultilinearSeries.compContinuousLinearMap, binomialSeries, Ring.choose_neg,
      Units.smul_def, ← pow_add, ← mul_assoc]

Premises used: mul_assoc, Ring.choose_neg, FormalMultilinearSeries.compContinuousLinearMap, pow_add, binomialSeries, Units.smul_def
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℂ
⊢ 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]
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℂ
H :
  Eq (α := FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.compContinuousLinearMap (binomialSeries ℂ (-a) : FormalMultilinearSeries ℂ ℂ ℂ) (-1) :
      FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ Ring.choose (a + (↑n : ℂ) - 1) n : FormalMultilinearSeries ℂ ℂ ℂ)
⊢ HasFPowerSeriesOnBall (fun (x : ℂ) ↦ (1 + x) ^ (-a)) (binomialSeries ℂ (-a)) (-0) 1

Tactic:
simpa using one_add_cpow_hasFPowerSeriesOnBall_zero

Premises used: Complex.one_add_cpow_hasFPowerSeriesOnBall_zero
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℂ
H :
  Eq (α := FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.compContinuousLinearMap (binomialSeries ℂ (-a) : FormalMultilinearSeries ℂ ℂ ℂ) (-1) :
      FormalMultilinearSeries ℂ ℂ ℂ)
    (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ Ring.choose (a + (↑n : ℂ) - 1) n : FormalMultilinearSeries ℂ ℂ ℂ)
⊢ 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