-- 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.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

Tactic:
rw [← hx', getElem_insertIdx_of_lt ht]

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
⊢ bs[n] ∈ bs

Proof state:
case cons.right.intro.mk.intro.mk.inr.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:
simp only [ht] at hm' hn'

Result:
case cons.right.intro.mk.intro.mk.inr.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
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
hn' : insertIdx m x as = a
⊢ False

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' : 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
⊢ False

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

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
⊢ False

case cons.right.intro.mk.intro.mk.inr.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

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
⊢ False

Proof state:
case cons.right.intro.mk.intro.mk.inr.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
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
hn' : insertIdx m x as = insertIdx m x bs
⊢ False

Tactic:
exact H (insertIdx_injective _ _ hn')

Result:
no goals

Proof state:
case cons.right.intro.mk.intro.mk.inr.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
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
hn' : insertIdx m x as = a
⊢ False

Tactic:
rw [← hm'] at hn'

Result:
case cons.right.intro.mk.intro.mk.inr.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
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
hn' : insertIdx m x as = insertIdx m x bs
⊢ False

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 : m < n
this : x ∈ as
⊢ False

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

Result:
no goals