awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
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)
⊢ Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (⊤ : ENNReal)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
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)
⊢ Ne (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (⊤ : ENNReal)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
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)
rw : HAdd.hAdd (α := ENNReal) 0 0 ≤ 0
⊢ HAdd.hAdd (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) sᶜ : ENNReal)
      ((μ : (a : Set α) → ENNReal) tᶜ : ENNReal) ≤
    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]

Premises used: MeasureTheory.measure_compl, MeasureTheory.IsZeroOneMeasure.measure_univ, tsub_self
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
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) 0 0 ≤ 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
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)
_₁ :
  HAdd.hAdd (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) sᶜ : ENNReal)
      ((μ : (a : Set α) → ENNReal) tᶜ : ENNReal) ≤
    0
⊢ LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t)ᶜ : ENNReal) (0 : 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

Premises used: Compl.compl, Union.union, DFunLike.coe, MeasureTheory.measure_union_le
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
⊢ LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)

Tactic:
have : μ (s ∩ t) ≤ μ s := measure_mono inter_subset_left
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
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)
⊢ LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)

Tactic:
have : μ (s ∩ t) ≤ μ t := measure_mono inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
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)
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)
⊢ (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)

Tactic:
cases μ.zero_one s

Premises used: MeasureTheory.Measure.zero_one
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
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)
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)
⊢ (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)

Tactic:
cases μ.zero_one t

Premises used: MeasureTheory.Measure.zero_one
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
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)
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)
⊢ (μ : (a : Set α) → ENNReal) (s ∩ t) =
    HMul.hMul (α := ENNReal) (β := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
      ((μ : (a : Set α) → ENNReal) t : ENNReal)

Tactic:
cases μ.zero_one t

Premises used: MeasureTheory.Measure.zero_one
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
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)
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)
⊢ (μ : (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)

Premises used: Inter.inter, MeasureTheory.Measure.zero_one
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
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)
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)
⊢ (μ : (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)

Premises used: Inter.inter, MeasureTheory.Measure.zero_one
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
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)
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)
⊢ (μ : (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)

Premises used: Inter.inter, MeasureTheory.Measure.zero_one
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
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)
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)
⊢ (μ : (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)

Premises used: Inter.inter, MeasureTheory.Measure.zero_one
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
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)
h_2 : 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:
simp_all [measure_inter_eq_one]

Premises used: MeasureTheory.IsZeroOneMeasure.measure_inter_eq_one
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
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)
h_2 : 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:
try simp_all [measure_inter_eq_one]

Premises used: MeasureTheory.IsZeroOneMeasure.measure_inter_eq_one
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
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)
h_2 : 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:
simp_all [measure_inter_eq_one]

Premises used: MeasureTheory.IsZeroOneMeasure.measure_inter_eq_one
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
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)
h_2 : 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:
try simp_all [measure_inter_eq_one]

Premises used: MeasureTheory.IsZeroOneMeasure.measure_inter_eq_one
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
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)
h_2 : 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:
simp_all [measure_inter_eq_one]

Premises used: MeasureTheory.IsZeroOneMeasure.measure_inter_eq_one
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
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)
h_2 : 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:
try simp_all [measure_inter_eq_one]

Premises used: MeasureTheory.IsZeroOneMeasure.measure_inter_eq_one
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
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)
h_2 : 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:
simp_all [measure_inter_eq_one]

Premises used: MeasureTheory.IsZeroOneMeasure.measure_inter_eq_one
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
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)
h_2 : 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:
try simp_all [measure_inter_eq_one]

Premises used: MeasureTheory.IsZeroOneMeasure.measure_inter_eq_one
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
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)
h_2 : 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:
simp_all [measure_inter_eq_one]

Premises used: MeasureTheory.IsZeroOneMeasure.measure_inter_eq_one
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
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)
h_2 : 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:
try simp_all [measure_inter_eq_one]

Premises used: MeasureTheory.IsZeroOneMeasure.measure_inter_eq_one
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
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)
h_2 : 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:
simp_all [measure_inter_eq_one]

Premises used: MeasureTheory.IsZeroOneMeasure.measure_inter_eq_one