awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_2 : |x| < 1
this : 0 ≤ 1 - x
⊢ Eq (α := ℝ)
    (Function.comp (β := ℂ) (⇑Complex.reCLM : (a : ℂ) → ℝ)
      ((fun (x : ℂ) ↦ 1 / (1 - x) ^ (↑a : ℂ)) ∘ (⇑Complex.ofRealCLM : (a : ℝ) → ℂ)) x)
    ((fun (x : ℝ) ↦ 1 / (1 - x) ^ a) x)

Tactic:
simp [-Complex.inv_re, ← Complex.ofReal_one, ← Complex.ofReal_sub, ← Complex.ofReal_cpow this]

Premises used: Complex.ofReal_cpow, Complex.inv_re, Complex.ofReal_one, Complex.ofReal_sub
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℕ
r : ℝ
hr : r ≠ 0
⊢ (↑r : ℂ) ≠ 0

Tactic:
simpa
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℕ
r : ℝ
hr : r ≠ 0
⊢ HasFPowerSeriesOnBall (fun (x : ℂ) ↦ 1 / ((↑r : ℂ) - x) ^ (a + 1))
    (FormalMultilinearSeries.restrictScalars ℝ (𝕜' := ℂ)
      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ ((↑r : ℂ) ^ (n + a + 1))⁻¹ * (↑((a + n).choose a) : ℂ) :
        FormalMultilinearSeries ℂ ℂ ℂ))
    0 ‖(↑r : ℂ)‖ₑ

Tactic:
have := (Complex.one_div_sub_pow_hasFPowerSeriesOnBall_zero a (z := r)
    (by simpa)).restrictScalars (𝕜 := ℝ)
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℕ
r : ℝ
hr : r ≠ 0
this :
  HasFPowerSeriesOnBall (fun (x : ℂ) ↦ 1 / ((↑r : ℂ) - x) ^ (a + 1))
    (FormalMultilinearSeries.restrictScalars ℝ (𝕜' := ℂ)
      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ ((↑r : ℂ) ^ (n + a + 1))⁻¹ * (↑((a + n).choose a) : ℂ) :
        FormalMultilinearSeries ℂ ℂ ℂ))
    0 ‖(↑r : ℂ)‖ₑ
⊢ HasFPowerSeriesOnBall (fun (x : ℂ) ↦ 1 / ((↑r : ℂ) - x) ^ (a + 1))
    (FormalMultilinearSeries.restrictScalars ℝ (𝕜' := ℂ)
      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ ((↑r : ℂ) ^ (n + a + 1))⁻¹ * (↑((a + n).choose a) : ℂ) :
        FormalMultilinearSeries ℂ ℂ ℂ))
    ((Complex.ofRealCLM : (a : ℝ) → ℂ) 0) ‖(↑r : ℂ)‖ₑ

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

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

Tactic:
(Complex.reCLM.comp_hasFPowerSeriesOnBall this.compContinuousLinearMap)

Premises used: HasFPowerSeriesOnBall.compContinuousLinearMap, ContinuousLinearMap.comp_hasFPowerSeriesOnBall, Complex.reCLM
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℕ
r : ℝ
hr : r ≠ 0
this :
  HasFPowerSeriesOnBall (fun (x : ℂ) ↦ 1 / ((↑r : ℂ) - x) ^ (a + 1))
    (FormalMultilinearSeries.restrictScalars ℝ (𝕜' := ℂ)
      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ ((↑r : ℂ) ^ (n + a + 1))⁻¹ * (↑((a + n).choose a) : ℂ) :
        FormalMultilinearSeries ℂ ℂ ℂ))
    ((Complex.ofRealCLM : (a : ℝ) → ℂ) 0) ‖(↑r : ℂ)‖ₑ
h :
  ∀ (x : ℝ),
    1 / (r - x) ^ (a + 1) =
      Function.comp (β := ℂ) (⇑Complex.reCLM : (a : ℂ) → ℝ)
        ((fun (x : ℂ) ↦ 1 / ((↑r : ℂ) - x) ^ (a + 1)) ∘ (⇑Complex.ofRealCLM : (a : ℝ) → ℂ)) x
h₁ :
  Eq (α := FormalMultilinearSeries ℝ ℝ ℝ)
    (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) ↦ (r ^ (n + a + 1))⁻¹ * (↑((a + n).choose a) : ℝ) :
      FormalMultilinearSeries ℝ ℝ ℝ)
    (Complex.reCLM.compFormalMultilinearSeries
        (FormalMultilinearSeries.compContinuousLinearMap
            (FormalMultilinearSeries.restrictScalars ℝ (𝕜' := ℂ)
                (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦
                    ((↑r : ℂ) ^ (n + a + 1))⁻¹ * (↑((a + n).choose a) : ℂ) :
                  FormalMultilinearSeries ℂ ℂ ℂ) :
              FormalMultilinearSeries ℝ ℂ ℂ)
            Complex.ofRealCLM :
          FormalMultilinearSeries ℝ ℝ ℂ) :
      FormalMultilinearSeries ℝ ℝ ℝ)
h₂ : ‖r‖ₑ = ‖(↑r : ℂ)‖ₑ / ‖Complex.ofRealCLM‖ₑ
⊢ HasFPowerSeriesOnBall (𝕜 := ℝ) (F := ℝ) (fun (x : ℝ) ↦ 1 / (r - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) ↦ (r ^ (n + a + 1))⁻¹ * (↑((a + n).choose a) : ℝ)) 0 ‖r‖ₑ

Tactic:
convert! (Complex.reCLM.comp_hasFPowerSeriesOnBall this.compContinuousLinearMap) using 2

Premises used: HasFPowerSeriesOnBall.compContinuousLinearMap, ContinuousLinearMap.comp_hasFPowerSeriesOnBall, Complex.reCLM
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℕ
r : ℝ
hr : r ≠ 0
this :
  HasFPowerSeriesOnBall (fun (x : ℂ) ↦ 1 / ((↑r : ℂ) - x) ^ (a + 1))
    (FormalMultilinearSeries.restrictScalars ℝ (𝕜' := ℂ)
      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ ((↑r : ℂ) ^ (n + a + 1))⁻¹ * (↑((a + n).choose a) : ℂ) :
        FormalMultilinearSeries ℂ ℂ ℂ))
    ((Complex.ofRealCLM : (a : ℝ) → ℂ) 0) ‖(↑r : ℂ)‖ₑ
x : ℝ
⊢ 1 / (r - x) ^ (a + 1) =
    Function.comp (β := ℂ) (⇑Complex.reCLM : (a : ℂ) → ℝ)
      ((fun (x : ℂ) ↦ 1 / ((↑r : ℂ) - x) ^ (a + 1)) ∘ (⇑Complex.ofRealCLM : (a : ℝ) → ℂ)) x

Tactic:
simp [-Complex.inv_re, ← Complex.ofReal_pow, ← Complex.ofReal_inv, ← Complex.ofReal_sub]

Premises used: Complex.inv_re, Complex.ofReal_sub, Complex.ofReal_pow, Complex.ofReal_inv
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℕ
r : ℝ
hr : r ≠ 0
this :
  HasFPowerSeriesOnBall (fun (x : ℂ) ↦ 1 / ((↑r : ℂ) - x) ^ (a + 1))
    (FormalMultilinearSeries.restrictScalars ℝ (𝕜' := ℂ)
      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ ((↑r : ℂ) ^ (n + a + 1))⁻¹ * (↑((a + n).choose a) : ℂ) :
        FormalMultilinearSeries ℂ ℂ ℂ))
    ((Complex.ofRealCLM : (a : ℝ) → ℂ) 0) ‖(↑r : ℂ)‖ₑ
h :
  ∀ (n : ℕ),
    Eq (α := ℝ)
      ((FormalMultilinearSeries.ofScalars ℝ (fun (n : ℕ) ↦ (r ^ (n + a + 1))⁻¹ * (↑((a + n).choose a) : ℝ)) n :
            (a : (i : Fin n) → ℝ) → ℝ)
          fun (x : Fin n) ↦ 1 :
        ℝ)
      ((Complex.reCLM.compFormalMultilinearSeries
              (FormalMultilinearSeries.compContinuousLinearMap
                  (FormalMultilinearSeries.restrictScalars ℝ (𝕜' := ℂ)
                      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦
                          ((↑r : ℂ) ^ (n + a + 1))⁻¹ * (↑((a + n).choose a) : ℂ) :
                        FormalMultilinearSeries ℂ ℂ ℂ) :
                    FormalMultilinearSeries ℝ ℂ ℂ)
                  Complex.ofRealCLM :
                FormalMultilinearSeries ℝ ℝ ℂ)
              n :
            (a : (i : Fin n) → ℝ) → ℝ)
          fun (x : Fin n) ↦ 1 :
        ℝ)
⊢ Eq (α := FormalMultilinearSeries ℝ ℝ ℝ)
    (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) ↦ (r ^ (n + a + 1))⁻¹ * (↑((a + n).choose a) : ℝ) :
      FormalMultilinearSeries ℝ ℝ ℝ)
    (Complex.reCLM.compFormalMultilinearSeries
        (FormalMultilinearSeries.compContinuousLinearMap
            (FormalMultilinearSeries.restrictScalars ℝ (𝕜' := ℂ)
                (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦
                    ((↑r : ℂ) ^ (n + a + 1))⁻¹ * (↑((a + n).choose a) : ℂ) :
                  FormalMultilinearSeries ℂ ℂ ℂ) :
              FormalMultilinearSeries ℝ ℂ ℂ)
            Complex.ofRealCLM :
          FormalMultilinearSeries ℝ ℝ ℂ) :
      FormalMultilinearSeries ℝ ℝ ℝ)

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

Tactic:
simp [-Complex.inv_re, ← Complex.ofReal_pow, ← Complex.ofReal_inv]

Premises used: Complex.inv_re, Complex.ofReal_pow, Complex.ofReal_inv
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a : ℕ
r : ℝ
hr : r ≠ 0
this :
  HasFPowerSeriesOnBall (fun (x : ℂ) ↦ 1 / ((↑r : ℂ) - x) ^ (a + 1))
    (FormalMultilinearSeries.restrictScalars ℝ (𝕜' := ℂ)
      (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) ↦ ((↑r : ℂ) ^ (n + a + 1))⁻¹ * (↑((a + n).choose a) : ℂ) :
        FormalMultilinearSeries ℂ ℂ ℂ))
    ((Complex.ofRealCLM : (a : ℝ) → ℂ) 0) ‖(↑r : ℂ)‖ₑ
⊢ ‖r‖ₑ = ‖(↑r : ℂ)‖ₑ / ‖Complex.ofRealCLM‖ₑ

Tactic:
simp [enorm_eq_nnnorm]

Premises used: enorm_eq_nnnorm
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
r : ℝ
hr : r ≠ 0
⊢ HasFPowerSeriesOnBall (𝕜 := ℝ) (F := ℝ) (fun (x : ℝ) ↦ 1 / (r - x))
    (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) ↦ (r ^ (n + 1))⁻¹) 0 ‖r‖ₑ

Tactic:
simpa using one_div_sub_pow_hasFPowerSeriesOnBall_zero (a := 0) hr

Premises used: Real.one_div_sub_pow_hasFPowerSeriesOnBall_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
r : ℝ
hr : r ≠ 0
⊢ HasFPowerSeriesOnBall (𝕜 := ℝ) (F := ℝ) (fun (x : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (r - x) 2)
    (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) ↦ (r ^ (n + 2))⁻¹ * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) 0 ‖r‖ₑ

Tactic:
simpa [add_comm 1] using one_div_sub_pow_hasFPowerSeriesOnBall_zero 1 hr

Premises used: add_comm, Real.one_div_sub_pow_hasFPowerSeriesOnBall_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
⊢ HasFPowerSeriesOnBall (𝕜 := ℝ) (F := ℝ) (fun (x : ℝ) ↦ 1 / (1 - x)) (FormalMultilinearSeries.ofScalars ℝ 1) 0 1

Tactic:
simpa using one_div_sub_hasFPowerSeriesOnBall_zero (r := 1)

Premises used: Real.one_div_sub_hasFPowerSeriesOnBall_zero
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
⊢ HasFPowerSeriesOnBall (𝕜 := ℝ) (F := ℝ) (fun (x : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (1 - x) 2)
    (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) 0 1

Tactic:
simpa using one_div_sub_sq_hasFPowerSeriesOnBall_zero (r := 1)

Premises used: Real.one_div_sub_sq_hasFPowerSeriesOnBall_zero
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a b : ℝ
⊢ HasFPowerSeriesOnBall
    ((HSMul.hSMul (β := ℝ → ℝ) (b - a) fun (x : ℝ) ↦ 1 / (1 - x)) +
      HSMul.hSMul (β := ℝ → ℝ) a fun (x : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (1 - x) 2)
    (HSMul.hSMul (β := FormalMultilinearSeries ℝ ℝ ℝ) (b - a)
        (FormalMultilinearSeries.ofScalars ℝ 1 : FormalMultilinearSeries ℝ ℝ ℝ) +
      HSMul.hSMul (β := FormalMultilinearSeries ℝ ℝ ℝ) a
        (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 :
          FormalMultilinearSeries ℝ ℝ ℝ))
    0 1

Tactic:
(one_div_one_sub_hasFPowerSeriesOnBall_zero.const_smul (c := b - a)).add
      (one_div_one_sub_sq_hasFPowerSeriesOnBall_zero.const_smul (c := a))

Premises used: HasFPowerSeriesOnBall.add, HasFPowerSeriesOnBall.const_smul, Real.one_div_one_sub_sq_hasFPowerSeriesOnBall_zero, Real.one_div_one_sub_hasFPowerSeriesOnBall_zero
-- Module: Mathlib.Analysis.Analytic.Binomial
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
h₁ :
  (FormalMultilinearSeries.ofScalars ℝ fun (x : ℕ) ↦ a * (↑x : ℝ) + b) =
    HSMul.hSMul (β := FormalMultilinearSeries ℝ ℝ ℝ) (b - a)
        (FormalMultilinearSeries.ofScalars ℝ 1 : FormalMultilinearSeries ℝ ℝ ℝ) +
      HSMul.hSMul (β := FormalMultilinearSeries ℝ ℝ ℝ) a
        (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 :
          FormalMultilinearSeries ℝ ℝ ℝ)
⊢ HasFPowerSeriesOnBall (𝕜 := ℝ) (F := ℝ) (fun (x : ℝ) ↦ (b - a) / (1 - x) + a / HPow.hPow (β := ℕ) (1 - x) 2)
    (FormalMultilinearSeries.ofScalars ℝ fun (x : ℕ) ↦ a * (↑x : ℝ) + b) 0 1

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

Premises used: HasFPowerSeriesOnBall.add, HasFPowerSeriesOnBall.const_smul, Real.one_div_one_sub_sq_hasFPowerSeriesOnBall_zero, Real.one_div_one_sub_hasFPowerSeriesOnBall_zero
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a b 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:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a b : ℝ
h :
  ∀ (n : ℕ),
    Eq (α := ℝ)
      ((FormalMultilinearSeries.ofScalars ℝ (fun (x : ℕ) ↦ a * (↑x : ℝ) + 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 :
        ℝ)
⊢ (FormalMultilinearSeries.ofScalars ℝ fun (x : ℕ) ↦ a * (↑x : ℝ) + b) =
    HSMul.hSMul (β := FormalMultilinearSeries ℝ ℝ ℝ) (b - a)
        (FormalMultilinearSeries.ofScalars ℝ 1 : FormalMultilinearSeries ℝ ℝ ℝ) +
      HSMul.hSMul (β := FormalMultilinearSeries ℝ ℝ ℝ) a
        (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) ↦ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 :
          FormalMultilinearSeries ℝ ℝ ℝ)

Tactic:
ext
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a b : ℝ
n : ℕ
h : a * (↑n : ℝ) + b = b - a + a * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ Eq (α := ℝ)
    ((FormalMultilinearSeries.ofScalars ℝ (fun (x : ℕ) ↦ a * (↑x : ℝ) + 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:
simp
-- Module: Mathlib.Analysis.Analytic.Binomial
Goal:
a b : ℝ
n : ℕ
⊢ a * (↑n : ℝ) + b = b - a + a * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
ring
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
c : F
e : E
⊢ HasFiniteFPowerSeriesOnBall (fun (x : E) ↦ c) (constFormalMultilinearSeries 𝕜 E c) e 1 ∞

Tactic:
⟨hasFPowerSeriesOnBall_const,
    fun _ hn ↦ constFormalMultilinearSeries_apply_of_nonzero (Nat.ne_zero_of_lt hn)⟩

Premises used: hasFPowerSeriesOnBall_const, HasFiniteFPowerSeriesOnBall.mk, constFormalMultilinearSeries_apply_of_nonzero, Nat.ne_zero_of_lt
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
c : F
e : E
⊢ HasFiniteFPowerSeriesAt (fun (x : E) ↦ c) (constFormalMultilinearSeries 𝕜 E c) e 1

Tactic:
⟨⊤, hasFiniteFPowerSeriesOnBall_const⟩

Premises used: HasFiniteFPowerSeriesAt, hasFiniteFPowerSeriesOnBall_const, Exists.intro, Top.top
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
v : F
⊢ CPolynomialAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (x : E) ↦ v) x

Tactic:
⟨constFormalMultilinearSeries 𝕜 E v, 1, hasFiniteFPowerSeriesAt_const⟩

Premises used: constFormalMultilinearSeries, hasFiniteFPowerSeriesAt_const, Exists.intro, CPolynomialAt, OfNat.ofNat
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
v : F
s : Set E
⊢ CPolynomialOn.{u_1, u_2, u_3} 𝕜 (F := F) (fun (x : E) ↦ v) s

Tactic:
fun _ _ => CPolynomialAt_const

Premises used: CPolynomialAt_const, CPolynomialOn
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n m : ℕ
hf : HasFiniteFPowerSeriesOnBall f pf x n r
hg : HasFiniteFPowerSeriesOnBall g pg x m r
N : ℕ
hN : max n m ≤ N
rw : pf N + pg N = 0
rw₁ : 0 + pg N = 0
rw₂ : HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin N) ↦ E) F) 0 0 = 0
rw₃ rw₄ : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin N) ↦ E) F) 0 0
⊢ (pf + pg) N = 0

Tactic:
rw [Pi.add_apply, hf.finite _ ((le_max_left n m).trans hN),
        hg.finite _ ((le_max_right n m).trans hN), zero_add]

Premises used: le_max_right, zero_add, Pi.add_apply, HasFiniteFPowerSeriesOnBall.finite, LE.le.trans, le_max_left
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
x : E
n m : ℕ
hf : HasFiniteFPowerSeriesAt f pf x n
hg : HasFiniteFPowerSeriesAt g pg x m
rcases :
  ∀ (r : ℝ≥0∞) (hr : HasFiniteFPowerSeriesOnBall f pf x n r ∧ HasFiniteFPowerSeriesOnBall g pg x m r),
    HasFiniteFPowerSeriesAt (f + g) (pf + pg) x (max n m)
⊢ HasFiniteFPowerSeriesAt (f + g) (pf + pg) x (max n m)

Tactic:
rcases (hf.eventually.and hg.eventually).exists with ⟨r, hr⟩

Premises used: Filter.Eventually.and, Filter.Eventually.exists, HasFiniteFPowerSeriesAt.eventually
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
x : E
n m : ℕ
hf : HasFiniteFPowerSeriesAt f pf x n
hg : HasFiniteFPowerSeriesAt g pg x m
r : ℝ≥0∞
hr : HasFiniteFPowerSeriesOnBall f pf x n r ∧ HasFiniteFPowerSeriesOnBall g pg x m r
⊢ HasFiniteFPowerSeriesAt (f + g) (pf + pg) x (max n m)

Tactic:
⟨r, hr.1.add hr.2⟩

Premises used: HasFiniteFPowerSeriesAt, And.right, And.left, HasFiniteFPowerSeriesOnBall.add, Exists.intro
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
x : E
n m : ℕ
hf : HasFiniteFPowerSeriesAt f pf x n
hg : HasFiniteFPowerSeriesAt g pg x m
r : ℝ≥0∞
hr : HasFiniteFPowerSeriesOnBall f pf x n r ∧ HasFiniteFPowerSeriesOnBall g pg x m r
⊢ HasFiniteFPowerSeriesAt (f + g) (pf + pg) x (max n m)

Tactic:
exact ⟨r, hr.1.add hr.2⟩
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
x : E
hf : CPolynomialAt 𝕜 f x
hg : CPolynomialAt 𝕜 g x
⊢ CPolynomialAt 𝕜 (f + g) x

Tactic:
let ⟨_, _, hpf⟩ := hf
  let ⟨_, _, hqf⟩ := hg
  (hpf.add hqf).cpolynomialAt

Premises used: _private.0.CPolynomialAt.add.match_1, HAdd.hAdd, HasFiniteFPowerSeriesAt.add, HasFiniteFPowerSeriesAt.cpolynomialAt, CPolynomialAt
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n : ℕ
hf : HasFiniteFPowerSeriesOnBall f pf x n r
m : ℕ
hm : n ≤ m
rw : -pf m = 0
rw₁ : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F) (-0) 0
rw₂ rw₃ : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F) 0 0
⊢ (-pf) m = 0

Tactic:
rw [Pi.neg_apply, hf.finite m hm, neg_zero]

Premises used: HasFiniteFPowerSeriesOnBall.finite, neg_zero, Pi.neg_apply
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
x : E
n : ℕ
hf : HasFiniteFPowerSeriesAt f pf x n
⊢ HasFiniteFPowerSeriesAt (-f) (-pf) x n

Tactic:
let ⟨_, hrf⟩ := hf
  hrf.neg.hasFiniteFPowerSeriesAt

Premises used: HasFiniteFPowerSeriesOnBall.hasFiniteFPowerSeriesAt, _private.0.HasFiniteFPowerSeriesAt.neg.match_1, HasFiniteFPowerSeriesAt, HasFiniteFPowerSeriesOnBall.neg, Neg.neg
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
hf : CPolynomialAt 𝕜 f x
⊢ CPolynomialAt 𝕜 (-f) x

Tactic:
let ⟨_, _, hpf⟩ := hf
  hpf.neg.cpolynomialAt

Premises used: HasFiniteFPowerSeriesAt.neg, _private.0.CPolynomialAt.add.match_1, HasFiniteFPowerSeriesAt.cpolynomialAt, CPolynomialAt, Neg.neg
-- Module: Mathlib.Analysis.Analytic.CPolynomial
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n m : ℕ
hf : HasFiniteFPowerSeriesOnBall f pf x n r
hg : HasFiniteFPowerSeriesOnBall g pg x m r
⊢ HasFiniteFPowerSeriesOnBall (f - g) (pf - pg) x (max n m) r

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Premises used: sub_eq_add_neg, HasFiniteFPowerSeriesOnBall.neg, HasFiniteFPowerSeriesOnBall.add