awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Perm.Subperm
Goal:
α : Type u_1
l : List α
a : α
mp : l <+~ [a] → l = [] ∨ l = [a]
mpr : l = [] ∨ l = [a] → l <+~ [a]
⊢ l <+~ [a] ↔ l = [] ∨ l = [a]

Tactic:
constructor
-- Module: Mathlib.Data.List.Perm.Subperm
Goal:
α : Type u_1
l : List α
a : α
mp : (∃ (l_1 : List α), l_1 ~ [a] ∧ l <+ l_1) → l = [] ∨ l = [a]
⊢ l <+~ [a] → l = [] ∨ l = [a]

Tactic:
rw [subperm_iff]

Premises used: List.subperm_iff
-- Module: Mathlib.Data.List.Perm.Subperm
Goal:
α : Type u_1
l : List α
a : α
s : List α
hla : s ~ [a]
h : l <+ s
mp : ∀ (h : l <+ [a]), l = [] ∨ l = [a]
mp₁ mp₂ mp₃ mp₄ : ∀ (h : l = [] ∨ l = [a]), l = [] ∨ l = [a]
⊢ l = [] ∨ l = [a]

Tactic:
rwa [perm_singleton.mp hla, sublist_singleton] at h

Premises used: List.perm_singleton, List.sublist_singleton, Iff.mp
-- Module: Mathlib.Data.List.Perm.Subperm
Goal:
α : Type u_1
a : α
⊢ [] <+~ [a]

Tactic:
nil_subperm

Premises used: List.nil_subperm
-- Module: Mathlib.Data.List.Perm.Subperm
Goal:
α : Type u_1
a : α
⊢ [a] <+~ [a]

Tactic:
Subperm.refl _

Premises used: List.Subperm.refl
-- Module: Mathlib.Data.List.Perm.Subperm
Goal:
α : Type u_1
a : α
⊢ [] <+~ [a]

Tactic:
exacts [nil_subperm, Subperm.refl _]

Premises used: List.Subperm.refl, List.nil_subperm
-- Module: Mathlib.Data.List.Perm.Subperm
Goal:
α : Type u_1
l : List α
a : α
⊢ l <+~ a :: l

Tactic:
⟨l, Perm.refl _, sublist_cons_self _ _⟩

Premises used: List.Perm.refl, List.Subperm, And.intro, Exists.intro, List.sublist_cons_self
-- Module: Mathlib.Data.List.Perm.Subperm
Goal:
α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
a : map f l₁ <+~ map f l₂
obtain : ∀ (w : List β) (perm : w ~ map f l₁) (sublist : w <+ map f l₂), l₁ <+~ l₂
⊢ l₁ <+~ l₂

Tactic:
obtain ⟨w, ⟨perm, sublist⟩⟩ := a
-- Module: Mathlib.Data.List.Perm.Subperm
Goal:
α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
w : List β
perm : w ~ map f l₁
sublist : w <+ map f l₂
obtain : ∀ (x : List α) (sublistₓ : x <+ l₂) (mapₓ : w = map f x), l₁ <+~ l₂
⊢ l₁ <+~ l₂

Tactic:
obtain ⟨x, ⟨sublistₓ, mapₓ⟩⟩ := sublist_map_iff.mp sublist

Premises used: List.sublist_map_iff, Iff.mp
-- Module: Mathlib.Data.List.Perm.Subperm
Goal:
α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
w : List β
perm : w ~ map f l₁
sublist : w <+ map f l₂
x : List α
sublistₓ : x <+ l₂
mapₓ : w = map f x
h : x ~ l₁ ∧ x <+ l₂
⊢ l₁ <+~ l₂

Tactic:
use x
-- Module: Mathlib.Data.List.Perm.Subperm
Goal:
α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
w : List β
perm : w ~ map f l₁
sublist : w <+ map f l₂
x : List α
sublistₓ : x <+ l₂
mapₓ : w = map f x
h : x ~ l₁
h₁ : x <+ l₂
⊢ x ~ l₁ ∧ x <+ l₂

Tactic:
constructor
-- Module: Mathlib.Data.List.Perm.Subperm
Goal:
α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
w : List β
perm : w ~ map f l₁
sublist : w <+ map f l₂
x : List α
sublistₓ : x <+ l₂
mapₓ : w = map f x
⊢ map f x ~ map f l₁

Tactic:
rw [mapₓ] at perm
-- Module: Mathlib.Data.List.Perm.Subperm
Goal:
α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
w : List β
perm : w ~ map f l₁
sublist : w <+ map f l₂
x : List α
sublistₓ : x <+ l₂
mapₓ : w = map f x
perm₁ : map f x ~ map f l₁
⊢ x <+ l₂

Tactic:
rw [mapₓ] at perm
-- Module: Mathlib.Data.List.Perm.Subperm
Goal:
α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
w : List β
perm : w ~ map f l₁
sublist : w <+ map f l₂
x : List α
sublistₓ : x <+ l₂
mapₓ : w = map f x
perm₁ : map f x ~ map f l₁
sublistₓ₁ : x <+ l₂
⊢ w = map f x

Tactic:
rw [mapₓ] at perm
-- Module: Mathlib.Data.List.Perm.Subperm
Goal:
α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
w : List β
sublist : w <+ map f l₂
x : List α
perm : map f x ~ map f l₁
sublistₓ : x <+ l₂
mapₓ : w = map f x
⊢ x ~ l₁

Tactic:
(map_perm_map_iff hf).mp perm

Premises used: List.map_perm_map_iff, Iff.mp
-- Module: Mathlib.Data.List.Perm.Subperm
Goal:
α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
w : List β
sublist : w <+ map f l₂
x : List α
perm : map f x ~ map f l₁
sublistₓ : x <+ l₂
mapₓ : w = map f x
⊢ x ~ l₁

Tactic:
exact (map_perm_map_iff hf).mp perm

Premises used: List.map_perm_map_iff, Iff.mp
-- Module: Mathlib.Data.List.Perm.Subperm
Goal:
α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
w : List β
perm : w ~ map f l₁
sublist : w <+ map f l₂
x : List α
sublistₓ : x <+ l₂
mapₓ : w = map f x
⊢ x <+ l₂

Tactic:
sublistₓ
-- Module: Mathlib.Data.List.Perm.Subperm
Goal:
α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
w : List β
perm : w ~ map f l₁
sublist : w <+ map f l₂
x : List α
sublistₓ : x <+ l₂
mapₓ : w = map f x
⊢ x <+ l₂

Tactic:
exact sublistₓ
-- Module: Mathlib.Data.List.Perm.Subperm
Goal:
α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
a : l₁ <+~ l₂
obtain : ∀ (l : List α) (hl_perm : l ~ l₁) (hl_sub : l <+ l₂), map f l₁ <+~ map f l₂
⊢ map f l₁ <+~ map f l₂

Tactic:
obtain ⟨l, hl_perm, hl_sub⟩ := a
-- Module: Mathlib.Data.List.Perm.Subperm
Goal:
α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
l : List α
hl_perm : l ~ l₁
hl_sub : l <+ l₂
⊢ map f l₁ <+~ map f l₂

Tactic:
⟨l.map f, hl_perm.map f, hl_sub.map f⟩

Premises used: List.map, List.Sublist.map, List.Subperm, And.intro, Exists.intro, List.Perm.map
-- Module: Mathlib.Data.List.Perm.Subperm
Goal:
α : Type u_2
β : Type u_3
l₁ l₂ : List α
f : α → β
hf : Function.Injective f
l : List α
hl_perm : l ~ l₁
hl_sub : l <+ l₂
⊢ map f l₁ <+~ map f l₂

Tactic:
exact ⟨l.map f, hl_perm.map f, hl_sub.map f⟩
-- Module: Mathlib.Data.List.Perm.Subperm
Goal:
α : Type u_1
l₁ l₂ : List α
d : l₁.Nodup
H : l₁ ⊆ l₂
⊢ l₁ <+~ l₂

Tactic:
subperm_of_subset d H

Premises used: List.subperm_of_subset
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
y : α
ys : List α
f : List α → β
⊢ (permutationsAux2 t ts r (y :: ys) f).fst = y :: ys ++ ts

Tactic:
simp [permutationsAux2, permutationsAux2_fst t _ _ ys]

Premises used: List.permutationsAux2
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
f : List α → β
⊢ (permutationsAux2 t ts r [] f).snd = r

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
y : α
ys : List α
f : List α → β
⊢ (permutationsAux2 t ts r (y :: ys) f).snd =
    f (t :: y :: ys ++ ts) :: (permutationsAux2 t ts r ys fun (x : List α) ↦ f (y :: x)).snd

Tactic:
simp [permutationsAux2, permutationsAux2_fst t _ _ ys]

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

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

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

Tactic:
simp [*]
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
f : List α → β
⊢ (permutationsAux2 t [] r [] fun (x : List α) ↦ f (x ++ ts)).snd = (permutationsAux2 t ts r [] f).snd

Tactic:
simp
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
ys_hd : α
tail : List α
ys_ih :
  ∀ (f : List α → β),
    (permutationsAux2 t [] r tail fun (x : List α) ↦ f (x ++ ts)).snd = (permutationsAux2 t ts r tail f).snd
f : List α → β
⊢ (permutationsAux2 t [] r (ys_hd :: tail) fun (x : List α) ↦ f (x ++ ts)).snd =
    (permutationsAux2 t ts r (ys_hd :: tail) f).snd

Tactic:
simp [ys_ih fun xs => f (ys_hd :: xs)]

Premises used: List.cons
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
β : Type u_2
t : α
ts ys : List α
r : List β
f : List α → β
nil :
  ∀ (f : List α → β),
    (permutationsAux2 t [] r [] fun (x : List α) ↦ f (x ++ ts)).snd = (permutationsAux2 t ts r [] f).snd
cons :
  ∀ (ys_hd : α) (tail : List α)
    (ys_ih :
      ∀ (f : List α → β),
        (permutationsAux2 t [] r tail fun (x : List α) ↦ f (x ++ ts)).snd = (permutationsAux2 t ts r tail f).snd)
    (f : List α → β),
    (permutationsAux2 t [] r (ys_hd :: tail) fun (x : List α) ↦ f (x ++ ts)).snd =
      (permutationsAux2 t ts r (ys_hd :: tail) f).snd
⊢ (permutationsAux2 t [] r ys fun (x : List α) ↦ f (x ++ ts)).snd = (permutationsAux2 t ts r ys f).snd

Tactic:
induction ys generalizing f with
  | nil => simp
  | cons ys_hd _ ys_ih => simp [ys_ih fun xs => f (ys_hd :: xs)]

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ map g' (permutationsAux2 t ts r [] f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g []) f').snd

Tactic:
simp
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
ys_hd : α
tail : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β') (H : ∀ (a : List α), g' (f a) = f' (map g a)),
    map g' (permutationsAux2 t ts r tail f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
cons :
  g' (f (t :: ys_hd :: (tail ++ ts))) = f' (g t :: g ys_hd :: (map g tail ++ map g ts)) ∧
    map g' (permutationsAux2 t ts r tail fun (x : List α) ↦ f (ys_hd :: x)).snd =
      (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) fun (x : List α') ↦ f' (g ys_hd :: x)).snd
⊢ map g' (permutationsAux2 t ts r (ys_hd :: tail) f).snd =
    (permutationsAux2 (g t) (map g ts) (map g' r) (map g (ys_hd :: tail)) f').snd

Tactic:
simp only [map, permutationsAux2_snd_cons, cons_append, cons.injEq]

Premises used: List.map, List.cons.injEq, List.permutationsAux2_snd_cons, List.cons_append
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
ys_hd : α
tail : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β') (H : ∀ (a : List α), g' (f a) = f' (map g a)),
    map g' (permutationsAux2 t ts r tail f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
cons :
  g' (f (t :: ys_hd :: (tail ++ ts))) = f' (g t :: g ys_hd :: (map g tail ++ map g ts)) ∧
    (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) fun (x : List α') ↦ f' (g ys_hd :: x)).snd =
      (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) fun (x : List α') ↦ f' (g ys_hd :: x)).snd
cons₁ : List α' → β'
cons₂ : ∀ (a : List α), g' (f (ys_hd :: a)) = f' (g ys_hd :: map g a)
⊢ g' (f (t :: ys_hd :: (tail ++ ts))) = f' (g t :: g ys_hd :: (map g tail ++ map g ts)) ∧
    map g' (permutationsAux2 t ts r tail fun (x : List α) ↦ f (ys_hd :: x)).snd =
      (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) fun (x : List α') ↦ f' (g ys_hd :: x)).snd

Tactic:
rw [ys_ih]
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
ys_hd : α
tail : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β') (H : ∀ (a : List α), g' (f a) = f' (map g a)),
    map g' (permutationsAux2 t ts r tail f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ g' (f (t :: ys_hd :: (tail ++ ts))) = f' (g t :: g ys_hd :: (map g tail ++ map g ts)) ∧
    (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) fun (x : List α') ↦ f' (g ys_hd :: x)).snd =
      (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) fun (x : List α') ↦ f' (g ys_hd :: x)).snd

Tactic:
⟨?_, rfl⟩

Premises used: And.intro, rfl
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
ys_hd : α
tail : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β') (H : ∀ (a : List α), g' (f a) = f' (map g a)),
    map g' (permutationsAux2 t ts r tail f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
cons : g' (f (t :: ys_hd :: (tail ++ ts))) = f' (g t :: g ys_hd :: (map g tail ++ map g ts))
⊢ g' (f (t :: ys_hd :: (tail ++ ts))) = f' (g t :: g ys_hd :: (map g tail ++ map g ts)) ∧
    (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) fun (x : List α') ↦ f' (g ys_hd :: x)).snd =
      (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) fun (x : List α') ↦ f' (g ys_hd :: x)).snd

Tactic:
refine ⟨?_, rfl⟩
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
ys_hd : α
tail : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β') (H : ∀ (a : List α), g' (f a) = f' (map g a)),
    map g' (permutationsAux2 t ts r tail f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
cons : g' (f (t :: ys_hd :: (tail ++ ts))) = f' (map g (t :: ys_hd :: (tail ++ ts)))
⊢ g' (f (t :: ys_hd :: (tail ++ ts))) = f' (g t :: g ys_hd :: (map g tail ++ map g ts))

Tactic:
simp only [← map_cons, ← map_append]

Premises used: List.map_cons, List.map_append
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
ys_hd : α
tail : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β') (H : ∀ (a : List α), g' (f a) = f' (map g a)),
    map g' (permutationsAux2 t ts r tail f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
⊢ g' (f (t :: ys_hd :: (tail ++ ts))) = f' (map g (t :: ys_hd :: (tail ++ ts)))

Tactic:
apply H
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts : List α
r : List β
ys_hd : α
tail : List α
ys_ih :
  ∀ (f : List α → β) (f' : List α' → β') (H : ∀ (a : List α), g' (f a) = f' (map g a)),
    map g' (permutationsAux2 t ts r tail f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) f').snd
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
a : List α
⊢ g' (f (ys_hd :: a)) = f' (g ys_hd :: map g a)

Tactic:
apply H
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
β : Type u_2
α' : Type u_3
β' : Type u_4
g : α → α'
g' : β → β'
t : α
ts ys : List α
r : List β
f : List α → β
f' : List α' → β'
H : ∀ (a : List α), g' (f a) = f' (map g a)
nil :
  ∀ (f : List α → β) (f' : List α' → β') (H : ∀ (a : List α), g' (f a) = f' (map g a)),
    map g' (permutationsAux2 t ts r [] f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g []) f').snd
cons :
  ∀ (ys_hd : α) (tail : List α)
    (ys_ih :
      ∀ (f : List α → β) (f' : List α' → β') (H : ∀ (a : List α), g' (f a) = f' (map g a)),
        map g' (permutationsAux2 t ts r tail f).snd =
          (permutationsAux2 (g t) (map g ts) (map g' r) (map g tail) f').snd)
    (f : List α → β) (f' : List α' → β') (H : ∀ (a : List α), g' (f a) = f' (map g a)),
    map g' (permutationsAux2 t ts r (ys_hd :: tail) f).snd =
      (permutationsAux2 (g t) (map g ts) (map g' r) (map g (ys_hd :: tail)) f').snd
⊢ map g' (permutationsAux2 t ts r ys f).snd = (permutationsAux2 (g t) (map g ts) (map g' r) (map g ys) f').snd

Tactic:
induction ys generalizing f f' with
  | nil => simp
  | cons ys_hd _ ys_ih =>
    simp only [map, permutationsAux2_snd_cons, cons_append, cons.injEq]
    rw [ys_ih]
    · refine ⟨?_, rfl⟩
      simp only [← map_cons, ← map_append]; apply H
    · intro a; apply H

Premises used: List.map_cons, List.map, List.cons, List.cons.injEq, List.permutationsAux2_snd_cons, List.map_append, List.cons_append, List.nil
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
rw : (permutationsAux2 (id t) ts (map f []) ys f).snd = (permutationsAux2 t ts [] ys f).snd
f' : List α → β
H : ∀ (a : List α), f (id a) = f (map id a)
⊢ map f (permutationsAux2 t ts [] ys id).snd = (permutationsAux2 t ts [] ys f).snd

Tactic:
rw [map_permutationsAux2' id, map_id, map_id]

Premises used: List.map_id, id, List.map_permutationsAux2'
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ (permutationsAux2 (id t) ts (map f []) ys f).snd = (permutationsAux2 t ts [] ys f).snd

Tactic:
rfl
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ ∀ (a : List α), f (id a) = f (map id a)

Tactic:
simp
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
β : Type u_2
t : α
ts : List α
r : List β
ys : List α
f : List α → β
rw :
  (permutationsAux2 t ts [] ys f).snd ++ r =
    map (fun (x : List α) ↦ f (x ++ ts)) (permutationsAux2 t [] [] ys id).snd ++ r
rw₁ :
  (permutationsAux2 t ts [] ys f).snd ++ r = Prod.snd (permutationsAux2 t [] [] ys fun (x : List α) ↦ f (x ++ ts)) ++ r
rw₂ rw₃ : (permutationsAux2 t ts [] ys f).snd ++ r = (permutationsAux2 t ts [] ys f).snd ++ r
⊢ (permutationsAux2 t ts r ys f).snd = map (fun (x : List α) ↦ f (x ++ ts)) (permutationsAux2 t [] [] ys id).snd ++ r

Tactic:
rw [← permutationsAux2_append, map_permutationsAux2, permutationsAux2_comp_append]

Premises used: List.map_permutationsAux2, List.permutationsAux2_comp_append, List.permutationsAux2_append
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
α' : Type u_3
g : α → α'
t : α
ts ys : List α
⊢ map (map g) (permutationsAux2 t ts [] ys id).snd = (permutationsAux2 (g t) (map g ts) [] (map g ys) id).snd

Tactic:
map_permutationsAux2' _ _ _ _ _ _ _ _ fun _ => rfl

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

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

Tactic:
simp only [permutations'Aux, map_cons, map_map, ← ih, Function.comp_def]

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

Tactic:
induction ts with
  | nil => rfl
  | cons a ts ih => simp only [permutations'Aux, map_cons, map_map, ← ih, Function.comp_def]

Premises used: List.map_cons, List.map_map, List.cons, Function.comp_def, List.permutations'Aux, List.nil
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
⊢ permutations'Aux t [] = (permutationsAux2 t [] [[] ++ [t]] [] id).snd

Tactic:
rfl
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t a : α
ts : List α
ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd
⊢ permutations'Aux t (a :: ts) = (permutationsAux2 t [] [a :: ts ++ [t]] (a :: ts) id).snd

Tactic:
?_
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t : α
ts : List α
cons :
  ∀ (a : α) (ts : List α) (ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd),
    permutations'Aux t (a :: ts) = (permutationsAux2 t [] [a :: ts ++ [t]] (a :: ts) id).snd
⊢ permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd

Tactic:
induction ts with | nil => rfl | cons a ts ih => ?_

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t a : α
ts : List α
ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd
cons :
  map (List.cons a) (permutationsAux2 t [] [ts ++ [t]] ts id).snd =
    (permutationsAux2 t [] [a :: (ts ++ [t])] ts fun (x : List α) ↦ a :: x).snd
⊢ permutations'Aux t (a :: ts) = (permutationsAux2 t [] [a :: ts ++ [t]] (a :: ts) id).snd

Tactic:
simp only [permutations'Aux, ih, cons_append, permutationsAux2_snd_cons, append_nil, id_eq,
    cons.injEq, true_and]

Premises used: List.append_nil, List.cons.injEq, List.permutationsAux2_snd_cons, List.permutations'Aux, List.cons_append, true_and, id_eq
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t a : α
ts : List α
ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd
cons :
  map (List.cons a) ((permutationsAux2 t [] [] ts id).snd ++ [ts ++ [t]]) =
    Prod.snd (permutationsAux2 t [] [] ts fun (x : List α) ↦ a :: x) ++ [a :: (ts ++ [t])]
⊢ map (List.cons a) (permutationsAux2 t [] [ts ++ [t]] ts id).snd =
    (permutationsAux2 t [] [a :: (ts ++ [t])] ts fun (x : List α) ↦ a :: x).snd

Tactic:
simp +singlePass only [← permutationsAux2_append]

Premises used: List.permutationsAux2_append
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
t a : α
ts : List α
ih : permutations'Aux t ts = (permutationsAux2 t [] [ts ++ [t]] ts id).snd
⊢ map (cons a) ((permutationsAux2 t [] [] ts id).snd ++ [ts ++ [t]]) =
    Prod.snd (permutationsAux2 t [] [] ts fun (x : List α) ↦ a :: x) ++ [a :: (ts ++ [t])]

Tactic:
simp [map_permutationsAux2]

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

Tactic:
simp +contextual
-- 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 α
⊢ 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:
?_