intro el
case h.a.mpr
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) }
pw : ↑(𝒫 Set.univ)
a : ↑indicator' :=
  Eq.mpr (_ : ↑indicator' = ↑Set.univ)
    {
      val := fun x =>
        let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
        if x ∈ real_set then binary.one else binary.zero,
      property :=
        (_ :
          (fun x =>
              let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
              if x ∈ real_set then binary.one else binary.zero) ∈
            Set.univ) }
x : ℝ
⊢ x ∈ ↑pw → (if x ∈ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw) then binary.one else binary.zero) = binary.one
case h.a.mpr
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) }
pw : ↑(𝒫 Set.univ)
a : ↑indicator' :=
  Eq.mpr (_ : ↑indicator' = ↑Set.univ)
    {
      val := fun x =>
        let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
        if x ∈ real_set then binary.one else binary.zero,
      property :=
        (_ :
          (fun x =>
              let_fun real_set := ↑(Eq.mp (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw);
              if x ∈ real_set then binary.one else binary.zero) ∈
            Set.univ) }
x : ℝ
el : x ∈ ↑pw
⊢ (if x ∈ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw) then binary.one else binary.zero) = binary.one