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)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ Pairwise (Disjoint on disjointed w)

Tactic:
exact disjoint_disjointed _

Premises used: disjoint_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
i : ℕ
⊢ MeasurableSet (disjointed w i)

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

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
i : ℕ
h : ∀ (n : ℕ), MeasurableSet (w n)
⊢ MeasurableSet (disjointed w i)

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

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
i 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
i 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
⊢ LE.le (α := ℝ≥0∞) ((μ.restrict (t ∩ u) : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), disjointed w n) : ℝ≥0∞)
    ((μ.restrict (t ∩ u) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
measure_mono (subset_univ _)

Premises used: Set.subset_univ, MeasureTheory.measure_mono
-- 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 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (univ ∩ (t ∩ u)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (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∞)

Tactic:
rw [restrict_apply MeasurableSet.univ, univ_inter]

Premises used: MeasureTheory.Measure.restrict_apply, Set.univ_inter, MeasurableSet.univ
-- 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∞)
    (∑' (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))
μ₃ :
  Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (t ∩ disjointed w n ∩ u))
    (∑' (n : ℕ), (μ.restrict (t ∩ u) : (a : Set α) → ℝ≥0∞) (disjointed w n))
μ₄ :
  Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ.restrict (t ∩ u) : (a : Set α) → ℝ≥0∞) (disjointed w n) : ℝ≥0∞)
    ((μ.restrict (t ∩ u) : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), disjointed w n) : ℝ≥0∞)
μ₅ : Eq (α := ℝ≥0∞) ((μ.restrict (t ∩ u) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ 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]

Premises used: Set.subset_univ, Set.univ, disjointed, MeasureTheory.Measure.restrict, Inter.inter, MeasureTheory.measure_mono, DFunLike.coe, Set.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∞)
⊢ ∃ t' ⊇ t,
    MeasurableSet t' ∧
      ∀ (u : Set α),
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)

Tactic:
have A : ∃ t', t' ⊇ t ∧ MeasurableSet t' ∧ ∀ u, MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u) := by
    let w n := toMeasurable μ (t ∩ v n)
    have hw : ∀ n, μ (w n) < ∞ := by
      intro n
      simp_rw [w, measure_toMeasurable]
      exact (h'v n).lt_top
    set t' := ⋃ n, toMeasurable μ (t ∩ disjointed w n) with ht'
    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 _ _
    refine ⟨t', tt', MeasurableSet.iUnion fun n => measurableSet_toMeasurable μ _, fun u hu => ?_⟩
    apply le_antisymm _ (by gcongr)
    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]
-- 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∞)
A :
  ∃ t' ⊇ t,
    MeasurableSet t' ∧
      ∀ (u : Set α),
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
rw :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        ((if h : ∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t then
            h.choose (p := fun (t_1 : Set α) ↦ t_1 ⊇ t ∧ MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t)
          else
            if h' :
                ∃ t_1 ⊇ t,
                  MeasurableSet t_1 ∧
                    ∀ (u : Set α),
                      MeasurableSet u →
                        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t_1 ∩ u) : ℝ≥0∞)
                          ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) then
              h'.choose (p := fun (t_1 : Set α) ↦
                t_1 ⊇ t ∧
                  MeasurableSet t_1 ∧
                    ∀ (u : Set α),
                      MeasurableSet u →
                        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t_1 ∩ u) : ℝ≥0∞)
                          ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞))
            else
              ⋯.choose (p := fun (t_1 : Set α) ↦
                t ⊆ t_1 ∧
                  MeasurableSet t_1 ∧
                    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t_1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞))) ∩
          s) :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ t ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)

Tactic:
rw [toMeasurable]

Premises used: MeasureTheory.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∞)
A :
  ∃ t' ⊇ t,
    MeasurableSet t' ∧
      ∀ (u : Set α),
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
pos :
  ∀ (ht : ∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t),
    Eq (α := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (ht.choose (p := fun (t_1 : Set α) ↦ t_1 ⊇ t ∧ MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t) ∩ s) :
        ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
neg :
  ∀ (ht : ¬∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t),
    Eq (α := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (A.choose (p := fun (t_1 : Set α) ↦
              t_1 ⊇ t ∧
                MeasurableSet t_1 ∧
                  ∀ (u : Set α),
                    MeasurableSet u →
                      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t_1 ∩ u) : ℝ≥0∞)
                        ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)) ∩
            s) :
        ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        ((if h : ∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t then
            h.choose (p := fun (t_1 : Set α) ↦ t_1 ⊇ t ∧ MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t)
          else
            if h' :
                ∃ t_1 ⊇ t,
                  MeasurableSet t_1 ∧
                    ∀ (u : Set α),
                      MeasurableSet u →
                        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t_1 ∩ u) : ℝ≥0∞)
                          ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) then
              h'.choose (p := fun (t_1 : Set α) ↦
                t_1 ⊇ t ∧
                  MeasurableSet t_1 ∧
                    ∀ (u : Set α),
                      MeasurableSet u →
                        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t_1 ∩ u) : ℝ≥0∞)
                          ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞))
            else
              ⋯.choose (p := fun (t_1 : Set α) ↦
                t ⊆ t_1 ∧
                  MeasurableSet t_1 ∧
                    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t_1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞))) ∩
          s) :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)

Tactic:
split_ifs with ht
-- 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∞)
A :
  ∃ t' ⊇ t,
    MeasurableSet t' ∧
      ∀ (u : Set α),
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
ht : ∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t
pos : ht.choose (p := fun (t_1 : Set α) ↦ t_1 ⊇ t ∧ MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t) ∩ s =ᶠ[ae μ] t ∩ s
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (ht.choose (p := fun (t_1 : Set α) ↦ t_1 ⊇ t ∧ MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t) ∩ s) :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)

Tactic:
apply measure_congr

Premises used: MeasureTheory.measure_congr
-- 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∞)
A :
  ∃ t' ⊇ t,
    MeasurableSet t' ∧
      ∀ (u : Set α),
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
ht : ∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t
⊢ ht.choose (p := fun (t_1 : Set α) ↦ t_1 ⊇ t ∧ MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t) ∩ s =ᶠ[ae μ] t ∩ s

Tactic:
ae_eq_set_inter ht.choose_spec.2.2 (ae_eq_refl _)

Premises used: Exists.choose_spec, MeasureTheory.ae_eq_refl, MeasureTheory.ae_eq_set_inter, And.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∞)
A :
  ∃ t' ⊇ t,
    MeasurableSet t' ∧
      ∀ (u : Set α),
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
ht : ∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t
⊢ ht.choose (p := fun (t_1 : Set α) ↦ t_1 ⊇ t ∧ MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t) ∩ s =ᶠ[ae μ] t ∩ s

Tactic:
exact ae_eq_set_inter ht.choose_spec.2.2 (ae_eq_refl _)

Premises used: Exists.choose_spec, MeasureTheory.ae_eq_refl, MeasureTheory.ae_eq_set_inter, And.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∞)
A :
  ∃ t' ⊇ t,
    MeasurableSet t' ∧
      ∀ (u : Set α),
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
ht : ¬∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (A.choose (p := fun (t_1 : Set α) ↦
            t_1 ⊇ t ∧
              MeasurableSet t_1 ∧
                ∀ (u : Set α),
                  MeasurableSet u →
                    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t_1 ∩ u) : ℝ≥0∞)
                      ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)) ∩
          s) :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)

Tactic:
A.choose_spec.2.2 s hs

Premises used: Exists.choose_spec, And.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∞)
A :
  ∃ t' ⊇ t,
    MeasurableSet t' ∧
      ∀ (u : Set α),
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
ht : ¬∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (A.choose (p := fun (t_1 : Set α) ↦
            t_1 ⊇ t ∧
              MeasurableSet t_1 ∧
                ∀ (u : Set α),
                  MeasurableSet u →
                    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t_1 ∩ u) : ℝ≥0∞)
                      ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)) ∩
          s) :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)

Tactic:
exact A.choose_spec.2.2 s hs

Premises used: Exists.choose_spec, And.right
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
v : ℕ → Set α
hv : s ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (toMeasurable μ s) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
simp only [restrict_apply ht, inter_comm t, measure_toMeasurable_inter_of_cover ht hv h'v]

Premises used: MeasureTheory.Measure.restrict_apply, MeasureTheory.Measure.measure_toMeasurable_inter_of_cover, Set.inter_comm
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
s : Set α
hs : MeasurableSet s
t : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ t ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)

Tactic:
measure_toMeasurable_inter_of_sum hs (fun _ ↦ measure_ne_top _ t) (sum_sfiniteSeq μ).symm

Premises used: MeasureTheory.measure_ne_top, MeasureTheory.sum_sfiniteSeq, MeasureTheory.Measure.measure_toMeasurable_inter_of_sum, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
s t : Set α
ht : MeasurableSet t
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ toMeasurable μ s) : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s ∩ t) : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
rw₄ rw₅ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (toMeasurable μ s) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [restrict_apply ht, inter_comm t, measure_toMeasurable_inter_of_sFinite ht,
      restrict_apply ht, inter_comm t]

Premises used: MeasureTheory.Measure.restrict_apply, MeasureTheory.Measure.measure_toMeasurable_inter_of_sFinite, Set.inter_comm
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : SigmaFinite μ
hs : MeasurableSet s
rw : Eq (α := ℝ≥0∞) ((μ.restrict univ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (⋃ (i : ℕ), spanningSets μ i) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [iUnion_spanningSets, restrict_univ]

Premises used: MeasureTheory.iUnion_spanningSets, MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
s : Set α
rw :
  Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) s)
    (⨆ (i : ℕ), (μ.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) (toMeasurable μ s))
⊢ Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [← measure_toMeasurable s,
    ← iSup_restrict_spanningSets_of_measurableSet (measurableSet_toMeasurable _ _)]

Premises used: MeasureTheory.measure_toMeasurable, MeasureTheory.measurableSet_toMeasurable, MeasureTheory.Measure.iSup_restrict_spanningSets_of_measurableSet