M : Type u_1
N : Type ?u.64181
P : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y : M
g : Con.Quotient c →* P
x : M
H : c ≤ ker (MonoidHom.comp g (mk' c))
⊢ ↑g ↑x = ↑(lift c (MonoidHom.comp g (mk' c)) H) ↑x
M : Type u_1
N : Type ?u.64181
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
g : Con.Quotient c →* P
Hg : MonoidHom.comp g (mk' c) = f
x : M
⊢ ↑g ↑x = ↑(lift c f H) ↑x
subst f
no goals
M : Type u_1
N : Type ?u.64181
P : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y : M
g : Con.Quotient c →* P
x : M
H : c ≤ ker (MonoidHom.comp g (mk' c))
⊢ ↑g ↑x = ↑(lift c (MonoidHom.comp g (mk' c)) H) ↑x
rfl