awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
inst_3 : IsFiniteMeasure μ
h : NeZero μ
c : E
rw : ∫ (x : α), c ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ = c
rw₁ : (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ).real univ • c = c
rw₂ :
  ENNReal.toReal ((HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ : (a : Set α) → ℝ≥0∞) univ) •
      c =
    c
rw₃ : ENNReal.toReal 1 • c = c
rw₄ : HSMul.hSMul (α := ℝ) 1 c = c
rw₅ rw₆ : c = c
⊢ ⨍ (_x : α), c ∂μ = c

Tactic:
rw [average, integral_const, measureReal_def, measure_univ, ENNReal.toReal_one, one_smul]

Premises used: ENNReal.toReal_one, MeasureTheory.IsProbabilityMeasure.measure_univ, MeasureTheory.average, one_smul, MeasureTheory.integral_const, MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
s : Set α
hs₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
⊢ ⨍ (x : α) in s, c ∂μ = c

Tactic:
have := NeZero.mk hs₀; have := Fact.mk hs.lt_top; average_const _ _

Premises used: NeZero.mk, MeasureTheory.Measure.restrict, Fact.mk, Ne.lt_top, MeasureTheory.average_const
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
inst_3 : IsFiniteMeasure μ
f : α → E
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α), ⨍ (a : α), f a ∂μ ∂μ) (∫ (x : α), f x ∂μ)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
inst_3 : IsFiniteMeasure μ
f : α → E
s : Set α
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, ⨍ (a : α) in s, f a ∂μ ∂μ) (∫ (x : α) in s, f x ∂μ)

Tactic:
integral_average _ _

Premises used: MeasureTheory.integral_average
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
inst_3 : IsFiniteMeasure μ
f : α → E
pos : ∀ (hf : Integrable f μ), Eq.{u_2 + 1} (α := E) (∫ (x : α), f x - ⨍ (a : α), f a ∂μ ∂μ) 0
neg : ∀ (hf : ¬Integrable f μ), Eq.{u_2 + 1} (α := E) (∫ (x : α), f x - ⨍ (a : α), f a ∂μ ∂μ) 0
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α), f x - ⨍ (a : α), f a ∂μ ∂μ) 0

Tactic:
by_cases hf : Integrable f μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
inst_3 : IsFiniteMeasure μ
f : α → E
hf : Integrable f μ
pos : HSub.hSub (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), ⨍ (a : α), f a ∂μ ∂μ) = 0
pos₁ : HSub.hSub (α := E) (∫ (a : α), f a ∂μ) (∫ (x : α), f x ∂μ) = 0
pos₂ pos₃ : Eq.{u_2 + 1} (α := E) 0 0
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α), f x - ⨍ (a : α), f a ∂μ ∂μ) 0

Tactic:
rw [integral_sub hf (integrable_const _), integral_average, sub_self]

Premises used: sub_self, MeasureTheory.integral_average, MeasureTheory.integral_sub, MeasureTheory.integrable_const
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
inst_3 : IsFiniteMeasure μ
f : α → E
hf : ¬Integrable f μ
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α), f x - ⨍ (a : α), f a ∂μ ∂μ) 0

Tactic:
integral_undef fun h => hf ?_

Premises used: MeasureTheory.integral_undef
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
inst_3 : IsFiniteMeasure μ
f : α → E
hf : ¬Integrable f μ
neg : ∀ (h : Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x - ⨍ (a : α), f a ∂μ) μ), Integrable f μ
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α), f x - ⨍ (a : α), f a ∂μ ∂μ) 0

Tactic:
refine integral_undef fun h => hf ?_

Premises used: MeasureTheory.integral_undef
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
inst_3 : IsFiniteMeasure μ
f : α → E
hf : ¬Integrable f μ
h : Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x - ⨍ (a : α), f a ∂μ) μ
⊢ Integrable (HAdd.hAdd (α := α → E) (fun (x : α) ↦ f x - ⨍ (a : α), f a ∂μ) fun (x : α) ↦ ⨍ (a : α), f a ∂μ) μ

Tactic:
h.add (integrable_const (⨍ a, f a ∂μ))

Premises used: MeasureTheory.average, MeasureTheory.Integrable.add, MeasureTheory.integrable_const
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
inst_3 : IsFiniteMeasure μ
f : α → E
hf : ¬Integrable f μ
h : Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x - ⨍ (a : α), f a ∂μ) μ
h₁ : f = HAdd.hAdd (α := α → E) (fun (x : α) ↦ f x - ⨍ (a : α), f a ∂μ) fun (x : α) ↦ ⨍ (a : α), f a ∂μ
⊢ Integrable f μ

Tactic:
convert! h.add (integrable_const (⨍ a, f a ∂μ))

Premises used: MeasureTheory.average, MeasureTheory.Integrable.add, MeasureTheory.integrable_const
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
inst_3 : IsFiniteMeasure μ
f : α → E
hf : ¬Integrable f μ
h : Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x - ⨍ (a : α), f a ∂μ) μ
⊢ f = HAdd.hAdd (α := α → E) (fun (x : α) ↦ f x - ⨍ (a : α), f a ∂μ) fun (x : α) ↦ ⨍ (a : α), f a ∂μ

Tactic:
(sub_add_cancel _ _).symm

Premises used: Eq.symm, sub_add_cancel
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
inst_3 : IsFiniteMeasure μ
f : α → E
hf : ¬Integrable f μ
h : Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x - ⨍ (a : α), f a ∂μ) μ
⊢ f = HAdd.hAdd (α := α → E) (fun (x : α) ↦ f x - ⨍ (a : α), f a ∂μ) fun (x : α) ↦ ⨍ (a : α), f a ∂μ

Tactic:
exact (sub_add_cancel _ _).symm

Premises used: Eq.symm, sub_add_cancel
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
s : Set α
inst_2 : CompleteSpace E
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : α → E
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x - ⨍ (a : α) in s, f a ∂μ ∂μ) 0

Tactic:
haveI : Fact (μ s < ∞) := ⟨lt_top_iff_ne_top.2 hs⟩
  integral_sub_average _ _

Premises used: MeasureTheory.Measure.restrict, MeasureTheory.integral_sub_average
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
f : α → E
inst_2 : CompleteSpace E
inst_3 : IsFiniteMeasure μ
hf : Integrable f μ
rw : HSub.hSub (α := E) (∫ (a : α), ⨍ (a : α), f a ∂μ ∂μ) (∫ (a : α), f a ∂μ) = 0
rw₁ : HSub.hSub (α := E) (∫ (x : α), f x ∂μ) (∫ (a : α), f a ∂μ) = 0
rw₂ rw₃ : Eq.{u_2 + 1} (α := E) 0 0
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α), ⨍ (a : α), f a ∂μ - f x ∂μ) 0

Tactic:
rw [integral_sub (integrable_const _) hf, integral_average, sub_self]

Premises used: sub_self, MeasureTheory.integral_average, MeasureTheory.integral_sub, MeasureTheory.integrable_const
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
s : Set α
f : α → E
inst_2 : CompleteSpace E
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, ⨍ (a : α) in s, f a ∂μ - f x ∂μ) 0

Tactic:
haveI : Fact (μ s < ∞) := ⟨lt_top_iff_ne_top.2 hs⟩
  integral_average_sub hf

Premises used: MeasureTheory.integral_average_sub
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf₀ : 0 ≤ᶠ[ae μ] f
inl :
  ∀ (hf : @Integrable _ _ _ _ m0 f 0) (hf₀ : 0 ≤ᶠ[ae (F := Measure α) 0] f),
    ENNReal.ofReal (⨍ (x : α), f x ∂0) =
      HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂0) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
inr :
  ∀ (hμ : μ ≠ 0),
    ENNReal.ofReal (⨍ (x : α), f x ∂μ) =
      HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ENNReal.ofReal (⨍ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
obtain rfl | hμ := eq_or_ne μ 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ
hf : @Integrable _ _ _ _ m0 f 0
hf₀ : 0 ≤ᶠ[ae (F := Measure α) 0] f
⊢ ENNReal.ofReal (⨍ (x : α), f x ∂0) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂0) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf₀ : 0 ≤ᶠ[ae μ] f
hμ : μ ≠ 0
inr :
  ENNReal.ofReal (HSMul.hSMul (β := ℝ) (μ.real univ)⁻¹ (∫ (x : α), f x ∂μ)) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
inr₁ :
  ENNReal.ofReal ((μ.real univ)⁻¹ * ∫ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
inr₂ :
  ENNReal.ofReal ((ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ))⁻¹ * ∫ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
inr₃ :
  ENNReal.ofReal (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ * ∫ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
inr₄ :
  ENNReal.ofReal (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹) * ENNReal.ofReal (∫ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
inr₅ :
  HMul.hMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (ENNReal.ofReal (∫ (x : α), f x ∂μ)) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
inr₆ :
  HMul.hMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
inr₇ inr₈ :
  HMul.hMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) =
    HMul.hMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ)
⊢ ENNReal.ofReal (⨍ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
rw [average_eq, smul_eq_mul, measureReal_def, ← toReal_inv, ofReal_mul toReal_nonneg,
      ofReal_toReal (inv_ne_top.2 <| measure_univ_ne_zero.2 hμ),
      ofReal_integral_eq_lintegral_ofReal hf hf₀, ENNReal.div_eq_inv_mul]

Premises used: Iff.mpr, ENNReal.ofReal_mul, ENNReal.inv_ne_top, MeasureTheory.Measure.measure_univ_ne_zero, ENNReal.toReal_inv, ENNReal.ofReal_toReal, ENNReal.toReal_nonneg, MeasureTheory.ofReal_integral_eq_lintegral_ofReal, MeasureTheory.measureReal_def, smul_eq_mul, ENNReal.div_eq_inv_mul, MeasureTheory.average_eq
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hf : IntegrableOn f s μ
hf₀ : 0 ≤ᶠ[ae (μ.restrict s)] f
⊢ ENNReal.ofReal (⨍ (x : α) in s, f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α) in s, ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simpa using ofReal_average hf hf₀

Premises used: MeasureTheory.ofReal_average
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf' : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
rw : (⨍⁻ (x : α), f x ∂μ).toReal = HSMul.hSMul (β := ℝ) (μ.real univ)⁻¹ (∫ (x : α), (f x).toReal ∂μ)
rw₁ :
  (HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)).toReal =
    HSMul.hSMul (β := ℝ) (μ.real univ)⁻¹ (∫ (x : α), (f x).toReal ∂μ)
rw₂ :
  (HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)).toReal =
    (μ.real univ)⁻¹ * ∫ (x : α), (f x).toReal ∂μ
rw₃ :
  (∫⁻ (x : α), f x ∂μ).toReal / ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) =
    (μ.real univ)⁻¹ * ∫ (x : α), (f x).toReal ∂μ
rw₄ :
  (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ))⁻¹ * (∫⁻ (x : α), f x ∂μ).toReal =
    (μ.real univ)⁻¹ * ∫ (x : α), (f x).toReal ∂μ
rw₅ :
  (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ))⁻¹ * ∫ (a : α), (f a).toReal ∂μ =
    (μ.real univ)⁻¹ * ∫ (x : α), (f x).toReal ∂μ
rw₆ rw₇ :
  (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ))⁻¹ * ∫ (a : α), (f a).toReal ∂μ =
    (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ))⁻¹ * ∫ (x : α), (f x).toReal ∂μ
⊢ (⨍⁻ (x : α), f x ∂μ).toReal = ⨍ (x : α), (f x).toReal ∂μ

Tactic:
rw [average_eq, laverage_eq, smul_eq_mul, toReal_div, div_eq_inv_mul, ←
      integral_toReal hf (hf'.mono fun _ => lt_top_iff_ne_top.2), measureReal_def]

Premises used: Iff.mpr, MeasureTheory.laverage_eq, lt_top_iff_ne_top, Filter.Eventually.mono, MeasureTheory.measureReal_def, smul_eq_mul, div_eq_inv_mul, ENNReal.toReal_div, MeasureTheory.integral_toReal, MeasureTheory.average_eq
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.restrict s)
hf' : ∀ᵐ (x : α) ∂μ.restrict s, f x ≠ ∞
⊢ (⨍⁻ (x : α) in s, f x ∂μ).toReal = ⨍ (x : α) in s, (f x).toReal ∂μ

Tactic:
simpa [laverage_eq] using toReal_laverage hf hf'

Premises used: MeasureTheory.laverage_eq, MeasureTheory.toReal_laverage
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞)

Tactic:
pos_iff_ne_zero.2 fun H => ?_

Premises used: Iff.mpr, pos_iff_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
refine :
  ∀ (H : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)),
    False
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞)

Tactic:
refine pos_iff_ne_zero.2 fun H => ?_

Premises used: Iff.mpr, pos_iff_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
rwa : NullMeasurableSet {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} (μ.restrict s)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rwa [restrict_apply₀, inter_comm]

Premises used: Set.inter_comm, MeasureTheory.Measure.restrict_apply₀
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ NullMeasurableSet {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} (μ.restrict s)

Tactic:
AEStronglyMeasurable.nullMeasurableSet_le hf.1 aestronglyMeasurable_const

Premises used: MeasureTheory.aestronglyMeasurable_const, setOf, And.left, MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_le
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ NullMeasurableSet {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} (μ.restrict s)

Tactic:
exact AEStronglyMeasurable.nullMeasurableSet_le hf.1 aestronglyMeasurable_const

Premises used: MeasureTheory.aestronglyMeasurable_const, And.left, MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_le
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
replace H : (μ.restrict s) {x | f x ≤ ⨍ a in s, f a ∂μ} = 0 := by
    rwa [restrict_apply₀, inter_comm]
    exact AEStronglyMeasurable.nullMeasurableSet_le hf.1 aestronglyMeasurable_const
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))

Tactic:
haveI := Fact.mk hμ₁.lt_top
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ False

Tactic:
(integral_sub_average (μ.restrict s) f).not_gt ?_

Premises used: Eq.not_gt, MeasureTheory.Measure.restrict, MeasureTheory.integral_sub_average
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
refine : LT.lt (α := ℝ) 0 (∫ (x : α) in s, f x - ⨍ (a : α) in s, f a ∂μ ∂μ)
⊢ False

Tactic:
refine (integral_sub_average (μ.restrict s) f).not_gt ?_

Premises used: Eq.not_gt, MeasureTheory.Measure.restrict, MeasureTheory.integral_sub_average
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ LT.lt (α := ℝ) 0 (∫ (x : α) in s, f x - ⨍ (a : α) in s, f a ∂μ ∂μ)

Tactic:
(setIntegral_pos_iff_support_of_nonneg_ae ?_ ?_).2 ?_

Premises used: Iff.mpr, MeasureTheory.setIntegral_pos_iff_support_of_nonneg_ae
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
refine_1 : (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ f x - ⨍ (a : α) in s, f a ∂μ
refine_2 : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x - ⨍ (a : α) in s, f a ∂μ) s μ
refine_3 :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((support (M := ℝ) fun (x : α) ↦ f x - ⨍ (a : α) in s, f a ∂μ) ∩ s) : ℝ≥0∞)
⊢ LT.lt (α := ℝ) 0 (∫ (x : α) in s, f x - ⨍ (a : α) in s, f a ∂μ ∂μ)

Tactic:
refine (setIntegral_pos_iff_support_of_nonneg_ae ?_ ?_).2 ?_

Premises used: Iff.mpr, MeasureTheory.setIntegral_pos_iff_support_of_nonneg_ae
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ f x - ⨍ (a : α) in s, f a ∂μ

Tactic:
measure_mono_null (fun x hx ↦ ?_) H

Premises used: Set.Mem, Filter.Eventually, setOf, MeasureTheory.measure_mono_null, Filter.EventuallyLE
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
refine_1 :
  ∀ (x : α)
    (hx :
      Membership.mem (γ := Set α)
        {x : α | (fun (x : α) ↦ LE.le (α := ℝ) (0 x) ((fun (x : α) ↦ f x - ⨍ (a : α) in s, f a ∂μ) x)) x}ᶜ x),
    Membership.mem (γ := Set α) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} x
⊢ (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ f x - ⨍ (a : α) in s, f a ∂μ

Tactic:
refine measure_mono_null (fun x hx ↦ ?_) H

Premises used: MeasureTheory.measure_mono_null
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
x : α
hx :
  Membership.mem (γ := Set α)
    {x : α | (fun (x : α) ↦ LE.le (α := ℝ) (0 x) ((fun (x : α) ↦ f x - ⨍ (a : α) in s, f a ∂μ) x)) x}ᶜ x
⊢ f x < ⨍ (a : α) in s, f a ∂μ

Tactic:
simp only [Pi.zero_apply, sub_nonneg, mem_compl_iff, mem_setOf_eq, not_le] at hx

Premises used: not_le, Pi.zero_apply, Set.mem_setOf_eq, sub_nonneg, Set.mem_compl_iff