case nil
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : IsSymm α r
hl✝ : Nodup l
hl : Nodup []
⊢ Set.Pairwise {a | a ∈ []} r ↔ Pairwise r []

case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b : α
inst✝ : IsSymm α r
hl✝ : Nodup l✝
a : α
l : List α
ih : Nodup l → (Set.Pairwise {a | a ∈ l} r ↔ Pairwise r l)
hl : Nodup (a :: l)
⊢ Set.Pairwise {a_1 | a_1 ∈ a :: l} r ↔ Pairwise r (a :: l)
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : IsSymm α r
hl : Nodup l
⊢ Set.Pairwise {a | a ∈ l} r ↔ Pairwise r l
induction' l with a l ih
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b : α
inst✝ : IsSymm α r
hl✝ : Nodup l✝
a : α
l : List α
ih : Nodup l → (Set.Pairwise {a | a ∈ l} r ↔ Pairwise r l)
hl : ¬a ∈ l ∧ Nodup l
⊢ Set.Pairwise {a_1 | a_1 ∈ a :: l} r ↔ Pairwise r (a :: l)
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b : α
inst✝ : IsSymm α r
hl✝ : Nodup l✝
a : α
l : List α
ih : Nodup l → (Set.Pairwise {a | a ∈ l} r ↔ Pairwise r l)
hl : Nodup (a :: l)
⊢ Set.Pairwise {a_1 | a_1 ∈ a :: l} r ↔ Pairwise r (a :: l)
rw [List.nodup_cons] at hl
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b : α
inst✝ : IsSymm α r
hl✝ : Nodup l✝
a : α
l : List α
ih : Nodup l → (Set.Pairwise {a | a ∈ l} r ↔ Pairwise r l)
hl : ¬a ∈ l ∧ Nodup l
this : ∀ (b : α), b ∈ l → (¬a = b → r a b ↔ r a b)
⊢ Set.Pairwise {a_1 | a_1 ∈ a :: l} r ↔ Pairwise r (a :: l)
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b : α
inst✝ : IsSymm α r
hl✝ : Nodup l✝
a : α
l : List α
ih : Nodup l → (Set.Pairwise {a | a ∈ l} r ↔ Pairwise r l)
hl : ¬a ∈ l ∧ Nodup l
⊢ Set.Pairwise {a_1 | a_1 ∈ a :: l} r ↔ Pairwise r (a :: l)
have : ∀ b ∈ l, ¬a = b → r a b ↔ r a b := fun b hb =>
  imp_iff_right (ne_of_mem_of_not_mem hb hl.1).symm
no goals
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a✝ b : α
inst✝ : IsSymm α r
hl✝ : Nodup l✝
a : α
l : List α
ih : Nodup l → (Set.Pairwise {a | a ∈ l} r ↔ Pairwise r l)
hl : ¬a ∈ l ∧ Nodup l
this : ∀ (b : α), b ∈ l → (¬a = b → r a b ↔ r a b)
⊢ Set.Pairwise {a_1 | a_1 ∈ a :: l} r ↔ Pairwise r (a :: l)
simp [Set.setOf_or, Set.pairwise_insert_of_symmetric (@symm_of _ r _), ih hl.2, and_comm,
  forall₂_congr this]
no goals
case nil
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a b : α
inst✝ : IsSymm α r
hl✝ : Nodup l
hl : Nodup []
⊢ Set.Pairwise {a | a ∈ []} r ↔ Pairwise r []
simp