awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
(measure_mono Set.inter_subset_right).trans_lt (measure_spanningSets_lt_top μ i)

Premises used: MeasureTheory.measure_spanningSets_lt_top, MeasureTheory.measure_mono, LE.le.trans_lt, Set.inter_subset_right
-- 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∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact (measure_mono Set.inter_subset_right).trans_lt (measure_spanningSets_lt_top μ i)

Premises used: MeasureTheory.measure_spanningSets_lt_top, MeasureTheory.measure_mono, LE.le.trans_lt, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
⊢ MeasurableSet μ.sigmaFiniteSet

Tactic:
measurableSet_sigmaFiniteSetWRT

Premises used: MeasureTheory.Measure.sigmaFiniteSet, MeasureTheory.measurableSet_sigmaFiniteSetWRT
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
t : Set α
inst : SFinite μ
ht_subset : t ⊆ μ.sigmaFiniteSetᶜ
rw :
  ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [or_iff_not_imp_left]

Premises used: Classical.or_iff_not_imp_left
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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∞)

Tactic:
measure_eq_top_of_subset_compl_sigmaFiniteSetWRT ht_subset

Premises used: MeasureTheory.measure_eq_top_of_subset_compl_sigmaFiniteSetWRT
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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∞)

Tactic:
exact measure_eq_top_of_subset_compl_sigmaFiniteSetWRT ht_subset

Premises used: MeasureTheory.measure_eq_top_of_subset_compl_sigmaFiniteSetWRT
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
s : Set α
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ μ.sigmaFiniteSetᶜ) : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ μ.sigmaFiniteSetᶜ) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict μ.sigmaFiniteSetᶜ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((μ.restrict μ.sigmaFiniteSetᶜ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [Measure.restrict_apply' measurableSet_sigmaFiniteSet.compl]

Premises used: MeasureTheory.measurableSet_sigmaFiniteSet, MeasurableSet.compl, MeasureTheory.Measure.restrict_apply'
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
s : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ μ.sigmaFiniteSetᶜ) : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ μ.sigmaFiniteSetᶜ) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
measure_eq_zero_or_top_of_subset_compl_sigmaFiniteSet Set.inter_subset_right

Premises used: MeasureTheory.measure_eq_zero_or_top_of_subset_compl_sigmaFiniteSet, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
s : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ μ.sigmaFiniteSetᶜ) : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ μ.sigmaFiniteSetᶜ) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact measure_eq_zero_or_top_of_subset_compl_sigmaFiniteSet Set.inter_subset_right

Premises used: MeasureTheory.measure_eq_zero_or_top_of_subset_compl_sigmaFiniteSet, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s t : Set α
⊢ SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT μ))

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) μ.sigmaFiniteSetᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
rw : SigmaFinite (μ.restrict μ.sigmaFiniteSet)
⊢ SigmaFinite μ

Tactic:
rw [← Measure.restrict_add_restrict_compl (μ := μ) (measurableSet_sigmaFiniteSet (μ := μ)),
    Measure.restrict_eq_zero.mpr h, add_zero]

Premises used: Iff.mpr, MeasureTheory.Measure.restrict_add_restrict_compl, MeasureTheory.Measure.restrict_eq_zero, MeasureTheory.measurableSet_sigmaFiniteSet, add_zero
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) μ.sigmaFiniteSetᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ SigmaFinite (μ.restrict μ.sigmaFiniteSet)

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) μ.sigmaFiniteSetᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_compl_sigmaFiniteSetWRT Measure.AbsolutelyContinuous.rfl

Premises used: MeasureTheory.measure_compl_sigmaFiniteSetWRT, Set.Mem, setOf, MeasureTheory.Measure.sigmaFiniteSet, MeasureTheory.Measure.AbsolutelyContinuous.rfl
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) μ.sigmaFiniteSetᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔ SigmaFinite μ

Tactic:
⟨sigmaFinite_of_measure_compl_sigmaFiniteSet_eq_zero, fun _ ↦ measure_compl_sigmaFiniteSet μ⟩

Premises used: MeasureTheory.measure_compl_sigmaFiniteSet, MeasureTheory.sigmaFinite_of_measure_compl_sigmaFiniteSet_eq_zero, Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn
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 α), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have hμ : ∀ s, μ s ≠ ∞ := measure_ne_top μ
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn
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 α), Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have hν : ∀ s, ν s ≠ ∞ := measure_ne_top ν
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn
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 α), (↑(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μ _
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn
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 α), (↑(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ν _
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn
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
dsimp :
  (↑(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))) : ℝ))
⊢ d s = d (s \ t) + d (s ∩ t)

Tactic:
dsimp only [d]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn
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
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))) : ℝ))
⊢ (↑(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))) : ℝ))

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]

Premises used: NNReal.coe_add, ENNReal.toNNReal_add, MeasureTheory.measure_inter_add_diff
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn
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
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))) : ℝ))
⊢ (↑(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]

Premises used: sub_eq_add_neg, neg_add
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn
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))) : ℝ))

Tactic:
abel
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn
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), 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
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn
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)))

Tactic:
Tendsto.sub ?_ ?_

Premises used: Filter.Tendsto.sub
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn
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))) : ℝ))
refine_2 :
  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)))

Tactic:
refine Tendsto.sub ?_ ?_

Premises used: ENNReal.Tendsto.sub
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn
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))) : ℝ))

Tactic:
NNReal.tendsto_coe.2 <| (ENNReal.tendsto_toNNReal ?_).comp <|
        tendsto_measure_iUnion_atTop hm

Premises used: Iff.mpr, MeasureTheory.tendsto_measure_iUnion_atTop, ENNReal.tendsto_toNNReal, NNReal.tendsto_coe, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Hahn
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 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Tendsto (fun (n : ℕ) ↦ (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) (s n))) : ℝ)) atTop
    (𝓝 (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n))) : ℝ))

Tactic:
refine NNReal.tendsto_coe.2 <| (ENNReal.tendsto_toNNReal ?_).comp <|
        tendsto_measure_iUnion_atTop hm

Premises used: Iff.mpr, MeasureTheory.tendsto_measure_iUnion_atTop, ENNReal.tendsto_toNNReal, NNReal.tendsto_coe, Filter.Tendsto.comp