case h
α : Type u_1
β : Type ?u.72118
ι : Type ?u.72121
M : Type u_2
N : Type ?u.72127
inst✝¹ : MulOneClass M
s t : Set α
f✝ g✝ : α → M
a : α
inst✝ : DecidablePred fun x => x ∈ s
f g : α → M
x : α
⊢ (mulIndicator s f * mulIndicator (sᶜ) g) x = piecewise s f g x
α : Type u_1
β : Type ?u.72118
ι : Type ?u.72121
M : Type u_2
N : Type ?u.72127
inst✝¹ : MulOneClass M
s t : Set α
f✝ g✝ : α → M
a : α
inst✝ : DecidablePred fun x => x ∈ s
f g : α → M
⊢ mulIndicator s f * mulIndicator (sᶜ) g = piecewise s f g
ext x
case pos
α : Type u_1
β : Type ?u.72118
ι : Type ?u.72121
M : Type u_2
N : Type ?u.72127
inst✝¹ : MulOneClass M
s t : Set α
f✝ g✝ : α → M
a : α
inst✝ : DecidablePred fun x => x ∈ s
f g : α → M
x : α
h : x ∈ s
⊢ (mulIndicator s f * mulIndicator (sᶜ) g) x = piecewise s f g x

case neg
α : Type u_1
β : Type ?u.72118
ι : Type ?u.72121
M : Type u_2
N : Type ?u.72127
inst✝¹ : MulOneClass M
s t : Set α
f✝ g✝ : α → M
a : α
inst✝ : DecidablePred fun x => x ∈ s
f g : α → M
x : α
h : ¬x ∈ s
⊢ (mulIndicator s f * mulIndicator (sᶜ) g) x = piecewise s f g x
case h
α : Type u_1
β : Type ?u.72118
ι : Type ?u.72121
M : Type u_2
N : Type ?u.72127
inst✝¹ : MulOneClass M
s t : Set α
f✝ g✝ : α → M
a : α
inst✝ : DecidablePred fun x => x ∈ s
f g : α → M
x : α
⊢ (mulIndicator s f * mulIndicator (sᶜ) g) x = piecewise s f g x
by_cases h : x ∈ s
no goals
case pos
α : Type u_1
β : Type ?u.72118
ι : Type ?u.72121
M : Type u_2
N : Type ?u.72127
inst✝¹ : MulOneClass M
s t : Set α
f✝ g✝ : α → M
a : α
inst✝ : DecidablePred fun x => x ∈ s
f g : α → M
x : α
h : x ∈ s
⊢ (mulIndicator s f * mulIndicator (sᶜ) g) x = piecewise s f g x
rw [piecewise_eq_of_mem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_mem h,
  Set.mulIndicator_of_not_mem (Set.not_mem_compl_iff.2 h), mul_one]
no goals
case neg
α : Type u_1
β : Type ?u.72118
ι : Type ?u.72121
M : Type u_2
N : Type ?u.72127
inst✝¹ : MulOneClass M
s t : Set α
f✝ g✝ : α → M
a : α
inst✝ : DecidablePred fun x => x ∈ s
f g : α → M
x : α
h : ¬x ∈ s
⊢ (mulIndicator s f * mulIndicator (sᶜ) g) x = piecewise s f g x
rw [piecewise_eq_of_not_mem _ _ _ h, Pi.mul_apply, Set.mulIndicator_of_not_mem h,
  Set.mulIndicator_of_mem (Set.mem_compl h), one_mul]