Theorem: Sublattice.prod_eq_top (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 : α
inst✝¹ : Nonempty α
inst✝ : Nonempty β
M : Sublattice β
⊢ L.prod M = ⊤ ↔ L = ⊤ ∧ M = ⊤
Tactic:
simpa only [← coe_inj] using Set.prod_eq_univ
State after:
no goals