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

Tactic:
rw [get_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' : 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

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
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
⊢ False

Tactic:
obtain ⟨⟨n, hn⟩, hn'⟩ := get_of_mem ha'

Result:
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

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

Tactic:
simp

Result:
no goals

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
⊢ (insertIdx n x as)[m] = x

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

Result:
no goals

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_1 ∈ l.permutations', (permutations'Aux x x_1).Nodup) ∧ Pairwise (Disjoint on permutations'Aux x) l.permutations'

Tactic:
constructor

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
⊢ ∀ x_1 ∈ l.permutations', (permutations'Aux x x_1).Nodup

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'

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

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

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
hx' : (insertIdx m x bs)[n] = x
⊢ False

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

Tactic:
suffices x ∈ as by exact h x (ha.subset this) rfl

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
⊢ x ∈ as

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

Tactic:
rintro a ha' b hb' rfl

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 : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux 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
⊢ m < (insertIdx n x as).length

Tactic:
rwa [length_insertIdx_of_le_length hn, Nat.lt_succ_iff, hl]

Result:
no goals

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
⊢ n < (insertIdx m x bs).length

Tactic:
rwa [length_insertIdx_of_le_length hm, Nat.lt_succ_iff, ← hl]

Result:
no goals