awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : StrongDual 𝕜 E), EventuallyEq.{u_1, u_3} (β := 𝕜) (ae μ) (fun (x : α) ↦ (c : (a : E) → 𝕜) (f x)) 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
this : Encodable (↑d : Type u_2)
s : (x : (↑d : Type u_2)) → StrongDual 𝕜 E
hs :
  ∀ (x : (↑d : Type u_2)), ‖s x‖ ≤ 1 ∧ Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) ((↑‖(↑x : E)‖ : 𝕜) : 𝕜)
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
a_mem : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
x : (↑d : Type u_2)
hx : dist a (↑x : E) < ‖a‖ / 2
I : ‖a‖ / 2 < ‖(↑x : E)‖
h : Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) a : 𝕜) (0 : 𝕜)
x₁ :
  norm.{u_3} (E := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) = norm.{u_3} (E := 𝕜) ((s x : (a : E) → 𝕜) ((↑x : E) - a) : 𝕜)
x₂ : 1 * ‖(↑x : E) - a‖ < ‖a‖ / 2
⊢ norm.{u_3} (E := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) < norm.{u_3} (E := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜)
have x₃ : ‖(↑x : E)‖ = norm.{u_3} (E := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜)
Tactic: calc
      ‖s x x‖ = ‖s x (x - a)‖ := by simp only [h, sub_zero, map_sub]
      _ ≤ 1 * ‖(x : E) - a‖ := ContinuousLinearMap.le_of_opNorm_le _ (hs x).1 _
      _ < ‖a‖ / 2 := by rw [one_mul]; rwa [dist_eq_norm'] at hx
      _ < ‖(x : E)‖ := I
      _ = ‖s x x‖ := by simp [(hs x).2]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (hypothesis)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : StrongDual 𝕜 E), EventuallyEq.{u_1, u_3} (β := 𝕜) (ae μ) (fun (x : α) ↦ (c : (a : E) → 𝕜) (f x)) 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
this : Encodable (↑d : Type u_2)
s : (x : (↑d : Type u_2)) → StrongDual 𝕜 E
hs :
  ∀ (x : (↑d : Type u_2)), ‖s x‖ ≤ 1 ∧ Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) ((↑‖(↑x : E)‖ : 𝕜) : 𝕜)
⊢ f =ᶠ[ae μ] 0
have A : ∀ a ∈ t, (∀ (x : (↑d : Type u_2)), Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) a : 𝕜) (0 : 𝕜)) → a = 0
Tactic: have A : ∀ a : E, a ∈ t → (∀ x, ⟪a, s x⟫ = (0 : 𝕜)) → a = 0 := by
    intro a hat ha
    contrapose! ha
    have a_pos : 0 < ‖a‖ := by simp only [ha, norm_pos_iff, Ne, not_false_iff]
    have a_mem : a ∈ closure d := hd hat
    obtain ⟨x, hx⟩ : ∃ x : d, dist a x < ‖a‖ / 2 := by
      rcases Metric.mem_closure_iff.1 a_mem (‖a‖ / 2) (half_pos a_pos) with ⟨x, h'x, hx⟩
      exact ⟨⟨x, h'x⟩, hx⟩
    use x
    have I : ‖a‖ / 2 < ‖(x : E)‖ := by
      have : ‖a‖ ≤ ‖(x : E)‖ + ‖a - x‖ := norm_le_insert' _ _
      have : ‖a - x‖ < ‖a‖ / 2 := by rwa [dist_eq_norm] at hx
      linarith
    intro h
    apply lt_irrefl ‖s x x‖
    calc
      ‖s x x‖ = ‖s x (x - a)‖ := by simp only [h, sub_zero, map_sub]
      _ ≤ 1 * ‖(x : E) - a‖ := ContinuousLinearMap.le_of_opNorm_le _ (hs x).1 _
      _ < ‖a‖ / 2 := by rw [one_mul]; rwa [dist_eq_norm'] at hx
      _ < ‖(x : E)‖ := I
      _ = ‖s x x‖ := by simp [(hs x).2]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (hypothesis)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : StrongDual 𝕜 E), EventuallyEq.{u_1, u_3} (β := 𝕜) (ae μ) (fun (x : α) ↦ (c : (a : E) → 𝕜) (f x)) 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
this : Encodable (↑d : Type u_2)
s : (x : (↑d : Type u_2)) → StrongDual 𝕜 E
hs :
  ∀ (x : (↑d : Type u_2)), ‖s x‖ ≤ 1 ∧ Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) ((↑‖(↑x : E)‖ : 𝕜) : 𝕜)
A : ∀ a ∈ t, (∀ (x : (↑d : Type u_2)), Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) a : 𝕜) (0 : 𝕜)) → a = 0
⊢ f =ᶠ[ae μ] 0
have hfs : ∀ (y : (↑d : Type u_2)), ∀ᵐ (x : α) ∂μ, Eq.{u_3 + 1} (α := 𝕜) ((s y : (a : E) → 𝕜) (f x) : 𝕜) (0 : 𝕜)
Tactic: have hfs : ∀ y : d, ∀ᵐ x ∂μ, ⟪f x, s y⟫ = (0 : 𝕜) := fun y => hf (s y)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (hypothesis)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : StrongDual 𝕜 E), EventuallyEq.{u_1, u_3} (β := 𝕜) (ae μ) (fun (x : α) ↦ (c : (a : E) → 𝕜) (f x)) 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
this : Encodable (↑d : Type u_2)
s : (x : (↑d : Type u_2)) → StrongDual 𝕜 E
hs :
  ∀ (x : (↑d : Type u_2)), ‖s x‖ ≤ 1 ∧ Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) ((↑‖(↑x : E)‖ : 𝕜) : 𝕜)
A : ∀ a ∈ t, (∀ (x : (↑d : Type u_2)), Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) a : 𝕜) (0 : 𝕜)) → a = 0
hfs : ∀ (y : (↑d : Type u_2)), ∀ᵐ (x : α) ∂μ, Eq.{u_3 + 1} (α := 𝕜) ((s y : (a : E) → 𝕜) (f x) : 𝕜) (0 : 𝕜)
⊢ f =ᶠ[ae μ] 0
have hf' : ∀ᵐ (x : α) ∂μ, ∀ (y : (↑d : Type u_2)), Eq.{u_3 + 1} (α := 𝕜) ((s y : (a : E) → 𝕜) (f x) : 𝕜) (0 : 𝕜)
Tactic: have hf' : ∀ᵐ x ∂μ, ∀ y : d, ⟪f x, s y⟫ = (0 : 𝕜) := by rwa [ae_all_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : StrongDual 𝕜 E), EventuallyEq.{u_1, u_3} (β := 𝕜) (ae μ) (fun (x : α) ↦ (c : (a : E) → 𝕜) (f x)) 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] d
this : Encodable (↑d : Type u_2)
s : (x : (↑d : Type u_2)) → StrongDual 𝕜 E
hs :
  ∀ (x : (↑d : Type u_2)), ‖s x‖ ≤ 1 ∧ Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜) ((↑‖(↑x : E)‖ : 𝕜) : 𝕜)
A : ∀ a ∈ t, (∀ (x : (↑d : Type u_2)), Eq.{u_3 + 1} (α := 𝕜) ((s x : (a : E) → 𝕜) a : 𝕜) (0 : 𝕜)) → a = 0
hfs : ∀ (y : (↑d : Type u_2)), ∀ᵐ (x : α) ∂μ, Eq.{u_3 + 1} (α := 𝕜) ((s y : (a : E) → 𝕜) (f x) : 𝕜) (0 : 𝕜)
hf' : ∀ᵐ (x : α) ∂μ, ∀ (y : (↑d : Type u_2)), Eq.{u_3 + 1} (α := 𝕜) ((s y : (a : E) → 𝕜) (f x) : 𝕜) (0 : 𝕜)
⊢ f =ᶠ[ae μ] 0
have h : ∀ (x : α) (hx : ∀ (y : (↑d : Type u_2)), Eq.{u_3 + 1} (α := 𝕜) ((s y : (a : E) → 𝕜) (f x) : 𝕜) (0 : 𝕜)) (h'x : f x ∈ t),
  f x = 0 x
Tactic: filter_upwards [hf', h't] with x hx h'x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
⊢ ∀ᵐ (x : α) ∂μ, 0 ≤ f x
have rw : ∀ b < 0, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ b} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [ae_const_le_iff_forall_lt_measure_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
b : ℝ
hb_neg : b < 0
s : Set α := {x : α | f x ≤ b}
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ b} : ℝ≥0∞) (0 : ℝ≥0∞)
have hs : NullMeasurableSet s μ
Tactic: have hs : NullMeasurableSet s μ := nullMeasurableSet_le hf.1.aemeasurable aemeasurable_const
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
b : ℝ
hb_neg : b < 0
s : Set α := {x : α | f x ≤ b}
hs : NullMeasurableSet s μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ b} : ℝ≥0∞) (0 : ℝ≥0∞)
have mus : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have mus : μ s < ∞ := Integrable.measure_le_lt_top hf hb_neg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
b : ℝ
hb_neg : b < 0
s : Set α := {x : α | f x ≤ b}
hs : NullMeasurableSet s μ
mus : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, b ∂μ)
have refine : f ≤ᶠ[ae (μ.restrict s)] fun (x : α) ↦ b
Tactic: refine setIntegral_mono_ae_restrict hf.integrableOn (integrableOn_const mus.ne) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
b : ℝ
hb_neg : b < 0
s : Set α := {x : α | f x ≤ b}
hs : NullMeasurableSet s μ
mus : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ f ≤ᶠ[ae (μ.restrict s)] fun (x : α) ↦ b
have rw : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ b
Tactic: rw [EventuallyLE, ae_restrict_iff₀ (hs.mono μ.restrict_le_self)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
b : ℝ
hb_neg : b < 0
s : Set α := {x : α | f x ≤ b}
hs : NullMeasurableSet s μ
mus : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫ (x : α) in s, f x ∂μ ≤ b * μ.real s
have h_const_le : LE.le (α := ℝ) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, b ∂μ)
Tactic: have h_const_le : (∫ x in s, f x ∂μ) ≤ ∫ _ in s, b ∂μ := by
      refine setIntegral_mono_ae_restrict hf.integrableOn (integrableOn_const mus.ne) ?_
      rw [EventuallyLE, ae_restrict_iff₀ (hs.mono μ.restrict_le_self)]
      exact Eventually.of_forall fun x hxs => hxs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
b : ℝ
hb_neg : b < 0
s : Set α := {x : α | f x ≤ b}
hs : NullMeasurableSet s μ
mus : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_const_le : LE.le (α := ℝ) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, b ∂μ)
⊢ ∫ (x : α) in s, f x ∂μ ≤ b * μ.real s
have rwa : ∀ (h_const_le : ∫ (x : α) in s, f x ∂μ ≤ μ.real s • b), ∫ (x : α) in s, f x ∂μ ≤ b * μ.real s
Tactic: rwa [setIntegral_const, smul_eq_mul, mul_comm] at h_const_le
Cleared hypotheses: h_const_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
b : ℝ
hb_neg : b < 0
s : Set α := {x : α | f x ≤ b}
hs : NullMeasurableSet s μ
mus : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_const_le : LE.le (α := ℝ) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, b ∂μ)
rwa : ∀ (h_const_le : ∫ (x : α) in s, f x ∂μ ≤ μ.real s • b), ∫ (x : α) in s, f x ∂μ ≤ b * μ.real s
⊢ ∫ (x : α) in s, f x ∂μ ≤ b * μ.real s
have rwa₁ : ∀ (h_const_le : ∫ (x : α) in s, f x ∂μ ≤ μ.real s * b), ∫ (x : α) in s, f x ∂μ ≤ b * μ.real s
Tactic: rwa [setIntegral_const, smul_eq_mul, mul_comm] at h_const_le
Cleared hypotheses: h_const_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
b : ℝ
hb_neg : b < 0
s : Set α := {x : α | f x ≤ b}
hs : NullMeasurableSet s μ
mus : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_const_le : LE.le (α := ℝ) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, b ∂μ)
rwa : ∀ (h_const_le : ∫ (x : α) in s, f x ∂μ ≤ μ.real s • b), ∫ (x : α) in s, f x ∂μ ≤ b * μ.real s
rwa₁ : ∀ (h_const_le : ∫ (x : α) in s, f x ∂μ ≤ μ.real s * b), ∫ (x : α) in s, f x ∂μ ≤ b * μ.real s
⊢ ∫ (x : α) in s, f x ∂μ ≤ b * μ.real s
have rwa₂ : ∀ (h_const_le : ∫ (x : α) in s, f x ∂μ ≤ b * μ.real s), ∫ (x : α) in s, f x ∂μ ≤ b * μ.real s
Tactic: rwa [setIntegral_const, smul_eq_mul, mul_comm] at h_const_le
Cleared hypotheses: h_const_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
b : ℝ
hb_neg : b < 0
s : Set α := {x : α | f x ≤ b}
hs : NullMeasurableSet s μ
mus : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ b} : ℝ≥0∞) (0 : ℝ≥0∞)
have h_int_gt : ∫ (x : α) in s, f x ∂μ ≤ b * μ.real s
Tactic: have h_int_gt : (∫ x in s, f x ∂μ) ≤ b * μ.real s := by
    have h_const_le : (∫ x in s, f x ∂μ) ≤ ∫ _ in s, b ∂μ := by
      refine setIntegral_mono_ae_restrict hf.integrableOn (integrableOn_const mus.ne) ?_
      rw [EventuallyLE, ae_restrict_iff₀ (hs.mono μ.restrict_le_self)]
      exact Eventually.of_forall fun x hxs => hxs
    rwa [setIntegral_const, smul_eq_mul, mul_comm] at h_const_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
b : ℝ
hb_neg : b < 0
s : Set α := {x : α | f x ≤ b}
hs : NullMeasurableSet s μ
mus : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_int_gt : ∫ (x : α) in s, f x ∂μ ≤ b * μ.real s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ b} : ℝ≥0∞) (0 : ℝ≥0∞)
have contrapose! : ∀ (H : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ b} : ℝ≥0∞) (0 : ℝ≥0∞)),
  b * μ.real s < ∫ (x : α) in s, f x ∂μ
Tactic: contrapose! h_int_gt with H
Cleared hypotheses: h_int_gt
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
b : ℝ
hb_neg : b < 0
s : Set α := {x : α | f x ≤ b}
hs : NullMeasurableSet s μ
mus : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
H : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ b} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
have rw : LE.le (α := ℝ) 0 (∫ (x : α) in toMeasurable μ s, f x ∂μ)
Tactic: rw [← μ.restrict_toMeasurable mus.ne]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
b : ℝ
hb_neg : b < 0
s : Set α := {x : α | f x ≤ b}
hs : NullMeasurableSet s μ
mus : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
H : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ b} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ b * μ.real s < ∫ (x : α) in s, f x ∂μ
have b₁ : LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
Tactic: calc
    b * μ.real s < 0 := mul_neg_of_neg_of_pos hb_neg <| ENNReal.toReal_pos H mus.ne
    _ ≤ ∫ x in s, f x ∂μ := by
      rw [← μ.restrict_toMeasurable mus.ne]
      exact hf_zero _ (measurableSet_toMeasurable ..) (by rwa [measure_toMeasurable])
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
hf_le :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LE.le (α := ℝ) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, g x ∂μ)
⊢ f ≤ᶠ[ae μ] g
have rw : 0 ≤ᶠ[ae μ] g - f
Tactic: rw [← eventually_sub_nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
hf_le :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LE.le (α := ℝ) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, g x ∂μ)
⊢ 0 ≤ᶠ[ae μ] g - f
have refine : ∀ (s : Set α) (hs : MeasurableSet s),
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, (g - f) x ∂μ)
Tactic: refine ae_nonneg_of_forall_setIntegral_nonneg (hg.sub hf) fun s hs => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
hf_le :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LE.le (α := ℝ) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, g x ∂μ)
s : Set α
hs : MeasurableSet s
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, (g - f) x ∂μ)
have rw : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
  LE.le (α := ℝ) (∫ (a : α) in s, f a ∂μ) (∫ (a : α) in s, g a ∂μ)
Tactic: rw [integral_sub' hg.integrableOn hf.integrableOn, sub_nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
t : Set α
hf : IntegrableOn f t μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LE.le (α := ℝ) 0 (∫ (x : α) in s ∩ t, f x ∂μ)
⊢ 0 ≤ᶠ[ae (μ.restrict t)] f
have refine : ∀ (s : Set α) (hs : MeasurableSet s)
  (h's : LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ.restrict t)
Tactic: refine ae_nonneg_of_forall_setIntegral_nonneg hf fun s hs h's => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
t : Set α
hf : IntegrableOn f t μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LE.le (α := ℝ) 0 (∫ (x : α) in s ∩ t, f x ∂μ)
s : Set α
hs : MeasurableSet s
h's : LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ.restrict t)
have simp_rw : LE.le (α := ℝ) 0 (∫ (x : α) in s ∩ t, f x ∂μ)
Tactic: simp_rw [Measure.restrict_restrict hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
t : Set α
hf : IntegrableOn f t μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LE.le (α := ℝ) 0 (∫ (x : α) in s ∩ t, f x ∂μ)
s : Set α
hs : MeasurableSet s
h's : LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ) 0 (∫ (x : α) in s ∩ t, f x ∂μ)
have apply : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: apply hf_zero s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
t : Set α
hf : IntegrableOn f t μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LE.le (α := ℝ) 0 (∫ (x : α) in s ∩ t, f x ∂μ)
s : Set α
hs : MeasurableSet s
h's : LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
have rwa : ∀ (h's : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)),
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rwa [Measure.restrict_apply hs] at h's
Cleared hypotheses: h's
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
⊢ 0 ≤ᶠ[ae μ] f
have h : ∀ (s : Set α),
  MeasurableSet s →
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ∀ᵐ (x : α) ∂μ.restrict s, 0 x ≤ f x
Tactic: apply ae_of_forall_measure_lt_top_ae_restrict
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f : α → ℝ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
t : Set α
t_meas : MeasurableSet t
t_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂μ.restrict t, 0 x ≤ f x
have h : ∀ (s : Set α),
  MeasurableSet s →
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞) →
      LE.le (α := ℝ) 0 (∫ (x : α) in s ∩ t, f x ∂μ)
Tactic: apply ae_nonneg_restrict_of_forall_setIntegral_nonneg_inter (hf_int_finite t t_meas t_lt_top)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEFinStronglyMeasurable f μ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
t : Set α := hf.sigmaFiniteSet
⊢ 0 ≤ᶠ[ae μ] f
have suffices : 0 ≤ᶠ[ae (μ.restrict t)] f
Tactic: suffices 0 ≤ᵐ[μ.restrict t] f from
    ae_of_ae_restrict_of_ae_restrict_compl _ this hf.ae_eq_zero_compl.symm.le
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEFinStronglyMeasurable f μ
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
t : Set α := hf.sigmaFiniteSet
⊢ 0 ≤ᶠ[ae (μ.restrict t)] f
have this : SigmaFinite (μ.restrict t)
Tactic: haveI : SigmaFinite (μ.restrict t) := hf.sigmaFinite_restrict