awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
n : ℕ
h : ¬Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n)ᶜᶜ : ENNReal) (0 : ENNReal)
have neg : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (0 : ENNReal)
Tactic: rw [compl_compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
n : ℕ
h : ¬Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (0 : ENNReal)
have neg : ∀ (h₀ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (0 : ENNReal)),
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (0 : ENNReal)
Tactic: rcases μ.zero_one (A n) with (h₀ | h₁)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
n : ℕ
h : ¬Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal)
neg :
  ∀ (h₀ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (0 : ENNReal)),
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (0 : ENNReal)
have neg₁ : ∀ (h₁ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal)),
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (0 : ENNReal)
Tactic: rcases μ.zero_one (A n) with (h₀ | h₁)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
⊢ ∃ (x₀ : α), μ = Measure.dirac x₀
have hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
Tactic: have hBn : μ (⋂ n, B n) = 1 := by
    refine (prob_compl_eq_zero_iff mBn).mp ?_
    simp only [dite_eq_ite, compl_iInter, measure_iUnion_null_iff, B]
    intro n
    split_ifs with h
    · simp_all
    · rw [compl_compl]
      rcases μ.zero_one (A n) with (h₀ | h₁)
      · exact h₀
      · simp_all
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
⊢ ∃ (x₀ : α), Eq (α := Set α) (⋂ (n : ℕ), B n) {x₀}
have simp_rw : ∃ (x₀ : α),
  Membership.mem (γ := Set α) (⋂ (n : ℕ), B n) x₀ ∧ ∀ (x : α), Membership.mem (γ := Set α) (⋂ (n : ℕ), B n) x → x = x₀
Tactic: simp_rw [eq_singleton_iff_unique_mem]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
⊢ Set.Nonempty.{u_1} (α := α) (⋂ (n : ℕ), B n)
have by_contra! : ∀ (h : Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), B n) ∅), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
h : Eq.{u_1 + 1} (α := Set α) (⋂ (n : ℕ), B n) ∅
⊢ False
have hBn₁ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) ∅ : ENNReal) (1 : ENNReal)
Tactic: rw [h] at hBn
Cleared hypotheses: hBn, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
⊢ ∃ (x₀ : α),
    Membership.mem (γ := Set α) (⋂ (n : ℕ), B n) x₀ ∧ ∀ (x : α), Membership.mem (γ := Set α) (⋂ (n : ℕ), B n) x → x = x₀
have neBn : Set.Nonempty.{u_1} (α := α) (⋂ (n : ℕ), B n)
Tactic: have neBn : (⋂ n, B n).Nonempty := by
      by_contra! h
      rw [h] at hBn
      simp_all
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
neBn : Set.Nonempty.{u_1} (α := α) (⋂ (n : ℕ), B n)
⊢ ∃ (x₀ : α),
    Membership.mem (γ := Set α) (⋂ (n : ℕ), B n) x₀ ∧ ∀ (x : α), Membership.mem (γ := Set α) (⋂ (n : ℕ), B n) x → x = x₀
have refine : ∀ (y : α) (hy : Membership.mem (γ := Set α) (⋂ (n : ℕ), B n) y), y = neBn.some (s := ⋂ (n : ℕ), B n)
Tactic: refine ⟨neBn.some, neBn.some_mem, fun y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
neBn : Set.Nonempty.{u_1} (α := α) (⋂ (n : ℕ), B n)
y : α
hy : Membership.mem (γ := Set α) (⋂ (n : ℕ), B n) y
⊢ y = neBn.some (s := ⋂ (n : ℕ), B n)
have refine : ∀ (n : ℕ), y ∈ A n ↔ neBn.some (s := ⋂ (n : ℕ), B n) ∈ A n
Tactic: refine hAsep y (by trivial) neBn.some (by trivial) fun n ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
neBn : Set.Nonempty.{u_1} (α := α) (⋂ (n : ℕ), B n)
y : α
hy : Membership.mem (γ := Set α) (⋂ (n : ℕ), B n) y
n : ℕ
⊢ y ∈ A n ↔ neBn.some (s := ⋂ (n : ℕ), B n) ∈ A n
have hsome : Membership.mem (γ := Set α) (⋂ (n : ℕ), B n) (neBn.some (s := ⋂ (n : ℕ), B n))
Tactic: have hsome := neBn.some_mem
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
neBn : Set.Nonempty.{u_1} (α := α) (⋂ (n : ℕ), B n)
y : α
hy : Membership.mem (γ := Set α) (⋂ (n : ℕ), B n) y
n : ℕ
hsome : Membership.mem (γ := Set α) (⋂ (n : ℕ), B n) (neBn.some (s := ⋂ (n : ℕ), B n))
⊢ y ∈ A n ↔ neBn.some (s := ⋂ (n : ℕ), B n) ∈ A n
have hsome₁ : ∀ (i : ℕ),
  sorry.some (s :=
      ⋂ (n : ℕ),
        if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ) ∈
    if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A i) : ENNReal) (1 : ENNReal) then A i else (A i)ᶜ
Tactic: simp only [dite_eq_ite, mem_iInter, B] at hsome hy
Cleared hypotheses: hy, hsome
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
neBn : Set.Nonempty.{u_1} (α := α) (⋂ (n : ℕ), B n)
y : α
hy : Membership.mem (γ := Set α) (⋂ (n : ℕ), B n) y
n : ℕ
hsome : Membership.mem (γ := Set α) (⋂ (n : ℕ), B n) (neBn.some (s := ⋂ (n : ℕ), B n))
hsome₁ :
  ∀ (i : ℕ),
    ⋯.some (s :=
        ⋂ (n : ℕ),
          if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ) ∈
      if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A i) : ENNReal) (1 : ENNReal) then A i else (A i)ᶜ
⊢ y ∈ A n ↔ neBn.some (s := ⋂ (n : ℕ), B n) ∈ A n
have hy₁ : ∀ (i : ℕ), y ∈ if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A i) : ENNReal) (1 : ENNReal) then A i else (A i)ᶜ
Tactic: simp only [dite_eq_ite, mem_iInter, B] at hsome hy
Cleared hypotheses: hy, hsome
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
neBn : Set.Nonempty.{u_1} (α := α) (⋂ (n : ℕ), B n)
y : α
n : ℕ
hsome :
  ∀ (i : ℕ),
    ⋯.some (s :=
        ⋂ (n : ℕ),
          if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ) ∈
      if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A i) : ENNReal) (1 : ENNReal) then A i else (A i)ᶜ
hy :
  ∀ (i : ℕ), y ∈ if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A i) : ENNReal) (1 : ENNReal) then A i else (A i)ᶜ
⊢ y ∈ A n ↔ neBn.some (s := ⋂ (n : ℕ), B n) ∈ A n
have hsome₁ : sorry.some (s :=
    ⋂ (n : ℕ), if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ) ∈
  if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
Tactic: specialize hsome n
Cleared hypotheses: hsome
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
neBn : Set.Nonempty.{u_1} (α := α) (⋂ (n : ℕ), B n)
y : α
n : ℕ
hy :
  ∀ (i : ℕ), y ∈ if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A i) : ENNReal) (1 : ENNReal) then A i else (A i)ᶜ
hsome :
  ⋯.some (s :=
      ⋂ (n : ℕ),
        if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ) ∈
    if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
⊢ y ∈ A n ↔ neBn.some (s := ⋂ (n : ℕ), B n) ∈ A n
have hy₁ : y ∈ if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
Tactic: specialize hy n
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
neBn : Set.Nonempty.{u_1} (α := α) (⋂ (n : ℕ), B n)
y : α
n : ℕ
hsome :
  ⋯.some (s :=
      ⋂ (n : ℕ),
        if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ) ∈
    if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
hy : y ∈ if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
⊢ y ∈ A n ↔ neBn.some (s := ⋂ (n : ℕ), B n) ∈ A n
have mp : y ∈ A n → neBn.some (s := ⋂ (n : ℕ), B n) ∈ A n
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
neBn : Set.Nonempty.{u_1} (α := α) (⋂ (n : ℕ), B n)
y : α
n : ℕ
hsome :
  ⋯.some (s :=
      ⋂ (n : ℕ),
        if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ) ∈
    if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
hy : y ∈ if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mp : y ∈ A n → neBn.some (s := ⋂ (n : ℕ), B n) ∈ A n
⊢ y ∈ A n ↔ neBn.some (s := ⋂ (n : ℕ), B n) ∈ A n
have mpr : neBn.some (s := ⋂ (n : ℕ), B n) ∈ A n → y ∈ A n
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
neBn : Set.Nonempty.{u_1} (α := α) (⋂ (n : ℕ), B n)
y : α
n : ℕ
hsome :
  ⋯.some (s :=
      ⋂ (n : ℕ),
        if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ) ∈
    if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
hy : y ∈ if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
h : y ∈ A n
⊢ neBn.some (s := ⋂ (n : ℕ), B n) ∈ A n
have pos : ∀ (hμAn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal)) (hy : y ∈ A n),
  neBn.some (s := ⋂ (n : ℕ), B n) ∈ A n
Tactic: split_ifs at hy with hμAn
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
inst_1 : StandardBorelSpace α
inst_2 : NeZero μ
this : IsProbabilityMeasure μ
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAsep :
  ∀ (x : α),
    Membership.mem (γ := Set α) univ x →
      ∀ (y : α), Membership.mem (γ := Set α) univ y → (∀ (n : ℕ), x ∈ A n ↔ y ∈ A n) → x = y
B : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦
    if h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
hBn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
neBn : Set.Nonempty.{u_1} (α := α) (⋂ (n : ℕ), B n)
y : α
n : ℕ
hsome :
  ⋯.some (s :=
      ⋂ (n : ℕ),
        if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ) ∈
    if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
hy : y ∈ if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ
h : y ∈ A n
pos :
  ∀ (hμAn : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal)) (hy : y ∈ A n),
    neBn.some (s := ⋂ (n : ℕ), B n) ∈ A n
⊢ neBn.some (s := ⋂ (n : ℕ), B n) ∈ A n
have neg : ∀ (hμAn : ¬Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal)) (hy : y ∈ (A n)ᶜ),
  neBn.some (s := ⋂ (n : ℕ), B n) ∈ A n
Tactic: split_ifs at hy with hμAn
Cleared hypotheses: hy