awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) → F :=
  fun (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) ↦
    ((p.changeOriginSeriesTerm (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))
              (s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β := fun (l : ℕ) ↦
                { s_1 :
                  Finset (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                  s_1.card = l }))
              (↑(s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).snd (β := fun (l : ℕ) ↦
                    { s_1 :
                      Finset
                        (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                      s_1.card = l })) :
                Finset (Fin (s.fst + s.snd.fst)))
              ⋯ :
            (a : (i : Fin s.snd.fst) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin s.fst) ↦ E) F)
          fun
            (x_1 :
              Fin
                (s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β := fun (l : ℕ) ↦
                  { s_1 :
                    Finset
                      (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                    s_1.card = l }))) ↦
          x :
        (a : (i : Fin s.fst) → E) → F)
      fun (x : Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))) ↦ y
⊢ Function.support f ⊆
    preimage (β := (n : ℕ) × Finset (Fin n))
      (⇑changeOriginIndexEquiv :
        (a : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) → (n : ℕ) × Finset (Fin n))
      (Sigma.fst (β := fun (n : ℕ) ↦ Finset (Fin n)) ⁻¹' {m : ℕ | m < n})
have ht : ∀ (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
  (hs :
    s ∉
      preimage (β := (n : ℕ) × Finset (Fin n))
        (⇑changeOriginIndexEquiv :
          (a : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) → (n : ℕ) × Finset (Fin n))
        (Sigma.fst (β := fun (n : ℕ) ↦ Finset (Fin n)) ⁻¹' {m : ℕ | m < n})),
  f s = 0
Tactic: refine fun s ↦ Not.imp_symm fun hs ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (hypothesis)
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
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) → F :=
  fun (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) ↦
    ((p.changeOriginSeriesTerm (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))
              (s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β := fun (l : ℕ) ↦
                { s_1 :
                  Finset (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                  s_1.card = l }))
              (↑(s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).snd (β := fun (l : ℕ) ↦
                    { s_1 :
                      Finset
                        (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                      s_1.card = l })) :
                Finset (Fin (s.fst + s.snd.fst)))
              ⋯ :
            (a : (i : Fin s.snd.fst) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin s.fst) ↦ E) F)
          fun
            (x_1 :
              Fin
                (s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β := fun (l : ℕ) ↦
                  { s_1 :
                    Finset
                      (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                    s_1.card = l }))) ↦
          x :
        (a : (i : Fin s.fst) → E) → F)
      fun (x : Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))) ↦ y
s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }
hs :
  s ∉
    preimage (β := (n : ℕ) × Finset (Fin n))
      (⇑changeOriginIndexEquiv :
        (a : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) → (n : ℕ) × Finset (Fin n))
      (Sigma.fst (β := fun (n : ℕ) ↦ Finset (Fin n)) ⁻¹' {m : ℕ | m < n})
⊢ f s = 0
have hs₁ : n ≤
  s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) +
    s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β := fun (l : ℕ) ↦
      { s_1 : Finset (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
        s_1.card = l })
Tactic: simp only [preimage_setOf_eq, changeOriginIndexEquiv_apply_fst, mem_setOf, not_lt] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (hypothesis)
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
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) → F :=
  fun (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) ↦
    ((p.changeOriginSeriesTerm (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))
              (s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β := fun (l : ℕ) ↦
                { s_1 :
                  Finset (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                  s_1.card = l }))
              (↑(s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).snd (β := fun (l : ℕ) ↦
                    { s_1 :
                      Finset
                        (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                      s_1.card = l })) :
                Finset (Fin (s.fst + s.snd.fst)))
              ⋯ :
            (a : (i : Fin s.snd.fst) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin s.fst) ↦ E) F)
          fun
            (x_1 :
              Fin
                (s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β := fun (l : ℕ) ↦
                  { s_1 :
                    Finset
                      (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                    s_1.card = l }))) ↦
          x :
        (a : (i : Fin s.fst) → E) → F)
      fun (x : Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))) ↦ y
⊢ (p.changeOrigin x).sum y = p.sum (x + y)
have finsupp : (Function.support f).Finite
Tactic: have finsupp : f.support.Finite := by
    apply Set.Finite.subset (s := changeOriginIndexEquiv ⁻¹' Sigma.fst ⁻¹' {m | m < n})
    · apply Set.Finite.preimage (Equiv.injective _).injOn
      simp_rw [← {m | m < n}.iUnion_of_singleton_coe, preimage_iUnion, ← range_sigmaMk]
      exact finite_iUnion fun _ ↦ finite_range _
    · refine fun s ↦ Not.imp_symm fun hs ↦ ?_
      simp only [preimage_setOf_eq, changeOriginIndexEquiv_apply_fst, mem_setOf, not_lt] at hs
      dsimp only [f]
      rw [changeOriginSeriesTerm_bound p hn _ _ _ hs, ContinuousMultilinearMap.zero_apply,
        ContinuousMultilinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) → F :=
  fun (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) ↦
    ((p.changeOriginSeriesTerm (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))
              (s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β := fun (l : ℕ) ↦
                { s_1 :
                  Finset (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                  s_1.card = l }))
              (↑(s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).snd (β := fun (l : ℕ) ↦
                    { s_1 :
                      Finset
                        (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                      s_1.card = l })) :
                Finset (Fin (s.fst + s.snd.fst)))
              ⋯ :
            (a : (i : Fin s.snd.fst) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin s.fst) ↦ E) F)
          fun
            (x_1 :
              Fin
                (s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β := fun (l : ℕ) ↦
                  { s_1 :
                    Finset
                      (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                    s_1.card = l }))) ↦
          x :
        (a : (i : Fin s.fst) → E) → F)
      fun (x : Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))) ↦ y
finsupp : (Function.support f).Finite
k l : ℕ
⊢ HasSum.{u_3, 0} (α := F)
    (fun (x : { s : Finset (Fin (k + l)) // s.card = l }) ↦
      f
        (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 x)))
    (((p.changeOriginSeries k l : (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)
have simp_rw : HasSum.{u_3, 0} (α := F)
  (fun (x : { s : Finset (Fin (k + l)) // s.card = l }) ↦
    f
      (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 x)))
  (∑ a : { s : Finset (Fin (k + l)) // s.card = l },
    ((p.changeOriginSeriesTerm k l (↑a : Finset (Fin (k + l))) sorry :
            (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)
Tactic: simp_rw [changeOriginSeries, ContinuousMultilinearMap.sum_apply]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (hypothesis)
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
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) → F :=
  fun (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) ↦
    ((p.changeOriginSeriesTerm (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))
              (s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β := fun (l : ℕ) ↦
                { s_1 :
                  Finset (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                  s_1.card = l }))
              (↑(s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).snd (β := fun (l : ℕ) ↦
                    { s_1 :
                      Finset
                        (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                      s_1.card = l })) :
                Finset (Fin (s.fst + s.snd.fst)))
              ⋯ :
            (a : (i : Fin s.snd.fst) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin s.fst) ↦ E) F)
          fun
            (x_1 :
              Fin
                (s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β := fun (l : ℕ) ↦
                  { s_1 :
                    Finset
                      (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                    s_1.card = l }))) ↦
          x :
        (a : (i : Fin s.fst) → E) → F)
      fun (x : Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))) ↦ y
finsupp : (Function.support f).Finite
⊢ (p.changeOrigin x).sum y = p.sum (x + y)
have hfkl : ∀ (k l : ℕ),
  HasSum.{u_3, 0} (α := F)
    (fun (x : { s : Finset (Fin (k + l)) // s.card = l }) ↦
      f
        (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 x)))
    (((p.changeOriginSeries k l : (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)
Tactic: have hfkl k l : HasSum (f ⟨k, l, ·⟩) (changeOriginSeries p k l (fun _ ↦ x) fun _ ↦ y) := by
    simp_rw [changeOriginSeries, ContinuousMultilinearMap.sum_apply]; apply hasSum_fintype
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (hypothesis)
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
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) → F :=
  fun (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) ↦
    ((p.changeOriginSeriesTerm (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))
              (s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β := fun (l : ℕ) ↦
                { s_1 :
                  Finset (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                  s_1.card = l }))
              (↑(s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).snd (β := fun (l : ℕ) ↦
                    { s_1 :
                      Finset
                        (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                      s_1.card = l })) :
                Finset (Fin (s.fst + s.snd.fst)))
              ⋯ :
            (a : (i : Fin s.snd.fst) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin s.fst) ↦ E) F)
          fun
            (x_1 :
              Fin
                (s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β := fun (l : ℕ) ↦
                  { s_1 :
                    Finset
                      (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                    s_1.card = l }))) ↦
          x :
        (a : (i : Fin s.fst) → E) → F)
      fun (x : Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))) ↦ y
finsupp : (Function.support f).Finite
hfkl :
  ∀ (k l : ℕ),
    HasSum.{u_3, 0} (α := F)
      (fun (x : { s : Finset (Fin (k + l)) // s.card = l }) ↦
        f
          (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 x)))
      (((p.changeOriginSeries k l : (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)
k m : ℕ
hm : m ∉ Finset.range n
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)
    ((p.changeOriginSeries k m : (a : (i : Fin m) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F)
      fun (x_1 : Fin m) ↦ x)
    0
have hm₁ : n ≤ m
Tactic: rw [Finset.mem_range, not_lt] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) → F :=
  fun (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) ↦
    ((p.changeOriginSeriesTerm (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))
              (s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β := fun (l : ℕ) ↦
                { s_1 :
                  Finset (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                  s_1.card = l }))
              (↑(s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).snd (β := fun (l : ℕ) ↦
                    { s_1 :
                      Finset
                        (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                      s_1.card = l })) :
                Finset (Fin (s.fst + s.snd.fst)))
              ⋯ :
            (a : (i : Fin s.snd.fst) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin s.fst) ↦ E) F)
          fun
            (x_1 :
              Fin
                (s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β := fun (l : ℕ) ↦
                  { s_1 :
                    Finset
                      (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                    s_1.card = l }))) ↦
          x :
        (a : (i : Fin s.fst) → E) → F)
      fun (x : Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))) ↦ y
finsupp : (Function.support f).Finite
hfkl :
  ∀ (k l : ℕ),
    HasSum.{u_3, 0} (α := F)
      (fun (x : { s : Finset (Fin (k + l)) // s.card = l }) ↦
        f
          (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 x)))
      (((p.changeOriginSeries k l : (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)
k m : ℕ
hm : n ≤ m
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)
    ((p.changeOriginSeries k m : (a : (i : Fin m) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F)
      fun (x_1 : Fin m) ↦ x)
    0
have rw : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)
  ((0 : (a : (i : Fin m) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F) fun (x_1 : Fin m) ↦ x) 0
Tactic: rw [changeOriginSeries_finite_of_finite _ hn _ (le_add_of_le_right hm),
        ContinuousMultilinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (hypothesis)
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
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x y : E
f : (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) → F :=
  fun (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) ↦
    ((p.changeOriginSeriesTerm (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))
              (s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β := fun (l : ℕ) ↦
                { s_1 :
                  Finset (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                  s_1.card = l }))
              (↑(s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).snd (β := fun (l : ℕ) ↦
                    { s_1 :
                      Finset
                        (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                      s_1.card = l })) :
                Finset (Fin (s.fst + s.snd.fst)))
              ⋯ :
            (a : (i : Fin s.snd.fst) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin s.fst) ↦ E) F)
          fun
            (x_1 :
              Fin
                (s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β := fun (l : ℕ) ↦
                  { s_1 :
                    Finset
                      (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                    s_1.card = l }))) ↦
          x :
        (a : (i : Fin s.fst) → E) → F)
      fun (x : Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))) ↦ y
finsupp : (Function.support f).Finite
hfkl :
  ∀ (k l : ℕ),
    HasSum.{u_3, 0} (α := F)
      (fun (x : { s : Finset (Fin (k + l)) // s.card = l }) ↦
        f
          (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 x)))
      (((p.changeOriginSeries k l : (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)
hfk :
  ∀ (k : ℕ),
    HasSum.{u_3, 0} (α := F)
      (fun (x : (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) ↦
        f (Sigma.mk (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) k x))
      ((p.changeOrigin x k : (a : (i : Fin k) → E) → F) fun (x : Fin k) ↦ y : F)
⊢ (p.changeOrigin x).sum y = p.sum (x + y)
have hf : HasSum f ((p.changeOrigin x).sum y)
Tactic: have hf : HasSum f ((p.changeOrigin x).sum y) :=
    ((p.changeOrigin x).hasSum_of_finite (fun _ ↦ changeOrigin_finite_of_finite p hn) _)
      |>.sigma_of_hasSum hfk (summable_of_hasFiniteSupport finsupp)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (hypothesis)
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
⊢ f (x + y + z) = (p.changeOrigin y).sum z
have hz₁ : (↑‖y‖₊ : ℝ≥0∞) + ‖z‖ₑ < r
Tactic: rw [mem_eball_zero_iff, lt_tsub_iff_right, add_comm] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
x y : E
hf : HasFiniteFPowerSeriesOnBall f p x n r
h : (↑‖y‖₊ : ℝ≥0∞) < r
z : E
hz : (↑‖y‖₊ : ℝ≥0∞) + ‖z‖ₑ < r
⊢ f (x + y + z) = (p.changeOrigin y).sum z
have rw : Membership.mem (γ := Set E) (Metric.eball 0 r) (y + z)
Tactic: rw [p.changeOrigin_eval_of_finite hf.finite, add_assoc, hf.sum]