simpa only [← coe_inj] using Set.prod_eq_univ
ι : 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 = ⊤
no goals