G : Type ?u.47261
M : Type u_1
N : Type u_2
α : Sort u_3
β : Sort ?u.47273
ι : Sort ?u.47276
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
g : α → M
h : Set.Finite (mulSupport (g ∘ PLift.down))
⊢ mulSupport ((fun x => ↑f (g x)) ∘ PLift.down) ⊆ ↑(Finite.toFinset h)
G : Type ?u.47261
M : Type u_1
N : Type u_2
α : Sort u_3
β : Sort ?u.47273
ι : Sort ?u.47276
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
g : α → M
h : Set.Finite (mulSupport (g ∘ PLift.down))
⊢ ↑f (∏ᶠ (x : α), g x) = ∏ᶠ (x : α), ↑f (g x)
rw [finprod_eq_prod_pLift_of_mulSupport_subset h.coe_toFinset.ge,
  finprod_eq_prod_pLift_of_mulSupport_subset, f.map_prod]
G : Type ?u.47261
M : Type u_1
N : Type u_2
α : Sort u_3
β : Sort ?u.47273
ι : Sort ?u.47276
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
g : α → M
h : Set.Finite (mulSupport (g ∘ PLift.down))
⊢ mulSupport ((fun x => ↑f (g x)) ∘ PLift.down) ⊆ mulSupport (g ∘ PLift.down)
G : Type ?u.47261
M : Type u_1
N : Type u_2
α : Sort u_3
β : Sort ?u.47273
ι : Sort ?u.47276
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
g : α → M
h : Set.Finite (mulSupport (g ∘ PLift.down))
⊢ mulSupport ((fun x => ↑f (g x)) ∘ PLift.down) ⊆ ↑(Finite.toFinset h)
rw [h.coe_toFinset]
no goals
G : Type ?u.47261
M : Type u_1
N : Type u_2
α : Sort u_3
β : Sort ?u.47273
ι : Sort ?u.47276
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : M →* N
g : α → M
h : Set.Finite (mulSupport (g ∘ PLift.down))
⊢ mulSupport ((fun x => ↑f (g x)) ∘ PLift.down) ⊆ mulSupport (g ∘ PLift.down)
exact mulSupport_comp_subset f.map_one (g ∘ PLift.down)