no goals
M : Type u
G : Type v
X : Type w
inst✝⁶ : PseudoEMetricSpace X
inst✝⁵ : Group G
inst✝⁴ : MulAction G X
inst✝³ : IsometricSMul G X
inst✝² : PseudoEMetricSpace G
inst✝¹ : IsometricSMul G G
inst✝ : IsometricSMul Gᵐᵒᵖ G
x y : G
⊢ edist x⁻¹ y = edist x y⁻¹
rw [← edist_inv_inv, inv_inv]