awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts ys l l' : List α
cons :
  ∀ (y : α) (ys : List α)
    (ih :
      ∀ {l : List α},
        Membership.mem (γ := List (List α)) (Prod.snd (permutationsAux2 t ts [] ys fun (x : List α) ↦ l ++ x)) l' ↔
          ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts)
    {l : List α},
    Membership.mem (γ := List (List α)) (Prod.snd (permutationsAux2 t ts [] (y :: ys) fun (x : List α) ↦ l ++ x)) l' ↔
      ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
⊢ Membership.mem (γ := List (List α)) (Prod.snd (permutationsAux2 t ts [] ys fun (x : List α) ↦ l ++ x)) l' ↔
    ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts

Tactic:
induction ys generalizing l with
  | nil => simp +contextual
  | cons y ys ih => ?_

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts l' : List α
y : α
ys : List α
ih :
  ∀ {l : List α},
    Membership.mem (γ := List (List α)) (Prod.snd (permutationsAux2 t ts [] ys fun (x : List α) ↦ l ++ x)) l' ↔
      ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
l : List α
⊢ Eq.{u_1 + 1} (α := (x : List α) → List α) (fun (x : List α) ↦ l ++ y :: x) fun (x : List α) ↦ l ++ [y] ++ x

Tactic:
simp
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts l' : List α
y : α
ys : List α
ih :
  ∀ {l : List α},
    Membership.mem (γ := List (List α)) (Prod.snd (permutationsAux2 t ts [] ys fun (x : List α) ↦ l ++ x)) l' ↔
      ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
l : List α
cons :
  (l' = l ++ (t :: y :: ys ++ ts) ∨
      ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts) ↔
    ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
⊢ Membership.mem (γ := List (List α)) (Prod.snd (permutationsAux2 t ts [] (y :: ys) fun (x : List α) ↦ l ++ x)) l' ↔
    ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts

Tactic:
rw [permutationsAux2_snd_cons,
    show (fun x : List α => l ++ y :: x) = (l ++ [y] ++ ·) by simp, mem_cons, ih]

Premises used: List.permutationsAux2_snd_cons, List.mem_cons
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts l' : List α
y : α
ys : List α
ih :
  ∀ {l : List α},
    Membership.mem (γ := List (List α)) (Prod.snd (permutationsAux2 t ts [] ys fun (x : List α) ↦ l ++ x)) l' ↔
      ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
l : List α
cons :
  (l' = l ++ (t :: y :: ys ++ ts) ∨
      ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts) →
    ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts
cons₁ :
  (∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts) →
    l' = l ++ (t :: y :: ys ++ ts) ∨
      ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts
⊢ (l' = l ++ (t :: y :: ys ++ ts) ∨
      ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts) ↔
    ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts

Tactic:
constructor
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts : List α
y : α
ys l : List α
ih :
  ∀ {l_1 : List α},
    Membership.mem (γ := List (List α)) (Prod.snd (permutationsAux2 t ts [] ys fun (x : List α) ↦ l_1 ++ x))
        (l ++ (t :: y :: ys ++ ts)) ↔
      ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l ++ (t :: y :: ys ++ ts) = l_1 ++ l₁ ++ t :: l₂ ++ ts
⊢ y :: ys ≠ [] ∧ y :: ys = [] ++ y :: ys ∧ l ++ (t :: y :: ys ++ ts) = l ++ [] ++ t :: y :: ys ++ ts

Tactic:
simp
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts : List α
y : α
ys l : List α
ih :
  ∀ {l_1 : List α},
    Membership.mem (γ := List (List α)) (Prod.snd (permutationsAux2 t ts [] ys fun (x : List α) ↦ l_1 ++ x))
        (l ++ (t :: y :: ys ++ ts)) ↔
      ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l ++ (t :: y :: ys ++ ts) = l_1 ++ l₁ ++ t :: l₂ ++ ts
⊢ ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ y :: ys = l₁ ++ l₂ ∧ l ++ (t :: y :: ys ++ ts) = l ++ l₁ ++ t :: l₂ ++ ts

Tactic:
exact ⟨[], y :: ys, by simp⟩
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts : List α
y : α
l l₁ l₂ : List α
l0 : l₂ ≠ []
ih :
  ∀ {l_1 : List α},
    Membership.mem (γ := List (List α)) (Prod.snd (permutationsAux2 t ts [] (l₁ ++ l₂) fun (x : List α) ↦ l_1 ++ x))
        (l ++ [y] ++ l₁ ++ t :: l₂ ++ ts) ↔
      ∃ (l₁_1 : List α),
        ∃ (l₂_1 : List α),
          l₂_1 ≠ [] ∧ l₁ ++ l₂ = l₁_1 ++ l₂_1 ∧ l ++ [y] ++ l₁ ++ t :: l₂ ++ ts = l_1 ++ l₁_1 ++ t :: l₂_1 ++ ts
⊢ y :: (l₁ ++ l₂) = y :: l₁ ++ l₂ ∧ l ++ [y] ++ l₁ ++ t :: l₂ ++ ts = l ++ y :: l₁ ++ t :: l₂ ++ ts

Tactic:
simp
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts : List α
y : α
l l₁ l₂ : List α
l0 : l₂ ≠ []
ih :
  ∀ {l_1 : List α},
    Membership.mem (γ := List (List α)) (Prod.snd (permutationsAux2 t ts [] (l₁ ++ l₂) fun (x : List α) ↦ l_1 ++ x))
        (l ++ [y] ++ l₁ ++ t :: l₂ ++ ts) ↔
      ∃ (l₁_1 : List α),
        ∃ (l₂_1 : List α),
          l₂_1 ≠ [] ∧ l₁ ++ l₂ = l₁_1 ++ l₂_1 ∧ l ++ [y] ++ l₁ ++ t :: l₂ ++ ts = l_1 ++ l₁_1 ++ t :: l₂_1 ++ ts
⊢ ∃ (l₁_1 : List α),
    ∃ (l₂_1 : List α),
      l₂_1 ≠ [] ∧ y :: (l₁ ++ l₂) = l₁_1 ++ l₂_1 ∧ l ++ [y] ++ l₁ ++ t :: l₂ ++ ts = l ++ l₁_1 ++ t :: l₂_1 ++ ts

Tactic:
exact ⟨y :: l₁, l₂, l0, by simp⟩
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts : List α
y : α
ys l l₂ : List α
l0 : l₂ ≠ []
ye : y :: ys = [] ++ l₂
ih :
  ∀ {l_1 : List α},
    Membership.mem (γ := List (List α)) (Prod.snd (permutationsAux2 t ts [] ys fun (x : List α) ↦ l_1 ++ x))
        (l ++ [] ++ t :: l₂ ++ ts) ↔
      ∃ (l₁ : List α),
        ∃ (l₂_1 : List α), l₂_1 ≠ [] ∧ ys = l₁ ++ l₂_1 ∧ l ++ [] ++ t :: l₂ ++ ts = l_1 ++ l₁ ++ t :: l₂_1 ++ ts
⊢ l ++ [] ++ t :: l₂ ++ ts = l ++ (t :: y :: ys ++ ts) ∨
    ∃ (l₁ : List α),
      ∃ (l₂_1 : List α), l₂_1 ≠ [] ∧ ys = l₁ ++ l₂_1 ∧ l ++ [] ++ t :: l₂ ++ ts = l ++ [y] ++ l₁ ++ t :: l₂_1 ++ ts

Tactic:
simp [ye]
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts : List α
y : α
ys l : List α
y' : α
l₁ l₂ : List α
l0 : l₂ ≠ []
ye : y :: ys = y' :: (l₁ ++ l₂)
ih :
  ∀ {l_1 : List α},
    Membership.mem (γ := List (List α)) (Prod.snd (permutationsAux2 t ts [] ys fun (x : List α) ↦ l_1 ++ x))
        (l ++ y' :: l₁ ++ t :: l₂ ++ ts) ↔
      ∃ (l₁_1 : List α),
        ∃ (l₂_1 : List α),
          l₂_1 ≠ [] ∧ ys = l₁_1 ++ l₂_1 ∧ l ++ y' :: l₁ ++ t :: l₂ ++ ts = l_1 ++ l₁_1 ++ t :: l₂_1 ++ ts
cons :
  ∀
    (ih :
      ∀ {l_1 : List α},
        Membership.mem (γ := List (List α)) (Prod.snd (permutationsAux2 t ts [] (l₁ ++ l₂) fun (x : List α) ↦ l_1 ++ x))
            (l ++ y :: l₁ ++ t :: l₂ ++ ts) ↔
          ∃ (l₁_1 : List α),
            ∃ (l₂_1 : List α),
              l₂_1 ≠ [] ∧ l₁ ++ l₂ = l₁_1 ++ l₂_1 ∧ l ++ y :: l₁ ++ t :: l₂ ++ ts = l_1 ++ l₁_1 ++ t :: l₂_1 ++ ts),
    l ++ y :: l₁ ++ t :: l₂ ++ ts = l ++ (t :: y :: (l₁ ++ l₂) ++ ts) ∨
      ∃ (l₁_1 : List α),
        ∃ (l₂_1 : List α),
          l₂_1 ≠ [] ∧ l₁ ++ l₂ = l₁_1 ++ l₂_1 ∧ l ++ y :: l₁ ++ t :: l₂ ++ ts = l ++ [y] ++ l₁_1 ++ t :: l₂_1 ++ ts
⊢ l ++ y' :: l₁ ++ t :: l₂ ++ ts = l ++ (t :: y :: ys ++ ts) ∨
    ∃ (l₁_1 : List α),
      ∃ (l₂_1 : List α),
        l₂_1 ≠ [] ∧ ys = l₁_1 ++ l₂_1 ∧ l ++ y' :: l₁ ++ t :: l₂ ++ ts = l ++ [y] ++ l₁_1 ++ t :: l₂_1 ++ ts

Tactic:
rcases ye with ⟨rfl, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts : List α
y : α
l l₁ l₂ : List α
l0 : l₂ ≠ []
ih :
  ∀ {l_1 : List α},
    Membership.mem (γ := List (List α)) (Prod.snd (permutationsAux2 t ts [] (l₁ ++ l₂) fun (x : List α) ↦ l_1 ++ x))
        (l ++ y :: l₁ ++ t :: l₂ ++ ts) ↔
      ∃ (l₁_1 : List α),
        ∃ (l₂_1 : List α),
          l₂_1 ≠ [] ∧ l₁ ++ l₂ = l₁_1 ++ l₂_1 ∧ l ++ y :: l₁ ++ t :: l₂ ++ ts = l_1 ++ l₁_1 ++ t :: l₂_1 ++ ts
⊢ l₁ ++ l₂ = l₁ ++ l₂ ∧ l ++ y :: l₁ ++ t :: l₂ ++ ts = l ++ [y] ++ l₁ ++ t :: l₂ ++ ts

Tactic:
simp
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts : List α
y : α
l l₁ l₂ : List α
l0 : l₂ ≠ []
ih :
  ∀ {l_1 : List α},
    Membership.mem (γ := List (List α)) (Prod.snd (permutationsAux2 t ts [] (l₁ ++ l₂) fun (x : List α) ↦ l_1 ++ x))
        (l ++ y :: l₁ ++ t :: l₂ ++ ts) ↔
      ∃ (l₁_1 : List α),
        ∃ (l₂_1 : List α),
          l₂_1 ≠ [] ∧ l₁ ++ l₂ = l₁_1 ++ l₂_1 ∧ l ++ y :: l₁ ++ t :: l₂ ++ ts = l_1 ++ l₁_1 ++ t :: l₂_1 ++ ts
⊢ l ++ y :: l₁ ++ t :: l₂ ++ ts = l ++ (t :: y :: (l₁ ++ l₂) ++ ts) ∨
    ∃ (l₁_1 : List α),
      ∃ (l₂_1 : List α),
        l₂_1 ≠ [] ∧ l₁ ++ l₂ = l₁_1 ++ l₂_1 ∧ l ++ y :: l₁ ++ t :: l₂ ++ ts = l ++ [y] ++ l₁_1 ++ t :: l₂_1 ++ ts

Tactic:
exact Or.inr ⟨l₁, l₂, l0, by simp⟩

Premises used: Or.inr
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts ys l : List α
h : ∀ (x : List α), id x = [] ++ x
⊢ Eq.{u_1 + 1} (α := (a : List α) → List α) id fun (x : List α) ↦ [] ++ x

Tactic:
funext _
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts ys l x : List α
⊢ id x = [] ++ x

Tactic:
rfl
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts ys l : List α
⊢ Membership.mem (γ := List (List α)) (Prod.snd (permutationsAux2 t ts [] ys fun (x : List α) ↦ [] ++ x)) l ↔
    ∃ (l₁ : List α), ∃ (l₂ : List α), l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l = l₁ ++ t :: l₂ ++ ts

Tactic:
apply mem_permutationsAux2

Premises used: List.mem_permutationsAux2
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
nil : ∀ (f : List α → β), (permutationsAux2 t ts [] [] f).snd.length = length.{u_1} (α := α) []
cons :
  ∀ (head : α) (tail : List α),
    (∀ (f : List α → β), (permutationsAux2 t ts [] tail f).snd.length = tail.length) →
      ∀ (f : List α → β), (permutationsAux2 t ts [] (head :: tail) f).snd.length = (head :: tail).length
⊢ (permutationsAux2 t ts [] ys f).snd.length = ys.length

Tactic:
induction ys generalizing f
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
β : Type u_2
t : α
ts : List α
f : List α → β
⊢ (permutationsAux2 t ts [] [] f).snd.length = length.{u_1} (α := α) []

Tactic:
simp [*]
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
β : Type u_2
t : α
ts : List α
head : α
tail : List α
tail_ih : ∀ (f : List α → β), (permutationsAux2 t ts [] tail f).snd.length = tail.length
f : List α → β
⊢ (permutationsAux2 t ts [] (head :: tail) f).snd.length = (head :: tail).length

Tactic:
simp [*]
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts : List α
r : List (List α)
⊢ foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r [] =
    flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) [] ++ r

Tactic:
rfl
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts : List α
r : List (List α)
l : List α
L : List (List α)
ih :
  foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r L =
    flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) L ++ r
cons :
  (permutationsAux2 t ts (foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r L) l
        id).snd =
    flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) (l :: L) ++ r
cons₁ :
  (permutationsAux2 t ts (flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) L ++ r) l id).snd =
    flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) (l :: L) ++ r
cons₂ :
  (permutationsAux2 t ts (flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) L ++ r) l id).snd =
    (permutationsAux2 t ts [] l id).snd ++ flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) L ++ r
cons₃ :
  (permutationsAux2 t ts (flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) L ++ r) l id).snd =
    (permutationsAux2 t ts [] l id).snd ++ (flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) L ++ r)
⊢ foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r (l :: L) =
    flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) (l :: L) ++ r

Tactic:
simp_rw [foldr_cons, ih, flatMap_cons, append_assoc, permutationsAux2_append]

Premises used: List.foldr_cons, List.append_assoc, List.flatMap_cons, List.permutationsAux2_append
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts : List α
r L : List (List α)
nil :
  foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r [] =
    flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) [] ++ r
cons :
  ∀ (l : List α) (L : List (List α))
    (ih :
      foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r L =
        flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) L ++ r),
    foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r (l :: L) =
      flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) (l :: L) ++ r
⊢ foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r L =
    flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) L ++ r

Tactic:
induction L with
  | nil => rfl
  | cons l L ih => simp_rw [foldr_cons, ih, flatMap_cons, append_assoc, permutationsAux2_append]

Premises used: List.foldr_cons, List.append_assoc, List.cons, List.flatMap_cons, List.permutationsAux2_append, List.nil
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts : List α
r L : List (List α)
l' : List α
⊢ (∃ (a : List α), a ∈ L ∧ ∃ (l₁ : List α), ∃ (l₂ : List α), ¬l₂ = [] ∧ a = l₁ ++ l₂ ∧ l' = l₁ ++ t :: (l₂ ++ ts)) ↔
    ∃ (l₁ : List α), ∃ (l₂ : List α), ¬l₂ = [] ∧ l₁ ++ l₂ ∈ L ∧ l' = l₁ ++ t :: (l₂ ++ ts)

Tactic:
have :
    (∃ a : List α,
        a ∈ L ∧ ∃ l₁ l₂ : List α, ¬l₂ = nil ∧ a = l₁ ++ l₂ ∧ l' = l₁ ++ t :: (l₂ ++ ts)) ↔
      ∃ l₁ l₂ : List α, ¬l₂ = nil ∧ l₁ ++ l₂ ∈ L ∧ l' = l₁ ++ t :: (l₂ ++ ts) :=
    ⟨fun ⟨_, aL, l₁, l₂, l0, e, h⟩ => ⟨l₁, l₂, l0, e ▸ aL, h⟩, fun ⟨l₁, l₂, l0, aL, h⟩ =>
      ⟨_, aL, l₁, l₂, l0, rfl, h⟩⟩
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts : List α
r L : List (List α)
l' : List α
this :
  (∃ (a : List α), a ∈ L ∧ ∃ (l₁ : List α), ∃ (l₂ : List α), ¬l₂ = [] ∧ a = l₁ ++ l₂ ∧ l' = l₁ ++ t :: (l₂ ++ ts)) ↔
    ∃ (l₁ : List α), ∃ (l₂ : List α), ¬l₂ = [] ∧ l₁ ++ l₂ ∈ L ∧ l' = l₁ ++ t :: (l₂ ++ ts)
rw :
  l' ∈ flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) L ++ r ↔
    l' ∈ r ∨ ∃ (l₁ : List α), ∃ (l₂ : List α), l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts
⊢ l' ∈ foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r L ↔
    l' ∈ r ∨ ∃ (l₁ : List α), ∃ (l₂ : List α), l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts

Tactic:
rw [foldr_permutationsAux2]

Premises used: List.foldr_permutationsAux2
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts : List α
r L : List (List α)
l' : List α
this :
  (∃ (a : List α), a ∈ L ∧ ∃ (l₁ : List α), ∃ (l₂ : List α), ¬l₂ = [] ∧ a = l₁ ++ l₂ ∧ l' = l₁ ++ t :: (l₂ ++ ts)) ↔
    ∃ (l₁ : List α), ∃ (l₂ : List α), ¬l₂ = [] ∧ l₁ ++ l₂ ∈ L ∧ l' = l₁ ++ t :: (l₂ ++ ts)
⊢ l' ∈ flatMap (fun (y : List α) ↦ (permutationsAux2 t ts [] y id).snd) L ++ r ↔
    l' ∈ r ∨ ∃ (l₁ : List α), ∃ (l₂ : List α), l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts

Tactic:
simp only [mem_permutationsAux2', ← this, or_comm, and_left_comm, mem_append, mem_flatMap,
    append_assoc, cons_append]

Premises used: List.append_assoc, and_left_comm, List.mem_permutationsAux2', List.mem_append, List.mem_flatMap, or_comm, List.cons_append
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts : List α
r L : List (List α)
⊢ (foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r L).length =
    (map length L).sum + r.length

Tactic:
simp [foldr_permutationsAux2, length_permutationsAux2, length_flatMap]

Premises used: List.length_flatMap, List.foldr_permutationsAux2, List.length_permutationsAux2
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts : List α
r L : List (List α)
n : ℕ
H : ∀ (l : List α), l ∈ L → l.length = n
rw : (map length L).sum = n * L.length
⊢ (foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) r L).length =
    n * L.length + r.length

Tactic:
rw [length_foldr_permutationsAux2, (_ : (map length L).sum = n * length L)]

Premises used: List.length_foldr_permutationsAux2
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts : List α
r : List (List α)
n : ℕ
H : ∀ (l : List α), Membership.mem (γ := List (List α)) [] l → l.length = n
⊢ (map.{u_1, 0} (α := List α) length []).sum = n * length.{u_1} (α := List α) []

Tactic:
simp
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts : List α
r : List (List α)
n : ℕ
l : List α
L : List (List α)
ih : ∀ (H : ∀ (l : List α), l ∈ L → l.length = n), (map length L).sum = n * L.length
H : ∀ (l_1 : List α), l_1 ∈ l :: L → l_1.length = n
⊢ (map length L).sum = n * L.length

Tactic:
have sum_map : (map length L).sum = n * length L := ih fun l m => H l (mem_cons_of_mem _ m)
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts : List α
r : List (List α)
n : ℕ
l : List α
L : List (List α)
ih : ∀ (H : ∀ (l : List α), l ∈ L → l.length = n), (map length L).sum = n * L.length
H : ∀ (l_1 : List α), l_1 ∈ l :: L → l_1.length = n
sum_map : (map length L).sum = n * L.length
⊢ l.length = n

Tactic:
have length_l : length l = n := H _ mem_cons_self
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts : List α
r : List (List α)
n : ℕ
l : List α
L : List (List α)
ih : ∀ (H : ∀ (l : List α), l ∈ L → l.length = n), (map length L).sum = n * L.length
H : ∀ (l_1 : List α), l_1 ∈ l :: L → l_1.length = n
sum_map : (map length L).sum = n * L.length
length_l : l.length = n
⊢ (map length (l :: L)).sum = n * (l :: L).length

Tactic:
simp [sum_map, length_l, Nat.add_comm, mul_succ]

Premises used: Nat.mul_succ, Nat.add_comm
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts : List α
r L : List (List α)
n : ℕ
H : ∀ (l : List α), l ∈ L → l.length = n
nil :
  ∀ (H : ∀ (l : List α), Membership.mem (γ := List (List α)) [] l → l.length = n),
    (map.{u_1, 0} (α := List α) length []).sum = n * length.{u_1} (α := List α) []
cons :
  ∀ (l : List α) (L : List (List α))
    (ih : ∀ (H : ∀ (l : List α), l ∈ L → l.length = n), (map length L).sum = n * L.length)
    (H : ∀ (l_1 : List α), l_1 ∈ l :: L → l_1.length = n), (map length (l :: L)).sum = n * (l :: L).length
⊢ (map length L).sum = n * L.length

Tactic:
induction L with
  | nil => simp
  | cons l L ih =>
    have sum_map : (map length L).sum = n * length L := ih fun l m => H l (mem_cons_of_mem _ m)
    have length_l : length l = n := H _ mem_cons_self
    simp [sum_map, length_l, Nat.add_comm, mul_succ]

Premises used: Nat.mul_succ, List.cons, List.nil, Nat.add_comm
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
is : List α
rw :
  Eq (α := List (List α))
    (permutationsAux.rec (C := fun (x x_1 : List α) ↦ List (List α)) (fun (x : List α) ↦ [])
        (fun (t : α) (ts is : List α) (IH1 IH2 : List (List α)) ↦
          foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) IH1 (is :: IH2))
        [] is :
      List (List α))
    ([] : List (List α))
rw₁ rw₂ : Eq.{u_1 + 1} (α := List (List α)) [] []
⊢ permutationsAux [] is = []

Tactic:
rw [permutationsAux, permutationsAux.rec]

Premises used: List.permutationsAux
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts is : List α
rw :
  foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd)
      (permutationsAux.rec (C := fun (x x_1 : List α) ↦ List (List α)) (fun (x : List α) ↦ [])
        (fun (t : α) (ts is : List α) (IH1 IH2 : List (List α)) ↦
          foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) IH1 (is :: IH2))
        ts (t :: is))
      (is ::
        permutationsAux.rec (C := fun (x x_1 : List α) ↦ List (List α)) (fun (x : List α) ↦ [])
          (fun (t : α) (ts is : List α) (IH1 IH2 : List (List α)) ↦
            foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) IH1 (is :: IH2))
          is []) =
    foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is))
      is.permutations
⊢ (t :: ts).permutationsAux is =
    foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is))
      is.permutations

Tactic:
rw [permutationsAux, permutationsAux.rec]

Premises used: List.permutationsAux
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts is : List α
⊢ foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd)
      (permutationsAux.rec (C := fun (x x_1 : List α) ↦ List (List α)) (fun (x : List α) ↦ [])
        (fun (t : α) (ts is : List α) (IH1 IH2 : List (List α)) ↦
          foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) IH1 (is :: IH2))
        ts (t :: is))
      (is ::
        permutationsAux.rec (C := fun (x x_1 : List α) ↦ List (List α)) (fun (x : List α) ↦ [])
          (fun (t : α) (ts is : List α) (IH1 IH2 : List (List α)) ↦
            foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) IH1 (is :: IH2))
          is []) =
    foldr (fun (y : List α) (r : List (List α)) ↦ (permutationsAux2 t ts r y id).snd) (ts.permutationsAux (t :: is))
      is.permutations

Tactic:
rfl
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
rw : Eq.{u_1 + 1} (α := List (List α)) ([] :: permutationsAux [] []) [[]]
rw₁ rw₂ : Eq.{u_1 + 1} (α := List (List α)) [[]] [[]]
⊢ Eq.{u_1 + 1} (α := List (List α)) (permutations []) [[]]

Tactic:
rw [permutations, permutationsAux_nil]

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

Tactic:
simp
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
β : Type u_2
f : α → β
refine :
  ∀ (t : α) (ts is : List α),
    map (map f) (ts.permutationsAux (t :: is)) = (map f ts).permutationsAux (map f (t :: is)) →
      map (map f) (is.permutationsAux []) = (map f is).permutationsAux (map f []) →
        map (map f) ((t :: ts).permutationsAux is) = (map f (t :: ts)).permutationsAux (map f is)
⊢ ∀ (ts is : List α), map (map f) (ts.permutationsAux is) = (map f ts).permutationsAux (map f is)

Tactic:
refine permutationsAux.rec (by simp) ?_
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
β : Type u_2
f : α → β
t : α
ts is : List α
IH1 : map (map f) (ts.permutationsAux (t :: is)) = (map f ts).permutationsAux (map f (t :: is))
IH2 : map (map f) (is.permutationsAux []) = (map f is).permutationsAux (map f [])
⊢ map (map f) (is.permutationsAux []) = (map f is).permutationsAux []

Tactic:
rw [map] at IH2

Premises used: List.map
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
β : Type u_2
f : α → β
t : α
ts is : List α
IH1 : map (map f) (ts.permutationsAux (t :: is)) = (map f ts).permutationsAux (map f (t :: is))
IH2 : map (map f) (is.permutationsAux []) = (map f is).permutationsAux []
⊢ map (map f) ((t :: ts).permutationsAux is) = (map f (t :: ts)).permutationsAux (map f is)

Tactic:
simp only [foldr_permutationsAux2, map_append, map, map_map_permutationsAux2, permutations,
    flatMap_map, IH1, append_assoc, permutationsAux_cons, flatMap_cons, ← IH2, map_flatMap]

Premises used: List.append_assoc, List.map, List.permutationsAux_cons, List.permutations, List.flatMap_cons, List.flatMap_map, List.foldr_permutationsAux2, List.map_flatMap, List.map_append, List.map_map_permutationsAux2