-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem summable_norm_mul_geometric_of_norm_lt_one {k : ℕ} {r : R}
    (hr : ‖r‖ < 1) {u : ℕ → ℕ} (hu : (fun n ↦ (u n : ℝ)) =O[atTop] (fun n ↦ (↑(n ^ k) : ℝ))) :
    Summable fun n : ℕ ↦ ‖(u n * r ^ n : R)‖

Proof state:
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n => ↑(u n)) =O[atTop] fun n => ↑(n ^ k)
⊢ Summable fun n => ‖↑(u n) * r ^ n‖

Tactic:
rcases exists_between hr with ⟨r', hrr', h⟩

Result:
case intro.intro
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n => ↑(u n)) =O[atTop] fun n => ↑(n ^ k)
r' : ℝ
hrr' : ‖r‖ < r'
h : r' < 1
⊢ Summable fun n => ‖↑(u n) * r ^ n‖

Proof state:
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n => ↑(u n)) =O[atTop] fun n => ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
⊢ (fun n => ↑(n ^ k) * ‖r‖ ^ n) =O[atTop] fun n => r' ^ n

Tactic:
simp only [cast_pow]

Result:
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n => ↑(u n)) =O[atTop] fun n => ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
⊢ (fun n => ↑n ^ k * ‖r‖ ^ n) =O[atTop] fun n => r' ^ n

Proof state:
case h₁
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n => ↑(u n)) =O[atTop] fun n => ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
⊢ ‖↑(u n)‖ ≤ ↑(u n) * ‖1‖

Tactic:
exact norm_cast_le (u n)

Result:
no goals

Proof state:
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n => ↑(u n)) =O[atTop] fun n => ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
⊢ ‖↑(u n)‖ * ‖r ^ n‖ ≤ ↑(u n) * ‖1‖ * ‖r‖ ^ n

Tactic:
gcongr

Result:
case h₁
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n => ↑(u n)) =O[atTop] fun n => ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
⊢ ‖↑(u n)‖ ≤ ↑(u n) * ‖1‖

Proof state:
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n => ↑(u n)) =O[atTop] fun n => ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
⊢ (fun n => ↑n ^ k * ‖r‖ ^ n) =O[atTop] fun n => r' ^ n

Tactic:
exact (isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt k hrr').isBigO

Result:
no goals

Proof state:
case intro.intro
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n => ↑(u n)) =O[atTop] fun n => ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
⊢ (fun n => ‖↑(u n) * r ^ n‖) =O[atTop] fun n => r' ^ n

Tactic:
calc
fun n ↦ ‖↑(u n) * r ^ n‖
_ =O[atTop] fun n ↦ u n * ‖r‖ ^ n := by
    apply (IsBigOWith.of_bound (c := ‖(1 : R)‖) ?_).isBigO
    filter_upwards [eventually_norm_pow_le r] with n hn
    simp only [norm_norm, norm_mul, Real.norm_eq_abs, abs_cast, norm_pow, abs_norm]
    apply (norm_mul_le _ _).trans
    have : ‖(u n : R)‖ * ‖r ^ n‖ ≤ (u n * ‖(1 : R)‖) * ‖r‖ ^ n := by
      gcongr; exact norm_cast_le (u n)
    exact this.trans (le_of_eq (by ring))
_ =O[atTop] fun n ↦ ↑(n ^ k) * ‖r‖ ^ n := hu.mul (isBigO_refl _ _)
_ =O[atTop] fun n ↦ r' ^ n := by
    simp only [cast_pow]
    exact (isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt k hrr').isBigO

Result:
no goals

Proof state:
case intro.intro
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n => ↑(u n)) =O[atTop] fun n => ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
⊢ Summable fun n => ‖↑(u n) * r ^ n‖

Tactic:
apply summable_of_isBigO_nat (summable_geometric_of_lt_one ((norm_nonneg _).trans hrr'.le) h)

Result:
case intro.intro
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n => ↑(u n)) =O[atTop] fun n => ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
⊢ (fun n => ‖↑(u n) * r ^ n‖) =O[atTop] fun n => r' ^ n

Proof state:
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n => ↑(u n)) =O[atTop] fun n => ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
this : ‖↑(u n)‖ * ‖r ^ n‖ ≤ ↑(u n) * ‖1‖ * ‖r‖ ^ n
⊢ ↑(u n) * ‖1‖ * ‖r‖ ^ n = ‖1‖ * (↑(u n) * ‖r‖ ^ n)

Tactic:
ring

Result:
no goals

Proof state:
case h
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n => ↑(u n)) =O[atTop] fun n => ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
this : ‖↑(u n)‖ * ‖r ^ n‖ ≤ ↑(u n) * ‖1‖ * ‖r‖ ^ n
⊢ ‖↑(u n)‖ * ‖r ^ n‖ ≤ ‖1‖ * (↑(u n) * ‖r‖ ^ n)

Tactic:
exact this.trans (le_of_eq (by ring))

Result:
no goals

Proof state:
case intro.intro
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n => ↑(u n)) =O[atTop] fun n => ↑(n ^ k)
r' : ℝ
hrr' : ‖r‖ < r'
h : r' < 1
⊢ Summable fun n => ‖↑(u n) * r ^ n‖

Tactic:
rw [← norm_norm] at hrr'

Result:
case intro.intro
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n => ↑(u n)) =O[atTop] fun n => ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
⊢ Summable fun n => ‖↑(u n) * r ^ n‖

Proof state:
case h
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n => ↑(u n)) =O[atTop] fun n => ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
⊢ ‖↑(u n)‖ * ‖r ^ n‖ ≤ ‖1‖ * (↑(u n) * ‖r‖ ^ n)

Tactic:
have : ‖(u n : R)‖ * ‖r ^ n‖ ≤ (u n * ‖(1 : R)‖) * ‖r‖ ^ n := by
  gcongr; exact norm_cast_le (u n)

Result:
case h
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n => ↑(u n)) =O[atTop] fun n => ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
this : ‖↑(u n)‖ * ‖r ^ n‖ ≤ ↑(u n) * ‖1‖ * ‖r‖ ^ n
⊢ ‖↑(u n)‖ * ‖r ^ n‖ ≤ ‖1‖ * (↑(u n) * ‖r‖ ^ n)

Proof state:
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n => ↑(u n)) =O[atTop] fun n => ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
⊢ ∀ᶠ (x : ℕ) in atTop, ‖‖↑(u x) * r ^ x‖‖ ≤ ‖1‖ * ‖↑(u x) * ‖r‖ ^ x‖

Tactic:
filter_upwards [eventually_norm_pow_le r] with n hn

Result:
case h
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n => ↑(u n)) =O[atTop] fun n => ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
⊢ ‖‖↑(u n) * r ^ n‖‖ ≤ ‖1‖ * ‖↑(u n) * ‖r‖ ^ n‖

Proof state:
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n => ↑(u n)) =O[atTop] fun n => ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
⊢ (fun n => ‖↑(u n) * r ^ n‖) =O[atTop] fun n => ↑(u n) * ‖r‖ ^ n

Tactic:
apply (IsBigOWith.of_bound (c := ‖(1 : R)‖) ?_).isBigO

Result:
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n => ↑(u n)) =O[atTop] fun n => ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
⊢ ∀ᶠ (x : ℕ) in atTop, ‖‖↑(u x) * r ^ x‖‖ ≤ ‖1‖ * ‖↑(u x) * ‖r‖ ^ x‖

Proof state:
case h
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n => ↑(u n)) =O[atTop] fun n => ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
⊢ ‖↑(u n) * r ^ n‖ ≤ ‖1‖ * (↑(u n) * ‖r‖ ^ n)

Tactic:
apply (norm_mul_le _ _).trans

Result:
case h
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n => ↑(u n)) =O[atTop] fun n => ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
⊢ ‖↑(u n)‖ * ‖r ^ n‖ ≤ ‖1‖ * (↑(u n) * ‖r‖ ^ n)

Proof state:
case h
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n => ↑(u n)) =O[atTop] fun n => ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
⊢ ‖‖↑(u n) * r ^ n‖‖ ≤ ‖1‖ * ‖↑(u n) * ‖r‖ ^ n‖

Tactic:
simp only [norm_norm, norm_mul, Real.norm_eq_abs, abs_cast, norm_pow, abs_norm]

Result:
case h
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r : R
hr : ‖r‖ < 1
u : ℕ → ℕ
hu : (fun n => ↑(u n)) =O[atTop] fun n => ↑(n ^ k)
r' : ℝ
hrr' : ‖‖r‖‖ < r'
h : r' < 1
n : ℕ
hn : ‖r ^ n‖ ≤ ‖r‖ ^ n
⊢ ‖↑(u n) * r ^ n‖ ≤ ‖1‖ * (↑(u n) * ‖r‖ ^ n)