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
μ₁ :
  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))
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
have μ₄ : 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: 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))
μ₃ :
  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∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
have μ₅ : Eq (α := ℝ≥0∞) ((μ.restrict (t ∩ u) : (a : Set α) → ℝ≥0∞) univ : ℝ≥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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (hypothesis)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ t ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
have A : ∃ 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]
-- 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∞)
A :
  ∃ t' ⊇ t,
    MeasurableSet t' ∧
      ∀ (u : Set α),
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ t ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
have 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
            sorry.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: rw [toMeasurable]
-- 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∞)
A :
  ∃ t' ⊇ t,
    MeasurableSet t' ∧
      ∀ (u : Set α),
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥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∞)
have 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∞)
Tactic: split_ifs with ht
-- 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∞)
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∞)
⊢ 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∞)
have 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∞)
Tactic: split_ifs with ht
-- 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∞)
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∞) (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∞)
have pos : ht.choose (p := fun (t_1 : Set α) ↦ t_1 ⊇ t ∧ MeasurableSet t_1 ∧ t_1 =ᶠ[ae μ] t) ∩ s =ᶠ[ae μ] t ∩ s
Tactic: apply measure_congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
s t : Set α
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (toMeasurable μ s) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ toMeasurable μ s) : ℝ≥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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (toMeasurable μ s) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s ∩ 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (toMeasurable μ s) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (toMeasurable μ s) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: rw [restrict_apply ht, inter_comm t, measure_toMeasurable_inter_of_sFinite ht,
      restrict_apply ht, inter_comm t]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (toMeasurable μ s) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw₄ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
Tactic: rw [restrict_apply ht, inter_comm t, measure_toMeasurable_inter_of_sFinite ht,
      restrict_apply ht, inter_comm t]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : SigmaFinite μ
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (⋃ (i : ℕ), spanningSets μ i) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ.restrict univ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [iUnion_spanningSets, restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (⋃ (i : ℕ), spanningSets μ i) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [iUnion_spanningSets, restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
s : Set α
⊢ Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) s)
  (⨆ (i : ℕ), (μ.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) (toMeasurable μ s))
Tactic: rw [← measure_toMeasurable s,
    ← iSup_restrict_spanningSets_of_measurableSet (measurableSet_toMeasurable _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
s : Set α
⊢ Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) s)
    (⨆ (i : ℕ), (μ.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) (toMeasurable μ s))
have simp_rw : Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ spanningSets μ i))
  (⨆ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s ∩ spanningSets μ i))
Tactic: simp_rw [restrict_apply' (measurableSet_spanningSets μ _), Set.inter_comm s,
    ← restrict_apply (measurableSet_spanningSets μ _), ← restrict_toMeasurable_of_sFinite s,
    restrict_apply (measurableSet_spanningSets μ _), Set.inter_comm _ (toMeasurable μ s)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
s : Set α
simp_rw :
  Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ spanningSets μ i))
    (⨆ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s ∩ spanningSets μ i))
⊢ Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) s)
    (⨆ (i : ℕ), (μ.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) (toMeasurable μ s))
have simp_rw₁ : Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (spanningSets μ i ∩ s))
  (⨆ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s ∩ spanningSets μ i))
Tactic: simp_rw [restrict_apply' (measurableSet_spanningSets μ _), Set.inter_comm s,
    ← restrict_apply (measurableSet_spanningSets μ _), ← restrict_toMeasurable_of_sFinite s,
    restrict_apply (measurableSet_spanningSets μ _), Set.inter_comm _ (toMeasurable μ s)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
s : Set α
simp_rw :
  Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ spanningSets μ i))
    (⨆ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s ∩ spanningSets μ i))
simp_rw₁ :
  Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (spanningSets μ i ∩ s))
    (⨆ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s ∩ spanningSets μ i))
⊢ Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) s)
    (⨆ (i : ℕ), (μ.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) (toMeasurable μ s))
have simp_rw₂ : Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ.restrict s : (a : Set α) → ℝ≥0∞) (spanningSets μ i))
  (⨆ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s ∩ spanningSets μ i))
Tactic: simp_rw [restrict_apply' (measurableSet_spanningSets μ _), Set.inter_comm s,
    ← restrict_apply (measurableSet_spanningSets μ _), ← restrict_toMeasurable_of_sFinite s,
    restrict_apply (measurableSet_spanningSets μ _), Set.inter_comm _ (toMeasurable μ s)]