-- Mathlib/Analysis/Analytic/ChangeOrigin.lean
theorem changeOrigin_radius : p.radius - ‖x‖₊ ≤ (p.changeOrigin x).radius

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0
_h0 : 0 < r
hr : ↑‖x‖₊ + ↑r < p.radius
hr' : ↑‖x‖₊ < p.radius
⊢ ↑r ≤ (p.changeOrigin x).radius

Tactic:
apply le_radius_of_summable_nnnorm

Result:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0
_h0 : 0 < r
hr : ↑‖x‖₊ + ↑r < p.radius
hr' : ↑‖x‖₊ < p.radius
⊢ Summable fun n => ‖p.changeOrigin x n‖₊ * r ^ n

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0
_h0 : 0 < r
hr : ↑‖x‖₊ + ↑r < p.radius
⊢ ↑r ≤ (p.changeOrigin x).radius

Tactic:
have hr' : (‖x‖₊ : ℝ≥0∞) < p.radius := (le_add_right le_rfl).trans_lt hr

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0
_h0 : 0 < r
hr : ↑‖x‖₊ + ↑r < p.radius
hr' : ↑‖x‖₊ < p.radius
⊢ ↑r ≤ (p.changeOrigin x).radius

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0
_h0 : 0 < r
hr : ↑‖x‖₊ + ↑r < p.radius
hr' : ↑‖x‖₊ < p.radius
this :
  ∀ (k : ℕ),
    ‖p.changeOrigin x k‖₊ * r ^ k ≤ (∑' (s : (l : ℕ) × { s // s.card = l }), ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst) * r ^ k
⊢ Summable fun n => ‖p.changeOrigin x n‖₊ * r ^ n

Tactic:
refine NNReal.summable_of_le this ?_

Result:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0
_h0 : 0 < r
hr : ↑‖x‖₊ + ↑r < p.radius
hr' : ↑‖x‖₊ < p.radius
this :
  ∀ (k : ℕ),
    ‖p.changeOrigin x k‖₊ * r ^ k ≤ (∑' (s : (l : ℕ) × { s // s.card = l }), ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst) * r ^ k
⊢ Summable fun b => (∑' (s : (l : ℕ) × { s // s.card = l }), ‖p (b + s.fst)‖₊ * ‖x‖₊ ^ s.fst) * r ^ b

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
⊢ p.radius - ↑‖x‖₊ ≤ (p.changeOrigin x).radius

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

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0
_h0 : 0 < r
hr : ↑r < p.radius - ↑‖x‖₊
⊢ ↑r ≤ (p.changeOrigin x).radius

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0
_h0 : 0 < r
hr : ↑‖x‖₊ + ↑r < p.radius
hr' : ↑‖x‖₊ < p.radius
⊢ Summable fun n => ‖p.changeOrigin x n‖₊ * r ^ n

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 :=
  fun k => mul_le_mul_right' (p.nnnorm_changeOrigin_le k hr') (r ^ k)

Result:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0
_h0 : 0 < r
hr : ↑‖x‖₊ + ↑r < p.radius
hr' : ↑‖x‖₊ < p.radius
this :
  ∀ (k : ℕ),
    ‖p.changeOrigin x k‖₊ * r ^ k ≤ (∑' (s : (l : ℕ) × { s // s.card = l }), ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst) * r ^ k
⊢ Summable fun n => ‖p.changeOrigin x n‖₊ * r ^ n

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0
_h0 : 0 < r
hr : ↑‖x‖₊ + ↑r < p.radius
hr' : ↑‖x‖₊ < p.radius
this :
  ∀ (k : ℕ),
    ‖p.changeOrigin x k‖₊ * r ^ k ≤ (∑' (s : (l : ℕ) × { s // s.card = l }), ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst) * r ^ k
⊢ Summable fun b => (∑' (s : (l : ℕ) × { s // s.card = l }), ‖p (b + s.fst)‖₊ * ‖x‖₊ ^ s.fst) * r ^ b

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

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0
_h0 : 0 < r
hr : ↑r < p.radius - ↑‖x‖₊
⊢ ↑r ≤ (p.changeOrigin x).radius

Tactic:
rw [lt_tsub_iff_right, add_comm] at hr

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0
_h0 : 0 < r
hr : ↑‖x‖₊ + ↑r < p.radius
⊢ ↑r ≤ (p.changeOrigin x).radius