α : Type u_1
β : Type ?u.122704
ι : Type ?u.122707
M : Type u_2
N : Type ?u.122713
inst✝ : MulZeroClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
⊢ (if a ∈ s then f a * g a else 0) = f a * if a ∈ s then g a else 0
α : Type u_1
β : Type ?u.122704
ι : Type ?u.122707
M : Type u_2
N : Type ?u.122713
inst✝ : MulZeroClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
⊢ indicator s (fun a => f a * g a) a = f a * indicator s g a
simp only [indicator]
case inl
α : Type u_1
β : Type ?u.122704
ι : Type ?u.122707
M : Type u_2
N : Type ?u.122713
inst✝ : MulZeroClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
h✝ : a ∈ s
⊢ f a * g a = f a * g a

case inr
α : Type u_1
β : Type ?u.122704
ι : Type ?u.122707
M : Type u_2
N : Type ?u.122713
inst✝ : MulZeroClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
h✝ : ¬a ∈ s
⊢ 0 = f a * 0
α : Type u_1
β : Type ?u.122704
ι : Type ?u.122707
M : Type u_2
N : Type ?u.122713
inst✝ : MulZeroClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
⊢ (if a ∈ s then f a * g a else 0) = f a * if a ∈ s then g a else 0
split_ifs
no goals
case inr
α : Type u_1
β : Type ?u.122704
ι : Type ?u.122707
M : Type u_2
N : Type ?u.122713
inst✝ : MulZeroClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
h✝ : ¬a ∈ s
⊢ 0 = f a * 0
rw [mul_zero]
no goals
case inl
α : Type u_1
β : Type ?u.122704
ι : Type ?u.122707
M : Type u_2
N : Type ?u.122713
inst✝ : MulZeroClass M
s✝ t : Set α
f✝ g✝ : α → M
a : α
s : Set α
f g : α → M
h✝ : a ∈ s
⊢ f a * g a = f a * g a
rfl