Theorem: List.join_intersperse_nil (One.lean)

State before:
α : Type u_1
l : List (List α)
⊢ join (intersperse [] l) = join l
Tactic:
match l with
| [] => simp only [join]
| [a] => simp only [join, append_nil]
| a :: b :: tail =>
  simp only [join, List.join_intersperse_nil, nil_append]
State after:
no goals

State before:
α : Type u_1
l : List (List α)
⊢ join (intersperse [] []) = join []
Tactic:
simp only [join]
State after:
no goals

State before:
α : Type u_1
l : List (List α)
a : List α
⊢ join (intersperse [] [a]) = join [a]
Tactic:
simp only [join, append_nil]
State after:
no goals

State before:
α : Type u_1
l : List (List α)
a b : List α
tail : List (List α)
⊢ join (intersperse [] (a :: b :: tail)) = join (a :: b :: tail)
Tactic:
simp only [join, List.join_intersperse_nil, nil_append]
State after:
no goals