-- 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
α : 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
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:
rw [mem_permutations'] at ha hb

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

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

Tactic:
rw [(permutations_perm_permutations' s).nodup_iff]

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

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
as : List α
ha : as ∈ l.permutations'
bs : List α
hb : bs ∈ l.permutations'
H : as ≠ bs
⊢ (Disjoint on permutations'Aux x) as bs

Tactic:
rw [Function.onFun, disjoint_iff_ne]

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
⊢ ∀ a ∈ permutations'Aux x as, ∀ b ∈ permutations'Aux x bs, a ≠ b

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
ys : List α
hy : ys ~ l
⊢ (permutations'Aux x ys).Nodup

Tactic:
rw [nodup_permutations'Aux_iff, hy.mem_iff]

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
⊢ x ∉ l

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
⊢ as[m] ∈ as

Tactic:
exact getElem_mem _

Result:
no goals

Proof state:
case cons.right.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.permutations'
bs : List α
hb : bs ∈ l.permutations'
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
⊢ False

Tactic:
obtain ⟨⟨m, hm⟩, hm'⟩ := get_of_mem hb'

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.permutations'
bs : List α
hb : bs ∈ l.permutations'
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

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

Tactic:
have hx : (insertIdx n x as)[m]'(by
    rwa [length_insertIdx_of_le_length hn, Nat.lt_succ_iff, hl]) = x := by
  simp [hn', ← hm', hm]

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

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
ys : List α
hy : ys ∈ l.permutations'
⊢ (permutations'Aux x ys).Nodup

Tactic:
rw [mem_permutations'] at 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'Aux x ys).Nodup

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
hl : as.length = bs.length
⊢ False

Tactic:
simp only [Nat.lt_succ_iff, length_permutations'Aux] at hn hm

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
hn : n ≤ as.length
hm : m ≤ bs.length
⊢ False

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
ys : List α
hy : ys ~ l
⊢ x ∉ l

Tactic:
exact fun H => h x H rfl

Result:
no goals