case h
α : Type u_1
β : Type ?u.208648
ι : Type ?u.208651
G : Type ?u.208654
M : Type u_2
N : Type ?u.208660
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s t : Set α
h : ∀ (x : α), x ∈ mulSupport f → (x ∈ s ↔ x ∈ t)
⊢ (s ∩ mulSupport fun i => f i) = t ∩ mulSupport fun i => f i
α : Type u_1
β : Type ?u.208648
ι : Type ?u.208651
G : Type ?u.208654
M : Type u_2
N : Type ?u.208660
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s t : Set α
h : ∀ (x : α), x ∈ mulSupport f → (x ∈ s ↔ x ∈ t)
⊢ (∏ᶠ (i : α) (_ : i ∈ s), f i) = ∏ᶠ (i : α) (_ : i ∈ t), f i
apply finprod_mem_inter_mulSupport_eq
case h.h
α : Type u_1
β : Type ?u.208648
ι : Type ?u.208651
G : Type ?u.208654
M : Type u_2
N : Type ?u.208660
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s t : Set α
h : ∀ (x : α), x ∈ mulSupport f → (x ∈ s ↔ x ∈ t)
x : α
⊢ (x ∈ s ∩ mulSupport fun i => f i) ↔ x ∈ t ∩ mulSupport fun i => f i
case h
α : Type u_1
β : Type ?u.208648
ι : Type ?u.208651
G : Type ?u.208654
M : Type u_2
N : Type ?u.208660
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s t : Set α
h : ∀ (x : α), x ∈ mulSupport f → (x ∈ s ↔ x ∈ t)
⊢ (s ∩ mulSupport fun i => f i) = t ∩ mulSupport fun i => f i
ext x
no goals
case h.h
α : Type u_1
β : Type ?u.208648
ι : Type ?u.208651
G : Type ?u.208654
M : Type u_2
N : Type ?u.208660
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
s t : Set α
h : ∀ (x : α), x ∈ mulSupport f → (x ∈ s ↔ x ∈ t)
x : α
⊢ (x ∈ s ∩ mulSupport fun i => f i) ↔ x ∈ t ∩ mulSupport fun i => f i
exact and_congr_left (h x)