awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m ⋯ = x
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (bs.insertIdx m x) n ⋯ = x

Tactic:
simp [hm', ← hn']
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m ⋯ = x
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (bs.insertIdx m x) n ⋯ = x

Tactic:
have hx' : (bs.insertIdx m x)[n]'(by
          rwa [length_insertIdx_of_le_length hm, Nat.lt_succ_iff, ← hl]) = x := by
        simp [hm', ← hn']
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m ⋯ = x
hx' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (bs.insertIdx m x) n ⋯ = x
cons : ∀ (ht : n < m), False
cons₁ : ∀ (ht : n = m), False
cons₂ : ∀ (ht : m < n), False
⊢ False

Tactic:
rcases lt_trichotomy n m with (ht | ht | ht)

Premises used: lt_trichotomy
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m ⋯ = x
hx' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (bs.insertIdx m x) n ⋯ = x
ht : n < m
this : x ∈ bs
⊢ False

Tactic:
h x (hb.subset this) rfl

Premises used: List.Perm.subset, rfl
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m ⋯ = x
hx' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (bs.insertIdx m x) n ⋯ = x
ht : n < m
this : x ∈ bs
⊢ False

Tactic:
exact h x (hb.subset this) rfl

Premises used: List.Perm.subset, rfl
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m ⋯ = x
hx' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (bs.insertIdx m x) n ⋯ = x
ht : n < m
cons : x ∈ bs
⊢ False

Tactic:
suffices x ∈ bs by exact h x (hb.subset this) rfl
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m ⋯ = x
hx' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (bs.insertIdx m x) n ⋯ = x
ht : n < m
cons : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) bs n ⋯ ∈ bs
⊢ x ∈ bs

Tactic:
rw [← hx', getElem_insertIdx_of_lt ht]

Premises used: List.getElem_insertIdx_of_lt
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m ⋯ = x
hx' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (bs.insertIdx m x) n ⋯ = x
ht : n < m
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) bs n ⋯ ∈ bs

Tactic:
getElem_mem _

Premises used: List.getElem_mem
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m ⋯ = x
hx' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (bs.insertIdx m x) n ⋯ = x
ht : n < m
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) bs n ⋯ ∈ bs

Tactic:
exact getElem_mem _

Premises used: List.getElem_mem
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m ⋯ = x
hx' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (bs.insertIdx m x) n ⋯ = x
ht : n = m
⊢ as.insertIdx m x = a

Tactic:
simp only [ht] at hm' hn'
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m ⋯ = x
hx' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (bs.insertIdx m x) n ⋯ = x
ht : n = m
hn' : as.insertIdx m x = a
⊢ as.insertIdx m x = bs.insertIdx m x

Tactic:
rw [← hm'] at hn'
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m ⋯ = x
hx' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (bs.insertIdx m x) n ⋯ = x
ht : n = m
hn' : as.insertIdx m x = bs.insertIdx m x
⊢ False

Tactic:
H (insertIdx_injective _ _ hn')

Premises used: List.insertIdx_injective
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m ⋯ = x
hx' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (bs.insertIdx m x) n ⋯ = x
ht : n = m
hn' : as.insertIdx m x = bs.insertIdx m x
⊢ False

Tactic:
exact H (insertIdx_injective _ _ hn')

Premises used: List.insertIdx_injective
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m ⋯ = x
hx' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (bs.insertIdx m x) n ⋯ = x
ht : m < n
this : x ∈ as
⊢ False

Tactic:
h x (ha.subset this) rfl

Premises used: List.Perm.subset, rfl
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m ⋯ = x
hx' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (bs.insertIdx m x) n ⋯ = x
ht : m < n
this : x ∈ as
⊢ False

Tactic:
exact h x (ha.subset this) rfl

Premises used: List.Perm.subset, rfl
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m ⋯ = x
hx' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (bs.insertIdx m x) n ⋯ = x
ht : m < n
cons : x ∈ as
⊢ False

Tactic:
suffices x ∈ as by exact h x (ha.subset this) rfl
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m ⋯ = x
hx' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (bs.insertIdx m x) n ⋯ = x
ht : m < n
cons : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) as m ⋯ ∈ as
⊢ x ∈ as

Tactic:
rw [← hx, getElem_insertIdx_of_lt ht]

Premises used: List.getElem_insertIdx_of_lt
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m ⋯ = x
hx' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (bs.insertIdx m x) n ⋯ = x
ht : m < n
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) as m ⋯ ∈ as

Tactic:
getElem_mem _

Premises used: List.getElem_mem
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m ⋯ = x
hx' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (bs.insertIdx m x) n ⋯ = x
ht : m < n
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) as m ⋯ ∈ as

Tactic:
exact getElem_mem _

Premises used: List.getElem_mem
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
hs : s.Nodup
nil : Nodup.{u_1} (α := List α) (permutations' [])
cons :
  ∀ {x : α} {l : List α} (h : ∀ (a' : α), a' ∈ l → x ≠ a') (h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l)
    (IH : l.permutations'.Nodup), (x :: l).permutations'.Nodup
⊢ s.permutations'.Nodup

Tactic:
induction hs with
  | nil => simp
  | @cons x l h h' IH =>
    rw [permutations']
    rw [nodup_flatMap]
    constructor
    · intro ys hy
      rw [mem_permutations'] at hy
      rw [nodup_permutations'Aux_iff, hy.mem_iff]
      exact fun H => h x H rfl
    · refine IH.pairwise_of_forall_ne fun as ha bs hb H => ?_
      rw [Function.onFun, disjoint_iff_ne]
      rintro a ha' b hb' rfl
      obtain ⟨⟨n, hn⟩, hn'⟩ := get_of_mem ha'
      obtain ⟨⟨m, hm⟩, hm'⟩ := get_of_mem hb'
      rw [mem_permutations'] at ha hb
      have hl : as.length = bs.length := (ha.trans hb.symm).length_eq
      simp only [Nat.lt_succ_iff, length_permutations'Aux] at hn hm
      rw [get_permutations'Aux] at hn' hm'
      have hx : (as.insertIdx n x)[m]'(by
          rwa [length_insertIdx_of_le_length hn, Nat.lt_succ_iff, hl]) = x := by
        simp [hn', ← hm']
      have hx' : (bs.insertIdx m x)[n]'(by
          rwa [length_insertIdx_of_le_length hm, Nat.lt_succ_iff, ← hl]) = x := by
        simp [hm', ← hn']
      rcases lt_trichotomy n m with (ht | ht | ht)
      · suffices x ∈ bs by exact h x (hb.subset this) rfl
        rw [← hx', getElem_insertIdx_of_lt ht]
        exact getElem_mem _
      · simp only [ht] at hm' hn'
        rw [← hm'] at hn'
        exact H (insertIdx_injective _ _ hn')
      · suffices x ∈ as by exact h x (ha.subset this) rfl
        rw [← hx, getElem_insertIdx_of_lt ht]
        exact getElem_mem _

Premises used: List.disjoint_iff_ne, Function.onFun, List.get_permutations'Aux, List.nodup_permutations'Aux_iff, List.cons, List.nodup_flatMap, List.length_permutations'Aux, Nat.lt_succ_iff, List.getElem_mem, List.mem_permutations', rfl, List.permutations', List.nil
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
x y : α
s : List α
nil : take 2 [x, y].permutations = [[x, y], [y, x]]
cons :
  ∀ (head : α) (tail : List α),
    take 2 (x :: y :: tail).permutations = [x :: y :: tail, y :: x :: tail] →
      take 2 (x :: y :: head :: tail).permutations = [x :: y :: head :: tail, y :: x :: head :: tail]
⊢ take 2 (x :: y :: s).permutations = [x :: y :: s, y :: x :: s]

Tactic:
induction s
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
x y : α
⊢ take 2 [x, y].permutations = [[x, y], [y, x]]

Tactic:
simp [permutations]

Premises used: List.permutations
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
x y head : α
tail : List α
tail_ih : take 2 (x :: y :: tail).permutations = [x :: y :: tail, y :: x :: tail]
⊢ take 2 (x :: y :: head :: tail).permutations = [x :: y :: head :: tail, y :: x :: head :: tail]

Tactic:
simp [permutations]

Premises used: List.permutations
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
⊢ s.permutations.Nodup ↔ s.Nodup

Tactic:
⟨?_, nodup_permutations s⟩

Premises used: List.nodup_permutations, Iff.intro
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
refine : s.permutations.Nodup → s.Nodup
⊢ s.permutations.Nodup ↔ s.Nodup

Tactic:
refine ⟨?_, nodup_permutations s⟩
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
contrapose : ¬s.Nodup → ¬s.permutations.Nodup
⊢ s.permutations.Nodup → s.Nodup

Tactic:
contrapose
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
rw : (∃ (x : α), Duplicate x s) → ¬s.permutations.Nodup
⊢ ¬s.Nodup → ¬s.permutations.Nodup

Tactic:
rw [← exists_duplicate_iff_not_nodup]

Premises used: List.exists_duplicate_iff_not_nodup
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
hs : Duplicate x s
⊢ [x, x] <+ s

Tactic:
rw [duplicate_iff_sublist] at hs

Premises used: List.duplicate_iff_sublist
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
obtain : ∀ (l : List α) (ht : s ~ [x, x] ++ l), ¬s.permutations.Nodup
⊢ ¬s.permutations.Nodup

Tactic:
obtain ⟨l, ht⟩ := List.Sublist.exists_perm_append hs

Premises used: List.Sublist.exists_perm_append
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
l : List α
ht : s ~ [x, x] ++ l
rw : ∃ (x_1 : List α), Duplicate x_1 ([x, x] ++ l).permutations
⊢ ¬s.permutations.Nodup

Tactic:
rw [List.Perm.nodup_iff (List.Perm.permutations ht), ← exists_duplicate_iff_not_nodup]

Premises used: List.Perm.nodup_iff, List.Perm.permutations, List.exists_duplicate_iff_not_nodup
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
l : List α
ht : s ~ [x, x] ++ l
h : Duplicate (x :: x :: l) ([x, x] ++ l).permutations
⊢ ∃ (x_1 : List α), Duplicate x_1 ([x, x] ++ l).permutations

Tactic:
use x :: x :: l
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
l : List α
ht : s ~ [x, x] ++ l
h : take 2 (x :: x :: l).permutations <+ ([x, x] ++ l).permutations
⊢ Duplicate (x :: x :: l) ([x, x] ++ l).permutations

Tactic:
rw [List.duplicate_iff_sublist, ← permutations_take_two]

Premises used: List.duplicate_iff_sublist, List.permutations_take_two
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
l : List α
ht : s ~ [x, x] ++ l
⊢ take 2 (x :: x :: l).permutations <+ ([x, x] ++ l).permutations

Tactic:
take_sublist 2 _

Premises used: List.append, List.take_sublist, OfNat.ofNat
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
hs : [x, x] <+ s
l : List α
ht : s ~ [x, x] ++ l
⊢ take 2 (x :: x :: l).permutations <+ ([x, x] ++ l).permutations

Tactic:
exact take_sublist 2 _

Premises used: List.take_sublist, OfNat.ofNat
-- Module: Mathlib.Data.List.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
α : ι → Sort u_2
i : ι
l : List ι
a : α i
f : (j : ι) → j ∈ l → α j
⊢ cons (α := α) i l a f = fun (j : ι) (hj : j ∈ i :: l) ↦
    if h : j = i then Eq.rec (motive := fun (x : ι) (x_1 : i = x) ↦ α x) a ⋯ else f j ⋯

Tactic:
rfl

Premises used: List.Pi.cons, Multiset.Pi.cons, rfl
-- Module: Mathlib.Data.List.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
α : ι → Sort u_2
i : ι
l : List ι
a : α i
f : (j : ι) → j ∈ l → α j
⊢ Multiset.Pi.cons (δ := α) (↑l : Multiset ι) i a f = cons (α := α) i l a f

Tactic:
rfl

Premises used: List.Pi.cons, rfl
-- Module: Mathlib.Data.List.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
α : ι → Sort u_2
i : ι
l : List ι
f : (j : ι) → j ∈ i :: l → α j
⊢ cons (α := α) i l (head (α := α) f) (tail (α := α) f) = f

Tactic:
Multiset.Pi.cons_eta (α := ι) (m := l) f

Premises used: List.Pi.cons, List.Pi.head, List.Pi.tail, Multiset.Mem, Multiset.Pi.cons_eta
-- Module: Mathlib.Data.List.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
α : ι → Sort u_2
i : ι
l : List ι
a : α i
f : (j : ι) → j ∈ l → α j
α' : ι → Sort u_3
φ : ⦃j : ι⦄ → α j → α' j
⊢ (cons (α := α') i l (φ a) fun (j : ι) (hj : j ∈ l) ↦ φ (f j hj)) = fun (j : ι) (hj : j ∈ i :: l) ↦
    φ (cons (α := α) i l a f j hj)

Tactic:
Multiset.Pi.cons_map _ _ _

Premises used: List.Pi.cons, Multiset.Pi.cons_map, Multiset.Mem
-- Module: Mathlib.Data.List.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
α : ι → Sort u_2
i : ι
l : List ι
r : ⦃i : ι⦄ → α i → α i → Prop
a₁ a₂ : α i
f₁ f₂ : (j : ι) → j ∈ l → α j
ha : r a₁ a₂
hf : ∀ (i : ι) (hi : i ∈ l), r (f₁ i hi) (f₂ i hi)
⊢ ∀ (j : ι) (hj : j ∈ i :: l), r (cons (α := α) i l a₁ f₁ j hj) (cons (α := α) i l a₂ f₂ j hj)

Tactic:
Multiset.Pi.forall_rel_cons_ext (α := ι) (m := l) ha hf

Premises used: Multiset.Pi.forall_rel_cons_ext, List.Pi.cons, Multiset.Mem
-- Module: Mathlib.Data.List.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
α : ι → Type u_2
t : (i : ι) → List (α i)
⊢ pi (α := α) [] t = [Pi.nil α]

Tactic:
rfl

Premises used: List.pi, rfl
-- Module: Mathlib.Data.List.Pi
Goal:
ι : Type u_1
inst : DecidableEq ι
α : ι → Type u_2
i : ι
l : List ι
t : (j : ι) → List (α j)
⊢ (i :: l).pi (α := α) t = flatMap (fun (b : α i) ↦ map (Pi.cons (α := α) i l b) (l.pi (α := α) t)) (t i)

Tactic:
rfl

Premises used: List.pi, rfl