case h
M : Type u_1
N : Type ?u.60480
P : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x y : M
f : M →* P
H : c ≤ ker f
x✝ : M
⊢ ↑(MonoidHom.comp (lift c f H) (mk' c)) x✝ = ↑f x✝
M : Type u_1
N : Type ?u.60480
P : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x y : M
f : M →* P
H : c ≤ ker f
⊢ MonoidHom.comp (lift c f H) (mk' c) = f
ext
no goals
case h
M : Type u_1
N : Type ?u.60480
P : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x y : M
f : M →* P
H : c ≤ ker f
x✝ : M
⊢ ↑(MonoidHom.comp (lift c f H) (mk' c)) x✝ = ↑f x✝
rfl