-- Mathlib/Data/List/Permutation.lean
theorem permutations_perm_permutations' (ts : List α) : ts.permutations ~ ts.permutations'

Proof state:
case intro.succ.refine_2
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
⊢ flatMap (fun y => (permutationsAux2 t [] [] y id).2) ts.permutations' ++ map (fun x => x ++ [t]) ts.permutations' ~
    ([t] ++ ts).permutations'

Tactic:
rw [map_eq_flatMap, singleton_append, permutations']

Result:
case intro.succ.refine_2
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
⊢ flatMap (fun y => (permutationsAux2 t [] [] y id).2) ts.permutations' ++
      flatMap (fun x => [x ++ [t]]) ts.permutations' ~
    flatMap (permutations'Aux t) ts.permutations'

Proof state:
case intro.succ.refine_2
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
⊢ (ts ++ [t]).permutations ~ (ts ++ [t]).permutations'

Tactic:
simp only [permutations_append, foldr_permutationsAux2, permutationsAux_nil,
  permutationsAux_cons, append_nil]

Result:
case intro.succ.refine_2
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
⊢ map (fun x => x ++ [t]) ts.permutations ++
      flatMap (fun y => (permutationsAux2 t [] [] y id).2) ts.reverse.permutations ~
    (ts ++ [t]).permutations'

Proof state:
case intro.succ.refine_2
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : (ts ++ [t]).length < n + 1
⊢ (ts ++ [t]).permutations ~ (ts ++ [t]).permutations'

Tactic:
rw [← concat_eq_append, length_concat, Nat.succ_lt_succ_iff] at h

Result:
case intro.succ.refine_2
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
⊢ (ts ++ [t]).permutations ~ (ts ++ [t]).permutations'

Proof state:
case intro.succ.refine_1
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts : List α
h : ts.length < n + 1
x✝ : [].length < n + 1
⊢ [].permutations ~ [].permutations'

Tactic:
simp [permutations]

Result:
no goals

Proof state:
case intro.succ.refine_2
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
⊢ flatMap (fun y => (permutationsAux2 t [] [] y id).2) ts.permutations' ++
      flatMap (fun x => [x ++ [t]]) ts.permutations' ~
    flatMap (permutations'Aux t) ts.permutations'

Tactic:
refine (flatMap_append_perm _ _ _).trans ?_

Result:
case intro.succ.refine_2
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
⊢ flatMap (fun x => (permutationsAux2 t [] [] x id).2 ++ [x ++ [t]]) ts.permutations' ~
    flatMap (permutations'Aux t) ts.permutations'

Proof state:
case intro.succ.refine_2
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
⊢ (ts ++ [t]).permutations ~ (ts ++ [t]).permutations'

Tactic:
have IH₂ := (IH ts.reverse (by rwa [length_reverse])).trans (reverse_perm _).permutations'

Result:
case intro.succ.refine_2
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
⊢ (ts ++ [t]).permutations ~ (ts ++ [t]).permutations'

Proof state:
case intro.succ.refine_2.e_b
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
⊢ (fun x => (permutationsAux2 t [] [] x id).2 ++ [x ++ [t]]) = permutations'Aux t

Tactic:
funext _

Result:
case intro.succ.refine_2.e_b.h
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝¹ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
x✝ : List α
⊢ (permutationsAux2 t [] [] x✝ id).2 ++ [x✝ ++ [t]] = permutations'Aux t x✝

Proof state:
case intro.succ
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts : List α
h : ts.length < n + 1
⊢ ts.permutations ~ ts.permutations'

Tactic:
refine List.reverseRecOn ts (fun _ => ?_) (fun ts t _ h => ?_) h

Result:
case intro.succ.refine_1
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts : List α
h : ts.length < n + 1
x✝ : [].length < n + 1
⊢ [].permutations ~ [].permutations'

case intro.succ.refine_2
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : (ts ++ [t]).length < n + 1
⊢ (ts ++ [t]).permutations ~ (ts ++ [t]).permutations'

Proof state:
case intro.zero
α : Type u_1
ts : List α
h : ts.length < 0
⊢ ts.permutations ~ ts.permutations'

Tactic:
cases h

Result:
no goals

Proof state:
case intro
α : Type u_1
ts : List α
n : ℕ
h : ts.length < n
⊢ ts.permutations ~ ts.permutations'

Tactic:
induction' n with n IH generalizing ts

Result:
case intro.zero
α : Type u_1
ts : List α
h : ts.length < 0
⊢ ts.permutations ~ ts.permutations'

case intro.succ
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts : List α
h : ts.length < n + 1
⊢ ts.permutations ~ ts.permutations'

Proof state:
case intro.succ.refine_2
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
⊢ flatMap (fun x => (permutationsAux2 t [] [] x id).2 ++ [x ++ [t]]) ts.permutations' =
    flatMap (permutations'Aux t) ts.permutations'

Tactic:
congr

Result:
case intro.succ.refine_2.e_b
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : ts.length < n
IH₂ : ts.reverse.permutations ~ ts.permutations'
⊢ (fun x => (permutationsAux2 t [] [] x id).2 ++ [x ++ [t]]) = permutations'Aux t