internlm/Lean-Github huggingface dataset:
Theorem: indicator_card_eq_powerset_card_bij
Proof 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
Proof 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
Theorem: indicator_card_eq_powerset_card_bij
Proof 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
Proof 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
Theorem: indicator_card_eq_powerset_card_bij
Proof 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]
Proof 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
Theorem: indicator_card_eq_powerset_card_bij
Proof 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
Proof 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
Theorem: indicator_card_eq_powerset_card_bij
Proof 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]
Proof 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
Theorem: indicator_card_eq_powerset_card_bij
Proof 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
Proof 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
Theorem: indicator_card_eq_powerset_card_bij
Proof 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]
Proof 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
Theorem: indicator_card_eq_powerset_card_bij
Proof 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
Proof 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
Theorem: indicator_card_eq_powerset_card_bij
Proof 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']
Proof 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
Theorem: indicator_card_eq_powerset_card_bij
Proof 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
Proof 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
Theorem: indicator_card_eq_powerset_card_bij
Proof 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]
Proof state after:
no goals
Theorem: indicator_card_eq_powerset_card_bij
Proof 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
Proof 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
Theorem: indicator_card_eq_powerset_card_bij
Proof 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
Proof 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
Theorem: indicator_card_eq_powerset_card_bij
Proof 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
Proof 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
Theorem: indicator_card_eq_powerset_card_bij
Proof 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)
Proof 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
Theorem: indicator_card_eq_powerset_card_bij
Proof 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)
Proof state after:
no goals
Theorem: indicator_card_eq_powerset_card_bij
Proof 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
Proof 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