ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
f : Π₀ (i : ι), Finset (α i)
⊢ ∏ i in support f, card (↑f i) = prod f fun i => ↑(card (↑f i))
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
f : Π₀ (i : ι), Finset (α i)
⊢ card (pi f) = prod f fun i => ↑(card (↑f i))
rw [pi, card_dfinsupp]
no goals
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
f : Π₀ (i : ι), Finset (α i)
⊢ ∏ i in support f, card (↑f i) = prod f fun i => ↑(card (↑f i))
exact Finset.prod_congr rfl fun i _ => by simp only [Pi.nat_apply, Nat.cast_id]
no goals
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
f : Π₀ (i : ι), Finset (α i)
i : ι
x✝ : i ∈ support f
⊢ card (↑f i) = (fun i => ↑(card (↑f i))) i (↑f i)
simp only [Pi.nat_apply, Nat.cast_id]