awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
x y : E
hf : HasFiniteFPowerSeriesOnBall f p x n r
h : (↑‖y‖₊ : ℝ≥0∞) < r
z : E
hz : Membership.mem (γ := Set E) (Metric.eball 0 (r - (↑‖y‖₊ : ℝ≥0∞))) z
this : f (x + y + z) = (p.changeOrigin y).sum z
rw :
  HasSum (fun (n : ℕ) ↦ (p.changeOrigin y n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z) ((p.changeOrigin y).sum z)
⊢ HasSum (fun (n : ℕ) ↦ (p.changeOrigin y n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z) (f (x + y + z))

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
x y : E
hf : HasFiniteFPowerSeriesOnBall f p x n r
h : (↑‖y‖₊ : ℝ≥0∞) < r
z : E
hz : Membership.mem (γ := Set E) (Metric.eball 0 (r - (↑‖y‖₊ : ℝ≥0∞))) z
this : f (x + y + z) = (p.changeOrigin y).sum z
⊢ HasSum (fun (n : ℕ) ↦ (p.changeOrigin y n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z) ((p.changeOrigin y).sum z)

Tactic:
apply (p.changeOrigin y).hasSum_of_finite fun _ => p.changeOrigin_finite_of_finite hf.finite

Premises used: FormalMultilinearSeries.hasSum_of_finite, FormalMultilinearSeries.changeOrigin, FormalMultilinearSeries.changeOrigin_finite_of_finite, HasFiniteFPowerSeriesOnBall.finite
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
x y : E
hf : HasFiniteFPowerSeriesOnBall f p x n r
h : y ∈ Metric.eball x r
⊢ (↑‖y - x‖₊ : ℝ≥0∞) < r

Tactic:
simpa [edist_eq_enorm_sub] using h

Premises used: edist_eq_enorm_sub
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
x y : E
hf : HasFiniteFPowerSeriesOnBall f p x n r
h : y ∈ Metric.eball x r
⊢ (↑‖y - x‖₊ : ℝ≥0∞) < r

Tactic:
have : (‖y - x‖₊ : ℝ≥0∞) < r := by simpa [edist_eq_enorm_sub] using h
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
x y : E
hf : HasFiniteFPowerSeriesOnBall f p x n r
h : y ∈ Metric.eball x r
this : (↑‖y - x‖₊ : ℝ≥0∞) < r
⊢ HasFiniteFPowerSeriesOnBall f (p.changeOrigin (y - x)) (x + (y - x)) n (r - (↑‖y - x‖₊ : ℝ≥0∞))

Tactic:
have := hf.changeOrigin this
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
x y : E
hf : HasFiniteFPowerSeriesOnBall f p x n r
h : y ∈ Metric.eball x r
this_1 : (↑‖y - x‖₊ : ℝ≥0∞) < r
this : HasFiniteFPowerSeriesOnBall f (p.changeOrigin (y - x)) (x + (y - x)) n (r - (↑‖y - x‖₊ : ℝ≥0∞))
⊢ HasFiniteFPowerSeriesOnBall f (p.changeOrigin (y - x)) y n (r - (↑‖y - x‖₊ : ℝ≥0∞))

Tactic:
rw [add_sub_cancel] at this

Premises used: add_sub_cancel
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
x y : E
hf : HasFiniteFPowerSeriesOnBall f p x n r
h : y ∈ Metric.eball x r
this_1 : (↑‖y - x‖₊ : ℝ≥0∞) < r
this : HasFiniteFPowerSeriesOnBall f (p.changeOrigin (y - x)) y n (r - (↑‖y - x‖₊ : ℝ≥0∞))
⊢ CPolynomialAt 𝕜 f y

Tactic:
this.cpolynomialAt

Premises used: HasFiniteFPowerSeriesOnBall.cpolynomialAt
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
x y : E
hf : HasFiniteFPowerSeriesOnBall f p x n r
h : y ∈ Metric.eball x r
this_1 : (↑‖y - x‖₊ : ℝ≥0∞) < r
this : HasFiniteFPowerSeriesOnBall f (p.changeOrigin (y - x)) y n (r - (↑‖y - x‖₊ : ℝ≥0∞))
⊢ CPolynomialAt 𝕜 f y

Tactic:
exact this.cpolynomialAt

Premises used: HasFiniteFPowerSeriesOnBall.cpolynomialAt
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
x : E
hf : HasFiniteFPowerSeriesOnBall f p x n r
⊢ CPolynomialOn 𝕜 f (Metric.eball x r)

Tactic:
fun _y hy => hf.cpolynomialAt_of_mem hy

Premises used: HasFiniteFPowerSeriesOnBall.cpolynomialAt_of_mem, CPolynomialOn
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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
rw : ∀ (x : E), Membership.mem (γ := Set E) {x : E | CPolynomialAt 𝕜 f x} x → {x : E | CPolynomialAt 𝕜 f x} ∈ 𝓝 x
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x : E | CPolynomialAt 𝕜 f x}

Tactic:
rw [isOpen_iff_mem_nhds]

Premises used: isOpen_iff_mem_nhds
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
r : ℝ≥0∞
hr : HasFiniteFPowerSeriesOnBall f p x n r
⊢ {x : E | CPolynomialAt 𝕜 f x} ∈ 𝓝 x

Tactic:
mem_of_superset (Metric.eball_mem_nhds _ hr.r_pos) fun y hy => hr.cpolynomialAt_of_mem hy

Premises used: HasFiniteFPowerSeriesOnBall.toHasFPowerSeriesOnBall, Metric.eball_mem_nhds, HasFiniteFPowerSeriesOnBall.cpolynomialAt_of_mem, HasFPowerSeriesOnBall.r_pos, Filter.mem_of_superset
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
r : ℝ≥0∞
hr : HasFiniteFPowerSeriesOnBall f p x n r
⊢ {x : E | CPolynomialAt 𝕜 f x} ∈ 𝓝 x

Tactic:
exact mem_of_superset (Metric.eball_mem_nhds _ hr.r_pos) fun y hy => hr.cpolynomialAt_of_mem hy

Premises used: HasFiniteFPowerSeriesOnBall.toHasFPowerSeriesOnBall, Metric.eball_mem_nhds, HasFiniteFPowerSeriesOnBall.cpolynomialAt_of_mem, HasFPowerSeriesOnBall.r_pos, Filter.mem_of_superset
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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
h : CPolynomialAt 𝕜 f x
⊢ ∀ᶠ (y : E) in 𝓝 x, CPolynomialAt 𝕜 f y

Tactic:
(isOpen_cpolynomialAt 𝕜 f).mem_nhds h

Premises used: Set.Mem, isOpen_cpolynomialAt, Filter.Eventually, setOf, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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
h : CPolynomialAt 𝕜 f x
⊢ ∃ s ∈ 𝓝 x, CPolynomialOn 𝕜 f s

Tactic:
h.eventually_cpolynomialAt.exists_mem

Premises used: CPolynomialAt.eventually_cpolynomialAt, Filter.Eventually.exists_mem, CPolynomialOn
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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
h : CPolynomialAt 𝕜 f x
⊢ ∃ (r : ℝ), 0 < r ∧ CPolynomialOn 𝕜 f (Metric.ball x r)

Tactic:
Metric.isOpen_iff.mp (isOpen_cpolynomialAt _ _) _ h

Premises used: Set.Mem, isOpen_cpolynomialAt, setOf, Set.Subset, Metric.isOpen_iff, Iff.mp, CPolynomialAt, CPolynomialOn
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
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
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
rw : Fintype.card (Fin (k + l)) - s.card = k
rw₁ : k + l - s.card = k
rw₂ : k + l - l = k
rw₃ rw₄ : k = k
⊢ sᶜ.card = k

Tactic:
rw [Finset.card_compl, Fintype.card_fin, hs, add_tsub_cancel_right]

Premises used: Fintype.card_fin, Finset.card_compl, add_tsub_cancel_right
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
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
p : FormalMultilinearSeries 𝕜 E F
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
x y : E
⊢ Eq.{u_3 + 1} (α := F)
    (((p.changeOriginSeriesTerm k l s hs : (a : (i : Fin l) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F)
            fun (x_1 : Fin l) ↦ x :
          (a : (i : Fin k) → E) → F)
        fun (x : Fin k) ↦ y :
      F)
    ((p (k + l) : (a : (i : Fin (k + l)) → E) → F)
        (s.piecewise (π := fun (i : Fin (k + l)) ↦ E) (fun (x_1 : Fin (k + l)) ↦ x) fun (x : Fin (k + l)) ↦ y) :
      F)

Tactic:
ContinuousMultilinearMap.curryFinFinset_apply_const _ _ _ _ _

Premises used: ContinuousMultilinearMap.curryFinFinset_apply_const
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
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
p : FormalMultilinearSeries 𝕜 E F
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
⊢ ‖p.changeOriginSeriesTerm k l s hs‖ =
    norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + l)) ↦ E) F) (p (k + l))

Tactic:
simp only [changeOriginSeriesTerm, LinearIsometryEquiv.norm_map]

Premises used: LinearIsometryEquiv.norm_map, FormalMultilinearSeries.changeOriginSeriesTerm
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
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
p : FormalMultilinearSeries 𝕜 E F
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
⊢ ‖p.changeOriginSeriesTerm k l s hs‖₊ =
    nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + l)) ↦ E) F) (p (k + l))

Tactic:
simp only [changeOriginSeriesTerm, LinearIsometryEquiv.nnnorm_map]

Premises used: LinearIsometryEquiv.nnnorm_map, FormalMultilinearSeries.changeOriginSeriesTerm
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
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
p : FormalMultilinearSeries 𝕜 E F
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
x y : E
rw :
  nnnorm.{u_3} (E := F)
      (((p.changeOriginSeriesTerm k l s hs : (a : (i : Fin l) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F)
              fun (x_1 : Fin l) ↦ x :
            (a : (i : Fin k) → E) → F)
          fun (x : Fin k) ↦ y :
        F) ≤
    (‖p.changeOriginSeriesTerm k l s hs‖₊ * ∏ _i : Fin l, ‖x‖₊) * ∏ _i : Fin k, ‖y‖₊
⊢ nnnorm.{u_3} (E := F)
      (((p.changeOriginSeriesTerm k l s hs : (a : (i : Fin l) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F)
              fun (x_1 : Fin l) ↦ x :
            (a : (i : Fin k) → E) → F)
          fun (x : Fin k) ↦ y :
        F) ≤
    nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + l)) ↦ E) F) (p (k + l)) * ‖x‖₊ ^ l *
      ‖y‖₊ ^ k

Tactic:
rw [← p.nnnorm_changeOriginSeriesTerm k l s hs, ← Fin.prod_const, ← Fin.prod_const]

Premises used: Fin.prod_const, FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
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
p : FormalMultilinearSeries 𝕜 E F
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
x y : E
h :
  nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)
      ((p.changeOriginSeriesTerm k l s hs : (a : (i : Fin l) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F)
        fun (x_1 : Fin l) ↦ x) ≤
    ‖p.changeOriginSeriesTerm k l s hs‖₊ * ∏ _i : Fin l, ‖x‖₊
⊢ nnnorm.{u_3} (E := F)
      (((p.changeOriginSeriesTerm k l s hs : (a : (i : Fin l) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F)
              fun (x_1 : Fin l) ↦ x :
            (a : (i : Fin k) → E) → F)
          fun (x : Fin k) ↦ y :
        F) ≤
    (‖p.changeOriginSeriesTerm k l s hs‖₊ * ∏ _i : Fin l, ‖x‖₊) * ∏ _i : Fin k, ‖y‖₊

Tactic:
apply ContinuousMultilinearMap.le_of_opNNNorm_le

Premises used: ContinuousMultilinearMap.le_of_opNNNorm_le
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
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
p : FormalMultilinearSeries 𝕜 E F
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
x y : E
⊢ nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)
      ((p.changeOriginSeriesTerm k l s hs : (a : (i : Fin l) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F)
        fun (x_1 : Fin l) ↦ x) ≤
    ‖p.changeOriginSeriesTerm k l s hs‖₊ * ∏ _i : Fin l, ‖x‖₊

Tactic:
apply ContinuousMultilinearMap.le_opNNNorm

Premises used: ContinuousMultilinearMap.le_opNNNorm
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
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
p : FormalMultilinearSeries 𝕜 E F
k l : ℕ
simp_rw :
  Eq (α := ℝ≥0)
    (∑ a : { s : Finset (Fin (k + l)) // s.card = l }, ‖p.changeOriginSeriesTerm k l (↑a : Finset (Fin (k + l))) ⋯‖₊)
    (∑ x : { s : Finset (Fin (k + l)) // s.card = l },
      nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + l)) ↦ E) F) (p (k + l)))
⊢ Eq (α := ℝ≥0)
    (∑ a : { s : Finset (Fin (k + l)) // s.card = l }, ‖p.changeOriginSeriesTerm k l (↑a : Finset (Fin (k + l))) ⋯‖₊)
    (∑' (x : { s : Finset (Fin (k + l)) // s.card = l }),
      nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + l)) ↦ E) F) (p (k + l)))

Tactic:
simp_rw [tsum_fintype, nnnorm_changeOriginSeriesTerm (p := p) (k := k) (l := l)]

Premises used: tsum_fintype, FormalMultilinearSeries.nnnorm_changeOriginSeriesTerm
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
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
p : FormalMultilinearSeries 𝕜 E F
k l : ℕ
x : E
rw :
  nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)
      ((p.changeOriginSeries k l : (a : (i : Fin l) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F)
        fun (x_1 : Fin l) ↦ x) ≤
    HMul.hMul (α := ℝ≥0)
      (∑' (x : { s : Finset (Fin (k + l)) // s.card = l }),
        nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + l)) ↦ E) F) (p (k + l)))
      (∏ _i : Fin l, ‖x‖₊)
⊢ nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)
      ((p.changeOriginSeries k l : (a : (i : Fin l) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F)
        fun (x_1 : Fin l) ↦ x) ≤
    ∑' (x_1 : { s : Finset (Fin (k + l)) // s.card = l }),
      nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + l)) ↦ E) F) (p (k + l)) * ‖x‖₊ ^ l

Tactic:
rw [NNReal.tsum_mul_right, ← Fin.prod_const]

Premises used: NNReal.tsum_mul_right, Fin.prod_const
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
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
p : FormalMultilinearSeries 𝕜 E F
k l : ℕ
x : E
⊢ nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)
      ((p.changeOriginSeries k l : (a : (i : Fin l) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F)
        fun (x_1 : Fin l) ↦ x) ≤
    HMul.hMul (α := ℝ≥0)
      (∑' (x : { s : Finset (Fin (k + l)) // s.card = l }),
        nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + l)) ↦ E) F) (p (k + l)))
      (∏ _i : Fin l, ‖x‖₊)

Tactic:
(p.changeOriginSeries k l).le_of_opNNNorm_le (p.nnnorm_changeOriginSeries_le_tsum _ _) _

Premises used: ContinuousMultilinearMap.le_of_opNNNorm_le, FormalMultilinearSeries.nnnorm_changeOriginSeries_le_tsum, FormalMultilinearSeries.changeOriginSeries, Multiset.powerset, Multiset.ofList, Multiset.filter
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
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
p : FormalMultilinearSeries 𝕜 E F
k l : ℕ
x : E
⊢ nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)
      ((p.changeOriginSeries k l : (a : (i : Fin l) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F)
        fun (x_1 : Fin l) ↦ x) ≤
    HMul.hMul (α := ℝ≥0)
      (∑' (x : { s : Finset (Fin (k + l)) // s.card = l }),
        nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + l)) ↦ E) F) (p (k + l)))
      (∏ _i : Fin l, ‖x‖₊)

Tactic:
exact (p.changeOriginSeries k l).le_of_opNNNorm_le (p.nnnorm_changeOriginSeries_le_tsum _ _) _

Premises used: ContinuousMultilinearMap.le_of_opNNNorm_le, FormalMultilinearSeries.nnnorm_changeOriginSeries_le_tsum, FormalMultilinearSeries.changeOriginSeries
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
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
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
this :
  ∀ (k' l' : ℕ),
    k' = k →
      l' = l →
        ∀ (hkl : k + l = k' + l') (hs' : (Finset.map (finCongr hkl).toEmbedding s).card = l'),
          Eq (α := (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
            (Sigma.mk (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) k'
              (Sigma.mk (β := fun (l : ℕ) ↦ { s : Finset (Fin (k' + l)) // s.card = l }) l'
                (Subtype.mk (p := fun (s : Finset (Fin (k' + l'))) ↦ s.card = l')
                  (Finset.map (finCongr hkl).toEmbedding s) hs')))
            (Sigma.mk (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) k
              (Sigma.mk (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }) l
                (Subtype.mk (p := fun (s : Finset (Fin (k + l))) ↦ s.card = l) s hs)))
a : k + l - s.card = k
a₁ : s.card = l
⊢ Eq (α := (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
    (Sigma.mk (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) (k + l - s.card)
      (Sigma.mk (β := fun (l_1 : ℕ) ↦ { s_1 : Finset (Fin (k + l - s.card + l_1)) // s_1.card = l_1 }) s.card
        (Subtype.mk (p := fun (s_1 : Finset (Fin (k + l - s.card + s.card))) ↦ s_1.card = s.card)
          (Finset.map (Equiv.toEmbedding (finCongr ⋯)) s) ⋯)))
    (Sigma.mk (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) k
      (Sigma.mk (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }) l
        (Subtype.mk (p := fun (s : Finset (Fin (k + l))) ↦ s.card = l) s hs)))

Tactic:
apply this
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
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
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
this :
  ∀ (k' l' : ℕ),
    k' = k →
      l' = l →
        ∀ (hkl : k + l = k' + l') (hs' : (Finset.map (finCongr hkl).toEmbedding s).card = l'),
          Eq (α := (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
            (Sigma.mk (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) k'
              (Sigma.mk (β := fun (l : ℕ) ↦ { s : Finset (Fin (k' + l)) // s.card = l }) l'
                (Subtype.mk (p := fun (s : Finset (Fin (k' + l'))) ↦ s.card = l')
                  (Finset.map (finCongr hkl).toEmbedding s) hs')))
            (Sigma.mk (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) k
              (Sigma.mk (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }) l
                (Subtype.mk (p := fun (s : Finset (Fin (k + l))) ↦ s.card = l) s hs)))
⊢ k + l - s.card = k

Tactic:
simp only [hs, add_tsub_cancel_right]

Premises used: add_tsub_cancel_right
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
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
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
this :
  ∀ (k' l' : ℕ),
    k' = k →
      l' = l →
        ∀ (hkl : k + l = k' + l') (hs' : (Finset.map (finCongr hkl).toEmbedding s).card = l'),
          Eq (α := (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
            (Sigma.mk (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) k'
              (Sigma.mk (β := fun (l : ℕ) ↦ { s : Finset (Fin (k' + l)) // s.card = l }) l'
                (Subtype.mk (p := fun (s : Finset (Fin (k' + l'))) ↦ s.card = l')
                  (Finset.map (finCongr hkl).toEmbedding s) hs')))
            (Sigma.mk (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) k
              (Sigma.mk (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }) l
                (Subtype.mk (p := fun (s : Finset (Fin (k + l))) ↦ s.card = l) s hs)))
⊢ s.card = l

Tactic:
simp only [hs, add_tsub_cancel_right]

Premises used: add_tsub_cancel_right