case mk.mk
M : Type u
toLeftCancelMonoid✝¹ : LeftCancelMonoid M
mul_right_cancel✝¹ : ∀ (a b c : M), a * b = c * b → a = c
toLeftCancelMonoid✝ : LeftCancelMonoid M
mul_right_cancel✝ : ∀ (a b c : M), a * b = c * b → a = c
h : toLeftCancelMonoid = toLeftCancelMonoid
⊢ mk mul_right_cancel✝¹ = mk mul_right_cancel✝
M : Type u
⊢ Function.Injective (@toLeftCancelMonoid M)
rintro ⟨⟩ ⟨⟩ h
no goals
case mk.mk
M : Type u
toLeftCancelMonoid✝¹ : LeftCancelMonoid M
mul_right_cancel✝¹ : ∀ (a b c : M), a * b = c * b → a = c
toLeftCancelMonoid✝ : LeftCancelMonoid M
mul_right_cancel✝ : ∀ (a b c : M), a * b = c * b → a = c
h : toLeftCancelMonoid = toLeftCancelMonoid
⊢ mk mul_right_cancel✝¹ = mk mul_right_cancel✝
congr