no goals
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 : P
R : ℝ
⊢ inversion c R c = c
simp [inversion]