awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
ht_subset : t ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hst : s ⊆ t
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
measure_eq_top_of_subset_compl_sigmaFiniteSetWRT'_of_measurableSet ht ht_subset ?_

Premises used: MeasureTheory.measure_eq_top_of_subset_compl_sigmaFiniteSetWRT'_of_measurableSet
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
ht_subset : t ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hst : s ⊆ t
ht : MeasurableSet t
refine : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
refine measure_eq_top_of_subset_compl_sigmaFiniteSetWRT'_of_measurableSet ht ht_subset ?_

Premises used: MeasureTheory.measure_eq_top_of_subset_compl_sigmaFiniteSetWRT'_of_measurableSet
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
ht_subset : t ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hst : s ⊆ t
ht : MeasurableSet t
⊢ Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
fun hνt ↦ hνs (measure_mono_null hst hνt)

Premises used: MeasureTheory.measure_mono_null, Not
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
ht_subset : t ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hst : s ⊆ t
ht : MeasurableSet t
⊢ Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact fun hνt ↦ hνs (measure_mono_null hst hνt)

Premises used: MeasureTheory.measure_mono_null
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : SFinite ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have :
  ∀ (ν' : Measure α) (hν' : IsFiniteMeasure ν') (hνν' : ν ≪ ν'),
    ν' ≪ ν → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have ⟨ν', hν', hνν', _⟩ := exists_isFiniteMeasure_absolutelyContinuous ν
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : SFinite ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ν' : Measure α
hν' : IsFiniteMeasure ν'
hνν' : ν ≪ ν'
right : ν' ≪ ν
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      SigmaFinite (μ.restrict s) ∧
        ∀ t ⊆ sᶜ,
          Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
            Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
⟨μ.sigmaFiniteSetWRT' ν', measurableSet_sigmaFiniteSetWRT',
      sigmaFinite_restrict_sigmaFiniteSetWRT' _ _,
      fun t ht_subset hνt ↦ measure_eq_top_of_subset_compl_sigmaFiniteSetWRT' ht_subset ?_⟩

Premises used: MeasureTheory.measure_eq_top_of_subset_compl_sigmaFiniteSetWRT', MeasureTheory.measurableSet_sigmaFiniteSetWRT', MeasureTheory.Measure.sigmaFiniteSetWRT', And.intro, Exists.intro, MeasureTheory.sigmaFinite_restrict_sigmaFiniteSetWRT'
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : SFinite ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ν' : Measure α
hν' : IsFiniteMeasure ν'
hνν' : ν ≪ ν'
right : ν' ≪ ν
refine :
  ∀ (t : Set α) (ht_subset : t ⊆ (μ.sigmaFiniteSetWRT' ν')ᶜ)
    (hνt : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)),
    Ne (α := ℝ≥0∞) ((ν' : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      SigmaFinite (μ.restrict s) ∧
        ∀ t ⊆ sᶜ,
          Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
            Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
refine ⟨μ.sigmaFiniteSetWRT' ν', measurableSet_sigmaFiniteSetWRT',
      sigmaFinite_restrict_sigmaFiniteSetWRT' _ _,
      fun t ht_subset hνt ↦ measure_eq_top_of_subset_compl_sigmaFiniteSetWRT' ht_subset ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : SFinite ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ν' : Measure α
hν' : IsFiniteMeasure ν'
hνν' : ν ≪ ν'
right : ν' ≪ ν
t : Set α
ht_subset : t ⊆ (μ.sigmaFiniteSetWRT' ν')ᶜ
hνt : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((ν' : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
fun hν't ↦ hνt (hνν' hν't)

Premises used: Not
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : SFinite ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ν' : Measure α
hν' : IsFiniteMeasure ν'
hνν' : ν ≪ ν'
right : ν' ≪ ν
t : Set α
ht_subset : t ⊆ (μ.sigmaFiniteSetWRT' ν')ᶜ
hνt : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((ν' : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact fun hν't ↦ hνt (hνν' hν't)
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : SFinite ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ν' : Measure α
hν' : IsFiniteMeasure ν'
hνν' : ν ≪ ν'
right : ν' ≪ ν
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      SigmaFinite (μ.restrict s) ∧
        ∀ t ⊆ sᶜ,
          Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
            Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have h : ∃ s : Set α, MeasurableSet s ∧ SigmaFinite (μ.restrict s)
      ∧ (∀ t ⊆ sᶜ, ν t ≠ 0 → μ t = ∞) := by
    refine ⟨μ.sigmaFiniteSetWRT' ν', measurableSet_sigmaFiniteSetWRT',
      sigmaFinite_restrict_sigmaFiniteSetWRT' _ _,
      fun t ht_subset hνt ↦ measure_eq_top_of_subset_compl_sigmaFiniteSetWRT' ht_subset ?_⟩
    exact fun hν't ↦ hνt (hνν' hν't)
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : SFinite ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ν' : Measure α
hν' : IsFiniteMeasure ν'
hνν' : ν ≪ ν'
right : ν' ≪ ν
h :
  ∃ (s : Set α),
    MeasurableSet s ∧
      SigmaFinite (μ.restrict s) ∧
        ∀ t ⊆ sᶜ,
          Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
            Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  ∀ (hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)) (ν' : Measure α) (hν' : IsFiniteMeasure ν')
    (hνν' : ν ≪ ν'),
    ν' ≪ ν →
      ∀
        (h :
          ∃ (s : Set α),
            MeasurableSet s ∧
              SigmaFinite (μ.restrict s) ∧
                ∀ t ⊆ sᶜ,
                  Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
                    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞))
        (hs_subset :
          s ⊆
            (h.choose (p := fun (s : Set α) ↦
                MeasurableSet s ∧
                  SigmaFinite (μ.restrict s) ∧
                    ∀ t ⊆ sᶜ,
                      Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
                        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)))ᶜ),
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [Measure.sigmaFiniteSetWRT, dif_pos h] at hs_subset

Premises used: MeasureTheory.Measure.sigmaFiniteSetWRT, dif_pos
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : SFinite ν
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ν' : Measure α
hν' : IsFiniteMeasure ν'
hνν' : ν ≪ ν'
right : ν' ≪ ν
h :
  ∃ (s : Set α),
    MeasurableSet s ∧
      SigmaFinite (μ.restrict s) ∧
        ∀ t ⊆ sᶜ,
          Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
            Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hs_subset :
  s ⊆
    (h.choose (p := fun (s : Set α) ↦
        MeasurableSet s ∧
          SigmaFinite (μ.restrict s) ∧
            ∀ t ⊆ sᶜ,
              Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
                Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)))ᶜ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
h.choose_spec.2.2 s hs_subset hνs

Premises used: Exists.choose_spec, And.right
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : SFinite ν
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ν' : Measure α
hν' : IsFiniteMeasure ν'
hνν' : ν ≪ ν'
right : ν' ≪ ν
h :
  ∃ (s : Set α),
    MeasurableSet s ∧
      SigmaFinite (μ.restrict s) ∧
        ∀ t ⊆ sᶜ,
          Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
            Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hs_subset :
  s ⊆
    (h.choose (p := fun (s : Set α) ↦
        MeasurableSet s ∧
          SigmaFinite (μ.restrict s) ∧
            ∀ t ⊆ sᶜ,
              Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
                Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)))ᶜ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact h.choose_spec.2.2 s hs_subset hνs

Premises used: Exists.choose_spec, And.right
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SFinite ν
hμν : μ ≪ ν
h :
  ∀ (s : Set α),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((μ.restrict (μ.sigmaFiniteSetWRT ν)ᶜ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
        ((HSMul.hSMul (α := ℝ≥0∞) ∞ (ν.restrict (μ.sigmaFiniteSetWRT ν)ᶜ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ.restrict (μ.sigmaFiniteSetWRT ν)ᶜ = HSMul.hSMul (α := ℝ≥0∞) ∞ (ν.restrict (μ.sigmaFiniteSetWRT ν)ᶜ)

Tactic:
ext s
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SFinite ν
hμν : μ ≪ ν
s : Set α
h_1 : MeasurableSet s
h :
  (μ : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (μ.sigmaFiniteSetWRT ν)ᶜ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) ∞ (ν.restrict (μ.sigmaFiniteSetWRT ν)ᶜ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [Measure.restrict_apply' measurableSet_sigmaFiniteSetWRT.compl,
    Measure.smul_apply, smul_eq_mul,
    Measure.restrict_apply' measurableSet_sigmaFiniteSetWRT.compl]

Premises used: MeasurableSet.compl, MeasureTheory.Measure.smul_apply, MeasureTheory.measurableSet_sigmaFiniteSetWRT, smul_eq_mul, MeasureTheory.Measure.restrict_apply'
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SFinite ν
hμν : μ ≪ ν
s : Set α
h : MeasurableSet s
pos :
  ∀ (hνs : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)),
    (μ : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞)
neg :
  ∀ (hνs : ¬Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)),
    (μ : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞)

Tactic:
by_cases hνs : ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = 0

Premises used: MeasureTheory.Measure.sigmaFiniteSetWRT, Compl.compl, Inter.inter, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SFinite ν
hμν : μ ≪ ν
s : Set α
h : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
pos : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞)

Tactic:
rw [hνs, mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SFinite ν
hμν : μ ≪ ν
s : Set α
h : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
hμν hνs
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SFinite ν
hμν : μ ≪ ν
s : Set α
h : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact hμν hνs
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SFinite ν
hμν : μ ≪ ν
s : Set α
h : MeasurableSet s
hνs : ¬Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
neg : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞) (∞ : ℝ≥0∞)
neg₁ neg₂ : Eq (α := ℝ≥0∞) ∞ ∞
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞)

Tactic:
rw [ENNReal.top_mul hνs, measure_eq_top_of_subset_compl_sigmaFiniteSetWRT
      Set.inter_subset_right hνs]

Premises used: MeasureTheory.measure_eq_top_of_subset_compl_sigmaFiniteSetWRT, ENNReal.top_mul, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SFinite ν
⊢ Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ∞ :=
    measure_eq_top_of_subset_compl_sigmaFiniteSetWRT subset_rfl
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SFinite ν
h :
  Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (∞ : ℝ≥0∞)
by_contra : ∀ (h0 : ¬Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)), False
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
by_contra h0
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SFinite ν
h :
  Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (∞ : ℝ≥0∞)
h0 : ¬Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ False

Tactic:
ENNReal.top_ne_zero ?_

Premises used: ENNReal.top_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SFinite ν
h :
  Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (∞ : ℝ≥0∞)
h0 : ¬Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
refine : Eq (α := ℝ≥0∞) ∞ 0
⊢ False

Tactic:
refine ENNReal.top_ne_zero ?_

Premises used: ENNReal.top_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SFinite ν
h :
  Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (∞ : ℝ≥0∞)
h0 : ¬Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
rw : Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ) 0
⊢ Eq (α := ℝ≥0∞) ∞ 0

Tactic:
rw [← h h0, ← Measure.iSup_restrict_spanningSets]

Premises used: MeasureTheory.Measure.iSup_restrict_spanningSets
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SFinite ν
h :
  Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (∞ : ℝ≥0∞)
h0 : ¬Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw :
  ∀ (i : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ) 0

Tactic:
simp_rw [Measure.restrict_apply' (measurableSet_spanningSets μ _), ENNReal.iSup_eq_zero]

Premises used: MeasureTheory.measurableSet_spanningSets, ENNReal.iSup_eq_zero, MeasureTheory.Measure.restrict_apply'
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SFinite ν
h :
  Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (∞ : ℝ≥0∞)
h0 : ¬Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
i : ℕ
by_contra :
  ∀
    (h_ne_zero :
      ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) : ℝ≥0∞) (0 : ℝ≥0∞)),
    False
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
by_contra h_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SFinite ν
h :
  Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (∞ : ℝ≥0∞)
h0 : ¬Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
i : ℕ
h_ne_zero : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) : ℝ≥0∞) (0 : ℝ≥0∞)
refine_2 :
  ∀
    (h_zero_top :
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) : ℝ≥0∞) (∞ : ℝ≥0∞)),
    False
refine_1 : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ False

Tactic:
have h_zero_top := measure_eq_top_of_subset_compl_sigmaFiniteSetWRT
    (Set.inter_subset_left : (μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i ⊆ _) ?_
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SFinite ν
h :
  Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (∞ : ℝ≥0∞)
h0 : ¬Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
i : ℕ
h_ne_zero : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
fun h ↦ h_ne_zero (hμν h)

Premises used: Not
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SFinite ν
h :
  Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (∞ : ℝ≥0∞)
h0 : ¬Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
i : ℕ
h_ne_zero : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact fun h ↦ h_ne_zero (hμν h)
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SFinite ν
h :
  Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (∞ : ℝ≥0∞)
h0 : ¬Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
i : ℕ
h_ne_zero : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) : ℝ≥0∞) (0 : ℝ≥0∞)
h_zero_top : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ False

Tactic:
absurd h_zero_top (ne_of_lt ?_)

Premises used: absurd, ne_of_lt
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SFinite ν
h :
  Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (∞ : ℝ≥0∞)
h0 : ¬Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
i : ℕ
h_ne_zero : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) : ℝ≥0∞) (0 : ℝ≥0∞)
h_zero_top : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_2 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ False

Tactic:
refine absurd h_zero_top (ne_of_lt ?_)

Premises used: absurd, ne_of_lt