α : Type u_1
β : Type u_2
ι : Type ?u.356139
G : Type ?u.356142
M : Type u_3
N : Type ?u.356148
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g✝ : α → M
a b : α
s✝ t✝ s : Set α
t : Set β
f : α → M
g : β → M
e : α → β
he₀ : BijOn e s t
he₁ : ∀ (x : α), x ∈ s → f x = g (e x)
⊢ (∏ᶠ (i : α) (_ : i ∈ s), f i) = ∏ᶠ (j : α) (_ : j ∈ s), g (e j)
α : Type u_1
β : Type u_2
ι : Type ?u.356139
G : Type ?u.356142
M : Type u_3
N : Type ?u.356148
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g✝ : α → M
a b : α
s✝ t✝ s : Set α
t : Set β
f : α → M
g : β → M
e : α → β
he₀ : BijOn e s t
he₁ : ∀ (x : α), x ∈ s → f x = g (e x)
⊢ (∏ᶠ (i : α) (_ : i ∈ s), f i) = ∏ᶠ (j : β) (_ : j ∈ t), g j
rw [← Set.BijOn.image_eq he₀, finprod_mem_image he₀.2.1]
no goals
α : Type u_1
β : Type u_2
ι : Type ?u.356139
G : Type ?u.356142
M : Type u_3
N : Type ?u.356148
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f✝ g✝ : α → M
a b : α
s✝ t✝ s : Set α
t : Set β
f : α → M
g : β → M
e : α → β
he₀ : BijOn e s t
he₁ : ∀ (x : α), x ∈ s → f x = g (e x)
⊢ (∏ᶠ (i : α) (_ : i ∈ s), f i) = ∏ᶠ (j : α) (_ : j ∈ s), g (e j)
exact finprod_mem_congr rfl he₁