-- Mathlib/Data/List/Permutation.lean
theorem perm_permutations'Aux_comm (a b : α) (l : List α) :
    (permutations'Aux a l).flatMap (permutations'Aux b) ~
      (permutations'Aux b l).flatMap (permutations'Aux a)

Proof state:
case cons.p
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
this :
  ∀ (a b : α),
    flatMap (permutations'Aux b) (map (cons c) (permutations'Aux a l)) ~
      map (cons b ∘ cons c) (permutations'Aux a l) ++ map (cons c) (flatMap (permutations'Aux b) (permutations'Aux a l))
⊢ map (cons a ∘ cons c) (permutations'Aux b l) ++ flatMap (permutations'Aux b) (map (cons c) (permutations'Aux a l)) ~
    map (cons b ∘ cons c) (permutations'Aux a l) ++ flatMap (permutations'Aux a) (map (cons c) (permutations'Aux b l))

Tactic:
refine (((this _ _).append_left _).trans ?_).trans ((this _ _).append_left _).symm

Result:
case cons.p
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
this :
  ∀ (a b : α),
    flatMap (permutations'Aux b) (map (cons c) (permutations'Aux a l)) ~
      map (cons b ∘ cons c) (permutations'Aux a l) ++ map (cons c) (flatMap (permutations'Aux b) (permutations'Aux a l))
⊢ map (cons a ∘ cons c) (permutations'Aux b l) ++
      (map (cons b ∘ cons c) (permutations'Aux a l) ++
        map (cons c) (flatMap (permutations'Aux b) (permutations'Aux a l))) ~
    map (cons b ∘ cons c) (permutations'Aux a l) ++
      (map (cons a ∘ cons c) (permutations'Aux b l) ++
        map (cons c) (flatMap (permutations'Aux a) (permutations'Aux b l)))

Proof state:
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
a' b' : α
⊢ map (fun x => b' :: c :: x) (permutations'Aux a' l) ++
      map (cons c) (flatMap (permutations'Aux b') (permutations'Aux a' l)) ~
    map (cons b' ∘ cons c) (permutations'Aux a' l) ++
      map (cons c) (flatMap (permutations'Aux b') (permutations'Aux a' l))

Tactic:
exact Perm.refl _

Result:
no goals

Proof state:
case cons.p
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
this :
  ∀ (a b : α),
    flatMap (permutations'Aux b) (map (cons c) (permutations'Aux a l)) ~
      map (cons b ∘ cons c) (permutations'Aux a l) ++ map (cons c) (flatMap (permutations'Aux b) (permutations'Aux a l))
⊢ map (cons a ∘ cons c) (permutations'Aux b l) ++ map (cons b ∘ cons c) (permutations'Aux a l) ++
      map (cons c) (flatMap (permutations'Aux b) (permutations'Aux a l)) ~
    map (cons b ∘ cons c) (permutations'Aux a l) ++ map (cons a ∘ cons c) (permutations'Aux b l) ++
      map (cons c) (flatMap (permutations'Aux a) (permutations'Aux b l))

Tactic:
exact perm_append_comm.append (ih.map _)

Result:
no goals

Proof state:
case cons
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
⊢ (b :: a :: c :: l) ::
      (a :: b :: c :: l) ::
        (map (cons a ∘ cons c) (permutations'Aux b l) ++
          flatMap (permutations'Aux b) (map (cons c) (permutations'Aux a l))) ~
    (a :: b :: c :: l) ::
      (b :: a :: c :: l) ::
        (map (cons b ∘ cons c) (permutations'Aux a l) ++
          flatMap (permutations'Aux a) (map (cons c) (permutations'Aux b l)))

Tactic:
apply Perm.swap'

Result:
case cons.p
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
⊢ map (cons a ∘ cons c) (permutations'Aux b l) ++ flatMap (permutations'Aux b) (map (cons c) (permutations'Aux a l)) ~
    map (cons b ∘ cons c) (permutations'Aux a l) ++ flatMap (permutations'Aux a) (map (cons c) (permutations'Aux b l))

Proof state:
case cons.p
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
⊢ map (cons a ∘ cons c) (permutations'Aux b l) ++ flatMap (permutations'Aux b) (map (cons c) (permutations'Aux a l)) ~
    map (cons b ∘ cons c) (permutations'Aux a l) ++ flatMap (permutations'Aux a) (map (cons c) (permutations'Aux b l))

Tactic:
have :
  ∀ a b,
    (map (cons c) (permutations'Aux a l)).flatMap (permutations'Aux b) ~
      map (cons b ∘ cons c) (permutations'Aux a l) ++
        map (cons c) ((permutations'Aux a l).flatMap (permutations'Aux b)) := by
  intros a' b'
  simp only [flatMap_map, permutations'Aux]
  show (permutations'Aux _ l).flatMap (fun a => ([b' :: c :: a] ++
    map (cons c) (permutations'Aux _ a))) ~ _
  refine (flatMap_append_perm _ (fun x => [b' :: c :: x]) _).symm.trans ?_
  rw [← map_eq_flatMap, ← map_flatMap]
  exact Perm.refl _

Result:
case cons.p
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
this :
  ∀ (a b : α),
    flatMap (permutations'Aux b) (map (cons c) (permutations'Aux a l)) ~
      map (cons b ∘ cons c) (permutations'Aux a l) ++ map (cons c) (flatMap (permutations'Aux b) (permutations'Aux a l))
⊢ map (cons a ∘ cons c) (permutations'Aux b l) ++ flatMap (permutations'Aux b) (map (cons c) (permutations'Aux a l)) ~
    map (cons b ∘ cons c) (permutations'Aux a l) ++ flatMap (permutations'Aux a) (map (cons c) (permutations'Aux b l))

Proof state:
case nil
α : Type u_1
a b : α
⊢ flatMap (permutations'Aux b) (permutations'Aux a []) ~ flatMap (permutations'Aux a) (permutations'Aux b [])

Tactic:
exact Perm.swap [a, b] [b, a] []

Result:
no goals

Proof state:
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
a' b' : α
⊢ flatMap (fun a => [b' :: c :: a] ++ map (cons c) (permutations'Aux b' a)) (permutations'Aux a' l) ~
    map (cons b' ∘ cons c) (permutations'Aux a' l) ++
      map (cons c) (flatMap (permutations'Aux b') (permutations'Aux a' l))

Tactic:
refine (flatMap_append_perm _ (fun x => [b' :: c :: x]) _).symm.trans ?_

Result:
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
a' b' : α
⊢ flatMap (fun x => [b' :: c :: x]) (permutations'Aux a' l) ++
      flatMap (fun a => map (cons c) (permutations'Aux b' a)) (permutations'Aux a' l) ~
    map (cons b' ∘ cons c) (permutations'Aux a' l) ++
      map (cons c) (flatMap (permutations'Aux b') (permutations'Aux a' l))

Proof state:
case cons
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
⊢ flatMap (permutations'Aux b) (permutations'Aux a (c :: l)) ~
    flatMap (permutations'Aux a) (permutations'Aux b (c :: l))

Tactic:
simp only [permutations'Aux, flatMap_cons, map_cons, map_map, cons_append]

Result:
case cons
α : Type u_1
a b c : α
l : List α
ih : flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)
⊢ (b :: a :: c :: l) ::
      (a :: b :: c :: l) ::
        (map (cons a ∘ cons c) (permutations'Aux b l) ++
          flatMap (permutations'Aux b) (map (cons c) (permutations'Aux a l))) ~
    (a :: b :: c :: l) ::
      (b :: a :: c :: l) ::
        (map (cons b ∘ cons c) (permutations'Aux a l) ++
          flatMap (permutations'Aux a) (map (cons c) (permutations'Aux b l)))