α : Type u_1
β : Type ?u.124894
ι : Type ?u.124897
M : Type u_2
N : Type ?u.124903
inst✝ : MulZeroClass M
s t : Set α
f✝ g✝ : α → M
a : α
t1 t2 : Set α
f g : α → M
x : α
⊢ indicator t1 (indicator t2 fun x => f x * g x) x = indicator t1 f x * indicator t2 g x
α : Type u_1
β : Type ?u.124894
ι : Type ?u.124897
M : Type u_2
N : Type ?u.124903
inst✝ : MulZeroClass M
s t : Set α
f✝ g✝ : α → M
a : α
t1 t2 : Set α
f g : α → M
x : α
⊢ indicator (t1 ∩ t2) (fun x => f x * g x) x = indicator t1 f x * indicator t2 g x
rw [← Set.indicator_indicator]
α : Type u_1
β : Type ?u.124894
ι : Type ?u.124897
M : Type u_2
N : Type ?u.124903
inst✝ : MulZeroClass M
s t : Set α
f✝ g✝ : α → M
a : α
t1 t2 : Set α
f g : α → M
x : α
⊢ (if x ∈ t1 then if x ∈ t2 then f x * g x else 0 else 0) = (if x ∈ t1 then f x else 0) * if x ∈ t2 then g x else 0
α : Type u_1
β : Type ?u.124894
ι : Type ?u.124897
M : Type u_2
N : Type ?u.124903
inst✝ : MulZeroClass M
s t : Set α
f✝ g✝ : α → M
a : α
t1 t2 : Set α
f g : α → M
x : α
⊢ indicator t1 (indicator t2 fun x => f x * g x) x = indicator t1 f x * indicator t2 g x
simp_rw [indicator]
no goals
α : Type u_1
β : Type ?u.124894
ι : Type ?u.124897
M : Type u_2
N : Type ?u.124903
inst✝ : MulZeroClass M
s t : Set α
f✝ g✝ : α → M
a : α
t1 t2 : Set α
f g : α → M
x : α
⊢ (if x ∈ t1 then if x ∈ t2 then f x * g x else 0 else 0) = (if x ∈ t1 then f x else 0) * if x ∈ t2 then g x else 0
split_ifs <;> simp