α : Type u_2
β : Type u_1
ι : Type ?u.393586
G : Type ?u.393589
M : Type u_3
N : Type ?u.393595
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g✝ : α → M
a b : α
s✝ t : Set α
inst✝ : DecidableEq β
s : Finset α
f : α → M
g : α → β
⊢ (mulSupport fun b => Finset.prod (filter (fun a => g a = b) s) f) ⊆ g '' ↑s
α : Type u_2
β : Type u_1
ι : Type ?u.393586
G : Type ?u.393589
M : Type u_3
N : Type ?u.393595
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g✝ : α → M
a b : α
s✝ t : Set α
inst✝ : DecidableEq β
s : Finset α
f : α → M
g : α → β
⊢ (mulSupport fun b => Finset.prod (filter (fun a => g a = b) s) f) ⊆ ↑(image g s)
simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe, Function.support_subset_iff]
α : Type u_2
β : Type u_1
ι : Type ?u.393586
G : Type ?u.393589
M : Type u_3
N : Type ?u.393595
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g✝ : α → M
a b✝ : α
s✝ t : Set α
inst✝ : DecidableEq β
s : Finset α
f : α → M
g : α → β
b : β
h : b ∈ mulSupport fun b => Finset.prod (filter (fun a => g a = b) s) f
⊢ b ∈ g '' ↑s
α : Type u_2
β : Type u_1
ι : Type ?u.393586
G : Type ?u.393589
M : Type u_3
N : Type ?u.393595
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g✝ : α → M
a b : α
s✝ t : Set α
inst✝ : DecidableEq β
s : Finset α
f : α → M
g : α → β
⊢ (mulSupport fun b => Finset.prod (filter (fun a => g a = b) s) f) ⊆ g '' ↑s
intro b h
α : Type u_2
β : Type u_1
ι : Type ?u.393586
G : Type ?u.393589
M : Type u_3
N : Type ?u.393595
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g✝ : α → M
a b✝ : α
s✝ t : Set α
inst✝ : DecidableEq β
s : Finset α
f : α → M
g : α → β
b : β
h : b ∈ mulSupport fun b => Finset.prod (filter (fun a => g a = b) s) f
⊢ Finset.Nonempty (filter (fun a => g a = b) s)
α : Type u_2
β : Type u_1
ι : Type ?u.393586
G : Type ?u.393589
M : Type u_3
N : Type ?u.393595
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g✝ : α → M
a b✝ : α
s✝ t : Set α
inst✝ : DecidableEq β
s : Finset α
f : α → M
g : α → β
b : β
h : b ∈ mulSupport fun b => Finset.prod (filter (fun a => g a = b) s) f
⊢ b ∈ g '' ↑s
suffices (s.filter fun a : α => g a = b).Nonempty by
  simpa only [s.fiber_nonempty_iff_mem_image g b, Finset.mem_image, exists_prop]
no goals
α : Type u_2
β : Type u_1
ι : Type ?u.393586
G : Type ?u.393589
M : Type u_3
N : Type ?u.393595
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g✝ : α → M
a b✝ : α
s✝ t : Set α
inst✝ : DecidableEq β
s : Finset α
f : α → M
g : α → β
b : β
h : b ∈ mulSupport fun b => Finset.prod (filter (fun a => g a = b) s) f
⊢ Finset.Nonempty (filter (fun a => g a = b) s)
exact Finset.nonempty_of_prod_ne_one h
no goals
α : Type u_2
β : Type u_1
ι : Type ?u.393586
G : Type ?u.393589
M : Type u_3
N : Type ?u.393595
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
f✝ g✝ : α → M
a b✝ : α
s✝ t : Set α
inst✝ : DecidableEq β
s : Finset α
f : α → M
g : α → β
b : β
h : b ∈ mulSupport fun b => Finset.prod (filter (fun a => g a = b) s) f
this : Finset.Nonempty (filter (fun a => g a = b) s)
⊢ b ∈ g '' ↑s
simpa only [s.fiber_nonempty_iff_mem_image g b, Finset.mem_image, exists_prop]