awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts is : List α
IH1 :
  ∀ (l : List α),
    l ~ t :: is ++ ts → (∃ (is' : List α), ∃ (x : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ (is' : List α), ∃ (x : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ l₂ : List α
p' : l₁ ++ t :: l₂ ~ t :: is
p : l₁ ++ l₂ ~ is
inl :
  ∀ (p' : l₁ ++ [t] ~ t :: is) (p : l₁ ++ [] ~ is),
    (∃ (is' : List α), ∃ (x : is' ~ is), l₁ ++ [t] ++ ts = is' ++ t :: ts) ∨
      l₁ ++ [t] ++ ts ∈ ts.permutationsAux (t :: is) ∨
        ∃ (l₁_1 : List α),
          ∃ (l₂ : List α), l₁_1 ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l₁ ++ [t] ++ ts = l₁_1 ++ t :: l₂ ++ ts
inl₁ :
  ∀ (a : α) (l₂' : List α) (p' : l₁ ++ t :: a :: l₂' ~ t :: is) (p : l₁ ++ a :: l₂' ~ is),
    (∃ (is' : List α), ∃ (x : is' ~ is), l₁ ++ t :: a :: l₂' ++ ts = is' ++ t :: ts) ∨
      l₁ ++ t :: a :: l₂' ++ ts ∈ ts.permutationsAux (t :: is) ∨
        ∃ (l₁_1 : List α),
          ∃ (l₂ : List α), l₁_1 ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l₁ ++ t :: a :: l₂' ++ ts = l₁_1 ++ t :: l₂ ++ ts
⊢ (∃ (is' : List α), ∃ (x : is' ~ is), l₁ ++ t :: l₂ ++ ts = is' ++ t :: ts) ∨
    l₁ ++ t :: l₂ ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ (l₁_1 : List α),
        ∃ (l₂_1 : List α), l₁_1 ++ l₂_1 ∈ is.permutations ∧ l₂_1 ≠ [] ∧ l₁ ++ t :: l₂ ++ ts = l₁_1 ++ t :: l₂_1 ++ ts

Tactic:
rcases l₂ with - | ⟨a, l₂'⟩
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts is : List α
IH1 :
  ∀ (l : List α),
    l ~ t :: is ++ ts → (∃ (is' : List α), ∃ (x : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ (is' : List α), ∃ (x : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ : List α
p' : l₁ ++ [t] ~ t :: is
p : l₁ ++ [] ~ is
⊢ ∃ (x : l₁ ~ is), l₁ ++ [t] ++ ts = l₁ ++ t :: ts

Tactic:
simpa using p
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts is : List α
IH1 :
  ∀ (l : List α),
    l ~ t :: is ++ ts → (∃ (is' : List α), ∃ (x : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ (is' : List α), ∃ (x : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ : List α
p' : l₁ ++ [t] ~ t :: is
p : l₁ ++ [] ~ is
⊢ (∃ (is' : List α), ∃ (x : is' ~ is), l₁ ++ [t] ++ ts = is' ++ t :: ts) ∨
    l₁ ++ [t] ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ (l₁_1 : List α),
        ∃ (l₂ : List α), l₁_1 ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l₁ ++ [t] ++ ts = l₁_1 ++ t :: l₂ ++ ts

Tactic:
exact Or.inl ⟨l₁, by simpa using p⟩

Premises used: Or.inl
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts is : List α
IH1 :
  ∀ (l : List α),
    l ~ t :: is ++ ts → (∃ (is' : List α), ∃ (x : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ (is' : List α), ∃ (x : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ : List α
a : α
l₂' : List α
p' : l₁ ++ t :: a :: l₂' ~ t :: is
p : l₁ ++ a :: l₂' ~ is
⊢ a :: l₂' ≠ [] ∧ l₁ ++ t :: a :: l₂' ++ ts = l₁ ++ t :: a :: l₂' ++ ts

Tactic:
simp
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts is : List α
IH1 :
  ∀ (l : List α),
    l ~ t :: is ++ ts → (∃ (is' : List α), ∃ (x : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ (is' : List α), ∃ (x : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ : List α
a : α
l₂' : List α
p' : l₁ ++ t :: a :: l₂' ~ t :: is
p : l₁ ++ a :: l₂' ~ is
⊢ (∃ (is' : List α), ∃ (x : is' ~ is), l₁ ++ t :: a :: l₂' ++ ts = is' ++ t :: ts) ∨
    l₁ ++ t :: a :: l₂' ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ (l₁_1 : List α),
        ∃ (l₂ : List α), l₁_1 ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l₁ ++ t :: a :: l₂' ++ ts = l₁_1 ++ t :: l₂ ++ ts

Tactic:
exact Or.inr (Or.inr ⟨l₁, a :: l₂', mem_permutations_of_perm_lemma (IH2 _) p, by simp⟩)

Premises used: Or.inr
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts is : List α
IH1 :
  ∀ (l : List α),
    l ~ t :: is ++ ts → (∃ (is' : List α), ∃ (x : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ (is' : List α), ∃ (x : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []
l : List α
p : l ~ is ++ t :: ts
m : l ∈ ts.permutationsAux (t :: is)
⊢ (∃ (is' : List α), ∃ (x : is' ~ is), l = is' ++ t :: ts) ∨
    l ∈ ts.permutationsAux (t :: is) ∨
      ∃ (l₁ : List α), ∃ (l₂ : List α), l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts

Tactic:
Or.inr (Or.inl m)

Premises used: Or.inl, Or.inr
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts is : List α
IH1 :
  ∀ (l : List α),
    l ~ t :: is ++ ts → (∃ (is' : List α), ∃ (x : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ (is' : List α), ∃ (x : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []
l : List α
p : l ~ is ++ t :: ts
m : l ∈ ts.permutationsAux (t :: is)
⊢ (∃ (is' : List α), ∃ (x : is' ~ is), l = is' ++ t :: ts) ∨
    l ∈ ts.permutationsAux (t :: is) ∨
      ∃ (l₁ : List α), ∃ (l₂ : List α), l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts

Tactic:
exact Or.inr (Or.inl m)

Premises used: Or.inl, Or.inr
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s t : List α
⊢ s ∈ t.permutations ↔ s ~ t

Tactic:
⟨perm_of_mem_permutations, mem_permutations_of_perm_lemma mem_permutationsAux_of_perm⟩

Premises used: List.mem_permutationsAux_of_perm, List.mem_permutations_of_perm_lemma, Iff.intro, List.perm_of_mem_permutations
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
a b : α
⊢ flatMap (permutations'Aux b) (permutations'Aux a []) ~ flatMap (permutations'Aux a) (permutations'Aux b [])

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

Premises used: List.Perm.swap, List.cons, List.append, List.flatten, List.nil
-- Module: Mathlib.Data.List.Permutation
Goal:
α : 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] []

Premises used: List.Perm.swap, List.cons, List.nil
-- Module: Mathlib.Data.List.Permutation
Goal:
α : 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:
?_
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
a b : α
l : List α
cons :
  ∀ (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))
⊢ flatMap (permutations'Aux b) (permutations'Aux a l) ~ flatMap (permutations'Aux a) (permutations'Aux b l)

Tactic:
induction l with
  | nil => exact Perm.swap [a, b] [b, a] []
  | cons c l ih => ?_

Premises used: List.Perm.swap, List.cons, List.nil
-- Module: Mathlib.Data.List.Permutation
Goal:
α : 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)
cons :
  (b :: a :: c :: l) ::
      (a :: b :: c :: l) ::
        (map (List.cons a ∘ List.cons c) (permutations'Aux b l) ++
          flatMap (permutations'Aux b) (map (List.cons c) (permutations'Aux a l))) ~
    (a :: b :: c :: l) ::
      (b :: a :: c :: l) ::
        (map (List.cons b ∘ List.cons c) (permutations'Aux a l) ++
          flatMap (permutations'Aux a) (map (List.cons c) (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]

Premises used: List.map_cons, List.map_map, List.flatMap_cons, List.permutations'Aux, List.cons_append
-- Module: Mathlib.Data.List.Permutation
Goal:
α : 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)
cons :
  map (List.cons a ∘ List.cons c) (permutations'Aux b l) ++
      flatMap (permutations'Aux b) (map (List.cons c) (permutations'Aux a l)) ~
    map (List.cons b ∘ List.cons c) (permutations'Aux a l) ++
      flatMap (permutations'Aux a) (map (List.cons c) (permutations'Aux b l))
⊢ (b :: a :: c :: l) ::
      (a :: b :: c :: l) ::
        (map (List.cons a ∘ List.cons c) (permutations'Aux b l) ++
          flatMap (permutations'Aux b) (map (List.cons c) (permutations'Aux a l))) ~
    (a :: b :: c :: l) ::
      (b :: a :: c :: l) ::
        (map (List.cons b ∘ List.cons c) (permutations'Aux a l) ++
          flatMap (permutations'Aux a) (map (List.cons c) (permutations'Aux b l)))

Tactic:
apply Perm.swap'

Premises used: List.Perm.swap'
-- Module: Mathlib.Data.List.Permutation
Goal:
α : 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' : α
simp :
  flatMap (fun (a : List α) ↦ (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))
⊢ 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))

Tactic:
simp only [flatMap_map, permutations'Aux]

Premises used: List.flatMap_map, List.permutations'Aux
-- Module: Mathlib.Data.List.Permutation
Goal:
α : 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 : List α) ↦ [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:
(flatMap_append_perm _ (fun x => [b' :: c :: x]) _).symm.trans ?_

Premises used: List.flatMap_append_perm, List.Perm.trans, List.cons, List.Perm.symm, List.nil
-- Module: Mathlib.Data.List.Permutation
Goal:
α : 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' : α
refine :
  HAppend.hAppend (α := List (List α)) (flatMap (fun (x : List α) ↦ [b' :: c :: x]) (permutations'Aux a' l))
      (flatMap (fun (a : List α) ↦ 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))
⊢ flatMap (fun (a : List α) ↦ [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 ?_

Premises used: List.flatMap_append_perm, List.Perm.trans, List.cons, List.Perm.symm, List.nil
-- Module: Mathlib.Data.List.Permutation
Goal:
α : 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' : α
rw :
  map (fun (x : List α) ↦ 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))
⊢ HAppend.hAppend (α := List (List α)) (flatMap (fun (x : List α) ↦ [b' :: c :: x]) (permutations'Aux a' l))
      (flatMap (fun (a : List α) ↦ 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:
rw [← map_eq_flatMap, ← map_flatMap]

Premises used: List.map_eq_flatMap, List.map_flatMap
-- Module: Mathlib.Data.List.Permutation
Goal:
α : 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 : List α) ↦ 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:
Perm.refl _

Premises used: List.Perm.refl
-- Module: Mathlib.Data.List.Permutation
Goal:
α : 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 : List α) ↦ 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 _

Premises used: List.Perm.refl
-- Module: Mathlib.Data.List.Permutation
Goal:
α : 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 (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))

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
    intro a' b'
    simp only [flatMap_map, permutations'Aux]
    change (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 _
-- Module: Mathlib.Data.List.Permutation
Goal:
α : 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:
(((this _ _).append_left _).trans ?_).trans ((this _ _).append_left _).symm

Premises used: List.Perm.append_left, List.Perm.trans, List.Perm.symm
-- Module: Mathlib.Data.List.Permutation
Goal:
α : 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 (List.cons c) (permutations'Aux a l)) ~
      map (List.cons b ∘ List.cons c) (permutations'Aux a l) ++
        map (List.cons c) (flatMap (permutations'Aux b) (permutations'Aux a l))
cons :
  map (List.cons a ∘ List.cons c) (permutations'Aux b l) ++
      (map (List.cons b ∘ List.cons c) (permutations'Aux a l) ++
        map (List.cons c) (flatMap (permutations'Aux b) (permutations'Aux a l))) ~
    map (List.cons b ∘ List.cons c) (permutations'Aux a l) ++
      (map (List.cons a ∘ List.cons c) (permutations'Aux b l) ++
        map (List.cons c) (flatMap (permutations'Aux a) (permutations'Aux b l)))
⊢ map (List.cons a ∘ List.cons c) (permutations'Aux b l) ++
      flatMap (permutations'Aux b) (map (List.cons c) (permutations'Aux a l)) ~
    map (List.cons b ∘ List.cons c) (permutations'Aux a l) ++
      flatMap (permutations'Aux a) (map (List.cons c) (permutations'Aux b l))

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

Premises used: List.Perm.append_left, List.Perm.trans, List.Perm.symm
-- Module: Mathlib.Data.List.Permutation
Goal:
α : 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 (List.cons c) (permutations'Aux a l)) ~
      map (List.cons b ∘ List.cons c) (permutations'Aux a l) ++
        map (List.cons c) (flatMap (permutations'Aux b) (permutations'Aux a l))
cons :
  map (List.cons a ∘ List.cons c) (permutations'Aux b l) ++ map (List.cons b ∘ List.cons c) (permutations'Aux a l) ++
      map (List.cons c) (flatMap (permutations'Aux b) (permutations'Aux a l)) ~
    map (List.cons b ∘ List.cons c) (permutations'Aux a l) ++ map (List.cons a ∘ List.cons c) (permutations'Aux b l) ++
      map (List.cons c) (flatMap (permutations'Aux a) (permutations'Aux b l))
⊢ map (List.cons a ∘ List.cons c) (permutations'Aux b l) ++
      (map (List.cons b ∘ List.cons c) (permutations'Aux a l) ++
        map (List.cons c) (flatMap (permutations'Aux b) (permutations'Aux a l))) ~
    map (List.cons b ∘ List.cons c) (permutations'Aux a l) ++
      (map (List.cons a ∘ List.cons c) (permutations'Aux b l) ++
        map (List.cons c) (flatMap (permutations'Aux a) (permutations'Aux b l)))

Tactic:
rw [← append_assoc, ← append_assoc]

Premises used: List.append_assoc
-- Module: Mathlib.Data.List.Permutation
Goal:
α : 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:
perm_append_comm.append (ih.map _)

Premises used: List.perm_append_comm, List.Perm.append, List.Perm.map
-- Module: Mathlib.Data.List.Permutation
Goal:
α : 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 _)

Premises used: List.perm_append_comm, List.Perm.append, List.Perm.map
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s t : List α
⊢ Perm.{u_1} (α := List α) (List.permutations' []) (List.permutations' [])

Tactic:
simp
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s t : List α
x : α
l₁ l₂ : List α
h : l₁ ~ l₂
IH : l₁.permutations' ~ l₂.permutations'
⊢ (x :: l₁).permutations' ~ (x :: l₂).permutations'

Tactic:
IH.flatMap_right _

Premises used: List.Perm.flatMap_right, List.permutations'
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s t : List α
x : α
l₁ l₂ : List α
h : l₁ ~ l₂
IH : l₁.permutations' ~ l₂.permutations'
⊢ (x :: l₁).permutations' ~ (x :: l₂).permutations'

Tactic:
exact IH.flatMap_right _

Premises used: List.Perm.flatMap_right
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s t : List α
x y : α
l : List α
swap :
  Perm (α := List α)
    (flatMap (fun (x_1 : List α) ↦ flatMap (permutations'Aux y) (permutations'Aux x x_1)) l.permutations')
    (flatMap (fun (x_1 : List α) ↦ flatMap (permutations'Aux x) (permutations'Aux y x_1)) l.permutations')
⊢ 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]

Premises used: List.flatMap_assoc
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s t : List α
x y : α
l : List α
swap :
  ∀ (a : List α),
    a ∈ l.permutations' →
      flatMap (permutations'Aux y) (permutations'Aux x a) ~ flatMap (permutations'Aux x) (permutations'Aux y a)
⊢ Perm (α := List α)
    (flatMap (fun (x_1 : List α) ↦ flatMap (permutations'Aux y) (permutations'Aux x x_1)) l.permutations')
    (flatMap (fun (x_1 : List α) ↦ flatMap (permutations'Aux x) (permutations'Aux y x_1)) l.permutations')

Tactic:
apply Perm.flatMap_left

Premises used: List.Perm.flatMap_left
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s t : List α
x y : α
l l' : List α
swap :
  l' ∈ l.permutations' →
    flatMap (permutations'Aux y) (permutations'Aux x l') ~ flatMap (permutations'Aux x) (permutations'Aux y l')
⊢ l' ∈ l.permutations' →
    flatMap (permutations'Aux y) (permutations'Aux x l') ~ flatMap (permutations'Aux x) (permutations'Aux y l')

Tactic:
_
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s t : List α
x y : α
l l' : List α
h : 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

Premises used: List.perm_permutations'Aux_comm
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s t l₁ l₂ l₃ : List α
h : l₁ ~ l₂
h_1 : l₂ ~ l₃
IH₁ : l₁.permutations' ~ l₂.permutations'
IH₂ : l₂.permutations' ~ l₃.permutations'
⊢ l₁.permutations' ~ l₃.permutations'

Tactic:
IH₁.trans IH₂

Premises used: List.Perm.trans
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s t l₁ l₂ l₃ : List α
h : l₁ ~ l₂
h_1 : l₂ ~ l₃
IH₁ : l₁.permutations' ~ l₂.permutations'
IH₂ : l₂.permutations' ~ l₃.permutations'
⊢ l₁.permutations' ~ l₃.permutations'

Tactic:
exact IH₁.trans IH₂

Premises used: List.Perm.trans
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s t : List α
p : s ~ t
nil : Perm.{u_1} (α := List α) (List.permutations' []) (List.permutations' [])
cons :
  ∀ (x : α) {l₁ l₂ : List α},
    l₁ ~ l₂ → ∀ (IH : l₁.permutations' ~ l₂.permutations'), (x :: l₁).permutations' ~ (x :: l₂).permutations'
swap : ∀ (x y : α) (l : List α), (y :: x :: l).permutations' ~ (x :: y :: l).permutations'
trans :
  ∀ {l₁ l₂ l₃ : List α},
    l₁ ~ l₂ →
      l₂ ~ l₃ →
        ∀ (IH₁ : l₁.permutations' ~ l₂.permutations') (IH₂ : l₂.permutations' ~ l₃.permutations'),
          l₁.permutations' ~ l₃.permutations'
⊢ 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₂

Premises used: List.Perm.cons, List.Perm.swap, List.Perm.trans, List.Perm.flatMap_left, List.flatMap_assoc, List.Perm.nil, List.perm_permutations'Aux_comm
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
ts : List α
⊢ ∃ (n : ℕ), ts.length < n

Tactic:
⟨_, Nat.lt_succ_self _⟩

Premises used: Nat.lt_succ_self, Exists.intro
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
ts : List α
obtain : ∀ (n : ℕ) (h : ts.length < n), ts.permutations ~ ts.permutations'
⊢ ts.permutations ~ ts.permutations'

Tactic:
obtain ⟨n, h⟩ : ∃ n, length ts < n := ⟨_, Nat.lt_succ_self _⟩

Premises used: List.length
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
ts : List α
h : ts.length < 0
⊢ ts.permutations ~ ts.permutations'

Tactic:
cases h