-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt {R : Type*} [NormedRing R] (k : ℕ)
    {r₁ : R} {r₂ : ℝ} (h : ‖r₁‖ < r₂) :
    (fun n ↦ (n : R) ^ k * r₁ ^ n : ℕ → R) =o[atTop] fun n ↦ r₂ ^ n

Proof state:
case neg
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
⊢ (fun n => ↑n ^ k * r₁ ^ n) =o[atTop] fun n => r₂ ^ n

Tactic:
have A : (fun n ↦ (n : R) ^ k : ℕ → R) =o[atTop] fun n ↦ (r₂ / ‖r₁‖) ^ n :=
  isLittleO_pow_const_const_pow_of_one_lt k ((one_lt_div h0).2 h)

Result:
case neg
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
A : (fun n => ↑n ^ k) =o[atTop] fun n => (r₂ / ‖r₁‖) ^ n
⊢ (fun n => ↑n ^ k * r₁ ^ n) =o[atTop] fun n => r₂ ^ n

Proof state:
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
⊢ (fun n => ↑n ^ k * r₁ ^ n) =o[atTop] fun n => r₂ ^ n

Tactic:
by_cases h0 : r₁ = 0

Result:
case pos
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : r₁ = 0
⊢ (fun n => ↑n ^ k * r₁ ^ n) =o[atTop] fun n => r₂ ^ n

case neg
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : ¬r₁ = 0
⊢ (fun n => ↑n ^ k * r₁ ^ n) =o[atTop] fun n => r₂ ^ n

Proof state:
case pos
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : r₁ = 0
⊢ (fun n => ↑n ^ k * r₁ ^ n) =o[atTop] fun n => r₂ ^ n

Tactic:
refine (isLittleO_zero _ _).congr' (mem_atTop_sets.2 <| ⟨1, fun n hn ↦ ?_⟩) EventuallyEq.rfl

Result:
case pos
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : r₁ = 0
n : ℕ
hn : n ≥ 1
⊢ n ∈ {x | (fun x => (fun _x => 0) x = (fun n => ↑n ^ k * r₁ ^ n) x) x}

Proof state:
case neg
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : ¬r₁ = 0
⊢ (fun n => ↑n ^ k * r₁ ^ n) =o[atTop] fun n => r₂ ^ n

Tactic:
rw [← Ne, ← norm_pos_iff] at h0

Result:
case neg
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
⊢ (fun n => ↑n ^ k * r₁ ^ n) =o[atTop] fun n => r₂ ^ n

Proof state:
case pos
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : r₁ = 0
n : ℕ
hn : n ≥ 1
⊢ n ∈ {x | (fun x => (fun _x => 0) x = (fun n => ↑n ^ k * r₁ ^ n) x) x}

Tactic:
simp [zero_pow (one_le_iff_ne_zero.1 hn), h0]

Result:
no goals

Proof state:
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
A : (fun n => ↑n ^ k) =o[atTop] fun n => (r₂ / ‖r₁‖) ^ n
this : (fun n => r₁ ^ n) =O[atTop] fun n => ‖r₁‖ ^ n
⊢ (fun n => ↑n ^ k * r₁ ^ n) =o[atTop] fun n => r₂ ^ n

Tactic:
simpa [div_mul_cancel₀ _ (pow_pos h0 _).ne', div_pow] using A.mul_isBigO this

Result:
no goals

Proof state:
case neg
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
A : (fun n => ↑n ^ k) =o[atTop] fun n => (r₂ / ‖r₁‖) ^ n
⊢ (fun n => r₁ ^ n) =O[atTop] fun n => ‖r₁‖ ^ n

Tactic:
exact .of_norm_eventuallyLE <| eventually_norm_pow_le r₁

Result:
no goals

Proof state:
case neg
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
A : (fun n => ↑n ^ k) =o[atTop] fun n => (r₂ / ‖r₁‖) ^ n
⊢ (fun n => ↑n ^ k * r₁ ^ n) =o[atTop] fun n => r₂ ^ n

Tactic:
suffices (fun n ↦ r₁ ^ n) =O[atTop] fun n ↦ ‖r₁‖ ^ n by
  simpa [div_mul_cancel₀ _ (pow_pos h0 _).ne', div_pow] using A.mul_isBigO this

Result:
case neg
R : Type u_2
inst✝ : NormedRing R
k : ℕ
r₁ : R
r₂ : ℝ
h : ‖r₁‖ < r₂
h0 : 0 < ‖r₁‖
A : (fun n => ↑n ^ k) =o[atTop] fun n => (r₂ / ‖r₁‖) ^ n
⊢ (fun n => r₁ ^ n) =O[atTop] fun n => ‖r₁‖ ^ n