awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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)
x : α
hx : x ∈ t
n : ℕ
hn : x ∈ v n
this : x ∈ t ∩ v n
⊢ x ∈ t ∩ w n

Tactic:
exact ⟨hx, subset_toMeasurable μ _ this⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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)
⊢ t ⊆ t'

Tactic:
have tt' : t ⊆ t' :=
      calc
        t ⊆ ⋃ n, t ∩ disjointed w n := by
          rw [← inter_iUnion, iUnion_disjointed, inter_iUnion]
          intro x hx
          rcases mem_iUnion.1 (hv hx) with ⟨n, hn⟩
          refine mem_iUnion.2 ⟨n, ?_⟩
          have : x ∈ t ∩ v n := ⟨hx, hn⟩
          exact ⟨hx, subset_toMeasurable μ _ this⟩
        _ ⊆ ⋃ n, toMeasurable μ (t ∩ disjointed w n) :=
          iUnion_mono fun n => subset_toMeasurable _ _
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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'
⊢ ∃ t' ⊇ t,
    MeasurableSet t' ∧
      ∀ (u : Set α),
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)

Tactic:
⟨t', tt', MeasurableSet.iUnion fun n => measurableSet_toMeasurable μ _, fun u hu => ?_⟩

Premises used: disjointed, Inter.inter, MeasureTheory.measurableSet_toMeasurable, And.intro, Exists.intro, MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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'
refine :
  ∀ (u : Set α) (hu : MeasurableSet u),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
⊢ ∃ t' ⊇ t,
    MeasurableSet t' ∧
      ∀ (u : Set α),
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)

Tactic:
refine ⟨t', tt', MeasurableSet.iUnion fun n => measurableSet_toMeasurable μ _, fun u hu => ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
apply : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)

Tactic:
apply le_antisymm _ (by gcongr)

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 :
  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∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞)
    (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (t ∩ disjointed w n) ∩ u) : ℝ≥0∞)

Tactic:
rw [ht', iUnion_inter]

Premises used: Set.iUnion_inter
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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∞) (⋃ (i : ℕ), toMeasurable μ (t ∩ disjointed w i) ∩ u) : ℝ≥0∞)
    (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (t ∩ disjointed w n) ∩ u) : ℝ≥0∞)

Tactic:
measure_iUnion_le _

Premises used: MeasureTheory.measure_iUnion_le
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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∞) (⋃ (i : ℕ), toMeasurable μ (t ∩ disjointed w i) ∩ u) : ℝ≥0∞)
    (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (t ∩ disjointed w n) ∩ u) : ℝ≥0∞)

Tactic:
exact measure_iUnion_le _

Premises used: MeasureTheory.measure_iUnion_le
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
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)
⊢ Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (t ∩ disjointed w n) ∩ u))
    (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n ∩ u))

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
e_f :
  ∀ (n : ℕ),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (t ∩ disjointed w n) ∩ u) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n ∩ u) : ℝ≥0∞)
⊢ Eq (α := ℕ → ℝ≥0∞) (fun (n : ℕ) ↦ (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (t ∩ disjointed w n) ∩ u)) fun (n : ℕ) ↦
    (μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n ∩ u)

Tactic:
ext1 n
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 : ℕ
e_f : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (t ∩ disjointed w n) ∩ u) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n ∩ u) : ℝ≥0∞)

Tactic:
apply measure_toMeasurable_inter hu

Premises used: MeasureTheory.Measure.measure_toMeasurable_inter
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 : ℕ
e_f : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
apply ne_of_lt

Premises used: ne_of_lt
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 : ℕ
h : disjointed w n ⊆ w n
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ w n) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 : ℕ
⊢ disjointed w n ⊆ w n

Tactic:
disjointed_le w n

Premises used: disjointed_le
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 : ℕ
⊢ disjointed w n ⊆ w n

Tactic:
exact disjointed_le w n

Premises used: disjointed_le
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 ∩ w n) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞)

Tactic:
measure_mono inter_subset_right

Premises used: MeasureTheory.measure_mono, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
hw n
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n) : ℝ≥0∞) (∞ : ℝ≥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

Premises used: disjointed, Inter.inter, MeasureTheory.measure_mono, DFunLike.coe, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
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)
⊢ Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n ∩ u))
    (∑' (n : ℕ), (μ.restrict (t ∩ u) : (a : Set α) → ℝ≥0∞) (disjointed w n))

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
e_f :
  ∀ (n : ℕ),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n ∩ u) : ℝ≥0∞)
      ((μ.restrict (t ∩ u) : (a : Set α) → ℝ≥0∞) (disjointed w n) : ℝ≥0∞)
⊢ Eq (α := ℕ → ℝ≥0∞) (fun (n : ℕ) ↦ (μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n ∩ u)) fun (n : ℕ) ↦
    (μ.restrict (t ∩ u) : (a : Set α) → ℝ≥0∞) (disjointed w n)

Tactic:
ext1 n
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 : ℕ
e_f : MeasurableSet (disjointed w n)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n ∩ u) : ℝ≥0∞)
    ((μ.restrict (t ∩ u) : (a : Set α) → ℝ≥0∞) (disjointed w n) : ℝ≥0∞)

Tactic:
rw [restrict_apply, inter_comm t _, inter_assoc]

Premises used: MeasureTheory.Measure.restrict_apply, Set.inter_comm, Set.inter_assoc
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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)

Tactic:
MeasurableSet.disjointed (fun n => ?_) n

Premises used: MeasurableSet.disjointed
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 : ℕ
e_f : ∀ (n : ℕ), MeasurableSet (w n)
⊢ MeasurableSet (disjointed w n)

Tactic:
refine MeasurableSet.disjointed (fun n => ?_) n

Premises used: MeasurableSet.disjointed
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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_1 n : ℕ
⊢ MeasurableSet (w n)

Tactic:
measurableSet_toMeasurable _ _

Premises used: MeasureTheory.measurableSet_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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_1 n : ℕ
⊢ MeasurableSet (w n)

Tactic:
exact measurableSet_toMeasurable _ _

Premises used: MeasureTheory.measurableSet_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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)
h : ∀ (i : ℕ), MeasurableSet (disjointed w i)
⊢ Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ.restrict (t ∩ u) : (a : Set α) → ℝ≥0∞) (disjointed w n) : ℝ≥0∞)
    ((μ.restrict (t ∩ u) : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), disjointed w n) : ℝ≥0∞)

Tactic:
rw [measure_iUnion]

Premises used: MeasureTheory.measure_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
⊢ Pairwise (Disjoint on disjointed w)

Tactic:
disjoint_disjointed _

Premises used: disjoint_disjointed