α : Type u_2
β : Type u_3
A : Type ?u.99397
B : Type ?u.99400
M : Type u_1
N : Type ?u.99406
P : Type ?u.99409
R : Type ?u.99412
S : Type ?u.99415
G : Type ?u.99418
M₀ : Type ?u.99421
G₀ : Type ?u.99424
ι : Sort ?u.99427
inst✝ : CommMonoid M
s : Finset α
f : α → β → M
⊢ ∀ (x : β), (¬x ∈ ⋃ (i : α) (_ : i ∈ s), mulSupport (f i)) → ∏ i in s, f i x = 1
α : Type u_2
β : Type u_3
A : Type ?u.99397
B : Type ?u.99400
M : Type u_1
N : Type ?u.99406
P : Type ?u.99409
R : Type ?u.99412
S : Type ?u.99415
G : Type ?u.99418
M₀ : Type ?u.99421
G₀ : Type ?u.99424
ι : Sort ?u.99427
inst✝ : CommMonoid M
s : Finset α
f : α → β → M
⊢ (mulSupport fun x => ∏ i in s, f i x) ⊆ ⋃ (i : α) (_ : i ∈ s), mulSupport (f i)
rw [mulSupport_subset_iff']
α : Type u_2
β : Type u_3
A : Type ?u.99397
B : Type ?u.99400
M : Type u_1
N : Type ?u.99406
P : Type ?u.99409
R : Type ?u.99412
S : Type ?u.99415
G : Type ?u.99418
M₀ : Type ?u.99421
G₀ : Type ?u.99424
ι : Sort ?u.99427
inst✝ : CommMonoid M
s : Finset α
f : α → β → M
⊢ ∀ (x : β), (∀ (x_1 : α), x_1 ∈ s → f x_1 x = 1) → ∏ i in s, f i x = 1
α : Type u_2
β : Type u_3
A : Type ?u.99397
B : Type ?u.99400
M : Type u_1
N : Type ?u.99406
P : Type ?u.99409
R : Type ?u.99412
S : Type ?u.99415
G : Type ?u.99418
M₀ : Type ?u.99421
G₀ : Type ?u.99424
ι : Sort ?u.99427
inst✝ : CommMonoid M
s : Finset α
f : α → β → M
⊢ ∀ (x : β), (¬x ∈ ⋃ (i : α) (_ : i ∈ s), mulSupport (f i)) → ∏ i in s, f i x = 1
simp only [mem_iUnion, not_exists, nmem_mulSupport]
no goals
α : Type u_2
β : Type u_3
A : Type ?u.99397
B : Type ?u.99400
M : Type u_1
N : Type ?u.99406
P : Type ?u.99409
R : Type ?u.99412
S : Type ?u.99415
G : Type ?u.99418
M₀ : Type ?u.99421
G₀ : Type ?u.99424
ι : Sort ?u.99427
inst✝ : CommMonoid M
s : Finset α
f : α → β → M
⊢ ∀ (x : β), (∀ (x_1 : α), x_1 ∈ s → f x_1 x = 1) → ∏ i in s, f i x = 1
exact fun x => Finset.prod_eq_one