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 μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this_1 : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
inl :
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal) →
    (μ : (a : Set α) → ENNReal) (s ∩ t) =
      HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
        ((μ : (a : Set α) → ENNReal) t : ENNReal)
⊢ (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)
have inl₁ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal) →
  (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)
Tactic: cases μ.zero_one t
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this_1 : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
⊢ (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)
have inr : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal) →
  (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)
Tactic: cases μ.zero_one t
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this_1 : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
inr :
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal) →
    (μ : (a : Set α) → ENNReal) (s ∩ t) =
      HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
        ((μ : (a : Set α) → ENNReal) t : ENNReal)
⊢ (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)
have inr₁ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal) →
  (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)
Tactic: cases μ.zero_one t
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this_1 : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
h_1 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal)
⊢ (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)
have inl : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal) →
  (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)
Tactic: cases μ.zero_one (s ∩ t)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this_1 : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
h_1 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal)
inl :
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal) →
    (μ : (a : Set α) → ENNReal) (s ∩ t) =
      HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
        ((μ : (a : Set α) → ENNReal) t : ENNReal)
⊢ (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)
have inl₁ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal) →
  (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)
Tactic: cases μ.zero_one (s ∩ t)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this_1 : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
h_1 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
⊢ (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)
have inl : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal) →
  (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)
Tactic: cases μ.zero_one (s ∩ t)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this_1 : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
h_1 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
inl :
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal) →
    (μ : (a : Set α) → ENNReal) (s ∩ t) =
      HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
        ((μ : (a : Set α) → ENNReal) t : ENNReal)
⊢ (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)
have inl₁ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal) →
  (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)
Tactic: cases μ.zero_one (s ∩ t)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this_1 : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
h_1 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal)
⊢ (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)
have inr : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal) →
  (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)
Tactic: cases μ.zero_one (s ∩ t)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this_1 : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
h_1 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal)
inr :
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal) →
    (μ : (a : Set α) → ENNReal) (s ∩ t) =
      HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
        ((μ : (a : Set α) → ENNReal) t : ENNReal)
⊢ (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)
have inr₁ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal) →
  (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)
Tactic: cases μ.zero_one (s ∩ t)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this_1 : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
h_1 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
⊢ (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)
have inr : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal) →
  (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)
Tactic: cases μ.zero_one (s ∩ t)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this_1 : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
h_1 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
inr :
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal) →
    (μ : (a : Set α) → ENNReal) (s ∩ t) =
      HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
        ((μ : (a : Set α) → ENNReal) t : ENNReal)
⊢ (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)
have inr₁ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal) →
  (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)
Tactic: cases μ.zero_one (s ∩ t)
-- 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 μ
⊢ IsProbabilityMeasure μ
have inl : ∀ (h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (0 : ENNReal)), IsProbabilityMeasure μ
Tactic: rcases IsZeroOrProbabilityMeasure.measure_univ (μ := μ) 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 μ
inl : ∀ (h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (0 : ENNReal)), IsProbabilityMeasure μ
⊢ IsProbabilityMeasure μ
have inr : ∀ (h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal)), IsProbabilityMeasure μ
Tactic: rcases IsZeroOrProbabilityMeasure.measure_univ (μ := μ) 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 μ
⊢ ∃ (x₀ : α), μ = Measure.dirac x₀
have this : IsProbabilityMeasure μ
Tactic: have : IsProbabilityMeasure μ := by
    rcases IsZeroOrProbabilityMeasure.measure_univ (μ := μ) with (h | h)
    · simp_all
    · exact ⟨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 μ
⊢ ∃ (x₀ : α), μ = Measure.dirac x₀
have obtain : ∀ (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),
  ∃ (x₀ : α), μ = Measure.dirac x₀
Tactic: obtain ⟨A, hAm, hAsep⟩ := exists_seq_separating (α := α) MeasurableSet.univ univ
-- 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)ᶜ
⊢ MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
have refine : ∀ (n : ℕ), MeasurableSet (B n)
Tactic: refine MeasurableSet.iInter fun n ↦ ?_
-- 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)ᶜ
n : ℕ
⊢ MeasurableSet (B n)
have simp : MeasurableSet (if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ)
Tactic: simp only [dite_eq_ite, B]
-- 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)ᶜ
n : ℕ
⊢ MeasurableSet (if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ)
have pos : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) → MeasurableSet (A n)
Tactic: split_ifs
-- 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)ᶜ
n : ℕ
pos : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) → MeasurableSet (A n)
⊢ MeasurableSet (if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ)
have neg : ¬Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) → MeasurableSet (A n)ᶜ
Tactic: split_ifs
-- 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)ᶜ
⊢ ∃ (x₀ : α), μ = Measure.dirac x₀
have mBn : MeasurableSet.{u_1} (α := α) (⋂ (n : ℕ), B n)
Tactic: have mBn : MeasurableSet (⋂ n, B n) := by
    refine MeasurableSet.iInter fun n ↦ ?_
    simp only [dite_eq_ite, B]
    split_ifs
    · exact hAm n
    · exact (hAm n).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)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n) : ENNReal) (1 : ENNReal)
have refine : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n)ᶜ : ENNReal) (0 : ENNReal)
Tactic: refine (prob_compl_eq_zero_iff mBn).mp ?_
-- 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)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (⋂ (n : ℕ), B n)ᶜ : ENNReal) (0 : ENNReal)
have simp : ∀ (i : ℕ),
  Eq (α := ENNReal)
    ((μ : (a : Set α) → ENNReal)
        (if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A i) : ENNReal) (1 : ENNReal) then A i else (A i)ᶜ)ᶜ :
      ENNReal)
    (0 : ENNReal)
Tactic: simp only [dite_eq_ite, compl_iInter, measure_iUnion_null_iff, B]
-- 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 : ℕ
⊢ Eq (α := ENNReal)
    ((μ : (a : Set α) → ENNReal)
        (if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (A n)ᶜ)ᶜ :
      ENNReal)
    (0 : ENNReal)
have pos : ∀ (h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal)),
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n)ᶜ : ENNReal) (0 : ENNReal)
Tactic: split_ifs with 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 : ℕ
pos :
  ∀ (h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal)),
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n)ᶜ : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal)
    ((μ : (a : Set α) → ENNReal)
        (if Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (A n) : ENNReal) (1 : ENNReal) then A n else (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: split_ifs with h