-- Mathlib/Data/List/Sym.lean
theorem Nodup.sym2 {xs : List α} (h : xs.Nodup) : xs.sym2.Nodup

Proof state:
case notmem
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
⊢ (fun y => s(x, y)) x ∉ map (fun y => s(x, y)) xs

case inj
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
⊢ Function.Injective fun y => s(x, y)

Tactic:
case notmem =>
  intro h'
  simp only [h.1, mem_map, Sym2.eq_iff, true_and, or_self, exists_eq_right] at h'

Result:
case inj
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
⊢ Function.Injective fun y => s(x, y)

Proof state:
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
⊢ (map (fun y => s(x, y)) (x :: xs)).Disjoint xs.sym2

Tactic:
intro z hz hz'

Result:
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
z : Sym2 α
hz : z ∈ map (fun y => s(x, y)) (x :: xs)
hz' : z ∈ xs.sym2
⊢ False

Proof state:
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
z : Sym2 α
hz : z ∈ map (fun y => s(x, y)) (x :: xs)
hz' : z ∈ xs.sym2
⊢ False

Tactic:
simp only [mem_cons, mem_map] at hz

Result:
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
z : Sym2 α
hz' : z ∈ xs.sym2
hz : ∃ a, (a = x ∨ a ∈ xs) ∧ s(x, a) = z
⊢ False

Proof state:
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
a b : α
⊢ (fun y => s(x, y)) a = (fun y => s(x, y)) b → a = b

Tactic:
simp only [Sym2.eq_iff, true_and]

Result:
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
a b : α
⊢ a = b ∨ x = b ∧ a = x → a = b

Proof state:
α : Type u_1
xs : List α
h : xs.Nodup
⊢ xs.sym2.Nodup

Tactic:
induction xs with
| nil => simp only [List.sym2, nodup_nil]
| cons x xs ih =>
  rw [List.sym2]
  specialize ih h.of_cons
  rw [nodup_cons] at h
  refine Nodup.append (Nodup.cons ?notmem (h.2.map ?inj)) ih ?disj
  case disj =>
    intro z hz hz'
    simp only [mem_cons, mem_map] at hz
    obtain ⟨_, (rfl | _), rfl⟩ := hz
      <;> simp [left_mem_of_mk_mem_sym2 hz'] at h
  case notmem =>
    intro h'
    simp only [h.1, mem_map, Sym2.eq_iff, true_and, or_self, exists_eq_right] at h'
  case inj =>
    intro a b
    simp only [Sym2.eq_iff, true_and]
    rintro (rfl | ⟨rfl, rfl⟩) <;> rfl

Result:
no goals

Proof state:
case notmem
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
⊢ (fun y => s(x, y)) x ∉ map (fun y => s(x, y)) xs

case inj
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
⊢ Function.Injective fun y => s(x, y)

case disj
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
⊢ (map (fun y => s(x, y)) (x :: xs)).Disjoint xs.sym2

Tactic:
case disj =>
  intro z hz hz'
  simp only [mem_cons, mem_map] at hz
  obtain ⟨_, (rfl | _), rfl⟩ := hz
    <;> simp [left_mem_of_mk_mem_sym2 hz'] at h

Result:
case notmem
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
⊢ (fun y => s(x, y)) x ∉ map (fun y => s(x, y)) xs

case inj
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
⊢ Function.Injective fun y => s(x, y)

Proof state:
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
z : Sym2 α
hz' : z ∈ xs.sym2
hz : ∃ a, (a = x ∨ a ∈ xs) ∧ s(x, a) = z
⊢ False

Tactic:
obtain ⟨_, (rfl | _), rfl⟩ := hz
  <;> simp [left_mem_of_mk_mem_sym2 hz'] at h

Result:
no goals

Proof state:
case cons
α : Type u_1
x : α
xs : List α
ih : xs.Nodup → xs.sym2.Nodup
h : (x :: xs).Nodup
⊢ (map (fun y => s(x, y)) (x :: xs) ++ xs.sym2).Nodup

Tactic:
specialize ih h.of_cons

Result:
case cons
α : Type u_1
x : α
xs : List α
h : (x :: xs).Nodup
ih : xs.sym2.Nodup
⊢ (map (fun y => s(x, y)) (x :: xs) ++ xs.sym2).Nodup

Proof state:
case nil
α : Type u_1
h : [].Nodup
⊢ [].sym2.Nodup

Tactic:
simp only [List.sym2, nodup_nil]

Result:
no goals

Proof state:
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
h' : (fun y => s(x, y)) x ∈ map (fun y => s(x, y)) xs
⊢ False

Tactic:
simp only [h.1, mem_map, Sym2.eq_iff, true_and, or_self, exists_eq_right] at h'

Result:
no goals

Proof state:
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
⊢ (fun y => s(x, y)) x ∉ map (fun y => s(x, y)) xs

Tactic:
intro h'

Result:
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
h' : (fun y => s(x, y)) x ∈ map (fun y => s(x, y)) xs
⊢ False

Proof state:
case cons
α : Type u_1
x : α
xs : List α
ih : xs.Nodup → xs.sym2.Nodup
h : (x :: xs).Nodup
⊢ (x :: xs).sym2.Nodup

Tactic:
rw [List.sym2]

Result:
case cons
α : Type u_1
x : α
xs : List α
ih : xs.Nodup → xs.sym2.Nodup
h : (x :: xs).Nodup
⊢ (map (fun y => s(x, y)) (x :: xs) ++ xs.sym2).Nodup

Proof state:
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
⊢ Function.Injective fun y => s(x, y)

Tactic:
intro a b

Result:
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
a b : α
⊢ (fun y => s(x, y)) a = (fun y => s(x, y)) b → a = b

Proof state:
case cons
α : Type u_1
x : α
xs : List α
h : (x :: xs).Nodup
ih : xs.sym2.Nodup
⊢ (map (fun y => s(x, y)) (x :: xs) ++ xs.sym2).Nodup

Tactic:
rw [nodup_cons] at h

Result:
case cons
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
⊢ (map (fun y => s(x, y)) (x :: xs) ++ xs.sym2).Nodup

Proof state:
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
a b : α
⊢ a = b ∨ x = b ∧ a = x → a = b

Tactic:
rintro (rfl | ⟨rfl, rfl⟩) <;> rfl

Result:
no goals

Proof state:
case inj
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
⊢ Function.Injective fun y => s(x, y)

Tactic:
case inj =>
  intro a b
  simp only [Sym2.eq_iff, true_and]
  rintro (rfl | ⟨rfl, rfl⟩) <;> rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
⊢ (map (fun y => s(x, y)) (x :: xs) ++ xs.sym2).Nodup

Tactic:
refine Nodup.append (Nodup.cons ?notmem (h.2.map ?inj)) ih ?disj

Result:
case notmem
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
⊢ (fun y => s(x, y)) x ∉ map (fun y => s(x, y)) xs

case inj
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
⊢ Function.Injective fun y => s(x, y)

case disj
α : Type u_1
x : α
xs : List α
h : x ∉ xs ∧ xs.Nodup
ih : xs.sym2.Nodup
⊢ (map (fun y => s(x, y)) (x :: xs)).Disjoint xs.sym2