awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : s₂ ⊆ s₁
h₂ : MeasurableSet s₂
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real (s₁ \ s₂) = μ.real s₁ - μ.real s₂
have rw : μ.real (s₁ ∪ s₂) - μ.real s₂ = μ.real s₁ - μ.real s₂
Tactic: rw [measureReal_diff' h₂ h₁ (measure_ne_top_of_subset h h₁), union_eq_self_of_subset_right h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : s₂ ⊆ s₁
h₂ : MeasurableSet s₂
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : μ.real (s₁ ∪ s₂) - μ.real s₂ = μ.real s₁ - μ.real s₂
⊢ μ.real (s₁ \ s₂) = μ.real s₁ - μ.real s₂
have rw₁ : μ.real s₁ - μ.real s₂ = μ.real s₁ - μ.real s₂
Tactic: rw [measureReal_diff' h₂ h₁ (measure_ne_top_of_subset h h₁), union_eq_self_of_subset_right h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real s₁ - μ.real s₂ ≤ μ.real (s₁ \ s₂)
have simp : μ.real s₁ ≤ μ.real s₂ + μ.real (s₁ \ s₂)
Tactic: simp only [tsub_le_iff_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
hst : s ⊆ t
ε : ℝ
h : μ.real t < μ.real s + ε
ht' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real (t \ s) < ε
have rw : μ.real t - μ.real s < ε
Tactic: rw [measureReal_diff hst hs ht']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
hst : s ⊆ t
ε : ℝ
h : μ.real t < μ.real s + ε
ht' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real t - μ.real s < ε
have linarith : ε ≤ μ.real t - μ.real s → μ.real t - (μ.real s + ε) + (ε - (μ.real t - μ.real s)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
hst : s ⊆ t
ε : ℝ
ht' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real (t \ s) ≤ ε ↔ μ.real t ≤ μ.real s + ε
have rw : μ.real t - μ.real s ≤ ε ↔ μ.real t ≤ μ.real s + ε
Tactic: rw [measureReal_diff hst hs ht', tsub_le_iff_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
hst : s ⊆ t
ε : ℝ
ht' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : μ.real t - μ.real s ≤ ε ↔ μ.real t ≤ μ.real s + ε
⊢ μ.real (t \ s) ≤ ε ↔ μ.real t ≤ μ.real s + ε
have rw₁ : μ.real t ≤ μ.real s + ε ↔ μ.real t ≤ μ.real s + ε
Tactic: rw [measureReal_diff hst hs ht', tsub_le_iff_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (hypothesis)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
hst : s ⊆ t
h_nulldiff : μ.real (t \ s) = 0
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real s = μ.real t
have h_nulldiff₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [measureReal_eq_zero_iff h] at h_nulldiff
Cleared hypotheses: h_nulldiff, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (hypothesis)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nulldiff : μ.real (s₃ \ s₁) = 0
h' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₃ \ s₁) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real s₁ = μ.real s₂ ∧ μ.real s₂ = μ.real s₃
have A : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) ∧
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₃ : ℝ≥0∞)
Tactic: have A : μ s₁ = μ s₂ ∧ μ s₂ = μ s₃ :=
    measure_eq_measure_of_between_null_diff h12 h23 ((measureReal_eq_zero_iff h').1 h_nulldiff)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsFiniteMeasure μ
h₁ : MeasurableSet s
⊢ μ.real sᶜ = μ.real univ - μ.real s
have rw : μ.real (univ \ s) = μ.real univ - μ.real s
Tactic: rw [compl_eq_univ_diff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsFiniteMeasure μ
h₁ : NullMeasurableSet s μ
⊢ μ.real sᶜ = μ.real univ - μ.real s
have linarith : μ.real sᶜ < μ.real univ - μ.real s → μ.real sᶜ - (μ.real univ - μ.real s) + -(μ.real s + μ.real sᶜ - μ.real univ) = 0
Tactic: linarith [measureReal_add_measureReal_compl₀ h₁]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsFiniteMeasure μ
h₁ : NullMeasurableSet s μ
linarith :
  μ.real sᶜ < μ.real univ - μ.real s → μ.real sᶜ - (μ.real univ - μ.real s) + -(μ.real s + μ.real sᶜ - μ.real univ) = 0
⊢ μ.real sᶜ = μ.real univ - μ.real s
have linarith₁ : μ.real univ - μ.real s < μ.real sᶜ → μ.real univ - μ.real s - μ.real sᶜ + (μ.real s + μ.real sᶜ - μ.real univ) = 0
Tactic: linarith [measureReal_add_measureReal_compl₀ h₁]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ.real s₂ ≤ μ.real s₁
ht : t₁ ⊆ t₂
htμ : μ.real t₂ ≤ μ.real t₁
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
h₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s₁ ∪ t₁)) = ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s₂ ∪ t₂))
have rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t₂ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t₁ : ℝ≥0∞)
Tactic: rw [measure_union_congr_of_subset hs _ ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ.real s₂ ≤ μ.real s₁
ht : t₁ ⊆ t₂
htμ : μ.real t₂ ≤ μ.real t₁
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
h₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t₂ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t₁ : ℝ≥0∞)
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s₁ ∪ t₁)) = ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s₂ ∪ t₂))
have rw₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞)
Tactic: rw [measure_union_congr_of_subset hs _ ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
ι : Type u_3
x : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (↑s : Set ι).PairwiseDisjoint t
⊢ ∑ x_1 ∈ s, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t x_1)) ≤ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ)
have rw : ENNReal.toReal (∑ a ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t a)) ≤ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ)
Tactic: rw [← ENNReal.toReal_sum (by finiteness)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
ι : Type u_3
x : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (↑s : Set ι).PairwiseDisjoint t
⊢ ENNReal.toReal (∑ a ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t a)) ≤ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ)
have apply : LE.le (α := ℝ≥0∞) (∑ a ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: apply ENNReal.toReal_mono (by finiteness)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
ι : Type u_3
x : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : μ.real univ < ∑ i ∈ s, μ.real (t i)
⊢ ∃ i ∈ s, ∃ j ∈ s, ∃ (_ : i ≠ j), (t i ∩ t j).Nonempty
have apply : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∑ i ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞)
Tactic: apply exists_nonempty_inter_of_measure_univ_lt_sum_measure μ
    (fun i mi ↦ (h i mi).nullMeasurableSet)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
x : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : μ.real univ < ∑ i ∈ s, μ.real (t i)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∑ i ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞)
have H₁ : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) < ∑ x_1 ∈ s, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t x_1))
Tactic: simp only [Measure.real] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
ι : Type u_3
x : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) < ∑ x_1 ∈ s, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t x_1))
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∑ i ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞)
have apply : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) < ENNReal.toReal (∑ i ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t i))
Tactic: apply (ENNReal.toReal_lt_toReal (by finiteness) _).1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
ι : Type u_3
x : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) < ∑ x_1 ∈ s, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t x_1))
apply : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) < ENNReal.toReal (∑ i ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t i))
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∑ i ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞)
have apply₁ : Ne (α := ℝ≥0∞) (∑ i ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t i)) ∞
Tactic: apply (ENNReal.toReal_lt_toReal (by finiteness) _).1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
ι : Type u_3
x : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) < ∑ x_1 ∈ s, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t x_1))
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) < ENNReal.toReal (∑ i ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t i))
have h₁ : ENNReal.toReal (∑ i ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t i)) = ∑ x_1 ∈ s, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t x_1))
Tactic: convert! H
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
ι : Type u_3
x : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) < ∑ x_1 ∈ s, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t x_1))
⊢ ENNReal.toReal (∑ i ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t i)) =
    ∑ x_1 ∈ s, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t x_1))
have h₁ : Eq (α := ℝ) (∑ a ∈ s, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t a)))
  (∑ x_1 ∈ s, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t x_1)))
Tactic: rw [ENNReal.toReal_sum (by finiteness)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real s + μ.real t
hu : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (s ∩ t).Nonempty
have apply : (μ : (a : Set α) → ℝ≥0∞) u <
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: apply nonempty_inter_of_measure_lt_add μ ht h's h't ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real s + μ.real t
hu : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) u <
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have apply : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) u) <
  (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)).toReal
Tactic: apply (ENNReal.toReal_lt_toReal hu _).1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real s + μ.real t
hu : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
apply :
  ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) u) <
    (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)).toReal
⊢ (μ : (a : Set α) → ℝ≥0∞) u <
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have apply₁ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≠ ∞
Tactic: apply (ENNReal.toReal_lt_toReal hu _).1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real s + μ.real t
hu : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) u) <
    (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)).toReal
have rw : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) u) <
  ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t)
Tactic: rw [ENNReal.toReal_add (measure_ne_top_of_subset h's hu) (measure_ne_top_of_subset h't hu)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (hypothesis)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real s + μ.real t
hu : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (s ∩ t).Nonempty
have h₁ : μ.real u < μ.real t + μ.real s
Tactic: rw [add_comm] at h
Cleared hypotheses: h, hu
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real t + μ.real s
hu : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (s ∩ t).Nonempty
have rw : (t ∩ s).Nonempty
Tactic: rw [inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsProbabilityMeasure μ
h : NullMeasurableSet s μ
⊢ μ.real sᶜ = 1 - μ.real s
have rw : μ.real univ - μ.real s = 1 - μ.real s
Tactic: rw [measureReal_compl₀ h, probReal_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsProbabilityMeasure μ
h : NullMeasurableSet s μ
rw : μ.real univ - μ.real s = 1 - μ.real s
⊢ μ.real sᶜ = 1 - μ.real s
have rw₁ : 1 - μ.real s = 1 - μ.real s
Tactic: rw [measureReal_compl₀ h, probReal_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
H : μ.InnerRegularWRT p q
hU : q U
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
    (⨆ (K : Set α), ⨆ (_ : K ⊆ U), ⨆ (_ : p K), (μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)
have le_antisymm : ∀ (r : ℝ≥0∞) (hr : r < (μ : (a : Set α) → ℝ≥0∞) U),
  r < ⨆ (K : Set α), ⨆ (_ : K ⊆ U), ⨆ (_ : p K), (μ : (a : Set α) → ℝ≥0∞) K
Tactic: refine
    le_antisymm (le_of_forall_lt fun r hr => ?_) (iSup₂_le fun K hK => iSup_le fun _ => μ.mono hK)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
ν : Measure α
hμ : μ.InnerRegularWRT p q
hν : ν.InnerRegularWRT p q
hμν : ∀ (U : Set α), p U → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
U : Set α
hU : q U
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (⨆ (K : Set α), ⨆ (_ : K ⊆ U), ⨆ (_ : p K), (μ : (a : Set α) → ℝ≥0∞) K)
  (⨆ (K : Set α), ⨆ (_ : K ⊆ U), ⨆ (_ : p K), (ν : (a : Set α) → ℝ≥0∞) K)
Tactic: rw [hμ.measure_eq_iSup hU, hν.measure_eq_iSup hU]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
ν : Measure α
hμ : μ.InnerRegularWRT p q
hν : ν.InnerRegularWRT p q
hμν : ∀ (U : Set α), p U → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
U : Set α
hU : q U
⊢ Eq (α := ℝ≥0∞) (⨆ (K : Set α), ⨆ (_ : K ⊆ U), ⨆ (_ : p K), (μ : (a : Set α) → ℝ≥0∞) K)
    (⨆ (K : Set α), ⨆ (_ : K ⊆ U), ⨆ (_ : p K), (ν : (a : Set α) → ℝ≥0∞) K)
have h : ∀ t ⊆ U, ∀ (ht2 : p t), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: congr! 4 with t _ ht2
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hε : ε ≠ 0
⊢ ∃ K ⊆ U, p K ∧ (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε
have inl : ∀ (h₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)),
  ∃ K ⊆ U, p K ∧ (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε
Tactic: rcases eq_or_ne (μ U) 0 with h₀ | h₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hε : ε ≠ 0
inl :
  ∀ (h₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)),
    ∃ K ⊆ U, p K ∧ (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε
⊢ ∃ K ⊆ U, p K ∧ (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε
have inr : ∀ (h₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)),
  ∃ K ⊆ U, p K ∧ (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε
Tactic: rcases eq_or_ne (μ U) 0 with h₀ | h₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hε : ε ≠ 0
h₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ K ⊆ U, p K ∧ (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε
have inl : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) ε
Tactic: refine ⟨∅, empty_subset _, h0, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hε : ε ≠ 0
h₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) ε
have inl : (μ : (a : Set α) → ℝ≥0∞) U < 0 + ε
Tactic: rwa [measure_empty, h₀, zero_add, pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hε : ε ≠ 0
h₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
inl : (μ : (a : Set α) → ℝ≥0∞) U < 0 + ε
⊢ (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) ε
have inl₁ : 0 < 0 + ε
Tactic: rwa [measure_empty, h₀, zero_add, pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hε : ε ≠ 0
h₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
inl : (μ : (a : Set α) → ℝ≥0∞) U < 0 + ε
inl₁ : 0 < 0 + ε
⊢ (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) ε
have inl₂ : 0 < ε
Tactic: rwa [measure_empty, h₀, zero_add, pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hε : ε ≠ 0
h₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ K ⊆ U, p K ∧ (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε
have inr : ∀ (K : Set α) (hKU : K ⊆ U) (hKc : p K)
  (hrK : HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ε < (μ : (a : Set α) → ℝ≥0∞) K),
  ∃ K ⊆ U, p K ∧ (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε
Tactic: rcases H hU _ (ENNReal.sub_lt_self hμU h₀ hε) with ⟨K, hKU, hKc, hrK⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α → β
hf : AEMeasurable f μ
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (f '' K)
hB₂ : ∀ (U : Set β), qb U → MeasurableSet U
U : Set β
hU : qb U
r : ℝ≥0∞
hr : r < ((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) U
⊢ ∃ K ⊆ U, pb K ∧ r < ((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) K
have hr₁ : r < (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' U)
Tactic: rw [map_apply_of_aemeasurable hf (hB₂ _ hU)] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α → β
hf : AEMeasurable f μ
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (f '' K)
hB₂ : ∀ (U : Set β), qb U → MeasurableSet U
U : Set β
hU : qb U
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' U)
⊢ ∃ K ⊆ U, pb K ∧ r < ((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) K
have rcases : ∀ (K : Set α) (hKU : K ⊆ f ⁻¹' U) (hKc : pa K) (hK : r < (μ : (a : Set α) → ℝ≥0∞) K),
  ∃ K ⊆ U, pb K ∧ r < ((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) K
Tactic: rcases H (hAB U hU) r hr with ⟨K, hKU, hKc, hK⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
pa qa : Set α → Prop
H : μ.InnerRegularWRT pa qa
f : α → β
hf : AEMeasurable f μ
pb qb : Set β → Prop
hAB : ∀ (U : Set β), qb U → qa (f ⁻¹' U)
hAB' : ∀ (K : Set α), pa K → pb (f '' K)
hB₂ : ∀ (U : Set β), qb U → MeasurableSet U
U : Set β
hU : qb U
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' U)
K : Set α
hKU : K ⊆ f ⁻¹' U
hKc : pa K
hK : r < (μ : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ U, pb K ∧ r < ((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) K
have refine : r < ((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) (f '' K)
Tactic: refine ⟨f '' K, image_subset_iff.2 hKU, hAB' _ hKc, ?_⟩