α : Type u_1
β : Type u_2
γ : Type ?u.60368
δ : Type ?u.60371
a✝ : α
b : β
s✝¹ : Multiset α
t✝ : Multiset β
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : Multiset β), s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u
t u : Multiset β
⊢ map (Prod.mk a) (t + u) + (s ×ˢ t + s ×ˢ u) = (a ::ₘ s) ×ˢ t + (a ::ₘ s) ×ˢ u
α : Type u_1
β : Type u_2
γ : Type ?u.60368
δ : Type ?u.60371
a✝ : α
b : β
s✝¹ : Multiset α
t✝ : Multiset β
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : Multiset β), s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u
t u : Multiset β
⊢ (a ::ₘ s) ×ˢ (t + u) = (a ::ₘ s) ×ˢ t + (a ::ₘ s) ×ˢ u
rw [cons_product, IH]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.60368
δ : Type ?u.60371
a✝ : α
b : β
s✝¹ : Multiset α
t✝ : Multiset β
s✝ : Multiset α
a : α
s : Multiset α
IH : ∀ (t u : Multiset β), s ×ˢ (t + u) = s ×ˢ t + s ×ˢ u
t u : Multiset β
⊢ map (Prod.mk a) (t + u) + (s ×ˢ t + s ×ˢ u) = (a ::ₘ s) ×ˢ t + (a ::ₘ s) ×ˢ u
simp [add_comm, add_left_comm, add_assoc]