case h
α : Type u_1
β : Type ?u.180404
inst✝ : SemilatticeSup α
a b x : α
⊢ x ∈ Ici a ∩ Ici b ↔ x ∈ Ici (a ⊔ b)
α : Type u_1
β : Type ?u.180404
inst✝ : SemilatticeSup α
a b : α
⊢ Ici a ∩ Ici b = Ici (a ⊔ b)
ext x
no goals
case h
α : Type u_1
β : Type ?u.180404
inst✝ : SemilatticeSup α
a b x : α
⊢ x ∈ Ici a ∩ Ici b ↔ x ∈ Ici (a ⊔ b)
simp [Ici]