α : Type u_1
β : Type ?u.188274
ι : Type ?u.188277
G : Type ?u.188280
M : Type u_2
N : Type ?u.188286
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
⊢ (∏ᶠ (i : α) (_ : p i), f i) = ∏ i in t, f i
α : Type u_1
β : Type ?u.188274
ι : Type ?u.188277
G : Type ?u.188280
M : Type u_2
N : Type ?u.188286
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
⊢ (∏ᶠ (i : α) (_ : p i), f i) = ∏ i in t, f i
set s := { x | p x }
α : Type u_1
β : Type ?u.188274
ι : Type ?u.188277
G : Type ?u.188280
M : Type u_2
N : Type ?u.188286
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
this : mulSupport (mulIndicator s f) ⊆ ↑t
⊢ (∏ᶠ (i : α) (_ : p i), f i) = ∏ i in t, f i
α : Type u_1
β : Type ?u.188274
ι : Type ?u.188277
G : Type ?u.188280
M : Type u_2
N : Type ?u.188286
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
⊢ (∏ᶠ (i : α) (_ : p i), f i) = ∏ i in t, f i
have : mulSupport (s.mulIndicator f) ⊆ t := by
  rw [Set.mulSupport_mulIndicator]
  intro x hx
  exact (h hx.2).1 hx.1
α : Type u_1
β : Type ?u.188274
ι : Type ?u.188277
G : Type ?u.188280
M : Type u_2
N : Type ?u.188286
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
this : mulSupport (mulIndicator s f) ⊆ ↑t
⊢ ∏ i in t, mulIndicator s f i = ∏ i in t, f i
α : Type u_1
β : Type ?u.188274
ι : Type ?u.188277
G : Type ?u.188280
M : Type u_2
N : Type ?u.188286
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
this : mulSupport (mulIndicator s f) ⊆ ↑t
⊢ (∏ᶠ (i : α) (_ : p i), f i) = ∏ i in t, f i
erw [finprod_mem_def, finprod_eq_prod_of_mulSupport_subset _ this]
α : Type u_1
β : Type ?u.188274
ι : Type ?u.188277
G : Type ?u.188280
M : Type u_2
N : Type ?u.188286
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
this : mulSupport (mulIndicator s f) ⊆ ↑t
x : α
hx : x ∈ t
hxs : ¬x ∈ s
⊢ f x = 1
α : Type u_1
β : Type ?u.188274
ι : Type ?u.188277
G : Type ?u.188280
M : Type u_2
N : Type ?u.188286
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
this : mulSupport (mulIndicator s f) ⊆ ↑t
⊢ ∏ i in t, mulIndicator s f i = ∏ i in t, f i
refine' Finset.prod_congr rfl fun x hx => mulIndicator_apply_eq_self.2 fun hxs => _
α : Type u_1
β : Type ?u.188274
ι : Type ?u.188277
G : Type ?u.188280
M : Type u_2
N : Type ?u.188286
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
this : mulSupport (mulIndicator s f) ⊆ ↑t
x : α
hx : x ∈ t
hxs : f x ≠ 1
⊢ x ∈ {x | p x}
α : Type u_1
β : Type ?u.188274
ι : Type ?u.188277
G : Type ?u.188280
M : Type u_2
N : Type ?u.188286
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
this : mulSupport (mulIndicator s f) ⊆ ↑t
x : α
hx : x ∈ t
hxs : ¬x ∈ s
⊢ f x = 1
contrapose! hxs
no goals
α : Type u_1
β : Type ?u.188274
ι : Type ?u.188277
G : Type ?u.188280
M : Type u_2
N : Type ?u.188286
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
this : mulSupport (mulIndicator s f) ⊆ ↑t
x : α
hx : x ∈ t
hxs : f x ≠ 1
⊢ x ∈ {x | p x}
exact (h hxs).2 hx
α : Type u_1
β : Type ?u.188274
ι : Type ?u.188277
G : Type ?u.188280
M : Type u_2
N : Type ?u.188286
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
⊢ s ∩ mulSupport f ⊆ ↑t
α : Type u_1
β : Type ?u.188274
ι : Type ?u.188277
G : Type ?u.188280
M : Type u_2
N : Type ?u.188286
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
⊢ mulSupport (mulIndicator s f) ⊆ ↑t
rw [Set.mulSupport_mulIndicator]
α : Type u_1
β : Type ?u.188274
ι : Type ?u.188277
G : Type ?u.188280
M : Type u_2
N : Type ?u.188286
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
x : α
hx : x ∈ s ∩ mulSupport f
⊢ x ∈ ↑t
α : Type u_1
β : Type ?u.188274
ι : Type ?u.188277
G : Type ?u.188280
M : Type u_2
N : Type ?u.188286
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
⊢ s ∩ mulSupport f ⊆ ↑t
intro x hx
no goals
α : Type u_1
β : Type ?u.188274
ι : Type ?u.188277
G : Type ?u.188280
M : Type u_2
N : Type ?u.188286
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
f : α → M
p : α → Prop
t : Finset α
h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)
s : Set α := {x | p x}
x : α
hx : x ∈ s ∩ mulSupport f
⊢ x ∈ ↑t
exact (h hx.2).1 hx.1