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
⊢ inversion x (dist x x) 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
hne : x ≠ c
⊢ inversion c (dist x c) x = x
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
⊢ inversion c (dist x c) x = x
rcases eq_or_ne x c with (rfl | hne)
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
⊢ inversion x (dist x x) x = x
apply inversion_self
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
hne : x ≠ c
⊢ dist x c ≠ 0
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
hne : x ≠ c
⊢ inversion c (dist x c) x = x
rw [inversion, div_self, one_pow, one_smul, vsub_vadd]
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
hne : x ≠ c
⊢ dist x c ≠ 0
rwa [dist_ne_zero]