no goals
ι : Type u_1
α : Type ?u.19416
M : Type u_2
N : Type u_3
P : Type ?u.19425
M₀ : Type ?u.19428
G : Type ?u.19431
R : Type ?u.19434
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l✝¹ l₁ l₂ : List M
a✝ : M
l✝ : List ι
r : M → N → Prop
f : ι → M
g : ι → N
h₁ : r 1 1
h₂ : ∀ ⦃i : ι⦄ ⦃a : M⦄ ⦃b : N⦄, r a b → r (f i * a) (g i * b)
a : ι
l : List ι
hl : r (prod (map f l)) (prod (map g l))
⊢ r (prod (map f (a :: l))) (prod (map g (a :: l)))
simp only [map_cons, prod_cons, h₂ hl]