case h.e'_2
α : Type u_1
β : Type ?u.100368
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Fintype.card { a // ¬IsDiag a } = Finset.card (image Quotient.mk' (offDiag univ))
α : Type u_1
β : Type ?u.100368
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Fintype.card { a // ¬IsDiag a } = Nat.choose (Fintype.card α) 2
convert card_image_offDiag (univ : Finset α)
case h.e'_2
α : Type u_1
β : Type ?u.100368
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Fintype.card { a // ¬IsDiag a } = Finset.card (image (fun a => Quotient.mk'' a) (offDiag univ))
case h.e'_2
α : Type u_1
β : Type ?u.100368
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Fintype.card { a // ¬IsDiag a } = Finset.card (image Quotient.mk' (offDiag univ))
simp_rw [Quotient.mk', ← Quotient.mk''_eq_mk]
case h.e'_2.H
α : Type u_1
β : Type ?u.100368
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ ∀ (x : Sym2 α), x ∈ filter (fun a => ¬IsDiag a) (image Quotient.mk'' (univ ×ˢ univ)) ↔ ¬IsDiag x
case h.e'_2
α : Type u_1
β : Type ?u.100368
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Fintype.card { a // ¬IsDiag a } = Finset.card (image (fun a => Quotient.mk'' a) (offDiag univ))
rw [Fintype.card_of_subtype, ← filter_image_quotient_mk''_not_isDiag]
case h.e'_2.H
α : Type u_1
β : Type ?u.100368
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
⊢ x ∈ filter (fun a => ¬IsDiag a) (image Quotient.mk'' (univ ×ˢ univ)) ↔ ¬IsDiag x
case h.e'_2.H
α : Type u_1
β : Type ?u.100368
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ ∀ (x : Sym2 α), x ∈ filter (fun a => ¬IsDiag a) (image Quotient.mk'' (univ ×ˢ univ)) ↔ ¬IsDiag x
rintro x
case h.e'_2.H
α : Type u_1
β : Type ?u.100368
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
⊢ (∃ a, a ∈ univ ∧ Quotient.mk'' a = x) ∧ ¬IsDiag x ↔ ¬IsDiag x
case h.e'_2.H
α : Type u_1
β : Type ?u.100368
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
⊢ x ∈ filter (fun a => ¬IsDiag a) (image Quotient.mk'' (univ ×ˢ univ)) ↔ ¬IsDiag x
rw [mem_filter, univ_product_univ, mem_image]
case h.e'_2.H.intro
α : Type u_1
β : Type ?u.100368
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
a : α × α
ha : Quotient.mk (Rel.setoid α) a = x
⊢ (∃ a, a ∈ univ ∧ Quotient.mk'' a = x) ∧ ¬IsDiag x ↔ ¬IsDiag x
case h.e'_2.H
α : Type u_1
β : Type ?u.100368
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
⊢ (∃ a, a ∈ univ ∧ Quotient.mk'' a = x) ∧ ¬IsDiag x ↔ ¬IsDiag x
obtain ⟨a, ha⟩ := Quotient.exists_rep x
no goals
case h.e'_2.H.intro
α : Type u_1
β : Type ?u.100368
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
a : α × α
ha : Quotient.mk (Rel.setoid α) a = x
⊢ (∃ a, a ∈ univ ∧ Quotient.mk'' a = x) ∧ ¬IsDiag x ↔ ¬IsDiag x
exact and_iff_right ⟨a, mem_univ _, ha⟩