awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSingletonClass α
inst_3 : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
pos :
  ∀ (hs : s.Finite),
    Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
      (((count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
neg :
  ∀ (hs : ¬s.Finite),
    Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
      (((count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
by_cases hs : s.Finite

Premises used: Set.Finite
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSingletonClass α
inst_3 : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
hs : s.Finite
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
count_injective_image' hf hs.measurableSet (Finite.image f hs).measurableSet

Premises used: MeasureTheory.Measure.count_injective_image', Set.Finite.image, Set.Finite.measurableSet
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSingletonClass α
inst_3 : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
hs : s.Finite
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact count_injective_image' hf hs.measurableSet (Finite.image f hs).measurableSet

Premises used: MeasureTheory.Measure.count_injective_image', Set.Finite.image, Set.Finite.measurableSet
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSingletonClass α
inst_3 : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
hs : ¬s.Finite
neg : Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [count_apply_infinite hs]

Premises used: MeasureTheory.Measure.count_apply_infinite
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSingletonClass α
inst_3 : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
hs : ¬s.Finite
⊢ ¬(f '' s).Finite

Tactic:
rw [← finite_image_iff hf.injOn] at hs

Premises used: Function.Injective.injOn, Set.finite_image_iff
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSingletonClass α
inst_3 : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
hs : ¬(f '' s).Finite
neg neg₁ : Eq (α := ℝ≥0∞) ∞ ∞
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [count_apply_infinite hs]

Premises used: MeasureTheory.Measure.count_apply_infinite
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
s : Set α
inst_2 : MeasurableSingletonClass α
inst_3 : Countable α
⊢ SigmaFinite.{u_1} (α := α) (m0 := inst) count

Tactic:
simp [sigmaFinite_iff_measure_singleton_lt_top]

Premises used: MeasureTheory.Measure.sigmaFinite_iff_measure_singleton_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
s : Set α
inst_2 : Finite α
⊢ LT.lt (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [Measure.count_apply]

Premises used: MeasureTheory.Measure.count_apply
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
⊢ ((count : Measure α) : (a : Set α) → ℝ≥0∞) univ = (↑(ENat.card α) : ℝ≥0∞)

Tactic:
simp [count_apply .univ, encard_univ]

Premises used: MeasureTheory.Measure.count_apply, Set.encard_univ, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Subsingleton α
i : α
⊢ Eq.{u_1 + 1} (α := Measure α) count (restrict count univ)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Subsingleton α
i : α
e_s : Eq (α := Set α) univ {i}
⊢ Eq (α := Measure α) (restrict count univ) (restrict count {i})

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Subsingleton α
i : α
e_s : ∀ (j : α), Membership.mem (γ := Set α) univ j ↔ Membership.mem (γ := Set α) {i} j
⊢ Eq (α := Set α) univ {i}

Tactic:
ext j
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Subsingleton α
i j : α
⊢ Membership.mem (γ := Set α) univ j ↔ Membership.mem (γ := Set α) {i} j

Tactic:
simp [Subsingleton.elim j i]

Premises used: Subsingleton.elim
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Subsingleton α
i : α
⊢ Eq (α := Measure α) (restrict count {i}) (dirac i)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Subsingleton α
i : α
calc : Eq.{u_1 + 1} (α := Measure α) count (restrict count univ)
calc₁ : Eq (α := Measure α) (restrict count univ) (restrict count {i})
calc₂ : Eq (α := Measure α) (restrict count {i}) (dirac i)
⊢ Eq (α := Measure α) count (dirac i)

Tactic:
calc count
      = count.restrict univ := by simp
    _ = count.restrict {i} := by congr; ext j; simp [Subsingleton.elim j i]
    _ = dirac i := by simp

Premises used: Set.univ, MeasureTheory.Measure.restrict, MeasureTheory.Measure.dirac, MeasureTheory.Measure.count, Singleton.singleton
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Unique α
⊢ Eq.{u_1 + 1} (α := Measure α) count (dirac default)

Tactic:
Subsingleton.count_eq_dirac _

Premises used: Subsingleton.count_eq_dirac
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
hf : Function.Injective f
h2f : Measurable f
⊢ LE.le (α := Measure β) (map f count) count

Tactic:
le_intro fun s hs _ ↦ ?_

Premises used: MeasureTheory.Measure.le_intro
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
hf : Function.Injective f
h2f : Measurable f
refine :
  ∀ (s : Set β) (hs : MeasurableSet s),
    s.Nonempty →
      LE.le (α := ℝ≥0∞) (((map f count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
        (((count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le (α := Measure β) (map f count) count

Tactic:
refine le_intro fun s hs _ ↦ ?_

Premises used: MeasureTheory.Measure.le_intro
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
hf : Function.Injective f
h2f : Measurable f
s : Set β
hs : MeasurableSet s
h : s.Nonempty
rw : (↑(f '' f ⁻¹' s).encard : ℝ≥0∞) ≤ (↑s.encard : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (((map f count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [map_apply h2f hs, count_apply (hs.preimage h2f), count_apply hs, ← hf.encard_image]

Premises used: MeasurableSet.preimage, MeasureTheory.Measure.count_apply, MeasureTheory.Measure.map_apply, Function.Injective.encard_image
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
hf : Function.Injective f
h2f : Measurable f
s : Set β
hs : MeasurableSet s
h : s.Nonempty
⊢ f '' f ⁻¹' s ⊆ s

Tactic:
have := image_preimage_subset f s
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
hf : Function.Injective f
h2f : Measurable f
s : Set β
hs : MeasurableSet s
h : s.Nonempty
this : f '' f ⁻¹' s ⊆ s
⊢ (↑(f '' f ⁻¹' s).encard : ℝ≥0∞) ≤ (↑s.encard : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
pos :
  ∀
    (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∞)),
    MeasurableSet
      (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∞)))
neg :
  ∀
    (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∞)),
    MeasurableSet.{u_1} (α := α) ∅
⊢ MeasurableSet.{u_1} (α := α)
    (if 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∞) then
      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∞))
    else ∅)

Tactic:
split_ifs with h
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
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∞)
⊢ MeasurableSet
    (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∞)))

Tactic:
h.choose_spec.1

Premises used: Exists.choose_spec, And.left
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
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∞)
⊢ MeasurableSet
    (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∞)))

Tactic:
exact h.choose_spec.1

Premises used: Exists.choose_spec, And.left
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
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∞)
⊢ MeasurableSet.{u_1} (α := α) ∅

Tactic:
MeasurableSet.empty

Premises used: MeasurableSet.empty
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
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∞)
⊢ MeasurableSet.{u_1} (α := α) ∅

Tactic:
exact MeasurableSet.empty

Premises used: MeasurableSet.empty
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s t : Set α
pos :
  ∀
    (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∞)),
    SigmaFinite
      (μ.restrict
        (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∞))))
neg :
  ∀
    (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∞)),
    SigmaFinite (μ.restrict ∅)
⊢ SigmaFinite
    (μ.restrict
      (if 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∞) then
        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∞))
      else ∅))

Tactic:
split_ifs with h
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s t : Set α
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∞)
⊢ SigmaFinite
    (μ.restrict
      (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∞))))

Tactic:
h.choose_spec.2.1

Premises used: Exists.choose_spec, And.right, And.left
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s t : Set α
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∞)
⊢ SigmaFinite
    (μ.restrict
      (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∞))))

Tactic:
exact h.choose_spec.2.1

Premises used: Exists.choose_spec, And.right, And.left
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s t : Set α
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∞)
neg : SigmaFinite.{u_1} (α := α) (m0 := mα) 0
⊢ SigmaFinite (μ.restrict ∅)

Tactic:
rw [Measure.restrict_empty]

Premises used: MeasureTheory.Measure.restrict_empty
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s t : Set α
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∞)
⊢ SigmaFinite.{u_1} (α := α) (m0 := mα) 0

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
pos :
  ∀
    (hC_lt :
      HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
        ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s),
    ∃ (t : Set α),
      MeasurableSet t ∧
        SigmaFinite (μ.restrict t) ∧
          (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
              HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) ≤
            (ν : (a : Set α) → ℝ≥0∞) t
neg :
  ∀
    (hC_lt :
      ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s ≤
        HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)),
    ∃ (t : Set α),
      MeasurableSet t ∧
        SigmaFinite (μ.restrict t) ∧
          (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
              HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) ≤
            (ν : (a : Set α) → ℝ≥0∞) t
⊢ ∃ (t : Set α),
    MeasurableSet t ∧
      SigmaFinite (μ.restrict t) ∧
        (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
            HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) ≤
          (ν : (a : Set α) → ℝ≥0∞) t

Tactic:
by_cases! hC_lt : 1 / n < ⨆ (s) (_ : MeasurableSet s) (_ : SigmaFinite (μ.restrict s)), ν s
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
hC_lt :
  HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
    ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s
⊢ LT.lt (α := ℝ≥0∞)
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) ∞

Tactic:
(?_ : ⨆ (s) (_ : MeasurableSet s)
        (_ : SigmaFinite (μ.restrict s)), ν s ≤ ν Set.univ).trans_lt (measure_lt_top _ _)

Premises used: MeasureTheory.measure_lt_top, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
hC_lt :
  HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
    ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s
refine :
  LE.le (α := ℝ≥0∞)
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞)
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) ∞

Tactic:
refine (?_ : ⨆ (s) (_ : MeasurableSet s)
        (_ : SigmaFinite (μ.restrict s)), ν s ≤ ν Set.univ).trans_lt (measure_lt_top _ _)

Premises used: MeasureTheory.measure_lt_top, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
hC_lt :
  HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
    ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
iSup_le (fun s ↦ ?_)

Premises used: iSup_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
hC_lt :
  HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
    ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s
refine :
  ∀ (s : Set α),
    LE.le (α := ℝ≥0∞) (⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
refine iSup_le (fun s ↦ ?_)

Premises used: iSup_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
hC_lt :
  HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
    ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s
s : Set α
⊢ LE.le (α := ℝ≥0∞) (⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
iSup_le (fun _ ↦ iSup_le (fun _ ↦ measure_mono (Set.subset_univ s)))

Premises used: Set.subset_univ, MeasureTheory.measure_mono, iSup_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
hC_lt :
  HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
    ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s
s : Set α
⊢ LE.le (α := ℝ≥0∞) (⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
exact iSup_le (fun _ ↦ iSup_le (fun _ ↦ measure_mono (Set.subset_univ s)))

Premises used: Set.subset_univ, MeasureTheory.measure_mono, iSup_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
hC_lt :
  HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
    ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s
⊢ LT.lt (α := ℝ≥0∞)
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) ∞

Tactic:
have h_lt_top : ⨆ (s) (_ : MeasurableSet s) (_ : SigmaFinite (μ.restrict s)), ν s < ∞ := by
      refine (?_ : ⨆ (s) (_ : MeasurableSet s)
        (_ : SigmaFinite (μ.restrict s)), ν s ≤ ν Set.univ).trans_lt (measure_lt_top _ _)
      refine iSup_le (fun s ↦ ?_)
      exact iSup_le (fun _ ↦ iSup_le (fun _ ↦ measure_mono (Set.subset_univ s)))
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
hC_lt :
  HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
    ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s
h_lt_top :
  LT.lt (α := ℝ≥0∞)
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) ∞
⊢ HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) ≠ 0

Tactic:
simp