awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hμst : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
have suffices : ∀ (u v : Set α),
  Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∆ v) : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞) →
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: suffices h : ∀ u v, μ (u ∆ v) ≠ ∞ → μ u = ∞ → μ v = ∞
    from ⟨h s t hμst, h t s (symmDiff_comm s t ▸ hμst)⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hμst : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
u v : Set α
hμuv : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∆ v) : ℝ≥0∞) (∞ : ℝ≥0∞)
hμu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)
have by_contra! : ∀ (hμv : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)), False
Tactic: by_contra! hμv
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hμst : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
u v : Set α
hμuv : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∆ v) : ℝ≥0∞) (∞ : ℝ≥0∞)
hμu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
hμv : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ False
have apply : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∆ v) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: apply hμuv
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hμst : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
u v : Set α
hμuv : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∆ v) : ℝ≥0∞) (∞ : ℝ≥0∞)
hμu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
hμv : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∆ v) : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u \ v ∪ v \ u) : ℝ≥0∞)
Tactic: rw [Set.symmDiff_def, eq_top_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hμst : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
u v : Set α
hμuv : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∆ v) : ℝ≥0∞) (∞ : ℝ≥0∞)
hμu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
hμv : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∞ = HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ∞ ∞
Tactic: rw [ENNReal.sub_eq_top_iff.2 ⟨hμu, hμv⟩]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hμst : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
u v : Set α
hμuv : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∆ v) : ℝ≥0∞) (∞ : ℝ≥0∞)
hμu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
hμv : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u \ v ∪ v \ u) : ℝ≥0∞)
have μ₁ : ∞ = HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) v : ℝ≥0∞)
Tactic: calc
    ∞ = μ u - μ v := by rw [ENNReal.sub_eq_top_iff.2 ⟨hμu, hμv⟩]
    _ ≤ μ (u \ v) := le_measure_diff
    _ ≤ μ (u \ v ∪ v \ u) := measure_mono subset_union_left
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
hst : s ⊆ t
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
h : (μ : (a : Set α) → ℝ≥0∞) t < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
⊢ (μ : (a : Set α) → ℝ≥0∞) (t \ s) < ε
have rw : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) < ε
Tactic: rw [measure_diff hst hs hs']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
hst : s ⊆ t
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
h : (μ : (a : Set α) → ℝ≥0∞) t < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
⊢ HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) < ε
have h₁ : (μ : (a : Set α) → ℝ≥0∞) t < HAdd.hAdd (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [add_comm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
hst : s ⊆ t
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
⊢ (μ : (a : Set α) → ℝ≥0∞) (t \ s) ≤ ε ↔
    (μ : (a : Set α) → ℝ≥0∞) t ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
have rw : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤ ε ↔
  (μ : (a : Set α) → ℝ≥0∞) t ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
Tactic: rw [measure_diff hst hs hs', tsub_le_iff_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
hst : s ⊆ t
hs' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ≥0∞
rw :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤ ε ↔
    (μ : (a : Set α) → ℝ≥0∞) t ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
⊢ (μ : (a : Set α) → ℝ≥0∞) (t \ s) ≤ ε ↔
    (μ : (a : Set α) → ℝ≥0∞) t ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
have rw₁ : (μ : (a : Set α) → ℝ≥0∞) t ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε ↔
  (μ : (a : Set α) → ℝ≥0∞) t ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ε
Tactic: rw [measure_diff hst hs hs', tsub_le_iff_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nulldiff : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₃ \ s₁) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₃ : ℝ≥0∞)
have le12 : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞)
Tactic: have le12 : μ s₁ ≤ μ s₂ := measure_mono h12
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nulldiff : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₃ \ s₁) : ℝ≥0∞) (0 : ℝ≥0∞)
le12 : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₃ : ℝ≥0∞)
have le23 : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₃ : ℝ≥0∞)
Tactic: have le23 : μ s₂ ≤ μ s₃ := measure_mono h23
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nulldiff : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₃ \ s₁) : ℝ≥0∞) (0 : ℝ≥0∞)
le12 : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞)
le23 : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₃ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₃ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₃ \ s₁ ∪ s₁) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₃ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₃ : ℝ≥0∞)
Tactic: rw [diff_union_of_subset (h12.trans h23)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nulldiff : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₃ \ s₁) : ℝ≥0∞) (0 : ℝ≥0∞)
le12 : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞)
le23 : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₃ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₃ : ℝ≥0∞)
have key : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₃ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞)
Tactic: have key : μ s₃ ≤ μ s₁ :=
    calc
      μ s₃ = μ (s₃ \ s₁ ∪ s₁) := by rw [diff_union_of_subset (h12.trans h23)]
      _ ≤ μ (s₃ \ s₁) + μ s₁ := measure_union_le _ _
      _ = μ s₁ := by simp only [h_nulldiff, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) sᶜ =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : (μ : (a : Set α) → ℝ≥0∞) sᶜ =
  HSub.hSub (β := ℝ≥0∞)
    (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞))
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← measure_add_measure_compl₀ h, ENNReal.add_sub_cancel_left hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  (μ : (a : Set α) → ℝ≥0∞) sᶜ =
    HSub.hSub (β := ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) sᶜ =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞)
Tactic: rw [← measure_add_measure_compl₀ h, ENNReal.add_sub_cancel_left hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← diff_compl, measure_diff_null']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ tᶜ) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← diff_compl, measure_diff_null ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
ht : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ tᶜ) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← diff_compl, measure_diff_null ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ s ∪ t =ᶠ[ae μ] s ↔ t ≤ᶠ[ae μ] s
have rw : s ∪ t =ᶠ[ae μ] s ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [ae_le_set]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ s ∪ t ≤ᶠ[ae μ] s
have rwa : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((s ∪ t) \ s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rwa [ae_le_set, union_diff_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ s ∪ t =ᶠ[ae μ] t ↔ s ≤ᶠ[ae μ] t
have rw : t ∪ s =ᶠ[ae μ] t ↔ s ≤ᶠ[ae μ] t
Tactic: rw [union_comm, union_ae_eq_left_iff_ae_subset]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
rw : t ∪ s =ᶠ[ae μ] t ↔ s ≤ᶠ[ae μ] t
⊢ s ∪ t =ᶠ[ae μ] t ↔ s ≤ᶠ[ae μ] t
have rw₁ : s ≤ᶠ[ae μ] t ↔ s ≤ᶠ[ae μ] t
Tactic: rw [union_comm, union_ae_eq_left_iff_ae_subset]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h₁ : s ≤ᶠ[ae μ] t
h₂ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
hsm : NullMeasurableSet s μ
ht : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ s =ᶠ[ae μ] t
have refine : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine eventuallyLE_antisymm_iff.mpr ⟨h₁, ae_le_set.mpr ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h₁ : s ≤ᶠ[ae μ] t
h₂ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
hsm : NullMeasurableSet s μ
ht : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (0 : ℝ≥0∞)
have h₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: replace h₂ : μ t = μ s := h₂.antisymm (measure_mono_ae h₁)
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h₁ : s ≤ᶠ[ae μ] t
hsm : NullMeasurableSet s μ
ht : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (0 : ℝ≥0∞)
have ht₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: replace ht : μ s ≠ ∞ := h₂ ▸ ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h₁ : s ≤ᶠ[ae μ] t
hsm : NullMeasurableSet s μ
h₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
ht : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∪ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) = 0
Tactic: rw [measure_diff' t hsm ht, measure_congr (union_ae_eq_left_iff_ae_subset.mpr h₁), h₂, tsub_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h₁ : s ≤ᶠ[ae μ] t
hsm : NullMeasurableSet s μ
h₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
ht : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∪ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) = 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₁ : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) = 0
Tactic: rw [measure_diff' t hsm ht, measure_congr (union_ae_eq_left_iff_ae_subset.mpr h₁), h₂, tsub_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h₁ : s ≤ᶠ[ae μ] t
hsm : NullMeasurableSet s μ
h₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
ht : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∪ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) = 0
rw₁ : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) = 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₂ : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) = 0
Tactic: rw [measure_diff' t hsm ht, measure_congr (union_ae_eq_left_iff_ae_subset.mpr h₁), h₂, tsub_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h₁ : s ≤ᶠ[ae μ] t
hsm : NullMeasurableSet s μ
h₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
ht : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∪ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) = 0
rw₁ : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) = 0
rw₂ : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) = 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₃ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [measure_diff' t hsm ht, measure_congr (union_ae_eq_left_iff_ae_subset.mpr h₁), h₂, tsub_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), t i) : ℝ≥0∞)
have refine : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞)
Tactic: refine le_antisymm (by gcongr; apply hsub) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), t i) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞)
have pos : ∀ (htop : ∃ (i : ι), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)),
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), t i) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞)
Tactic: by_cases! htop : ∃ i, μ (t i) = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
pos :
  ∀ (htop : ∃ (i : ι), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), t i) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), t i) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞)
have neg : ∀ (htop : ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)),
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), t i) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞)
Tactic: by_cases! htop : ∃ i, μ (t i) = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
htop : ∃ (i : ι), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), t i) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞)
have pos : ∀ (i : ι) (hi : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)),
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), t i) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), s i) : ℝ≥0∞)
Tactic: rcases htop with ⟨i, hi⟩
Cleared hypotheses: htop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
htop : ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)
M : (s : Set α) → Set α := toMeasurable μ
⊢ ∀ (b : ι), M (t b) ∩ M (⋃ (b : ι), s b) =ᶠ[ae μ] M (t b)
have refine_1 : ∀ (b : ι),
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (M (t b)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (M (t b) ∩ M (⋃ (b : ι), s b)) : ℝ≥0∞)
Tactic: refine fun b => ae_eq_of_subset_of_measure_ge inter_subset_left ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
htop : ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)
M : (s : Set α) → Set α := toMeasurable μ
refine_1 :
  ∀ (b : ι),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (M (t b)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (M (t b) ∩ M (⋃ (b : ι), s b)) : ℝ≥0∞)
⊢ ∀ (b : ι), M (t b) ∩ M (⋃ (b : ι), s b) =ᶠ[ae μ] M (t b)
have refine_2 : ∀ (b : ι), NullMeasurableSet (M (t b) ∩ M (⋃ (b : ι), s b)) μ
Tactic: refine fun b => ae_eq_of_subset_of_measure_ge inter_subset_left ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
htop : ∀ (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞) (∞ : ℝ≥0∞)
M : (s : Set α) → Set α := toMeasurable μ
refine_1 :
  ∀ (b : ι),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (M (t b)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (M (t b) ∩ M (⋃ (b : ι), s b)) : ℝ≥0∞)
refine_2 : ∀ (b : ι), NullMeasurableSet (M (t b) ∩ M (⋃ (b : ι), s b)) μ
⊢ ∀ (b : ι), M (t b) ∩ M (⋃ (b : ι), s b) =ᶠ[ae μ] M (t b)
have refine_3 : ∀ (b : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (M (t b)) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine fun b => ae_eq_of_subset_of_measure_ge inter_subset_left ?_ ?_ ?_