Theorem: FormalMultilinearSeries.unshift_radius' (Ray/Analytic/Analytic.lean)

State before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
⊢ (p.unshift' c).radius = p.radius
Tactic:
simp_rw [FormalMultilinearSeries.radius]
State after:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
⊢ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ C), ↑r = ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r

State before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
⊢ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ C), ↑r = ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r
Tactic:
apply le_antisymm
State after:
case a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
⊢ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ C), ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r

case a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
⊢ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ C), ↑r

State before:
case a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
⊢ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ C), ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r
Tactic:
refine iSup₂_le ?_
State after:
case a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
⊢ ∀ (i : ℝ≥0) (j : ℝ),
    ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑i ^ n ≤ j), ↑i ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r

State before:
case a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
⊢ ∀ (i : ℝ≥0) (j : ℝ),
    ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑i ^ n ≤ j), ↑i ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r
Tactic:
intro r k
State after:
case a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
⊢ ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k), ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r

State before:
case a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
⊢ ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k), ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r
Tactic:
refine iSup_le ?_
State after:
case a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
⊢ (∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k) → ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r

State before:
case a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
⊢ (∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k) → ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r
Tactic:
intro h
State after:
case a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
⊢ ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r

State before:
case a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
⊢ ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r
Tactic:
refine le_trans ?_ (le_iSup₂ r (k * ↑r⁻¹))
State after:
case a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
⊢ ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * ↑r⁻¹), ↑r

State before:
case a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
⊢ ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * ↑r⁻¹), ↑r
Tactic:
have h := fun n ↦ mul_le_mul_of_nonneg_right (h (n + 1)) (NNReal.coe_nonneg r⁻¹)
State after:
case a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h✝ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
h : ∀ (n : ℕ), ‖p.unshift' c (n + 1)‖ * ↑r ^ (n + 1) * ↑r⁻¹ ≤ k * ↑r⁻¹
⊢ ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * ↑r⁻¹), ↑r

State before:
case a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h✝ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
h : ∀ (n : ℕ), ‖p.unshift' c (n + 1)‖ * ↑r ^ (n + 1) * ↑r⁻¹ ≤ k * ↑r⁻¹
⊢ ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * ↑r⁻¹), ↑r
Tactic:
by_cases r0 : r = 0
State after:
case pos
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h✝ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
h : ∀ (n : ℕ), ‖p.unshift' c (n + 1)‖ * ↑r ^ (n + 1) * ↑r⁻¹ ≤ k * ↑r⁻¹
r0 : r = 0
⊢ ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * ↑r⁻¹), ↑r

case neg
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h✝ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
h : ∀ (n : ℕ), ‖p.unshift' c (n + 1)‖ * ↑r ^ (n + 1) * ↑r⁻¹ ≤ k * ↑r⁻¹
r0 : ¬r = 0
⊢ ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * ↑r⁻¹), ↑r

State before:
case neg
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h✝ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
h : ∀ (n : ℕ), ‖p.unshift' c (n + 1)‖ * ↑r ^ (n + 1) * ↑r⁻¹ ≤ k * ↑r⁻¹
r0 : ¬r = 0
⊢ ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * ↑r⁻¹), ↑r
Tactic:
simp only [pow_succ, ←mul_assoc _ _ (r:ℝ), mul_assoc _ (r:ℝ) _,
  mul_inv_cancel (NNReal.coe_ne_zero.mpr r0), NNReal.coe_inv, mul_one, p.unshift_norm'] at h
State after:
case neg
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h✝ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
r0 : ¬r = 0
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * (↑r)⁻¹
⊢ ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * ↑r⁻¹), ↑r

State before:
case neg
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h✝ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
r0 : ¬r = 0
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * (↑r)⁻¹
⊢ ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * ↑r⁻¹), ↑r
Tactic:
simp only [NNReal.coe_inv]
State after:
case neg
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h✝ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
r0 : ¬r = 0
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * (↑r)⁻¹
⊢ ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * (↑r)⁻¹), ↑r

State before:
case neg
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h✝ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
r0 : ¬r = 0
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * (↑r)⁻¹
⊢ ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * (↑r)⁻¹), ↑r
Tactic:
convert le_iSup _ h
State after:
case h.e'_3
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h✝ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
r0 : ¬r = 0
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * (↑r)⁻¹
⊢ ↑r = ↑r

State before:
case h.e'_3
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h✝ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
r0 : ¬r = 0
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * (↑r)⁻¹
⊢ ↑r = ↑r
Tactic:
rfl
State after:
no goals

State before:
case pos
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h✝ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ k
h : ∀ (n : ℕ), ‖p.unshift' c (n + 1)‖ * ↑r ^ (n + 1) * ↑r⁻¹ ≤ k * ↑r⁻¹
r0 : r = 0
⊢ ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k * ↑r⁻¹), ↑r
Tactic:
simp only [r0, ENNReal.coe_zero, ENNReal.iSup_zero_eq_zero, le_zero_iff]
State after:
no goals

State before:
case a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
⊢ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C), ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ C), ↑r
Tactic:
refine iSup₂_le ?_
State after:
case a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
⊢ ∀ (i : ℝ≥0) (j : ℝ),
    ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑i ^ n ≤ j), ↑i ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ C), ↑r

State before:
case a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
⊢ ∀ (i : ℝ≥0) (j : ℝ),
    ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑i ^ n ≤ j), ↑i ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ C), ↑r
Tactic:
intro r k
State after:
case a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
⊢ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k), ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ C), ↑r

State before:
case a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
⊢ ⨆ (_ : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k), ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ C), ↑r
Tactic:
refine iSup_le ?_
State after:
case a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
⊢ (∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k) → ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ C), ↑r

State before:
case a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
⊢ (∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k) → ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ C), ↑r
Tactic:
intro h
State after:
case a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k
⊢ ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ C), ↑r

State before:
case a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k
⊢ ↑r ≤ ⨆ r, ⨆ C, ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ C), ↑r
Tactic:
refine le_trans ?_ (le_iSup₂ r (max ‖c‖ (k * ↑r)))
State after:
case a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k
⊢ ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)), ↑r

State before:
case a
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k
h' : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)
⊢ ↑r ≤ ⨆ (_ : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)), ↑r
Tactic:
convert le_iSup _ h'
State after:
case h.e'_3
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k
h' : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)
⊢ ↑r = ↑r

State before:
case h.e'_3
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k
h' : ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)
⊢ ↑r = ↑r
Tactic:
rfl
State after:
no goals

State before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k
⊢ ∀ (n : ℕ), ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)
Tactic:
intro n
State after:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k
n : ℕ
⊢ ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)

State before:
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k
n : ℕ
⊢ ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)
Tactic:
induction' n with n _
State after:
case zero
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k
⊢ ‖p.unshift' c 0‖ * ↑r ^ 0 ≤ max ‖c‖ (k * ↑r)

case succ
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k
n : ℕ
a✝ : ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)
⊢ ‖p.unshift' c (n + 1)‖ * ↑r ^ (n + 1) ≤ max ‖c‖ (k * ↑r)

State before:
case zero
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k
⊢ ‖p.unshift' c 0‖ * ↑r ^ 0 ≤ max ‖c‖ (k * ↑r)
Tactic:
simp only [FormalMultilinearSeries.unshift_coeff_zero,
  FormalMultilinearSeries.norm_apply_eq_norm_coef, pow_zero, mul_one, le_max_iff, le_refl,
  true_or_iff]
State after:
no goals

State before:
case succ
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
h : ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ k
n : ℕ
a✝ : ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)
⊢ ‖p.unshift' c (n + 1)‖ * ↑r ^ (n + 1) ≤ max ‖c‖ (k * ↑r)
Tactic:
simp only [FormalMultilinearSeries.norm_apply_eq_norm_coef] at h
State after:
case succ
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
n : ℕ
a✝ : ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)
h : ∀ (n : ℕ), ‖p.coeff n‖ * ↑r ^ n ≤ k
⊢ ‖p.unshift' c (n + 1)‖ * ↑r ^ (n + 1) ≤ max ‖c‖ (k * ↑r)

State before:
case succ
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
n : ℕ
a✝ : ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)
h : ∀ (n : ℕ), ‖p.coeff n‖ * ↑r ^ n ≤ k
⊢ ‖p.unshift' c (n + 1)‖ * ↑r ^ (n + 1) ≤ max ‖c‖ (k * ↑r)
Tactic:
simp only [FormalMultilinearSeries.unshift_coeff_succ, pow_succ, ← mul_assoc,
  FormalMultilinearSeries.norm_apply_eq_norm_coef, le_max_iff]
State after:
case succ
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
n : ℕ
a✝ : ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)
h : ∀ (n : ℕ), ‖p.coeff n‖ * ↑r ^ n ≤ k
⊢ ‖p.coeff n‖ * ↑r ^ n * ↑r ≤ ‖c‖ ∨ ‖p.coeff n‖ * ↑r ^ n * ↑r ≤ k * ↑r

State before:
case succ
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
n : ℕ
a✝ : ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)
h : ∀ (n : ℕ), ‖p.coeff n‖ * ↑r ^ n ≤ k
⊢ ‖p.coeff n‖ * ↑r ^ n * ↑r ≤ ‖c‖ ∨ ‖p.coeff n‖ * ↑r ^ n * ↑r ≤ k * ↑r
Tactic:
right
State after:
case succ.h
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
n : ℕ
a✝ : ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)
h : ∀ (n : ℕ), ‖p.coeff n‖ * ↑r ^ n ≤ k
⊢ ‖p.coeff n‖ * ↑r ^ n * ↑r ≤ k * ↑r

State before:
case succ.h
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : CompleteSpace E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
inst✝⁶ : CompleteSpace F
G : Type
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : CompleteSpace G
H : Type
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : CompleteSpace H
p : FormalMultilinearSeries 𝕜 𝕜 E
c : E
r : ℝ≥0
k : ℝ
n : ℕ
a✝ : ‖p.unshift' c n‖ * ↑r ^ n ≤ max ‖c‖ (k * ↑r)
h : ∀ (n : ℕ), ‖p.coeff n‖ * ↑r ^ n ≤ k
⊢ ‖p.coeff n‖ * ↑r ^ n * ↑r ≤ k * ↑r
Tactic:
exact mul_le_mul_of_nonneg_right (h n) (NNReal.coe_nonneg _)
State after:
no goals