let f : indicator' → (𝒫 (Set.univ : Set ℝ)) := by
  rw [indicator']
  rintro ⟨fn, _⟩
  exact {
    val := Set.preimage fn {binary.one}
    property := by simp only [Set.powerset_univ, Set.mem_univ]
  }
⊢ ∃ f, Function.Bijective f
f : ↑indicator' → ↑(𝒫 Set.univ) :=
  Eq.mpr (_ : (↑indicator' → ↑(𝒫 Set.univ)) = (↑Set.univ → ↑(𝒫 Set.univ))) fun a =>
    Subtype.casesOn a fun fn property =>
      { val := fn ⁻¹' {binary.one}, property := (_ : fn ⁻¹' {binary.one} ∈ 𝒫 Set.univ) }
⊢ ∃ f, Function.Bijective f