@[simp]

theorem Complex.ofReal_indicator_one {α : Type u_1} (s : Set α) (x : α) : ↑(s.indicator (fun (x : α) => 1) x) = s.indicator (fun (x : α) => 1) x

@[simp]

theorem Complex.ofReal_comp_indicator_one {α : Type u_1} (s : Set α) : (ofReal ∘ s.indicator fun (x : α) => 1) = s.indicator fun (x : α) => 1