α : Type u_2
β : Type u_1
ι : Type ?u.354818
G : Type ?u.354821
M : Type u_3
N : Type ?u.354827
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s t : Set α
g : β → α
hg : InjOn g (mulSupport (f ∘ g))
⊢ InjOn g (univ ∩ mulSupport ((fun i => f i) ∘ g))
α : Type u_2
β : Type u_1
ι : Type ?u.354818
G : Type ?u.354821
M : Type u_3
N : Type ?u.354827
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s t : Set α
g : β → α
hg : InjOn g (mulSupport (f ∘ g))
⊢ (∏ᶠ (i : α) (_ : i ∈ range g), f i) = ∏ᶠ (j : β), f (g j)
rw [← image_univ, finprod_mem_image', finprod_mem_univ]
no goals
α : Type u_2
β : Type u_1
ι : Type ?u.354818
G : Type ?u.354821
M : Type u_3
N : Type ?u.354827
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g✝ : α → M
a b : α
s t : Set α
g : β → α
hg : InjOn g (mulSupport (f ∘ g))
⊢ InjOn g (univ ∩ mulSupport ((fun i => f i) ∘ g))
rwa [univ_inter]