no goals
F : Type ?u.76609
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.76621
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
g : BoundedOrderHom β γ
f₁ f₂ : BoundedOrderHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
rw [← BoundedOrderHom.comp_apply, h, BoundedOrderHom.comp_apply]