no goals
α : Type ?u.168920
β : Type ?u.168923
M : Type u_1
N : Type u_2
P : Type u_3
G : Type ?u.168935
H : Type ?u.168938
F : Type ?u.168941
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul 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 [← MulHom.comp_apply, h, MulHom.comp_apply]