no goals
α : Type ?u.6052
β : Type ?u.6055
n✝ n : ℕ
⊢ Fintype.card (Sym (Fin n) 0) = multichoose n 0
simp
α : Type ?u.6052
β : Type ?u.6055
n k : ℕ
⊢ Fintype.card (Sym (Fin 0) (k + 1)) = 0
α : Type ?u.6052
β : Type ?u.6055
n k : ℕ
⊢ Fintype.card (Sym (Fin 0) (k + 1)) = multichoose 0 (k + 1)
rw [multichoose_zero_succ]
no goals
α : Type ?u.6052
β : Type ?u.6055
n k : ℕ
⊢ Fintype.card (Sym (Fin 0) (k + 1)) = 0
exact card_eq_zero
no goals
α : Type ?u.6052
β : Type ?u.6055
n k : ℕ
⊢ Fintype.card (Sym (Fin 1) (k + 1)) = multichoose 1 (k + 1)
simp
α : Type ?u.6052
β : Type ?u.6055
n✝ n k : ℕ
⊢ Fintype.card (Sym (Fin (n + 2)) (k + 1)) = Fintype.card (Sym (Fin (n + 2)) k ⊕ Sym (Fin (n + 1)) (k + 1))
α : Type ?u.6052
β : Type ?u.6055
n✝ n k : ℕ
⊢ Fintype.card (Sym (Fin (n + 2)) (k + 1)) = multichoose (n + 2) (k + 1)
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]
α : Type ?u.6052
β : Type ?u.6055
n✝ n k : ℕ
⊢ Sym (Fin (n + 2)) k ⊕ Sym (Fin (n + 1)) (k + 1) ≃ Sym (Fin (n + 2)) (k + 1)
α : Type ?u.6052
β : Type ?u.6055
n✝ n k : ℕ
⊢ Fintype.card (Sym (Fin (n + 2)) (k + 1)) = Fintype.card (Sym (Fin (n + 2)) k ⊕ Sym (Fin (n + 1)) (k + 1))
refine Fintype.card_congr (Equiv.symm ?_)
α : Type ?u.6052
β : Type ?u.6055
n✝ n k : ℕ
⊢ { s // 0 ∈ s } ⊕ { s // ¬0 ∈ s } ≃ Sym (Fin (n + 2)) (k + 1)
α : Type ?u.6052
β : Type ?u.6055
n✝ n k : ℕ
⊢ Sym (Fin (n + 2)) k ⊕ Sym (Fin (n + 1)) (k + 1) ≃ Sym (Fin (n + 2)) (k + 1)
apply (Sym.e1.symm.sumCongr Sym.e2.symm).trans
no goals
α : Type ?u.6052
β : Type ?u.6055
n✝ n k : ℕ
⊢ { s // 0 ∈ s } ⊕ { s // ¬0 ∈ s } ≃ Sym (Fin (n + 2)) (k + 1)
apply Equiv.sumCompl