awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ HasFiniteFPowerSeriesAt (f - g) (pf - pg) x (max n m)

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

Premises used: HasFiniteFPowerSeriesAt.neg, sub_eq_add_neg, HasFiniteFPowerSeriesAt.add
-- 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:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Premises used: CPolynomialAt.add, sub_eq_add_neg, CPolynomialAt.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
s : Set E
hf : CPolynomialOn 𝕜 f s
hg : CPolynomialOn 𝕜 g s
⊢ CPolynomialOn 𝕜 (f + g) s

Tactic:
fun z hz => (hf z hz).add (hg z hz)

Premises used: CPolynomialAt.add, 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
s : Set E
hf : CPolynomialOn 𝕜 f s
hg : CPolynomialOn 𝕜 g s
⊢ CPolynomialOn 𝕜 (f - g) s

Tactic:
fun z hz => (hf z hz).sub (hg z hz)

Premises used: CPolynomialAt.sub, CPolynomialOn
-- Module: Mathlib.Analysis.Analytic.CPolynomial
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)
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)
⊢ 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)

Tactic:
rw [Finset.sum_eq_single_of_mem _ (Finset.self_mem_range_succ _), zero_add]

Premises used: Finset.sum_eq_single_of_mem, zero_add, Finset.self_mem_range_succ
-- Module: Mathlib.Analysis.Analytic.CPolynomial
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)
    ((domDomCongr (Fintype.equivFinOfCardEq ⋯)
            (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)
⊢ 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 [toFormalMultilinearSeries, dif_pos rfl]

Premises used: dif_pos, ContinuousMultilinearMap.toFormalMultilinearSeries, rfl
-- Module: Mathlib.Analysis.Analytic.CPolynomial
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)
    ((domDomCongr (Fintype.equivFinOfCardEq ⋯)
            (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:
rfl
-- Module: Mathlib.Analysis.Analytic.CPolynomial
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 : ℕ
_ :
  m ∈ Finset.range (Fintype.card ι + 1) →
    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)
⊢ m ∈ Finset.range (Fintype.card ι + 1) →
    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)

Tactic:
_
-- Module: Mathlib.Analysis.Analytic.CPolynomial
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 ι
rw : Eq.{u_3 + 1} (α := F) ((0 : (a : (i : Fin m) → (i : ι) → Em i) → F) fun (x : Fin m) ↦ y : F) (0 : F)
⊢ 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)

Tactic:
rw [toFormalMultilinearSeries, dif_neg ne.symm]

Premises used: Ne.symm, ContinuousMultilinearMap.toFormalMultilinearSeries, dif_neg
-- Module: Mathlib.Analysis.Analytic.CPolynomial
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) ((0 : (a : (i : Fin m) → (i : ι) → Em i) → F) fun (x : Fin m) ↦ y : F) (0 : F)

Tactic:
rfl
-- Module: Mathlib.Analysis.Analytic.CPolynomial
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
x : (i : ι) → Em i
⊢ Membership.mem (γ := Set ((i : ι) → Em i)) (Metric.eball 0 ∞) x

Tactic:
simp only [Metric.eball_top, Set.mem_univ]

Premises used: Metric.eball_top, Set.mem_univ
-- Module: Mathlib.Analysis.Analytic.CPolynomial
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
s : Set ((i : ι) → Em i)
⊢ CPolynomialOn 𝕜 (F := F) (⇑f : (a : (i : ι) → Em i) → F) s

Tactic:
fun _ _ ↦ f.cpolynomialAt

Premises used: ContinuousMultilinearMap.cpolynomialAt, CPolynomialOn
-- Module: Mathlib.Analysis.Analytic.CPolynomial
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
s : Set ((i : ι) → Em i)
⊢ AnalyticOnNhd 𝕜 (F := F) (⇑f : (a : (i : ι) → Em i) → F) s

Tactic:
f.cpolynomialOn.analyticOnNhd

Premises used: ContinuousMultilinearMap.cpolynomialOn, CPolynomialOn.analyticOnNhd
-- Module: Mathlib.Analysis.Analytic.CPolynomial
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
s : Set ((i : ι) → Em i)
⊢ AnalyticOn 𝕜 (F := F) (⇑f : (a : (i : ι) → Em i) → F) s

Tactic:
f.analyticOnNhd.analyticOn

Premises used: AnalyticOnNhd.analyticOn, ContinuousMultilinearMap.analyticOnNhd
-- Module: Mathlib.Analysis.Analytic.CPolynomial
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
x : (i : ι) → Em i
⊢ AnalyticAt 𝕜 (F := F) (⇑f : (a : (i : ι) → Em i) → F) x

Tactic:
f.cpolynomialAt.analyticAt

Premises used: ContinuousMultilinearMap.cpolynomialAt, CPolynomialAt.analyticAt
-- Module: Mathlib.Analysis.Analytic.CPolynomial
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
x : (i : ι) → Em i
s : Set ((i : ι) → Em i)
⊢ AnalyticWithinAt 𝕜 (F := F) (⇑f : (a : (i : ι) → Em i) → F) s x

Tactic:
f.analyticAt.analyticWithinAt

Premises used: ContinuousMultilinearMap.analyticAt, AnalyticAt.analyticWithinAt
-- Module: Mathlib.Analysis.Analytic.CPolynomial
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
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)
⊢ 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) ∞

Tactic:
apply HasFiniteFPowerSeriesOnBall.mk' ?_ ENNReal.zero_lt_top ?_

Premises used: ENNReal.zero_lt_top, HasFiniteFPowerSeriesOnBall.mk'
-- Module: Mathlib.Analysis.Analytic.CPolynomial
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
hnc : ¬Fintype.card.{u_5} (Option ι) = m
⊢ f.toFormalMultilinearSeriesOfMultilinear (Em := Em) m = 0

Tactic:
apply dif_neg

Premises used: dif_neg
-- Module: Mathlib.Analysis.Analytic.CPolynomial
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
⊢ ¬Fintype.card.{u_5} (Option ι) = m

Tactic:
Nat.ne_of_lt hm

Premises used: Nat.ne_of_lt
-- Module: Mathlib.Analysis.Analytic.CPolynomial
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
⊢ ¬Fintype.card.{u_5} (Option ι) = m

Tactic:
exact Nat.ne_of_lt hm

Premises used: Nat.ne_of_lt
-- Module: Mathlib.Analysis.Analytic.CPolynomial
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)
_ :
  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)
⊢ 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:
_
-- Module: Mathlib.Analysis.Analytic.CPolynomial
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)
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)
⊢ 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:
rw [Finset.sum_eq_single_of_mem _ (Finset.self_mem_range_succ _), zero_add]

Premises used: Finset.sum_eq_single_of_mem, zero_add, Finset.self_mem_range_succ
-- Module: Mathlib.Analysis.Analytic.CPolynomial
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)
    ((ContinuousMultilinearMap.domDomCongr (Fintype.equivFinOfCardEq ⋯) (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)
⊢ 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 [toFormalMultilinearSeriesOfMultilinear, dif_pos rfl]

Premises used: dif_pos, ContinuousLinearMap.toFormalMultilinearSeriesOfMultilinear, rfl
-- Module: Mathlib.Analysis.Analytic.CPolynomial
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)
    ((ContinuousMultilinearMap.domDomCongr (Fintype.equivFinOfCardEq ⋯) (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:
rfl
-- Module: Mathlib.Analysis.Analytic.CPolynomial
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 : ℕ
_ :
  m ∈ Finset.range (Fintype.card.{u_5} (Option ι) + 1) →
    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)
⊢ m ∈ Finset.range (Fintype.card.{u_5} (Option ι) + 1) →
    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)

Tactic:
_
-- Module: Mathlib.Analysis.Analytic.CPolynomial
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 ι)
rw : Eq.{u_3 + 1} (α := F) ((0 : (a : (i : Fin m) → G × ((i : ι) → Em i)) → F) fun (x : Fin m) ↦ y : F) (0 : F)
⊢ 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)

Tactic:
rw [toFormalMultilinearSeriesOfMultilinear, dif_neg ne.symm]

Premises used: ContinuousLinearMap.toFormalMultilinearSeriesOfMultilinear, Ne.symm, dif_neg
-- Module: Mathlib.Analysis.Analytic.CPolynomial
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) ((0 : (a : (i : Fin m) → G × ((i : ι) → Em i)) → F) fun (x : Fin m) ↦ y : F) (0 : F)

Tactic:
rfl
-- Module: Mathlib.Analysis.Analytic.CPolynomial
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
x : G × ((i : ι) → Em i)
⊢ Membership.mem (γ := Set (G × ((i : ι) → Em i))) (Metric.eball 0 ∞) x

Tactic:
simp only [Metric.eball_top, Set.mem_univ]

Premises used: Metric.eball_top, Set.mem_univ