simp only [eq_mpr_eq_cast, cast_eq, Subtype.mk.injEq] at heq
case h.left.mk.mk
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) }
fa : ℝ → binary
property✝¹ : fa ∈ indicator'
fb : ℝ → binary
property✝ : fb ∈ indicator'
heq : f✝ { val := fa, property := property✝¹ } = f✝ { val := fb, property := property✝ }
f : ↑indicator' → ↑Set.univ
⊢ { val := fa, property := property✝¹ } = { val := fb, property := property✝ }
case h.left.mk.mk
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) }
fa : ℝ → binary
property✝¹ : fa ∈ indicator'
fb : ℝ → binary
property✝ : fb ∈ indicator'
f : ↑indicator' → ↑Set.univ
heq : fa ⁻¹' {binary.one} = fb ⁻¹' {binary.one}
⊢ { val := fa, property := property✝¹ } = { val := fb, property := property✝ }