no goals
F : Type ?u.55900
ι : Type ?u.55903
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.55915
inst✝³ : Sup α
inst✝² : Sup β
inst✝¹ : Sup γ
inst✝ : Sup δ
g : SupHom β γ
f₁ f₂ : SupHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
rw [← SupHom.comp_apply, h, SupHom.comp_apply]