no goals
α : Type u_1
β : Type ?u.49319
ι : Type ?u.49322
M : Type u_2
N : Type ?u.49328
inst✝ : MulOneClass M
s t : Set α
f✝ g : α → M
a : α
h : ¬a ∈ s ∩ t
f : α → M
⊢ mulIndicator (s ∪ t) f a = mulIndicator s f a * mulIndicator t f a
rw [← mulIndicator_union_mul_inter_apply f s t, mulIndicator_of_not_mem h, mul_one]