simp [indicator_of_mem ha]
case mk
α✝ : Type u_1
β✝ : Type u_2
ι : Type u_3
s✝ : Set α✝
α : Type u_4
β : Type u_5
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : AddCommMonoid β
inst✝ : T2Space β
s : Set α
a : α
ha : a ∈ s
⊢ f ↑⟨a, ha⟩ = s.indicator f ↑⟨a, ha⟩
no goals