no goals
α : Type u_1
β : Type ?u.5793
γ : Type ?u.5796
δ : Type ?u.5799
S : Multiset (Multiset α)
⊢ ↑card (join 0) = sum (map (↑card) 0)
simp
no goals
α : Type u_1
β : Type ?u.5793
γ : Type ?u.5796
δ : Type ?u.5799
S : Multiset (Multiset α)
⊢ ∀ ⦃a : Multiset α⦄ {s : Multiset (Multiset α)},
    ↑card (join s) = sum (map (↑card) s) → ↑card (join (a ::ₘ s)) = sum (map (↑card) (a ::ₘ s))
simp