awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
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∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞)
have neg₁ : Eq (α := ℝ≥0∞) ∞ ∞
Tactic: rw [ENNReal.top_mul hνs, measure_eq_top_of_subset_compl_sigmaFiniteSetWRT
      Set.inter_subset_right hνs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst : SigmaFinite μ
inst_1 : SFinite ν
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have h : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have by_contra : ∀ (h0 : ¬Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)), False
Tactic: by_contra h0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
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
have refine : Eq (α := ℝ≥0∞) ∞ 0
Tactic: refine ENNReal.top_ne_zero ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ∞ 0
have rw : Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ) 0
Tactic: rw [← h h0, ← Measure.iSup_restrict_spanningSets]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT ν)ᶜ) 0
have simp_rw : ∀ (i : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [Measure.restrict_apply' (measurableSet_spanningSets μ _), ENNReal.iSup_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
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 : ℕ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) : ℝ≥0∞) (0 : ℝ≥0∞)
have by_contra : ∀
  (h_ne_zero :
    ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) : ℝ≥0∞) (0 : ℝ≥0∞)),
  False
Tactic: by_contra h_ne_zero
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
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∞)
⊢ False
have refine_2 : ∀
  (h_zero_top :
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) : ℝ≥0∞) (∞ : ℝ≥0∞)),
  False
Tactic: have h_zero_top := measure_eq_top_of_subset_compl_sigmaFiniteSetWRT
    (Set.inter_subset_left : (μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i ⊆ _) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
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
⊢ False
have refine_1 : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have h_zero_top := measure_eq_top_of_subset_compl_sigmaFiniteSetWRT
    (Set.inter_subset_left : (μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i ⊆ _) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
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
have refine_2 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine absurd h_zero_top (ne_of_lt ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
t : Set α
inst : SFinite μ
ht_subset : t ⊆ μ.sigmaFiniteSetᶜ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [or_iff_not_imp_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
s : Set α
⊢ Eq (α := ℝ≥0∞) ((μ.restrict μ.sigmaFiniteSetᶜ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((μ.restrict μ.sigmaFiniteSetᶜ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ μ.sigmaFiniteSetᶜ) : ℝ≥0∞) (0 : ℝ≥0∞) ∨
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ μ.sigmaFiniteSetᶜ) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [Measure.restrict_apply' measurableSet_sigmaFiniteSet.compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) μ.sigmaFiniteSetᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ SigmaFinite μ
have rw : SigmaFinite (μ.restrict μ.sigmaFiniteSet)
Tactic: rw [← Measure.restrict_add_restrict_compl (μ := μ) (measurableSet_sigmaFiniteSet (μ := μ)),
    Measure.restrict_eq_zero.mpr h, add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Hahn (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
d : Set α → ℝ :=
  fun (s : Set α) ↦
    (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ) - (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ)
c : Set ℝ := d '' {s : Set α | MeasurableSet s}
γ : ℝ := sSup c
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      (∀ (t : Set α),
          MeasurableSet t →
            t ⊆ s → LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) ∧
        ∀ (t : Set α),
          MeasurableSet t →
            t ⊆ sᶜ → LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have hμ : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have hμ : ∀ s, μ s ≠ ∞ := measure_ne_top μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Hahn (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
d : Set α → ℝ :=
  fun (s : Set α) ↦
    (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ) - (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ)
c : Set ℝ := d '' {s : Set α | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      (∀ (t : Set α),
          MeasurableSet t →
            t ⊆ s → LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) ∧
        ∀ (t : Set α),
          MeasurableSet t →
            t ⊆ sᶜ → LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have hν : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have hν : ∀ s, ν s ≠ ∞ := measure_ne_top ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Hahn (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
d : Set α → ℝ :=
  fun (s : Set α) ↦
    (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ) - (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ)
c : Set ℝ := d '' {s : Set α | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hν : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      (∀ (t : Set α),
          MeasurableSet t →
            t ⊆ s → LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) ∧
        ∀ (t : Set α),
          MeasurableSet t →
            t ⊆ sᶜ → LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have to_nnreal_μ : ∀ (s : Set α), (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) s
Tactic: have to_nnreal_μ : ∀ s, ((μ s).toNNReal : ℝ≥0∞) = μ s := fun s => ENNReal.coe_toNNReal <| hμ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Hahn (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
d : Set α → ℝ :=
  fun (s : Set α) ↦
    (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ) - (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ)
c : Set ℝ := d '' {s : Set α | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hν : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
to_nnreal_μ : ∀ (s : Set α), (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) s
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      (∀ (t : Set α),
          MeasurableSet t →
            t ⊆ s → LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) ∧
        ∀ (t : Set α),
          MeasurableSet t →
            t ⊆ sᶜ → LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have to_nnreal_ν : ∀ (s : Set α), (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (ν : (a : Set α) → ℝ≥0∞) s
Tactic: have to_nnreal_ν : ∀ s, ((ν s).toNNReal : ℝ≥0∞) = ν s := fun s => ENNReal.coe_toNNReal <| hν _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
d : Set α → ℝ :=
  fun (s : Set α) ↦
    (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ) - (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ)
c : Set ℝ := d '' {s : Set α | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hν : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
to_nnreal_μ : ∀ (s : Set α), (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) s
to_nnreal_ν : ∀ (s : Set α), (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (ν : (a : Set α) → ℝ≥0∞) s
s t : Set α
ht : MeasurableSet t
⊢ (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ) - (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ) =
    (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t))) : ℝ) -
        (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) (s \ t))) : ℝ) +
      ((↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t))) : ℝ) -
        (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t))) : ℝ))
have rw : (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t))) : ℝ) +
      (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t))) : ℝ) -
    ((↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t))) : ℝ) +
      (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) (s \ t))) : ℝ)) =
  (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t))) : ℝ) -
      (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) (s \ t))) : ℝ) +
    ((↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t))) : ℝ) -
      (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t))) : ℝ))
Tactic: rw [← measure_inter_add_diff s ht, ← measure_inter_add_diff s ht,
      ENNReal.toNNReal_add (hμ _) (hμ _), ENNReal.toNNReal_add (hν _) (hν _), NNReal.coe_add,
      NNReal.coe_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
d : Set α → ℝ :=
  fun (s : Set α) ↦
    (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ) - (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ)
c : Set ℝ := d '' {s : Set α | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hν : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
to_nnreal_μ : ∀ (s : Set α), (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) s
to_nnreal_ν : ∀ (s : Set α), (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (ν : (a : Set α) → ℝ≥0∞) s
s t : Set α
ht : MeasurableSet t
⊢ (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t))) : ℝ) +
        (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t))) : ℝ) -
      ((↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t))) : ℝ) +
        (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) (s \ t))) : ℝ)) =
    (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t))) : ℝ) -
        (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) (s \ t))) : ℝ) +
      ((↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t))) : ℝ) -
        (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t))) : ℝ))
have simp : (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t))) : ℝ) +
      (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t))) : ℝ) +
    (-(↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t))) : ℝ) +
      -(↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) (s \ t))) : ℝ)) =
  (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t))) : ℝ) +
      -(↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) (s \ t))) : ℝ) +
    ((↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t))) : ℝ) +
      -(↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) (s ∩ t))) : ℝ))
Tactic: simp only [sub_eq_add_neg, neg_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Hahn (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
d : Set α → ℝ :=
  fun (s : Set α) ↦
    (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ) - (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ)
c : Set ℝ := d '' {s : Set α | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hν : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
to_nnreal_μ : ∀ (s : Set α), (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) s
to_nnreal_ν : ∀ (s : Set α), (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (ν : (a : Set α) → ℝ≥0∞) s
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      (∀ (t : Set α),
          MeasurableSet t →
            t ⊆ s → LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) ∧
        ∀ (t : Set α),
          MeasurableSet t →
            t ⊆ sᶜ → LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have d_split : ∀ (s t : Set α) (ht : MeasurableSet t), d s = d (s \ t) + d (s ∩ t)
Tactic: have d_split s t (ht : MeasurableSet t) : d s = d (s \ t) + d (s ∩ t) := by
    dsimp only [d]
    rw [← measure_inter_add_diff s ht, ← measure_inter_add_diff s ht,
      ENNReal.toNNReal_add (hμ _) (hμ _), ENNReal.toNNReal_add (hν _) (hν _), NNReal.coe_add,
      NNReal.coe_add]
    simp only [sub_eq_add_neg, neg_add]
    abel
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
d : Set α → ℝ :=
  fun (s : Set α) ↦
    (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ) - (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ)
c : Set ℝ := d '' {s : Set α | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hν : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
to_nnreal_μ : ∀ (s : Set α), (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) s
to_nnreal_ν : ∀ (s : Set α), (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (ν : (a : Set α) → ℝ≥0∞) s
d_split : ∀ (s t : Set α) (ht : MeasurableSet t), d s = d (s \ t) + d (s ∩ t)
s : ℕ → Set α
hm : Monotone s
⊢ Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋃ (n : ℕ), s n)))
have refine_1 : Tendsto (fun (n : ℕ) ↦ (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) (s n))) : ℝ)) atTop
  (𝓝 (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n))) : ℝ))
Tactic: refine Tendsto.sub ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
d : Set α → ℝ :=
  fun (s : Set α) ↦
    (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ) - (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ)
c : Set ℝ := d '' {s : Set α | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hν : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
to_nnreal_μ : ∀ (s : Set α), (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) s
to_nnreal_ν : ∀ (s : Set α), (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (ν : (a : Set α) → ℝ≥0∞) s
d_split : ∀ (s t : Set α) (ht : MeasurableSet t), d s = d (s \ t) + d (s ∩ t)
s : ℕ → Set α
hm : Monotone s
refine_1 :
  Tendsto (fun (n : ℕ) ↦ (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) (s n))) : ℝ)) atTop
    (𝓝 (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n))) : ℝ))
⊢ Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋃ (n : ℕ), s n)))
have refine_2 : Tendsto (fun (n : ℕ) ↦ (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) (s n))) : ℝ)) atTop
  (𝓝 (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n))) : ℝ))
Tactic: refine Tendsto.sub ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
d : Set α → ℝ :=
  fun (s : Set α) ↦
    (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ) - (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ)
c : Set ℝ := d '' {s : Set α | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hν : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
to_nnreal_μ : ∀ (s : Set α), (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) s
to_nnreal_ν : ∀ (s : Set α), (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (ν : (a : Set α) → ℝ≥0∞) s
d_split : ∀ (s t : Set α) (ht : MeasurableSet t), d s = d (s \ t) + d (s ∩ t)
s : ℕ → Set α
hm : Monotone s
⊢ Tendsto (fun (n : ℕ) ↦ (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) (s n))) : ℝ)) atTop
    (𝓝 (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n))) : ℝ))
have refine_1 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine NNReal.tendsto_coe.2 <| (ENNReal.tendsto_toNNReal ?_).comp <|
        tendsto_measure_iUnion_atTop hm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Hahn (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
d : Set α → ℝ :=
  fun (s : Set α) ↦
    (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ) - (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ)
c : Set ℝ := d '' {s : Set α | MeasurableSet s}
γ : ℝ := sSup c
hμ : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hν : ∀ (s : Set α), Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
to_nnreal_μ : ∀ (s : Set α), (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) s
to_nnreal_ν : ∀ (s : Set α), (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) s)) : ℝ≥0∞) = (ν : (a : Set α) → ℝ≥0∞) s
d_split : ∀ (s t : Set α) (ht : MeasurableSet t), d s = d (s \ t) + d (s ∩ t)
s : ℕ → Set α
hm : Monotone s
⊢ Tendsto (fun (n : ℕ) ↦ (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) (s n))) : ℝ)) atTop
    (𝓝 (↑(ENNReal.toNNReal ((ν : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n))) : ℝ))
have refine_2 : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine NNReal.tendsto_coe.2 <| (ENNReal.tendsto_toNNReal ?_).comp <|
        tendsto_measure_iUnion_atTop hm