awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (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 : ℕ
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F →L[𝕜] E →L[𝕜] F)
        (↑(↑(continuousMultilinearCurryFin1 𝕜 E F) :
              ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F ≃L[𝕜] E →L[𝕜] F) :
          ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F →L[𝕜] E →L[𝕜] F) *
      norm (E :=
        ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E)
          (ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F))
        (p.changeOriginSeries 1 n) ≤
    norm (E :=
      ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E)
        (ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F))
      (p.changeOriginSeries 1 n)
have apply : norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F →L[𝕜] E →L[𝕜] F)
    (↑(↑(continuousMultilinearCurryFin1 𝕜 E F) : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F ≃L[𝕜] E →L[𝕜] F) :
      ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F →L[𝕜] E →L[𝕜] F) ≤
  1
Tactic: apply mul_le_of_le_one_left (norm_nonneg _)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (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 : ℕ
hp : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) 0
this :
  Eq (α :=
    ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E)
      (ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F))
    (p.changeOriginSeries 1 n) 0
⊢ p.derivSeries n = 0
have H : ∀ (v : (i : Fin n) → E) (x : E),
  Eq.{u_3 + 1} (α := F) ((((p.derivSeries n : (a : (i : Fin n) → E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) x : F)
    ((((0 : (a : (i : Fin n) → E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) x : F)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (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 : ℕ
hp : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) 0
⊢ p.derivSeries n = 0
have suffices : Eq (α :=
  ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E)
    (ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F))
  (p.changeOriginSeries 1 n) 0
Tactic: suffices p.changeOriginSeries 1 n = 0 by ext v; simp [derivSeries, this]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (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 : ℕ
hp : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) 0
⊢ Eq (α :=
    ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E)
      (ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F))
    (p.changeOriginSeries 1 n) 0
have apply : ∀ (s : { s : Finset (Fin (1 + n)) // s.card = n })
  (hs : Membership.mem (γ := Finset { s : Finset (Fin (1 + n)) // s.card = n }) Finset.univ s),
  p.changeOriginSeriesTerm 1 n (↑s : Finset (Fin (1 + n))) sorry = 0
Tactic: apply Finset.sum_eq_zero (fun s hs ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (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 : ℕ
hp : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) 0
s : { s : Finset (Fin (1 + n)) // s.card = n }
hs : Membership.mem (γ := Finset { s : Finset (Fin (1 + n)) // s.card = n }) Finset.univ s
⊢ p.changeOriginSeriesTerm 1 n (↑s : Finset (Fin (1 + n))) ⋯ = 0
have this : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (1 + n)) ↦ E) F) (p (1 + n)) 0
Tactic: have : p (1 + n) = 0 := p.congr_zero (by abel) hp
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (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 : ℕ
hp : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 1)) ↦ E) F) (p (n + 1)) 0
s : { s : Finset (Fin (1 + n)) // s.card = n }
hs : Membership.mem (γ := Finset { s : Finset (Fin (1 + n)) // s.card = n }) Finset.univ s
this : Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (1 + n)) ↦ E) F) (p (1 + n)) 0
⊢ p.changeOriginSeriesTerm 1 n (↑s : Finset (Fin (1 + n))) ⋯ = 0
have simp : Eq (α :=
  ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E)
    (ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F))
  ((ContinuousMultilinearMap.curryFinFinset 𝕜 E F sorry sorry :
      (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin (1 + n)) ↦ E) F) →
        ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F))
    0)
  0
Tactic: simp [changeOriginSeriesTerm, this]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (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
inst_5 : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : (↑‖x‖₊ : ℝ≥0∞) + (↑‖y‖₊ : ℝ≥0∞) < p.radius
⊢ (p.changeOrigin x).sum y = p.sum (x + y)
have x_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 p.radius) x
Tactic: have x_mem_ball : x ∈ Metric.eball (0 : E) p.radius :=
    mem_eball_zero_iff.2 ((le_add_right le_rfl).trans_lt h)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (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
inst_5 : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : (↑‖x‖₊ : ℝ≥0∞) + (↑‖y‖₊ : ℝ≥0∞) < p.radius
x_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 p.radius) x
⊢ Membership.mem (γ := Set E) (Metric.eball 0 (p.changeOrigin x).radius) y
have refine : ‖y‖ₑ < p.radius - (↑‖x‖₊ : ℝ≥0∞)
Tactic: refine mem_eball_zero_iff.2 (lt_of_lt_of_le ?_ p.changeOrigin_radius)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (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
inst_5 : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : (↑‖x‖₊ : ℝ≥0∞) + (↑‖y‖₊ : ℝ≥0∞) < p.radius
x_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 p.radius) x
⊢ ‖y‖ₑ < p.radius - (↑‖x‖₊ : ℝ≥0∞)
have rwa : ‖y‖ₑ + (↑‖x‖₊ : ℝ≥0∞) < p.radius
Tactic: rwa [lt_tsub_iff_right, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (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
inst_5 : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : (↑‖x‖₊ : ℝ≥0∞) + (↑‖y‖₊ : ℝ≥0∞) < p.radius
x_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 p.radius) x
rwa : ‖y‖ₑ + (↑‖x‖₊ : ℝ≥0∞) < p.radius
⊢ ‖y‖ₑ < p.radius - (↑‖x‖₊ : ℝ≥0∞)
have rwa₁ : (↑‖x‖₊ : ℝ≥0∞) + ‖y‖ₑ < p.radius
Tactic: rwa [lt_tsub_iff_right, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (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
inst_5 : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : (↑‖x‖₊ : ℝ≥0∞) + (↑‖y‖₊ : ℝ≥0∞) < p.radius
x_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 p.radius) x
⊢ (p.changeOrigin x).sum y = p.sum (x + y)
have y_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 (p.changeOrigin x).radius) y
Tactic: have y_mem_ball : y ∈ Metric.eball (0 : E) (p.changeOrigin x).radius := by
    refine mem_eball_zero_iff.2 (lt_of_lt_of_le ?_ p.changeOrigin_radius)
    rwa [lt_tsub_iff_right, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (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
inst_5 : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : (↑‖x‖₊ : ℝ≥0∞) + (↑‖y‖₊ : ℝ≥0∞) < p.radius
x_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 p.radius) x
y_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 (p.changeOrigin x).radius) y
⊢ Membership.mem (γ := Set E) (Metric.eball 0 p.radius) (x + y)
have refine : ‖x + y‖ₑ ≤ (↑‖x‖₊ : ℝ≥0∞) + (↑‖y‖₊ : ℝ≥0∞)
Tactic: refine mem_eball_zero_iff.2 (lt_of_le_of_lt ?_ h)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (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
inst_5 : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : (↑‖x‖₊ : ℝ≥0∞) + (↑‖y‖₊ : ℝ≥0∞) < p.radius
x_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 p.radius) x
y_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 (p.changeOrigin x).radius) y
⊢ (p.changeOrigin x).sum y = p.sum (x + y)
have x_add_y_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 p.radius) (x + y)
Tactic: have x_add_y_mem_ball : x + y ∈ Metric.eball (0 : E) p.radius := by
    refine mem_eball_zero_iff.2 (lt_of_le_of_lt ?_ h)
    exact mod_cast nnnorm_add_le x y
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (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
inst_5 : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : (↑‖x‖₊ : ℝ≥0∞) + (↑‖y‖₊ : ℝ≥0∞) < p.radius
x_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 p.radius) x
y_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 (p.changeOrigin x).radius) y
x_add_y_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 p.radius) (x + y)
f : (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 hsf : Summable f
Tactic: have hsf : Summable f := by
    refine .of_nnnorm_bounded (p.changeOriginSeries_summable_aux₁ h) ?_
    rintro ⟨k, l, s, hs⟩
    dsimp only [Subtype.coe_mk]
    exact p.nnnorm_changeOriginSeriesTerm_apply_le _ _ _ _ _ _
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (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
inst_5 : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : (↑‖x‖₊ : ℝ≥0∞) + (↑‖y‖₊ : ℝ≥0∞) < p.radius
x_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 p.radius) x
y_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 (p.changeOrigin x).radius) y
x_add_y_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 p.radius) (x + y)
f : (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
hsf : Summable f
⊢ HasSum f ((p.changeOrigin x).sum y)
have refine : ∀ (k : ℕ),
  HasSum.{u_3, 0} (α := F)
    (fun (c : (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) ↦
      f (Sigma.mk (β := fun (b : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (b + l)) // s.card = l }) k c))
    ((p.changeOrigin x k : (a : (i : Fin k) → E) → F) fun (x : Fin k) ↦ y : F)
Tactic: refine HasSum.sigma_of_hasSum ((p.changeOrigin x).summable y_mem_ball).hasSum (fun k => ?_) hsf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (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
inst_5 : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : (↑‖x‖₊ : ℝ≥0∞) + (↑‖y‖₊ : ℝ≥0∞) < p.radius
x_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 p.radius) x
y_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 (p.changeOrigin x).radius) y
x_add_y_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 p.radius) (x + y)
f : (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
hsf : Summable f
k : ℕ
⊢ HasSum
    (fun (c : (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) ↦
      (p.changeOriginSeriesTerm k (c.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))
            (↑(c.snd (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })) : Finset (Fin (k + c.fst))) ⋯ :
          (a : (i : Fin c.fst) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F)
        fun (x_1 : Fin (c.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) ↦ x)
    (p.changeOrigin x k)
have this : HasSum
  (fun (n : ℕ) ↦
    (p.changeOriginSeries k n : (a : (i : Fin n) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F)
      fun (x_1 : Fin n) ↦ x)
  (p.changeOrigin (0 + x) k)
Tactic: have := (p.hasFPowerSeriesOnBall_changeOrigin k h.pos).hasSum x_mem_ball
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (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
inst_5 : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : (↑‖x‖₊ : ℝ≥0∞) + (↑‖y‖₊ : ℝ≥0∞) < p.radius
x_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 p.radius) x
y_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 (p.changeOrigin x).radius) y
x_add_y_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 p.radius) (x + y)
f : (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
hsf : Summable 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) := by
    refine HasSum.sigma_of_hasSum ((p.changeOrigin x).summable y_mem_ball).hasSum (fun k => ?_) hsf
    · dsimp +instances only [f]
      refine ContinuousMultilinearMap.hasSum_eval ?_ _
      have := (p.hasFPowerSeriesOnBall_changeOrigin k h.pos).hasSum x_mem_ball
      rw [zero_add] at this
      refine HasSum.sigma_of_hasSum this (fun l => ?_) ?_
      · simp only [changeOriginSeries, ContinuousMultilinearMap.sum_apply]
        apply hasSum_fintype
      · refine .of_nnnorm_bounded
          (p.changeOriginSeries_summable_aux₂ (mem_eball_zero_iff.1 x_mem_ball) k)
            fun s => ?_
        refine (ContinuousMultilinearMap.le_opNNNorm _ _).trans_eq ?_
        simp
-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (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
inst_5 : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
x y : E
h : (↑‖x‖₊ : ℝ≥0∞) + (↑‖y‖₊ : ℝ≥0∞) < p.radius
x_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 p.radius) x
y_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 (p.changeOrigin x).radius) y
x_add_y_mem_ball : Membership.mem (γ := Set E) (Metric.eball 0 p.radius) (x + y)
f : (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
hsf : Summable f
hf : HasSum f ((p.changeOrigin x).sum y)
⊢ (p.changeOrigin x).sum y = p.sum (x + y)
have refine : HasSum (β := (n : ℕ) × Finset (Fin n))
  (f ∘
    (⇑changeOriginIndexEquiv.symm :
      (a : (n : ℕ) × Finset (Fin n)) → (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))
  (p.sum (x + y))
Tactic: refine hf.unique (changeOriginIndexEquiv.symm.hasSum_iff.1 ?_)