awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
d_split : ∀ (s t : Set α) (ht : MeasurableSet t), d s = d (s \ t) + d (s ∩ t)
⊢ ∃ (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_Union : ∀ (s : ℕ → Set α) (hm : Monotone s), Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋃ (n : ℕ), s n)))
Tactic: have d_Union (s : ℕ → Set α) (hm : Monotone s) :
    Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋃ n, s n))) := by
    refine Tendsto.sub ?_ ?_ <;>
      refine NNReal.tendsto_coe.2 <| (ENNReal.tendsto_toNNReal ?_).comp <|
        tendsto_measure_iUnion_atTop hm
    · exact hμ _
    · exact 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
d_split : ∀ (s t : Set α) (ht : MeasurableSet t), d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α) (hm : Monotone s), Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋃ (n : ℕ), s n)))
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hm : ∀ (n m : ℕ), n ≤ m → s m ⊆ s n
⊢ 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)
d_Union : ∀ (s : ℕ → Set α) (hm : Monotone s), Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋃ (n : ℕ), s n)))
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hm : ∀ (n m : ℕ), n ≤ m → s m ⊆ s n
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)
d_Union : ∀ (s : ℕ → Set α) (hm : Monotone s), Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋃ (n : ℕ), s n)))
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hm : ∀ (n m : ℕ), n ≤ m → s m ⊆ s n
⊢ 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_iInter_atTop (fun n ↦ (hs n).nullMeasurableSet) 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)
d_Union : ∀ (s : ℕ → Set α) (hm : Monotone s), Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋃ (n : ℕ), s n)))
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hm : ∀ (n m : ℕ), n ≤ m → s m ⊆ s n
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))) : ℝ))
have refine_1₁ : ∃ (i : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine NNReal.tendsto_coe.2 <| (ENNReal.tendsto_toNNReal <| ?_).comp <|
        tendsto_measure_iInter_atTop (fun n ↦ (hs n).nullMeasurableSet) 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)
d_Union : ∀ (s : ℕ → Set α) (hm : Monotone s), Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋃ (n : ℕ), s n)))
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hm : ∀ (n m : ℕ), n ≤ m → s m ⊆ s n
⊢ 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_iInter_atTop (fun n ↦ (hs n).nullMeasurableSet) 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)
d_Union : ∀ (s : ℕ → Set α) (hm : Monotone s), Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋃ (n : ℕ), s n)))
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hm : ∀ (n m : ℕ), n ≤ m → s m ⊆ s n
refine_2 : 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))) : ℝ))
have refine_2₁ : ∃ (i : ℕ), Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine NNReal.tendsto_coe.2 <| (ENNReal.tendsto_toNNReal <| ?_).comp <|
        tendsto_measure_iInter_atTop (fun n ↦ (hs n).nullMeasurableSet) hm ?_
-- 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
d_split : ∀ (s t : Set α) (ht : MeasurableSet t), d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α) (hm : Monotone s), Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋃ (n : ℕ), s n)))
⊢ ∃ (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_Inter : ∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)) (hm : ∀ (n m : ℕ), n ≤ m → s m ⊆ s n),
  Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋂ (n : ℕ), s n)))
Tactic: have d_Inter (s : ℕ → Set α) (hs : ∀ n, MeasurableSet (s n)) (hm : ∀ n m, n ≤ m → s m ⊆ s n) :
        Tendsto (fun n => d (s n)) atTop (𝓝 (d (⋂ n, s n))) := by
    refine Tendsto.sub ?_ ?_ <;>
      refine NNReal.tendsto_coe.2 <| (ENNReal.tendsto_toNNReal <| ?_).comp <|
        tendsto_measure_iInter_atTop (fun n ↦ (hs n).nullMeasurableSet) hm ?_
    exacts [hμ _, ⟨0, hμ _⟩, hν _, ⟨0, 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
d_split : ∀ (s t : Set α) (ht : MeasurableSet t), d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α) (hm : Monotone s), Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋃ (n : ℕ), s n)))
d_Inter :
  ∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)) (hm : ∀ (n m : ℕ), n ≤ m → s m ⊆ s n),
    Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋂ (n : ℕ), s n)))
⊢ BddAbove c
have h : (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) univ)) : ℝ) ∈ upperBounds c
Tactic: use (μ univ).toNNReal
-- 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)
d_Union : ∀ (s : ℕ → Set α) (hm : Monotone s), Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋃ (n : ℕ), s n)))
d_Inter :
  ∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)) (hm : ∀ (n m : ℕ), n ≤ m → s m ⊆ s n),
    Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋂ (n : ℕ), s n)))
s : Set α
_hs : Membership.mem (γ := Set (Set α)) {s : Set α | MeasurableSet s} s
⊢ d s ≤ (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) univ)) : ℝ)
have h : (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ) ≤ (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) univ)) : ℝ)
Tactic: refine le_trans (sub_le_self _ <| NNReal.coe_nonneg _) ?_
-- 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)
d_Union : ∀ (s : ℕ → Set α) (hm : Monotone s), Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋃ (n : ℕ), s n)))
d_Inter :
  ∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)) (hm : ∀ (n m : ℕ), n ≤ m → s m ⊆ s n),
    Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋂ (n : ℕ), s n)))
s : Set α
_hs : Membership.mem (γ := Set (Set α)) {s : Set α | MeasurableSet s} s
⊢ (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) s)) : ℝ) ≤ (↑(ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) univ)) : ℝ)
have h : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [NNReal.coe_le_coe, ← ENNReal.coe_le_coe, to_nnreal_μ, to_nnreal_μ]
-- 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
d_split : ∀ (s t : Set α) (ht : MeasurableSet t), d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α) (hm : Monotone s), Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋃ (n : ℕ), s n)))
d_Inter :
  ∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)) (hm : ∀ (n m : ℕ), n ≤ m → s m ⊆ s n),
    Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋂ (n : ℕ), s n)))
⊢ ∃ (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 bdd_c : BddAbove c
Tactic: have bdd_c : BddAbove c := by
    use (μ univ).toNNReal
    rintro r ⟨s, _hs, rfl⟩
    refine le_trans (sub_le_self _ <| NNReal.coe_nonneg _) ?_
    rw [NNReal.coe_le_coe, ← ENNReal.coe_le_coe, to_nnreal_μ, to_nnreal_μ]
    exact measure_mono (subset_univ _)
-- 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
d_split : ∀ (s t : Set α) (ht : MeasurableSet t), d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α) (hm : Monotone s), Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋃ (n : ℕ), s n)))
d_Inter :
  ∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)) (hm : ∀ (n m : ℕ), n ≤ m → s m ⊆ s n),
    Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋂ (n : ℕ), s n)))
bdd_c : BddAbove 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 c_nonempty : c.Nonempty
Tactic: have c_nonempty : c.Nonempty := Nonempty.image _ ⟨_, MeasurableSet.empty⟩
-- 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
d_split : ∀ (s t : Set α) (ht : MeasurableSet t), d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α) (hm : Monotone s), Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋃ (n : ℕ), s n)))
d_Inter :
  ∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)) (hm : ∀ (n m : ℕ), n ≤ m → s m ⊆ s n),
    Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋂ (n : ℕ), s n)))
bdd_c : BddAbove c
c_nonempty : c.Nonempty
⊢ ∃ (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_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ
Tactic: have d_le_γ : ∀ s, MeasurableSet s → d s ≤ γ := fun s hs => le_csSup bdd_c ⟨s, hs, rfl⟩
-- 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
d_split : ∀ (s t : Set α) (ht : MeasurableSet t), d s = d (s \ t) + d (s ∩ t)
d_Union : ∀ (s : ℕ → Set α) (hm : Monotone s), Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋃ (n : ℕ), s n)))
d_Inter :
  ∀ (s : ℕ → Set α) (hs : ∀ (n : ℕ), MeasurableSet (s n)) (hm : ∀ (n m : ℕ), n ≤ m → s m ⊆ s n),
    Tendsto (fun (n : ℕ) ↦ d (s n)) atTop (𝓝 (d (⋂ (n : ℕ), s n)))
bdd_c : BddAbove c
c_nonempty : c.Nonempty
d_le_γ : ∀ (s : Set α), MeasurableSet s → d s ≤ γ
n : ℕ
⊢ ∃ (s : Set α), MeasurableSet s ∧ γ - (1 / 2) ^ n < d s
have this : γ - (1 / 2) ^ n < γ
Tactic: have : γ - (1 / 2) ^ n < γ := sub_lt_self γ (pow_pos (half_pos zero_lt_one) n)