no goals
α : Type u_1
a : α
⊢ a ∈ join [] ↔ ∃ l, l ∈ [] ∧ a ∈ l
simp
no goals
α : Type u_1
a : α
b : List α
l : List (List α)
⊢ a ∈ join (b :: l) ↔ ∃ l_1, l_1 ∈ b :: l ∧ a ∈ l_1
simp [mem_join, or_and_right, exists_or]