[GOAL]
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
y : α
ys : List α
f : List α → β
⊢ (permutationsAux2 t ts r (y :: ys) f).fst = y :: ys ++ ts
[PROOFSTEP]
simp [permutationsAux2, permutationsAux2_fst t _ _ ys]
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
y : α
ys : List α
f : List α → β
⊢ (permutationsAux2 t ts r (y :: ys) f).snd =
    f (t :: y :: ys ++ ts) :: (permutationsAux2 t ts r ys fun x => f (y :: x)).snd
[PROOFSTEP]
simp [permutationsAux2, permutationsAux2_fst t _ _ ys]
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
ys : List α
f : List α → β
⊢ (permutationsAux2 t ts [] ys f).snd ++ r = (permutationsAux2 t ts r ys f).snd
[PROOFSTEP]
induction ys generalizing f
[GOAL]
case nil
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
f : List α → β
⊢ (permutationsAux2 t ts [] [] f).snd ++ r = (permutationsAux2 t ts r [] f).snd
[PROOFSTEP]
simp [*]
[GOAL]
case cons
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (f : List α → β), (permutationsAux2 t ts [] tail✝ f).snd ++ r = (permutationsAux2 t ts r tail✝ f).snd
f : List α → β
⊢ (permutationsAux2 t ts [] (head✝ :: tail✝) f).snd ++ r = (permutationsAux2 t ts r (head✝ :: tail✝) f).snd
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts ys : List α
r : List β
f : List α → β
⊢ (permutationsAux2 t [] r ys fun x => f (x ++ ts)).snd = (permutationsAux2 t ts r ys f).snd
[PROOFSTEP]
induction' ys with ys_hd _ ys_ih generalizing f
[GOAL]
case nil
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
f✝ f : List α → β
⊢ (permutationsAux2 t [] r [] fun x => f (x ++ ts)).snd = (permutationsAux2 t ts r [] f).snd
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
f✝ : List α → β
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β), (permutationsAux2 t [] r tail✝ fun x => f (x ++ ts)).snd = (permutationsAux2 t ts r tail✝ f).snd
f : List α → β
⊢ (permutationsAux2 t [] r (ys_hd :: tail✝) fun x => f (x ++ ts)).snd = (permutationsAux2 t ts r (ys_hd :: tail✝) f).snd
[PROOFSTEP]
simp [ys_ih fun xs => f (ys_hd :: xs)]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
α' : Type u_5
β' : Type u_6
g : α → α'
g' : β → β'
t : α
ts ys : List α
r : List β
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ map g' (permutationsAux2 t ts r ys f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g ys) f').snd
[PROOFSTEP]
induction' ys with ys_hd _ ys_ih generalizing f f'
[GOAL]
case nil
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
α' : Type u_5
β' : Type u_6
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
f✝ : List α → β
f'✝ : List α' → β'
H✝ : ∀ (a : List α), g' (f✝ a) = f'✝ (map g a)
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ map g' (permutationsAux2 t ts r [] f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g []) f').snd
[PROOFSTEP]
simp
[GOAL]
case cons
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
α' : Type u_5
β' : Type u_6
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
f✝ : List α → β
f'✝ : List α' → β'
H✝ : ∀ (a : List α), g' (f✝ a) = f'✝ (map g a)
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ map g' (permutationsAux2 t ts r (ys_hd :: tail✝) f).snd =
    (permutationsAux2 (g t) (map g ts) (map g' r) (map g (ys_hd :: tail✝)) f').snd
[PROOFSTEP]
simp only [map, permutationsAux2_snd_cons, cons_append, cons.injEq]
[GOAL]
case cons
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
α' : Type u_5
β' : Type u_6
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
f✝ : List α → β
f'✝ : List α' → β'
H✝ : ∀ (a : List α), g' (f✝ a) = f'✝ (map g a)
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ g' (f (t :: ys_hd :: (permutationsAux2 t ts r tail✝ fun x => f (ys_hd :: x)).fst)) =
      f' (g t :: g ys_hd :: (map g tail✝ ++ map g ts)) ∧
    map g' (permutationsAux2 t ts r tail✝ fun x => f (ys_hd :: x)).snd =
      (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) fun x => f' (g ys_hd :: x)).snd
[PROOFSTEP]
rw [ys_ih, permutationsAux2_fst]
[GOAL]
case cons
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
α' : Type u_5
β' : Type u_6
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
f✝ : List α → β
f'✝ : List α' → β'
H✝ : ∀ (a : List α), g' (f✝ a) = f'✝ (map g a)
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ g' (f (t :: ys_hd :: (tail✝ ++ ts))) = f' (g t :: g ys_hd :: (map g tail✝ ++ map g ts)) ∧
    (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) ?cons.f').snd =
      (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) fun x => f' (g ys_hd :: x)).snd
case cons.f'
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
α' : Type u_5
β' : Type u_6
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
f✝ : List α → β
f'✝ : List α' → β'
H✝ : ∀ (a : List α), g' (f✝ a) = f'✝ (map g a)
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ List α' → β'
case cons.f'
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
α' : Type u_5
β' : Type u_6
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
f✝ : List α → β
f'✝ : List α' → β'
H✝ : ∀ (a : List α), g' (f✝ a) = f'✝ (map g a)
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ List α' → β'
case cons.H
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
α' : Type u_5
β' : Type u_6
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
f✝ : List α → β
f'✝ : List α' → β'
H✝ : ∀ (a : List α), g' (f✝ a) = f'✝ (map g a)
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ ∀ (a : List α), g' (f (ys_hd :: a)) = ?cons.f' (map g a)
[PROOFSTEP]
refine' ⟨_, rfl⟩
[GOAL]
case cons
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
α' : Type u_5
β' : Type u_6
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
f✝ : List α → β
f'✝ : List α' → β'
H✝ : ∀ (a : List α), g' (f✝ a) = f'✝ (map g a)
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ g' (f (t :: ys_hd :: (tail✝ ++ ts))) = f' (g t :: g ys_hd :: (map g tail✝ ++ map g ts))
[PROOFSTEP]
simp only [← map_cons, ← map_append]
[GOAL]
case cons
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
α' : Type u_5
β' : Type u_6
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
f✝ : List α → β
f'✝ : List α' → β'
H✝ : ∀ (a : List α), g' (f✝ a) = f'✝ (map g a)
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ g' (f (t :: ys_hd :: (tail✝ ++ ts))) = f' (map g (t :: ys_hd :: (tail✝ ++ ts)))
[PROOFSTEP]
apply H
[GOAL]
case cons.H
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
α' : Type u_5
β' : Type u_6
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
f✝ : List α → β
f'✝ : List α' → β'
H✝ : ∀ (a : List α), g' (f✝ a) = f'✝ (map g a)
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ ∀ (a : List α), g' (f (ys_hd :: a)) = f' (g ys_hd :: map g a)
[PROOFSTEP]
intro a
[GOAL]
case cons.H
α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
α' : Type u_5
β' : Type u_6
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
f✝ : List α → β
f'✝ : List α' → β'
H✝ : ∀ (a : List α), g' (f✝ a) = f'✝ (map g a)
ys_hd : α
tail✝ : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β'),
    (∀ (a : List α), g' (f a) = f' (map g a)) →
      map g' (permutationsAux2 t ts r tail✝ f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail✝) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
a : List α
⊢ g' (f (ys_hd :: a)) = f' (g ys_hd :: map g a)
[PROOFSTEP]
apply H
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ map f (permutationsAux2 t ts [] ys id).snd = (permutationsAux2 t ts [] ys f).snd
[PROOFSTEP]
rw [map_permutationsAux2' id, map_id, map_id]
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ (permutationsAux2 (id t) ts (map f []) ys ?f').snd = (permutationsAux2 t ts [] ys f).snd
case f'
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ List α → β
case f'
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ List α → β
case f'
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ List α → β
case H α : Type u_1 β : Type u_2 t : α ts ys : List α f : List α → β ⊢ ∀ (a : List α), f (id a) = ?f' (map id a)
[PROOFSTEP]
rfl
[GOAL]
case H
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ ∀ (a : List α), f (id a) = f (map id a)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
ys : List α
f : List α → β
⊢ (permutationsAux2 t ts r ys f).snd = map (fun x => f (x ++ ts)) (permutationsAux2 t [] [] ys id).snd ++ r
[PROOFSTEP]
rw [← permutationsAux2_append, map_permutationsAux2, permutationsAux2_comp_append]
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
t : α
ts : List α
⊢ map (map f) (permutations'Aux t ts) = permutations'Aux (f t) (map f ts)
[PROOFSTEP]
induction' ts with a ts ih <;> [rfl; (simp [← ih]; rfl)]
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
t : α
ts : List α
⊢ map (map f) (permutations'Aux t ts) = permutations'Aux (f t) (map f ts)
[PROOFSTEP]
induction' ts with a ts ih
[GOAL]
case nil
α : Type u_1
β : Type u_2
f : α → β
t : α
⊢ map (map f) (permutations'Aux t []) = permutations'Aux (f t) (map f [])
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
β : Type u_2
f : α → β
t a : α
ts : List α
ih : map (map f) (permutations'Aux t ts) = permutations'Aux (f t) (map f ts)
⊢ map (map f) (permutations'Aux t (a :: ts)) = permutations'Aux (f t) (map f (a :: ts))
[PROOFSTEP]
simp [← ih]
[GOAL]
case cons
α : Type u_1
β : Type u_2
f : α → β
t a : α
ts : List α
ih : map (map f) (permutations'Aux t ts) = permutations'Aux (f t) (map f ts)
⊢ map (map f ∘ cons a) (permutations'Aux t ts) = map (cons (f a) ∘ map f) (permutations'Aux t ts)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts : List α
⊢ permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd
[PROOFSTEP]
induction' ts with a ts ih
[GOAL]
case nil
α : Type u_1
β : Type u_2
t : α
⊢ permutations'Aux t [] = (permutationsAux2 t [] [[] ++ [t]] [] id).snd
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
β : Type u_2
t a : α
ts : List α
ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd
⊢ permutations'Aux t (a :: ts) = (permutationsAux2 t [] [a :: ts ++ [t]] (a :: ts) id).snd
[PROOFSTEP]
simp [permutations'Aux, permutationsAux2_snd_cons, ih]
[GOAL]
case cons
α : Type u_1
β : Type u_2
t a : α
ts : List α
ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd
⊢ map (cons a) (permutationsAux2 t [] [ts ++ [t]] ts id).snd =
    (permutationsAux2 t [] [a :: (ts ++ [t])] ts fun x => a :: x).snd
[PROOFSTEP]
simp (config := { singlePass := true }) only [← permutationsAux2_append]
[GOAL]
case cons
α : Type u_1
β : Type u_2
t a : α
ts : List α
ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd
⊢ map (cons a) ((permutationsAux2 t [] [] ts id).snd ++ [ts ++ [t]]) =
    (permutationsAux2 t [] [] ts fun x => a :: x).snd ++ [a :: (ts ++ [t])]
[PROOFSTEP]
simp [map_permutationsAux2]
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts ys l l' : List α
⊢ l' ∈ (permutationsAux2 t ts [] ys fun x => l ++ x).snd ↔
    ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
[PROOFSTEP]
induction' ys with y ys ih generalizing l
[GOAL]
case nil
α : Type u_1
β : Type u_2
t : α
ts l✝ l' l : List α
⊢ l' ∈ (permutationsAux2 t ts [] [] fun x => l ++ x).snd ↔
    ∃ l₁ l₂, l₂ ≠ [] ∧ [] = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
case cons
α : Type u_1
β : Type u_2
t : α
ts l✝ l' : List α
y : α
ys : List α
ih :
  ∀ {l : List α},
    l' ∈ (permutationsAux2 t ts [] ys fun x => l ++ x).snd ↔
      ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
l : List α
⊢ l' ∈ (permutationsAux2 t ts [] (y :: ys) fun x => l ++ x).snd ↔
    ∃ l₁ l₂, l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
[PROOFSTEP]
rw [permutationsAux2_snd_cons, show (fun x : List α => l ++ y :: x) = (l ++ [y] ++ ·) by funext _; simp, mem_cons, ih]
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts l✝ l' : List α
y : α
ys : List α
ih :
  ∀ {l : List α},
    l' ∈ (permutationsAux2 t ts [] ys fun x => l ++ x).snd ↔
      ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
l : List α
⊢ (fun x => l ++ y :: x) = fun x => l ++ [y] ++ x
[PROOFSTEP]
funext _
[GOAL]
case h
α : Type u_1
β : Type u_2
t : α
ts l✝ l' : List α
y : α
ys : List α
ih :
  ∀ {l : List α},
    l' ∈ (permutationsAux2 t ts [] ys fun x => l ++ x).snd ↔
      ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
l x✝ : List α
⊢ l ++ y :: x✝ = l ++ [y] ++ x✝
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
t : α
ts l✝ l' : List α
y : α
ys : List α
ih :
  ∀ {l : List α},
    l' ∈ (permutationsAux2 t ts [] ys fun x => l ++ x).snd ↔
      ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
l : List α
⊢ (l' = l ++ (t :: y :: ys ++ ts) ∨ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts) ↔
    ∃ l₁ l₂, l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
[PROOFSTEP]
constructor
[GOAL]
case cons.mp
α : Type u_1
β : Type u_2
t : α
ts l✝ l' : List α
y : α
ys : List α
ih :
  ∀ {l : List α},
    l' ∈ (permutationsAux2 t ts [] ys fun x => l ++ x).snd ↔
      ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
l : List α
⊢ (l' = l ++ (t :: y :: ys ++ ts) ∨ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts) →
    ∃ l₁ l₂, l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
[PROOFSTEP]
rintro (rfl | ⟨l₁, l₂, l0, rfl, rfl⟩)
[GOAL]
case cons.mp.inl
α : Type u_1
β : Type u_2
t : α
ts l✝ : List α
y : α
ys l : List α
ih :
  ∀ {l_1 : List α},
    l ++ (t :: y :: ys ++ ts) ∈ (permutationsAux2 t ts [] ys fun x => l_1 ++ x).snd ↔
      ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l ++ (t :: y :: ys ++ ts) = l_1 ++ l₁ ++ t :: l₂ ++ ts
⊢ ∃ l₁ l₂, l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l ++ (t :: y :: ys ++ ts) = l ++ l₁ ++ t :: l₂ ++ ts
[PROOFSTEP]
exact ⟨[], y :: ys, by simp⟩
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts l✝ : List α
y : α
ys l : List α
ih :
  ∀ {l_1 : List α},
    l ++ (t :: y :: ys ++ ts) ∈ (permutationsAux2 t ts [] ys fun x => l_1 ++ x).snd ↔
      ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l ++ (t :: y :: ys ++ ts) = l_1 ++ l₁ ++ t :: l₂ ++ ts
⊢ y :: ys ≠ [] ∧ y :: ys = [] ++ y :: ys ∧ l ++ (t :: y :: ys ++ ts) = l ++ [] ++ t :: y :: ys ++ ts
[PROOFSTEP]
simp
[GOAL]
case cons.mp.inr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
t : α
ts l✝ : List α
y : α
l l₁ l₂ : List α
l0 : l₂ ≠ []
ih :
  ∀ {l_1 : List α},
    l ++ [y] ++ l₁ ++ t :: l₂ ++ ts ∈ (permutationsAux2 t ts [] (l₁ ++ l₂) fun x => l_1 ++ x).snd ↔
      ∃ l₁_1 l₂_1,
        l₂_1 ≠ [] ∧ l₁ ++ l₂ = l₁_1 ++ l₂_1 ∧ l ++ [y] ++ l₁ ++ t :: l₂ ++ ts = l_1 ++ l₁_1 ++ t :: l₂_1 ++ ts
⊢ ∃ l₁_1 l₂_1,
    l₂_1 ≠ [] ∧ y :: (l₁ ++ l₂) = l₁_1 ++ l₂_1 ∧ l ++ [y] ++ l₁ ++ t :: l₂ ++ ts = l ++ l₁_1 ++ t :: l₂_1 ++ ts
[PROOFSTEP]
exact ⟨y :: l₁, l₂, l0, by simp⟩
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts l✝ : List α
y : α
l l₁ l₂ : List α
l0 : l₂ ≠ []
ih :
  ∀ {l_1 : List α},
    l ++ [y] ++ l₁ ++ t :: l₂ ++ ts ∈ (permutationsAux2 t ts [] (l₁ ++ l₂) fun x => l_1 ++ x).snd ↔
      ∃ l₁_1 l₂_1,
        l₂_1 ≠ [] ∧ l₁ ++ l₂ = l₁_1 ++ l₂_1 ∧ l ++ [y] ++ l₁ ++ t :: l₂ ++ ts = l_1 ++ l₁_1 ++ t :: l₂_1 ++ ts
⊢ y :: (l₁ ++ l₂) = y :: l₁ ++ l₂ ∧ l ++ [y] ++ l₁ ++ t :: l₂ ++ ts = l ++ y :: l₁ ++ t :: l₂ ++ ts
[PROOFSTEP]
simp
[GOAL]
case cons.mpr
α : Type u_1
β : Type u_2
t : α
ts l✝ l' : List α
y : α
ys : List α
ih :
  ∀ {l : List α},
    l' ∈ (permutationsAux2 t ts [] ys fun x => l ++ x).snd ↔
      ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
l : List α
⊢ (∃ l₁ l₂, l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts) →
    l' = l ++ (t :: y :: ys ++ ts) ∨ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts
[PROOFSTEP]
rintro ⟨_ | ⟨y', l₁⟩, l₂, l0, ye, rfl⟩
[GOAL]
case cons.mpr.intro.nil.intro.intro.intro
α : Type u_1
β : Type u_2
t : α
ts l✝ : List α
y : α
ys l l₂ : List α
l0 : l₂ ≠ []
ye : y :: ys = [] ++ l₂
ih :
  ∀ {l_1 : List α},
    l ++ [] ++ t :: l₂ ++ ts ∈ (permutationsAux2 t ts [] ys fun x => l_1 ++ x).snd ↔
      ∃ l₁ l₂_1, l₂_1 ≠ [] ∧ ys = l₁ ++ l₂_1 ∧ l ++ [] ++ t :: l₂ ++ ts = l_1 ++ l₁ ++ t :: l₂_1 ++ ts
⊢ l ++ [] ++ t :: l₂ ++ ts = l ++ (t :: y :: ys ++ ts) ∨
    ∃ l₁ l₂_1, l₂_1 ≠ [] ∧ ys = l₁ ++ l₂_1 ∧ l ++ [] ++ t :: l₂ ++ ts = l ++ [y] ++ l₁ ++ t :: l₂_1 ++ ts
[PROOFSTEP]
simp [ye]
[GOAL]
case cons.mpr.intro.cons.intro.intro.intro
α : Type u_1
β : Type u_2
t : α
ts l✝ : List α
y : α
ys l : List α
y' : α
l₁ l₂ : List α
l0 : l₂ ≠ []
ye : y :: ys = y' :: l₁ ++ l₂
ih :
  ∀ {l_1 : List α},
    l ++ y' :: l₁ ++ t :: l₂ ++ ts ∈ (permutationsAux2 t ts [] ys fun x => l_1 ++ x).snd ↔
      ∃ l₁_1 l₂_1, l₂_1 ≠ [] ∧ ys = l₁_1 ++ l₂_1 ∧ l ++ y' :: l₁ ++ t :: l₂ ++ ts = l_1 ++ l₁_1 ++ t :: l₂_1 ++ ts
⊢ l ++ y' :: l₁ ++ t :: l₂ ++ ts = l ++ (t :: y :: ys ++ ts) ∨
    ∃ l₁_1 l₂_1, l₂_1 ≠ [] ∧ ys = l₁_1 ++ l₂_1 ∧ l ++ y' :: l₁ ++ t :: l₂ ++ ts = l ++ [y] ++ l₁_1 ++ t :: l₂_1 ++ ts
[PROOFSTEP]
simp only [cons_append] at ye 
[GOAL]
case cons.mpr.intro.cons.intro.intro.intro
α : Type u_1
β : Type u_2
t : α
ts l✝ : List α
y : α
ys l : List α
y' : α
l₁ l₂ : List α
l0 : l₂ ≠ []
ye : y :: ys = y' :: (l₁ ++ l₂)
ih :
  ∀ {l_1 : List α},
    l ++ y' :: l₁ ++ t :: l₂ ++ ts ∈ (permutationsAux2 t ts [] ys fun x => l_1 ++ x).snd ↔
      ∃ l₁_1 l₂_1, l₂_1 ≠ [] ∧ ys = l₁_1 ++ l₂_1 ∧ l ++ y' :: l₁ ++ t :: l₂ ++ ts = l_1 ++ l₁_1 ++ t :: l₂_1 ++ ts
⊢ l ++ y' :: l₁ ++ t :: l₂ ++ ts = l ++ (t :: y :: ys ++ ts) ∨
    ∃ l₁_1 l₂_1, l₂_1 ≠ [] ∧ ys = l₁_1 ++ l₂_1 ∧ l ++ y' :: l₁ ++ t :: l₂ ++ ts = l ++ [y] ++ l₁_1 ++ t :: l₂_1 ++ ts
[PROOFSTEP]
rcases ye with ⟨rfl, rfl⟩
[GOAL]
case cons.mpr.intro.cons.intro.intro.intro.refl
α : Type u_1
β : Type u_2
t : α
ts l✝ : List α
y : α
l l₁ l₂ : List α
l0 : l₂ ≠ []
ih :
  ∀ {l_1 : List α},
    l ++ y :: l₁ ++ t :: l₂ ++ ts ∈ (permutationsAux2 t ts [] (l₁ ++ l₂) fun x => l_1 ++ x).snd ↔
      ∃ l₁_1 l₂_1, l₂_1 ≠ [] ∧ l₁ ++ l₂ = l₁_1 ++ l₂_1 ∧ l ++ y :: l₁ ++ t :: l₂ ++ ts = l_1 ++ l₁_1 ++ t :: l₂_1 ++ ts
⊢ l ++ y :: l₁ ++ t :: l₂ ++ ts = l ++ (t :: y :: (l₁ ++ l₂) ++ ts) ∨
    ∃ l₁_1 l₂_1,
      l₂_1 ≠ [] ∧ l₁ ++ l₂ = l₁_1 ++ l₂_1 ∧ l ++ y :: l₁ ++ t :: l₂ ++ ts = l ++ [y] ++ l₁_1 ++ t :: l₂_1 ++ ts
[PROOFSTEP]
exact Or.inr ⟨l₁, l₂, l0, by simp⟩
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts l✝ : List α
y : α
l l₁ l₂ : List α
l0 : l₂ ≠ []
ih :
  ∀ {l_1 : List α},
    l ++ y :: l₁ ++ t :: l₂ ++ ts ∈ (permutationsAux2 t ts [] (l₁ ++ l₂) fun x => l_1 ++ x).snd ↔
      ∃ l₁_1 l₂_1, l₂_1 ≠ [] ∧ l₁ ++ l₂ = l₁_1 ++ l₂_1 ∧ l ++ y :: l₁ ++ t :: l₂ ++ ts = l_1 ++ l₁_1 ++ t :: l₂_1 ++ ts
⊢ l₁ ++ l₂ = l₁ ++ l₂ ∧ l ++ y :: l₁ ++ t :: l₂ ++ ts = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts ys l : List α
⊢ l ∈ (permutationsAux2 t ts [] ys id).snd ↔ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l = l₁ ++ t :: l₂ ++ ts
[PROOFSTEP]
rw [show @id (List α) = ([] ++ ·) by funext _; rfl]
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts ys l : List α
⊢ id = fun x => [] ++ x
[PROOFSTEP]
funext _
[GOAL]
case h
α : Type u_1
β : Type u_2
t : α
ts ys l x✝ : List α
⊢ id x✝ = [] ++ x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts ys l : List α
⊢ l ∈ (permutationsAux2 t ts [] ys fun x => [] ++ x).snd ↔ ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l = l₁ ++ t :: l₂ ++ ts
[PROOFSTEP]
apply mem_permutationsAux2
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ length (permutationsAux2 t ts [] ys f).snd = length ys
[PROOFSTEP]
induction ys generalizing f
[GOAL]
case nil
α : Type u_1
β : Type u_2
t : α
ts : List α
f : List α → β
⊢ length (permutationsAux2 t ts [] [] f).snd = length []
[PROOFSTEP]
simp [*]
[GOAL]
case cons
α : Type u_1
β : Type u_2
t : α
ts : List α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (f : List α → β), length (permutationsAux2 t ts [] tail✝ f).snd = length tail✝
f : List α → β
⊢ length (permutationsAux2 t ts [] (head✝ :: tail✝) f).snd = length (head✝ :: tail✝)
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts : List α
r L : List (List α)
⊢ foldr (fun y r => (permutationsAux2 t ts r y id).snd) r L =
    (List.bind L fun y => (permutationsAux2 t ts [] y id).snd) ++ r
[PROOFSTEP]
induction' L with l L ih
[GOAL]
case nil
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List (List α)
⊢ foldr (fun y r => (permutationsAux2 t ts r y id).snd) r [] =
    (List.bind [] fun y => (permutationsAux2 t ts [] y id).snd) ++ r
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List (List α)
l : List α
L : List (List α)
ih :
  foldr (fun y r => (permutationsAux2 t ts r y id).snd) r L =
    (List.bind L fun y => (permutationsAux2 t ts [] y id).snd) ++ r
⊢ foldr (fun y r => (permutationsAux2 t ts r y id).snd) r (l :: L) =
    (List.bind (l :: L) fun y => (permutationsAux2 t ts [] y id).snd) ++ r
[PROOFSTEP]
simp [ih]
[GOAL]
case cons
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List (List α)
l : List α
L : List (List α)
ih :
  foldr (fun y r => (permutationsAux2 t ts r y id).snd) r L =
    (List.bind L fun y => (permutationsAux2 t ts [] y id).snd) ++ r
⊢ (permutationsAux2 t ts ((List.bind L fun y => (permutationsAux2 t ts [] y id).snd) ++ r) l id).snd =
    (permutationsAux2 t ts [] l id).snd ++ ((List.bind L fun y => (permutationsAux2 t ts [] y id).snd) ++ r)
[PROOFSTEP]
rw [← permutationsAux2_append]
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts : List α
r L : List (List α)
l' : List α
⊢ l' ∈ foldr (fun y r => (permutationsAux2 t ts r y id).snd) r L ↔
    l' ∈ r ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts
[PROOFSTEP]
have :
  (∃ a : List α, a ∈ L ∧ ∃ l₁ l₂ : List α, ¬l₂ = nil ∧ a = l₁ ++ l₂ ∧ l' = l₁ ++ t :: (l₂ ++ ts)) ↔
    ∃ l₁ l₂ : List α, ¬l₂ = nil ∧ l₁ ++ l₂ ∈ L ∧ l' = l₁ ++ t :: (l₂ ++ ts) :=
  ⟨fun ⟨_, aL, l₁, l₂, l0, e, h⟩ => ⟨l₁, l₂, l0, e ▸ aL, h⟩, fun ⟨l₁, l₂, l0, aL, h⟩ => ⟨_, aL, l₁, l₂, l0, rfl, h⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts : List α
r L : List (List α)
l' : List α
this :
  (∃ a, a ∈ L ∧ ∃ l₁ l₂, ¬l₂ = [] ∧ a = l₁ ++ l₂ ∧ l' = l₁ ++ t :: (l₂ ++ ts)) ↔
    ∃ l₁ l₂, ¬l₂ = [] ∧ l₁ ++ l₂ ∈ L ∧ l' = l₁ ++ t :: (l₂ ++ ts)
⊢ l' ∈ foldr (fun y r => (permutationsAux2 t ts r y id).snd) r L ↔
    l' ∈ r ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts
[PROOFSTEP]
rw [foldr_permutationsAux2]
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts : List α
r L : List (List α)
l' : List α
this :
  (∃ a, a ∈ L ∧ ∃ l₁ l₂, ¬l₂ = [] ∧ a = l₁ ++ l₂ ∧ l' = l₁ ++ t :: (l₂ ++ ts)) ↔
    ∃ l₁ l₂, ¬l₂ = [] ∧ l₁ ++ l₂ ∈ L ∧ l' = l₁ ++ t :: (l₂ ++ ts)
⊢ l' ∈ (List.bind L fun y => (permutationsAux2 t ts [] y id).snd) ++ r ↔
    l' ∈ r ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts
[PROOFSTEP]
simp only [mem_permutationsAux2', ← this, or_comm, and_left_comm, mem_append, mem_bind, append_assoc, cons_append,
  exists_prop]
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts : List α
r L : List (List α)
⊢ length (foldr (fun y r => (permutationsAux2 t ts r y id).snd) r L) = sum (map length L) + length r
[PROOFSTEP]
simp [foldr_permutationsAux2, (· ∘ ·), length_permutationsAux2]
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts : List α
r L : List (List α)
n : ℕ
H : ∀ (l : List α), l ∈ L → length l = n
⊢ length (foldr (fun y r => (permutationsAux2 t ts r y id).snd) r L) = n * length L + length r
[PROOFSTEP]
rw [length_foldr_permutationsAux2, (_ : List.sum (map length L) = n * length L)]
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts : List α
r L : List (List α)
n : ℕ
H : ∀ (l : List α), l ∈ L → length l = n
⊢ sum (map length L) = n * length L
[PROOFSTEP]
induction' L with l L ih
[GOAL]
case nil
α : Type u_1
β : Type u_2
t : α
ts : List α
r L : List (List α)
n : ℕ
H✝ : ∀ (l : List α), l ∈ L → length l = n
H : ∀ (l : List α), l ∈ [] → length l = n
⊢ sum (map length []) = n * length []
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
t : α
ts : List α
r L✝ : List (List α)
n : ℕ
H✝ : ∀ (l : List α), l ∈ L✝ → length l = n
l : List α
L : List (List α)
ih : (∀ (l : List α), l ∈ L → length l = n) → sum (map length L) = n * length L
H : ∀ (l_1 : List α), l_1 ∈ l :: L → length l_1 = n
⊢ sum (map length (l :: L)) = n * length (l :: L)
[PROOFSTEP]
have sum_map : sum (map length L) = n * length L := ih fun l m => H l (mem_cons_of_mem _ m)
[GOAL]
case cons
α : Type u_1
β : Type u_2
t : α
ts : List α
r L✝ : List (List α)
n : ℕ
H✝ : ∀ (l : List α), l ∈ L✝ → length l = n
l : List α
L : List (List α)
ih : (∀ (l : List α), l ∈ L → length l = n) → sum (map length L) = n * length L
H : ∀ (l_1 : List α), l_1 ∈ l :: L → length l_1 = n
sum_map : sum (map length L) = n * length L
⊢ sum (map length (l :: L)) = n * length (l :: L)
[PROOFSTEP]
have length_l : length l = n := H _ (mem_cons_self _ _)
[GOAL]
case cons
α : Type u_1
β : Type u_2
t : α
ts : List α
r L✝ : List (List α)
n : ℕ
H✝ : ∀ (l : List α), l ∈ L✝ → length l = n
l : List α
L : List (List α)
ih : (∀ (l : List α), l ∈ L → length l = n) → sum (map length L) = n * length L
H : ∀ (l_1 : List α), l_1 ∈ l :: L → length l_1 = n
sum_map : sum (map length L) = n * length L
length_l : length l = n
⊢ sum (map length (l :: L)) = n * length (l :: L)
[PROOFSTEP]
simp [sum_map, length_l, mul_add, add_comm, mul_succ]
[GOAL]
α : Type u_1
β : Type u_2
is : List α
⊢ permutationsAux [] is = []
[PROOFSTEP]
rw [permutationsAux, permutationsAux.rec]
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts is : List α
⊢ permutationsAux (t :: ts) is =
    foldr (fun y r => (permutationsAux2 t ts r y id).snd) (permutationsAux ts (t :: is)) (permutations is)
[PROOFSTEP]
rw [permutationsAux, permutationsAux.rec]
[GOAL]
α : Type u_1
β : Type u_2
t : α
ts is : List α
⊢ foldr (fun y r => (permutationsAux2 t ts r y id).snd)
      (permutationsAux.rec (fun x => [])
        (fun t ts is IH1 IH2 => foldr (fun y r => (permutationsAux2 t ts r y id).snd) IH1 (is :: IH2)) ts (t :: is))
      (is ::
        permutationsAux.rec (fun x => [])
          (fun t ts is IH1 IH2 => foldr (fun y r => (permutationsAux2 t ts r y id).snd) IH1 (is :: IH2)) is []) =
    foldr (fun y r => (permutationsAux2 t ts r y id).snd)
      (permutationsAux.rec (fun x => [])
        (fun t ts is IH1 IH2 => foldr (fun y r => (permutationsAux2 t ts r y id).snd) IH1 (is :: IH2)) ts (t :: is))
      (permutations is)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
⊢ permutations [] = [[]]
[PROOFSTEP]
rw [permutations, permutationsAux_nil]
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
⊢ ∀ (ts is : List α), map (map f) (permutationsAux ts is) = permutationsAux (map f ts) (map f is)
[PROOFSTEP]
refine' permutationsAux.rec (by simp) _
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
⊢ ∀ (is : List α), map (map f) (permutationsAux [] is) = permutationsAux (map f []) (map f is)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
⊢ ∀ (t : α) (ts is : List α),
    map (map f) (permutationsAux ts (t :: is)) = permutationsAux (map f ts) (map f (t :: is)) →
      map (map f) (permutationsAux is []) = permutationsAux (map f is) (map f []) →
        map (map f) (permutationsAux (t :: ts) is) = permutationsAux (map f (t :: ts)) (map f is)
[PROOFSTEP]
introv IH1 IH2
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
t : α
ts is : List α
IH1 : map (map f) (permutationsAux ts (t :: is)) = permutationsAux (map f ts) (map f (t :: is))
IH2 : map (map f) (permutationsAux is []) = permutationsAux (map f is) (map f [])
⊢ map (map f) (permutationsAux (t :: ts) is) = permutationsAux (map f (t :: ts)) (map f is)
[PROOFSTEP]
rw [map] at IH2 
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
t : α
ts is : List α
IH1 : map (map f) (permutationsAux ts (t :: is)) = permutationsAux (map f ts) (map f (t :: is))
IH2 : map (map f) (permutationsAux is []) = permutationsAux (map f is) []
⊢ map (map f) (permutationsAux (t :: ts) is) = permutationsAux (map f (t :: ts)) (map f is)
[PROOFSTEP]
simp only [foldr_permutationsAux2, map_append, map, map_map_permutationsAux2, permutations, bind_map, IH1, append_assoc,
  permutationsAux_cons, cons_bind, ← IH2, map_bind]
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
ts : List α
⊢ map (map f) (permutations ts) = permutations (map f ts)
[PROOFSTEP]
rw [permutations, permutations, map, map_permutationsAux, map]
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
ts : List α
⊢ map (map f) (permutations' ts) = permutations' (map f ts)
[PROOFSTEP]
induction' ts with t ts ih <;> [rfl; simp [← ih, map_bind, ← map_map_permutations'Aux, bind_map]]
[GOAL]
α : Type u_1
β : Type u_2
f : α → β
ts : List α
⊢ map (map f) (permutations' ts) = permutations' (map f ts)
[PROOFSTEP]
induction' ts with t ts ih
[GOAL]
case nil
α : Type u_1
β : Type u_2
f : α → β
⊢ map (map f) (permutations' []) = permutations' (map f [])
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
β : Type u_2
f : α → β
t : α
ts : List α
ih : map (map f) (permutations' ts) = permutations' (map f ts)
⊢ map (map f) (permutations' (t :: ts)) = permutations' (map f (t :: ts))
[PROOFSTEP]
simp [← ih, map_bind, ← map_map_permutations'Aux, bind_map]
[GOAL]
α : Type u_1
β : Type u_2
is is' ts : List α
⊢ permutationsAux (is ++ ts) is' =
    map (fun x => x ++ ts) (permutationsAux is is') ++ permutationsAux ts (reverse is ++ is')
[PROOFSTEP]
induction' is with t is ih generalizing is'
[GOAL]
case nil
α : Type u_1
β : Type u_2
is'✝ ts is' : List α
⊢ permutationsAux ([] ++ ts) is' =
    map (fun x => x ++ ts) (permutationsAux [] is') ++ permutationsAux ts (reverse [] ++ is')
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
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')
[PROOFSTEP]
simp only [foldr_permutationsAux2, ih, bind_map, cons_append, permutationsAux_cons, map_append, reverse_cons,
  append_assoc, singleton_append]
[GOAL]
case cons
α : Type u_1
β : Type u_2
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')))
[PROOFSTEP]
congr 2
[GOAL]
case cons.e_a.e_b
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
funext _
[GOAL]
case cons.e_a.e_b.h
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rw [map_permutationsAux2]
[GOAL]
case cons.e_a.e_b.h
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
simp (config := { singlePass := true }) only [← permutationsAux2_comp_append]
[GOAL]
case cons.e_a.e_b.h
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
simp only [id, append_assoc]
[GOAL]
α : Type u_1
β : Type u_2
is ts : List α
⊢ permutations (is ++ ts) = map (fun x => x ++ ts) (permutations is) ++ permutationsAux ts (reverse is)
[PROOFSTEP]
simp [permutations, permutationsAux_append]
