no goals
α : Type u_2
β : Type ?u.99527
ι : Type ?u.99530
M : Type ?u.99533
N : Type ?u.99536
G✝ : Type ?u.99539
inst✝¹ : Group G✝
s✝ t✝ : Set α
f✝ g : α → G✝
a : α
G : Type u_1
inst✝ : AddGroup G
s t : Set α
h : s ⊆ t
f : α → G
⊢ indicator (t \ s) f = indicator t f - indicator s f
rw [indicator_diff' h, sub_eq_add_neg]