no goals
F : Type ?u.38681
α : Type u_3
β : Type u_1
γ : Type u_2
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
g✝ : β →ₙ+* γ
f : α →ₙ+* β
g : β →ₙ+* γ
f₁ f₂ : α →ₙ+* β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
x : α
⊢ ↑g (↑f₁ x) = ↑g (↑f₂ x)
rw [← comp_apply, h, comp_apply]