no goals
F : Type ?u.49422
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.49434
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : Preorder α
inst✝⁵ : NonAssocSemiring β
inst✝⁴ : Preorder β
inst✝³ : NonAssocSemiring γ
inst✝² : Preorder γ
inst✝¹ : NonAssocSemiring δ
inst✝ : Preorder δ
f : β →+*o γ
g₁ g₂ : α →+*o β
hf : Injective ↑f
h : OrderRingHom.comp f g₁ = OrderRingHom.comp f g₂
a : α
⊢ ↑f (↑g₁ a) = ↑f (↑g₂ a)
rw [← comp_apply, h, comp_apply]