no goals
α : Type ?u.167782
β : Type ?u.167785
M : Type u_1
N : Type u_2
P : Type u_3
G : Type ?u.167797
H : Type ?u.167800
F : Type ?u.167803
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
g : OneHom N P
f₁ f₂ : OneHom M N
hg : Function.Injective ↑g
h : comp g f₁ = comp g f₂
x : M
⊢ ↑g (↑f₁ x) = ↑g (↑f₂ x)
rw [← OneHom.comp_apply, h, OneHom.comp_apply]