-- Mathlib/Analysis/Analytic/Basic.lean
theorem radius_shift (p : FormalMultilinearSeries 𝕜 E F) : p.shift.radius = p.radius

Proof state:
case h.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
r : ℝ≥0
C : ℝ
⊢ (∀ (n : ℕ), ‖p (n + 1)‖ * ↑r ^ n ≤ C) → ∃ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ ‖p 0‖ ⊔ C * ↑r), ↑r ≤ ↑r

Tactic:
intro h

Result:
case h.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
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p (n + 1)‖ * ↑r ^ n ≤ C
⊢ ∃ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ ‖p 0‖ ⊔ C * ↑r), ↑r ≤ ↑r

Proof state:
case h.h.succ.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
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p (n + 1)‖ * ↑r ^ n ≤ C
m : ℕ
⊢ ‖p (m + 1)‖ * ↑r ^ m * ↑r ≤ C * ↑r

Tactic:
apply mul_le_mul_of_nonneg_right (h m) zero_le_coe

Result:
no goals

Proof state:
case e_s.h.a.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
r : ℝ≥0
C : ℝ
⊢ ∃ i', ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p (n + 1)‖ * ↑r ^ n ≤ i'), ↑r

Tactic:
use ‖p 1‖ ⊔ C / r

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
r : ℝ≥0
C : ℝ
⊢ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p (n + 1)‖ * ↑r ^ n ≤ ‖p 1‖ ⊔ C / ↑r), ↑r

Proof state:
case h.h.inl
𝕜 : 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
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
n : ℕ
hr : r = 0
⊢ ‖p (n + 1)‖ * ↑0 ^ n ≤ ‖p 1‖ ∨ ‖p (n + 1)‖ * ↑0 ^ n ≤ C / ↑0

Tactic:
cases n <;> simp

Result:
no goals

Proof state:
case h.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
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
n : ℕ
⊢ ‖p (n + 1)‖ * ↑r ^ n ≤ ‖p 1‖ ∨ ‖p (n + 1)‖ * ↑r ^ n ≤ C / ↑r

Tactic:
cases eq_zero_or_pos r with
| inl hr =>
  rw [hr]
  cases n <;> simp
| inr hr =>
  right
  rw [← NNReal.coe_pos] at hr
  specialize h (n + 1)
  rw [le_div_iff₀ hr]
  rwa [pow_succ, ← mul_assoc] at h

Result:
no goals

Proof state:
case h.h.inl
𝕜 : 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
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
n : ℕ
hr : r = 0
⊢ ‖p (n + 1)‖ * ↑r ^ n ≤ ‖p 1‖ ∨ ‖p (n + 1)‖ * ↑r ^ n ≤ C / ↑r

Tactic:
rw [hr]

Result:
case h.h.inl
𝕜 : 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
r : ℝ≥0
C : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C
n : ℕ
hr : r = 0
⊢ ‖p (n + 1)‖ * ↑0 ^ n ≤ ‖p 1‖ ∨ ‖p (n + 1)‖ * ↑0 ^ n ≤ C / ↑0

Proof state:
case e_s.h.a.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
r : ℝ≥0
⊢ ∀ (i : ℝ), ∃ i', ⨆ (_ : ∀ (n : ℕ), ‖p (n + 1)‖ * ↑r ^ n ≤ i), ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ i'), ↑r

Tactic:
intro C

Result:
case e_s.h.a.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
r : ℝ≥0
C : ℝ
⊢ ∃ i', ⨆ (_ : ∀ (n : ℕ), ‖p (n + 1)‖ * ↑r ^ n ≤ C), ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ i'), ↑r

Proof state:
case h.h.inr.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
r : ℝ≥0
C : ℝ
n : ℕ
hr : 0 < ↑r
h : ‖p (n + 1)‖ * ↑r ^ (n + 1) ≤ C
⊢ ‖p (n + 1)‖ * ↑r ^ n ≤ C / ↑r

Tactic:
rw [le_div_iff₀ hr]

Result:
case h.h.inr.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
r : ℝ≥0
C : ℝ
n : ℕ
hr : 0 < ↑r
h : ‖p (n + 1)‖ * ↑r ^ (n + 1) ≤ C
⊢ ‖p (n + 1)‖ * ↑r ^ n * ↑r ≤ C

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
⊢ p.shift.radius = p.radius

Tactic:
simp only [radius, shift, Nat.succ_eq_add_one, ContinuousMultilinearMap.curryRight_norm]

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
⊢ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p (n + 1)‖ * ↑r ^ n ≤ C), ↑r = ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r

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
r : ℝ≥0
C : ℝ
⊢ ⨆ (_ : ∀ (n : ℕ), ‖p (n + 1)‖ * ↑r ^ n ≤ C), ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ ‖p 0‖ ⊔ C * ↑r), ↑r

Tactic:
apply iSup_mono'

Result:
case h.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
r : ℝ≥0
C : ℝ
⊢ (∀ (n : ℕ), ‖p (n + 1)‖ * ↑r ^ n ≤ C) → ∃ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ ‖p 0‖ ⊔ C * ↑r), ↑r ≤ ↑r

Proof state:
case e_s.h.a.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
r : ℝ≥0
C : ℝ
⊢ ∃ i', ⨆ (_ : ∀ (n : ℕ), ‖p (n + 1)‖ * ↑r ^ n ≤ C), ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ i'), ↑r

Tactic:
use ‖p 0‖ ⊔ (C * r)

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
r : ℝ≥0
C : ℝ
⊢ ⨆ (_ : ∀ (n : ℕ), ‖p (n + 1)‖ * ↑r ^ n ≤ C), ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ ‖p 0‖ ⊔ C * ↑r), ↑r