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
μ : Measure α
inst_2 : IsFiniteMeasure μ
f : α → E
hμ : μ = 0
inl :
  HSMul.hSMul (β := E) (Measure.real.{u_1} (α := α) (m := m0) 0 univ) (⨍ (x : α), f x ∂0) =
    @integral _ _ _ _ m0 0 fun (x : α) ↦ f x
inl₁ : HSMul.hSMul (β := E) (Measure.real.{u_1} (α := α) (m := m0) 0 univ) (⨍ (x : α), f x ∂0) = 0
inl₂ : HSMul.hSMul (β := E) (Measure.real.{u_1} (α := α) (m := m0) 0 univ) 0 = 0
inl₃ inl₄ : Eq.{u_2 + 1} (α := E) 0 0
⊢ HSMul.hSMul (β := E) (μ.real univ) (⨍ (x : α), f x ∂μ) = ∫ (x : α), f x ∂μ

Tactic:
rw [hμ, integral_zero_measure, average_zero_measure, smul_zero]

Premises used: MeasureTheory.average_zero_measure, smul_zero, MeasureTheory.integral_zero_measure
-- 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 : IsFiniteMeasure μ
f : α → E
hμ : μ ≠ 0
inr : μ.real univ ≠ 0
⊢ HSMul.hSMul (β := E) (μ.real univ) (⨍ (x : α), f x ∂μ) = ∫ (x : α), f x ∂μ

Tactic:
rw [average_eq, smul_inv_smul₀]

Premises used: smul_inv_smul₀, MeasureTheory.average_eq
-- 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 : IsFiniteMeasure μ
f : α → E
hμ : μ ≠ 0
⊢ μ.real univ ≠ 0

Tactic:
(ENNReal.toReal_pos ?_ <| measure_ne_top _ _).ne'

Premises used: MeasureTheory.Measure.real, MeasureTheory.measure_ne_top, ENNReal.toReal_pos, LT.lt.ne'
-- 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 : IsFiniteMeasure μ
f : α → E
hμ : μ ≠ 0
inr : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ.real univ ≠ 0

Tactic:
refine (ENNReal.toReal_pos ?_ <| measure_ne_top _ _).ne'

Premises used: MeasureTheory.measure_ne_top, ENNReal.toReal_pos, LT.lt.ne'
-- 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 : IsFiniteMeasure μ
f : α → E
hμ : μ ≠ 0
inr : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
inr₁ inr₂ inr₃ inr₄ : ¬μ = 0
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rwa [Ne, measure_univ_eq_zero]

Premises used: Ne, MeasureTheory.Measure.measure_univ_eq_zero
-- 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
s : Set α
rw :
  HSMul.hSMul (β := E) ((μ.restrict s).real univ)⁻¹ (∫ (x : α) in s, f x ∂μ) =
    HSMul.hSMul (β := E) (μ.real s)⁻¹ (∫ (x : α) in s, f x ∂μ)
rw₁ rw₂ :
  HSMul.hSMul (β := E) (μ.real s)⁻¹ (∫ (x : α) in s, f x ∂μ) =
    HSMul.hSMul (β := E) (μ.real s)⁻¹ (∫ (x : α) in s, f x ∂μ)
⊢ ⨍ (x : α) in s, f x ∂μ = HSMul.hSMul (β := E) (μ.real s)⁻¹ (∫ (x : α) in s, f x ∂μ)

Tactic:
rw [average_eq, measureReal_restrict_apply_univ]

Premises used: MeasureTheory.measureReal_restrict_apply_univ, MeasureTheory.average_eq
-- 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
s : Set α
⊢ Eq.{u_2 + 1} (α := E) (⨍ (x : α) in s, f x ∂μ)
    (∫ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s))

Tactic:
simp only [average_eq', restrict_apply_univ]

Premises used: MeasureTheory.Measure.restrict_apply_univ, MeasureTheory.average_eq'
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
f g : α → E
h : f =ᶠ[ae μ] g
⊢ Eq.{u_2 + 1} (α := E) (⨍ (x : α), f x ∂μ) (⨍ (x : α), g x ∂μ)

Tactic:
simp only [average_eq, integral_congr_ae h]

Premises used: MeasureTheory.integral_congr_ae, MeasureTheory.average_eq
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
s t : Set α
f : α → E
h : s =ᶠ[ae μ] t
⊢ Eq.{u_2 + 1} (α := E) (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ)

Tactic:
simp only [setAverage_eq, setIntegral_congr_set h, measureReal_congr h]

Premises used: MeasureTheory.setAverage_eq, MeasureTheory.measureReal_congr, MeasureTheory.setIntegral_congr_set
-- 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 g : α → E
hs : MeasurableSet s
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
⊢ Eq.{u_2 + 1} (α := E) (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in s, g x ∂μ)

Tactic:
simp only [average_eq, setIntegral_congr_ae hs h]

Premises used: MeasureTheory.setIntegral_congr_ae, MeasureTheory.average_eq
-- 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 : IsFiniteMeasure μ
ν : Measure α
inst_3 : IsFiniteMeasure ν
f : α → E
hμ : Integrable f μ
hν : Integrable f ν
simp : ⨍ (x : α), f x ∂(μ + ν) = HSMul.hSMul (β := E) (μ.real univ + ν.real univ)⁻¹ (∫ (x : α), f x ∂(μ + ν))
⊢ ⨍ (x : α), f x ∂(μ + ν) =
    HSMul.hSMul (β := E) (μ.real univ / (μ.real univ + ν.real univ)) (⨍ (x : α), f x ∂μ) +
      HSMul.hSMul (β := E) (ν.real univ / (μ.real univ + ν.real univ)) (⨍ (x : α), f x ∂ν)

Tactic:
simp only [div_eq_inv_mul, mul_smul, measure_smul_average, ← smul_add,
    ← integral_add_measure hμ hν]

Premises used: MeasureTheory.integral_add_measure, MeasureTheory.measure_smul_average, div_eq_inv_mul, SemigroupAction.mul_smul, smul_add
-- 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 : IsFiniteMeasure μ
ν : Measure α
inst_3 : IsFiniteMeasure ν
f : α → E
hμ : Integrable f μ
hν : Integrable f ν
rw :
  HSMul.hSMul (β := E) ((μ + ν).real univ)⁻¹ (∫ (x : α), f x ∂(μ + ν)) =
    HSMul.hSMul (β := E) (μ.real univ + ν.real univ)⁻¹ (∫ (x : α), f x ∂(μ + ν))
rw₁ rw₂ :
  HSMul.hSMul (β := E) (μ.real univ + ν.real univ)⁻¹ (∫ (x : α), f x ∂(μ + ν)) =
    HSMul.hSMul (β := E) (μ.real univ + ν.real univ)⁻¹ (∫ (x : α), f x ∂(μ + ν))
⊢ ⨍ (x : α), f x ∂(μ + ν) = HSMul.hSMul (β := E) (μ.real univ + ν.real univ)⁻¹ (∫ (x : α), f x ∂(μ + ν))

Tactic:
rw [average_eq, measureReal_add_apply]

Premises used: MeasureTheory.measureReal_add_apply, MeasureTheory.average_eq
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
μ : Measure α
inst_5 : CompleteSpace E
f : α → E
g : α → F
hfi : Integrable f μ
hgi : Integrable g μ
⊢ Eq (α := E × F) (⨍ (x : α), (f x, g x) ∂μ) (⨍ (x : α), f x ∂μ, ⨍ (x : α), g x ∂μ)

Tactic:
integral_pair hfi.to_average hgi.to_average

Premises used: MeasureTheory.average, MeasureTheory.Integrable.to_average, integral_pair
-- 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
s : Set α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥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
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
f : α → E
s : Set α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
rw :
  HSMul.hSMul (β := E) (μ.real s) (⨍ (x : α) in s, f x ∂μ) =
    HSMul.hSMul (β := E) ((μ.restrict s).real univ) (⨍ (x : α) in s, f x ∂μ)
rw₁ rw₂ :
  HSMul.hSMul (β := E) (μ.real s) (⨍ (x : α) in s, f x ∂μ) = HSMul.hSMul (β := E) (μ.real s) (⨍ (x : α) in s, f x ∂μ)
⊢ HSMul.hSMul (β := E) (μ.real s) (⨍ (x : α) in s, f x ∂μ) = ∫ (x : α) in s, f x ∂μ

Tactic:
rw [← measure_smul_average, measureReal_restrict_apply_univ]

Premises used: MeasureTheory.measure_smul_average, MeasureTheory.measureReal_restrict_apply_univ
-- 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
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
htμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
⊢ Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))

Tactic:
haveI := Fact.mk hsμ.lt_top
-- 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
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
htμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞))

Tactic:
haveI := Fact.mk htμ.lt_top
-- 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
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
htμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞))
rw :
  ⨍ (x : α), f x ∂(μ.restrict s + μ.restrict t) =
    HSMul.hSMul (β := E) (μ.real s / (μ.real s + μ.real t)) (⨍ (x : α) in s, f x ∂μ) +
      HSMul.hSMul (β := E) (μ.real t / (μ.real s + μ.real t)) (⨍ (x : α) in t, f x ∂μ)
rw₁ :
  HSMul.hSMul (β := E) ((μ.restrict s).real univ / ((μ.restrict s).real univ + (μ.restrict t).real univ))
        (⨍ (x : α) in s, f x ∂μ) +
      HSMul.hSMul (β := E) ((μ.restrict t).real univ / ((μ.restrict s).real univ + (μ.restrict t).real univ))
        (⨍ (x : α) in t, f x ∂μ) =
    HSMul.hSMul (β := E) (μ.real s / (μ.real s + μ.real t)) (⨍ (x : α) in s, f x ∂μ) +
      HSMul.hSMul (β := E) (μ.real t / (μ.real s + μ.real t)) (⨍ (x : α) in t, f x ∂μ)
rw₂ :
  HSMul.hSMul (β := E) (μ.real s / (μ.real s + (μ.restrict t).real univ)) (⨍ (x : α) in s, f x ∂μ) +
      HSMul.hSMul (β := E) ((μ.restrict t).real univ / (μ.real s + (μ.restrict t).real univ)) (⨍ (x : α) in t, f x ∂μ) =
    HSMul.hSMul (β := E) (μ.real s / (μ.real s + μ.real t)) (⨍ (x : α) in s, f x ∂μ) +
      HSMul.hSMul (β := E) (μ.real t / (μ.real s + μ.real t)) (⨍ (x : α) in t, f x ∂μ)
rw₃ rw₄ :
  HSMul.hSMul (β := E) (μ.real s / (μ.real s + μ.real t)) (⨍ (x : α) in s, f x ∂μ) +
      HSMul.hSMul (β := E) (μ.real t / (μ.real s + μ.real t)) (⨍ (x : α) in t, f x ∂μ) =
    HSMul.hSMul (β := E) (μ.real s / (μ.real s + μ.real t)) (⨍ (x : α) in s, f x ∂μ) +
      HSMul.hSMul (β := E) (μ.real t / (μ.real s + μ.real t)) (⨍ (x : α) in t, f x ∂μ)
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ =
    HSMul.hSMul (β := E) (μ.real s / (μ.real s + μ.real t)) (⨍ (x : α) in s, f x ∂μ) +
      HSMul.hSMul (β := E) (μ.real t / (μ.real s + μ.real t)) (⨍ (x : α) in t, f x ∂μ)

Tactic:
rw [restrict_union₀ hd ht, average_add_measure hfs hft, measureReal_restrict_apply_univ,
    measureReal_restrict_apply_univ]

Premises used: MeasureTheory.Measure.restrict_union₀, MeasureTheory.average_add_measure, MeasureTheory.measureReal_restrict_apply_univ
-- 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
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hs₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ht₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
hsμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
htμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
⊢ 0 < μ.real s

Tactic:
replace hs₀ : 0 < μ.real s := ENNReal.toReal_pos hs₀ hsμ
-- 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
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
ht₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
hsμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
htμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hs₀ : 0 < μ.real s
⊢ 0 < μ.real t

Tactic:
replace ht₀ : 0 < μ.real t := ENNReal.toReal_pos ht₀ htμ
-- 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
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
htμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hs₀ : 0 < μ.real s
ht₀ : 0 < μ.real t
⊢ Membership.mem (γ := Set E) (openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ))
    (⨍ (x : α) in s ∪ t, f x ∂μ)

Tactic:
mem_openSegment_iff_div.mpr
    ⟨μ.real s, μ.real t, hs₀, ht₀, (average_union hd ht hsμ htμ hfs hft).symm⟩

Premises used: Iff.mpr, Set.Mem, MeasureTheory.Measure.real, And.intro, Exists.intro, mem_openSegment_iff_div, Eq.symm, MeasureTheory.average_union
-- 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
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
htμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hs₀ : 0 < μ.real s
ht₀ : 0 < μ.real t
⊢ Membership.mem (γ := Set E) (openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ))
    (⨍ (x : α) in s ∪ t, f x ∂μ)

Tactic:
exact mem_openSegment_iff_div.mpr
    ⟨μ.real s, μ.real t, hs₀, ht₀, (average_union hd ht hsμ htμ hfs hft).symm⟩

Premises used: Iff.mpr, MeasureTheory.Measure.real, And.intro, Exists.intro, mem_openSegment_iff_div, Eq.symm, MeasureTheory.average_union
-- 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
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
htμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
pos :
  ∀ (hse : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    Membership.mem (γ := Set E) [⨍ (x : α) in s, f x ∂μ -[ℝ] ⨍ (x : α) in t, f x ∂μ] (⨍ (x : α) in s ∪ t, f x ∂μ)
neg :
  ∀ (hse : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    Membership.mem (γ := Set E) [⨍ (x : α) in s, f x ∂μ -[ℝ] ⨍ (x : α) in t, f x ∂μ] (⨍ (x : α) in s ∪ t, f x ∂μ)
⊢ Membership.mem (γ := Set E) [⨍ (x : α) in s, f x ∂μ -[ℝ] ⨍ (x : α) in t, f x ∂μ] (⨍ (x : α) in s ∪ t, f x ∂μ)

Tactic:
by_cases hse : μ s = 0

Premises used: DFunLike.coe
-- 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
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
htμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hse : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ s =ᶠ[ae μ] ∅

Tactic:
rw [← ae_eq_empty] at hse

Premises used: MeasureTheory.ae_eq_empty
-- 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
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
htμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hse : s =ᶠ[ae μ] ∅
pos : Membership.mem (γ := Set E) [⨍ (x : α) in s, f x ∂μ -[ℝ] ⨍ (x : α) in t, f x ∂μ] (⨍ (x : α) in t, f x ∂μ)
⊢ Membership.mem (γ := Set E) [⨍ (x : α) in s, f x ∂μ -[ℝ] ⨍ (x : α) in t, f x ∂μ] (⨍ (x : α) in s ∪ t, f x ∂μ)

Tactic:
rw [restrict_congr_set (hse.union EventuallyEq.rfl), empty_union]

Premises used: MeasureTheory.Measure.restrict_congr_set, Set.empty_union, Filter.EventuallyEq.union, Filter.EventuallyEq.rfl
-- 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
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
htμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hse : s =ᶠ[ae μ] ∅
⊢ Membership.mem (γ := Set E) [⨍ (x : α) in s, f x ∂μ -[ℝ] ⨍ (x : α) in t, f x ∂μ] (⨍ (x : α) in t, f x ∂μ)

Tactic:
right_mem_segment _ _ _

Premises used: Set.Mem, right_mem_segment
-- 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
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
htμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hse : s =ᶠ[ae μ] ∅
⊢ Membership.mem (γ := Set E) [⨍ (x : α) in s, f x ∂μ -[ℝ] ⨍ (x : α) in t, f x ∂μ] (⨍ (x : α) in t, f x ∂μ)

Tactic:
exact right_mem_segment _ _ _

Premises used: right_mem_segment
-- 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
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
htμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hse : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Membership.mem (γ := Set E) [⨍ (x : α) in s, f x ∂μ -[ℝ] ⨍ (x : α) in t, f x ∂μ] (⨍ (x : α) in s ∪ t, f x ∂μ)

Tactic:
mem_segment_iff_div.mpr
        ⟨μ.real s, μ.real t, ENNReal.toReal_nonneg, ENNReal.toReal_nonneg, ?_,
          (average_union hd ht hsμ htμ hfs hft).symm⟩

Premises used: Iff.mpr, Set.Mem, MeasureTheory.Measure.real, ENNReal.toReal_nonneg, And.intro, Exists.intro, mem_segment_iff_div, Eq.symm, MeasureTheory.average_union
-- 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
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
htμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hse : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
neg : 0 < μ.real s + μ.real t
⊢ Membership.mem (γ := Set E) [⨍ (x : α) in s, f x ∂μ -[ℝ] ⨍ (x : α) in t, f x ∂μ] (⨍ (x : α) in s ∪ t, f x ∂μ)

Tactic:
refine
      mem_segment_iff_div.mpr
        ⟨μ.real s, μ.real t, ENNReal.toReal_nonneg, ENNReal.toReal_nonneg, ?_,
          (average_union hd ht hsμ htμ hfs hft).symm⟩

Premises used: Iff.mpr, MeasureTheory.Measure.real, ENNReal.toReal_nonneg, And.intro, Exists.intro, mem_segment_iff_div, Eq.symm, MeasureTheory.average_union
-- 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
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
htμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hse : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ 0 < μ.real s

Tactic:
ENNReal.toReal_pos hse hsμ

Premises used: MeasureTheory.Measure.real, ENNReal.toReal_pos
-- 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
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
htμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hse : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ.real s ≤ μ.real s + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t)

Tactic:
le_add_of_nonneg_right ENNReal.toReal_nonneg

Premises used: ENNReal.toReal_nonneg, le_add_of_nonneg_right
-- 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
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
htμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hse : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ 0 < μ.real s + μ.real t

Tactic:
calc
      0 < μ.real s := ENNReal.toReal_pos hse hsμ
      _ ≤ _ := le_add_of_nonneg_right ENNReal.toReal_nonneg

Premises used: MeasureTheory.Measure.real, ENNReal.toReal_nonneg, ENNReal.toReal_pos, le_add_of_nonneg_right
-- 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 : IsFiniteMeasure μ
f : α → E
s : Set α
hs : NullMeasurableSet s μ
hs₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hsc₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hfi : Integrable f μ
⊢ Membership.mem (γ := Set E) (openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in sᶜ, f x ∂μ)) (⨍ (x : α), f x ∂μ)

Tactic:
simpa only [union_compl_self, restrict_univ] using
    average_union_mem_openSegment aedisjoint_compl_right hs.compl hs₀ hsc₀ (measure_ne_top _ _)
      (measure_ne_top _ _) hfi.integrableOn hfi.integrableOn

Premises used: MeasureTheory.aedisjoint_compl_right, MeasureTheory.NullMeasurableSet.compl, MeasureTheory.measure_ne_top, Set.union_compl_self, MeasureTheory.Integrable.integrableOn, MeasureTheory.average_union_mem_openSegment, MeasureTheory.Measure.restrict_univ