Theorem: latticeClosure_prod (LeanCamCombi/Mathlib/Order/SupClosed.lean)

State before:
α : Type u_1
β : Type u_2
inst✝¹ : DistribLattice α
inst✝ : DistribLattice β
s✝ s : Set α
t : Set β
⊢ latticeClosure (s ×ˢ t) = latticeClosure s ×ˢ latticeClosure t
Tactic:
simp_rw [← supClosure_infClosure]
State after:
α : Type u_1
β : Type u_2
inst✝¹ : DistribLattice α
inst✝ : DistribLattice β
s✝ s : Set α
t : Set β
⊢ supClosure (infClosure (s ×ˢ t)) = supClosure (infClosure s) ×ˢ supClosure (infClosure t)

State before:
α : Type u_1
β : Type u_2
inst✝¹ : DistribLattice α
inst✝ : DistribLattice β
s✝ s : Set α
t : Set β
⊢ supClosure (infClosure (s ×ˢ t)) = supClosure (infClosure s) ×ˢ supClosure (infClosure t)
Tactic:
simp
State after:
no goals