case mk.mk.refl
G✝ : Type ?u.58954
G : Type u
toGroup✝ : Group G
mul_comm✝¹ mul_comm✝ : ∀ (a b : G), a * b = b * a
⊢ mk mul_comm✝¹ = mk mul_comm✝
G✝ : Type ?u.58954
G : Type u
⊢ Injective (@toGroup G)
rintro ⟨⟩ ⟨⟩ ⟨⟩
no goals
case mk.mk.refl
G✝ : Type ?u.58954
G : Type u
toGroup✝ : Group G
mul_comm✝¹ mul_comm✝ : ∀ (a b : G), a * b = b * a
⊢ mk mul_comm✝¹ = mk mul_comm✝
rfl