simp [mem_prod, LatticeHom.coe_fst]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
L✝ M : Sublattice α
f : LatticeHom α β
s t : Set α
a✝ : α
L : Sublattice α
a : α × β
⊢ a ∈ L.prod ⊤ ↔ a ∈ comap (LatticeHom.fst α β) L
no goals