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

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