R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
h_is_o : (fun t => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] fun x => 1
⊢ ContinuousAt inverse ↑x
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
⊢ ContinuousAt inverse ↑x
have h_is_o : (fun t : R => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] (fun _ => 1 : R → ℝ) :=
  (inverse_add_norm_diff_first_order x).trans_isLittleO (isLittleO_id_const one_ne_zero).norm_left
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
h_is_o : (fun t => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] fun x => 1
h_lim : Tendsto (fun y => y - ↑x) (𝓝 ↑x) (𝓝 0)
⊢ ContinuousAt inverse ↑x
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
h_is_o : (fun t => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] fun x => 1
⊢ ContinuousAt inverse ↑x
have h_lim : Tendsto (fun y : R => y - x) (𝓝 x) (𝓝 0) := by
  refine' tendsto_zero_iff_norm_tendsto_zero.mpr _
  exact tendsto_iff_norm_tendsto_zero.mp tendsto_id
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
h_is_o : (fun t => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] fun x => 1
h_lim : Tendsto (fun y => y - ↑x) (𝓝 ↑x) (𝓝 0)
⊢ Tendsto (fun e => ‖inverse e - ↑x⁻¹‖) (𝓝 ↑x) (𝓝 0)
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
h_is_o : (fun t => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] fun x => 1
h_lim : Tendsto (fun y => y - ↑x) (𝓝 ↑x) (𝓝 0)
⊢ ContinuousAt inverse ↑x
rw [ContinuousAt, tendsto_iff_norm_tendsto_zero, inverse_unit]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
h_is_o : (fun t => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] fun x => 1
⊢ Tendsto (fun e => ‖e - ↑x‖) (𝓝 ↑x) (𝓝 0)
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
h_is_o : (fun t => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] fun x => 1
⊢ Tendsto (fun y => y - ↑x) (𝓝 ↑x) (𝓝 0)
refine' tendsto_zero_iff_norm_tendsto_zero.mpr _
no goals
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
h_is_o : (fun t => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] fun x => 1
⊢ Tendsto (fun e => ‖e - ↑x‖) (𝓝 ↑x) (𝓝 0)
exact tendsto_iff_norm_tendsto_zero.mp tendsto_id