awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
t : Set α
f : α → E
inst_3 : IsFiniteMeasure μ
hs : Convex ℝ s
h0 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
ht : ⨍ (x : α) in t, f x ∂μ ∈ interior s
h0₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ t) : ℝ≥0∞) (0 : ℝ≥0∞)
hfs₁ : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi₁ : Integrable f μ
⊢ ⨍ (x : α) in t, f x ∂μ ∈ interior s

Tactic:
rw [← measure_toMeasurable] at h0

Premises used: MeasureTheory.measure_toMeasurable
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
t : Set α
f : α → E
inst_3 : IsFiniteMeasure μ
hs : Convex ℝ s
h0 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ t) : ℝ≥0∞) (0 : ℝ≥0∞)
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
ht : ⨍ (x : α) in t, f x ∂μ ∈ interior s
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
t : Set α
f : α → E
inst_3 : IsFiniteMeasure μ
hs : Convex ℝ s
h0 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ t) : ℝ≥0∞) (0 : ℝ≥0∞)
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
ht : ⨍ (x : α) in t, f x ∂μ ∈ interior s
⊢ ⨍ (x : α) in toMeasurable μ t, f x ∂μ ∈ interior s

Tactic:
rw [← restrict_toMeasurable (by finiteness)] at ht

Premises used: MeasureTheory.Measure.restrict_toMeasurable
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
t : Set α
f : α → E
inst_3 : IsFiniteMeasure μ
hs : Convex ℝ s
h0 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ t) : ℝ≥0∞) (0 : ℝ≥0∞)
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
ht : ⨍ (x : α) in toMeasurable μ t, f x ∂μ ∈ interior s
pos :
  ∀ (h0' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ t)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    ⨍ (x : α), f x ∂μ ∈ interior s
neg :
  ∀ (h0' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ t)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    ⨍ (x : α), f x ∂μ ∈ interior s
⊢ ⨍ (x : α), f x ∂μ ∈ interior s

Tactic:
by_cases h0' : μ (toMeasurable μ t)ᶜ = 0

Premises used: Compl.compl, MeasureTheory.toMeasurable, DFunLike.coe
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
t : Set α
f : α → E
inst_3 : IsFiniteMeasure μ
hs : Convex ℝ s
h0 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ t) : ℝ≥0∞) (0 : ℝ≥0∞)
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
ht : ⨍ (x : α) in toMeasurable μ t, f x ∂μ ∈ interior s
h0' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ t)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ toMeasurable μ t =ᶠ[ae μ] univ

Tactic:
rw [← ae_eq_univ] at h0'

Premises used: MeasureTheory.ae_eq_univ
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
t : Set α
f : α → E
inst_3 : IsFiniteMeasure μ
hs : Convex ℝ s
h0 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ t) : ℝ≥0∞) (0 : ℝ≥0∞)
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
ht : ⨍ (x : α) in toMeasurable μ t, f x ∂μ ∈ interior s
h0' : toMeasurable μ t =ᶠ[ae μ] univ
pos :
  ∀ (ht : ⨍ (x : α) in univ, f x ∂μ ∈ interior s) (h0' : toMeasurable μ t =ᶠ[ae μ] univ), ⨍ (x : α), f x ∂μ ∈ interior s
pos₁ pos₂ pos₃ pos₄ :
  ∀ (ht : ⨍ (x : α), f x ∂μ ∈ interior s) (h0' : toMeasurable μ t =ᶠ[ae μ] univ), ⨍ (x : α), f x ∂μ ∈ interior s
⊢ ⨍ (x : α), f x ∂μ ∈ interior s

Tactic:
rwa [restrict_congr_set h0', restrict_univ] at ht

Premises used: MeasureTheory.Measure.restrict_congr_set, MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
t : Set α
f : α → E
inst_3 : IsFiniteMeasure μ
hs : Convex ℝ s
h0 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ t) : ℝ≥0∞) (0 : ℝ≥0∞)
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
ht : ⨍ (x : α) in toMeasurable μ t, f x ∂μ ∈ interior s
h0' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ t)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ t)ᶜ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
t : Set α
f : α → E
inst_3 : IsFiniteMeasure μ
hs : Convex ℝ s
h0 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ t) : ℝ≥0∞) (0 : ℝ≥0∞)
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
ht : ⨍ (x : α) in toMeasurable μ t, f x ∂μ ∈ interior s
h0' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ t)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ⨍ (x : α), f x ∂μ ∈ interior s

Tactic:
exact hs.openSegment_interior_closure_subset_interior ht
      (hs.set_average_mem_closure h0' (by finiteness) (ae_restrict_of_ae hfs) hfi.integrableOn)
      (average_mem_openSegment_compl_self (measurableSet_toMeasurable μ t).nullMeasurableSet h0
        h0' hfi)

Premises used: MeasureTheory.average_mem_openSegment_compl_self, MeasurableSet.nullMeasurableSet, MeasureTheory.ae_restrict_of_ae, Convex.set_average_mem_closure, MeasureTheory.measurableSet_toMeasurable, MeasureTheory.Integrable.integrableOn, Convex.openSegment_interior_closure_subset_interior
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsFiniteMeasure μ
hs : StrictConvex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
t : Set α
ht : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsFiniteMeasure μ
hs : StrictConvex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
⊢ ∀ {t : Set α}, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) → ⨍ (x : α) in t, f x ∂μ ∈ s

Tactic:
have : ∀ {t}, μ t ≠ 0 → (⨍ x in t, f x ∂μ) ∈ s := fun ht =>
    hs.convex.set_average_mem hsc ht (by finiteness) (ae_restrict_of_ae hfs) hfi.integrableOn
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsFiniteMeasure μ
hs : StrictConvex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
this : ∀ {t : Set α}, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) → ⨍ (x : α) in t, f x ∂μ ∈ s
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ ⨍ (x : α), f x ∂μ ∈ interior s

Tactic:
(ae_eq_const_or_exists_average_ne_compl hfi).imp_right ?_

Premises used: ae_eq_const_or_exists_average_ne_compl, Or.imp_right
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsFiniteMeasure μ
hs : StrictConvex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
this : ∀ {t : Set α}, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) → ⨍ (x : α) in t, f x ∂μ ∈ s
refine :
  (∃ (t : Set α),
      MeasurableSet t ∧
        Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∧
          Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ∧
            Ne.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)) →
    ⨍ (x : α), f x ∂μ ∈ interior s
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ ⨍ (x : α), f x ∂μ ∈ interior s

Tactic:
refine (ae_eq_const_or_exists_average_ne_compl hfi).imp_right ?_

Premises used: ae_eq_const_or_exists_average_ne_compl, Or.imp_right
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsFiniteMeasure μ
hs : StrictConvex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
this : ∀ {t : Set α}, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) → ⨍ (x : α) in t, f x ∂μ ∈ s
t : Set α
hm : MeasurableSet t
h₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h₀' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hne : Ne.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
⊢ ⨍ (x : α), f x ∂μ ∈ interior s

Tactic:
hs.openSegment_subset (this h₀) (this h₀') hne
      (average_mem_openSegment_compl_self hm.nullMeasurableSet h₀ h₀' hfi)

Premises used: MeasureTheory.average_mem_openSegment_compl_self, MeasurableSet.nullMeasurableSet, StrictConvex.openSegment_subset
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsFiniteMeasure μ
hs : StrictConvex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
this : ∀ {t : Set α}, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) → ⨍ (x : α) in t, f x ∂μ ∈ s
t : Set α
hm : MeasurableSet t
h₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h₀' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hne : Ne.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
⊢ ⨍ (x : α), f x ∂μ ∈ interior s

Tactic:
exact
    hs.openSegment_subset (this h₀) (this h₀') hne
      (average_mem_openSegment_compl_self hm.nullMeasurableSet h₀ h₀' hfi)

Premises used: MeasureTheory.average_mem_openSegment_compl_self, MeasurableSet.nullMeasurableSet, StrictConvex.openSegment_subset
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
g : E → ℝ
inst_3 : IsFiniteMeasure μ
hg : StrictConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
t : Set α
ht : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
g : E → ℝ
inst_3 : IsFiniteMeasure μ
hg : StrictConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
⊢ ∀ {t : Set α},
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
      ⨍ (x : α) in t, f x ∂μ ∈ s ∧ g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ

Tactic:
have : ∀ {t}, μ t ≠ 0 → (⨍ x in t, f x ∂μ) ∈ s ∧ g (⨍ x in t, f x ∂μ) ≤ ⨍ x in t, g (f x) ∂μ :=
    fun ht =>
    hg.convexOn.set_average_mem_epigraph hgc hsc ht (by finiteness) (ae_restrict_of_ae hfs)
      hfi.integrableOn hgi.integrableOn
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
g : E → ℝ
inst_3 : IsFiniteMeasure μ
hg : StrictConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
this :
  ∀ {t : Set α},
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
      ⨍ (x : α) in t, f x ∂μ ∈ s ∧ g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ g (⨍ (x : α), f x ∂μ) < ⨍ (x : α), g (f x) ∂μ

Tactic:
(ae_eq_const_or_exists_average_ne_compl hfi).imp_right ?_

Premises used: ae_eq_const_or_exists_average_ne_compl, Or.imp_right
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
g : E → ℝ
inst_3 : IsFiniteMeasure μ
hg : StrictConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
this :
  ∀ {t : Set α},
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
      ⨍ (x : α) in t, f x ∂μ ∈ s ∧ g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ
refine :
  (∃ (t : Set α),
      MeasurableSet t ∧
        Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) ∧
          Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ∧
            Ne.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)) →
    g (⨍ (x : α), f x ∂μ) < ⨍ (x : α), g (f x) ∂μ
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ g (⨍ (x : α), f x ∂μ) < ⨍ (x : α), g (f x) ∂μ

Tactic:
refine (ae_eq_const_or_exists_average_ne_compl hfi).imp_right ?_

Premises used: ae_eq_const_or_exists_average_ne_compl, Or.imp_right
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
g : E → ℝ
inst_3 : IsFiniteMeasure μ
hg : StrictConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
this :
  ∀ {t : Set α},
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
      ⨍ (x : α) in t, f x ∂μ ∈ s ∧ g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ
t : Set α
hm : MeasurableSet t
h₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h₀' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hne : Ne.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
rcases :
  ∀ (a b : ℝ) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1)
    (h_avg :
      HSMul.hSMul (β := E × ℝ) a (⨍ (x : α) in t, (f x, (g ∘ f) x) ∂μ) +
          HSMul.hSMul (β := E × ℝ) b (⨍ (x : α) in tᶜ, (f x, (g ∘ f) x) ∂μ) =
        ⨍ (x : α), (f x, (g ∘ f) x) ∂μ),
    g (⨍ (x : α), f x ∂μ) < ⨍ (x : α), g (f x) ∂μ
⊢ g (⨍ (x : α), f x ∂μ) < ⨍ (x : α), g (f x) ∂μ

Tactic:
rcases average_mem_openSegment_compl_self hm.nullMeasurableSet h₀ h₀' (hfi.prodMk hgi) with
    ⟨a, b, ha, hb, hab, h_avg⟩

Premises used: MeasureTheory.average_mem_openSegment_compl_self, MeasurableSet.nullMeasurableSet, MeasureTheory.Integrable.prodMk
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
g : E → ℝ
inst_3 : IsFiniteMeasure μ
hg : StrictConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
this :
  ∀ {t : Set α},
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
      ⨍ (x : α) in t, f x ∂μ ∈ s ∧ g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ
t : Set α
hm : MeasurableSet t
h₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h₀' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hne : Ne.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h_avg :
  HSMul.hSMul (β := E × ℝ) a (⨍ (x : α) in t, (f x, (g ∘ f) x) ∂μ) +
      HSMul.hSMul (β := E × ℝ) b (⨍ (x : α) in tᶜ, (f x, (g ∘ f) x) ∂μ) =
    ⨍ (x : α), (f x, (g ∘ f) x) ∂μ
⊢ HSMul.hSMul (β := E) a (⨍ (x : α) in t, f x ∂μ) + HSMul.hSMul (β := E) b (⨍ (x : α) in tᶜ, f x ∂μ) =
      ⨍ (x : α), f x ∂μ ∧
    HSMul.hSMul (β := ℝ) a (⨍ (x : α) in t, (g ∘ f) x ∂μ) + HSMul.hSMul (β := ℝ) b (⨍ (x : α) in tᶜ, (g ∘ f) x ∂μ) =
      ⨍ (x : α), (g ∘ f) x ∂μ

Tactic:
rw [average_pair hfi hgi, average_pair hfi.integrableOn hgi.integrableOn,
    average_pair hfi.integrableOn hgi.integrableOn, Prod.smul_mk,
    Prod.smul_mk, Prod.mk_add_mk, Prod.mk_inj] at h_avg

Premises used: Prod.mk_add_mk, Prod.mk_inj, MeasureTheory.average_pair, MeasureTheory.Integrable.integrableOn, Prod.smul_mk
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
g : E → ℝ
inst_3 : IsFiniteMeasure μ
hg : StrictConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
this :
  ∀ {t : Set α},
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
      ⨍ (x : α) in t, f x ∂μ ∈ s ∧ g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ
t : Set α
hm : MeasurableSet t
h₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h₀' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hne : Ne.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h_avg :
  HSMul.hSMul (β := E) a (⨍ (x : α) in t, f x ∂μ) + HSMul.hSMul (β := E) b (⨍ (x : α) in tᶜ, f x ∂μ) =
      ⨍ (x : α), f x ∂μ ∧
    HSMul.hSMul (β := ℝ) a (⨍ (x : α) in t, g (f x) ∂μ) + HSMul.hSMul (β := ℝ) b (⨍ (x : α) in tᶜ, g (f x) ∂μ) =
      ⨍ (x : α), g (f x) ∂μ
rw :
  g (HSMul.hSMul (β := E) a (⨍ (x : α) in t, f x ∂μ) + HSMul.hSMul (β := E) b (⨍ (x : α) in tᶜ, f x ∂μ)) <
    HSMul.hSMul (β := ℝ) a (⨍ (x : α) in t, g (f x) ∂μ) + HSMul.hSMul (β := ℝ) b (⨍ (x : α) in tᶜ, g (f x) ∂μ)
⊢ g (⨍ (x : α), f x ∂μ) < ⨍ (x : α), g (f x) ∂μ

Tactic:
rw [← h_avg.1, ← h_avg.2]

Premises used: And.right, And.left
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
g : E → ℝ
inst_3 : IsFiniteMeasure μ
hg : StrictConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
this :
  ∀ {t : Set α},
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
      ⨍ (x : α) in t, f x ∂μ ∈ s ∧ g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ
t : Set α
hm : MeasurableSet t
h₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h₀' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hne : Ne.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h_avg :
  HSMul.hSMul (β := E) a (⨍ (x : α) in t, f x ∂μ) + HSMul.hSMul (β := E) b (⨍ (x : α) in tᶜ, f x ∂μ) =
      ⨍ (x : α), f x ∂μ ∧
    HSMul.hSMul (β := ℝ) a (⨍ (x : α) in t, g (f x) ∂μ) + HSMul.hSMul (β := ℝ) b (⨍ (x : α) in tᶜ, g (f x) ∂μ) =
      ⨍ (x : α), g (f x) ∂μ
⊢ g (HSMul.hSMul (β := E) a (⨍ (x : α) in t, f x ∂μ) + HSMul.hSMul (β := E) b (⨍ (x : α) in tᶜ, f x ∂μ)) <
    a * g (⨍ (x : α) in t, f x ∂μ) + b * g (⨍ (x : α) in tᶜ, f x ∂μ)

Tactic:
hg.2 (this h₀).1 (this h₀').1 hne ha hb hab

Premises used: And.right, And.left
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
g : E → ℝ
inst_3 : IsFiniteMeasure μ
hg : StrictConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
this :
  ∀ {t : Set α},
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
      ⨍ (x : α) in t, f x ∂μ ∈ s ∧ g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ
t : Set α
hm : MeasurableSet t
h₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h₀' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hne : Ne.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h_avg :
  HSMul.hSMul (β := E) a (⨍ (x : α) in t, f x ∂μ) + HSMul.hSMul (β := E) b (⨍ (x : α) in tᶜ, f x ∂μ) =
      ⨍ (x : α), f x ∂μ ∧
    HSMul.hSMul (β := ℝ) a (⨍ (x : α) in t, g (f x) ∂μ) + HSMul.hSMul (β := ℝ) b (⨍ (x : α) in tᶜ, g (f x) ∂μ) =
      ⨍ (x : α), g (f x) ∂μ
h₁ : g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ
h₂ : g (⨍ (x : α) in tᶜ, f x ∂μ) ≤ ⨍ (x : α) in tᶜ, g (f x) ∂μ
⊢ a * g (⨍ (x : α) in t, f x ∂μ) + b * g (⨍ (x : α) in tᶜ, f x ∂μ) ≤
    a * ⨍ (x : α) in t, g (f x) ∂μ + b * ⨍ (x : α) in tᶜ, g (f x) ∂μ

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
g : E → ℝ
inst_3 : IsFiniteMeasure μ
hg : StrictConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
this :
  ∀ {t : Set α},
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
      ⨍ (x : α) in t, f x ∂μ ∈ s ∧ g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ
t : Set α
hm : MeasurableSet t
h₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h₀' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hne : Ne.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h_avg :
  HSMul.hSMul (β := E) a (⨍ (x : α) in t, f x ∂μ) + HSMul.hSMul (β := E) b (⨍ (x : α) in tᶜ, f x ∂μ) =
      ⨍ (x : α), f x ∂μ ∧
    HSMul.hSMul (β := ℝ) a (⨍ (x : α) in t, g (f x) ∂μ) + HSMul.hSMul (β := ℝ) b (⨍ (x : α) in tᶜ, g (f x) ∂μ) =
      ⨍ (x : α), g (f x) ∂μ
⊢ g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ

Tactic:
(this h₀).2

Premises used: And.right