case h
α : Type u_1
β : Type ?u.177459
inst✝ : SemilatticeInf α
a b x : α
⊢ x ∈ Iic a ∩ Iic b ↔ x ∈ Iic (a ⊓ b)
α : Type u_1
β : Type ?u.177459
inst✝ : SemilatticeInf α
a b : α
⊢ Iic a ∩ Iic b = Iic (a ⊓ b)
ext x
no goals
case h
α : Type u_1
β : Type ?u.177459
inst✝ : SemilatticeInf α
a b x : α
⊢ x ∈ Iic a ∩ Iic b ↔ x ∈ Iic (a ⊓ b)
simp [Iic]