G : Type ?u.40546
M : Type u_1
N : Type ?u.40552
α : Sort ?u.40555
β : Sort ?u.40558
ι : Sort ?u.40561
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
p : Prop
f g : p → M
hfg : ∀ (h : p), f (_ : p) = g h
⊢ finprod f = finprod g
G : Type ?u.40546
M : Type u_1
N : Type ?u.40552
α : Sort ?u.40555
β : Sort ?u.40558
ι : Sort ?u.40561
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
p q : Prop
f : p → M
g : q → M
hpq : p = q
hfg : ∀ (h : q), f (_ : p) = g h
⊢ finprod f = finprod g
subst q
no goals
G : Type ?u.40546
M : Type u_1
N : Type ?u.40552
α : Sort ?u.40555
β : Sort ?u.40558
ι : Sort ?u.40561
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
p : Prop
f g : p → M
hfg : ∀ (h : p), f (_ : p) = g h
⊢ finprod f = finprod g
exact finprod_congr hfg