case nil
α : Type u_1
β : Type ?u.31644
is'✝ ts is' : List α
⊢ permutationsAux ([] ++ ts) is' =
    map (fun x => x ++ ts) (permutationsAux [] is') ++ permutationsAux ts (reverse [] ++ is')

case cons
α : Type u_1
β : Type ?u.31644
is'✝ ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    permutationsAux (is ++ ts) is' =
      map (fun x => x ++ ts) (permutationsAux is is') ++ permutationsAux ts (reverse is ++ is')
is' : List α
⊢ permutationsAux (t :: is ++ ts) is' =
    map (fun x => x ++ ts) (permutationsAux (t :: is) is') ++ permutationsAux ts (reverse (t :: is) ++ is')
α : Type u_1
β : Type ?u.31644
is is' ts : List α
⊢ permutationsAux (is ++ ts) is' =
    map (fun x => x ++ ts) (permutationsAux is is') ++ permutationsAux ts (reverse is ++ is')
induction' is with t is ih generalizing is'
case cons
α : Type u_1
β : Type ?u.31644
is'✝ ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    permutationsAux (is ++ ts) is' =
      map (fun x => x ++ ts) (permutationsAux is is') ++ permutationsAux ts (reverse is ++ is')
is' : List α
⊢ (List.bind (permutations is') fun y => (permutationsAux2 t (is ++ ts) [] y id).snd) ++
      (map (fun x => x ++ ts) (permutationsAux is (t :: is')) ++ permutationsAux ts (reverse is ++ t :: is')) =
    (List.bind (permutations is') fun a => map (fun x => x ++ ts) (permutationsAux2 t is [] a id).snd) ++
      (map (fun x => x ++ ts) (permutationsAux is (t :: is')) ++ permutationsAux ts (reverse is ++ t :: ([] ++ is')))
case cons
α : Type u_1
β : Type ?u.31644
is'✝ ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    permutationsAux (is ++ ts) is' =
      map (fun x => x ++ ts) (permutationsAux is is') ++ permutationsAux ts (reverse is ++ is')
is' : List α
⊢ permutationsAux (t :: is ++ ts) is' =
    map (fun x => x ++ ts) (permutationsAux (t :: is) is') ++ permutationsAux ts (reverse (t :: is) ++ is')
simp only [foldr_permutationsAux2, ih, bind_map, cons_append, permutationsAux_cons, map_append,
  reverse_cons, append_assoc, singleton_append]
case cons.e_a.e_b
α : Type u_1
β : Type ?u.31644
is'✝ ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    permutationsAux (is ++ ts) is' =
      map (fun x => x ++ ts) (permutationsAux is is') ++ permutationsAux ts (reverse is ++ is')
is' : List α
⊢ (fun y => (permutationsAux2 t (is ++ ts) [] y id).snd) = fun a =>
    map (fun x => x ++ ts) (permutationsAux2 t is [] a id).snd
case cons
α : Type u_1
β : Type ?u.31644
is'✝ ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    permutationsAux (is ++ ts) is' =
      map (fun x => x ++ ts) (permutationsAux is is') ++ permutationsAux ts (reverse is ++ is')
is' : List α
⊢ (List.bind (permutations is') fun y => (permutationsAux2 t (is ++ ts) [] y id).snd) ++
      (map (fun x => x ++ ts) (permutationsAux is (t :: is')) ++ permutationsAux ts (reverse is ++ t :: is')) =
    (List.bind (permutations is') fun a => map (fun x => x ++ ts) (permutationsAux2 t is [] a id).snd) ++
      (map (fun x => x ++ ts) (permutationsAux is (t :: is')) ++ permutationsAux ts (reverse is ++ t :: ([] ++ is')))
congr 2
case cons.e_a.e_b.h
α : Type u_1
β : Type ?u.31644
is'✝ ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    permutationsAux (is ++ ts) is' =
      map (fun x => x ++ ts) (permutationsAux is is') ++ permutationsAux ts (reverse is ++ is')
is' x✝ : List α
⊢ (permutationsAux2 t (is ++ ts) [] x✝ id).snd = map (fun x => x ++ ts) (permutationsAux2 t is [] x✝ id).snd
case cons.e_a.e_b
α : Type u_1
β : Type ?u.31644
is'✝ ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    permutationsAux (is ++ ts) is' =
      map (fun x => x ++ ts) (permutationsAux is is') ++ permutationsAux ts (reverse is ++ is')
is' : List α
⊢ (fun y => (permutationsAux2 t (is ++ ts) [] y id).snd) = fun a =>
    map (fun x => x ++ ts) (permutationsAux2 t is [] a id).snd
funext _
case cons.e_a.e_b.h
α : Type u_1
β : Type ?u.31644
is'✝ ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    permutationsAux (is ++ ts) is' =
      map (fun x => x ++ ts) (permutationsAux is is') ++ permutationsAux ts (reverse is ++ is')
is' x✝ : List α
⊢ (permutationsAux2 t (is ++ ts) [] x✝ id).snd = (permutationsAux2 t is [] x✝ fun x => x ++ ts).snd
case cons.e_a.e_b.h
α : Type u_1
β : Type ?u.31644
is'✝ ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    permutationsAux (is ++ ts) is' =
      map (fun x => x ++ ts) (permutationsAux is is') ++ permutationsAux ts (reverse is ++ is')
is' x✝ : List α
⊢ (permutationsAux2 t (is ++ ts) [] x✝ id).snd = map (fun x => x ++ ts) (permutationsAux2 t is [] x✝ id).snd
rw [map_permutationsAux2]
case cons.e_a.e_b.h
α : Type u_1
β : Type ?u.31644
is'✝ ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    permutationsAux (is ++ ts) is' =
      map (fun x => x ++ ts) (permutationsAux is is') ++ permutationsAux ts (reverse is ++ is')
is' x✝ : List α
⊢ (permutationsAux2 t [] [] x✝ fun x => id (x ++ (is ++ ts))).snd =
    (permutationsAux2 t [] [] x✝ fun x => x ++ is ++ ts).snd
case cons.e_a.e_b.h
α : Type u_1
β : Type ?u.31644
is'✝ ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    permutationsAux (is ++ ts) is' =
      map (fun x => x ++ ts) (permutationsAux is is') ++ permutationsAux ts (reverse is ++ is')
is' x✝ : List α
⊢ (permutationsAux2 t (is ++ ts) [] x✝ id).snd = (permutationsAux2 t is [] x✝ fun x => x ++ ts).snd
simp (config := { singlePass := true }) only [← permutationsAux2_comp_append]
no goals
case cons.e_a.e_b.h
α : Type u_1
β : Type ?u.31644
is'✝ ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    permutationsAux (is ++ ts) is' =
      map (fun x => x ++ ts) (permutationsAux is is') ++ permutationsAux ts (reverse is ++ is')
is' x✝ : List α
⊢ (permutationsAux2 t [] [] x✝ fun x => id (x ++ (is ++ ts))).snd =
    (permutationsAux2 t [] [] x✝ fun x => x ++ is ++ ts).snd
simp only [id, append_assoc]
no goals
case nil
α : Type u_1
β : Type ?u.31644
is'✝ ts is' : List α
⊢ permutationsAux ([] ++ ts) is' =
    map (fun x => x ++ ts) (permutationsAux [] is') ++ permutationsAux ts (reverse [] ++ is')
simp