no goals
α : Type u_1
β : Type ?u.15893
ι : Type ?u.15896
M : Type u_2
N : Type ?u.15902
inst✝¹ : One M
inst✝ : One N
s✝ t : Set α
f✝ g : α → M
a : α
s : Set α
f : α → M
⊢ mulIndicator (s ∩ mulSupport f) f = mulIndicator s f
rw [← mulIndicator_mulIndicator, mulIndicator_mulSupport]