α : Type u_1
β : Type ?u.120254
inst✝ : DecidableEq α
s : Finset α
⊢ Disjoint (image Quotient.mk' (Finset.diag s)) (image Quotient.mk' (offDiag s))
α : Type u_1
β : Type ?u.120254
inst✝ : DecidableEq α
s : Finset α
⊢ Finset.card (Finset.sym2 s) = Finset.card s * (Finset.card s + 1) / 2
rw [← image_diag_union_image_offDiag, card_union_eq, Sym2.card_image_diag,
  Sym2.card_image_offDiag, Nat.choose_two_right, add_comm, ← Nat.triangle_succ, Nat.succ_sub_one,
  mul_comm]
α : Type u_1
β : Type ?u.120254
inst✝ : DecidableEq α
s : Finset α
⊢ ∀ ⦃a : Quotient (Rel.setoid α)⦄, a ∈ image Quotient.mk' (Finset.diag s) → ¬a ∈ image Quotient.mk' (offDiag s)
α : Type u_1
β : Type ?u.120254
inst✝ : DecidableEq α
s : Finset α
⊢ Disjoint (image Quotient.mk' (Finset.diag s)) (image Quotient.mk' (offDiag s))
rw [disjoint_left]
α : Type u_1
β : Type ?u.120254
inst✝ : DecidableEq α
s : Finset α
m : Quotient (Rel.setoid α)
ha : m ∈ image Quotient.mk' (Finset.diag s)
hb : m ∈ image Quotient.mk' (offDiag s)
⊢ False
α : Type u_1
β : Type ?u.120254
inst✝ : DecidableEq α
s : Finset α
⊢ ∀ ⦃a : Quotient (Rel.setoid α)⦄, a ∈ image Quotient.mk' (Finset.diag s) → ¬a ∈ image Quotient.mk' (offDiag s)
rintro m ha hb
α : Type u_1
β : Type ?u.120254
inst✝ : DecidableEq α
s : Finset α
m : Quotient (Rel.setoid α)
ha : ∃ a, a ∈ Finset.diag s ∧ Quotient.mk' a = m
hb : ∃ a, a ∈ offDiag s ∧ Quotient.mk' a = m
⊢ False
α : Type u_1
β : Type ?u.120254
inst✝ : DecidableEq α
s : Finset α
m : Quotient (Rel.setoid α)
ha : m ∈ image Quotient.mk' (Finset.diag s)
hb : m ∈ image Quotient.mk' (offDiag s)
⊢ False
rw [mem_image] at ha hb
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.120254
inst✝ : DecidableEq α
s : Finset α
a : α × α
ha : a ∈ Finset.diag s
b : α × α
hb : b ∈ offDiag s
hab : Quotient.mk' b = Quotient.mk' a
⊢ False
α : Type u_1
β : Type ?u.120254
inst✝ : DecidableEq α
s : Finset α
m : Quotient (Rel.setoid α)
ha : ∃ a, a ∈ Finset.diag s ∧ Quotient.mk' a = m
hb : ∃ a, a ∈ offDiag s ∧ Quotient.mk' a = m
⊢ False
obtain ⟨⟨a, ha, rfl⟩, ⟨b, hb, hab⟩⟩ := ha, hb
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.120254
inst✝ : DecidableEq α
s : Finset α
a : α × α
ha : a ∈ Finset.diag s
b : α × α
hb : b ∈ offDiag s
hab : Quotient.mk' b = Quotient.mk' a
⊢ IsDiag (Quotient.mk (Rel.setoid α) b)
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.120254
inst✝ : DecidableEq α
s : Finset α
a : α × α
ha : a ∈ Finset.diag s
b : α × α
hb : b ∈ offDiag s
hab : Quotient.mk' b = Quotient.mk' a
⊢ False
refine' not_isDiag_mk'_of_mem_offDiag hb _
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.120254
inst✝ : DecidableEq α
s : Finset α
a : α × α
ha : a ∈ Finset.diag s
b : α × α
hb : b ∈ offDiag s
hab : Quotient.mk (Rel.setoid α) b = Quotient.mk (Rel.setoid α) a
⊢ IsDiag (Quotient.mk (Rel.setoid α) b)
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.120254
inst✝ : DecidableEq α
s : Finset α
a : α × α
ha : a ∈ Finset.diag s
b : α × α
hb : b ∈ offDiag s
hab : Quotient.mk' b = Quotient.mk' a
⊢ IsDiag (Quotient.mk (Rel.setoid α) b)
dsimp [Quotient.mk'] at hab
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.120254
inst✝ : DecidableEq α
s : Finset α
a : α × α
ha : a ∈ Finset.diag s
b : α × α
hb : b ∈ offDiag s
hab : Quotient.mk (Rel.setoid α) b = Quotient.mk (Rel.setoid α) a
⊢ IsDiag (Quotient.mk (Rel.setoid α) a)
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.120254
inst✝ : DecidableEq α
s : Finset α
a : α × α
ha : a ∈ Finset.diag s
b : α × α
hb : b ∈ offDiag s
hab : Quotient.mk (Rel.setoid α) b = Quotient.mk (Rel.setoid α) a
⊢ IsDiag (Quotient.mk (Rel.setoid α) b)
rw [hab]
no goals
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.120254
inst✝ : DecidableEq α
s : Finset α
a : α × α
ha : a ∈ Finset.diag s
b : α × α
hb : b ∈ offDiag s
hab : Quotient.mk (Rel.setoid α) b = Quotient.mk (Rel.setoid α) a
⊢ IsDiag (Quotient.mk (Rel.setoid α) a)
exact isDiag_mk'_of_mem_diag ha