no goals
α : Type u_1
β : Type ?u.43706
ι : Type ?u.43709
M : Type u_2
N : Type ?u.43715
inst✝ : MulOneClass M
s✝ t✝ : Set α
f✝ g : α → M
a✝ : α
f : α → M
s t : Set α
a : α
⊢ mulIndicator (s ∪ t) f a * mulIndicator (s ∩ t) f a = mulIndicator s f a * mulIndicator t f a
by_cases hs : a ∈ s <;> by_cases ht : a ∈ t <;> simp [*]