awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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
x₃ : ‖(↑x : E)‖ = norm.{u_3} (E := 𝕜) ((s x : (a : E) → 𝕜) (↑x : E) : 𝕜)
⊢ norm.{u_3} (E := 𝕜) ((s x : (a : E) → 𝕜) (↑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]

Premises used: HSub.hSub, ContinuousLinearMap.le_of_opNorm_le, And.left, Subtype.val, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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 ∈ 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]
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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
⊢ ∀ (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)
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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 rwa rwa₁ rwa₂ rwa₃ :
  ∀ (i : (↑d : Type u_2)), ∀ᵐ (a : α) ∂μ, Eq.{u_3 + 1} (α := 𝕜) ((s i : (a : E) → 𝕜) (f a) : 𝕜) (0 : 𝕜)
⊢ ∀ᵐ (x : α) ∂μ, ∀ (y : (↑d : Type u_2)), Eq.{u_3 + 1} (α := 𝕜) ((s y : (a : E) → 𝕜) (f x) : 𝕜) (0 : 𝕜)

Tactic:
rwa [ae_all_iff]

Premises used: MeasureTheory.ae_all_iff
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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 : 𝕜)
⊢ ∀ᵐ (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]
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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 : 𝕜)
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
⊢ f =ᶠ[ae μ] 0

Tactic:
filter_upwards [hf', h't] with x hx h'x
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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 : 𝕜)
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:
A (f x) h'x hx
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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 : 𝕜)
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:
exact A (f x) h'x hx
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SecondCountableTopology E
f : α → E
hf : ∀ (c : StrongDual 𝕜 E), EventuallyEq.{u_1, u_3} (β := 𝕜) (ae μ) (fun (x : α) ↦ (c : (a : E) → 𝕜) (f x)) 0
⊢ f =ᶠ[ae μ] 0

Tactic:
ae_eq_zero_of_forall_dual_of_isSeparable 𝕜 (.of_separableSpace Set.univ) hf
    (Eventually.of_forall fun _ => Set.mem_univ _)

Premises used: Set.univ, Filter.Eventually.of_forall, TopologicalSpace.IsSeparable.of_separableSpace, Set.mem_univ, MeasureTheory.ae_eq_zero_of_forall_dual_of_isSeparable
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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 ∂μ)
rw : ∀ b < 0, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ b} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂μ, 0 ≤ f x

Tactic:
rw [ae_const_le_iff_forall_lt_measure_zero]

Premises used: MeasureTheory.ae_const_le_iff_forall_lt_measure_zero
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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}
⊢ NullMeasurableSet s μ

Tactic:
have hs : NullMeasurableSet s μ := nullMeasurableSet_le hf.1.aemeasurable aemeasurable_const
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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 μ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have mus : μ s < ∞ := Integrable.measure_le_lt_top hf hb_neg
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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 ∂μ)

Tactic:
setIntegral_mono_ae_restrict hf.integrableOn (integrableOn_const mus.ne) ?_

Premises used: MeasureTheory.integrableOn_const, MeasureTheory.setIntegral_mono_ae_restrict, MeasureTheory.Integrable.integrableOn, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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∞)
refine : f ≤ᶠ[ae (μ.restrict s)] fun (x : α) ↦ b
⊢ LE.le (α := ℝ) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, b ∂μ)

Tactic:
refine setIntegral_mono_ae_restrict hf.integrableOn (integrableOn_const mus.ne) ?_

Premises used: MeasureTheory.integrableOn_const, MeasureTheory.setIntegral_mono_ae_restrict, MeasureTheory.Integrable.integrableOn, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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∞)
rw : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ b
⊢ f ≤ᶠ[ae (μ.restrict s)] fun (x : α) ↦ b

Tactic:
rw [EventuallyLE, ae_restrict_iff₀ (hs.mono μ.restrict_le_self)]

Premises used: MeasureTheory.ae_restrict_iff₀, MeasureTheory.Measure.restrict_le_self, Filter.EventuallyLE, MeasureTheory.NullMeasurableSet.mono
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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 : α) ∂μ, x ∈ s → f x ≤ b

Tactic:
Eventually.of_forall fun x hxs => hxs

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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 : α) ∂μ, x ∈ s → f x ≤ b

Tactic:
exact Eventually.of_forall fun x hxs => hxs

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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 ∂μ)

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
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (h_const_le : ∫ (x : α) in s, f x ∂μ ≤ b * μ.real s), ∫ (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

Premises used: mul_comm, smul_eq_mul, MeasureTheory.setIntegral_const
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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

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
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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
contrapose! :
  ∀ (H : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ b} : ℝ≥0∞) (0 : ℝ≥0∞)),
    b * μ.real s < ∫ (x : α) in s, f x ∂μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ b} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
contrapose! h_int_gt with H
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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 < 0

Tactic:
mul_neg_of_neg_of_pos hb_neg <| ENNReal.toReal_pos H mus.ne

Premises used: mul_neg_of_neg_of_pos, ENNReal.toReal_pos, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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∞)
rw : LE.le (α := ℝ) 0 (∫ (x : α) in toMeasurable μ s, f x ∂μ)
⊢ LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)

Tactic:
rw [← μ.restrict_toMeasurable mus.ne]

Premises used: MeasureTheory.Measure.restrict_toMeasurable, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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∞)
rwa rwa₁ rwa₂ rwa₃ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rwa [measure_toMeasurable]

Premises used: MeasureTheory.measure_toMeasurable
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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 toMeasurable μ s, f x ∂μ)

Tactic:
exact hf_zero _ (measurableSet_toMeasurable ..) (by rwa [measure_toMeasurable])

Premises used: MeasureTheory.measurableSet_toMeasurable
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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₁ : LE.le (α := ℝ) 0 (∫ (x : α) in s, f x ∂μ)
⊢ b * μ.real s < ∫ (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])

Premises used: mul_neg_of_neg_of_pos, MeasureTheory.Measure.real, ENNReal.toReal_pos, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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 ∂μ)
rw : 0 ≤ᶠ[ae μ] g - f
⊢ f ≤ᶠ[ae μ] g

Tactic:
rw [← eventually_sub_nonneg]

Premises used: Filter.eventually_sub_nonneg
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
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

Tactic:
ae_nonneg_of_forall_setIntegral_nonneg (hg.sub hf) fun s hs => ?_

Premises used: MeasureTheory.Integrable.sub, MeasureTheory.ae_nonneg_of_forall_setIntegral_nonneg