no goals
α : Type u_1
β : Type ?u.44018
R S T : α → α → Prop
a : α
l✝ l : List α
r : α → α → Prop
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → r a b
⊢ Pairwise r l
classical
  refine'
    pairwise_of_reflexive_on_dupl_of_forall_ne (fun a ha' => _) fun a ha b hb _ => h a ha b hb
  have ha := List.one_le_count_iff_mem.1 ha'.le
  exact h a ha a ha
α : Type u_1
β : Type ?u.44018
R S T : α → α → Prop
a✝ : α
l✝ l : List α
r : α → α → Prop
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → r a b
a : α
ha' : 1 < count a l
⊢ r a a
α : Type u_1
β : Type ?u.44018
R S T : α → α → Prop
a : α
l✝ l : List α
r : α → α → Prop
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → r a b
⊢ Pairwise r l
refine'
  pairwise_of_reflexive_on_dupl_of_forall_ne (fun a ha' => _) fun a ha b hb _ => h a ha b hb
α : Type u_1
β : Type ?u.44018
R S T : α → α → Prop
a✝ : α
l✝ l : List α
r : α → α → Prop
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → r a b
a : α
ha' : 1 < count a l
ha : a ∈ l
⊢ r a a
α : Type u_1
β : Type ?u.44018
R S T : α → α → Prop
a✝ : α
l✝ l : List α
r : α → α → Prop
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → r a b
a : α
ha' : 1 < count a l
⊢ r a a
have ha := List.one_le_count_iff_mem.1 ha'.le
no goals
α : Type u_1
β : Type ?u.44018
R S T : α → α → Prop
a✝ : α
l✝ l : List α
r : α → α → Prop
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → r a b
a : α
ha' : 1 < count a l
ha : a ∈ l
⊢ r a a
exact h a ha a ha