Theorem: indicator_card_eq_powerset_card_bij (meetings/ex5.lean)

State before:
⊢ ∃ f, Function.Bijective f
Tactic:
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]
  }
State after:
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

State before:
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
Tactic:
use f
State after:
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) }
⊢ Function.Bijective f

State before:
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) }
⊢ Function.Bijective f
Tactic:
constructor
State after:
case h.left
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) }
⊢ Function.Injective f

case h.right
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) }
⊢ Function.Surjective f

State before:
⊢ ↑indicator' → ↑(𝒫 Set.univ)
Tactic:
rw [indicator']
State after:
⊢ ↑Set.univ → ↑(𝒫 Set.univ)

State before:
⊢ ↑Set.univ → ↑(𝒫 Set.univ)
Tactic:
rintro ⟨fn, _⟩
State after:
case mk
fn : ℝ → binary
property✝ : fn ∈ Set.univ
⊢ ↑(𝒫 Set.univ)

State before:
case mk
fn : ℝ → binary
property✝ : fn ∈ Set.univ
⊢ ↑(𝒫 Set.univ)
Tactic:
exact {
  val := Set.preimage fn {binary.one}
  property := by simp only [Set.powerset_univ, Set.mem_univ]
}
State after:
no goals

State before:
fn : ℝ → binary
property✝ : fn ∈ Set.univ
⊢ fn ⁻¹' {binary.one} ∈ 𝒫 Set.univ
Tactic:
simp only [Set.powerset_univ, Set.mem_univ]
State after:
no goals

State before:
case h.left
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) }
⊢ Function.Injective f
Tactic:
rintro ⟨fa, _⟩ ⟨fb, _⟩ heq
State after:
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✝ }
⊢ { val := fa, property := property✝¹ } = { val := fb, property := property✝ }

State before:
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✝ }
⊢ { val := fa, property := property✝¹ } = { val := fb, property := property✝ }
Tactic:
simp only [Set.powerset_univ] at f
State after:
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✝ }

State before:
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✝ }
Tactic:
simp only [eq_mpr_eq_cast, cast_eq, Subtype.mk.injEq] at heq
State after:
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✝ }

State before:
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✝ }
Tactic:
rw [Set.ext_iff] at heq
State after:
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 : ∀ (x : ℝ), x ∈ fa ⁻¹' {binary.one} ↔ x ∈ fb ⁻¹' {binary.one}
⊢ { val := fa, property := property✝¹ } = { val := fb, property := property✝ }

State before:
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 : ∀ (x : ℝ), x ∈ fa ⁻¹' {binary.one} ↔ x ∈ fb ⁻¹' {binary.one}
⊢ { val := fa, property := property✝¹ } = { val := fb, property := property✝ }
Tactic:
simp only [Set.mem_preimage, Set.mem_singleton_iff] at heq
State after:
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 : ∀ (x : ℝ), fa x = binary.one ↔ fb x = binary.one
⊢ { val := fa, property := property✝¹ } = { val := fb, property := property✝ }

State before:
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 : ∀ (x : ℝ), fa x = binary.one ↔ fb x = binary.one
heqv : fa = fb
⊢ { val := fa, property := property✝¹ } = { val := fb, property := property✝ }
Tactic:
exact SetCoe.ext heqv
State after:
no goals

State before:
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 : ∀ (x : ℝ), fa x = binary.one ↔ fb x = binary.one
⊢ fa = fb
Tactic:
ext x
State after:
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) }
fa : ℝ → binary
property✝¹ : fa ∈ indicator'
fb : ℝ → binary
property✝ : fb ∈ indicator'
f : ↑indicator' → ↑Set.univ
heq : ∀ (x : ℝ), fa x = binary.one ↔ fb x = binary.one
x : ℝ
⊢ fa x = fb x

State before:
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) }
fa : ℝ → binary
property✝¹ : fa ∈ indicator'
fb : ℝ → binary
property✝ : fb ∈ indicator'
f : ↑indicator' → ↑Set.univ
heq : ∀ (x : ℝ), fa x = binary.one ↔ fb x = binary.one
x : ℝ
⊢ fa x = fb x
Tactic:
specialize heq x
State after:
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) }
fa : ℝ → binary
property✝¹ : fa ∈ indicator'
fb : ℝ → binary
property✝ : fb ∈ indicator'
f : ↑indicator' → ↑Set.univ
x : ℝ
heq : fa x = binary.one ↔ fb x = binary.one
⊢ fa x = fb x

State before:
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) }
fa : ℝ → binary
property✝¹ : fa ∈ indicator'
fb : ℝ → binary
property✝ : fb ∈ indicator'
f : ↑indicator' → ↑Set.univ
x : ℝ
heq : fa x = binary.one ↔ fb x = binary.one
⊢ fa x = fb x
Tactic:
have hzero_iff := binary_zero_eq_iff_one_eq heq
State after:
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) }
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
⊢ fa x = fb x

State before:
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) }
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
⊢ fa x = fb x
Tactic:
by_cases heqfa : fa x = binary.one
State after:
case pos
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
⊢ fa x = fb x

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
⊢ fa x = fb x

State before:
case pos
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
⊢ fa x = fb x
Tactic:
have heqfbzero := heq.mp heqfa
State after:
case pos
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
heqfbzero : fb x = binary.one
⊢ fa x = fb x

State before:
case pos
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
heqfbzero : fb x = binary.one
⊢ fa x = fb x
Tactic:
rw [←heqfbzero] at heqfa
State after:
case pos
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 = fb x
heqfbzero : fb x = binary.one
⊢ fa x = fb x

State before:
case pos
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 = fb x
heqfbzero : fb x = binary.one
⊢ fa x = fb x
Tactic:
exact heqfa
State after:
no goals

State before:
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
⊢ fa x = fb x
Tactic:
have heqfazero := binary_ne_one_eq_zero heqfa
State after:
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 = binary.zero
⊢ fa x = fb x

State before:
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 = binary.zero
⊢ fa x = fb x
Tactic:
have heqfbone := hzero_iff.mp heqfazero
State after:
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 = binary.zero
heqfbone : fb x = binary.zero
⊢ fa x = fb x

State before:
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 = binary.zero
heqfbone : fb x = binary.zero
⊢ fa x = fb x
Tactic:
rw [←heqfbone] at heqfazero
State after:
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

State before:
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
Tactic:
exact heqfazero
State after:
no goals

State before:
case h.right
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) }
⊢ Function.Surjective f
Tactic:
intro pw
State after:
case h.right
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, f a = pw

State before:
case h.right
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) }
⊢ ∃ a, f a = pw
Tactic:
use a
State after:
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) }
⊢ f a = pw

State before:
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) }
⊢ f a = pw
Tactic:
simp only [eq_mpr_eq_cast, cast_eq, eq_mp_eq_cast, Set.powerset_univ, set_coe_cast]
State after:
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

State before:
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
Tactic:
apply Subtype.eq
State after:
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

State before:
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
Tactic:
simp only [Set.powerset_univ, set_coe_cast, Set.ext_iff]
State after:
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) }
⊢ ∀ (x : ℝ),
    x ∈ (fun x => if x ∈ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw) then binary.one else binary.zero) ⁻¹' {binary.one} ↔
      x ∈ ↑pw

State before:
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) }
⊢ ∀ (x : ℝ),
    x ∈ (fun x => if x ∈ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw) then binary.one else binary.zero) ⁻¹' {binary.one} ↔
      x ∈ ↑pw
Tactic:
intro x
State after:
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) }
x : ℝ
⊢ x ∈ (fun x => if x ∈ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw) then binary.one else binary.zero) ⁻¹' {binary.one} ↔
    x ∈ ↑pw

State before:
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) }
x : ℝ
⊢ x ∈ (fun x => if x ∈ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw) then binary.one else binary.zero) ⁻¹' {binary.one} ↔
    x ∈ ↑pw
Tactic:
simp only [Set.powerset_univ, set_coe_cast, Set.mem_preimage, Set.mem_singleton_iff]
State after:
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) }
x : ℝ
⊢ (if x ∈ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw) then binary.one else binary.zero) = binary.one ↔ x ∈ ↑pw

State before:
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) }
x : ℝ
⊢ (if x ∈ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw) then binary.one else binary.zero) = binary.one ↔ x ∈ ↑pw
Tactic:
constructor
State after:
case h.a.mp
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 : ℝ
⊢ (if x ∈ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw) then binary.one else binary.zero) = binary.one → x ∈ ↑pw

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

State before:
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)
⊢ ↑indicator'
Tactic:
rw [indicator']
State after:
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)
⊢ ↑Set.univ

State before:
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)
⊢ ↑Set.univ
Tactic:
constructor
State after:
case property
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)
⊢ ?val ∈ Set.univ

case val
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)
⊢ ℝ → binary

State before:
case property
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)
⊢ ?val ∈ Set.univ
Tactic:
simp only [Set.mem_univ]
State after:
no goals

State before:
case val
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)
⊢ ℝ → binary
Tactic:
intro x
State after:
case val
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)
x : ℝ
⊢ binary

State before:
case val
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)
x : ℝ
⊢ binary
Tactic:
simp only [Set.powerset_univ] at pw
State after:
case val
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) }
x : ℝ
pw : ↑Set.univ
⊢ binary

State before:
case val
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) }
x : ℝ
pw : ↑Set.univ
⊢ binary
Tactic:
have real_set := pw.1
State after:
case val
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) }
x : ℝ
pw : ↑Set.univ
real_set : Set ℝ
⊢ binary

State before:
case val
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) }
x : ℝ
pw : ↑Set.univ
real_set : Set ℝ
⊢ binary
Tactic:
haveI := Classical.dec (x ∈ real_set)
State after:
case val
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) }
x : ℝ
pw : ↑Set.univ
real_set : Set ℝ
this : Decidable (x ∈ real_set)
⊢ binary

State before:
case val
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) }
x : ℝ
pw : ↑Set.univ
real_set : Set ℝ
this : Decidable (x ∈ real_set)
⊢ binary
Tactic:
exact (ite (x ∈ real_set) binary.one binary.zero)
State after:
no goals

State before:
case h.a.mp
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 : ℝ
⊢ (if x ∈ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw) then binary.one else binary.zero) = binary.one → x ∈ ↑pw
Tactic:
intro hite
State after:
case h.a.mp
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 : ℝ
hite : (if x ∈ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw) then binary.one else binary.zero) = binary.one
⊢ x ∈ ↑pw

State before:
case h.a.mp
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 : ℝ
hite : (if x ∈ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw) then binary.one else binary.zero) = binary.one
⊢ x ∈ ↑pw
Tactic:
split_ifs at hite with hi
State after:
case pos
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 : ℝ
hi : x ∈ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw)
hite : binary.one = binary.one
⊢ x ∈ ↑pw

State before:
case pos
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 : ℝ
hi : x ∈ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw)
hite : binary.one = binary.one
⊢ x ∈ ↑pw
Tactic:
simp only [Set.powerset_univ, set_coe_cast] at hi
State after:
case pos
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 : ℝ
hite : binary.one = binary.one
hi : x ∈ ↑pw
⊢ x ∈ ↑pw

State before:
case pos
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 : ℝ
hite : binary.one = binary.one
hi : x ∈ ↑pw
⊢ x ∈ ↑pw
Tactic:
exact hi
State after:
no goals

State before:
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
Tactic:
intro el
State after:
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

State before:
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
Tactic:
split_ifs with hi
State after:
case pos
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
hi : x ∈ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw)
⊢ binary.one = binary.one

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) }
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
hi : x ∉ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw)
⊢ False

State before:
case pos
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
hi : x ∈ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw)
⊢ binary.one = binary.one
Tactic:
rfl
State after:
no goals

State before:
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) }
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
hi : x ∉ ↑(cast (_ : ↑(𝒫 Set.univ) = ↑Set.univ) pw)
⊢ False
Tactic:
simp only [Set.powerset_univ, set_coe_cast] at hi
State after:
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) }
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
hi : x ∉ ↑pw
⊢ False

State before:
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) }
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
hi : x ∉ ↑pw
⊢ False
Tactic:
exact hi el
State after:
no goals