no goals
α : Type ?u.170280
β : Type ?u.170283
M : Type u_1
N : Type u_2
P : Type u_3
G : Type ?u.170295
H : Type ?u.170298
F : Type ?u.170301
inst✝² : MulZeroOneClass M
inst✝¹ : MulZeroOneClass N
inst✝ : MulZeroOneClass P
g : N →*₀ P
f₁ f₂ : M →*₀ N
hg : Function.Injective ↑g
h : comp g f₁ = comp g f₂
x : M
⊢ ↑g (↑f₁ x) = ↑g (↑f₂ x)
rw [← MonoidWithZeroHom.comp_apply, h,
MonoidWithZeroHom.comp_apply]