awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
have apply : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
Tactic: apply le_antisymm _ (by gcongr)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞)
    (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (t ∩ disjointed w n) ∩ u) : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), toMeasurable μ (t ∩ disjointed w i) ∩ u) : ℝ≥0∞)
  (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (t ∩ disjointed w n) ∩ u) : ℝ≥0∞)
Tactic: rw [ht', iUnion_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (t ∩ disjointed w n) ∩ u))
    (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n ∩ u))
have e_f : Eq (α := ℕ → ℝ≥0∞) (fun (n : ℕ) ↦ (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (t ∩ disjointed w n) ∩ u)) fun (n : ℕ) ↦
  (μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n ∩ u)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ Eq (α := ℕ → ℝ≥0∞) (fun (n : ℕ) ↦ (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (t ∩ disjointed w n) ∩ u)) fun (n : ℕ) ↦
    (μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n ∩ u)
have e_f : ∀ (n : ℕ),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (t ∩ disjointed w n) ∩ u) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n ∩ u) : ℝ≥0∞)
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n : ℕ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (t ∩ disjointed w n) ∩ u) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n ∩ u) : ℝ≥0∞)
have e_f : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: apply measure_toMeasurable_inter hu
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n : ℕ
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
have e_f : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: apply ne_of_lt
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n : ℕ
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ w n) : ℝ≥0∞)
have h : disjointed w n ⊆ w n
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n : ℕ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
have μ₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ w n) : ℝ≥0∞)
Tactic: calc
          μ (t ∩ disjointed w n) ≤ μ (t ∩ w n) := by
            gcongr
            exact disjointed_le w n
          _ ≤ μ (w n) := measure_mono inter_subset_right
          _ < ∞ := hw n
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n ∩ u))
    (∑' (n : ℕ), (μ.restrict (t ∩ u) : (a : Set α) → ℝ≥0∞) (disjointed w n))
have e_f : Eq (α := ℕ → ℝ≥0∞) (fun (n : ℕ) ↦ (μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n ∩ u)) fun (n : ℕ) ↦
  (μ.restrict (t ∩ u) : (a : Set α) → ℝ≥0∞) (disjointed w n)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ Eq (α := ℕ → ℝ≥0∞) (fun (n : ℕ) ↦ (μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n ∩ u)) fun (n : ℕ) ↦
    (μ.restrict (t ∩ u) : (a : Set α) → ℝ≥0∞) (disjointed w n)
have e_f : ∀ (n : ℕ),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n ∩ u) : ℝ≥0∞)
    ((μ.restrict (t ∩ u) : (a : Set α) → ℝ≥0∞) (disjointed w n) : ℝ≥0∞)
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n : ℕ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n ∩ u) : ℝ≥0∞)
    ((μ.restrict (t ∩ u) : (a : Set α) → ℝ≥0∞) (disjointed w n) : ℝ≥0∞)
have e_f : MeasurableSet (disjointed w n)
Tactic: rw [restrict_apply, inter_comm t _, inter_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n : ℕ
⊢ MeasurableSet (disjointed w n)
have e_f : ∀ (n : ℕ), MeasurableSet (w n)
Tactic: refine MeasurableSet.disjointed (fun n => ?_) n
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ.restrict (t ∩ u) : (a : Set α) → ℝ≥0∞) (disjointed w n) : ℝ≥0∞)
    ((μ.restrict (t ∩ u) : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), disjointed w n) : ℝ≥0∞)
have hn : Pairwise (Disjoint on disjointed w)
Tactic: rw [measure_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
hn : Pairwise (Disjoint on disjointed w)
⊢ Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ.restrict (t ∩ u) : (a : Set α) → ℝ≥0∞) (disjointed w n) : ℝ≥0∞)
    ((μ.restrict (t ∩ u) : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), disjointed w n) : ℝ≥0∞)
have h : ∀ (i : ℕ), MeasurableSet (disjointed w i)
Tactic: rw [measure_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
i : ℕ
⊢ MeasurableSet (disjointed w i)
have h : ∀ (n : ℕ), MeasurableSet (w n)
Tactic: refine MeasurableSet.disjointed (fun n => ?_) i
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (t ∩ u) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (univ ∩ (t ∩ u)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
Tactic: rw [restrict_apply MeasurableSet.univ, univ_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (univ ∩ (t ∩ u)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (t ∩ u) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
Tactic: rw [restrict_apply MeasurableSet.univ, univ_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
have μ₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞)
  (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (t ∩ disjointed w n) ∩ u) : ℝ≥0∞)
Tactic: calc
      μ (t' ∩ u) ≤ ∑' n, μ (toMeasurable μ (t ∩ disjointed w n) ∩ u) := by
        rw [ht', iUnion_inter]
        exact measure_iUnion_le _
      _ = ∑' n, μ (t ∩ disjointed w n ∩ u) := by
        congr 1
        ext1 n
        apply measure_toMeasurable_inter hu
        apply ne_of_lt
        calc
          μ (t ∩ disjointed w n) ≤ μ (t ∩ w n) := by
            gcongr
            exact disjointed_le w n
          _ ≤ μ (w n) := measure_mono inter_subset_right
          _ < ∞ := hw n
      _ = ∑' n, μ.restrict (t ∩ u) (disjointed w n) := by
        congr 1
        ext1 n
        rw [restrict_apply, inter_comm t _, inter_assoc]
        refine MeasurableSet.disjointed (fun n => ?_) n
        exact measurableSet_toMeasurable _ _
      _ = μ.restrict (t ∩ u) (⋃ n, disjointed w n) := by
        rw [measure_iUnion]
        · exact disjoint_disjointed _
        · intro i
          refine MeasurableSet.disjointed (fun n => ?_) i
          exact measurableSet_toMeasurable _ _
      _ ≤ μ.restrict (t ∩ u) univ := measure_mono (subset_univ _)
      _ = μ (t ∩ u) := by rw [restrict_apply MeasurableSet.univ, univ_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
μ₁ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞)
    (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (t ∩ disjointed w n) ∩ u) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
have μ₂ : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (t ∩ disjointed w n) ∩ u))
  (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n ∩ u))
Tactic: calc
      μ (t' ∩ u) ≤ ∑' n, μ (toMeasurable μ (t ∩ disjointed w n) ∩ u) := by
        rw [ht', iUnion_inter]
        exact measure_iUnion_le _
      _ = ∑' n, μ (t ∩ disjointed w n ∩ u) := by
        congr 1
        ext1 n
        apply measure_toMeasurable_inter hu
        apply ne_of_lt
        calc
          μ (t ∩ disjointed w n) ≤ μ (t ∩ w n) := by
            gcongr
            exact disjointed_le w n
          _ ≤ μ (w n) := measure_mono inter_subset_right
          _ < ∞ := hw n
      _ = ∑' n, μ.restrict (t ∩ u) (disjointed w n) := by
        congr 1
        ext1 n
        rw [restrict_apply, inter_comm t _, inter_assoc]
        refine MeasurableSet.disjointed (fun n => ?_) n
        exact measurableSet_toMeasurable _ _
      _ = μ.restrict (t ∩ u) (⋃ n, disjointed w n) := by
        rw [measure_iUnion]
        · exact disjoint_disjointed _
        · intro i
          refine MeasurableSet.disjointed (fun n => ?_) i
          exact measurableSet_toMeasurable _ _
      _ ≤ μ.restrict (t ∩ u) univ := measure_mono (subset_univ _)
      _ = μ (t ∩ u) := by rw [restrict_apply MeasurableSet.univ, univ_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
μ₁ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞)
    (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (t ∩ disjointed w n) ∩ u) : ℝ≥0∞)
μ₂ :
  Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (t ∩ disjointed w n) ∩ u))
    (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n ∩ u))
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
have μ₃ : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n ∩ u))
  (∑' (n : ℕ), (μ.restrict (t ∩ u) : (a : Set α) → ℝ≥0∞) (disjointed w n))
Tactic: calc
      μ (t' ∩ u) ≤ ∑' n, μ (toMeasurable μ (t ∩ disjointed w n) ∩ u) := by
        rw [ht', iUnion_inter]
        exact measure_iUnion_le _
      _ = ∑' n, μ (t ∩ disjointed w n ∩ u) := by
        congr 1
        ext1 n
        apply measure_toMeasurable_inter hu
        apply ne_of_lt
        calc
          μ (t ∩ disjointed w n) ≤ μ (t ∩ w n) := by
            gcongr
            exact disjointed_le w n
          _ ≤ μ (w n) := measure_mono inter_subset_right
          _ < ∞ := hw n
      _ = ∑' n, μ.restrict (t ∩ u) (disjointed w n) := by
        congr 1
        ext1 n
        rw [restrict_apply, inter_comm t _, inter_assoc]
        refine MeasurableSet.disjointed (fun n => ?_) n
        exact measurableSet_toMeasurable _ _
      _ = μ.restrict (t ∩ u) (⋃ n, disjointed w n) := by
        rw [measure_iUnion]
        · exact disjoint_disjointed _
        · intro i
          refine MeasurableSet.disjointed (fun n => ?_) i
          exact measurableSet_toMeasurable _ _
      _ ≤ μ.restrict (t ∩ u) univ := measure_mono (subset_univ _)
      _ = μ (t ∩ u) := by rw [restrict_apply MeasurableSet.univ, univ_inter]