R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
⊢ (fun x_1 =>
      (∑ i in range n, (-↑x⁻¹ * x_1) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * x_1) ^ n * inverse (↑x + x_1) -
        (∑ i in range n, (-↑x⁻¹ * x_1) ^ i) * ↑x⁻¹) =O[𝓝 0]
    fun t => ‖t‖ ^ n
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
⊢ (fun t => inverse (↑x + t) - (∑ i in range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹) =O[𝓝 0] fun t => ‖t‖ ^ n
refine EventuallyEq.trans_isBigO (.sub (inverse_add_nth_order x n) (.refl _ _)) ?_
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
⊢ (fun x_1 => (-↑x⁻¹ * x_1) ^ n * inverse (↑x + x_1)) =O[𝓝 0] fun t => ‖t‖ ^ n
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
⊢ (fun x_1 =>
      (∑ i in range n, (-↑x⁻¹ * x_1) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * x_1) ^ n * inverse (↑x + x_1) -
        (∑ i in range n, (-↑x⁻¹ * x_1) ^ i) * ↑x⁻¹) =O[𝓝 0]
    fun t => ‖t‖ ^ n
simp only [add_sub_cancel']
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
⊢ (fun x_1 => ‖(-↑x⁻¹ * x_1) ^ n‖ * 1) =O[𝓝 0] fun t => ‖t‖ ^ n
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
⊢ (fun x_1 => (-↑x⁻¹ * x_1) ^ n * inverse (↑x + x_1)) =O[𝓝 0] fun t => ‖t‖ ^ n
refine ((isBigO_refl _ _).norm_right.mul (inverse_add_norm x)).trans ?_
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
⊢ (fun x_1 => (-↑x⁻¹ * x_1) ^ n) =O[𝓝 0] fun t => ‖t‖ ^ n
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
⊢ (fun x_1 => ‖(-↑x⁻¹ * x_1) ^ n‖ * 1) =O[𝓝 0] fun t => ‖t‖ ^ n
simp only [mul_one, isBigO_norm_left]
no goals
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
⊢ (fun x_1 => (-↑x⁻¹ * x_1) ^ n) =O[𝓝 0] fun t => ‖t‖ ^ n
exact ((isBigO_refl _ _).norm_right.const_mul_left _).pow _