no goals
α : Type u_1
β : Type ?u.1507
inst✝ : DecidablePred fun l => isEmpty l = false
L : List (List α)
⊢ join (filter (fun l => decide (isEmpty l = false)) ([] :: L)) = join ([] :: L)
simp [join_filter_isEmpty_eq_false (L := L), isEmpty_iff_eq_nil]
α : Type u_1
β : Type ?u.1507
inst✝ : DecidablePred fun l => isEmpty l = false
a : α
l : List α
L : List (List α)
cons_not_empty : isEmpty (a :: l) = false
⊢ join (filter (fun l => decide (isEmpty l = false)) ((a :: l) :: L)) = join ((a :: l) :: L)
α : Type u_1
β : Type ?u.1507
inst✝ : DecidablePred fun l => isEmpty l = false
a : α
l : List α
L : List (List α)
⊢ join (filter (fun l => decide (isEmpty l = false)) ((a :: l) :: L)) = join ((a :: l) :: L)
have cons_not_empty : isEmpty (a :: l) = false := rfl
no goals
α : Type u_1
β : Type ?u.1507
inst✝ : DecidablePred fun l => isEmpty l = false
a : α
l : List α
L : List (List α)
cons_not_empty : isEmpty (a :: l) = false
⊢ join (filter (fun l => decide (isEmpty l = false)) ((a :: l) :: L)) = join ((a :: l) :: L)
simp [join_filter_isEmpty_eq_false (L := L), cons_not_empty]