α : Type u
β : Type v
e✝ e : α ≃ β
inst✝ : Mul β
b : β
⊢ ↑(MulEquiv.symm (mulEquiv e)) b = ↑e.symm b
α : Type u
β : Type v
e✝ e : α ≃ β
inst✝ : Mul β
b : β
⊢ ↑(MulEquiv.symm (mulEquiv e)) b = ↑e.symm b
intros
no goals
α : Type u
β : Type v
e✝ e : α ≃ β
inst✝ : Mul β
b : β
⊢ ↑(MulEquiv.symm (mulEquiv e)) b = ↑e.symm b
rfl