-- Mathlib/Data/List/Permutation.lean
theorem Perm.permutations' {s t : List α} (p : s ~ t) : permutations' s ~ permutations' t

Proof state:
case swap.h
α : Type u_1
s t : List α
x✝ y✝ : α
l✝ : List α
⊢ ∀ a ∈ l✝.permutations',
    flatMap (permutations'Aux y✝) (permutations'Aux x✝ a) ~ flatMap (permutations'Aux x✝) (permutations'Aux y✝ a)

Tactic:
intro l' _

Result:
case swap.h
α : Type u_1
s t : List α
x✝ y✝ : α
l✝ l' : List α
a✝ : l' ∈ l✝.permutations'
⊢ flatMap (permutations'Aux y✝) (permutations'Aux x✝ l') ~ flatMap (permutations'Aux x✝) (permutations'Aux y✝ l')

Proof state:
case swap.h
α : Type u_1
s t : List α
x✝ y✝ : α
l✝ l' : List α
a✝ : l' ∈ l✝.permutations'
⊢ flatMap (permutations'Aux y✝) (permutations'Aux x✝ l') ~ flatMap (permutations'Aux x✝) (permutations'Aux y✝ l')

Tactic:
apply perm_permutations'Aux_comm

Result:
no goals

Proof state:
case swap
α : Type u_1
s t : List α
x✝ y✝ : α
l✝ : List α
⊢ flatMap (fun x => flatMap (permutations'Aux y✝) (permutations'Aux x✝ x)) l✝.permutations' ~
    flatMap (fun x => flatMap (permutations'Aux x✝) (permutations'Aux y✝ x)) l✝.permutations'

Tactic:
apply Perm.flatMap_left

Result:
case swap.h
α : Type u_1
s t : List α
x✝ y✝ : α
l✝ : List α
⊢ ∀ a ∈ l✝.permutations',
    flatMap (permutations'Aux y✝) (permutations'Aux x✝ a) ~ flatMap (permutations'Aux x✝) (permutations'Aux y✝ a)

Proof state:
case trans
α : Type u_1
s t l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
IH₁ : l₁✝.permutations' ~ l₂✝.permutations'
IH₂ : l₂✝.permutations' ~ l₃✝.permutations'
⊢ l₁✝.permutations' ~ l₃✝.permutations'

Tactic:
exact IH₁.trans IH₂

Result:
no goals

Proof state:
case nil
α : Type u_1
s t : List α
⊢ [].permutations' ~ [].permutations'

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
s t : List α
p : s ~ t
⊢ s.permutations' ~ t.permutations'

Tactic:
induction p with
| nil => simp
| cons _ _ IH => exact IH.flatMap_right _
| swap =>
  dsimp
  rw [flatMap_assoc, flatMap_assoc]
  apply Perm.flatMap_left
  intro l' _
  apply perm_permutations'Aux_comm
| trans _ _ IH₁ IH₂ => exact IH₁.trans IH₂

Result:
no goals

Proof state:
case cons
α : Type u_1
s t : List α
x✝ : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
IH : l₁✝.permutations' ~ l₂✝.permutations'
⊢ (x✝ :: l₁✝).permutations' ~ (x✝ :: l₂✝).permutations'

Tactic:
exact IH.flatMap_right _

Result:
no goals

Proof state:
case swap
α : Type u_1
s t : List α
x✝ y✝ : α
l✝ : List α
⊢ (y✝ :: x✝ :: l✝).permutations' ~ (x✝ :: y✝ :: l✝).permutations'

Tactic:
dsimp

Result:
case swap
α : Type u_1
s t : List α
x✝ y✝ : α
l✝ : List α
⊢ flatMap (permutations'Aux y✝) (flatMap (permutations'Aux x✝) l✝.permutations') ~
    flatMap (permutations'Aux x✝) (flatMap (permutations'Aux y✝) l✝.permutations')

Proof state:
case swap
α : Type u_1
s t : List α
x✝ y✝ : α
l✝ : List α
⊢ flatMap (permutations'Aux y✝) (flatMap (permutations'Aux x✝) l✝.permutations') ~
    flatMap (permutations'Aux x✝) (flatMap (permutations'Aux y✝) l✝.permutations')

Tactic:
rw [flatMap_assoc, flatMap_assoc]

Result:
case swap
α : Type u_1
s t : List α
x✝ y✝ : α
l✝ : List α
⊢ flatMap (fun x => flatMap (permutations'Aux y✝) (permutations'Aux x✝ x)) l✝.permutations' ~
    flatMap (fun x => flatMap (permutations'Aux x✝) (permutations'Aux y✝ x)) l✝.permutations'