awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)))
⊢ 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:
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]
-- 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
⊢ ∀ (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:
simp
-- 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
n : ℕ
s : Finset (Fin n)
⊢ Eq (α := (n : ℕ) × Finset (Fin n))
    ((fun (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) ↦
        (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin 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 }))
            (↑(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))) :
          (n : ℕ) × Finset (Fin n)))
      ((fun (s : (n : ℕ) × Finset (Fin n)) ↦
          (Sigma.mk (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
              (s.fst (β := fun (n : ℕ) ↦ Finset (Fin n)) - s.snd (β := fun (n : ℕ) ↦ Finset (Fin n)).card)
              (Sigma.mk (β := fun (l : ℕ) ↦
                { s_1 :
                  Finset
                    (Fin
                      (s.fst (β := fun (n : ℕ) ↦ Finset (Fin n)) - s.snd (β := fun (n : ℕ) ↦ Finset (Fin n)).card +
                        l)) //
                  s_1.card = l })
                s.snd (β := fun (n : ℕ) ↦ Finset (Fin n)).card
                (Subtype.mk (p :=
                  fun
                    (s_1 :
                      Finset
                        (Fin
                          (s.fst (β := fun (n : ℕ) ↦ Finset (Fin n)) - s.snd (β := fun (n : ℕ) ↦ Finset (Fin n)).card +
                            s.snd (β := fun (n : ℕ) ↦ Finset (Fin n)).card))) ↦
                  s_1.card = s.snd (β := fun (n : ℕ) ↦ Finset (Fin n)).card)
                  (Finset.map (Equiv.toEmbedding (finCongr ⋯)) (s.snd (β := fun (n : ℕ) ↦ Finset (Fin n)))) ⋯)) :
            (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))
        (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n s)))
    (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n s)

Tactic:
simp [tsub_add_cancel_of_le (card_finset_fin_le s), finCongr_eq_equivCast]

Premises used: finCongr_eq_equivCast, tsub_add_cancel_of_le, card_finset_fin_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
x y : E
n : ℕ
t : Finset (Fin n)
⊢ 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 n : (a : (i : Fin n) → E) → F)
        ((Finset.map (finCongr ⋯).toEmbedding t).piecewise (π := fun (i : Fin n) ↦ E) (fun (x_1 : Fin n) ↦ x)
          fun (x : Fin n) ↦ y) :
      F)

Tactic:
simp +unfoldPartialApp [Finset.piecewise]

Premises used: Finset.piecewise
-- 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
n : ℕ
t : Finset (Fin n)
⊢ ∀ (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]
-- 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
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))
convert_2 : HasSum (fun (s : Finset (Fin n)) ↦ ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))) (‖p n‖₊ * (r + r') ^ 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)

Tactic:
convert_to HasSum (fun s : Finset (Fin n) => ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))) _

Premises used: HMul.hMul, NNNorm.nnnorm, HSub.hSub, HPow.hPow, HasSum, Finset.card, SummationFilter.unconditional
-- 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
r r' : ℝ≥0
hr : (↑r : ℝ≥0∞) + (↑r' : ℝ≥0∞) < p.radius
n : ℕ
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))
⊢ 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:
ext1 s
-- 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
r r' : ℝ≥0
hr : (↑r : ℝ≥0∞) + (↑r' : ℝ≥0∞) < p.radius
n : ℕ
s : Finset (Fin n)
h : ‖p n‖₊ * r ^ s.card * r' ^ (n - s.card) = ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))
h₁ h₂ : ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card)) = ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))
⊢ 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:
rw [tsub_add_cancel_of_le (card_finset_fin_le _), mul_assoc]

Premises used: mul_assoc, tsub_add_cancel_of_le, card_finset_fin_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
r r' : ℝ≥0
hr : (↑r : ℝ≥0∞) + (↑r' : ℝ≥0∞) < p.radius
n : ℕ
convert_2 :
  HasSum (fun (s : Finset (Fin n)) ↦ ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card)))
    (‖p n‖₊ * ∑ s : Finset (Fin n), r ^ s.card * r' ^ (n - s.card))
⊢ HasSum (fun (s : Finset (Fin n)) ↦ ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))) (‖p n‖₊ * (r + r') ^ n)

Tactic:
rw [← Fin.sum_pow_mul_eq_add_pow]

Premises used: Fin.sum_pow_mul_eq_add_pow
-- 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
r r' : ℝ≥0
hr : (↑r : ℝ≥0∞) + (↑r' : ℝ≥0∞) < p.radius
n : ℕ
⊢ HasSum (fun (s : Finset (Fin n)) ↦ ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card)))
    (‖p n‖₊ * ∑ s : Finset (Fin n), r ^ s.card * r' ^ (n - s.card))

Tactic:
(hasSum_fintype _).mul_left _

Premises used: HasSum.mul_left, hasSum_fintype, SummationFilter.unconditional
-- 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
r r' : ℝ≥0
hr : (↑r : ℝ≥0∞) + (↑r' : ℝ≥0∞) < p.radius
n : ℕ
⊢ HasSum (fun (s : Finset (Fin n)) ↦ ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card)))
    (‖p n‖₊ * ∑ s : Finset (Fin n), r ^ s.card * r' ^ (n - s.card))

Tactic:
exact (hasSum_fintype _).mul_left _

Premises used: HasSum.mul_left, hasSum_fintype, SummationFilter.unconditional
-- 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
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)

Tactic:
have : ∀ n : ℕ,
      HasSum (fun s : Finset (Fin n) => ‖p (n - s.card + s.card)‖₊ * r ^ s.card * r' ^ (n - s.card))
        (‖p n‖₊ * (r + r') ^ n) := by
    intro n
    -- TODO: why `simp only [tsub_add_cancel_of_le (card_finset_fin_le _)]` fails?
    convert_to HasSum (fun s : Finset (Fin n) => ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))) _
    · ext1 s
      rw [tsub_add_cancel_of_le (card_finset_fin_le _), mul_assoc]
    rw [← Fin.sum_pow_mul_eq_add_pow]
    exact (hasSum_fintype _).mul_left _
-- 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
r r' : ℝ≥0
hr : (↑r : ℝ≥0∞) + (↑r' : ℝ≥0∞) < p.radius
this :
  ∀ (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)
⊢ 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:
NNReal.summable_sigma.2 ⟨fun n => (this n).summable, ?_⟩

Premises used: Iff.mpr, NNReal.summable_sigma, HasSum.summable, And.intro
-- 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
r r' : ℝ≥0
hr : (↑r : ℝ≥0∞) + (↑r' : ℝ≥0∞) < p.radius
this :
  ∀ (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)
⊢ Summable (α := ℝ≥0) fun (x : ℕ) ↦ ‖p x‖₊ * (r + r') ^ x

Tactic:
p.summable_nnnorm_mul_pow hr

Premises used: FormalMultilinearSeries.summable_nnnorm_mul_pow
-- 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
r r' : ℝ≥0
hr : (↑r : ℝ≥0∞) + (↑r' : ℝ≥0∞) < p.radius
this :
  ∀ (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)
⊢ Summable (α := ℝ≥0) fun (x : ℕ) ↦ ‖p x‖₊ * (r + r') ^ x

Tactic:
exact p.summable_nnnorm_mul_pow hr

Premises used: FormalMultilinearSeries.summable_nnnorm_mul_pow
-- 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
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
k : ℕ
rcases :
  ∀ (r' : ℝ≥0) (h0 : 0 < r') (hr' : (↑r : ℝ≥0∞) + (↑r' : ℝ≥0∞) < p.radius),
    Summable (α := ℝ≥0) fun (s : (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) ↦
      nnnorm (E :=
          ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜
            (fun (i : Fin (k + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) ↦ E) F)
          (p (k + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) *
        r ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
⊢ Summable (α := ℝ≥0) fun (s : (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) ↦
    nnnorm (E :=
        ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜
          (fun (i : Fin (k + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) ↦ E) F)
        (p (k + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) *
      r ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })

Tactic:
rcases ENNReal.lt_iff_exists_add_pos_lt.1 hr with ⟨r', h0, hr'⟩

Premises used: ENNReal.lt_iff_exists_add_pos_lt, Iff.mp
-- 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
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
k : ℕ
r' : ℝ≥0
h0 : 0 < r'
hr' : (↑r : ℝ≥0∞) + (↑r' : ℝ≥0∞) < p.radius
⊢ Summable (α := ℝ≥0) fun (s : (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) ↦
    nnnorm (E :=
        ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜
          (fun (i : Fin (k + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) ↦ E) F)
        (p (k + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))) *
      r ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })

Tactic:
simpa only [mul_inv_cancel_right₀ (pow_pos h0 _).ne'] using
    ((NNReal.summable_sigma.1 (p.changeOriginSeries_summable_aux₁ hr')).1 k).mul_right (r' ^ k)⁻¹

Premises used: pow_pos, NNReal.summable_sigma, Summable.mul_right, mul_inv_cancel_right₀, LT.lt.ne', Inv.inv, HPow.hPow, FormalMultilinearSeries.changeOriginSeries_summable_aux₁, And.left, Iff.mp
-- 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
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
k : ℕ
⊢ Summable (α := ℝ≥0) fun (l : ℕ) ↦ ‖p.changeOriginSeries k l‖₊ * r ^ l

Tactic:
NNReal.summable_of_le
    (fun n => ?_) (NNReal.summable_sigma.1 <| p.changeOriginSeries_summable_aux₂ hr k).2

Premises used: NNReal.summable_sigma, And.right, FormalMultilinearSeries.changeOriginSeries_summable_aux₂, Iff.mp, NNReal.summable_of_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
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
k : ℕ
refine :
  ∀ (n : ℕ),
    ‖p.changeOriginSeries k n‖₊ * r ^ n ≤
      ∑' (y : { s : Finset (Fin (k + n)) // s.card = n }),
        nnnorm (E :=
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜
              (fun
                  (i :
                    Fin
                      (k +
                        Sigma.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
                          (Sigma.mk (β := fun (x : ℕ) ↦ { s : Finset (Fin (k + x)) // s.card = x }) n y))) ↦
                E)
              F)
            (p
              (k +
                Sigma.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
                  (Sigma.mk (β := fun (x : ℕ) ↦ { s : Finset (Fin (k + x)) // s.card = x }) n y))) *
          r ^
            Sigma.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
              (Sigma.mk (β := fun (x : ℕ) ↦ { s : Finset (Fin (k + x)) // s.card = x }) n y)
⊢ Summable (α := ℝ≥0) fun (l : ℕ) ↦ ‖p.changeOriginSeries k l‖₊ * r ^ l

Tactic:
refine NNReal.summable_of_le
    (fun n => ?_) (NNReal.summable_sigma.1 <| p.changeOriginSeries_summable_aux₂ hr k).2

Premises used: NNReal.summable_sigma, And.right, FormalMultilinearSeries.changeOriginSeries_summable_aux₂, Iff.mp, NNReal.summable_of_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
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
k n : ℕ
simp :
  ‖p.changeOriginSeries k n‖₊ * r ^ n ≤
    (∑' (x : { s : Finset (Fin (k + n)) // s.card = n }),
        nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + n)) ↦ E) F) (p (k + n))) *
      r ^ n
⊢ ‖p.changeOriginSeries k n‖₊ * r ^ n ≤
    ∑' (y : { s : Finset (Fin (k + n)) // s.card = n }),
      nnnorm (E :=
          ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜
            (fun
                (i :
                  Fin
                    (k +
                      Sigma.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
                        (Sigma.mk (β := fun (x : ℕ) ↦ { s : Finset (Fin (k + x)) // s.card = x }) n y))) ↦
              E)
            F)
          (p
            (k +
              Sigma.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
                (Sigma.mk (β := fun (x : ℕ) ↦ { s : Finset (Fin (k + x)) // s.card = x }) n y))) *
        r ^
          Sigma.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
            (Sigma.mk (β := fun (x : ℕ) ↦ { s : Finset (Fin (k + x)) // s.card = x }) n y)

Tactic:
simp only [NNReal.tsum_mul_right]

Premises used: NNReal.tsum_mul_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
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
k n : ℕ
bc :
  ‖p.changeOriginSeries k n‖₊ ≤
    ∑' (x : { s : Finset (Fin (k + n)) // s.card = n }),
      nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + n)) ↦ E) F) (p (k + n))
⊢ ‖p.changeOriginSeries k n‖₊ * r ^ n ≤
    (∑' (x : { s : Finset (Fin (k + n)) // s.card = n }),
        nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + n)) ↦ E) F) (p (k + n))) *
      r ^ n

Tactic:
gcongr