no goals
ι : Type u_2
α : Type u_3
β : Type u_1
γ : Type ?u.53519
inst✝¹ : CommMonoid α
s✝ t : Multiset α
a : α
m : Multiset ι
f✝ g✝ : ι → α
inst✝ : CommMonoid β
s : Multiset ι
r : α → β → Prop
f : ι → α
g : ι → β
h₁ : r 1 1
h₂ : ∀ ⦃a : ι⦄ ⦃b : α⦄ ⦃c : β⦄, r b c → r (f a * b) (g a * c)
l : List ι
⊢ r (prod (map f (Quotient.mk (List.isSetoid ι) l))) (prod (map g (Quotient.mk (List.isSetoid ι) l)))
simp only [l.prod_hom_rel h₁ h₂, quot_mk_to_coe, coe_map, coe_prod]