M : Type u_1
N : Type ?u.62273
P : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x y : M
f✝ : M →* P
f g : Con.Quotient c →* P
h : ∀ (a : M), ↑f ↑a = ↑g ↑a
⊢ lift c (MonoidHom.comp f (mk' c)) (_ : ∀ (x y : M), ↑c x y → ↑f ↑x = ↑f ↑y) =
    lift c (MonoidHom.comp g (mk' c)) (_ : ∀ (x y : M), ↑c x y → ↑g ↑x = ↑g ↑y)
M : Type u_1
N : Type ?u.62273
P : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x y : M
f✝ : M →* P
f g : Con.Quotient c →* P
h : ∀ (a : M), ↑f ↑a = ↑g ↑a
⊢ f = g
rw [← lift_apply_mk' f, ← lift_apply_mk' g]
case e_f
M : Type u_1
N : Type ?u.62273
P : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x y : M
f✝ : M →* P
f g : Con.Quotient c →* P
h : ∀ (a : M), ↑f ↑a = ↑g ↑a
⊢ MonoidHom.comp f (mk' c) = MonoidHom.comp g (mk' c)
M : Type u_1
N : Type ?u.62273
P : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x y : M
f✝ : M →* P
f g : Con.Quotient c →* P
h : ∀ (a : M), ↑f ↑a = ↑g ↑a
⊢ lift c (MonoidHom.comp f (mk' c)) (_ : ∀ (x y : M), ↑c x y → ↑f ↑x = ↑f ↑y) =
    lift c (MonoidHom.comp g (mk' c)) (_ : ∀ (x y : M), ↑c x y → ↑g ↑x = ↑g ↑y)
congr 1
no goals
case e_f
M : Type u_1
N : Type ?u.62273
P : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x y : M
f✝ : M →* P
f g : Con.Quotient c →* P
h : ∀ (a : M), ↑f ↑a = ↑g ↑a
⊢ MonoidHom.comp f (mk' c) = MonoidHom.comp g (mk' c)
exact FunLike.ext_iff.2 h