Theorem: Sublattice.le_prod_iff (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 : α
M : Sublattice β
N : Sublattice (α × β)
⊢ N ≤ L.prod M ↔ N ≤ comap (LatticeHom.fst α β) L ∧ N ≤ comap (LatticeHom.snd α β) M
Tactic:
simp [SetLike.le_def, forall_and]
State after:
no goals