awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
β : Type u_2
f : α → β
ts : List α
rw : map (map f) (ts :: ts.permutationsAux []) = (map f ts).permutations
rw₁ : map (map f) (ts :: ts.permutationsAux []) = map f ts :: (map f ts).permutationsAux []
rw₂ : map f ts :: map (map f) (ts.permutationsAux []) = map f ts :: (map f ts).permutationsAux []
rw₃ : map f ts :: (map f ts).permutationsAux (map f []) = map f ts :: (map f ts).permutationsAux []
rw₄ rw₅ : map f ts :: (map f ts).permutationsAux [] = map f ts :: (map f ts).permutationsAux []
⊢ map (map f) ts.permutations = (map f ts).permutations

Tactic:
rw [permutations, permutations, map, map_permutationsAux, map]

Premises used: List.map, List.permutations, List.map_permutationsAux
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ map (map f) (permutations' []) = (map f []).permutations'

Tactic:
rfl
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
β : Type u_2
f : α → β
t : α
ts : List α
ih : map (map f) ts.permutations' = (map f ts).permutations'
⊢ map (map f) (t :: ts).permutations' = (map f (t :: ts)).permutations'

Tactic:
simp [← ih, map_flatMap, ← map_map_permutations'Aux, flatMap_map]

Premises used: List.flatMap_map, List.map_map_permutations'Aux, List.map_flatMap
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
β : Type u_2
f : α → β
ts : List α
nil : map (map f) (permutations' []) = (map f []).permutations'
cons :
  ∀ (t : α) (ts : List α) (ih : map (map f) ts.permutations' = (map f ts).permutations'),
    map (map f) (t :: ts).permutations' = (map f (t :: ts)).permutations'
⊢ map (map f) ts.permutations' = (map f ts).permutations'

Tactic:
induction ts with
  | nil => rfl
  | cons t ts ih => simp [← ih, map_flatMap, ← map_map_permutations'Aux, flatMap_map]

Premises used: List.cons, List.flatMap_map, List.map_map_permutations'Aux, List.map_flatMap, List.nil
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
ts is' : List α
⊢ ([] ++ ts).permutationsAux is' =
    map (fun (x : List α) ↦ x ++ ts) (permutationsAux [] is') ++ ts.permutationsAux (reverse [] ++ is')

Tactic:
simp
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun (x : List α) ↦ x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' : List α
cons :
  flatMap (fun (y : List α) ↦ (permutationsAux2 t (is ++ ts) [] y id).snd) is'.permutations ++
      (map (fun (x : List α) ↦ x ++ ts) (is.permutationsAux (t :: is')) ++
        ts.permutationsAux (is.reverse ++ t :: is')) =
    flatMap (fun (a : List α) ↦ map (fun (x : List α) ↦ x ++ ts) (permutationsAux2 t is [] a id).snd)
        is'.permutations ++
      (map (fun (x : List α) ↦ x ++ ts) (is.permutationsAux (t :: is')) ++
        ts.permutationsAux (is.reverse ++ t :: ([] ++ is')))
⊢ (t :: is ++ ts).permutationsAux is' =
    map (fun (x : List α) ↦ 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]

Premises used: List.append_assoc, List.permutationsAux_cons, List.reverse_cons, List.foldr_permutationsAux2, List.map_flatMap, List.map_append, List.cons_append
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun (x : List α) ↦ x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' : List α
cons :
  Eq.{u_1 + 1} (α := List α → List (List α)) (fun (y : List α) ↦ (permutationsAux2 t (is ++ ts) [] y id).snd)
    fun (a : List α) ↦ map (fun (x : List α) ↦ x ++ ts) (permutationsAux2 t is [] a id).snd
⊢ flatMap (fun (y : List α) ↦ (permutationsAux2 t (is ++ ts) [] y id).snd) is'.permutations ++
      (map (fun (x : List α) ↦ x ++ ts) (is.permutationsAux (t :: is')) ++
        ts.permutationsAux (is.reverse ++ t :: is')) =
    flatMap (fun (a : List α) ↦ map (fun (x : List α) ↦ x ++ ts) (permutationsAux2 t is [] a id).snd)
        is'.permutations ++
      (map (fun (x : List α) ↦ x ++ ts) (is.permutationsAux (t :: is')) ++
        ts.permutationsAux (is.reverse ++ t :: ([] ++ is')))

Tactic:
congr 2
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun (x : List α) ↦ x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' : List α
cons :
  ∀ (x : List α),
    (permutationsAux2 t (is ++ ts) [] x id).snd = map (fun (x : List α) ↦ x ++ ts) (permutationsAux2 t is [] x id).snd
⊢ Eq.{u_1 + 1} (α := List α → List (List α)) (fun (y : List α) ↦ (permutationsAux2 t (is ++ ts) [] y id).snd)
    fun (a : List α) ↦ map (fun (x : List α) ↦ x ++ ts) (permutationsAux2 t is [] a id).snd

Tactic:
funext _
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun (x : List α) ↦ x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' x : List α
cons : (permutationsAux2 t (is ++ ts) [] x id).snd = Prod.snd (permutationsAux2 t is [] x fun (x : List α) ↦ x ++ ts)
⊢ (permutationsAux2 t (is ++ ts) [] x id).snd = map (fun (x : List α) ↦ x ++ ts) (permutationsAux2 t is [] x id).snd

Tactic:
rw [map_permutationsAux2]

Premises used: List.map_permutationsAux2
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun (x : List α) ↦ x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' x : List α
cons :
  Eq (α := List (List α)) (Prod.snd (permutationsAux2 t [] [] x fun (x : List α) ↦ id (x ++ (is ++ ts))))
    (Prod.snd (permutationsAux2 t [] [] x fun (x : List α) ↦ x ++ is ++ ts))
⊢ (permutationsAux2 t (is ++ ts) [] x id).snd = Prod.snd (permutationsAux2 t is [] x fun (x : List α) ↦ x ++ ts)

Tactic:
simp +singlePass only [← permutationsAux2_comp_append]

Premises used: List.permutationsAux2_comp_append
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
ts : List α
t : α
is : List α
ih :
  ∀ (is' : List α),
    (is ++ ts).permutationsAux is' =
      map (fun (x : List α) ↦ x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')
is' x : List α
⊢ Eq (α := List (List α)) (Prod.snd (permutationsAux2 t [] [] x fun (x : List α) ↦ id (x ++ (is ++ ts))))
    (Prod.snd (permutationsAux2 t [] [] x fun (x : List α) ↦ x ++ is ++ ts))

Tactic:
simp only [id, append_assoc]

Premises used: List.append_assoc, id
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
is is' ts : List α
nil :
  ∀ (is' : List α),
    ([] ++ ts).permutationsAux is' =
      map (fun (x : List α) ↦ x ++ ts) (permutationsAux [] is') ++ ts.permutationsAux (reverse [] ++ is')
cons :
  ∀ (t : α) (is : List α)
    (ih :
      ∀ (is' : List α),
        (is ++ ts).permutationsAux is' =
          map (fun (x : List α) ↦ x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is'))
    (is' : List α),
    (t :: is ++ ts).permutationsAux is' =
      map (fun (x : List α) ↦ x ++ ts) ((t :: is).permutationsAux is') ++ ts.permutationsAux ((t :: is).reverse ++ is')
⊢ (is ++ ts).permutationsAux is' =
    map (fun (x : List α) ↦ x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')

Tactic:
induction is generalizing is' with | nil => simp | cons t is ih =>
  simp only [foldr_permutationsAux2, ih, map_flatMap, cons_append, permutationsAux_cons, map_append,
    reverse_cons, append_assoc]
  congr 2
  funext _
  rw [map_permutationsAux2]
  simp +singlePass only [← permutationsAux2_comp_append]
  simp only [id, append_assoc]

Premises used: List.map_permutationsAux2, List.permutationsAux2_comp_append, List.append_assoc, List.permutationsAux_cons, id, List.cons, List.reverse_cons, List.foldr_permutationsAux2, List.map_flatMap, List.map_append, List.cons_append, List.nil
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
is ts : List α
⊢ (is ++ ts).permutations = map (fun (x : List α) ↦ x ++ ts) is.permutations ++ ts.permutationsAux is.reverse

Tactic:
simp [permutations, permutationsAux_append]

Premises used: List.permutations, List.permutationsAux_append
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
⊢ ∀ (is l : List α), l ∈ permutationsAux [] is → l ~ [] ++ is

Tactic:
simp
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
refine :
  ∀ (t : α) (ts is : List α),
    (∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is) →
      (∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []) →
        ∀ (l : List α), l ∈ (t :: ts).permutationsAux is → l ~ t :: ts ++ is
⊢ ∀ (ts is l : List α), l ∈ ts.permutationsAux is → l ~ ts ++ is

Tactic:
refine permutationsAux.rec (by simp) ?_
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l : List α
m : l ∈ (t :: ts).permutationsAux is
⊢ l ∈ ts.permutationsAux (t :: is) ∨
    ∃ (l₁ : List α), ∃ (l₂ : List α), l₁ ++ l₂ ∈ is :: is.permutationsAux [] ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts

Tactic:
rw [permutationsAux_cons, permutations, mem_foldr_permutationsAux2] at m

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

Tactic:
rcases m with (m | ⟨l₁, l₂, m, _, rfl⟩)

Premises used: rfl
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l : List α
m : l ∈ ts.permutationsAux (t :: is)
⊢ l ~ t :: ts ++ is

Tactic:
(IH1 _ m).trans perm_middle

Premises used: List.Perm.trans, List.perm_middle
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l : List α
m : l ∈ ts.permutationsAux (t :: is)
⊢ l ~ t :: ts ++ is

Tactic:
exact (IH1 _ m).trans perm_middle

Premises used: List.Perm.trans, List.perm_middle
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l₁ l₂ : List α
m : l₁ ++ l₂ ∈ is :: is.permutationsAux []
left : l₂ ≠ []
⊢ l₁ ++ l₂ = is ∨ l₁ ++ l₂ ∈ is.permutationsAux []

Tactic:
simp only [mem_cons] at m

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

Tactic:
rcases m with e | m
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l₁ l₂ : List α
left : l₂ ≠ []
e : l₁ ++ l₂ = is
⊢ l₁ ++ l₂ ~ is

Tactic:
simp [e]
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l₁ l₂ : List α
left : l₂ ≠ []
m : l₁ ++ l₂ ∈ is.permutationsAux []
⊢ l₁ ++ l₂ ~ is

Tactic:
is.append_nil ▸ IH2 _ m

Premises used: Eq.rec, List.append_nil
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l₁ l₂ : List α
left : l₂ ≠ []
m : l₁ ++ l₂ ∈ is.permutationsAux []
⊢ l₁ ++ l₂ ~ is

Tactic:
exact is.append_nil ▸ IH2 _ m
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l₁ l₂ : List α
m : l₁ ++ l₂ ∈ is :: is.permutationsAux []
left : l₂ ≠ []
⊢ l₁ ++ l₂ ~ is

Tactic:
have p : l₁ ++ l₂ ~ is := by
      simp only [mem_cons] at m
      rcases m with e | m
      · simp [e]
      exact is.append_nil ▸ IH2 _ m
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l₁ l₂ : List α
m : l₁ ++ l₂ ∈ is :: is.permutationsAux []
left : l₂ ≠ []
p : l₁ ++ l₂ ~ is
⊢ l₁ ++ t :: l₂ ++ ts ~ t :: ts ++ is

Tactic:
((perm_middle.trans (p.cons _)).append_right _).trans (perm_append_comm.cons _)

Premises used: List.Perm.cons, List.Perm.trans, List.perm_append_comm, List.perm_middle, List.Perm.append_right
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l₁ l₂ : List α
m : l₁ ++ l₂ ∈ is :: is.permutationsAux []
left : l₂ ≠ []
p : l₁ ++ l₂ ~ is
⊢ l₁ ++ t :: l₂ ++ ts ~ t :: ts ++ is

Tactic:
exact ((perm_middle.trans (p.cons _)).append_right _).trans (perm_append_comm.cons _)

Premises used: List.Perm.cons, List.Perm.trans, List.perm_append_comm, List.perm_middle, List.Perm.append_right
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
l₁ l₂ : List α
h : l₁ ∈ l₂.permutations
⊢ l₁ ~ l₂

Tactic:
(eq_or_mem_of_mem_cons h).elim (fun e => e ▸ Perm.refl _) fun m =>
    append_nil l₂ ▸ perm_of_mem_permutationsAux m

Premises used: Eq.rec, List.eq_or_mem_of_mem_cons, List.Perm.refl, List.append_nil, List.perm_of_mem_permutationsAux, Or.elim
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
⊢ ∀ (is : List α), (permutationsAux [] is).length + is.length ! = (length.{u_1} (α := α) [] + is.length)!

Tactic:
simp
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
refine :
  ∀ (t : α) (ts is : List α),
    (ts.permutationsAux (t :: is)).length + (t :: is).length ! = (ts.length + (t :: is).length)! →
      (is.permutationsAux []).length + (length.{u_1} (α := α) [])! = (is.length + length.{u_1} (α := α) [])! →
        ((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!
⊢ ∀ (ts is : List α), (ts.permutationsAux is).length + is.length ! = (ts.length + is.length)!

Tactic:
refine permutationsAux.rec (by simp) ?_
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts is : List α
IH1 : (ts.permutationsAux (t :: is)).length + (t :: is).length ! = (ts.length + (t :: is).length)!
IH2 : (is.permutationsAux []).length + (length.{u_1} (α := α) [])! = (is.length + length.{u_1} (α := α) [])!
⊢ (is.permutationsAux []).length + 1 = is.length !

Tactic:
simpa using IH2
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts is : List α
IH1 : (ts.permutationsAux (t :: is)).length + (t :: is).length ! = (ts.length + (t :: is).length)!
IH2 : (is.permutationsAux []).length + (length.{u_1} (α := α) [])! = (is.length + length.{u_1} (α := α) [])!
⊢ (is.permutationsAux []).length + 1 = is.length !

Tactic:
have IH2 : length (permutationsAux is nil) + 1 = is.length ! := by simpa using IH2
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts is : List α
IH1 : (ts.permutationsAux (t :: is)).length + (t :: is).length ! = (ts.length + (t :: is).length)!
IH2_1 : (is.permutationsAux []).length + (length.{u_1} (α := α) [])! = (is.length + length.{u_1} (α := α) [])!
IH2 : (is.permutationsAux []).length + 1 = is.length !
⊢ (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ =
    (ts.length + is.length)! * (ts.length + is.length).succ

Tactic:
simp only [factorial, Nat.mul_comm, add_eq] at IH1

Premises used: Nat.add_eq, Nat.mul_comm, Nat.factorial
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
l : List α
⊢ l.permutations.length = l.length !

Tactic:
length_permutationsAux l []

Premises used: Nat.factorial, List.length_permutationsAux, List.nil
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
is l : List α
H : l ~ [] ++ is → (∃ (ts' : List α), ∃ (x : ts' ~ []), l = ts' ++ is) ∨ l ∈ is.permutationsAux []
⊢ l ~ is → l ∈ is.permutations

Tactic:
simpa [permutations, perm_nil] using H

Premises used: List.perm_nil, List.permutations
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
⊢ ∀ (is l : List α), l ~ is ++ [] → (∃ (is' : List α), ∃ (x : is' ~ is), l = is' ++ []) ∨ l ∈ permutationsAux [] is

Tactic:
simp
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
refine :
  ∀ (t : α) (ts is : List α),
    (∀ (l : List α),
        l ~ t :: is ++ ts →
          (∃ (is' : List α), ∃ (x : is' ~ t :: is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)) →
      (∀ (l : List α), l ~ [] ++ is → (∃ (is' : List α), ∃ (x : is' ~ []), l = is' ++ is) ∨ l ∈ is.permutationsAux []) →
        ∀ (l : List α),
          l ~ is ++ t :: ts →
            (∃ (is' : List α), ∃ (x : is' ~ is), l = is' ++ t :: ts) ∨ l ∈ (t :: ts).permutationsAux is
⊢ ∀ (ts is l : List α), l ~ is ++ ts → (∃ (is' : List α), ∃ (x : is' ~ is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux is

Tactic:
refine permutationsAux.rec (by 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 α
p : l ~ is ++ t :: ts
rw :
  (∃ (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
⊢ (∃ (is' : List α), ∃ (x : is' ~ is), l = is' ++ t :: ts) ∨ l ∈ (t :: ts).permutationsAux is

Tactic:
rw [permutationsAux_cons, mem_foldr_permutationsAux2]

Premises used: List.permutationsAux_cons, List.mem_foldr_permutationsAux2
-- 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
inl :
  ∀ (is' : List α) (p' : is' ~ t :: is) (e : l = is' ++ ts),
    (∃ (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
inr :
  ∀ (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
⊢ (∃ (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:
rcases IH1 _ (p.trans perm_middle) with (⟨is', p', e⟩ | m)

Premises used: List.Perm.trans, List.perm_middle
-- 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 is' : List α
p' : is' ~ t :: is
e : l = is' ++ ts
inl :
  (∃ (is'_1 : List α), ∃ (x : is'_1 ~ is), is' ++ ts = is'_1 ++ t :: ts) ∨
    is' ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ (l₁ : List α), ∃ (l₂ : List α), l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ is' ++ ts = l₁ ++ t :: l₂ ++ ts
⊢ (∃ (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:
subst e
-- 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 []
is' : List α
p' : is' ~ t :: is
inl :
  ∀ (l₁ l₂ : List α) (e : is' = l₁ ++ t :: l₂),
    (∃ (is'_1 : List α), ∃ (x : is'_1 ~ is), is' ++ ts = is'_1 ++ t :: ts) ∨
      is' ++ ts ∈ ts.permutationsAux (t :: is) ∨
        ∃ (l₁ : List α), ∃ (l₂ : List α), l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ is' ++ ts = l₁ ++ t :: l₂ ++ ts
⊢ (∃ (is'_1 : List α), ∃ (x : is'_1 ~ is), is' ++ ts = is'_1 ++ t :: ts) ∨
    is' ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ (l₁ : List α), ∃ (l₂ : List α), l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ is' ++ ts = l₁ ++ t :: l₂ ++ ts

Tactic:
rcases append_of_mem (p'.symm.subset mem_cons_self) with ⟨l₁, l₂, e⟩

Premises used: List.Perm.subset, List.append_of_mem, List.Perm.symm, List.mem_cons_self
-- 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 []
is' : List α
p' : is' ~ t :: is
l₁ l₂ : List α
e : is' = l₁ ++ t :: l₂
inl :
  ∀ (p' : l₁ ++ t :: l₂ ~ t :: is),
    (∃ (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
⊢ (∃ (is'_1 : List α), ∃ (x : is'_1 ~ is), is' ++ ts = is'_1 ++ t :: ts) ∨
    is' ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ (l₁ : List α), ∃ (l₂ : List α), l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ is' ++ ts = l₁ ++ t :: l₂ ++ ts

Tactic:
subst is'
-- 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
⊢ l₁ ++ l₂ ~ is

Tactic:
have p := (perm_middle.symm.trans p').cons_inv