case inl
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d x✝ y z : P
R✝ : ℝ
x : P
R : ℝ
⊢ dist (inversion x R x) x = R ^ 2 / dist x x

case inr
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c✝ d x✝ y z : P
R✝ : ℝ
c x : P
R : ℝ
hx : x ≠ c
⊢ dist (inversion c R x) c = R ^ 2 / dist x c
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c✝ d x✝ y z : P
R✝ : ℝ
c x : P
R : ℝ
⊢ dist (inversion c R x) c = R ^ 2 / dist x c
rcases eq_or_ne x c with (rfl | hx)
case inr
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c✝ d x✝ y z : P
R✝ : ℝ
c x : P
R : ℝ
hx : x ≠ c
this : dist x c ≠ 0
⊢ dist (inversion c R x) c = R ^ 2 / dist x c
case inr
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c✝ d x✝ y z : P
R✝ : ℝ
c x : P
R : ℝ
hx : x ≠ c
⊢ dist (inversion c R x) c = R ^ 2 / dist x c
have : dist x c ≠ 0 := dist_ne_zero.2 hx
no goals
case inr
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c✝ d x✝ y z : P
R✝ : ℝ
c x : P
R : ℝ
hx : x ≠ c
this : dist x c ≠ 0
⊢ dist (inversion c R x) c = R ^ 2 / dist x c
field_simp [inversion, norm_smul, abs_div, ← dist_eq_norm_vsub, sq, mul_assoc]
no goals
case inl
V : Type u_2
P : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d x✝ y z : P
R✝ : ℝ
x : P
R : ℝ
⊢ dist (inversion x R x) x = R ^ 2 / dist x x
simp