no goals
F : Type ?u.77892
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.77904
ι : Sort ?u.77907
κ : ι → Sort ?u.77912
inst✝³ : CompleteLattice α
inst✝² : CompleteLattice β
inst✝¹ : CompleteLattice γ
inst✝ : CompleteLattice δ
g : CompleteLatticeHom β γ
f₁ f₂ : CompleteLatticeHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
rw [← comp_apply, h, comp_apply]