α : Type u_2
β : Type ?u.71688
γ : Type ?u.71691
δ : Type ?u.71694
σ : α → Type u_1
a✝ : α
s✝ : Multiset α
t✝ : (a : α) → Multiset (σ a)
a : α
s : Multiset α
IH : ∀ (t u : (a : α) → Multiset (σ a)), (Multiset.sigma s fun a => t a + u a) = Multiset.sigma s t + Multiset.sigma s u
t u : (a : α) → Multiset (σ a)
⊢ map (Sigma.mk a) (t a + u a) + ((Multiset.sigma s fun a => t a) + Multiset.sigma s fun a => u a) =
    Multiset.sigma (a ::ₘ s) t + Multiset.sigma (a ::ₘ s) u
α : Type u_2
β : Type ?u.71688
γ : Type ?u.71691
δ : Type ?u.71694
σ : α → Type u_1
a✝ : α
s✝ : Multiset α
t✝ : (a : α) → Multiset (σ a)
a : α
s : Multiset α
IH : ∀ (t u : (a : α) → Multiset (σ a)), (Multiset.sigma s fun a => t a + u a) = Multiset.sigma s t + Multiset.sigma s u
t u : (a : α) → Multiset (σ a)
⊢ (Multiset.sigma (a ::ₘ s) fun a => t a + u a) = Multiset.sigma (a ::ₘ s) t + Multiset.sigma (a ::ₘ s) u
rw [cons_sigma, IH]
no goals
α : Type u_2
β : Type ?u.71688
γ : Type ?u.71691
δ : Type ?u.71694
σ : α → Type u_1
a✝ : α
s✝ : Multiset α
t✝ : (a : α) → Multiset (σ a)
a : α
s : Multiset α
IH : ∀ (t u : (a : α) → Multiset (σ a)), (Multiset.sigma s fun a => t a + u a) = Multiset.sigma s t + Multiset.sigma s u
t u : (a : α) → Multiset (σ a)
⊢ map (Sigma.mk a) (t a + u a) + ((Multiset.sigma s fun a => t a) + Multiset.sigma s fun a => u a) =
    Multiset.sigma (a ::ₘ s) t + Multiset.sigma (a ::ₘ s) u
simp [add_comm, add_left_comm, add_assoc]