case nil
α : Type u_1
β : Type ?u.18108
x : List α
⊢ x ++ join (map (fun l => l ++ x) []) = join (map (fun l => x ++ l) []) ++ x

case cons
α : Type u_1
β : Type ?u.18108
x head✝ : List α
tail✝ : List (List α)
ih : x ++ join (map (fun l => l ++ x) tail✝) = join (map (fun l => x ++ l) tail✝) ++ x
⊢ x ++ join (map (fun l => l ++ x) (head✝ :: tail✝)) = join (map (fun l => x ++ l) (head✝ :: tail✝)) ++ x
α : Type u_1
β : Type ?u.18108
L : List (List α)
x : List α
⊢ x ++ join (map (fun l => l ++ x) L) = join (map (fun l => x ++ l) L) ++ x
induction' L with _ _ ih
no goals
case nil
α : Type u_1
β : Type ?u.18108
x : List α
⊢ x ++ join (map (fun l => l ++ x) []) = join (map (fun l => x ++ l) []) ++ x
rw [map_nil, join, append_nil, map_nil, join, nil_append]
no goals
case cons
α : Type u_1
β : Type ?u.18108
x head✝ : List α
tail✝ : List (List α)
ih : x ++ join (map (fun l => l ++ x) tail✝) = join (map (fun l => x ++ l) tail✝) ++ x
⊢ x ++ join (map (fun l => l ++ x) (head✝ :: tail✝)) = join (map (fun l => x ++ l) (head✝ :: tail✝)) ++ x
rw [map_cons, join, map_cons, join, append_assoc, ih, append_assoc, append_assoc]