R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
✝ : Nontrivial R
⊢ ∀ᶠ (t : R) in 𝓝 0, inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
⊢ ∀ᶠ (t : R) in 𝓝 0, inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
nontriviality R
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
✝ : Nontrivial R
⊢ ∃ ε, ε > 0 ∧ ∀ ⦃y : R⦄, dist y 0 < ε → inverse (↑x + y) = inverse (1 + ↑x⁻¹ * y) * ↑x⁻¹
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
✝ : Nontrivial R
⊢ ∀ᶠ (t : R) in 𝓝 0, inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
rw [Metric.eventually_nhds_iff]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
✝ : Nontrivial R
t : R
ht : dist t 0 < ‖↑x⁻¹‖⁻¹
⊢ inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
✝ : Nontrivial R
⊢ ∃ ε, ε > 0 ∧ ∀ ⦃y : R⦄, dist y 0 < ε → inverse (↑x + y) = inverse (1 + ↑x⁻¹ * y) * ↑x⁻¹
refine ⟨‖(↑x⁻¹ : R)‖⁻¹, by cancel_denoms, fun t ht ↦ ?_⟩
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
✝ : Nontrivial R
t : R
ht : ‖t‖ < ‖↑x⁻¹‖⁻¹
⊢ inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
✝ : Nontrivial R
t : R
ht : dist t 0 < ‖↑x⁻¹‖⁻¹
⊢ inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
rw [dist_zero_right] at ht
no goals
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
✝ : Nontrivial R
t : R
ht : ‖t‖ < ‖↑x⁻¹‖⁻¹
⊢ inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
rw [← x.add_val t ht, inverse_unit, Units.add, Units.copy_eq, mul_inv_rev, Units.val_mul,
  ← inverse_unit, Units.oneSub_val, sub_neg_eq_add]
no goals
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
✝ : Nontrivial R
⊢ ‖↑x⁻¹‖⁻¹ > 0
cancel_denoms