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
a b : G
⊢ edist a⁻¹ b⁻¹ = edist a b
rw [← edist_mul_left a, ← edist_mul_right _ _ b, mul_right_inv, one_mul, inv_mul_cancel_right,
  edist_comm]