@[simp]

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

@[simp]

theorem NNReal.coe_comp_indicator_one {α : Type u_1} (s : Set α) : (toReal ∘ s.indicator fun (x : α) => 1) = s.indicator fun (x : α) => 1