case h
α : Type u_1
inst✝ : NonUnitalNonAssocSemiring α
s : Multiset α
a : α
a✝ : List α
h : ∀ (b : α), b ∈ Quotient.mk (List.isSetoid α) a✝ → Commute a b
⊢ Commute a (sum (Quotient.mk (List.isSetoid α) a✝))
α : Type u_1
inst✝ : NonUnitalNonAssocSemiring α
s : Multiset α
a : α
h : ∀ (b : α), b ∈ s → Commute a b
⊢ Commute a (sum s)
induction s using Quotient.inductionOn
case h
α : Type u_1
inst✝ : NonUnitalNonAssocSemiring α
s : Multiset α
a : α
a✝ : List α
h : ∀ (b : α), b ∈ Quotient.mk (List.isSetoid α) a✝ → Commute a b
⊢ Commute a (List.sum a✝)
case h
α : Type u_1
inst✝ : NonUnitalNonAssocSemiring α
s : Multiset α
a : α
a✝ : List α
h : ∀ (b : α), b ∈ Quotient.mk (List.isSetoid α) a✝ → Commute a b
⊢ Commute a (sum (Quotient.mk (List.isSetoid α) a✝))
rw [quot_mk_to_coe, coe_sum]
no goals
case h
α : Type u_1
inst✝ : NonUnitalNonAssocSemiring α
s : Multiset α
a : α
a✝ : List α
h : ∀ (b : α), b ∈ Quotient.mk (List.isSetoid α) a✝ → Commute a b
⊢ Commute a (List.sum a✝)
exact Commute.list_sum_right _ _ h