apply Subtype.eq
case h
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) }
⊢ {
      val :=
        (fun x => if x ∈ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw) then binary.one else binary.zero) ⁻¹' {binary.one},
      property :=
        (_ :
          ↑{ val := fun x => if x ∈ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw) then binary.one else binary.zero,
                  property :=
                    (_ :
                      (fun x => x ∈ Set.univ) fun x =>
                        if x ∈ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw) then binary.one else binary.zero) } ⁻¹'
              {binary.one} ∈
            𝒫 Set.univ) } =
    pw
case h.a
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) }
⊢ ↑{
        val :=
          (fun x => if x ∈ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw) then binary.one else binary.zero) ⁻¹'
            {binary.one},
        property :=
          (_ :
            ↑{ val := fun x => if x ∈ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw) then binary.one else binary.zero,
                    property :=
                      (_ :
                        (fun x => x ∈ Set.univ) fun x =>
                          if x ∈ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw) then binary.one else binary.zero) } ⁻¹'
                {binary.one} ∈
              𝒫 Set.univ) } =
    ↑pw