awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Binomial
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‖ₑ
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‖ₑ
⊢ 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:
refine .sub ?_ ?_
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
w x : ℂ
hw : w ≠ x
⊢ w - x ≠ 0

Tactic:
simp [sub_eq_zero, hw]

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
w x : ℂ
hw : w ≠ x
⊢ 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:
simpa only [sub_sub_sub_cancel_right, zero_add, sub_sq_comm w, zpow_neg, zpow_natCast, mul_comm]
      using (one_div_sub_sq_hasFPowerSeriesOnBall_zero
        (z := w - x) (by simp [sub_eq_zero, hw])).comp_sub x

Premises used: zpow_natCast, sub_sub_sub_cancel_right, HasFPowerSeriesOnBall.comp_sub, sub_sq_comm, Complex.one_div_sub_sq_hasFPowerSeriesOnBall_zero, zero_add, zpow_neg, mul_comm
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
w x : ℂ
hw : w ≠ x
⊢ HasFPowerSeriesOnBall (fun (x : ℂ) ↦ 1 / HPow.hPow (β := ℕ) w 2)
    (constFormalMultilinearSeries ℂ ℂ (1 / HPow.hPow (β := ℕ) w 2)) x ‖w - x‖ₑ

Tactic:
hasFPowerSeriesOnBall_const.mono _ le_top

Premises used: hasFPowerSeriesOnBall_const, le_top, HasFPowerSeriesOnBall.mono
-- Module: Mathlib.Analysis.Analytic.Binomial
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 ℂ ℂ ℂ)
refine_2 : 0 < ‖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‖ₑ

Tactic:
convert! hasFPowerSeriesOnBall_const.mono _ le_top

Premises used: hasFPowerSeriesOnBall_const, le_top, HasFPowerSeriesOnBall.mono
-- Module: Mathlib.Analysis.Analytic.Binomial
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 :
      ℂ)
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 :
        ℂ)
⊢ 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:
ext (_ | _)
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
w x : ℂ
hw : w ≠ x
⊢ 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:
simp [zpow_ofNat]

Premises used: zpow_ofNat
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
w x : ℂ
hw : w ≠ x
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:
simp [zpow_ofNat]

Premises used: zpow_ofNat
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
w x : ℂ
hw : w ≠ x
⊢ 0 < ‖w - x‖ₑ

Tactic:
simpa [sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℝ
⊢ Eq (α := FormalMultilinearSeries ℝ ℂ ℂ) (binomialSeries ℂ a : FormalMultilinearSeries ℝ ℂ ℂ)
    (FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ (↑a : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ) :
      FormalMultilinearSeries ℝ ℂ ℂ)

Tactic:
aesop
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℝ
⊢ Eq (α := FormalMultilinearSeries ℝ ℂ ℂ) (binomialSeries ℂ a : FormalMultilinearSeries ℝ ℂ ℂ)
    (FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ (↑a : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ) :
      FormalMultilinearSeries ℝ ℂ ℂ)

Tactic:
have H : binomialSeries ℂ a = (binomialSeries ℂ (a : ℂ)).restrictScalars (𝕜 := ℝ) := by aesop
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℝ
H :
  Eq (α := FormalMultilinearSeries ℝ ℂ ℂ) (binomialSeries ℂ a : FormalMultilinearSeries ℝ ℂ ℂ)
    (FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ (↑a : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ) :
      FormalMultilinearSeries ℝ ℂ ℂ)
⊢ HasFPowerSeriesOnBall (fun (x : ℂ) ↦ (1 + x) ^ (↑a : ℂ)) (binomialSeries ℂ a) ((Complex.ofRealCLM : (a : ℝ) → ℂ) 0) 1

Tactic:
have : HasFPowerSeriesOnBall (fun x ↦ (1 + x) ^ (a : ℂ)) (binomialSeries ℂ a) (.ofRealCLM 0) 1 :=
    Complex.ofRealCLM.map_zero ▸ H ▸ Complex.one_add_cpow_hasFPowerSeriesOnBall_zero.restrictScalars
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℝ
H :
  Eq (α := FormalMultilinearSeries ℝ ℂ ℂ) (binomialSeries ℂ a : FormalMultilinearSeries ℝ ℂ ℂ)
    (FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ (↑a : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ) :
      FormalMultilinearSeries ℝ ℂ ℂ)
this :
  HasFPowerSeriesOnBall (fun (x : ℂ) ↦ (1 + x) ^ (↑a : ℂ)) (binomialSeries ℂ a) ((Complex.ofRealCLM : (a : ℝ) → ℂ) 0) 1
⊢ HasFPowerSeriesOnBall (fun (x : ℝ) ↦ (1 + x) ^ a)
    (Complex.reCLM.compFormalMultilinearSeries
      (FormalMultilinearSeries.compContinuousLinearMap (binomialSeries ℂ a : FormalMultilinearSeries ℝ ℂ ℂ)
          Complex.ofRealCLM :
        FormalMultilinearSeries ℝ ℝ ℂ))
    0 (1 / ‖Complex.ofRealCLM‖ₑ)

Tactic:
(Complex.reCLM.comp_hasFPowerSeriesOnBall this.compContinuousLinearMap).congr ?_

Premises used: HasFPowerSeriesOnBall.congr, HasFPowerSeriesOnBall.compContinuousLinearMap, ContinuousLinearMap.comp_hasFPowerSeriesOnBall, Complex.reCLM
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℝ
H :
  Eq (α := FormalMultilinearSeries ℝ ℂ ℂ) (binomialSeries ℂ a : FormalMultilinearSeries ℝ ℂ ℂ)
    (FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ (↑a : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ) :
      FormalMultilinearSeries ℝ ℂ ℂ)
this :
  HasFPowerSeriesOnBall (fun (x : ℂ) ↦ (1 + x) ^ (↑a : ℂ)) (binomialSeries ℂ a) ((Complex.ofRealCLM : (a : ℝ) → ℂ) 0) 1
h :
  Eq (α := FormalMultilinearSeries ℝ ℝ ℝ) (binomialSeries ℝ a : FormalMultilinearSeries ℝ ℝ ℝ)
    (Complex.reCLM.compFormalMultilinearSeries
        (FormalMultilinearSeries.compContinuousLinearMap (binomialSeries ℂ a : FormalMultilinearSeries ℝ ℂ ℂ)
            Complex.ofRealCLM :
          FormalMultilinearSeries ℝ ℝ ℂ) :
      FormalMultilinearSeries ℝ ℝ ℝ)
h₁ : 1 = 1 / ‖Complex.ofRealCLM‖ₑ
convert_2 :
  Set.EqOn (β := ℝ)
    (Function.comp (β := ℂ) (⇑Complex.reCLM : (a : ℂ) → ℝ)
      ((fun (x : ℂ) ↦ (1 + x) ^ (↑a : ℂ)) ∘ (⇑Complex.ofRealCLM : (a : ℝ) → ℂ)))
    (fun (x : ℝ) ↦ (1 + x) ^ a) (Metric.eball 0 (1 / ‖Complex.ofRealCLM‖ₑ))
⊢ HasFPowerSeriesOnBall (fun (x : ℝ) ↦ (1 + x) ^ a) (binomialSeries ℝ a) 0 1

Tactic:
convert! (Complex.reCLM.comp_hasFPowerSeriesOnBall this.compContinuousLinearMap).congr ?_

Premises used: HasFPowerSeriesOnBall.congr, HasFPowerSeriesOnBall.compContinuousLinearMap, ContinuousLinearMap.comp_hasFPowerSeriesOnBall, Complex.reCLM
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℝ
H :
  Eq (α := FormalMultilinearSeries ℝ ℂ ℂ) (binomialSeries ℂ a : FormalMultilinearSeries ℝ ℂ ℂ)
    (FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ (↑a : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ) :
      FormalMultilinearSeries ℝ ℂ ℂ)
this :
  HasFPowerSeriesOnBall (fun (x : ℂ) ↦ (1 + x) ^ (↑a : ℂ)) (binomialSeries ℂ a) ((Complex.ofRealCLM : (a : ℝ) → ℂ) 0) 1
h :
  ∀ (n : ℕ),
    Eq (α := ℝ) ((binomialSeries ℝ a n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)
      ((Complex.reCLM.compFormalMultilinearSeries
              (FormalMultilinearSeries.compContinuousLinearMap (binomialSeries ℂ a : FormalMultilinearSeries ℝ ℂ ℂ)
                  Complex.ofRealCLM :
                FormalMultilinearSeries ℝ ℝ ℂ)
              n :
            (a : (i : Fin n) → ℝ) → ℝ)
          fun (x : Fin n) ↦ 1 :
        ℝ)
⊢ Eq (α := FormalMultilinearSeries ℝ ℝ ℝ) (binomialSeries ℝ a : FormalMultilinearSeries ℝ ℝ ℝ)
    (Complex.reCLM.compFormalMultilinearSeries
        (FormalMultilinearSeries.compContinuousLinearMap (binomialSeries ℂ a : FormalMultilinearSeries ℝ ℂ ℂ)
            Complex.ofRealCLM :
          FormalMultilinearSeries ℝ ℝ ℂ) :
      FormalMultilinearSeries ℝ ℝ ℝ)

Tactic:
ext
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℝ
H :
  Eq (α := FormalMultilinearSeries ℝ ℂ ℂ) (binomialSeries ℂ a : FormalMultilinearSeries ℝ ℂ ℂ)
    (FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ (↑a : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ) :
      FormalMultilinearSeries ℝ ℂ ℂ)
this :
  HasFPowerSeriesOnBall (fun (x : ℂ) ↦ (1 + x) ^ (↑a : ℂ)) (binomialSeries ℂ a) ((Complex.ofRealCLM : (a : ℝ) → ℂ) 0) 1
n : ℕ
⊢ Eq (α := ℝ) ((binomialSeries ℝ a n : (a : (i : Fin n) → ℝ) → ℝ) fun (x : Fin n) ↦ 1 : ℝ)
    ((Complex.reCLM.compFormalMultilinearSeries
            (FormalMultilinearSeries.compContinuousLinearMap (binomialSeries ℂ a : FormalMultilinearSeries ℝ ℂ ℂ)
                Complex.ofRealCLM :
              FormalMultilinearSeries ℝ ℝ ℂ)
            n :
          (a : (i : Fin n) → ℝ) → ℝ)
        fun (x : Fin n) ↦ 1 :
      ℝ)

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℝ
H :
  Eq (α := FormalMultilinearSeries ℝ ℂ ℂ) (binomialSeries ℂ a : FormalMultilinearSeries ℝ ℂ ℂ)
    (FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ (↑a : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ) :
      FormalMultilinearSeries ℝ ℂ ℂ)
this :
  HasFPowerSeriesOnBall (fun (x : ℂ) ↦ (1 + x) ^ (↑a : ℂ)) (binomialSeries ℂ a) ((Complex.ofRealCLM : (a : ℝ) → ℂ) 0) 1
⊢ 1 = 1 / ‖Complex.ofRealCLM‖ₑ

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℝ
H :
  Eq (α := FormalMultilinearSeries ℝ ℂ ℂ) (binomialSeries ℂ a : FormalMultilinearSeries ℝ ℂ ℂ)
    (FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ (↑a : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ) :
      FormalMultilinearSeries ℝ ℂ ℂ)
this :
  HasFPowerSeriesOnBall (fun (x : ℂ) ↦ (1 + x) ^ (↑a : ℂ)) (binomialSeries ℂ a) ((Complex.ofRealCLM : (a : ℝ) → ℂ) 0) 1
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Metric.eball 0 (1 / ‖Complex.ofRealCLM‖ₑ)) x
convert_2 :
  ∀
    (this :
      HasFPowerSeriesOnBall (fun (x : ℂ) ↦ (1 + x) ^ (↑a : ℂ))
        (FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ (↑a : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ)) 0 1)
    (hx : ‖x‖ₑ < 1), ((1 + (↑x : ℂ)) ^ (↑a : ℂ)).re = (1 + x) ^ a
⊢ Eq (α := ℝ)
    (Function.comp (β := ℂ) (⇑Complex.reCLM : (a : ℂ) → ℝ)
      ((fun (x : ℂ) ↦ (1 + x) ^ (↑a : ℂ)) ∘ (⇑Complex.ofRealCLM : (a : ℝ) → ℂ)) x)
    ((fun (x : ℝ) ↦ (1 + x) ^ a) x)

Tactic:
simp_all
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℝ
H :
  Eq (α := FormalMultilinearSeries ℝ ℂ ℂ) (binomialSeries ℂ a : FormalMultilinearSeries ℝ ℂ ℂ)
    (FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ (↑a : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ) :
      FormalMultilinearSeries ℝ ℂ ℂ)
x : ℝ
this :
  HasFPowerSeriesOnBall (fun (x : ℂ) ↦ (1 + x) ^ (↑a : ℂ))
    (FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ (↑a : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ)) 0 1
hx : ‖x‖ₑ < 1
convert_2 convert_2₁ convert_2₂ convert_2₃ : ((↑(1 + x) : ℂ) ^ (↑a : ℂ)).re = (1 + x) ^ a
⊢ ((1 + (↑x : ℂ)) ^ (↑a : ℂ)).re = (1 + x) ^ a

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℝ
⊢ HasFPowerSeriesAt (fun (x : ℝ) ↦ (1 + x) ^ a) (binomialSeries ℝ a) 0

Tactic:
one_add_rpow_hasFPowerSeriesOnBall_zero.hasFPowerSeriesAt

Premises used: Real.one_add_rpow_hasFPowerSeriesOnBall_zero, HasFPowerSeriesOnBall.hasFPowerSeriesAt
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℝ
⊢ HasFPowerSeriesOnBall (fun (x : ℂ) ↦ 1 / (1 - x) ^ (↑a : ℂ))
    (FormalMultilinearSeries.restrictScalars ℝ (𝕜' := ℂ)
      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ Ring.choose ((↑a : ℂ) + (↑n : ℂ) - 1) n :
        FormalMultilinearSeries ℂ ℂ ℂ))
    0 1

Tactic:
have := (Complex.one_div_one_sub_cpow_hasFPowerSeriesOnBall_zero a).restrictScalars (𝕜 := ℝ)
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℝ
this :
  HasFPowerSeriesOnBall (fun (x : ℂ) ↦ 1 / (1 - x) ^ (↑a : ℂ))
    (FormalMultilinearSeries.restrictScalars ℝ (𝕜' := ℂ)
      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ Ring.choose ((↑a : ℂ) + (↑n : ℂ) - 1) n :
        FormalMultilinearSeries ℂ ℂ ℂ))
    0 1
⊢ HasFPowerSeriesOnBall (fun (x : ℂ) ↦ 1 / (1 - x) ^ (↑a : ℂ))
    (FormalMultilinearSeries.restrictScalars ℝ (𝕜' := ℂ)
      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ Ring.choose ((↑a : ℂ) + (↑n : ℂ) - 1) n :
        FormalMultilinearSeries ℂ ℂ ℂ))
    ((Complex.ofRealCLM : (a : ℝ) → ℂ) 0) 1

Tactic:
rw [← Complex.ofRealCLM.map_zero] at this

Premises used: ContinuousLinearMap.map_zero, Complex.ofRealCLM
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℝ
this :
  HasFPowerSeriesOnBall (fun (x : ℂ) ↦ 1 / (1 - x) ^ (↑a : ℂ))
    (FormalMultilinearSeries.restrictScalars ℝ (𝕜' := ℂ)
      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ Ring.choose ((↑a : ℂ) + (↑n : ℂ) - 1) n :
        FormalMultilinearSeries ℂ ℂ ℂ))
    ((Complex.ofRealCLM : (a : ℝ) → ℂ) 0) 1
⊢ HasFPowerSeriesOnBall (fun (x : ℝ) ↦ 1 / (1 - x) ^ a)
    (Complex.reCLM.compFormalMultilinearSeries
      (FormalMultilinearSeries.compContinuousLinearMap
          (FormalMultilinearSeries.restrictScalars ℝ (𝕜' := ℂ)
              (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ Ring.choose ((↑a : ℂ) + (↑n : ℂ) - 1) n :
                FormalMultilinearSeries ℂ ℂ ℂ) :
            FormalMultilinearSeries ℝ ℂ ℂ)
          Complex.ofRealCLM :
        FormalMultilinearSeries ℝ ℝ ℂ))
    0 (1 / ‖Complex.ofRealCLM‖ₑ)

Tactic:
(Complex.reCLM.comp_hasFPowerSeriesOnBall this.compContinuousLinearMap).congr ?_

Premises used: HasFPowerSeriesOnBall.congr, HasFPowerSeriesOnBall.compContinuousLinearMap, ContinuousLinearMap.comp_hasFPowerSeriesOnBall, Complex.reCLM
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℝ
this :
  HasFPowerSeriesOnBall (fun (x : ℂ) ↦ 1 / (1 - x) ^ (↑a : ℂ))
    (FormalMultilinearSeries.restrictScalars ℝ (𝕜' := ℂ)
      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ Ring.choose ((↑a : ℂ) + (↑n : ℂ) - 1) n :
        FormalMultilinearSeries ℂ ℂ ℂ))
    ((Complex.ofRealCLM : (a : ℝ) → ℂ) 0) 1
h :
  Eq (α := FormalMultilinearSeries ℝ ℝ ℝ)
    (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) ↦ Ring.choose (a + (↑n : ℝ) - 1) n : FormalMultilinearSeries ℝ ℝ ℝ)
    (Complex.reCLM.compFormalMultilinearSeries
        (FormalMultilinearSeries.compContinuousLinearMap
            (FormalMultilinearSeries.restrictScalars ℝ (𝕜' := ℂ)
                (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ Ring.choose ((↑a : ℂ) + (↑n : ℂ) - 1) n :
                  FormalMultilinearSeries ℂ ℂ ℂ) :
              FormalMultilinearSeries ℝ ℂ ℂ)
            Complex.ofRealCLM :
          FormalMultilinearSeries ℝ ℝ ℂ) :
      FormalMultilinearSeries ℝ ℝ ℝ)
h₁ : 1 = 1 / ‖Complex.ofRealCLM‖ₑ
convert_2 :
  Set.EqOn (β := ℝ)
    (Function.comp (β := ℂ) (⇑Complex.reCLM : (a : ℂ) → ℝ)
      ((fun (x : ℂ) ↦ 1 / (1 - x) ^ (↑a : ℂ)) ∘ (⇑Complex.ofRealCLM : (a : ℝ) → ℂ)))
    (fun (x : ℝ) ↦ 1 / (1 - x) ^ a) (Metric.eball 0 (1 / ‖Complex.ofRealCLM‖ₑ))
⊢ HasFPowerSeriesOnBall (𝕜 := ℝ) (F := ℝ) (fun (x : ℝ) ↦ 1 / (1 - x) ^ a)
    (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) ↦ Ring.choose (a + (↑n : ℝ) - 1) n) 0 1

Tactic:
convert! (Complex.reCLM.comp_hasFPowerSeriesOnBall this.compContinuousLinearMap).congr ?_ using 1

Premises used: HasFPowerSeriesOnBall.congr, HasFPowerSeriesOnBall.compContinuousLinearMap, ContinuousLinearMap.comp_hasFPowerSeriesOnBall, Complex.reCLM
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℝ
this :
  HasFPowerSeriesOnBall (fun (x : ℂ) ↦ 1 / (1 - x) ^ (↑a : ℂ))
    (FormalMultilinearSeries.restrictScalars ℝ (𝕜' := ℂ)
      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ Ring.choose ((↑a : ℂ) + (↑n : ℂ) - 1) n :
        FormalMultilinearSeries ℂ ℂ ℂ))
    ((Complex.ofRealCLM : (a : ℝ) → ℂ) 0) 1
h :
  ∀ (n : ℕ),
    Eq (α := ℝ)
      ((FormalMultilinearSeries.ofScalars ℝ (fun (n : ℕ) ↦ Ring.choose (a + (↑n : ℝ) - 1) n) n :
            (a : (i : Fin n) → ℝ) → ℝ)
          fun (x : Fin n) ↦ 1 :
        ℝ)
      ((Complex.reCLM.compFormalMultilinearSeries
              (FormalMultilinearSeries.compContinuousLinearMap
                  (FormalMultilinearSeries.restrictScalars ℝ (𝕜' := ℂ)
                      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ Ring.choose ((↑a : ℂ) + (↑n : ℂ) - 1) n :
                        FormalMultilinearSeries ℂ ℂ ℂ) :
                    FormalMultilinearSeries ℝ ℂ ℂ)
                  Complex.ofRealCLM :
                FormalMultilinearSeries ℝ ℝ ℂ)
              n :
            (a : (i : Fin n) → ℝ) → ℝ)
          fun (x : Fin n) ↦ 1 :
        ℝ)
⊢ Eq (α := FormalMultilinearSeries ℝ ℝ ℝ)
    (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) ↦ Ring.choose (a + (↑n : ℝ) - 1) n : FormalMultilinearSeries ℝ ℝ ℝ)
    (Complex.reCLM.compFormalMultilinearSeries
        (FormalMultilinearSeries.compContinuousLinearMap
            (FormalMultilinearSeries.restrictScalars ℝ (𝕜' := ℂ)
                (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ Ring.choose ((↑a : ℂ) + (↑n : ℂ) - 1) n :
                  FormalMultilinearSeries ℂ ℂ ℂ) :
              FormalMultilinearSeries ℝ ℂ ℂ)
            Complex.ofRealCLM :
          FormalMultilinearSeries ℝ ℝ ℂ) :
      FormalMultilinearSeries ℝ ℝ ℝ)

Tactic:
ext n
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℝ
this :
  HasFPowerSeriesOnBall (fun (x : ℂ) ↦ 1 / (1 - x) ^ (↑a : ℂ))
    (FormalMultilinearSeries.restrictScalars ℝ (𝕜' := ℂ)
      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ Ring.choose ((↑a : ℂ) + (↑n : ℂ) - 1) n :
        FormalMultilinearSeries ℂ ℂ ℂ))
    ((Complex.ofRealCLM : (a : ℝ) → ℂ) 0) 1
n : ℕ
h : Ring.choose (a + (↑n : ℝ) - 1) n = (Ring.choose ((↑a : ℂ) + (↑n : ℂ) - 1) n).re
⊢ Eq (α := ℝ)
    ((FormalMultilinearSeries.ofScalars ℝ (fun (n : ℕ) ↦ Ring.choose (a + (↑n : ℝ) - 1) n) n :
          (a : (i : Fin n) → ℝ) → ℝ)
        fun (x : Fin n) ↦ 1 :
      ℝ)
    ((Complex.reCLM : (a : ℂ) → ℝ)
        ((FormalMultilinearSeries.restrictScalars ℝ (𝕜' := ℂ)
                (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ Ring.choose ((↑a : ℂ) + (↑n : ℂ) - 1) n :
                  FormalMultilinearSeries ℂ ℂ ℂ)
                n :
              (a : (i : Fin n) → ℂ) → ℂ)
            (Function.comp (β := ℝ) (⇑Complex.ofRealCLM : (a : ℝ) → ℂ) fun (x : Fin n) ↦ 1) :
          ℂ) :
      ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℝ
this :
  HasFPowerSeriesOnBall (fun (x : ℂ) ↦ 1 / (1 - x) ^ (↑a : ℂ))
    (FormalMultilinearSeries.restrictScalars ℝ (𝕜' := ℂ)
      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ Ring.choose ((↑a : ℂ) + (↑n : ℂ) - 1) n :
        FormalMultilinearSeries ℂ ℂ ℂ))
    ((Complex.ofRealCLM : (a : ℝ) → ℂ) 0) 1
n : ℕ
h h₁ h₂ h₃ : Ring.choose (a + (↑n : ℝ) - 1) n = Ring.choose (a + (↑n : ℝ) - 1) n
⊢ Ring.choose (a + (↑n : ℝ) - 1) n = (Ring.choose ((↑a : ℂ) + (↑n : ℂ) - 1) n).re

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℝ
this :
  HasFPowerSeriesOnBall (fun (x : ℂ) ↦ 1 / (1 - x) ^ (↑a : ℂ))
    (FormalMultilinearSeries.restrictScalars ℝ (𝕜' := ℂ)
      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ Ring.choose ((↑a : ℂ) + (↑n : ℂ) - 1) n :
        FormalMultilinearSeries ℂ ℂ ℂ))
    ((Complex.ofRealCLM : (a : ℝ) → ℂ) 0) 1
⊢ 1 = 1 / ‖Complex.ofRealCLM‖ₑ

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℝ
this :
  HasFPowerSeriesOnBall (fun (x : ℂ) ↦ 1 / (1 - x) ^ (↑a : ℂ))
    (FormalMultilinearSeries.restrictScalars ℝ (𝕜' := ℂ)
      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ Ring.choose ((↑a : ℂ) + (↑n : ℂ) - 1) n :
        FormalMultilinearSeries ℂ ℂ ℂ))
    ((Complex.ofRealCLM : (a : ℝ) → ℂ) 0) 1
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Metric.eball 0 (1 / ‖Complex.ofRealCLM‖ₑ)) x
⊢ |x| < 1

Tactic:
simpa [enorm_eq_nnnorm] using hx

Premises used: enorm_eq_nnnorm
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℝ
this :
  HasFPowerSeriesOnBall (fun (x : ℂ) ↦ 1 / (1 - x) ^ (↑a : ℂ))
    (FormalMultilinearSeries.restrictScalars ℝ (𝕜' := ℂ)
      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ Ring.choose ((↑a : ℂ) + (↑n : ℂ) - 1) n :
        FormalMultilinearSeries ℂ ℂ ℂ))
    ((Complex.ofRealCLM : (a : ℝ) → ℂ) 0) 1
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Metric.eball 0 (1 / ‖Complex.ofRealCLM‖ₑ)) x
⊢ |x| < 1

Tactic:
have : |x| < 1 := by simpa [enorm_eq_nnnorm] using hx
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℝ
this_1 :
  HasFPowerSeriesOnBall (fun (x : ℂ) ↦ 1 / (1 - x) ^ (↑a : ℂ))
    (FormalMultilinearSeries.restrictScalars ℝ (𝕜' := ℂ)
      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ Ring.choose ((↑a : ℂ) + (↑n : ℂ) - 1) n :
        FormalMultilinearSeries ℂ ℂ ℂ))
    ((Complex.ofRealCLM : (a : ℝ) → ℂ) 0) 1
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Metric.eball 0 (1 / ‖Complex.ofRealCLM‖ₑ)) x
this : |x| < 1
⊢ 0 ≤ 1 - x

Tactic:
grind
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℝ
this_1 :
  HasFPowerSeriesOnBall (fun (x : ℂ) ↦ 1 / (1 - x) ^ (↑a : ℂ))
    (FormalMultilinearSeries.restrictScalars ℝ (𝕜' := ℂ)
      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ Ring.choose ((↑a : ℂ) + (↑n : ℂ) - 1) n :
        FormalMultilinearSeries ℂ ℂ ℂ))
    ((Complex.ofRealCLM : (a : ℝ) → ℂ) 0) 1
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Metric.eball 0 (1 / ‖Complex.ofRealCLM‖ₑ)) x
this : |x| < 1
⊢ 0 ≤ 1 - x

Tactic:
have : 0 ≤ 1 - x := by grind