no goals
α : Type u_2
β : Type ?u.95909
ι : Type ?u.95912
M : Type ?u.95915
N : Type ?u.95918
G✝ : Type ?u.95921
inst✝¹ : Group G✝
s✝ t : Set α
f✝ g : α → G✝
a : α
G : Type u_1
inst✝ : AddGroup G
s : Set α
f : α → G
⊢ indicator (sᶜ) f = f - indicator s f
rw [sub_eq_add_neg, indicator_compl']