no goals
α : Type ?u.169579
β : Type ?u.169582
M : Type u_1
N : Type u_2
P : Type u_3
G : Type ?u.169594
H : Type ?u.169597
F : Type ?u.169600
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass 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 [← MonoidHom.comp_apply, h, MonoidHom.comp_apply]