awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᶠ[ae μ] g
hg : AEMeasurable g μ
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ
⊢ ∫⁻ (x : α), φ x ∂μ + HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x + ε ≤ g x} : ℝ≥0∞) ≤
    ∫⁻ (x : α), φ x ∂μ + HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | φ x + ε ≤ g x} : ℝ≥0∞)
have bc : ∀ (a : α), φ a ≤ f a
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᶠ[ae μ] g
hg : AEMeasurable g μ
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ
⊢ ∫⁻ (x : α), φ x ∂μ + HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | φ x + ε ≤ g x} : ℝ≥0∞) =
    ∫⁻ (x : α), φ x + indicator {x : α | φ x + ε ≤ g x} (fun (x : α) ↦ ε) x ∂μ
have hs : NullMeasurableSet {x : α | φ x + ε ≤ g x} μ
Tactic: rw [lintegral_add_left hφm, lintegral_indicator₀, setLIntegral_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᶠ[ae μ] g
hg : AEMeasurable g μ
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ
⊢ ∫⁻ (a : α), f a ∂μ + HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x + ε ≤ g x} : ℝ≥0∞) ≤
    ∫⁻ (a : α), g a ∂μ
have f₁ : ∀ (x : α) (hx₁ : f x ≤ g x), φ x + indicator {x : α | φ x + ε ≤ g x} (fun (x : α) ↦ ε) x ≤ g x
Tactic: calc
    ∫⁻ x, f x ∂μ + ε * μ { x | f x + ε ≤ g x } = ∫⁻ x, φ x ∂μ + ε * μ { x | f x + ε ≤ g x } := by
      rw [hφ_eq]
    _ ≤ ∫⁻ x, φ x ∂μ + ε * μ { x | φ x + ε ≤ g x } := by
      gcongr
      exact hφ_le _
    _ = ∫⁻ x, φ x + indicator { x | φ x + ε ≤ g x } (fun _ => ε) x ∂μ := by
      rw [lintegral_add_left hφm, lintegral_indicator₀, setLIntegral_const]
      exact measurableSet_le (hφm.nullMeasurable.measurable'.add_const _) hg.nullMeasurable
    _ ≤ ∫⁻ x, g x ∂μ := lintegral_mono_ae (hle.mono fun x hx₁ => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᶠ[ae μ] g
hg : AEMeasurable g μ
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ
x : α
hx₁ : f x ≤ g x
⊢ φ x + indicator {x : α | φ x + ε ≤ g x} (fun (x : α) ↦ ε) x ≤ g x
have simp : (φ x + if Membership.mem (γ := Set α) {x : α | φ x + ε ≤ g x} x then ε else 0) ≤ g x
Tactic: simp only [indicator_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᶠ[ae μ] g
hg : AEMeasurable g μ
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ
x : α
hx₁ : f x ≤ g x
⊢ (φ x + if Membership.mem (γ := Set α) {x : α | φ x + ε ≤ g x} x then ε else 0) ≤ g x
have pos : ∀ (hx₂ : Membership.mem (γ := Set α) {x : α | φ x + ε ≤ g x} x), φ x + ε ≤ g x
Tactic: split_ifs with hx₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hle : f ≤ᶠ[ae μ] g
hg : AEMeasurable g μ
ε : ℝ≥0∞
φ : α → ℝ≥0∞
hφm : Measurable φ
hφ_le : φ ≤ f
hφ_eq : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), φ a ∂μ
x : α
hx₁ : f x ≤ g x
pos : ∀ (hx₂ : Membership.mem (γ := Set α) {x : α | φ x + ε ≤ g x} x), φ x + ε ≤ g x
⊢ (φ x + if Membership.mem (γ := Set α) {x : α | φ x + ε ≤ g x} x then ε else 0) ≤ g x
have neg : ∀ (hx₂ : x ∉ {x : α | φ x + ε ≤ g x}), φ x + 0 ≤ g x
Tactic: split_ifs with hx₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
s : Set α
hs : ∀ x ∈ s, 1 ≤ f x
⊢ (μ : (a : Set α) → ℝ≥0∞) s ≤ ∫⁻ (a : α), f a ∂μ
have apply : (μ : (a : Set α) → ℝ≥0∞) s ≤
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | 1 ≤ f x} : ℝ≥0∞)
Tactic: apply le_trans _ (mul_meas_ge_le_lintegral₀ hf 1)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
s : Set α
hs : ∀ x ∈ s, 1 ≤ f x
⊢ (μ : (a : Set α) → ℝ≥0∞) s ≤
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | 1 ≤ f x} : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | 1 ≤ f x} : ℝ≥0∞)
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hf : ∀ (a : α), f a ≤ 1
h'f : ∀ a ∈ sᶜ, f a = 0
⊢ ∫⁻ (a : α), f a ∂μ ≤ (μ : (a : Set α) → ℝ≥0∞) s
have apply : ∀ (x : α), f x ≤ s.indicator 1 x
Tactic: apply (lintegral_mono (fun x ↦ ?_)).trans (lintegral_indicator_one_le s)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hf : ∀ (a : α), f a ≤ 1
h'f : ∀ a ∈ sᶜ, f a = 0
x : α
⊢ f x ≤ s.indicator 1 x
have pos : ∀ (hx : x ∈ s), f x ≤ s.indicator 1 x
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hf : ∀ (a : α), f a ≤ 1
h'f : ∀ a ∈ sᶜ, f a = 0
x : α
pos : ∀ (hx : x ∈ s), f x ≤ s.indicator 1 x
⊢ f x ≤ s.indicator 1 x
have neg : ∀ (hx : x ∉ s), f x ≤ s.indicator 1 x
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ (μ : (a : Set α) → ℝ≥0∞) t
have rw : ∫⁻ (a : α), s.indicator f a ∂μ ≤ (μ : (a : Set α) → ℝ≥0∞) t
Tactic: rw [← lintegral_indicator hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
⊢ ∫⁻ (a : α), s.indicator f a ∂μ ≤ (μ : (a : Set α) → ℝ≥0∞) t
have refine : ∀ (a : α), s.indicator f a ≤ 1
Tactic: refine lintegral_le_meas (fun a ↦ ?_) (by simp_all)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
a : α
⊢ s.indicator f a ≤ 1
have pos : ∀ (has : a ∈ s), s.indicator f a ≤ 1
Tactic: by_cases has : a ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
a : α
pos : ∀ (has : a ∈ s), s.indicator f a ≤ 1
⊢ s.indicator f a ≤ 1
have neg : ∀ (has : a ∉ s), s.indicator f a ≤ 1
Tactic: by_cases has : a ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
a : α
has : a ∈ s
⊢ s.indicator f a ≤ 1
have pos : ∀ (hat : a ∈ t), s.indicator f a ≤ 1
Tactic: by_cases hat : a ∈ t
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
a : α
has : a ∈ s
pos : ∀ (hat : a ∈ t), s.indicator f a ≤ 1
⊢ s.indicator f a ≤ 1
have neg : ∀ (hat : a ∉ t), s.indicator f a ≤ 1
Tactic: by_cases hat : a ∈ t
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
a : α
⊢ s.indicator f a ≤ 1
have pos : ∀ (has : a ∈ s) (hat : a ∈ t), s.indicator f a ≤ 1
Tactic: by_cases has : a ∈ s <;> [by_cases hat : a ∈ t; skip]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
a : α
pos : ∀ (has : a ∈ s) (hat : a ∈ t), s.indicator f a ≤ 1
⊢ s.indicator f a ≤ 1
have neg : ∀ (has : a ∈ s) (hat : a ∉ t), s.indicator f a ≤ 1
Tactic: by_cases has : a ∈ s <;> [by_cases hat : a ∈ t; skip]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
a : α
pos : ∀ (has : a ∈ s) (hat : a ∈ t), s.indicator f a ≤ 1
neg : ∀ (has : a ∈ s) (hat : a ∉ t), s.indicator f a ≤ 1
⊢ s.indicator f a ≤ 1
have neg₁ : ∀ (has : a ∉ s), s.indicator f a ≤ 1
Tactic: by_cases has : a ∈ s <;> [by_cases hat : a ∈ t; skip]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f (μ.restrict s)
hμf : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ f x = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ f x = ∞} : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x = ∞} : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | f a = ∞} ∩ s) : ℝ≥0∞)
  ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x = ∞} : ℝ≥0∞)
Tactic: rw [← setOf_inter_eq_sep]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
hε' : ε ≠ ∞
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) ε ≤ ∫⁻ (a : α), f a ∂μ
have rw : HMul.hMul (β := ℝ≥0∞) ε ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ f x} : ℝ≥0∞) ≤ ∫⁻ (a : α), f a ∂μ
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hg : AEMeasurable g μ
hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
n : ℕ
⊢ ∀ᵐ (x : α) ∂μ, g x < f x + (↑n : ℝ≥0∞)⁻¹
have simp : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | f a + (↑n : ℝ≥0∞)⁻¹ ≤ g a} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [ae_iff, not_lt]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hg : AEMeasurable g μ
hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
n : ℕ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | f a + (↑n : ℝ≥0∞)⁻¹ ≤ g a} : ℝ≥0∞) (0 : ℝ≥0∞)
have this : ∫⁻ (x : α), f x ∂μ +
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞)⁻¹ : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x + (↑n : ℝ≥0∞)⁻¹ ≤ g x} : ℝ≥0∞) ≤
  ∫⁻ (x : α), f x ∂μ
Tactic: have : ∫⁻ x, f x ∂μ + (↑n)⁻¹ * μ { x : α | f x + (n : ℝ≥0∞)⁻¹ ≤ g x } ≤ ∫⁻ x, f x ∂μ :=
      (lintegral_add_mul_meas_add_le_le_lintegral hfg hg n⁻¹).trans hgf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hg : AEMeasurable g μ
hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
n : ℕ
this :
  ∫⁻ (x : α), f x ∂μ +
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑n : ℝ≥0∞)⁻¹ : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x + (↑n : ℝ≥0∞)⁻¹ ≤ g x} : ℝ≥0∞) ≤
    ∫⁻ (x : α), f x ∂μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | f a + (↑n : ℝ≥0∞)⁻¹ ≤ g a} : ℝ≥0∞) (0 : ℝ≥0∞)
have this₁ : Eq (α := ℝ≥0∞) (↑n : ℝ≥0∞)⁻¹ 0 ∨
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x + (↑n : ℝ≥0∞)⁻¹ ≤ g x} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [(ENNReal.cancel_of_ne hf).add_le_iff_nonpos_right, nonpos_iff_eq_zero, mul_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hg : AEMeasurable g μ
hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
⊢ f =ᶠ[ae μ] g
have this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, g x < f x + (↑n : ℝ≥0∞)⁻¹
Tactic: have : ∀ n : ℕ, ∀ᵐ x ∂μ, g x < f x + (n : ℝ≥0∞)⁻¹ := by
    intro n
    simp only [ae_iff, not_lt]
    have : ∫⁻ x, f x ∂μ + (↑n)⁻¹ * μ { x : α | f x + (n : ℝ≥0∞)⁻¹ ≤ g x } ≤ ∫⁻ x, f x ∂μ :=
      (lintegral_add_mul_meas_add_le_le_lintegral hfg hg n⁻¹).trans hgf
    rw [(ENNReal.cancel_of_ne hf).add_le_iff_nonpos_right, nonpos_iff_eq_zero, mul_eq_zero] at this
    exact this.resolve_left (ENNReal.inv_ne_zero.2 (ENNReal.natCast_ne_top _))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hg : AEMeasurable g μ
hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, g x < f x + (↑n : ℝ≥0∞)⁻¹
⊢ f =ᶠ[ae μ] g
have refine : ∀ (x : α) (hlt : ∀ (i : ℕ), g x < f x + (↑i : ℝ≥0∞)⁻¹) (hle : f x ≤ g x), g x ≤ f x
Tactic: refine hfg.mp ((ae_all_iff.2 this).mono fun x hlt hle => hle.antisymm ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hg : AEMeasurable g μ
hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, g x < f x + (↑n : ℝ≥0∞)⁻¹
x : α
hlt : ∀ (i : ℕ), g x < f x + (↑i : ℝ≥0∞)⁻¹
hle : f x ≤ g x
⊢ g x ≤ f x
have suffices : Tendsto (fun (n : ℕ) ↦ f x + (↑n : ℝ≥0∞)⁻¹) atTop (𝓝 (f x))
Tactic: suffices Tendsto (fun n : ℕ => f x + (n : ℝ≥0∞)⁻¹) atTop (𝓝 (f x)) from
    ge_of_tendsto' this fun i => (hlt i).le
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
h_le : f ≤ᶠ[ae μ] g
h : ∃ᵐ (x : α) ∂μ, f x ≠ g x
⊢ ∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ
have contrapose! : ∀ (h : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ), ∀ᵐ (x : α) ∂μ, f x = g x
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hμ : μ ≠ 0
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ᵐ (x : α) ∂μ, f x < g x
⊢ ∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ
have hμ₁ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [Ne, ← Measure.measure_univ_eq_zero] at hμ
Cleared hypotheses: hμ, hg, hfi, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ᵐ (x : α) ∂μ, f x < g x
⊢ ∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ
have refine : ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set α) univ x → f x < g x
Tactic: refine lintegral_strict_mono_of_ae_le_of_ae_lt_on hg hfi (ae_le_of_ae_lt h) hμ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Markov (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
h2f : ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ ∀ᵐ (x : α) ∂μ, f x < ∞
have simp_rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | f a = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [ae_iff, ENNReal.not_lt_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Norm (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
⊢ ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ ≤ ∫⁻ (x : α), ‖f x‖ₑ ∂μ
have simp_rw : ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ ≤ ∫⁻ (x : α), ENNReal.ofReal ‖f x‖ ∂μ
Tactic: simp_rw [← ofReal_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Norm (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
⊢ ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ ≤ ∫⁻ (x : α), ENNReal.ofReal ‖f x‖ ∂μ
have refine : ∀ (x : α), f x ≤ ‖f x‖
Tactic: refine lintegral_mono fun x => ENNReal.ofReal_le_ofReal ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Norm (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
h_nonneg : 0 ≤ᶠ[ae μ] f
⊢ ∫⁻ (x : α), ‖f x‖ₑ ∂μ = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ
have h : (ae μ).EventuallyEq (β := ENNReal) (fun (a : α) ↦ ‖f a‖ₑ) fun (a : α) ↦ ENNReal.ofReal (f a)
Tactic: apply lintegral_congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Norm (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
h_nonneg : 0 ≤ᶠ[ae μ] f
⊢ (ae μ).EventuallyEq (β := ENNReal) (fun (a : α) ↦ ‖f a‖ₑ) fun (a : α) ↦ ENNReal.ofReal (f a)
have h : ∀ (x : α) (hx : 0 x ≤ f x), ‖f x‖ₑ = ENNReal.ofReal (f x)
Tactic: filter_upwards [h_nonneg] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Norm (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
h_nonneg : 0 ≤ᶠ[ae μ] f
x : α
hx : 0 x ≤ f x
⊢ ‖f x‖ₑ = ENNReal.ofReal (f x)
have h : ENNReal.ofReal (f x) = ENNReal.ofReal (f x)
Tactic: rw [Real.enorm_eq_ofReal hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
hg_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
h_le : g ≤ᶠ[ae μ] f
⊢ ∫⁻ (a : α), f a - g a ∂μ = ∫⁻ (a : α), f a ∂μ - ∫⁻ (a : α), g a ∂μ
have refine : ∫⁻ (a : α), f a - g a ∂μ + ∫⁻ (a : α), g a ∂μ = ∫⁻ (a : α), f a ∂μ
Tactic: refine ENNReal.eq_sub_of_add_eq hg_fin ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hg : AEMeasurable g μ
hg_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
h_le : g ≤ᶠ[ae μ] f
⊢ ∫⁻ (a : α), f a - g a ∂μ + ∫⁻ (a : α), g a ∂μ = ∫⁻ (a : α), f a ∂μ
have rw : ∫⁻ (a : α), f a - g a + g a ∂μ = ∫⁻ (a : α), f a ∂μ
Tactic: rw [← lintegral_add_right' _ hg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ ∫⁻ (x : α), g x ∂μ - ∫⁻ (x : α), f x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ
have rw : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ + ∫⁻ (x : α), f x ∂μ
Tactic: rw [tsub_le_iff_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ + ∫⁻ (x : α), f x ∂μ
have pos : ∀ (hfi : ∫⁻ (x : α), f x ∂μ = ∞), ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ + ∫⁻ (x : α), f x ∂μ
Tactic: by_cases hfi : ∫⁻ x, f x ∂μ = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
pos : ∀ (hfi : ∫⁻ (x : α), f x ∂μ = ∞), ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ + ∫⁻ (x : α), f x ∂μ
⊢ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ + ∫⁻ (x : α), f x ∂μ
have neg : ∀ (hfi : ¬∫⁻ (x : α), f x ∂μ = ∞), ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ + ∫⁻ (x : α), f x ∂μ
Tactic: by_cases hfi : ∫⁻ x, f x ∂μ = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hfi : ∫⁻ (x : α), f x ∂μ = ∞
⊢ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ + ∫⁻ (x : α), f x ∂μ
have pos : ∫⁻ (x : α), g x ∂μ ≤ ∞
Tactic: rw [hfi, add_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hfi : ¬∫⁻ (x : α), f x ∂μ = ∞
⊢ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ + ∫⁻ (x : α), f x ∂μ
have neg : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (a : α), g a - f a + f a ∂μ
Tactic: rw [← lintegral_add_right' _ hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hfi : ¬∫⁻ (x : α), f x ∂μ = ∞
⊢ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (a : α), g a - f a + f a ∂μ
have neg : ∀ (x : α), g x ≤ g x - f x + f x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), Measurable (f n)
h_mono_1 : ∀ (n : ℕ), f n.succ ≤ᶠ[ae μ] f n
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
fn_le_f0 : ∫⁻ (a : α), ⨅ (n : ℕ), f n a ∂μ ≤ ∫⁻ (a : α), f 0 a ∂μ
fn_le_f0' : ⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ ≤ ∫⁻ (a : α), f 0 a ∂μ
h_mono : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), f n.succ a ≤ f n a
n : ℕ
a : α
h : ∀ (n : ℕ), f n.succ a ≤ f n a
⊢ f n a ≤ f 0 a
have zero : f 0 a ≤ f 0 a
Tactic: induction n with
              | zero => rfl
              | succ n ih => exact (h n).trans ih
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), Measurable (f n)
h_mono_1 : ∀ (n : ℕ), f n.succ ≤ᶠ[ae μ] f n
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
fn_le_f0 : ∫⁻ (a : α), ⨅ (n : ℕ), f n a ∂μ ≤ ∫⁻ (a : α), f 0 a ∂μ
fn_le_f0' : ⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ ≤ ∫⁻ (a : α), f 0 a ∂μ
h_mono : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), f n.succ a ≤ f n a
n : ℕ
a : α
h : ∀ (n : ℕ), f n.succ a ≤ f n a
zero : f 0 a ≤ f 0 a
⊢ f n a ≤ f 0 a
have succ : ∀ (n : ℕ) (ih : f n a ≤ f 0 a), f (n + 1) a ≤ f 0 a
Tactic: induction n with
              | zero => rfl
              | succ n ih => exact (h n).trans ih
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
⊢ ∫⁻ (a : α), ⨅ (n : ℕ), f n a ∂μ = ⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
have simp_rw : ∫⁻ (a : α), (⨅ (i : ℕ), f i) a ∂μ = ⨅ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
Tactic: simp_rw [← iInf_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : ℕ) ↦ f i x
n m : ℕ
hnm : n ≤ m
x : α
⊢ aeSeq h_meas p m x ≤ aeSeq h_meas p n x
have pos : ∀ (hx : x ∈ aeSeqSet h_meas p), aeSeq h_meas p m x ≤ aeSeq h_meas p n x
Tactic: by_cases hx : x ∈ aeSeqSet h_meas p
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
p : α → (ℕ → ℝ≥0∞) → Prop := fun (x : α) (f' : ℕ → ℝ≥0∞) ↦ Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun (i : ℕ) ↦ f i x
n m : ℕ
hnm : n ≤ m
x : α
pos : ∀ (hx : x ∈ aeSeqSet h_meas p), aeSeq h_meas p m x ≤ aeSeq h_meas p n x
⊢ aeSeq h_meas p m x ≤ aeSeq h_meas p n x
have neg : ∀ (hx : x ∉ aeSeqSet h_meas p), aeSeq h_meas p m x ≤ aeSeq h_meas p n x
Tactic: by_cases hx : x ∈ aeSeqSet h_meas p