awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℂ)‖ₑ
⊢ 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 ℝ ℝ ℝ)
have 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 :
      ℝ)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a b : ℝ
⊢ HasFPowerSeriesOnBall (𝕜 := ℝ) (F := ℝ) (fun (x : ℝ) ↦ (b - a) / (1 - x) + a / HPow.hPow (β := ℕ) (1 - x) 2)
    (FormalMultilinearSeries.ofScalars ℝ fun (x : ℕ) ↦ a * (↑x : ℝ) + b) 0 1
have 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
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
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
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
⊢ HasFPowerSeriesOnBall (𝕜 := ℝ) (F := ℝ) (fun (x : ℝ) ↦ (b - a) / (1 - x) + a / HPow.hPow (β := ℕ) (1 - x) 2)
    (FormalMultilinearSeries.ofScalars ℝ fun (x : ℕ) ↦ a * (↑x : ℝ) + b) 0 1
have 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 ℝ ℝ ℝ)
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
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a b : ℝ
⊢ (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 ℝ ℝ ℝ)
have 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 :
      ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Binomial (goal)
Goal:
a b : ℝ
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 :
      ℝ)
have h : a * (↑n : ℝ) + b = b - a + a * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomial (goal)
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
⊢ (pf + pg) N = 0
have rw : pf N + 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]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomial (goal)
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
⊢ (pf + pg) N = 0
have rw₁ : 0 + 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]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomial (goal)
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
⊢ (pf + pg) N = 0
have rw₂ : HAdd.hAdd (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin N) ↦ E) F) 0 0 = 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]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomial (goal)
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
⊢ (pf + pg) N = 0
have rw₃ : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin N) ↦ E) F) 0 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]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomial (goal)
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
⊢ HasFiniteFPowerSeriesAt (f + g) (pf + pg) x (max n m)
have 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)
Tactic: rcases (hf.eventually.and hg.eventually).exists with ⟨r, hr⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomial (goal)
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
⊢ (-pf) m = 0
have rw : -pf m = 0
Tactic: rw [Pi.neg_apply, hf.finite m hm, neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomial (goal)
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
⊢ (-pf) m = 0
have rw₁ : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F) (-0) 0
Tactic: rw [Pi.neg_apply, hf.finite m hm, neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomial (goal)
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
⊢ (-pf) m = 0
have rw₂ : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F) 0 0
Tactic: rw [Pi.neg_apply, hf.finite m hm, neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomial (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_5
Em : ι → Type u_6
inst_3 : (i : ι) → NormedAddCommGroup (Em i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 Em F
y : (i : ι) → Em i
h : Membership.mem (γ := Set ((i : ι) → Em i)) (Metric.eball 0 ∞) y
⊢ Eq.{u_3 + 1} (α := F)
    (∑ i ∈ Finset.range (Fintype.card ι + 1),
        (f.toFormalMultilinearSeries (E := Em) i : (a : (i : Fin i) → (i : ι) → Em i) → F) fun (x : Fin i) ↦ y :
      F)
    ((f : (a : (i : ι) → Em i) → F) (0 + y) : F)
have rw : Eq.{u_3 + 1} (α := F)
  ((f.toFormalMultilinearSeries (E := Em) (Fintype.card ι) : (a : (i : Fin (Fintype.card ι)) → (i : ι) → Em i) → F)
      fun (x : Fin (Fintype.card ι)) ↦ y :
    F)
  ((f : (a : (i : ι) → Em i) → F) y : F)
Tactic: rw [Finset.sum_eq_single_of_mem _ (Finset.self_mem_range_succ _), zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomial (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_5
Em : ι → Type u_6
inst_3 : (i : ι) → NormedAddCommGroup (Em i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 Em F
y : (i : ι) → Em i
h : Membership.mem (γ := Set ((i : ι) → Em i)) (Metric.eball 0 ∞) y
rw :
  Eq.{u_3 + 1} (α := F)
    ((f.toFormalMultilinearSeries (E := Em) (Fintype.card ι) : (a : (i : Fin (Fintype.card ι)) → (i : ι) → Em i) → F)
        fun (x : Fin (Fintype.card ι)) ↦ y :
      F)
    ((f : (a : (i : ι) → Em i) → F) y : F)
⊢ Eq.{u_3 + 1} (α := F)
    (∑ i ∈ Finset.range (Fintype.card ι + 1),
        (f.toFormalMultilinearSeries (E := Em) i : (a : (i : Fin i) → (i : ι) → Em i) → F) fun (x : Fin i) ↦ y :
      F)
    ((f : (a : (i : ι) → Em i) → F) (0 + y) : F)
have rw₁ : ∀ b ∈ Finset.range (Fintype.card ι + 1),
  b ≠ Fintype.card ι →
    Eq.{u_3 + 1} (α := F)
      ((f.toFormalMultilinearSeries (E := Em) b : (a : (i : Fin b) → (i : ι) → Em i) → F) fun (x : Fin b) ↦ y : F)
      (0 : F)
Tactic: rw [Finset.sum_eq_single_of_mem _ (Finset.self_mem_range_succ _), zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomial (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_5
Em : ι → Type u_6
inst_3 : (i : ι) → NormedAddCommGroup (Em i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 Em F
y : (i : ι) → Em i
h : Membership.mem (γ := Set ((i : ι) → Em i)) (Metric.eball 0 ∞) y
⊢ Eq.{u_3 + 1} (α := F)
    ((f.toFormalMultilinearSeries (E := Em) (Fintype.card ι) : (a : (i : Fin (Fintype.card ι)) → (i : ι) → Em i) → F)
        fun (x : Fin (Fintype.card ι)) ↦ y :
      F)
    ((f : (a : (i : ι) → Em i) → F) y : F)
have rw : Eq.{u_3 + 1} (α := F)
  ((domDomCongr (Fintype.equivFinOfCardEq sorry)
          (f.compContinuousLinearMap (M₁ := fun (i : ι) ↦ (i : ι) → Em i) (M₁' := Em)
            (ContinuousLinearMap.proj (φ := Em))) :
        (a : (i : Fin (Fintype.card ι)) → (i : ι) → Em i) → F)
      fun (x : Fin (Fintype.card ι)) ↦ y :
    F)
  ((f : (a : (i : ι) → Em i) → F) y : F)
Tactic: rw [toFormalMultilinearSeries, dif_pos rfl]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomial (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_5
Em : ι → Type u_6
inst_3 : (i : ι) → NormedAddCommGroup (Em i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_5 : Fintype ι
f : ContinuousMultilinearMap 𝕜 Em F
y : (i : ι) → Em i
h : Membership.mem (γ := Set ((i : ι) → Em i)) (Metric.eball 0 ∞) y
m : ℕ
h_1 : m ∈ Finset.range (Fintype.card ι + 1)
ne : m ≠ Fintype.card ι
⊢ Eq.{u_3 + 1} (α := F)
    ((f.toFormalMultilinearSeries (E := Em) m : (a : (i : Fin m) → (i : ι) → Em i) → F) fun (x : Fin m) ↦ y : F) (0 : F)
have rw : Eq.{u_3 + 1} (α := F) ((0 : (a : (i : Fin m) → (i : ι) → Em i) → F) fun (x : Fin m) ↦ y : F) (0 : F)
Tactic: rw [toFormalMultilinearSeries, dif_neg ne.symm]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomial (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst_5 : (i : ι) → NormedAddCommGroup (Em i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_7 : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F
⊢ HasFiniteFPowerSeriesOnBall (𝕜 := 𝕜) (F := F)
    (fun (p : G × ((i : ι) → Em i)) ↦
      (((f : (a : G) → ContinuousMultilinearMap 𝕜 Em F) p.1 : ContinuousMultilinearMap 𝕜 Em F) :
          (a : (i : ι) → Em i) → F)
        p.2)
    (f.toFormalMultilinearSeriesOfMultilinear (Em := Em)) 0 (Fintype.card.{u_5} (Option ι) + 1) ∞
have apply : ∀ (m : ℕ), Fintype.card.{u_5} (Option ι) + 1 ≤ m → f.toFormalMultilinearSeriesOfMultilinear (Em := Em) m = 0
Tactic: apply HasFiniteFPowerSeriesOnBall.mk' ?_ ENNReal.zero_lt_top ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomial (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst_5 : (i : ι) → NormedAddCommGroup (Em i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_7 : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F
apply : ∀ (m : ℕ), Fintype.card.{u_5} (Option ι) + 1 ≤ m → f.toFormalMultilinearSeriesOfMultilinear (Em := Em) m = 0
⊢ HasFiniteFPowerSeriesOnBall (𝕜 := 𝕜) (F := F)
    (fun (p : G × ((i : ι) → Em i)) ↦
      (((f : (a : G) → ContinuousMultilinearMap 𝕜 Em F) p.1 : ContinuousMultilinearMap 𝕜 Em F) :
          (a : (i : ι) → Em i) → F)
        p.2)
    (f.toFormalMultilinearSeriesOfMultilinear (Em := Em)) 0 (Fintype.card.{u_5} (Option ι) + 1) ∞
have apply₁ : ∀ (y : G × ((i : ι) → Em i)),
  Membership.mem (γ := Set (G × ((i : ι) → Em i))) (Metric.eball 0 ∞) y →
    Eq.{u_3 + 1} (α := F)
      (∑ i ∈ Finset.range (Fintype.card.{u_5} (Option ι) + 1),
          (f.toFormalMultilinearSeriesOfMultilinear (Em := Em) i : (a : (i : Fin i) → G × ((i : ι) → Em i)) → F)
            fun (x : Fin i) ↦ y :
        F)
      ((((f : (a : G) → ContinuousMultilinearMap 𝕜 Em F) (0 + y).1 : ContinuousMultilinearMap 𝕜 Em F) :
            (a : (i : ι) → Em i) → F)
          (0 + y).2 :
        F)
Tactic: apply HasFiniteFPowerSeriesOnBall.mk' ?_ ENNReal.zero_lt_top ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomial (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst_5 : (i : ι) → NormedAddCommGroup (Em i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_7 : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F
m : ℕ
hm : Fintype.card.{u_5} (Option ι) + 1 ≤ m
⊢ f.toFormalMultilinearSeriesOfMultilinear (Em := Em) m = 0
have hnc : ¬Fintype.card.{u_5} (Option ι) = m
Tactic: apply dif_neg
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomial (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst_5 : (i : ι) → NormedAddCommGroup (Em i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_7 : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F
y : G × ((i : ι) → Em i)
h : Membership.mem (γ := Set (G × ((i : ι) → Em i))) (Metric.eball 0 ∞) y
⊢ Eq.{u_3 + 1} (α := F)
    (∑ i ∈ Finset.range (Fintype.card.{u_5} (Option ι) + 1),
        (f.toFormalMultilinearSeriesOfMultilinear (Em := Em) i : (a : (i : Fin i) → G × ((i : ι) → Em i)) → F)
          fun (x : Fin i) ↦ y :
      F)
    ((((f : (a : G) → ContinuousMultilinearMap 𝕜 Em F) (0 + y).1 : ContinuousMultilinearMap 𝕜 Em F) :
          (a : (i : ι) → Em i) → F)
        (0 + y).2 :
      F)
have rw : Eq.{u_3 + 1} (α := F)
  ((f.toFormalMultilinearSeriesOfMultilinear (Em := Em) (Fintype.card.{u_5} (Option ι)) :
        (a : (i : Fin (Fintype.card (Option ι))) → G × ((i : ι) → Em i)) → F)
      fun (x : Fin (Fintype.card.{u_5} (Option ι))) ↦ y :
    F)
  ((((f : (a : G) → ContinuousMultilinearMap 𝕜 Em F) y.1 : ContinuousMultilinearMap 𝕜 Em F) : (a : (i : ι) → Em i) → F)
      y.2 :
    F)
Tactic: rw [Finset.sum_eq_single_of_mem _ (Finset.self_mem_range_succ _), zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomial (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst_5 : (i : ι) → NormedAddCommGroup (Em i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_7 : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F
y : G × ((i : ι) → Em i)
h : Membership.mem (γ := Set (G × ((i : ι) → Em i))) (Metric.eball 0 ∞) y
rw :
  Eq.{u_3 + 1} (α := F)
    ((f.toFormalMultilinearSeriesOfMultilinear (Em := Em) (Fintype.card.{u_5} (Option ι)) :
          (a : (i : Fin (Fintype.card (Option ι))) → G × ((i : ι) → Em i)) → F)
        fun (x : Fin (Fintype.card.{u_5} (Option ι))) ↦ y :
      F)
    ((((f : (a : G) → ContinuousMultilinearMap 𝕜 Em F) y.1 : ContinuousMultilinearMap 𝕜 Em F) :
          (a : (i : ι) → Em i) → F)
        y.2 :
      F)
⊢ Eq.{u_3 + 1} (α := F)
    (∑ i ∈ Finset.range (Fintype.card.{u_5} (Option ι) + 1),
        (f.toFormalMultilinearSeriesOfMultilinear (Em := Em) i : (a : (i : Fin i) → G × ((i : ι) → Em i)) → F)
          fun (x : Fin i) ↦ y :
      F)
    ((((f : (a : G) → ContinuousMultilinearMap 𝕜 Em F) (0 + y).1 : ContinuousMultilinearMap 𝕜 Em F) :
          (a : (i : ι) → Em i) → F)
        (0 + y).2 :
      F)
have rw₁ : ∀ b ∈ Finset.range (Fintype.card.{u_5} (Option ι) + 1),
  b ≠ Fintype.card.{u_5} (Option ι) →
    Eq.{u_3 + 1} (α := F)
      ((f.toFormalMultilinearSeriesOfMultilinear (Em := Em) b : (a : (i : Fin b) → G × ((i : ι) → Em i)) → F)
          fun (x : Fin b) ↦ y :
        F)
      (0 : F)
Tactic: rw [Finset.sum_eq_single_of_mem _ (Finset.self_mem_range_succ _), zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomial (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst_5 : (i : ι) → NormedAddCommGroup (Em i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_7 : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F
y : G × ((i : ι) → Em i)
h : Membership.mem (γ := Set (G × ((i : ι) → Em i))) (Metric.eball 0 ∞) y
⊢ Eq.{u_3 + 1} (α := F)
    ((f.toFormalMultilinearSeriesOfMultilinear (Em := Em) (Fintype.card.{u_5} (Option ι)) :
          (a : (i : Fin (Fintype.card (Option ι))) → G × ((i : ι) → Em i)) → F)
        fun (x : Fin (Fintype.card.{u_5} (Option ι))) ↦ y :
      F)
    ((((f : (a : G) → ContinuousMultilinearMap 𝕜 Em F) y.1 : ContinuousMultilinearMap 𝕜 Em F) :
          (a : (i : ι) → Em i) → F)
        y.2 :
      F)
have rw : Eq.{u_3 + 1} (α := F)
  ((ContinuousMultilinearMap.domDomCongr (Fintype.equivFinOfCardEq sorry) (f.continuousMultilinearMapOption (E := Em)) :
        (a : (i : Fin (Fintype.card (Option ι))) → G × ((i : ι) → Em i)) → F)
      fun (x : Fin (Fintype.card.{u_5} (Option ι))) ↦ y :
    F)
  ((((f : (a : G) → ContinuousMultilinearMap 𝕜 Em F) y.1 : ContinuousMultilinearMap 𝕜 Em F) : (a : (i : ι) → Em i) → F)
      y.2 :
    F)
Tactic: rw [toFormalMultilinearSeriesOfMultilinear, dif_pos rfl]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomial (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst_5 : (i : ι) → NormedAddCommGroup (Em i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_7 : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F
y : G × ((i : ι) → Em i)
h : Membership.mem (γ := Set (G × ((i : ι) → Em i))) (Metric.eball 0 ∞) y
m : ℕ
h_1 : m ∈ Finset.range (Fintype.card.{u_5} (Option ι) + 1)
ne : m ≠ Fintype.card.{u_5} (Option ι)
⊢ Eq.{u_3 + 1} (α := F)
    ((f.toFormalMultilinearSeriesOfMultilinear (Em := Em) m : (a : (i : Fin m) → G × ((i : ι) → Em i)) → F)
        fun (x : Fin m) ↦ y :
      F)
    (0 : F)
have rw : Eq.{u_3 + 1} (α := F) ((0 : (a : (i : Fin m) → G × ((i : ι) → Em i)) → F) fun (x : Fin m) ↦ y : F) (0 : F)
Tactic: rw [toFormalMultilinearSeriesOfMultilinear, dif_neg ne.symm]