[GOAL]
α : Type u_1
β : Type u_2
n✝ n k : ℕ
s : { s // 0 ∈ s }
⊢ (fun s => { val := 0 ::ₛ s, property := (_ : 0 ∈ 0 ::ₛ s) }) ((fun s => erase (↑s) 0 (_ : 0 ∈ ↑s)) s) = s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
n✝ n k : ℕ
s : Sym (Fin (succ n)) k
⊢ (fun s => erase (↑s) 0 (_ : 0 ∈ ↑s)) ((fun s => { val := 0 ::ₛ s, property := (_ : 0 ∈ 0 ::ₛ s) }) s) = s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
n✝ n k : ℕ
s : { s // ¬0 ∈ s }
⊢ (fun s => { val := map (Fin.succAbove 0) s, property := (_ : ¬0 ∈ map (Fin.succAbove 0) s) })
      ((fun s => map (Fin.predAbove 0) ↑s) s) =
    s
[PROOFSTEP]
ext1
[GOAL]
case a
α : Type u_1
β : Type u_2
n✝ n k : ℕ
s : { s // ¬0 ∈ s }
⊢ ↑((fun s => { val := map (Fin.succAbove 0) s, property := (_ : ¬0 ∈ map (Fin.succAbove 0) s) })
        ((fun s => map (Fin.predAbove 0) ↑s) s)) =
    ↑s
[PROOFSTEP]
simp only [map_map]
[GOAL]
case a
α : Type u_1
β : Type u_2
n✝ n k : ℕ
s : { s // ¬0 ∈ s }
⊢ map (Fin.succAbove 0 ∘ Fin.predAbove 0) ↑s = ↑s
[PROOFSTEP]
refine (Sym.map_congr fun v hv ↦ ?_).trans (map_id' _)
[GOAL]
case a
α : Type u_1
β : Type u_2
n✝ n k : ℕ
s : { s // ¬0 ∈ s }
v : Fin (succ n + 1)
hv : v ∈ ↑s
⊢ (Fin.succAbove 0 ∘ Fin.predAbove 0) v = v
[PROOFSTEP]
exact Fin.succAbove_predAbove (ne_of_mem_of_not_mem hv s.2)
[GOAL]
α : Type u_1
β : Type u_2
n✝ n k : ℕ
s : Sym (Fin (succ n)) k
⊢ (fun s => map (Fin.predAbove 0) ↑s)
      ((fun s => { val := map (Fin.succAbove 0) s, property := (_ : ¬0 ∈ map (Fin.succAbove 0) s) }) s) =
    s
[PROOFSTEP]
simp only [map_map, comp_apply, ← Fin.castSucc_zero, Fin.predAbove_succAbove, map_id']
[GOAL]
α : Type u_1
β : Type u_2
n✝ n : ℕ
⊢ Fintype.card (Sym (Fin n) 0) = multichoose n 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
n k : ℕ
⊢ Fintype.card (Sym (Fin 0) (k + 1)) = multichoose 0 (k + 1)
[PROOFSTEP]
rw [multichoose_zero_succ]
[GOAL]
α : Type u_1
β : Type u_2
n k : ℕ
⊢ Fintype.card (Sym (Fin 0) (k + 1)) = 0
[PROOFSTEP]
exact card_eq_zero
[GOAL]
α : Type u_1
β : Type u_2
n k : ℕ
⊢ Fintype.card (Sym (Fin 1) (k + 1)) = multichoose 1 (k + 1)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
n✝ n k : ℕ
⊢ Fintype.card (Sym (Fin (n + 2)) (k + 1)) = multichoose (n + 2) (k + 1)
[PROOFSTEP]
rw [multichoose_succ_succ, ← card_sym_fin_eq_multichoose (n + 1) (k + 1), ← card_sym_fin_eq_multichoose (n + 2) k,
  add_comm (Fintype.card _), ← card_sum]
[GOAL]
α : Type u_1
β : Type u_2
n✝ n k : ℕ
⊢ Fintype.card (Sym (Fin (n + 2)) (k + 1)) = Fintype.card (Sym (Fin (n + 2)) k ⊕ Sym (Fin (n + 1)) (k + 1))
[PROOFSTEP]
refine Fintype.card_congr (Equiv.symm ?_)
[GOAL]
α : Type u_1
β : Type u_2
n✝ n k : ℕ
⊢ Sym (Fin (n + 2)) k ⊕ Sym (Fin (n + 1)) (k + 1) ≃ Sym (Fin (n + 2)) (k + 1)
[PROOFSTEP]
apply (Sym.e1.symm.sumCongr Sym.e2.symm).trans
[GOAL]
α : Type u_1
β : Type u_2
n✝ n k : ℕ
⊢ { s // 0 ∈ s } ⊕ { s // ¬0 ∈ s } ≃ Sym (Fin (n + 2)) (k + 1)
[PROOFSTEP]
apply Equiv.sumCompl
[GOAL]
α✝ : Type u_1
β : Type u_2
n : ℕ
α : Type u_3
k : ℕ
inst✝¹ : Fintype α
inst✝ : Fintype (Sym α k)
⊢ Fintype.card (Sym α k) = multichoose (Fintype.card α) k
[PROOFSTEP]
rw [← card_sym_fin_eq_multichoose]
[GOAL]
α✝ : Type u_1
β : Type u_2
n : ℕ
α : Type u_3
k : ℕ
inst✝¹ : Fintype α
inst✝ : Fintype (Sym α k)
⊢ Fintype.card (Sym α k) = Fintype.card (Sym (Fin (Fintype.card α)) k)
[PROOFSTEP]
exact card_congr (equivCongr (equivFin α))
[GOAL]
α✝ : Type u_1
β : Type u_2
n : ℕ
α : Type u_3
inst✝¹ : Fintype α
k : ℕ
inst✝ : Fintype (Sym α k)
⊢ Fintype.card (Sym α k) = Nat.choose (Fintype.card α + k - 1) k
[PROOFSTEP]
rw [card_sym_eq_multichoose, Nat.multichoose_eq]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
⊢ Finset.card (image Quotient.mk' (Finset.diag s)) = Finset.card s
[PROOFSTEP]
rw [card_image_of_injOn, diag_card]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
⊢ Set.InjOn Quotient.mk' ↑(Finset.diag s)
[PROOFSTEP]
rintro ⟨x₀, x₁⟩ hx _ _ h
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x₀ x₁ : α
hx : (x₀, x₁) ∈ ↑(Finset.diag s)
x₂✝ : α × α
a✝ : x₂✝ ∈ ↑(Finset.diag s)
h : Quotient.mk' (x₀, x₁) = Quotient.mk' x₂✝
⊢ (x₀, x₁) = x₂✝
[PROOFSTEP]
cases Quotient.eq'.1 h
[GOAL]
case mk.refl
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x₀ x₁ : α
hx a✝ : (x₀, x₁) ∈ ↑(Finset.diag s)
h : Quotient.mk' (x₀, x₁) = Quotient.mk' (x₀, x₁)
⊢ (x₀, x₁) = (x₀, x₁)
[PROOFSTEP]
rfl
[GOAL]
case mk.swap
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x₀ x₁ : α
hx : (x₀, x₁) ∈ ↑(Finset.diag s)
a✝ : (x₁, x₀) ∈ ↑(Finset.diag s)
h : Quotient.mk' (x₀, x₁) = Quotient.mk' (x₁, x₀)
⊢ (x₀, x₁) = (x₁, x₀)
[PROOFSTEP]
simp only [mem_coe, mem_diag] at hx 
[GOAL]
case mk.swap
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x₀ x₁ : α
a✝ : (x₁, x₀) ∈ ↑(Finset.diag s)
h : Quotient.mk' (x₀, x₁) = Quotient.mk' (x₁, x₀)
hx : x₀ ∈ s ∧ x₀ = x₁
⊢ (x₀, x₁) = (x₁, x₀)
[PROOFSTEP]
rw [hx.2]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
⊢ 2 * Finset.card (image Quotient.mk' (offDiag s)) = Finset.card (offDiag s)
[PROOFSTEP]
rw [card_eq_sum_card_image (Quotient.mk' : α × α → _), sum_const_nat (Quotient.ind' _), mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rintro ⟨x, y⟩ hxy
[GOAL]
case mk
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
simp_rw [mem_image, mem_offDiag] at hxy 
[GOAL]
case mk
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
obtain ⟨a, ⟨ha₁, ha₂, ha⟩, h⟩ := hxy
[GOAL]
case mk.intro.intro.intro.intro
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
replace h := Quotient.eq.1 h
[GOAL]
case mk.intro.intro.intro.intro
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
obtain ⟨hx, hy, hxy⟩ : x ∈ s ∧ y ∈ s ∧ x ≠ y := by cases h <;> refine' ⟨‹_›, ‹_›, _⟩ <;> [exact ha; exact ha.symm]
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
cases h <;> refine' ⟨‹_›, ‹_›, _⟩ <;> [exact ha; exact ha.symm]
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
cases h
[GOAL]
case refl
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x y : α
ha₁ : (x, y).fst ∈ s
ha₂ : (x, y).snd ∈ s
ha : (x, y).fst ≠ (x, y).snd
⊢ x ∈ s ∧ y ∈ s ∧ x ≠ y
[PROOFSTEP]
refine' ⟨‹_›, ‹_›, _⟩
[GOAL]
case swap
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x y : α
ha₁ : (y, x).fst ∈ s
ha₂ : (y, x).snd ∈ s
ha : (y, x).fst ≠ (y, x).snd
⊢ x ∈ s ∧ y ∈ s ∧ x ≠ y
[PROOFSTEP]
refine' ⟨‹_›, ‹_›, _⟩
[GOAL]
case refl
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x y : α
ha₁ : (x, y).fst ∈ s
ha₂ : (x, y).snd ∈ s
ha : (x, y).fst ≠ (x, y).snd
⊢ x ≠ y
[PROOFSTEP]
exact ha
[GOAL]
case swap
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
x y : α
ha₁ : (y, x).fst ∈ s
ha₂ : (y, x).snd ∈ s
ha : (y, x).fst ≠ (y, x).snd
⊢ x ≠ y
[PROOFSTEP]
exact ha.symm
[GOAL]
case mk.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
have hxy' : y ≠ x := hxy.symm
[GOAL]
case mk.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
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]
    -- `hxy'` is used in `exact`
  rintro (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩) <;> rw [mem_offDiag] <;> exact ⟨‹_›, ‹_›, ‹_›⟩
[GOAL]
α : Type u_1
β : Type u_2
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)}
[PROOFSTEP]
ext ⟨x₁, y₁⟩
[GOAL]
case a.mk
α : Type u_1
β : Type u_2
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)}
[PROOFSTEP]
rw [mem_filter, mem_insert, mem_singleton, Sym2.eq_iff, Prod.mk.inj_iff, Prod.mk.inj_iff, and_iff_right_iff_imp]
  -- `hxy'` is used in `exact`
[GOAL]
case a.mk
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rintro (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)
[GOAL]
case a.mk.inl.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
x₁ y₁ : α
hx : x₁ ∈ s
hy : y₁ ∈ s
h : a ≈ (x₁, y₁)
hxy : x₁ ≠ y₁
hxy' : y₁ ≠ x₁
⊢ (x₁, y₁) ∈ offDiag s
[PROOFSTEP]
rw [mem_offDiag]
[GOAL]
case a.mk.inr.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
x₁ y₁ : α
hy : x₁ ∈ s
hx : y₁ ∈ s
h : a ≈ (y₁, x₁)
hxy : y₁ ≠ x₁
hxy' : x₁ ≠ y₁
⊢ (x₁, y₁) ∈ offDiag s
[PROOFSTEP]
rw [mem_offDiag]
[GOAL]
case a.mk.inl.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
x₁ y₁ : α
hx : x₁ ∈ s
hy : y₁ ∈ s
h : a ≈ (x₁, y₁)
hxy : x₁ ≠ y₁
hxy' : y₁ ≠ x₁
⊢ (x₁, y₁).fst ∈ s ∧ (x₁, y₁).snd ∈ s ∧ (x₁, y₁).fst ≠ (x₁, y₁).snd
[PROOFSTEP]
exact ⟨‹_›, ‹_›, ‹_›⟩
[GOAL]
case a.mk.inr.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
a : α × α
ha₁ : a.fst ∈ s
ha₂ : a.snd ∈ s
ha : a.fst ≠ a.snd
x₁ y₁ : α
hy : x₁ ∈ s
hx : y₁ ∈ s
h : a ≈ (y₁, x₁)
hxy : y₁ ≠ x₁
hxy' : x₁ ≠ y₁
⊢ (x₁, y₁).fst ∈ s ∧ (x₁, y₁).snd ∈ s ∧ (x₁, y₁).fst ≠ (x₁, y₁).snd
[PROOFSTEP]
exact ⟨‹_›, ‹_›, ‹_›⟩
[GOAL]
case mk.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
dsimp [Quotient.mk', Quotient.mk''_eq_mk]
  -- Porting note: Added `dsimp`
[GOAL]
case mk.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
rw [this, card_insert_of_not_mem, card_singleton]
[GOAL]
case mk.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
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)}
[PROOFSTEP]
simp only [not_and, Prod.mk.inj_iff, mem_singleton]
[GOAL]
case mk.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact fun _ => hxy'
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
⊢ Finset.card (image Quotient.mk' (offDiag s)) = Nat.choose (Finset.card s) 2
[PROOFSTEP]
rw [Nat.choose_two_right, mul_tsub, mul_one, ← offDiag_card,
  Nat.div_eq_of_eq_mul_right zero_lt_two (two_mul_card_image_offDiag s).symm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Fintype.card { a // IsDiag a } = Fintype.card α
[PROOFSTEP]
convert card_image_diag (univ : Finset α)
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Fintype.card { a // IsDiag a } = Finset.card (image Quotient.mk' (Finset.diag univ))
[PROOFSTEP]
simp_rw [Quotient.mk', ← Quotient.mk''_eq_mk]
  -- Porting note: Added `simp_rw`
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Fintype.card { a // IsDiag a } = Finset.card (image (fun a => Quotient.mk'' a) (Finset.diag univ))
[PROOFSTEP]
rw [Fintype.card_of_subtype, ← filter_image_quotient_mk''_isDiag]
[GOAL]
case h.e'_2.H
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ ∀ (x : Sym2 α), x ∈ filter IsDiag (image Quotient.mk'' (univ ×ˢ univ)) ↔ IsDiag x
[PROOFSTEP]
rintro x
[GOAL]
case h.e'_2.H
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
⊢ x ∈ filter IsDiag (image Quotient.mk'' (univ ×ˢ univ)) ↔ IsDiag x
[PROOFSTEP]
rw [mem_filter, univ_product_univ, mem_image]
[GOAL]
case h.e'_2.H
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
⊢ (∃ a, a ∈ univ ∧ Quotient.mk'' a = x) ∧ IsDiag x ↔ IsDiag x
[PROOFSTEP]
obtain ⟨a, ha⟩ := Quotient.exists_rep x
[GOAL]
case h.e'_2.H.intro
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact and_iff_right ⟨a, mem_univ _, ha⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Fintype.card { a // ¬IsDiag a } = Nat.choose (Fintype.card α) 2
[PROOFSTEP]
convert card_image_offDiag (univ : Finset α)
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Fintype.card { a // ¬IsDiag a } = Finset.card (image Quotient.mk' (offDiag univ))
[PROOFSTEP]
simp_rw [Quotient.mk', ← Quotient.mk''_eq_mk]
  -- Porting note: Added `simp_rw`
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Fintype.card { a // ¬IsDiag a } = Finset.card (image (fun a => Quotient.mk'' a) (offDiag univ))
[PROOFSTEP]
rw [Fintype.card_of_subtype, ← filter_image_quotient_mk''_not_isDiag]
[GOAL]
case h.e'_2.H
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ ∀ (x : Sym2 α), x ∈ filter (fun a => ¬IsDiag a) (image Quotient.mk'' (univ ×ˢ univ)) ↔ ¬IsDiag x
[PROOFSTEP]
rintro x
[GOAL]
case h.e'_2.H
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
⊢ x ∈ filter (fun a => ¬IsDiag a) (image Quotient.mk'' (univ ×ˢ univ)) ↔ ¬IsDiag x
[PROOFSTEP]
rw [mem_filter, univ_product_univ, mem_image]
[GOAL]
case h.e'_2.H
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x : Sym2 α
⊢ (∃ a, a ∈ univ ∧ Quotient.mk'' a = x) ∧ ¬IsDiag x ↔ ¬IsDiag x
[PROOFSTEP]
obtain ⟨a, ha⟩ := Quotient.exists_rep x
[GOAL]
case h.e'_2.H.intro
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
exact and_iff_right ⟨a, mem_univ _, ha⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
⊢ Finset.card (Finset.sym2 s) = Finset.card s * (Finset.card s + 1) / 2
[PROOFSTEP]
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]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
⊢ Disjoint (image Quotient.mk' (Finset.diag s)) (image Quotient.mk' (offDiag s))
[PROOFSTEP]
rw [disjoint_left]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
⊢ ∀ ⦃a : Quotient (Rel.setoid α)⦄, a ∈ image Quotient.mk' (Finset.diag s) → ¬a ∈ image Quotient.mk' (offDiag s)
[PROOFSTEP]
rintro m ha hb
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
m : Quotient (Rel.setoid α)
ha : m ∈ image Quotient.mk' (Finset.diag s)
hb : m ∈ image Quotient.mk' (offDiag s)
⊢ False
[PROOFSTEP]
rw [mem_image] at ha hb 
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
obtain ⟨⟨a, ha, rfl⟩, ⟨b, hb, hab⟩⟩ := ha, hb
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset α
a : α × α
ha : a ∈ Finset.diag s
b : α × α
hb : b ∈ offDiag s
hab : Quotient.mk' b = Quotient.mk' a
⊢ False
[PROOFSTEP]
refine' not_isDiag_mk'_of_mem_offDiag hb _
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
dsimp [Quotient.mk'] at hab 
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
rw [hab]
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
exact isDiag_mk'_of_mem_diag ha
