no goals
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m : Multiset α
t : (a : α) → Multiset (β a)
⊢ ↑card (pi 0 t) = prod (map (fun a => ↑card (t a)) 0)
simp
no goals
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u
δ : α → Sort v
m : Multiset α
t : (a : α) → Multiset (β a)
⊢ ∀ ⦃a : α⦄ {s : Multiset α},
    ↑card (pi s t) = prod (map (fun a => ↑card (t a)) s) →
      ↑card (pi (a ::ₘ s) t) = prod (map (fun a => ↑card (t a)) (a ::ₘ s))
simp (config := { contextual := true }) [mul_comm]