awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ HasSum (fun (n : ℕ) ↦ (p.changeOrigin y n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z) (f (x + y + z))
have this : f (x + y + z) = (p.changeOrigin y).sum z
Tactic: have : f (x + y + z) =
        FormalMultilinearSeries.sum (FormalMultilinearSeries.changeOrigin p y) z := by
      rw [mem_eball_zero_iff, lt_tsub_iff_right, add_comm] at hz
      rw [p.changeOrigin_eval_of_finite hf.finite, add_assoc, hf.sum]
      exact mem_eball_zero_iff.2 ((enorm_add_le _ _).trans_lt 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 : 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) (f (x + y + z))
have rw : HasSum (fun (n : ℕ) ↦ (p.changeOrigin y n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ z) ((p.changeOrigin y).sum z)
Tactic: rw [this]
-- 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 ∈ Metric.eball x r
⊢ CPolynomialAt 𝕜 f y
have this : (↑‖y - x‖₊ : ℝ≥0∞) < r
Tactic: have : (‖y - x‖₊ : ℝ≥0∞) < r := by simpa [edist_eq_enorm_sub] using h
-- 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 ∈ Metric.eball x r
this : (↑‖y - x‖₊ : ℝ≥0∞) < r
⊢ CPolynomialAt 𝕜 f y
have this₁ : HasFiniteFPowerSeriesOnBall f (p.changeOrigin (y - x)) (x + (y - x)) n (r - (↑‖y - x‖₊ : ℝ≥0∞))
Tactic: have := hf.changeOrigin this
-- 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 ∈ 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∞))
⊢ CPolynomialAt 𝕜 f y
have this₁ : HasFiniteFPowerSeriesOnBall f (p.changeOrigin (y - x)) y n (r - (↑‖y - x‖₊ : ℝ≥0∞))
Tactic: rw [add_sub_cancel] at this
Cleared hypotheses: this
-- 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
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x : E | CPolynomialAt 𝕜 f x}
have rw : ∀ (x : E), Membership.mem (γ := Set E) {x : E | CPolynomialAt 𝕜 f x} x → {x : E | CPolynomialAt 𝕜 f x} ∈ 𝓝 x
Tactic: rw [isOpen_iff_mem_nhds]
-- 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
x y : E
r : ℝ≥0
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
⊢ sᶜ.card = k
have rw : Fintype.card (Fin (k + l)) - s.card = k
Tactic: rw [Finset.card_compl, Fintype.card_fin, hs, add_tsub_cancel_right]
-- 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
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
⊢ sᶜ.card = k
have rw₁ : k + l - s.card = k
Tactic: rw [Finset.card_compl, Fintype.card_fin, hs, add_tsub_cancel_right]
-- 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
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
⊢ sᶜ.card = k
have rw₂ : k + l - l = k
Tactic: rw [Finset.card_compl, Fintype.card_fin, hs, add_tsub_cancel_right]
-- 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
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
⊢ sᶜ.card = k
have rw₃ : k = k
Tactic: rw [Finset.card_compl, Fintype.card_fin, hs, add_tsub_cancel_right]
-- 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
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
x y : E
⊢ 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
have 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‖₊
Tactic: rw [← p.nnnorm_changeOriginSeriesTerm k l s hs, ← Fin.prod_const, ← Fin.prod_const]
-- 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
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
x y : E
⊢ 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‖₊
have 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‖₊
Tactic: apply ContinuousMultilinearMap.le_of_opNNNorm_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
p : FormalMultilinearSeries 𝕜 E F
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)))
have simp_rw : Eq (α := ℝ≥0)
  (∑ a : { s : Finset (Fin (k + l)) // s.card = l }, ‖p.changeOriginSeriesTerm k l (↑a : Finset (Fin (k + l))) sorry‖₊)
  (∑ 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)]
-- 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
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) ≤
    ∑' (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
have 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‖₊)
Tactic: rw [NNReal.tsum_mul_right, ← Fin.prod_const]
-- 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
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)))
⊢ 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)))
have a : k + l - s.card = k
Tactic: apply 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
x y : E
r : ℝ≥0
k l : ℕ
s : Finset (Fin (k + l))
hs : 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)))
have suffices : ∀ (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)))
Tactic: suffices ∀ k' l', k' = k → l' = l → ∀ (hkl : k + l = k' + l') (hs'),
        (⟨k', l', ⟨s.map (finCongr hkl).toEmbedding, hs'⟩⟩ :
          Σ k l : ℕ, { s : Finset (Fin (k + l)) // s.card = l }) = ⟨k, l, ⟨s, hs⟩⟩ by
      apply this <;> simp only [hs, add_tsub_cancel_right]
-- 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
x y : E
n : ℕ
t : Finset (Fin n)
⊢ let s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l } :=
    (changeOriginIndexEquiv.symm :
        (a : (n : ℕ) × Finset (Fin n)) → (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
      (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n t);
  Eq.{u_3 + 1} (α := F)
    (((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 :
      F)
    ((p n : (a : (i : Fin n) → E) → F)
        (t.piecewise (π := fun (i : Fin n) ↦ E) (fun (x_1 : Fin n) ↦ x) fun (x : Fin n) ↦ y) :
      F)
have this : ∀ (m : ℕ) (hm : n = m),
  Eq.{u_3 + 1} (α := F)
    ((p n : (a : (i : Fin n) → E) → F)
        (t.piecewise (π := fun (i : Fin n) ↦ E) (fun (x_1 : Fin n) ↦ x) fun (x : Fin n) ↦ y) :
      F)
    ((p m : (a : (i : Fin m) → E) → F)
        ((Finset.map (finCongr hm).toEmbedding t).piecewise (π := fun (i : Fin m) ↦ E) (fun (x_1 : Fin m) ↦ x)
          fun (x : Fin m) ↦ y) :
      F)
Tactic: have : ∀ (m) (hm : n = m), p n (t.piecewise (fun _ ↦ x) fun _ ↦ y) =
      p m ((t.map (finCongr hm).toEmbedding).piecewise (fun _ ↦ x) fun _ ↦ y) := by
    rintro m rfl
    simp +unfoldPartialApp [Finset.piecewise]
-- 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
r r' : ℝ≥0
hr : (↑r : ℝ≥0∞) + (↑r' : ℝ≥0∞) < p.radius
⊢ Summable (α := ℝ≥0) (β := (n : ℕ) × Finset (Fin n))
    ((fun (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) ↦
        nnnorm (E :=
              ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜
                (fun
                    (i :
                      Fin
                        (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 }))) ↦
                  E)
                F)
              (p
                (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 }))) *
            r ^
              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 }) *
          r' ^ s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })) ∘
      (⇑changeOriginIndexEquiv.symm :
        (a : (n : ℕ) × Finset (Fin n)) → (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))
have dsimp : Summable (α := ℝ≥0) fun (x : (n : ℕ) × Finset (Fin n)) ↦
  nnnorm (E :=
        ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜
          (fun
              (i :
                Fin
                  (x.fst (β := fun (n : ℕ) ↦ Finset (Fin n)) - x.snd (β := fun (n : ℕ) ↦ Finset (Fin n)).card +
                    x.snd (β := fun (n : ℕ) ↦ Finset (Fin n)).card)) ↦
            E)
          F)
        (p
          (x.fst (β := fun (n : ℕ) ↦ Finset (Fin n)) - x.snd (β := fun (n : ℕ) ↦ Finset (Fin n)).card +
            x.snd (β := fun (n : ℕ) ↦ Finset (Fin n)).card)) *
      r ^ x.snd (β := fun (n : ℕ) ↦ Finset (Fin n)).card *
    r' ^ (x.fst (β := fun (n : ℕ) ↦ Finset (Fin n)) - x.snd (β := fun (n : ℕ) ↦ Finset (Fin n)).card)
Tactic: dsimp only [Function.comp_def, changeOriginIndexEquiv_symm_apply_fst,
    changeOriginIndexEquiv_symm_apply_snd_fst]
-- 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
r r' : ℝ≥0
hr : (↑r : ℝ≥0∞) + (↑r' : ℝ≥0∞) < p.radius
n : ℕ
⊢ HasSum
    (fun (s : Finset (Fin n)) ↦
      nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n - s.card + s.card)) ↦ E) F)
            (p (n - s.card + s.card)) *
          r ^ s.card *
        r' ^ (n - s.card))
    (‖p n‖₊ * (r + r') ^ n)
have h : Eq (α := Finset (Fin n) → ℝ≥0)
  (fun (s : Finset (Fin n)) ↦
    nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n - s.card + s.card)) ↦ E) F)
          (p (n - s.card + s.card)) *
        r ^ s.card *
      r' ^ (n - s.card))
  fun (s : Finset (Fin n)) ↦ ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))
Tactic: convert_to HasSum (fun s : Finset (Fin n) => ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))) _
-- 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
r r' : ℝ≥0
hr : (↑r : ℝ≥0∞) + (↑r' : ℝ≥0∞) < p.radius
n : ℕ
h :
  Eq (α := Finset (Fin n) → ℝ≥0)
    (fun (s : Finset (Fin n)) ↦
      nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n - s.card + s.card)) ↦ E) F)
            (p (n - s.card + s.card)) *
          r ^ s.card *
        r' ^ (n - s.card))
    fun (s : Finset (Fin n)) ↦ ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))
⊢ HasSum
    (fun (s : Finset (Fin n)) ↦
      nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n - s.card + s.card)) ↦ E) F)
            (p (n - s.card + s.card)) *
          r ^ s.card *
        r' ^ (n - s.card))
    (‖p n‖₊ * (r + r') ^ n)
have convert_2 : HasSum (fun (s : Finset (Fin n)) ↦ ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))) (‖p n‖₊ * (r + r') ^ n)
Tactic: convert_to HasSum (fun s : Finset (Fin n) => ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))) _
-- 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
r r' : ℝ≥0
hr : (↑r : ℝ≥0∞) + (↑r' : ℝ≥0∞) < p.radius
n : ℕ
⊢ Eq (α := Finset (Fin n) → ℝ≥0)
    (fun (s : Finset (Fin n)) ↦
      nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n - s.card + s.card)) ↦ E) F)
            (p (n - s.card + s.card)) *
          r ^ s.card *
        r' ^ (n - s.card))
    fun (s : Finset (Fin n)) ↦ ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))
have h : ∀ (s : Finset (Fin n)),
  nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n - s.card + s.card)) ↦ E) F)
          (p (n - s.card + s.card)) *
        r ^ s.card *
      r' ^ (n - s.card) =
    ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))
Tactic: ext1 s