awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (hypothesis)
Goal:
a : ℝ
⊢ HasFPowerSeriesOnBall (fun (x : ℝ) ↦ (1 + x) ^ a) (binomialSeries ℝ a) 0 1
have H : Eq (α := FormalMultilinearSeries ℝ ℂ ℂ) (binomialSeries ℂ a : FormalMultilinearSeries ℝ ℂ ℂ)
  (FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ (↑a : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ) :
    FormalMultilinearSeries ℝ ℂ ℂ)
Tactic: have H : binomialSeries ℂ a = (binomialSeries ℂ (a : ℂ)).restrictScalars (𝕜 := ℝ) := by aesop
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (hypothesis)
Goal:
a : ℝ
H :
  Eq (α := FormalMultilinearSeries ℝ ℂ ℂ) (binomialSeries ℂ a : FormalMultilinearSeries ℝ ℂ ℂ)
    (FormalMultilinearSeries.restrictScalars ℝ (binomialSeries ℂ (↑a : ℂ) : FormalMultilinearSeries ℂ ℂ ℂ) :
      FormalMultilinearSeries ℝ ℂ ℂ)
⊢ HasFPowerSeriesOnBall (fun (x : ℝ) ↦ (1 + x) ^ a) (binomialSeries ℝ a) 0 1
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
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) (binomialSeries ℝ a) 0 1
have h : Eq (α := FormalMultilinearSeries ℝ ℝ ℝ) (binomialSeries ℝ a : FormalMultilinearSeries ℝ ℝ ℝ)
  (Complex.reCLM.compFormalMultilinearSeries
      (FormalMultilinearSeries.compContinuousLinearMap (binomialSeries ℂ a : FormalMultilinearSeries ℝ ℂ ℂ)
          Complex.ofRealCLM :
        FormalMultilinearSeries ℝ ℝ ℂ) :
    FormalMultilinearSeries ℝ ℝ ℝ)
Tactic: convert! (Complex.reCLM.comp_hasFPowerSeriesOnBall this.compContinuousLinearMap).congr ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
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 ℝ ℝ ℝ)
⊢ HasFPowerSeriesOnBall (fun (x : ℝ) ↦ (1 + x) ^ a) (binomialSeries ℝ a) 0 1
have h₁ : 1 = 1 / ‖Complex.ofRealCLM‖ₑ
Tactic: convert! (Complex.reCLM.comp_hasFPowerSeriesOnBall this.compContinuousLinearMap).congr ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
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‖ₑ
⊢ HasFPowerSeriesOnBall (fun (x : ℝ) ↦ (1 + x) ^ a) (binomialSeries ℝ a) 0 1
have 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‖ₑ))
Tactic: convert! (Complex.reCLM.comp_hasFPowerSeriesOnBall this.compContinuousLinearMap).congr ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
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
⊢ Eq (α := FormalMultilinearSeries ℝ ℝ ℝ) (binomialSeries ℝ a : FormalMultilinearSeries ℝ ℝ ℝ)
    (Complex.reCLM.compFormalMultilinearSeries
        (FormalMultilinearSeries.compContinuousLinearMap (binomialSeries ℂ a : FormalMultilinearSeries ℝ ℂ ℂ)
            Complex.ofRealCLM :
          FormalMultilinearSeries ℝ ℝ ℂ) :
      FormalMultilinearSeries ℝ ℝ ℝ)
have 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 :
      ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
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
⊢ Eq (α := ℝ)
    (Function.comp (β := ℂ) (⇑Complex.reCLM : (a : ℂ) → ℝ)
      ((fun (x : ℂ) ↦ (1 + x) ^ (↑a : ℂ)) ∘ (⇑Complex.ofRealCLM : (a : ℝ) → ℂ)) x)
    ((fun (x : ℝ) ↦ (1 + x) ^ a) x)
have 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
Tactic: simp_all
Cleared hypotheses: this, hx
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
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
⊢ ((1 + (↑x : ℂ)) ^ (↑a : ℂ)).re = (1 + x) ^ a
have convert_2 : ((↑(1 + x) : ℂ) ^ (↑a : ℂ)).re = (1 + x) ^ a
Tactic: norm_cast
-- 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 this : 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 (𝕜 := ℝ)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (hypothesis)
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 (𝕜 := ℝ) (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 / (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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
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 (𝕜 := ℝ) (F := ℝ) (fun (x : ℝ) ↦ 1 / (1 - x) ^ a)
    (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) ↦ Ring.choose (a + (↑n : ℝ) - 1) n) 0 1
have 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 ℝ ℝ ℝ)
Tactic: convert! (Complex.reCLM.comp_hasFPowerSeriesOnBall this.compContinuousLinearMap).congr ?_ using 1
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
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 ℝ ℝ ℝ)
⊢ HasFPowerSeriesOnBall (𝕜 := ℝ) (F := ℝ) (fun (x : ℝ) ↦ 1 / (1 - x) ^ a)
    (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) ↦ Ring.choose (a + (↑n : ℝ) - 1) n) 0 1
have h₁ : 1 = 1 / ‖Complex.ofRealCLM‖ₑ
Tactic: convert! (Complex.reCLM.comp_hasFPowerSeriesOnBall this.compContinuousLinearMap).congr ?_ using 1
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
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‖ₑ
⊢ HasFPowerSeriesOnBall (𝕜 := ℝ) (F := ℝ) (fun (x : ℝ) ↦ 1 / (1 - x) ^ a)
    (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) ↦ Ring.choose (a + (↑n : ℝ) - 1) n) 0 1
have 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‖ₑ))
Tactic: convert! (Complex.reCLM.comp_hasFPowerSeriesOnBall this.compContinuousLinearMap).congr ?_ using 1
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
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
⊢ 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 ℝ ℝ ℝ)
have 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 :
      ℝ)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
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 : ℕ
⊢ 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) :
          ℂ) :
      ℝ)
have h : Ring.choose (a + (↑n : ℝ) - 1) n = (Ring.choose ((↑a : ℂ) + (↑n : ℂ) - 1) n).re
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
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 : ℕ
⊢ Ring.choose (a + (↑n : ℝ) - 1) n = (Ring.choose ((↑a : ℂ) + (↑n : ℂ) - 1) n).re
have h : Ring.choose (a + (↑n : ℝ) - 1) n = Ring.choose (a + (↑n : ℝ) - 1) n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (hypothesis)
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
⊢ Eq (α := ℝ)
    (Function.comp (β := ℂ) (⇑Complex.reCLM : (a : ℂ) → ℝ)
      ((fun (x : ℂ) ↦ 1 / (1 - x) ^ (↑a : ℂ)) ∘ (⇑Complex.ofRealCLM : (a : ℝ) → ℂ)) x)
    ((fun (x : ℝ) ↦ 1 / (1 - x) ^ a) x)
have this₁ : |x| < 1
Tactic: have : |x| < 1 := by simpa [enorm_eq_nnnorm] using hx
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (hypothesis)
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
⊢ Eq (α := ℝ)
    (Function.comp (β := ℂ) (⇑Complex.reCLM : (a : ℂ) → ℝ)
      ((fun (x : ℂ) ↦ 1 / (1 - x) ^ (↑a : ℂ)) ∘ (⇑Complex.ofRealCLM : (a : ℝ) → ℂ)) x)
    ((fun (x : ℝ) ↦ 1 / (1 - x) ^ a) x)
have this₁ : 0 ≤ 1 - x
Tactic: have : 0 ≤ 1 - x := by grind
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (hypothesis)
Goal:
a : ℕ
r : ℝ
hr : r ≠ 0
⊢ HasFPowerSeriesOnBall (𝕜 := ℝ) (F := ℝ) (fun (x : ℝ) ↦ 1 / (r - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) ↦ (r ^ (n + a + 1))⁻¹ * (↑((a + n).choose a) : ℝ)) 0 ‖r‖ₑ
have 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 : ℂ)‖ₑ
Tactic: have := (Complex.one_div_sub_pow_hasFPowerSeriesOnBall_zero a (z := r)
    (by simpa)).restrictScalars (𝕜 := ℝ)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (hypothesis)
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 (𝕜 := ℝ) (F := ℝ) (fun (x : ℝ) ↦ 1 / (r - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) ↦ (r ^ (n + a + 1))⁻¹ * (↑((a + n).choose a) : ℝ)) 0 ‖r‖ₑ
have 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 : ℂ)‖ₑ
Tactic: rw [← Complex.ofRealCLM.map_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
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 (𝕜 := ℝ) (F := ℝ) (fun (x : ℝ) ↦ 1 / (r - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) ↦ (r ^ (n + a + 1))⁻¹ * (↑((a + n).choose a) : ℝ)) 0 ‖r‖ₑ
have h : ∀ (x : ℝ),
  1 / (r - x) ^ (a + 1) =
    Function.comp (β := ℂ) (⇑Complex.reCLM : (a : ℂ) → ℝ)
      ((fun (x : ℂ) ↦ 1 / ((↑r : ℂ) - x) ^ (a + 1)) ∘ (⇑Complex.ofRealCLM : (a : ℝ) → ℂ)) x
Tactic: convert! (Complex.reCLM.comp_hasFPowerSeriesOnBall this.compContinuousLinearMap) using 2
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
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
⊢ HasFPowerSeriesOnBall (𝕜 := ℝ) (F := ℝ) (fun (x : ℝ) ↦ 1 / (r - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) ↦ (r ^ (n + a + 1))⁻¹ * (↑((a + n).choose a) : ℝ)) 0 ‖r‖ₑ
have 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 ℝ ℝ ℝ)
Tactic: convert! (Complex.reCLM.comp_hasFPowerSeriesOnBall this.compContinuousLinearMap) using 2
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
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 ℝ ℝ ℝ)
⊢ HasFPowerSeriesOnBall (𝕜 := ℝ) (F := ℝ) (fun (x : ℝ) ↦ 1 / (r - x) ^ (a + 1))
    (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) ↦ (r ^ (n + a + 1))⁻¹ * (↑((a + n).choose a) : ℝ)) 0 ‖r‖ₑ
have h₂ : ‖r‖ₑ = ‖(↑r : ℂ)‖ₑ / ‖Complex.ofRealCLM‖ₑ
Tactic: convert! (Complex.reCLM.comp_hasFPowerSeriesOnBall this.compContinuousLinearMap) using 2