no goals
F : Type ?u.48360
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.48372
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : Preorder α
inst✝⁵ : NonAssocSemiring β
inst✝⁴ : Preorder β
inst✝³ : NonAssocSemiring γ
inst✝² : Preorder γ
inst✝¹ : NonAssocSemiring δ
inst✝ : Preorder δ
f₁ f₂ : β →+*o γ
g : α →+*o β
hg : Surjective ↑g
h : f₁ = f₂
⊢ OrderRingHom.comp f₁ g = OrderRingHom.comp f₂ g
rw [h]