α : Type u_2
β : Type ?u.100673
ι : Type ?u.100676
M : Type u_3
N : Type u_1
inst✝¹ : CommMonoid M
inst✝ : One N
f : α → N
g : α → N → M
s t : Finset α
h : s ⊆ t
hg : ∀ (a : α), g a 1 = 1
⊢ ∏ i in s, g i (f i) = ∏ x in s, g x (mulIndicator (↑s) f x)

α : Type u_2
β : Type ?u.100673
ι : Type ?u.100676
M : Type u_3
N : Type u_1
inst✝¹ : CommMonoid M
inst✝ : One N
f : α → N
g : α → N → M
s t : Finset α
h : s ⊆ t
hg : ∀ (a : α), g a 1 = 1
⊢ ∀ (x : α), x ∈ t → ¬x ∈ s → g x (mulIndicator (↑s) f x) = 1
α : Type u_2
β : Type ?u.100673
ι : Type ?u.100676
M : Type u_3
N : Type u_1
inst✝¹ : CommMonoid M
inst✝ : One N
f : α → N
g : α → N → M
s t : Finset α
h : s ⊆ t
hg : ∀ (a : α), g a 1 = 1
⊢ ∏ i in s, g i (f i) = ∏ i in t, g i (mulIndicator (↑s) f i)
rw [← Finset.prod_subset h _]
α : Type u_2
β : Type ?u.100673
ι : Type ?u.100676
M : Type u_3
N : Type u_1
inst✝¹ : CommMonoid M
inst✝ : One N
f : α → N
g : α → N → M
s t : Finset α
h : s ⊆ t
hg : ∀ (a : α), g a 1 = 1
⊢ ∀ (x : α), x ∈ s → g x (f x) = g x (mulIndicator (↑s) f x)
α : Type u_2
β : Type ?u.100673
ι : Type ?u.100676
M : Type u_3
N : Type u_1
inst✝¹ : CommMonoid M
inst✝ : One N
f : α → N
g : α → N → M
s t : Finset α
h : s ⊆ t
hg : ∀ (a : α), g a 1 = 1
⊢ ∏ i in s, g i (f i) = ∏ x in s, g x (mulIndicator (↑s) f x)
apply Finset.prod_congr rfl
α : Type u_2
β : Type ?u.100673
ι : Type ?u.100676
M : Type u_3
N : Type u_1
inst✝¹ : CommMonoid M
inst✝ : One N
f : α → N
g : α → N → M
s t : Finset α
h : s ⊆ t
hg : ∀ (a : α), g a 1 = 1
i : α
hi : i ∈ s
⊢ g i (f i) = g i (mulIndicator (↑s) f i)
α : Type u_2
β : Type ?u.100673
ι : Type ?u.100676
M : Type u_3
N : Type u_1
inst✝¹ : CommMonoid M
inst✝ : One N
f : α → N
g : α → N → M
s t : Finset α
h : s ⊆ t
hg : ∀ (a : α), g a 1 = 1
⊢ ∀ (x : α), x ∈ s → g x (f x) = g x (mulIndicator (↑s) f x)
intro i hi
case e_a
α : Type u_2
β : Type ?u.100673
ι : Type ?u.100676
M : Type u_3
N : Type u_1
inst✝¹ : CommMonoid M
inst✝ : One N
f : α → N
g : α → N → M
s t : Finset α
h : s ⊆ t
hg : ∀ (a : α), g a 1 = 1
i : α
hi : i ∈ s
⊢ f i = mulIndicator (↑s) f i
α : Type u_2
β : Type ?u.100673
ι : Type ?u.100676
M : Type u_3
N : Type u_1
inst✝¹ : CommMonoid M
inst✝ : One N
f : α → N
g : α → N → M
s t : Finset α
h : s ⊆ t
hg : ∀ (a : α), g a 1 = 1
i : α
hi : i ∈ s
⊢ g i (f i) = g i (mulIndicator (↑s) f i)
congr
case e_a
α : Type u_2
β : Type ?u.100673
ι : Type ?u.100676
M : Type u_3
N : Type u_1
inst✝¹ : CommMonoid M
inst✝ : One N
f : α → N
g : α → N → M
s t : Finset α
h : s ⊆ t
hg : ∀ (a : α), g a 1 = 1
i : α
hi : i ∈ s
⊢ mulIndicator (↑s) f i = f i
case e_a
α : Type u_2
β : Type ?u.100673
ι : Type ?u.100676
M : Type u_3
N : Type u_1
inst✝¹ : CommMonoid M
inst✝ : One N
f : α → N
g : α → N → M
s t : Finset α
h : s ⊆ t
hg : ∀ (a : α), g a 1 = 1
i : α
hi : i ∈ s
⊢ f i = mulIndicator (↑s) f i
symm
no goals
case e_a
α : Type u_2
β : Type ?u.100673
ι : Type ?u.100676
M : Type u_3
N : Type u_1
inst✝¹ : CommMonoid M
inst✝ : One N
f : α → N
g : α → N → M
s t : Finset α
h : s ⊆ t
hg : ∀ (a : α), g a 1 = 1
i : α
hi : i ∈ s
⊢ mulIndicator (↑s) f i = f i
exact mulIndicator_of_mem (α := α) hi f
α : Type u_2
β : Type ?u.100673
ι : Type ?u.100676
M : Type u_3
N : Type u_1
inst✝¹ : CommMonoid M
inst✝ : One N
f : α → N
g : α → N → M
s t : Finset α
h : s ⊆ t
hg : ∀ (a : α), g a 1 = 1
i : α
x✝ : i ∈ t
hn : ¬i ∈ s
⊢ g i (mulIndicator (↑s) f i) = 1
α : Type u_2
β : Type ?u.100673
ι : Type ?u.100676
M : Type u_3
N : Type u_1
inst✝¹ : CommMonoid M
inst✝ : One N
f : α → N
g : α → N → M
s t : Finset α
h : s ⊆ t
hg : ∀ (a : α), g a 1 = 1
⊢ ∀ (x : α), x ∈ t → ¬x ∈ s → g x (mulIndicator (↑s) f x) = 1
refine' fun i _ hn => _
case h.e'_2.h.e'_2
α : Type u_2
β : Type ?u.100673
ι : Type ?u.100676
M : Type u_3
N : Type u_1
inst✝¹ : CommMonoid M
inst✝ : One N
f : α → N
g : α → N → M
s t : Finset α
h : s ⊆ t
hg : ∀ (a : α), g a 1 = 1
i : α
x✝ : i ∈ t
hn : ¬i ∈ s
⊢ mulIndicator (↑s) f i = 1
α : Type u_2
β : Type ?u.100673
ι : Type ?u.100676
M : Type u_3
N : Type u_1
inst✝¹ : CommMonoid M
inst✝ : One N
f : α → N
g : α → N → M
s t : Finset α
h : s ⊆ t
hg : ∀ (a : α), g a 1 = 1
i : α
x✝ : i ∈ t
hn : ¬i ∈ s
⊢ g i (mulIndicator (↑s) f i) = 1
convert hg i
no goals
case h.e'_2.h.e'_2
α : Type u_2
β : Type ?u.100673
ι : Type ?u.100676
M : Type u_3
N : Type u_1
inst✝¹ : CommMonoid M
inst✝ : One N
f : α → N
g : α → N → M
s t : Finset α
h : s ⊆ t
hg : ∀ (a : α), g a 1 = 1
i : α
x✝ : i ∈ t
hn : ¬i ∈ s
⊢ mulIndicator (↑s) f i = 1
exact mulIndicator_of_not_mem (α := α) hn f