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
r : ℝ≥0
hr : (↑r : ℝ≥0∞) < p.radius
k n : ℕ
⊢ ‖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))

Tactic:
apply p.nnnorm_changeOriginSeries_le_tsum

Premises used: FormalMultilinearSeries.nnnorm_changeOriginSeries_le_tsum
-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
k : ℕ
⊢ p.radius ≤
    (p.changeOriginSeries k).radius (𝕜 := 𝕜) (E := E) (F :=
      ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)

Tactic:
ENNReal.le_of_forall_nnreal_lt fun _r hr =>
    le_radius_of_summable_nnnorm _ (p.changeOriginSeries_summable_aux₃ hr k)

Premises used: FormalMultilinearSeries.changeOriginSeries_summable_aux₃, FormalMultilinearSeries.le_radius_of_summable_nnnorm, FormalMultilinearSeries.changeOriginSeries, ENNReal.le_of_forall_nnreal_lt
-- 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 : E
k : ℕ
h : (↑‖x‖₊ : ℝ≥0∞) < p.radius
⊢ ‖p.changeOrigin x k‖₊ ≤
    ∑' (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 }))) *
        ‖x‖₊ ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })

Tactic:
tsum_of_nnnorm_bounded ?_ fun l => p.nnnorm_changeOriginSeries_apply_le_tsum k l x

Premises used: FormalMultilinearSeries.changeOrigin, FormalMultilinearSeries.nnnorm_changeOriginSeries_apply_le_tsum, tsum_of_nnnorm_bounded, FormalMultilinearSeries.sum
-- 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 : E
k : ℕ
h : (↑‖x‖₊ : ℝ≥0∞) < p.radius
refine :
  HasSum (α := ℝ≥0)
    (fun (l : ℕ) ↦
      ∑' (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)
    (∑' (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 }))) *
        ‖x‖₊ ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))
⊢ ‖p.changeOrigin x k‖₊ ≤
    ∑' (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 }))) *
        ‖x‖₊ ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })

Tactic:
refine tsum_of_nnnorm_bounded ?_ fun l => p.nnnorm_changeOriginSeries_apply_le_tsum k l x

Premises used: FormalMultilinearSeries.nnnorm_changeOriginSeries_apply_le_tsum, tsum_of_nnnorm_bounded
-- 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 : E
k : ℕ
h : (↑‖x‖₊ : ℝ≥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 }))) *
      ‖x‖₊ ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })

Tactic:
have := p.changeOriginSeries_summable_aux₂ h k
-- 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 : E
k : ℕ
h : (↑‖x‖₊ : ℝ≥0∞) < p.radius
this :
  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 }))) *
      ‖x‖₊ ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
refine :
  ∀ (l : ℕ),
    HasSum (α := ℝ≥0)
      (fun (c : { s : Finset (Fin (k + l)) // s.card = l }) ↦
        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 (b : ℕ) ↦ { s : Finset (Fin (k + b)) // s.card = b }) l c))) ↦
                E)
              F)
            (p
              (k +
                Sigma.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
                  (Sigma.mk (β := fun (b : ℕ) ↦ { s : Finset (Fin (k + b)) // s.card = b }) l c))) *
          ‖x‖₊ ^
            Sigma.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
              (Sigma.mk (β := fun (b : ℕ) ↦ { s : Finset (Fin (k + b)) // s.card = b }) l c))
      (∑' (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)
⊢ HasSum (α := ℝ≥0)
    (fun (l : ℕ) ↦
      ∑' (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)
    (∑' (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 }))) *
        ‖x‖₊ ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }))

Tactic:
refine HasSum.sigma this.hasSum fun l => ?_

Premises used: HasSum.sigma, Summable.hasSum
-- 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 : E
k : ℕ
h : (↑‖x‖₊ : ℝ≥0∞) < p.radius
this :
  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 }))) *
      ‖x‖₊ ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
l : ℕ
⊢ HasSum (α := ℝ≥0)
    (fun (c : { s : Finset (Fin (k + l)) // s.card = l }) ↦
      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 (b : ℕ) ↦ { s : Finset (Fin (k + b)) // s.card = b }) l c))) ↦
              E)
            F)
          (p
            (k +
              Sigma.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
                (Sigma.mk (β := fun (b : ℕ) ↦ { s : Finset (Fin (k + b)) // s.card = b }) l c))) *
        ‖x‖₊ ^
          Sigma.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
            (Sigma.mk (β := fun (b : ℕ) ↦ { s : Finset (Fin (k + b)) // s.card = b }) l c))
    (∑' (x_1 : { s : Finset (Fin (k + l)) // s.card = l }),
      nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + l)) ↦ E) F) (p (k + l)) * ‖x‖₊ ^ l)

Tactic:
((NNReal.summable_sigma.1 this).1 l).hasSum

Premises used: NNReal.summable_sigma, Summable.hasSum, 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
x : E
k : ℕ
h : (↑‖x‖₊ : ℝ≥0∞) < p.radius
this :
  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 }))) *
      ‖x‖₊ ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
l : ℕ
⊢ HasSum (α := ℝ≥0)
    (fun (c : { s : Finset (Fin (k + l)) // s.card = l }) ↦
      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 (b : ℕ) ↦ { s : Finset (Fin (k + b)) // s.card = b }) l c))) ↦
              E)
            F)
          (p
            (k +
              Sigma.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
                (Sigma.mk (β := fun (b : ℕ) ↦ { s : Finset (Fin (k + b)) // s.card = b }) l c))) *
        ‖x‖₊ ^
          Sigma.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
            (Sigma.mk (β := fun (b : ℕ) ↦ { s : Finset (Fin (k + b)) // s.card = b }) l c))
    (∑' (x_1 : { s : Finset (Fin (k + l)) // s.card = l }),
      nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + l)) ↦ E) F) (p (k + l)) * ‖x‖₊ ^ l)

Tactic:
exact ((NNReal.summable_sigma.1 this).1 l).hasSum

Premises used: NNReal.summable_sigma, Summable.hasSum, 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
x : E
⊢ p.radius - (↑‖x‖₊ : ℝ≥0∞) ≤ (p.changeOrigin x).radius

Tactic:
ENNReal.le_of_forall_pos_nnreal_lt fun r _h0 hr => ?_

Premises used: ENNReal.le_of_forall_pos_nnreal_lt
-- 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 : E
refine :
  ∀ (r : ℝ≥0) (_h0 : 0 < r) (hr : (↑r : ℝ≥0∞) < p.radius - (↑‖x‖₊ : ℝ≥0∞)), (↑r : ℝ≥0∞) ≤ (p.changeOrigin x).radius
⊢ p.radius - (↑‖x‖₊ : ℝ≥0∞) ≤ (p.changeOrigin x).radius

Tactic:
refine ENNReal.le_of_forall_pos_nnreal_lt fun r _h0 hr => ?_

Premises used: ENNReal.le_of_forall_pos_nnreal_lt
-- 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 : E
r : ℝ≥0
_h0 : 0 < r
hr : (↑r : ℝ≥0∞) < p.radius - (↑‖x‖₊ : ℝ≥0∞)
⊢ (↑‖x‖₊ : ℝ≥0∞) + (↑r : ℝ≥0∞) < p.radius

Tactic:
rw [lt_tsub_iff_right, add_comm] at hr

Premises used: lt_tsub_iff_right, add_comm
-- 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 : E
r : ℝ≥0
_h0 : 0 < r
hr : (↑‖x‖₊ : ℝ≥0∞) + (↑r : ℝ≥0∞) < p.radius
⊢ (↑‖x‖₊ : ℝ≥0∞) < p.radius

Tactic:
have hr' : (‖x‖₊ : ℝ≥0∞) < p.radius := (le_add_right le_rfl).trans_lt hr
-- 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 : E
r : ℝ≥0
_h0 : 0 < r
hr : (↑‖x‖₊ : ℝ≥0∞) + (↑r : ℝ≥0∞) < p.radius
hr' : (↑‖x‖₊ : ℝ≥0∞) < p.radius
h : Summable (α := ℝ≥0) fun (n : ℕ) ↦ ‖p.changeOrigin x n‖₊ * r ^ n
⊢ (↑r : ℝ≥0∞) ≤ (p.changeOrigin x).radius

Tactic:
apply le_radius_of_summable_nnnorm

Premises used: FormalMultilinearSeries.le_radius_of_summable_nnnorm
-- 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 : E
r : ℝ≥0
_h0 : 0 < r
hr : (↑‖x‖₊ : ℝ≥0∞) + (↑r : ℝ≥0∞) < p.radius
hr' : (↑‖x‖₊ : ℝ≥0∞) < p.radius
k : ℕ
bc :
  ‖p.changeOrigin x k‖₊ ≤
    ∑' (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 }))) *
        ‖x‖₊ ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })
⊢ ‖p.changeOrigin x k‖₊ * r ^ k ≤
    (∑' (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 }))) *
          ‖x‖₊ ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })) *
      r ^ k

Tactic:
gcongr
-- 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 : E
r : ℝ≥0
_h0 : 0 < r
hr : (↑‖x‖₊ : ℝ≥0∞) + (↑r : ℝ≥0∞) < p.radius
hr' : (↑‖x‖₊ : ℝ≥0∞) < p.radius
k : ℕ
⊢ ‖p.changeOrigin x k‖₊ ≤
    ∑' (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 }))) *
        ‖x‖₊ ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })

Tactic:
p.nnnorm_changeOrigin_le k hr'

Premises used: FormalMultilinearSeries.nnnorm_changeOrigin_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 : E
r : ℝ≥0
_h0 : 0 < r
hr : (↑‖x‖₊ : ℝ≥0∞) + (↑r : ℝ≥0∞) < p.radius
hr' : (↑‖x‖₊ : ℝ≥0∞) < p.radius
k : ℕ
⊢ ‖p.changeOrigin x k‖₊ ≤
    ∑' (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 }))) *
        ‖x‖₊ ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })

Tactic:
exact p.nnnorm_changeOrigin_le k hr'

Premises used: FormalMultilinearSeries.nnnorm_changeOrigin_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 : E
r : ℝ≥0
_h0 : 0 < r
hr : (↑‖x‖₊ : ℝ≥0∞) + (↑r : ℝ≥0∞) < p.radius
hr' : (↑‖x‖₊ : ℝ≥0∞) < p.radius
⊢ ∀ (k : ℕ),
    ‖p.changeOrigin x k‖₊ * r ^ k ≤
      (∑' (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 }))) *
            ‖x‖₊ ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })) *
        r ^ k

Tactic:
have (k : ℕ) :
      ‖p.changeOrigin x k‖₊ * r ^ k ≤
        (∑' s : Σ l : ℕ, { s : Finset (Fin (k + l)) // s.card = l }, ‖p (k + s.1)‖₊ * ‖x‖₊ ^ s.1) *
          r ^ k := by
    gcongr; exact p.nnnorm_changeOrigin_le k hr'
-- 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 : E
r : ℝ≥0
_h0 : 0 < r
hr : (↑‖x‖₊ : ℝ≥0∞) + (↑r : ℝ≥0∞) < p.radius
hr' : (↑‖x‖₊ : ℝ≥0∞) < p.radius
this :
  ∀ (k : ℕ),
    ‖p.changeOrigin x k‖₊ * r ^ k ≤
      (∑' (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 }))) *
            ‖x‖₊ ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })) *
        r ^ k
⊢ Summable (α := ℝ≥0) fun (n : ℕ) ↦ ‖p.changeOrigin x n‖₊ * r ^ n

Tactic:
NNReal.summable_of_le this ?_

Premises used: 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
x : E
r : ℝ≥0
_h0 : 0 < r
hr : (↑‖x‖₊ : ℝ≥0∞) + (↑r : ℝ≥0∞) < p.radius
hr' : (↑‖x‖₊ : ℝ≥0∞) < p.radius
this :
  ∀ (k : ℕ),
    ‖p.changeOrigin x k‖₊ * r ^ k ≤
      (∑' (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 }))) *
            ‖x‖₊ ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l })) *
        r ^ k
h :
  Summable (α := ℝ≥0) fun (b : ℕ) ↦
    (∑' (s : (l : ℕ) × { s : Finset (Fin (b + l)) // s.card = l }),
        nnnorm (E :=
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜
              (fun (i : Fin (b + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (b + l)) // s.card = l }))) ↦ E) F)
            (p (b + s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (b + l)) // s.card = l }))) *
          ‖x‖₊ ^ s.fst (β := fun (l : ℕ) ↦ { s : Finset (Fin (b + l)) // s.card = l })) *
      r ^ b
⊢ Summable (α := ℝ≥0) fun (n : ℕ) ↦ ‖p.changeOrigin x n‖₊ * r ^ n

Tactic:
refine NNReal.summable_of_le this ?_

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

Tactic:
simpa only [← NNReal.tsum_mul_right] using
    (NNReal.summable_sigma.1 (p.changeOriginSeries_summable_aux₁ hr)).2

Premises used: NNReal.summable_sigma, NNReal.tsum_mul_right, And.right, FormalMultilinearSeries.changeOriginSeries_summable_aux₁, 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
apply :
  ∀ (n : ℕ),
    ‖p.derivSeries 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)
⊢ p.radius ≤ p.derivSeries.radius (𝕜 := 𝕜) (E := E) (F := E →L[𝕜] F)

Tactic:
apply (p.le_changeOriginSeries_radius 1).trans (radius_le_of_le (fun n ↦ ?_))

Premises used: FormalMultilinearSeries.le_changeOriginSeries_radius, FormalMultilinearSeries.radius_le_of_le, LE.le.trans, OfNat.ofNat