no goals
α : Type u_1
β : Type ?u.2829
inst✝ : DecidablePred fun l => l ≠ []
L : List (List α)
⊢ join (filter (fun l => decide (l ≠ [])) L) = join L
simp [join_filter_isEmpty_eq_false, ← isEmpty_iff_eq_nil]