no goals
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r✝ : α → α → Prop
a b : α
l : List α
r : α → α → Prop
hl : Nodup l
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
⊢ Pairwise r l
classical
  refine' pairwise_of_reflexive_on_dupl_of_forall_ne _ h
  intro x hx
  rw [nodup_iff_count_le_one] at hl
  exact absurd (hl x) hx.not_le
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r✝ : α → α → Prop
a b : α
l : List α
r : α → α → Prop
hl : Nodup l
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
⊢ ∀ (a : α), 1 < count a l → r a a
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r✝ : α → α → Prop
a b : α
l : List α
r : α → α → Prop
hl : Nodup l
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
⊢ Pairwise r l
refine' pairwise_of_reflexive_on_dupl_of_forall_ne _ h
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r✝ : α → α → Prop
a b : α
l : List α
r : α → α → Prop
hl : Nodup l
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
x : α
hx : 1 < count x l
⊢ r x x
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r✝ : α → α → Prop
a b : α
l : List α
r : α → α → Prop
hl : Nodup l
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
⊢ ∀ (a : α), 1 < count a l → r a a
intro x hx
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r✝ : α → α → Prop
a b : α
l : List α
r : α → α → Prop
hl✝ : Nodup l
hl : ∀ (a : α), count a l ≤ 1
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
x : α
hx : 1 < count x l
⊢ r x x
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r✝ : α → α → Prop
a b : α
l : List α
r : α → α → Prop
hl : Nodup l
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
x : α
hx : 1 < count x l
⊢ r x x
rw [nodup_iff_count_le_one] at hl
no goals
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r✝ : α → α → Prop
a b : α
l : List α
r : α → α → Prop
hl✝ : Nodup l
hl : ∀ (a : α), count a l ≤ 1
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → r a b
x : α
hx : 1 < count x l
⊢ r x x
exact absurd (hl x) hx.not_le