-- Mathlib/Data/List/Permutation.lean
theorem permutationsAux_append (is is' ts : List α) :
    permutationsAux (is ++ ts) is' =
      (permutationsAux is is').map (· ++ ts) ++ permutationsAux ts (is.reverse ++ is')

Proof state:
case cons.e_a.e_b.h
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun x => x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' x✝ : List α
⊢ (permutationsAux2 t (is ++ ts) [] x✝ id).2 = (permutationsAux2 t is [] x✝ fun x => x ++ ts).2

Tactic:
simp (config := { singlePass := true }) only [← permutationsAux2_comp_append]

Result:
case cons.e_a.e_b.h
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun x => x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' x✝ : List α
⊢ (permutationsAux2 t [] [] x✝ fun x => id (x ++ (is ++ ts))).2 = (permutationsAux2 t [] [] x✝ fun x => x ++ is ++ ts).2

Proof state:
case cons.e_a.e_b.h
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun x => x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' x✝ : List α
⊢ (permutationsAux2 t [] [] x✝ fun x => id (x ++ (is ++ ts))).2 = (permutationsAux2 t [] [] x✝ fun x => x ++ is ++ ts).2

Tactic:
simp only [id, append_assoc]

Result:
no goals

Proof state:
case cons.e_a.e_b
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun x => x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' : List α
⊢ (fun y => (permutationsAux2 t (is ++ ts) [] y id).2) = fun a =>
    map (fun x => x ++ ts) (permutationsAux2 t is [] a id).2

Tactic:
funext _

Result:
case cons.e_a.e_b.h
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun x => x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' x✝ : List α
⊢ (permutationsAux2 t (is ++ ts) [] x✝ id).2 = map (fun x => x ++ ts) (permutationsAux2 t is [] x✝ id).2

Proof state:
case cons
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun x => x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' : List α
⊢ (t :: is ++ ts).permutationsAux is' =
    map (fun x => x ++ ts) ((t :: is).permutationsAux is') ++ ts.permutationsAux ((t :: is).reverse ++ is')

Tactic:
simp only [foldr_permutationsAux2, ih, map_flatMap, cons_append, permutationsAux_cons, map_append,
  reverse_cons, append_assoc, singleton_append]

Result:
case cons
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun x => x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' : List α
⊢ flatMap (fun y => (permutationsAux2 t (is ++ ts) [] y id).2) is'.permutations ++
      (map (fun x => x ++ ts) (is.permutationsAux (t :: is')) ++ ts.permutationsAux (is.reverse ++ t :: is')) =
    flatMap (fun a => map (fun x => x ++ ts) (permutationsAux2 t is [] a id).2) is'.permutations ++
      (map (fun x => x ++ ts) (is.permutationsAux (t :: is')) ++ ts.permutationsAux (is.reverse ++ t :: ([] ++ is')))

Proof state:
case nil
α : Type u_1
ts is' : List α
⊢ ([] ++ ts).permutationsAux is' =
    map (fun x => x ++ ts) ([].permutationsAux is') ++ ts.permutationsAux ([].reverse ++ is')

Tactic:
simp

Result:
no goals

Proof state:
case cons.e_a.e_b.h
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun x => x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' x✝ : List α
⊢ (permutationsAux2 t (is ++ ts) [] x✝ id).2 = map (fun x => x ++ ts) (permutationsAux2 t is [] x✝ id).2

Tactic:
rw [map_permutationsAux2]

Result:
case cons.e_a.e_b.h
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun x => x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' x✝ : List α
⊢ (permutationsAux2 t (is ++ ts) [] x✝ id).2 = (permutationsAux2 t is [] x✝ fun x => x ++ ts).2

Proof state:
case cons
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun x => x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' : List α
⊢ flatMap (fun y => (permutationsAux2 t (is ++ ts) [] y id).2) is'.permutations ++
      (map (fun x => x ++ ts) (is.permutationsAux (t :: is')) ++ ts.permutationsAux (is.reverse ++ t :: is')) =
    flatMap (fun a => map (fun x => x ++ ts) (permutationsAux2 t is [] a id).2) is'.permutations ++
      (map (fun x => x ++ ts) (is.permutationsAux (t :: is')) ++ ts.permutationsAux (is.reverse ++ t :: ([] ++ is')))

Tactic:
congr 2

Result:
case cons.e_a.e_b
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun x => x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' : List α
⊢ (fun y => (permutationsAux2 t (is ++ ts) [] y id).2) = fun a =>
    map (fun x => x ++ ts) (permutationsAux2 t is [] a id).2

Proof state:
α : Type u_1
is is' ts : List α
⊢ (is ++ ts).permutationsAux is' =
    map (fun x => x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')

Tactic:
induction' is with t is ih generalizing is'

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

case cons
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun x => x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' : List α
⊢ (t :: is ++ ts).permutationsAux is' =
    map (fun x => x ++ ts) ((t :: is).permutationsAux is') ++ ts.permutationsAux ((t :: is).reverse ++ is')