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
hμs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
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)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
have inl : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal) →
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
Tactic: rcases μ.zero_one t with (_ | hμ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
hμs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
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) →
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
have inl₁ : ∀ (hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)),
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
Tactic: rcases μ.zero_one t with (_ | hμ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
hμs_1 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
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μs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
have inr : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal) →
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
Tactic: rcases μ.zero_one t with (_ | hμ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
hμs_1 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
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μs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
inr :
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal) →
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
have inr₁ : ∀ (hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)),
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
Tactic: rcases μ.zero_one t with (_ | hμ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
hμs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
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)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
have inl : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal) →
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
Tactic: rcases μ.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
hμs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
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) →
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
have inl₁ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal) →
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
Tactic: rcases μ.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
hμs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt_1 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
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μt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
have inl : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal) →
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
Tactic: rcases μ.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
hμs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt_1 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
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μt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
inl :
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal) →
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
have inl₁ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal) →
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
Tactic: rcases μ.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
hμs_1 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
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μs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
have inr : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal) →
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
Tactic: rcases μ.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
hμs_1 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
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μs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal)
inr :
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal) →
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
have inr₁ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal) →
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
Tactic: rcases μ.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
hμs_1 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt_1 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
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μs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
have inr : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal) →
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
Tactic: rcases μ.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
hμs_1 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt_1 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
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μs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
inr :
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal) →
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
have inr₁ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal) →
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
Tactic: rcases μ.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
hμs_1 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt_1 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
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μs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
have inr : False
Tactic: simp_all only [zero_le, zero_ne_one]
Cleared hypotheses: hμs_1, hμt_1, this_1, this
-- 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
hμs_1 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt_1 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
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μs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
have inr : False
Tactic: try simp_all only [zero_le, zero_ne_one]
Cleared hypotheses: hμs_1, hμt_1, this_1, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal)
this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t)ᶜ : ENNReal) (0 : ENNReal)
⊢ False
have this₁ : HSub.hSub (α := ENNReal) (β := ENNReal) (1 : ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ≤ 0
Tactic: rw [measure_compl (hs.inter ht) (by simp), measure_univ ‹_›] at this
Cleared hypotheses: this
-- 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
hμs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal)
⊢ False
have inr : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t)ᶜ : ENNReal) (0 : ENNReal)
Tactic: suffices μ (s ∩ t)ᶜ ≤ 0 by
    rw [measure_compl (hs.inter ht) (by simp), measure_univ ‹_›] at this
    simp_all
-- 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
hμs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal)
⊢ HAdd.hAdd (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) sᶜ : ENNReal)
      ((μ : (a : Set α) → ENNReal) tᶜ : ENNReal) ≤
    0
have rw : HAdd.hAdd (α := ENNReal) 0 0 ≤ 0
Tactic: rw [measure_compl hs (by simp), measure_univ hμs, hμs, tsub_self,
      measure_compl ht (by simp), measure_univ hμt, hμt, tsub_self]
-- 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
hμs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal)
⊢ LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t)ᶜ : ENNReal) (0 : ENNReal)
have _ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t)ᶜ : ENNReal) ((μ : (a : Set α) → ENNReal) (sᶜ ∪ tᶜ) : ENNReal)
Tactic: calc
  _ = μ (sᶜ ∪ tᶜ) := by simp [compl_inter]
  _ ≤ μ sᶜ + μ tᶜ := measure_union_le _ _
  _ ≤ 0 := by
    rw [measure_compl hs (by simp), measure_univ hμs, hμs, tsub_self,
      measure_compl ht (by simp), measure_univ hμt, hμt, tsub_self]
    simp
-- 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
hμs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal)
_ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t)ᶜ : ENNReal) ((μ : (a : Set α) → ENNReal) (sᶜ ∪ tᶜ) : ENNReal)
⊢ LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t)ᶜ : ENNReal) (0 : ENNReal)
have _₁ : HAdd.hAdd (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) sᶜ : ENNReal)
    ((μ : (a : Set α) → ENNReal) tᶜ : ENNReal) ≤
  0
Tactic: calc
  _ = μ (sᶜ ∪ tᶜ) := by simp [compl_inter]
  _ ≤ μ sᶜ + μ tᶜ := measure_union_le _ _
  _ ≤ 0 := by
    rw [measure_compl hs (by simp), measure_univ hμs, hμs, tsub_self,
      measure_compl ht (by simp), measure_univ hμt, hμt, tsub_self]
    simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)
have this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
Tactic: have : μ (s ∩ t) ≤ μ s := measure_mono inter_subset_left
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
⊢ (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)
have this₁ : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
Tactic: have : μ (s ∩ t) ≤ μ t := measure_mono inter_subset_right
-- 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)
⊢ (μ : (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 : 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
-- 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)
inl :
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : 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 : 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
-- 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)
⊢ (μ : (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) (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