internlm/Lean-Github huggingface dataset:
Theorem: binary_zero_eq_iff_one_eq
Proof state before:
case zero
a : binary
hb : ¬a = binary.one
⊢ True ↔ a = binary.zero
Tactic:
cases a
Proof state after:
case zero.zero
hb : ¬binary.zero = binary.one
⊢ True ↔ binary.zero = binary.zero

case zero.one
hb : ¬binary.one = binary.one
⊢ True ↔ binary.one = binary.zero
Theorem: binary_zero_eq_iff_one_eq
Proof state before:
case zero.zero
hb : ¬binary.zero = binary.one
⊢ True ↔ binary.zero = binary.zero
Tactic:
simp only
Proof state after:
no goals
Theorem: binary_zero_eq_iff_one_eq
Proof state before:
case zero.one
hb : ¬binary.one = binary.one
⊢ True ↔ binary.one = binary.zero
Tactic:
simp only [not_true_eq_false] at *
Proof state after:
no goals
Theorem: binary_zero_eq_iff_one_eq
Proof state before:
case one
a : binary
hb : binary.one = binary.one ↔ a = binary.one
⊢ binary.one = binary.zero ↔ a = binary.zero
Tactic:
simp only [true_iff, false_iff] at *
Proof state after:
case one
a : binary
hb : a = binary.one
⊢ ¬a = binary.zero
Theorem: binary_zero_eq_iff_one_eq
Proof state before:
case one
a : binary
hb : a = binary.one
⊢ ¬a = binary.zero
Tactic:
cases a
Proof state after:
case one.zero
hb : binary.zero = binary.one
⊢ ¬binary.zero = binary.zero

case one.one
hb : binary.one = binary.one
⊢ ¬binary.one = binary.zero
Theorem: binary_zero_eq_iff_one_eq
Proof state before:
case one.zero
hb : binary.zero = binary.one
⊢ ¬binary.zero = binary.zero
Tactic:
simp only at *
Proof state after:
no goals
Theorem: binary_zero_eq_iff_one_eq
Proof state before:
case one.one
hb : binary.one = binary.one
⊢ ¬binary.one = binary.zero
Tactic:
simp only [not_false_eq_true]
Proof state after:
no goals
Theorem: binary_ne_one_eq_zero
Proof state before:
b : binary
hb : ¬b = binary.one
⊢ b = binary.zero
Tactic:
cases b
Proof state after:
case zero
hb : ¬binary.zero = binary.one
⊢ binary.zero = binary.zero

case one
hb : ¬binary.one = binary.one
⊢ binary.one = binary.zero
Theorem: binary_ne_one_eq_zero
Proof state before:
case zero
hb : ¬binary.zero = binary.one
⊢ binary.zero = binary.zero
Tactic:
simp only
Proof state after:
no goals
Theorem: binary_ne_one_eq_zero
Proof state before:
case one
hb : ¬binary.one = binary.one
⊢ binary.one = binary.zero
Tactic:
simp only [not_true_eq_false] at *
Proof state after:
no goals
Theorem: indicator_card_eq_powerset_card_bij
Proof 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]
  }
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) }
⊢ ∃ f, Function.Bijective f
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) }
⊢ ∃ f, Function.Bijective f
Tactic:
use f
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) }
⊢ Function.Bijective f
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) }
⊢ Function.Bijective f
Tactic:
constructor
Proof 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
Theorem: indicator_card_eq_powerset_card_bij
Proof state before:
⊢ ↑indicator' → ↑(𝒫 Set.univ)
Tactic:
rw [indicator']
Proof state after:
⊢ ↑Set.univ → ↑(𝒫 Set.univ)
Theorem: indicator_card_eq_powerset_card_bij
Proof state before:
⊢ ↑Set.univ → ↑(𝒫 Set.univ)
Tactic:
rintro ⟨fn, _⟩
Proof state after:
case mk
fn : ℝ → binary
property✝ : fn ∈ Set.univ
⊢ ↑(𝒫 Set.univ)
Theorem: indicator_card_eq_powerset_card_bij
Proof 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]
}
Proof state after:
no goals
Theorem: indicator_card_eq_powerset_card_bij
Proof state before:
fn : ℝ → binary
property✝ : fn ∈ Set.univ
⊢ fn ⁻¹' {binary.one} ∈ 𝒫 Set.univ
Tactic:
simp only [Set.powerset_univ, Set.mem_univ]
Proof state after:
no goals
Theorem: indicator_card_eq_powerset_card_bij
Proof 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
Proof 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✝ }
Theorem: indicator_card_eq_powerset_card_bij
Proof 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
Proof 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✝ }
Theorem: indicator_card_eq_powerset_card_bij
Proof 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
Proof 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✝ }
Theorem: indicator_card_eq_powerset_card_bij
Proof 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
Proof 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✝ }
Theorem: indicator_card_eq_powerset_card_bij
Proof 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
Proof 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✝ }
Theorem: indicator_card_eq_powerset_card_bij
Proof 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
Proof state after:
no goals
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) }
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
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) }
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
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) }
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
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) }
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
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) }
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
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) }
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
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) }
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
Proof 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
Theorem: indicator_card_eq_powerset_card_bij
Proof 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
Proof 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
Theorem: indicator_card_eq_powerset_card_bij
Proof 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
Proof 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
Theorem: indicator_card_eq_powerset_card_bij
Proof 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
Proof state after:
no goals
Theorem: indicator_card_eq_powerset_card_bij
Proof 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
Proof 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
Theorem: indicator_card_eq_powerset_card_bij
Proof 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
Proof 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
Theorem: indicator_card_eq_powerset_card_bij
Proof 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
Proof 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
Theorem: indicator_card_eq_powerset_card_bij
Proof 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
Proof state after:
no goals