-- Mathlib/Algebra/BigOperators/Pi.lean
lemma prod_indicator_apply (s : Finset ι) (f : ι → Set κ) (g : ι → κ → α) (j : κ) :
    ∏ i ∈ s, (f i).indicator (g i) j = (⋂ x ∈ s, f x).indicator (∏ i ∈ s, g i) j

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝ : CommSemiring α
s : Finset ι
f : ι → Set κ
g : ι → κ → α
j : κ
⊢ ∏ i ∈ s, (f i).indicator (g i) j = (⋂ x ∈ s, f x).indicator (∏ i ∈ s, g i) j

Tactic:
rw [Set.indicator]

Result:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝ : CommSemiring α
s : Finset ι
f : ι → Set κ
g : ι → κ → α
j : κ
⊢ ∏ i ∈ s, (f i).indicator (g i) j = if j ∈ ⋂ x ∈ s, f x then (∏ i ∈ s, g i) j else 0

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝ : CommSemiring α
s : Finset ι
f : ι → Set κ
g : ι → κ → α
j : κ
⊢ ∏ i ∈ s, (f i).indicator (g i) j = if j ∈ ⋂ x ∈ s, f x then (∏ i ∈ s, g i) j else 0

Tactic:
split_ifs with hj

Result:
case pos
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝ : CommSemiring α
s : Finset ι
f : ι → Set κ
g : ι → κ → α
j : κ
hj : j ∈ ⋂ x ∈ s, f x
⊢ ∏ i ∈ s, (f i).indicator (g i) j = (∏ i ∈ s, g i) j

case neg
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝ : CommSemiring α
s : Finset ι
f : ι → Set κ
g : ι → κ → α
j : κ
hj : j ∉ ⋂ x ∈ s, f x
⊢ ∏ i ∈ s, (f i).indicator (g i) j = 0

Proof state:
case neg
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝ : CommSemiring α
s : Finset ι
f : ι → Set κ
g : ι → κ → α
j : κ
hj : j ∉ ⋂ x ∈ s, f x
⊢ ∏ i ∈ s, (f i).indicator (g i) j = 0

Tactic:
obtain ⟨i, hi, hj⟩ := by simpa using hj

Result:
case neg.intro.intro
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝ : CommSemiring α
s : Finset ι
f : ι → Set κ
g : ι → κ → α
j : κ
hj✝ : j ∉ ⋂ x ∈ s, f x
i : ι
hi : i ∈ s
hj : j ∉ f i
⊢ ∏ i ∈ s, (f i).indicator (g i) j = 0

Proof state:
case pos.a
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝ : CommSemiring α
s : Finset ι
f : ι → Set κ
g : ι → κ → α
j : κ
i : ι
hi : i ∈ s
hj : ∀ i ∈ s, j ∈ f i
⊢ (f i).indicator (g i) j = g i j

Tactic:
exact Set.indicator_of_mem (hj _ hi) _

Result:
no goals

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝ : CommSemiring α
s : Finset ι
f : ι → Set κ
g : ι → κ → α
j : κ
hj : j ∉ ⋂ x ∈ s, f x
⊢ ?m.11121

Tactic:
simpa using hj

Result:
no goals

Proof state:
case pos
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝ : CommSemiring α
s : Finset ι
f : ι → Set κ
g : ι → κ → α
j : κ
hj : j ∈ ⋂ x ∈ s, f x
⊢ ∏ i ∈ s, (f i).indicator (g i) j = ∏ c ∈ s, g c j

Tactic:
congr! 1 with i hi

Result:
case pos.a
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝ : CommSemiring α
s : Finset ι
f : ι → Set κ
g : ι → κ → α
j : κ
hj : j ∈ ⋂ x ∈ s, f x
i : ι
hi : i ∈ s
⊢ (f i).indicator (g i) j = g i j

Proof state:
case pos
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝ : CommSemiring α
s : Finset ι
f : ι → Set κ
g : ι → κ → α
j : κ
hj : j ∈ ⋂ x ∈ s, f x
⊢ ∏ i ∈ s, (f i).indicator (g i) j = (∏ i ∈ s, g i) j

Tactic:
rw [Finset.prod_apply]

Result:
case pos
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝ : CommSemiring α
s : Finset ι
f : ι → Set κ
g : ι → κ → α
j : κ
hj : j ∈ ⋂ x ∈ s, f x
⊢ ∏ i ∈ s, (f i).indicator (g i) j = ∏ c ∈ s, g c j

Proof state:
case neg.intro.intro
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝ : CommSemiring α
s : Finset ι
f : ι → Set κ
g : ι → κ → α
j : κ
hj✝ : j ∉ ⋂ x ∈ s, f x
i : ι
hi : i ∈ s
hj : j ∉ f i
⊢ ∏ i ∈ s, (f i).indicator (g i) j = 0

Tactic:
exact Finset.prod_eq_zero hi <| Set.indicator_of_not_mem hj _

Result:
no goals

Proof state:
case pos.a
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝ : CommSemiring α
s : Finset ι
f : ι → Set κ
g : ι → κ → α
j : κ
hj : j ∈ ⋂ x ∈ s, f x
i : ι
hi : i ∈ s
⊢ (f i).indicator (g i) j = g i j

Tactic:
simp only [Finset.inf_set_eq_iInter, Set.mem_iInter] at hj

Result:
case pos.a
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝ : CommSemiring α
s : Finset ι
f : ι → Set κ
g : ι → κ → α
j : κ
i : ι
hi : i ∈ s
hj : ∀ i ∈ s, j ∈ f i
⊢ (f i).indicator (g i) j = g i j