case h
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
hzero : Tendsto (fun x_1 => -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
t : R
ht : inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
ht' : inverse (1 - -↑x⁻¹ * t) = ∑ i in range n, (-↑x⁻¹ * t) ^ i + (-↑x⁻¹ * t) ^ n * inverse (1 - -↑x⁻¹ * t)
⊢ inverse (↑x + t) = (∑ i in range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (↑x + t)
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
hzero : Tendsto (fun x_1 => -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
⊢ ∀ᶠ (t : R) in 𝓝 0, inverse (↑x + t) = (∑ i in range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (↑x + t)
filter_upwards [inverse_add x, hzero.eventually (inverse_one_sub_nth_order n)] with t ht ht'
case h
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
hzero : Tendsto (fun x_1 => -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
t : R
ht : inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
ht' : inverse (1 + ↑x⁻¹ * t) = ∑ i in range n, (-(↑x⁻¹ * t)) ^ i + (-(↑x⁻¹ * t)) ^ n * inverse (1 + ↑x⁻¹ * t)
⊢ inverse (↑x + t) = (∑ i in range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (↑x + t)
case h
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
hzero : Tendsto (fun x_1 => -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
t : R
ht : inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
ht' : inverse (1 - -↑x⁻¹ * t) = ∑ i in range n, (-↑x⁻¹ * t) ^ i + (-↑x⁻¹ * t) ^ n * inverse (1 - -↑x⁻¹ * t)
⊢ inverse (↑x + t) = (∑ i in range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (↑x + t)
rw [neg_mul, sub_neg_eq_add] at ht'
case h
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
hzero : Tendsto (fun x_1 => -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
t : R
ht : inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
ht' : inverse (1 + ↑x⁻¹ * t) = ∑ i in range n, (-(↑x⁻¹ * t)) ^ i + (-(↑x⁻¹ * t)) ^ n * inverse (1 + ↑x⁻¹ * t)
⊢ (∑ i in range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * (inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹) =
    (∑ i in range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (↑x + t)
case h
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
hzero : Tendsto (fun x_1 => -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
t : R
ht : inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
ht' : inverse (1 + ↑x⁻¹ * t) = ∑ i in range n, (-(↑x⁻¹ * t)) ^ i + (-(↑x⁻¹ * t)) ^ n * inverse (1 + ↑x⁻¹ * t)
⊢ inverse (↑x + t) = (∑ i in range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (↑x + t)
conv_lhs => rw [ht, ht', add_mul, ← neg_mul, mul_assoc]
no goals
case h
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
hzero : Tendsto (fun x_1 => -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
t : R
ht : inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
ht' : inverse (1 + ↑x⁻¹ * t) = ∑ i in range n, (-(↑x⁻¹ * t)) ^ i + (-(↑x⁻¹ * t)) ^ n * inverse (1 + ↑x⁻¹ * t)
⊢ (∑ i in range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * (inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹) =
    (∑ i in range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (↑x + t)
rw [ht]