awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : IsFiniteMeasure (m0 := ⊥) (μ.trim ⋯)
h_univ : LT.lt (α := ℝ≥0∞) (((μ.trim ⋯ : Measure α) : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine_1 : ∀ (h_univ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)),
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rwa [trim_measurableSet_eq bot_le MeasurableSet.univ] at h_univ
Cleared hypotheses: h_univ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
hm : m ≤ m0
⊢ μ.trim hm ≪ ν.trim hm
have refine : ∀ (s : Set α) (hs : MeasurableSet s) (hsν : Eq (α := ℝ≥0∞) ((ν.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine Measure.AbsolutelyContinuous.mk (fun s hs hsν ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
hm : m ≤ m0
s : Set α
hs : MeasurableSet s
hsν : Eq (α := ℝ≥0∞) ((ν.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : ∀ (hsν : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [trim_measurableSet_eq hm hs] at hsν ⊢
Cleared hypotheses: hsν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Trim (goal)
Goal:
α : Type u_3
β : Type u_4
m m0 : MeasurableSpace α
μ : Measure α
inst : MeasurableSpace β
inst_1 : MeasurableEq β
hm : m ≤ m0
f g : α → β
hf : Measurable f
hg : Measurable g
hfg : f =ᶠ[ae μ] g
⊢ f =ᶠ[ae (μ.trim hm)] g
have rwa : MeasurableSet.{u_3} (α := α) {a : α | ¬f a = g a}
Tactic: rwa [Filter.EventuallyEq, ae_iff, trim_measurableSet_eq hm _]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : (μ : (a : Set α) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε
⊢ (μ : (a : Set α) → ℝ≥0∞) tᶜ ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) ε
have rw : (μ : (a : Set α) → ℝ≥0∞) univ ≤
  HAdd.hAdd (β := ℝ≥0∞)
    (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) + ε)
    ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [measure_compl ht (by finiteness), measure_compl hs (by finiteness), tsub_le_iff_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : (μ : (a : Set α) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε
⊢ HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) +
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε =
    HAdd.hAdd (β := ℝ≥0∞)
      (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) + ε)
      ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) +
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε =
  HAdd.hAdd (β := ℝ≥0∞)
      (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) +
    ε
Tactic: rw [add_right_comm, add_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : (μ : (a : Set α) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε
rw :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) +
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε =
    HAdd.hAdd (β := ℝ≥0∞)
        (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
        ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) +
      ε
⊢ HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) +
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε =
    HAdd.hAdd (β := ℝ≥0∞)
      (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) + ε)
      ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have rw₁ : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) +
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε =
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) +
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε
Tactic: rw [add_right_comm, add_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : (μ : (a : Set α) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε
⊢ (μ : (a : Set α) → ℝ≥0∞) univ ≤
    HAdd.hAdd (β := ℝ≥0∞)
      (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) + ε)
      ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have μ₁ : HAdd.hAdd (β := ℝ≥0∞)
    (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) +
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε
Tactic: calc
    μ univ = μ univ - μ s + μ s := (tsub_add_cancel_of_le <| measure_mono s.subset_univ).symm
    _ ≤ μ univ - μ s + (μ t + ε) := by gcongr
    _ = _ := by rw [add_right_comm, add_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : (μ : (a : Set α) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε
μ₁ :
  HAdd.hAdd (β := ℝ≥0∞)
      (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) +
      HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε
⊢ (μ : (a : Set α) → ℝ≥0∞) univ ≤
    HAdd.hAdd (β := ℝ≥0∞)
      (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) + ε)
      ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have μ₂ : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) +
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ε =
  HAdd.hAdd (β := ℝ≥0∞)
    (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) + ε)
    ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: calc
    μ univ = μ univ - μ s + μ s := (tsub_add_cancel_of_le <| measure_mono s.subset_univ).symm
    _ ≤ μ univ - μ s + (μ t + ε) := by gcongr
    _ = _ := by rw [add_right_comm, add_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ ν ν₁ ν₂ : Measure α
s t : Set α
inst : IsEmpty α
⊢ IsFiniteMeasure μ
have rw : IsFiniteMeasure.{u_1} (α := α) (m0 := m0) 0
Tactic: rw [eq_zero_of_isEmpty μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ ν ν₁ ν₂ : Measure α
s t : Set α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
⊢ LT.lt (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
  LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [Measure.coe_add, Pi.add_apply, ENNReal.add_lt_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ ν ν₁ ν₂ : Measure α
s t : Set α
⊢ LT.lt (α := ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) < ∞
Tactic: rw [smul_apply, smul_eq_mul, ← ENNReal.div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ ν ν₁ ν₂ : Measure α
s t : Set α
R : Type u_5
inst : SMul R ℝ≥0
inst_1 : SMul R ℝ≥0∞
inst_2 : IsScalarTower R ℝ≥0 ℝ≥0∞
inst_3 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_4 : IsFiniteMeasure μ
r : R
⊢ IsFiniteMeasure (r • μ)
have rw : IsFiniteMeasure (HSMul.hSMul (β := ℝ≥0) r 1 • μ)
Tactic: rw [← smul_one_smul ℝ≥0 r μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
f : α → β
⊢ IsFiniteMeasure (m0 := mβ) (map f μ)
have pos : ∀ (hf : AEMeasurable f μ), IsFiniteMeasure (m0 := mβ) (map f μ)
Tactic: by_cases hf : AEMeasurable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
f : α → β
pos : ∀ (hf : AEMeasurable f μ), IsFiniteMeasure (m0 := mβ) (map f μ)
⊢ IsFiniteMeasure (m0 := mβ) (map f μ)
have neg : ∀ (hf : ¬AEMeasurable f μ), IsFiniteMeasure (m0 := mβ) (map f μ)
Tactic: by_cases hf : AEMeasurable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
f : α → β
hf : AEMeasurable f μ
⊢ IsFiniteMeasure (m0 := mβ) (map f μ)
have pos : LT.lt (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
f : α → β
hf : AEMeasurable f μ
⊢ LT.lt (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have pos : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' univ) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [map_apply_of_aemeasurable hf MeasurableSet.univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
mβ : MeasurableSpace β
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
f : α → β
hf : ¬AEMeasurable f μ
⊢ IsFiniteMeasure (m0 := mβ) (map f μ)
have neg : IsFiniteMeasure.{u_2} (α := β) (m0 := mβ) 0
Tactic: rw [map_of_not_aemeasurable hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
inst : IsFiniteMeasure (m0 := mβ) (map f μ)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : LT.lt (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← Set.preimage_univ (f := f), ← map_apply_of_aemeasurable hf .univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
⊢ measureUnivNNReal μ = 0 ↔ μ = 0
have rw : measureUnivNNReal μ = 0 ↔ (↑(measureUnivNNReal μ) : ℝ≥0∞) = 0
Tactic: rw [← MeasureTheory.Measure.measure_univ_eq_zero, ← coe_measureUnivNNReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
⊢ measureUnivNNReal μ = 0 ↔ (↑(measureUnivNNReal μ) : ℝ≥0∞) = 0
have norm_cast : measureUnivNNReal μ = 0 ↔ measureUnivNNReal μ = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
⊢ 0 < measureUnivNNReal μ
have contrapose! : ∀ (hμ : measureUnivNNReal μ ≤ 0), μ = 0
Tactic: contrapose! hμ
Cleared hypotheses: hμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
hμν : μ ≤ ν
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ μ = ν
have refine : ∀ (s : Set α) (hs : MeasurableSet s),
  s.Nonempty → LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: refine le_antisymm hμν (le_intro fun s hs _ ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
hμν : μ ≤ ν
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h : s.Nonempty
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have by_contra! : ∀ (h_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)), False
Tactic: by_contra! h_lt
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
hμν : μ ≤ ν
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h : s.Nonempty
h_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ False
have h_disj : Disjoint s sᶜ
Tactic: have h_disj : Disjoint s sᶜ := disjoint_compl_right_iff_subset.mpr subset_rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
hμν : μ ≤ ν
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h : s.Nonempty
h_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h_disj : Disjoint s sᶜ
⊢ False
have h_univ₁ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞)
Tactic: rw [← union_compl_self s, measure_union h_disj hs.compl, measure_union h_disj hs.compl] at h_univ
Cleared hypotheses: h_univ, hs, h, h_lt, h_disj
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ Summable (α := ℝ) fun (x : ℕ) ↦ μ.real (f x)
have hsum : Ne (α := ℝ≥0∞) (∑' (x : ℕ), (μ : (a : Set α) → ℝ≥0∞) (f x)) ∞
Tactic: apply ENNReal.summable_toReal
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ Ne (α := ℝ≥0∞) (∑' (x : ℕ), (μ : (a : Set α) → ℝ≥0∞) (f x)) ∞
have hsum : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← MeasureTheory.measure_iUnion hf₂ hf₁]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
p : α → Prop
hp : NullMeasurableSet {a : α | p a} μ
⊢ (∀ᵐ (a : α) ∂μ, p a) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | p a} : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have rw : (∀ᵐ (a : α) ∂μ, p a) ↔ {a : α | p a} =ᶠ[ae μ] univ
Tactic: rw [← ae_eq_univ_iff_measure_eq hp, eventuallyEq_univ, eventually_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
p : α → Prop
hp : NullMeasurableSet {a : α | p a} μ
rw : (∀ᵐ (a : α) ∂μ, p a) ↔ {a : α | p a} =ᶠ[ae μ] univ
⊢ (∀ᵐ (a : α) ∂μ, p a) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | p a} : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have rw₁ : (∀ᵐ (a : α) ∂μ, p a) ↔ {a : α | p a} ∈ ae μ
Tactic: rw [← ae_eq_univ_iff_measure_eq hp, eventuallyEq_univ, eventually_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
p : α → Prop
hp : NullMeasurableSet {a : α | p a} μ
rw : (∀ᵐ (a : α) ∂μ, p a) ↔ {a : α | p a} =ᶠ[ae μ] univ
rw₁ : (∀ᵐ (a : α) ∂μ, p a) ↔ {a : α | p a} ∈ ae μ
⊢ (∀ᵐ (a : α) ∂μ, p a) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | p a} : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have rw₂ : {x : α | p x} ∈ ae μ ↔ {a : α | p a} ∈ ae μ
Tactic: rw [← ae_eq_univ_iff_measure_eq hp, eventuallyEq_univ, eventually_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (hypothesis)
Goal:
X : Type u_5
inst : MeasurableSpace X
μ : Measure X
inst_1 : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
⊢ Tendsto (α := ℕ) (β := ℝ≥0∞)
    (comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i) atTop (𝓝 0)
have decr : Antitone.{0, u_5} (β := Set X) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i
Tactic: have decr : Antitone fun n ↦ ⋃ i ≥ n, Es i :=
    fun n m hnm ↦ biUnion_mono (fun _ hi ↦ le_trans hnm hi) (fun _ _ ↦ subset_rfl)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
X : Type u_5
inst : MeasurableSpace X
μ : Measure X
inst_1 : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
decr : Antitone.{0, u_5} (β := Set X) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i
⊢ Eq.{u_5 + 1} (α := Set X) (⋂ (n : ℕ), ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i) ∅
have apply : Subset.{u_5} (α := Set X) (⋂ (n : ℕ), ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i) ∅
Tactic: apply subset_antisymm _ (empty_subset _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (hypothesis)
Goal:
X : Type u_5
inst : MeasurableSpace X
μ : Measure X
inst_1 : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
decr : Antitone.{0, u_5} (β := Set X) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i
x : X
hx : Membership.mem (γ := Set X) (⋂ (n : ℕ), ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i) x
⊢ Membership.mem (γ := Set X) ∅ x
have hx₁ : ∀ (i : ℕ), ∃ i_1 ≥ i, x ∈ Es i_1
Tactic: simp only [mem_iInter, mem_iUnion, exists_prop] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
X : Type u_5
inst : MeasurableSpace X
μ : Measure X
inst_1 : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
decr : Antitone.{0, u_5} (β := Set X) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i
x : X
hx : ∀ (i : ℕ), ∃ i_1 ≥ i, x ∈ Es i_1
⊢ Membership.mem (γ := Set X) ∅ x
have obtain : ∀ j ≥ 0, ∀ (x_in_Es_j : x ∈ Es j), Membership.mem (γ := Set X) ∅ x
Tactic: obtain ⟨j, _, x_in_Es_j⟩ := hx 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
X : Type u_5
inst : MeasurableSpace X
μ : Measure X
inst_1 : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
decr : Antitone.{0, u_5} (β := Set X) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i
x : X
hx : ∀ (i : ℕ), ∃ i_1 ≥ i, x ∈ Es i_1
j : ℕ
left : j ≥ 0
x_in_Es_j : x ∈ Es j
⊢ Membership.mem (γ := Set X) ∅ x
have obtain : ∀ (k : ℕ) (k_gt_j : k ≥ j + 1) (x_in_Es_k : x ∈ Es k), Membership.mem (γ := Set X) ∅ x
Tactic: obtain ⟨k, k_gt_j, x_in_Es_k⟩ := hx (j + 1)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (hypothesis)
Goal:
X : Type u_5
inst : MeasurableSpace X
μ : Measure X
inst_1 : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
decr : Antitone.{0, u_5} (β := Set X) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i
x : X
hx : ∀ (i : ℕ), ∃ i_1 ≥ i, x ∈ Es i_1
j : ℕ
left : j ≥ 0
x_in_Es_j : x ∈ Es j
k : ℕ
k_gt_j : k ≥ j + 1
x_in_Es_k : x ∈ Es k
⊢ Membership.mem (γ := Set X) ∅ x
have oops : x ≠ x
Tactic: have oops := (Es_disj (Nat.ne_of_lt k_gt_j)).ne_of_mem x_in_Es_j x_in_Es_k
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (hypothesis)
Goal:
X : Type u_5
inst : MeasurableSpace X
μ : Measure X
inst_1 : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
decr : Antitone.{0, u_5} (β := Set X) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i
⊢ Tendsto (α := ℕ) (β := ℝ≥0∞)
    (comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i) atTop (𝓝 0)
have nothing : Eq.{u_5 + 1} (α := Set X) (⋂ (n : ℕ), ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i) ∅
Tactic: have nothing : ⋂ n, ⋃ i ≥ n, Es i = ∅ := by
    apply subset_antisymm _ (empty_subset _)
    intro x hx
    simp only [mem_iInter, mem_iUnion, exists_prop] at hx
    obtain ⟨j, _, x_in_Es_j⟩ := hx 0
    obtain ⟨k, k_gt_j, x_in_Es_k⟩ := hx (j + 1)
    have oops := (Es_disj (Nat.ne_of_lt k_gt_j)).ne_of_mem x_in_Es_j x_in_Es_k
    contradiction
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (hypothesis)
Goal:
X : Type u_5
inst : MeasurableSpace X
μ : Measure X
inst_1 : IsFiniteMeasure μ
Es : ℕ → Set X
Es_mble : ∀ (i : ℕ), NullMeasurableSet (Es i) μ
Es_disj : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
decr : Antitone.{0, u_5} (β := Set X) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i
nothing : Eq.{u_5 + 1} (α := Set X) (⋂ (n : ℕ), ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i) ∅
⊢ Tendsto (α := ℕ) (β := ℝ≥0∞)
    (comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i) atTop (𝓝 0)
have key : Tendsto (α := ℕ) (β := ℝ≥0∞)
  (comp (β := Set X) (⇑μ : (a : Set X) → ℝ≥0∞) fun (n : ℕ) ↦ ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i : ℕ → ℝ≥0∞) atTop
  (𝓝 ((μ : (a : Set X) → ℝ≥0∞) (⋂ (n : ℕ), ⋃ (i : ℕ), ⋃ (_ : i ≥ n), Es i)) : Filter ℝ≥0∞)
Tactic: have key := tendsto_measure_iInter_atTop (μ := μ) (fun n ↦ by measurability)
    decr ⟨0, measure_ne_top _ _⟩