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