Theorem: Sublattice.top_prod (LeanCamCombi/Mathlib/Order/Sublattice.lean)

State before:
ι : 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 ∈ ⊤.prod L ↔ a ∈ comap (LatticeHom.snd α β) L
Tactic:
simp [mem_prod, LatticeHom.coe_snd]
State after:
no goals