-- Mathlib/Analysis/Normed/Ring/Units.lean
theorem inverse_add_nth_order (x : Rˣ) (n : ℕ) :
    ∀ᶠ t in 𝓝 0, inverse ((x : R) + t) =
      (∑ i ∈ range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (x + t)

Proof state:
case h
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries 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 ∈ range n, (-↑x⁻¹ * t) ^ i + (-↑x⁻¹ * t) ^ n * inverse (1 - -↑x⁻¹ * t)
⊢ inverse (↑x + t) = (∑ i ∈ range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (↑x + t)

Tactic:
rw [neg_mul, sub_neg_eq_add] at ht'

Result:
case h
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries 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 ∈ range n, (-(↑x⁻¹ * t)) ^ i + (-(↑x⁻¹ * t)) ^ n * inverse (1 + ↑x⁻¹ * t)
⊢ inverse (↑x + t) = (∑ i ∈ range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (↑x + t)

Proof state:
case h
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries 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 ∈ range n, (-(↑x⁻¹ * t)) ^ i + (-(↑x⁻¹ * t)) ^ n * inverse (1 + ↑x⁻¹ * t)
⊢ (∑ i ∈ range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * (inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹) =
    (∑ i ∈ range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (↑x + t)

Tactic:
rw [ht]

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries 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 ∈ range n, (-(↑x⁻¹ * t)) ^ i + (-(↑x⁻¹ * t)) ^ n * inverse (1 + ↑x⁻¹ * t)
⊢ inverse (↑x + t) = (∑ i ∈ range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (↑x + t)

Tactic:
conv_lhs => rw [ht, ht', add_mul, ← neg_mul, mul_assoc]

Result:
case h
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries 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 ∈ range n, (-(↑x⁻¹ * t)) ^ i + (-(↑x⁻¹ * t)) ^ n * inverse (1 + ↑x⁻¹ * t)
⊢ (∑ i ∈ range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * (inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹) =
    (∑ i ∈ range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (↑x + t)

Proof state:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
n : ℕ
hzero : Tendsto (fun x_1 => -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
⊢ ∀ᶠ (t : R) in 𝓝 0, inverse (↑x + t) = (∑ i ∈ range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (↑x + t)

Tactic:
filter_upwards [inverse_add x, hzero.eventually (inverse_one_sub_nth_order n)] with t ht ht'

Result:
case h
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries 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 ∈ range n, (-↑x⁻¹ * t) ^ i + (-↑x⁻¹ * t) ^ n * inverse (1 - -↑x⁻¹ * t)
⊢ inverse (↑x + t) = (∑ i ∈ range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (↑x + t)