n✝ n : ℕ
this : Fintype.card (Finset (Fin (n - 1))) = 2 ^ (n - 1)
⊢ Fintype.card (CompositionAsSet n) = 2 ^ (n - 1)
n✝ n : ℕ
⊢ Fintype.card (CompositionAsSet n) = 2 ^ (n - 1)
have : Fintype.card (Finset (Fin (n - 1))) = 2 ^ (n - 1) := by simp
n✝ n : ℕ
this : Fintype.card (Finset (Fin (n - 1))) = 2 ^ (n - 1)
⊢ Fintype.card (CompositionAsSet n) = Fintype.card (Finset (Fin (n - 1)))
n✝ n : ℕ
this : Fintype.card (Finset (Fin (n - 1))) = 2 ^ (n - 1)
⊢ Fintype.card (CompositionAsSet n) = 2 ^ (n - 1)
rw [← this]
no goals
n✝ n : ℕ
this : Fintype.card (Finset (Fin (n - 1))) = 2 ^ (n - 1)
⊢ Fintype.card (CompositionAsSet n) = Fintype.card (Finset (Fin (n - 1)))
exact Fintype.card_congr (compositionAsSetEquiv n)
no goals
n✝ n : ℕ
⊢ Fintype.card (Finset (Fin (n - 1))) = 2 ^ (n - 1)
simp