exact heqfazero
case neg
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
x : ℝ
heq : fa x = binary.one ↔ fb x = binary.one
hzero_iff : fa x = binary.zero ↔ fb x = binary.zero
heqfa : ¬fa x = binary.one
heqfazero : fa x = fb x
heqfbone : fb x = binary.zero
⊢ fa x = fb x
no goals