α : Type u_1
β : Type ?u.73737
inst✝ : DecidableEq α
s : Finset α
⊢ ∀ (a : α × α),
    Quotient.mk'' a ∈ image Quotient.mk' (offDiag s) →
      Finset.card (filter (fun x => Quotient.mk' x = Quotient.mk'' a) (offDiag s)) = 2
α : Type u_1
β : Type ?u.73737
inst✝ : DecidableEq α
s : Finset α
⊢ 2 * Finset.card (image Quotient.mk' (offDiag s)) = Finset.card (offDiag s)
rw [card_eq_sum_card_image (Quotient.mk' : α × α → _), sum_const_nat (Quotient.ind' _), mul_comm]
case mk
α : Type u_1
β : Type ?u.73737
inst✝ : DecidableEq α
s : Finset α
x y : α
hxy : Quotient.mk'' (x, y) ∈ image Quotient.mk' (offDiag s)
⊢ Finset.card (filter (fun x_1 => Quotient.mk' x_1 = Quotient.mk'' (x, y)) (offDiag s)) = 2
α : Type u_1
β : Type ?u.73737
inst✝ : DecidableEq α
s : Finset α
⊢ ∀ (a : α × α),
    Quotient.mk'' a ∈ image Quotient.mk' (offDiag s) →
      Finset.card (filter (fun x => Quotient.mk' x = Quotient.mk'' a) (offDiag s)) = 2
rintro ⟨x, y⟩ hxy
case mk
α : Type u_1
β : Type ?u.73737
inst✝ : DecidableEq α
s : Finset α
x y : α
hxy : ∃ a, (a.fst ∈ s ∧ a.snd ∈ s ∧ a.fst ≠ a.snd) ∧ Quotient.mk' a = Quotient.mk'' (x, y)
⊢ Finset.card (filter (fun x_1 => Quotient.mk' x_1 = Quotient.mk'' (x, y)) (offDiag s)) = 2
case mk
α : Type u_1
β : Type ?u.73737
inst✝ : DecidableEq α
s : Finset α
x y : α
hxy : Quotient.mk'' (x, y) ∈ image Quotient.mk' (offDiag s)
⊢ Finset.card (filter (fun x_1 => Quotient.mk' x_1 = Quotient.mk'' (x, y)) (offDiag s)) = 2
simp_rw [mem_image, mem_offDiag] at hxy
case mk.intro.intro.intro.intro
α : Type u_1
β : Type ?u.73737
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
h : Quotient.mk' a = Quotient.mk'' (x, y)
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
⊢ Finset.card (filter (fun x_1 => Quotient.mk' x_1 = Quotient.mk'' (x, y)) (offDiag s)) = 2
case mk
α : Type u_1
β : Type ?u.73737
inst✝ : DecidableEq α
s : Finset α
x y : α
hxy : ∃ a, (a.fst ∈ s ∧ a.snd ∈ s ∧ a.fst ≠ a.snd) ∧ Quotient.mk' a = Quotient.mk'' (x, y)
⊢ Finset.card (filter (fun x_1 => Quotient.mk' x_1 = Quotient.mk'' (x, y)) (offDiag s)) = 2
obtain ⟨a, ⟨ha₁, ha₂, ha⟩, h⟩ := hxy
case mk.intro.intro.intro.intro
α : Type u_1
β : Type ?u.73737
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
⊢ Finset.card (filter (fun x_1 => Quotient.mk' x_1 = Quotient.mk'' (x, y)) (offDiag s)) = 2
case mk.intro.intro.intro.intro
α : Type u_1
β : Type ?u.73737
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
h : Quotient.mk' a = Quotient.mk'' (x, y)
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
⊢ Finset.card (filter (fun x_1 => Quotient.mk' x_1 = Quotient.mk'' (x, y)) (offDiag s)) = 2
replace h := Quotient.eq.1 h
case mk.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.73737
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
⊢ Finset.card (filter (fun x_1 => Quotient.mk' x_1 = Quotient.mk'' (x, y)) (offDiag s)) = 2
case mk.intro.intro.intro.intro
α : Type u_1
β : Type ?u.73737
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
⊢ Finset.card (filter (fun x_1 => Quotient.mk' x_1 = Quotient.mk'' (x, y)) (offDiag s)) = 2
obtain ⟨hx, hy, hxy⟩ : x ∈ s ∧ y ∈ s ∧ x ≠ y := by
  cases h <;> refine' ⟨‹_›, ‹_›, _⟩ <;> [exact ha; exact ha.symm]
case mk.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.73737
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
⊢ Finset.card (filter (fun x_1 => Quotient.mk' x_1 = Quotient.mk'' (x, y)) (offDiag s)) = 2
case mk.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.73737
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
⊢ Finset.card (filter (fun x_1 => Quotient.mk' x_1 = Quotient.mk'' (x, y)) (offDiag s)) = 2
have hxy' : y ≠ x := hxy.symm
case mk.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.73737
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
this : filter (fun z => Quotient.mk (Rel.setoid α) z = Quotient.mk (Rel.setoid α) (x, y)) (offDiag s) = {(x, y), (y, x)}
⊢ Finset.card (filter (fun x_1 => Quotient.mk' x_1 = Quotient.mk'' (x, y)) (offDiag s)) = 2
case mk.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.73737
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
⊢ Finset.card (filter (fun x_1 => Quotient.mk' x_1 = Quotient.mk'' (x, y)) (offDiag s)) = 2
have : (s.offDiag.filter fun z => ⟦z⟧ = ⟦(x, y)⟧) = ({(x, y), (y, x)} : Finset _) := by
  ext ⟨x₁, y₁⟩
  rw [mem_filter, mem_insert, mem_singleton, Sym2.eq_iff, Prod.mk.inj_iff, Prod.mk.inj_iff,
    and_iff_right_iff_imp]
  rintro (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩) <;> rw [mem_offDiag] <;> exact ⟨‹_›, ‹_›, ‹_›⟩
case mk.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.73737
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
this : filter (fun z => Quotient.mk (Rel.setoid α) z = Quotient.mk (Rel.setoid α) (x, y)) (offDiag s) = {(x, y), (y, x)}
⊢ Finset.card (filter (fun x_1 => Quotient.mk (Rel.setoid α) x_1 = Quotient.mk (Rel.setoid α) (x, y)) (offDiag s)) = 2
case mk.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.73737
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
this : filter (fun z => Quotient.mk (Rel.setoid α) z = Quotient.mk (Rel.setoid α) (x, y)) (offDiag s) = {(x, y), (y, x)}
⊢ Finset.card (filter (fun x_1 => Quotient.mk' x_1 = Quotient.mk'' (x, y)) (offDiag s)) = 2
dsimp [Quotient.mk', Quotient.mk''_eq_mk]
case mk.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.73737
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
this : filter (fun z => Quotient.mk (Rel.setoid α) z = Quotient.mk (Rel.setoid α) (x, y)) (offDiag s) = {(x, y), (y, x)}
⊢ ¬(x, y) ∈ {(y, x)}
case mk.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.73737
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
this : filter (fun z => Quotient.mk (Rel.setoid α) z = Quotient.mk (Rel.setoid α) (x, y)) (offDiag s) = {(x, y), (y, x)}
⊢ Finset.card (filter (fun x_1 => Quotient.mk (Rel.setoid α) x_1 = Quotient.mk (Rel.setoid α) (x, y)) (offDiag s)) = 2
rw [this, card_insert_of_not_mem, card_singleton]
case mk.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.73737
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
this : filter (fun z => Quotient.mk (Rel.setoid α) z = Quotient.mk (Rel.setoid α) (x, y)) (offDiag s) = {(x, y), (y, x)}
⊢ x = y → ¬y = x
case mk.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.73737
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
this : filter (fun z => Quotient.mk (Rel.setoid α) z = Quotient.mk (Rel.setoid α) (x, y)) (offDiag s) = {(x, y), (y, x)}
⊢ ¬(x, y) ∈ {(y, x)}
simp only [not_and, Prod.mk.inj_iff, mem_singleton]
no goals
case mk.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.73737
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
this : filter (fun z => Quotient.mk (Rel.setoid α) z = Quotient.mk (Rel.setoid α) (x, y)) (offDiag s) = {(x, y), (y, x)}
⊢ x = y → ¬y = x
exact fun _ => hxy'
no goals
α : Type u_1
β : Type ?u.73737
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
⊢ x ∈ s ∧ y ∈ s ∧ x ≠ y
cases h <;> refine' ⟨‹_›, ‹_›, _⟩ <;> [exact ha; exact ha.symm]
case a.mk
α : Type u_1
β : Type ?u.73737
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
x₁ y₁ : α
⊢ (x₁, y₁) ∈ filter (fun z => Quotient.mk (Rel.setoid α) z = Quotient.mk (Rel.setoid α) (x, y)) (offDiag s) ↔
    (x₁, y₁) ∈ {(x, y), (y, x)}
α : Type u_1
β : Type ?u.73737
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
⊢ filter (fun z => Quotient.mk (Rel.setoid α) z = Quotient.mk (Rel.setoid α) (x, y)) (offDiag s) = {(x, y), (y, x)}
ext ⟨x₁, y₁⟩
case a.mk
α : Type u_1
β : Type ?u.73737
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
x₁ y₁ : α
⊢ x₁ = x ∧ y₁ = y ∨ x₁ = y ∧ y₁ = x → (x₁, y₁) ∈ offDiag s
case a.mk
α : Type u_1
β : Type ?u.73737
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
x₁ y₁ : α
⊢ (x₁, y₁) ∈ filter (fun z => Quotient.mk (Rel.setoid α) z = Quotient.mk (Rel.setoid α) (x, y)) (offDiag s) ↔
    (x₁, y₁) ∈ {(x, y), (y, x)}
rw [mem_filter, mem_insert, mem_singleton, Sym2.eq_iff, Prod.mk.inj_iff, Prod.mk.inj_iff,
  and_iff_right_iff_imp]
no goals
case a.mk
α : Type u_1
β : Type ?u.73737
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
h : a ≈ (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
x₁ y₁ : α
⊢ x₁ = x ∧ y₁ = y ∨ x₁ = y ∧ y₁ = x → (x₁, y₁) ∈ offDiag s
rintro (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩) <;> rw [mem_offDiag] <;> exact ⟨‹_›, ‹_›, ‹_›⟩