α : Type u_1
l : List α
hl : Nodup l
⊢ (∃ x y _h, x ∈ ↑l ∧ y ∈ ↑l) ↔ 2 ≤ List.length l
α : Type u_1
l : List α
hl : Nodup l
⊢ Nontrivial ↑l ↔ 2 ≤ List.length l
rw [Nontrivial]
case nil
α : Type u_1
hl : Nodup []
⊢ (∃ x y _h, x ∈ ↑[] ∧ y ∈ ↑[]) ↔ 2 ≤ List.length []

case cons.nil
α : Type u_1
hd : α
hl : Nodup [hd]
⊢ (∃ x y _h, x ∈ ↑[hd] ∧ y ∈ ↑[hd]) ↔ 2 ≤ List.length [hd]

case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : Nodup (hd :: hd' :: tl)
⊢ (∃ x y _h, x ∈ ↑(hd :: hd' :: tl) ∧ y ∈ ↑(hd :: hd' :: tl)) ↔ 2 ≤ List.length (hd :: hd' :: tl)
α : Type u_1
l : List α
hl : Nodup l
⊢ (∃ x y _h, x ∈ ↑l ∧ y ∈ ↑l) ↔ 2 ≤ List.length l
rcases l with (_ | ⟨hd, _ | ⟨hd', tl⟩⟩)
no goals
case nil
α : Type u_1
hl : Nodup []
⊢ (∃ x y _h, x ∈ ↑[] ∧ y ∈ ↑[]) ↔ 2 ≤ List.length []
simp
no goals
case cons.nil
α : Type u_1
hd : α
hl : Nodup [hd]
⊢ (∃ x y _h, x ∈ ↑[hd] ∧ y ∈ ↑[hd]) ↔ 2 ≤ List.length [hd]
simp
case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : Nodup (hd :: hd' :: tl)
⊢ ∃ x y, ¬x = y ∧ (x = hd ∨ x = hd' ∨ x ∈ tl) ∧ (y = hd ∨ y = hd' ∨ y ∈ tl)
case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : Nodup (hd :: hd' :: tl)
⊢ (∃ x y _h, x ∈ ↑(hd :: hd' :: tl) ∧ y ∈ ↑(hd :: hd' :: tl)) ↔ 2 ≤ List.length (hd :: hd' :: tl)
simp only [mem_cons, exists_prop, mem_coe_iff, List.length, Ne.def, Nat.succ_le_succ_iff,
  zero_le, iff_true_iff]
case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : Nodup (hd :: hd' :: tl)
⊢ ¬hd = hd'
case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : Nodup (hd :: hd' :: tl)
⊢ ∃ x y, ¬x = y ∧ (x = hd ∨ x = hd' ∨ x ∈ tl) ∧ (y = hd ∨ y = hd' ∨ y ∈ tl)
refine' ⟨hd, hd', _, by simp⟩
case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : (¬hd = hd' ∧ ¬hd ∈ tl) ∧ ¬hd' ∈ tl ∧ Nodup tl
⊢ ¬hd = hd'
case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : Nodup (hd :: hd' :: tl)
⊢ ¬hd = hd'
simp only [not_or, mem_cons, nodup_cons] at hl
no goals
case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : (¬hd = hd' ∧ ¬hd ∈ tl) ∧ ¬hd' ∈ tl ∧ Nodup tl
⊢ ¬hd = hd'
exact hl.left.left
no goals
α : Type u_1
hd hd' : α
tl : List α
hl : Nodup (hd :: hd' :: tl)
⊢ (hd = hd ∨ hd = hd' ∨ hd ∈ tl) ∧ (hd' = hd ∨ hd' = hd' ∨ hd' ∈ tl)
simp