α : Type u_1
β : Type ?u.345276
ι : Type ?u.345279
G : Type ?u.345282
M : Type u_2
N : Type ?u.345288
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
h : ¬a ∈ s → f a = 1
x : α
hx : x ∈ mulSupport fun i => f i
⊢ x ∈ insert a s → x ∈ s
α : Type u_1
β : Type ?u.345276
ι : Type ?u.345279
G : Type ?u.345282
M : Type u_2
N : Type ?u.345288
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
h : ¬a ∈ s → f a = 1
⊢ (∏ᶠ (i : α) (_ : i ∈ insert a s), f i) = ∏ᶠ (i : α) (_ : i ∈ s), f i
refine' finprod_mem_inter_mulSupport_eq' _ _ _ fun x hx => ⟨_, Or.inr⟩
case inl
α : Type u_1
β : Type ?u.345276
ι : Type ?u.345279
G : Type ?u.345282
M : Type u_2
N : Type ?u.345288
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
b : α
s t : Set α
x : α
hx : x ∈ mulSupport fun i => f i
h : ¬x ∈ s → f x = 1
⊢ x ∈ s

case inr
α : Type u_1
β : Type ?u.345276
ι : Type ?u.345279
G : Type ?u.345282
M : Type u_2
N : Type ?u.345288
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
h : ¬a ∈ s → f a = 1
x : α
hx : x ∈ mulSupport fun i => f i
hxs : x ∈ s
⊢ x ∈ s
α : Type u_1
β : Type ?u.345276
ι : Type ?u.345279
G : Type ?u.345282
M : Type u_2
N : Type ?u.345288
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
h : ¬a ∈ s → f a = 1
x : α
hx : x ∈ mulSupport fun i => f i
⊢ x ∈ insert a s → x ∈ s
rintro (rfl | hxs)
no goals
case inl
α : Type u_1
β : Type ?u.345276
ι : Type ?u.345279
G : Type ?u.345282
M : Type u_2
N : Type ?u.345288
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
b : α
s t : Set α
x : α
hx : x ∈ mulSupport fun i => f i
h : ¬x ∈ s → f x = 1
⊢ x ∈ s

case inr
α : Type u_1
β : Type ?u.345276
ι : Type ?u.345279
G : Type ?u.345282
M : Type u_2
N : Type ?u.345288
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f g : α → M
a b : α
s t : Set α
h : ¬a ∈ s → f a = 1
x : α
hx : x ∈ mulSupport fun i => f i
hxs : x ∈ s
⊢ x ∈ s
exacts [not_imp_comm.1 h hx, hxs]