-- Mathlib/Data/List/Sym.lean
theorem Nodup.sym (n : ℕ) {xs : List α} (h : xs.Nodup) : (xs.sym n).Nodup :=
  match n, xs with
  | 0, _ => by simp [List.sym]
  | n + 1, [] => by simp [List.sym]
  | n + 1, x :: xs => by
    rw [List.sym]
    refine Nodup.append (Nodup.map ?inj (Nodup.sym n h)) (Nodup.sym (n + 1) h.of_cons) ?disj
    case inj =>
      intro z z'
      simp
    case disj =>
      intro z hz hz'
      rw [mem_map] at hz
      obtain ⟨z, _hz, rfl⟩ := hz
      have := first_mem_of_cons_mem_sym hz'
      simp only [nodup_cons, this, not_true_eq_false, false_and] at h

Proof state:
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ (map (fun p => x ::ₛ p) (List.sym n (x :: xs))).Disjoint (List.sym (n + 1) xs)

Tactic:
intro z hz hz'

Result:
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
z : Sym α (n + 1)
hz : z ∈ map (fun p => x ::ₛ p) (List.sym n (x :: xs))
hz' : z ∈ List.sym (n + 1) xs
⊢ False

Proof state:
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
z z' : Sym α n
⊢ (fun p => x ::ₛ p) z = (fun p => x ::ₛ p) z' → z = z'

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ Function.Injective fun p => x ::ₛ p

Tactic:
intro z z'

Result:
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
z z' : Sym α n
⊢ (fun p => x ::ₛ p) z = (fun p => x ::ₛ p) z' → z = z'

Proof state:
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
z : Sym α (n + 1)
hz : ∃ a ∈ List.sym n (x :: xs), x ::ₛ a = z
hz' : z ∈ List.sym (n + 1) xs
⊢ False

Tactic:
obtain ⟨z, _hz, rfl⟩ := hz

Result:
case intro.intro
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
z : Sym α n
_hz : z ∈ List.sym n (x :: xs)
hz' : x ::ₛ z ∈ List.sym (n + 1) xs
⊢ False

Proof state:
case intro.intro
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
z : Sym α n
_hz : z ∈ List.sym n (x :: xs)
hz' : x ::ₛ z ∈ List.sym (n + 1) xs
this : x ∈ xs
⊢ False

Tactic:
simp only [nodup_cons, this, not_true_eq_false, false_and] at h

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
xs x✝ : List α
h : x✝.Nodup
⊢ (List.sym 0 x✝).Nodup

Tactic:
simp [List.sym]

Result:
no goals

Proof state:
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
z : Sym α (n + 1)
hz : z ∈ map (fun p => x ::ₛ p) (List.sym n (x :: xs))
hz' : z ∈ List.sym (n + 1) xs
⊢ False

Tactic:
rw [mem_map] at hz

Result:
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
z : Sym α (n + 1)
hz : ∃ a ∈ List.sym n (x :: xs), x ::ₛ a = z
hz' : z ∈ List.sym (n + 1) xs
⊢ False

Proof state:
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ (map (fun p => x ::ₛ p) (List.sym n (x :: xs)) ++ List.sym (n + 1) xs).Nodup

Tactic:
refine Nodup.append (Nodup.map ?inj (Nodup.sym n h)) (Nodup.sym (n + 1) h.of_cons) ?disj

Result:
case inj
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ Function.Injective fun p => x ::ₛ p

case disj
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ (map (fun p => x ::ₛ p) (List.sym n (x :: xs))).Disjoint (List.sym (n + 1) xs)

Proof state:
case intro.intro
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
z : Sym α n
_hz : z ∈ List.sym n (x :: xs)
hz' : x ::ₛ z ∈ List.sym (n + 1) xs
⊢ False

Tactic:
have := first_mem_of_cons_mem_sym hz'

Result:
case intro.intro
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
z : Sym α n
_hz : z ∈ List.sym n (x :: xs)
hz' : x ::ₛ z ∈ List.sym (n + 1) xs
this : x ∈ xs
⊢ False

Proof state:
α : Type u_1
n✝ : ℕ
xs : List α
n : ℕ
h : [].Nodup
⊢ (List.sym (n + 1) []).Nodup

Tactic:
simp [List.sym]

Result:
no goals

Proof state:
case inj
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ Function.Injective fun p => x ::ₛ p

case disj
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ (map (fun p => x ::ₛ p) (List.sym n (x :: xs))).Disjoint (List.sym (n + 1) xs)

Tactic:
case inj =>
  intro z z'
  simp

Result:
case disj
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ (map (fun p => x ::ₛ p) (List.sym n (x :: xs))).Disjoint (List.sym (n + 1) xs)

Proof state:
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ (List.sym (n + 1) (x :: xs)).Nodup

Tactic:
rw [List.sym]

Result:
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ (map (fun p => x ::ₛ p) (List.sym n (x :: xs)) ++ List.sym (n + 1) xs).Nodup

Proof state:
case disj
α : Type u_1
n✝ : ℕ
xs✝ : List α
n : ℕ
x : α
xs : List α
h : (x :: xs).Nodup
⊢ (map (fun p => x ::ₛ p) (List.sym n (x :: xs))).Disjoint (List.sym (n + 1) xs)

Tactic:
case disj =>
  intro z hz hz'
  rw [mem_map] at hz
  obtain ⟨z, _hz, rfl⟩ := hz
  have := first_mem_of_cons_mem_sym hz'
  simp only [nodup_cons, this, not_true_eq_false, false_and] at h

Result:
no goals