α : Type u_1
β : Type u_2
γ : Type ?u.549294
s : Finset α
a : α
ha : ¬a ∈ s
r : β → β → Prop
f : α → β
⊢ Set.Pairwise (↑s) (r on f) →
    ((∀ (b : α), b ∈ s → a ≠ b → (r on f) a b ∧ (r on f) b a) ↔ ∀ (b : α), b ∈ s → r (f a) (f b) ∧ r (f b) (f a))
α : Type u_1
β : Type u_2
γ : Type ?u.549294
s : Finset α
a : α
ha : ¬a ∈ s
r : β → β → Prop
f : α → β
⊢ _root_.Pairwise (r on fun a_1 => f ↑a_1) ↔
    _root_.Pairwise (r on fun a => f ↑a) ∧ ∀ (b : α), b ∈ s → r (f a) (f b) ∧ r (f b) (f a)
simp only [pairwise_subtype_iff_pairwise_finset', Finset.coe_cons, Set.pairwise_insert,
  Finset.mem_coe, and_congr_right_iff]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.549294
s : Finset α
a : α
ha : ¬a ∈ s
r : β → β → Prop
f : α → β
⊢ Set.Pairwise (↑s) (r on f) →
    ((∀ (b : α), b ∈ s → a ≠ b → (r on f) a b ∧ (r on f) b a) ↔ ∀ (b : α), b ∈ s → r (f a) (f b) ∧ r (f b) (f a))
exact fun _ =>
  ⟨fun h b hb =>
    h b hb <| by
      rintro rfl
      contradiction,
    fun h b hb _ => h b hb⟩
α : Type u_1
β : Type u_2
γ : Type ?u.549294
s : Finset α
a : α
ha : ¬a ∈ s
r : β → β → Prop
f : α → β
x✝ : Set.Pairwise (↑s) (r on f)
h : ∀ (b : α), b ∈ s → a ≠ b → (r on f) a b ∧ (r on f) b a
hb : a ∈ s
⊢ False
α : Type u_1
β : Type u_2
γ : Type ?u.549294
s : Finset α
a : α
ha : ¬a ∈ s
r : β → β → Prop
f : α → β
x✝ : Set.Pairwise (↑s) (r on f)
h : ∀ (b : α), b ∈ s → a ≠ b → (r on f) a b ∧ (r on f) b a
b : α
hb : b ∈ s
⊢ a ≠ b
rintro rfl
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.549294
s : Finset α
a : α
ha : ¬a ∈ s
r : β → β → Prop
f : α → β
x✝ : Set.Pairwise (↑s) (r on f)
h : ∀ (b : α), b ∈ s → a ≠ b → (r on f) a b ∧ (r on f) b a
hb : a ∈ s
⊢ False
contradiction