[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a✝ b c d a : α
⊢ symm (mulRight a) = mulRight a⁻¹
[PROOFSTEP]
ext x
[GOAL]
case h.h
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a✝ b c d a x : α
⊢ ↑(symm (mulRight a)) x = ↑(mulRight a⁻¹) x
[PROOFSTEP]
rfl
[GOAL]
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a : α
⊢ symm (mulLeft a) = mulLeft a⁻¹
[PROOFSTEP]
ext x
[GOAL]
case h.h
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a x : α
⊢ ↑(symm (mulLeft a)) x = ↑(mulLeft a⁻¹) x
[PROOFSTEP]
rfl
