-- Mathlib/Data/List/Permutation.lean
theorem nodup_permutations (s : List α) (hs : Nodup s) : Nodup s.permutations

Proof state:
case cons.right.intro.mk.intro.mk.inr.inr
α : Type u_1
s : List α
x : α
l : List α
h : ∀ 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✝ : n < (permutations'Aux x as).length
hn' : insertIdx n x as = a
m : ℕ
hm✝ : m < (permutations'Aux x bs).length
hm' : insertIdx m x bs = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : (insertIdx n x as)[m] = x
hx' : (insertIdx m x bs)[n] = x
ht : m < n
⊢ x ∈ as

Tactic:
rw [← hx, getElem_insertIdx_of_lt ht]

Result:
case cons.right.intro.mk.intro.mk.inr.inr
α : Type u_1
s : List α
x : α
l : List α
h : ∀ 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✝ : n < (permutations'Aux x as).length
hn' : insertIdx n x as = a
m : ℕ
hm✝ : m < (permutations'Aux x bs).length
hm' : insertIdx m x bs = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : (insertIdx n x as)[m] = x
hx' : (insertIdx m x bs)[n] = x
ht : m < n
⊢ as[m] ∈ as

Proof state:
case cons
α : Type u_1
s : List α
x : α
l : List α
h : ∀ a' ∈ l, x ≠ a'
h' : Pairwise (fun x1 x2 => x1 ≠ x2) l
IH : l.permutations'.Nodup
⊢ (flatMap (permutations'Aux x) l.permutations').Nodup

Tactic:
rw [nodup_flatMap]

Result:
case cons
α : Type u_1
s : List α
x : α
l : List α
h : ∀ a' ∈ l, x ≠ a'
h' : Pairwise (fun x1 x2 => x1 ≠ x2) l
IH : l.permutations'.Nodup
⊢ (∀ x_1 ∈ l.permutations', (permutations'Aux x x_1).Nodup) ∧ Pairwise (Disjoint on permutations'Aux x) l.permutations'

Proof state:
case cons.left
α : Type u_1
s : List α
x : α
l : List α
h : ∀ a' ∈ l, x ≠ a'
h' : Pairwise (fun x1 x2 => x1 ≠ x2) l
IH : l.permutations'.Nodup
⊢ ∀ x_1 ∈ l.permutations', (permutations'Aux x x_1).Nodup

Tactic:
intro ys hy

Result:
case cons.left
α : Type u_1
s : List α
x : α
l : List α
h : ∀ a' ∈ l, x ≠ a'
h' : Pairwise (fun x1 x2 => x1 ≠ x2) l
IH : l.permutations'.Nodup
ys : List α
hy : ys ∈ l.permutations'
⊢ (permutations'Aux x ys).Nodup

Proof state:
case cons.right.intro.mk.intro.mk.inl
α : Type u_1
s : List α
x : α
l : List α
h : ∀ 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✝ : n < (permutations'Aux x as).length
hn' : insertIdx n x as = a
m : ℕ
hm✝ : m < (permutations'Aux x bs).length
hm' : insertIdx m x bs = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : (insertIdx n x as)[m] = x
hx' : (insertIdx m x bs)[n] = x
ht : n < m
⊢ False

Tactic:
suffices x ∈ bs by exact h x (hb.subset this) rfl

Result:
case cons.right.intro.mk.intro.mk.inl
α : Type u_1
s : List α
x : α
l : List α
h : ∀ 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✝ : n < (permutations'Aux x as).length
hn' : insertIdx n x as = a
m : ℕ
hm✝ : m < (permutations'Aux x bs).length
hm' : insertIdx m x bs = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : (insertIdx n x as)[m] = x
hx' : (insertIdx m x bs)[n] = x
ht : n < m
⊢ x ∈ bs

Proof state:
case cons.right.intro.mk.intro.mk.inl
α : Type u_1
s : List α
x : α
l : List α
h : ∀ 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✝ : n < (permutations'Aux x as).length
hn' : insertIdx n x as = a
m : ℕ
hm✝ : m < (permutations'Aux x bs).length
hm' : insertIdx m x bs = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : (insertIdx n x as)[m] = x
hx' : (insertIdx m x bs)[n] = x
ht : n < m
⊢ bs[n] ∈ bs

Tactic:
exact getElem_mem _

Result:
no goals

Proof state:
α : Type u_1
s : List α
hs : s.Nodup
⊢ s.permutations'.Nodup

Tactic:
induction' hs with x l h h' IH

Result:
case nil
α : Type u_1
s : List α
⊢ [].permutations'.Nodup

case cons
α : Type u_1
s : List α
x : α
l : List α
h : ∀ a' ∈ l, x ≠ a'
h' : Pairwise (fun x1 x2 => x1 ≠ x2) l
IH : l.permutations'.Nodup
⊢ (x :: l).permutations'.Nodup

Proof state:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ 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✝ : n < (permutations'Aux x as).length
hn' : insertIdx n x as = a
m : ℕ
hm✝ : m < (permutations'Aux x bs).length
hm' : insertIdx m x bs = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : (insertIdx n x as)[m] = x
⊢ (insertIdx m x bs)[n] = x

Tactic:
simp [hm', ← hn', hn]

Result:
no goals

Proof state:
case cons.right
α : Type u_1
s : List α
x : α
l : List α
h : ∀ a' ∈ l, x ≠ a'
h' : Pairwise (fun x1 x2 => x1 ≠ x2) l
IH : l.permutations'.Nodup
⊢ Pairwise (Disjoint on permutations'Aux x) l.permutations'

Tactic:
refine IH.pairwise_of_forall_ne fun as ha bs hb H => ?_

Result:
case cons.right
α : Type u_1
s : List α
x : α
l : List α
h : ∀ a' ∈ l, x ≠ a'
h' : Pairwise (fun x1 x2 => x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ∈ l.permutations'
bs : List α
hb : bs ∈ l.permutations'
H : as ≠ bs
⊢ (Disjoint on permutations'Aux x) as bs

Proof state:
case cons.right.intro.mk.intro.mk
α : Type u_1
s : List α
x : α
l : List α
h : ∀ 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 : n < (permutations'Aux x as).length
hn' : (permutations'Aux x as).get ⟨n, hn⟩ = a
m : ℕ
hm : m < (permutations'Aux x bs).length
hm' : (permutations'Aux x bs).get ⟨m, hm⟩ = a
⊢ False

Tactic:
have hl : as.length = bs.length := (ha.trans hb.symm).length_eq

Result:
case cons.right.intro.mk.intro.mk
α : Type u_1
s : List α
x : α
l : List α
h : ∀ 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 : n < (permutations'Aux x as).length
hn' : (permutations'Aux x as).get ⟨n, hn⟩ = a
m : ℕ
hm : m < (permutations'Aux x bs).length
hm' : (permutations'Aux x bs).get ⟨m, hm⟩ = a
hl : as.length = bs.length
⊢ False

Proof state:
case cons
α : Type u_1
s : List α
x : α
l : List α
h : ∀ a' ∈ l, x ≠ a'
h' : Pairwise (fun x1 x2 => x1 ≠ x2) l
IH : l.permutations'.Nodup
⊢ (x :: l).permutations'.Nodup

Tactic:
rw [permutations']

Result:
case cons
α : Type u_1
s : List α
x : α
l : List α
h : ∀ a' ∈ l, x ≠ a'
h' : Pairwise (fun x1 x2 => x1 ≠ x2) l
IH : l.permutations'.Nodup
⊢ (flatMap (permutations'Aux x) l.permutations').Nodup

Proof state:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ 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✝ : n < (permutations'Aux x as).length
hn' : insertIdx n x as = a
m : ℕ
hm✝ : m < (permutations'Aux x bs).length
hm' : insertIdx m x bs = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : (insertIdx n x as)[m] = x
hx' : (insertIdx m x bs)[n] = x
ht : n < m
this : x ∈ bs
⊢ False

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

Result:
no goals