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
f : α → E
g : E → ℝ
inst_3 : IsFiniteMeasure μ
inst_4 : NeZero μ
hg : ConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
ht_mem : ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set (E × ℝ)) {p : E × ℝ | p.1 ∈ s ∧ g p.1 ≤ p.2} (f x, g (f x))
⊢ Membership.mem (γ := Set (E × ℝ)) {p : E × ℝ | p.1 ∈ s ∧ g p.1 ≤ p.2} (⨍ (x : α), f x ∂μ, ⨍ (x : α), g (f x) ∂μ)

Tactic:
exact average_pair hfi hgi ▸
    hg.convex_epigraph.average_mem (hsc.epigraph hgc) ht_mem (hfi.prodMk hgi)
-- 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 μ
inst_4 : NeZero μ
hg : ConcaveOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
⊢ Membership.mem (γ := Set (E × ℝ)) {p : E × ℝ | p.1 ∈ s ∧ p.2 ≤ g p.1} (⨍ (x : α), f x ∂μ, ⨍ (x : α), g (f x) ∂μ)

Tactic:
simpa only [mem_setOf_eq, Pi.neg_apply, average_neg, neg_le_neg_iff] using
    hg.neg.average_mem_epigraph hgc.neg hsc hfs hfi hgi.neg

Premises used: ContinuousOn.neg, MeasureTheory.Integrable.neg, Set.mem_setOf_eq, ConvexOn.average_mem_epigraph, ConcaveOn.neg, MeasureTheory.average_neg, Pi.neg_apply, neg_le_neg_iff
-- 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 μ
inst_4 : NeZero μ
hg : ConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
⊢ g (⨍ (x : α), f x ∂μ) ≤ ⨍ (x : α), g (f x) ∂μ

Tactic:
(hg.average_mem_epigraph hgc hsc hfs hfi hgi).2

Premises used: MeasureTheory.average, ConvexOn.average_mem_epigraph, And.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 μ
inst_4 : NeZero μ
hg : ConcaveOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
⊢ ⨍ (x : α), g (f x) ∂μ ≤ g (⨍ (x : α), f x ∂μ)

Tactic:
(hg.average_mem_hypograph hgc hsc hfs hfi hgi).2

Premises used: MeasureTheory.average, And.right, ConcaveOn.average_mem_hypograph
-- 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
g : E → ℝ
hg : ConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h0 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
ht : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hfs : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s
hfi : IntegrableOn f t μ
hgi : IntegrableOn (g ∘ f) t μ
⊢ Membership.mem (γ := Set (E × ℝ)) {p : E × ℝ | p.1 ∈ s ∧ g p.1 ≤ p.2}
    (⨍ (x : α) in t, f x ∂μ, ⨍ (x : α) in t, g (f x) ∂μ)

Tactic:
have := Fact.mk ht.lt_top
  have := NeZero.mk h0
  hg.average_mem_epigraph hgc hsc hfs hfi hgi

Premises used: NeZero.mk, Fact.mk, ConvexOn.average_mem_epigraph, Ne.lt_top
-- 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
g : E → ℝ
hg : ConcaveOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h0 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
ht : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hfs : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s
hfi : IntegrableOn f t μ
hgi : IntegrableOn (g ∘ f) t μ
⊢ Membership.mem (γ := Set (E × ℝ)) {p : E × ℝ | p.1 ∈ s ∧ p.2 ≤ g p.1}
    (⨍ (x : α) in t, f x ∂μ, ⨍ (x : α) in t, g (f x) ∂μ)

Tactic:
simpa only [mem_setOf_eq, Pi.neg_apply, average_neg, neg_le_neg_iff] using
    hg.neg.set_average_mem_epigraph hgc.neg hsc h0 ht hfs hfi hgi.neg

Premises used: ContinuousOn.neg, ConvexOn.set_average_mem_epigraph, Set.mem_setOf_eq, ConcaveOn.neg, MeasureTheory.IntegrableOn.neg, MeasureTheory.average_neg, Pi.neg_apply, neg_le_neg_iff
-- 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
g : E → ℝ
hg : ConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h0 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
ht : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hfs : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s
hfi : IntegrableOn f t μ
hgi : IntegrableOn (g ∘ f) t μ
⊢ g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ

Tactic:
(hg.set_average_mem_epigraph hgc hsc h0 ht hfs hfi hgi).2

Premises used: ConvexOn.set_average_mem_epigraph, MeasureTheory.average, And.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
t : Set α
f : α → E
g : E → ℝ
hg : ConcaveOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h0 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
ht : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hfs : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s
hfi : IntegrableOn f t μ
hgi : IntegrableOn (g ∘ f) t μ
⊢ ⨍ (x : α) in t, g (f x) ∂μ ≤ g (⨍ (x : α) in t, f x ∂μ)

Tactic:
(hg.set_average_mem_hypograph hgc hsc h0 ht hfs hfi hgi).2

Premises used: MeasureTheory.average, ConcaveOn.set_average_mem_hypograph, And.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 : IsProbabilityMeasure μ
hg : ConvexOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
⊢ g (∫ (x : α), f x ∂μ) ≤ ∫ (x : α), g (f x) ∂μ

Tactic:
simpa only [average_eq_integral] using hg.map_average_le hgc hsc hfs hfi hgi

Premises used: MeasureTheory.average_eq_integral, ConvexOn.map_average_le
-- 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 : IsProbabilityMeasure μ
hg : ConcaveOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
⊢ ∫ (x : α), g (f x) ∂μ ≤ g (∫ (x : α), f x ∂μ)

Tactic:
simpa only [average_eq_integral] using hg.le_map_average hgc hsc hfs hfi hgi

Premises used: MeasureTheory.average_eq_integral, ConcaveOn.le_map_average
-- 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 α
f : α → E
inst_3 : IsFiniteMeasure μ
hfi : Integrable f μ
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨
    ∃ (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 ∂μ)

Tactic:
or_iff_not_imp_right.mpr fun H => ?_

Premises used: Iff.mpr, Classical.or_iff_not_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 α
f : α → E
inst_3 : IsFiniteMeasure μ
hfi : Integrable f μ
refine :
  ∀
    (H :
      ¬∃ (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 ∂μ)),
    f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ)
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨
    ∃ (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 ∂μ)

Tactic:
refine or_iff_not_imp_right.mpr fun H => ?_

Premises used: Iff.mpr, Classical.or_iff_not_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 α
f : α → E
inst_3 : IsFiniteMeasure μ
hfi : Integrable f μ
H :
  ¬∃ (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 ∂μ)
⊢ ∀ (t : Set α) (_ : MeasurableSet t) (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞))
    (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)

Tactic:
push Not at H

Premises used: Not
-- 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 α
f : α → E
inst_3 : IsFiniteMeasure μ
hfi : Integrable f μ
H :
  ∀ (t : Set α) (_ : MeasurableSet t) (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞))
    (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ)

Tactic:
hfi.ae_eq_of_forall_setIntegral_eq _ _ (integrable_const _) fun t ht ht' => ?_

Premises used: MeasureTheory.Integrable.ae_eq_of_forall_setIntegral_eq, MeasureTheory.integrable_const
-- 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 α
f : α → E
inst_3 : IsFiniteMeasure μ
hfi : Integrable f μ
H :
  ∀ (t : Set α) (_ : MeasurableSet t) (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞))
    (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
refine :
  ∀ (t : Set α) (ht : MeasurableSet t) (ht' : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)),
    Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, f x ∂μ) (∫ (x : α) in t, const α (⨍ (x : α), f x ∂μ) x ∂μ)
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ)

Tactic:
refine hfi.ae_eq_of_forall_setIntegral_eq _ _ (integrable_const _) fun t ht ht' => ?_

Premises used: MeasureTheory.Integrable.ae_eq_of_forall_setIntegral_eq, MeasureTheory.integrable_const
-- 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 α
f : α → E
inst_3 : IsFiniteMeasure μ
hfi : Integrable f μ
H :
  ∀ (t : Set α) (_ : MeasurableSet t) (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞))
    (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
t : Set α
ht : MeasurableSet t
simp : ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, f x ∂μ) (∫ (x : α) in t, const α (⨍ (x : α), f x ∂μ) x ∂μ)

Tactic:
simp only [const_apply, setIntegral_const]

Premises used: Function.const_apply, MeasureTheory.setIntegral_const
-- 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 α
f : α → E
inst_3 : IsFiniteMeasure μ
hfi : Integrable f μ
H :
  ∀ (t : Set α) (_ : MeasurableSet t) (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞))
    (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
t : Set α
ht : MeasurableSet t
pos :
  ∀ (h₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)),
    ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
neg :
  ∀ (h₀ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)),
    ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
⊢ ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)

Tactic:
by_cases h₀ : μ t = 0

Premises used: 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 α
f : α → E
inst_3 : IsFiniteMeasure μ
hfi : Integrable f μ
H :
  ∀ (t : Set α) (_ : MeasurableSet t) (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞))
    (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
t : Set α
ht : MeasurableSet t
h₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
pos : (@integral _ _ _ _ m0 0 fun (x : α) ↦ f x) = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
pos₁ : 0 = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
pos₂ : 0 = HSMul.hSMul (β := E) (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t)) (⨍ (x : α), f x ∂μ)
pos₃ : 0 = HSMul.hSMul (β := E) (ENNReal.toReal 0) (⨍ (x : α), f x ∂μ)
pos₄ : 0 = HSMul.hSMul (α := ℝ) (β := E) 0 (⨍ (x : α), f x ∂μ)
pos₅ pos₆ : Eq.{u_2 + 1} (α := E) 0 0
⊢ ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)

Tactic:
rw [restrict_eq_zero.2 h₀, integral_zero_measure, measureReal_def, h₀,
      ENNReal.toReal_zero, zero_smul]

Premises used: Iff.mpr, MeasureTheory.Measure.restrict_eq_zero, zero_smul, ENNReal.toReal_zero, MeasureTheory.measureReal_def, MeasureTheory.integral_zero_measure
-- 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 α
f : α → E
inst_3 : IsFiniteMeasure μ
hfi : Integrable f μ
H :
  ∀ (t : Set α) (_ : MeasurableSet t) (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞))
    (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
t : Set α
ht : MeasurableSet t
h₀ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
pos :
  ∀ (h₀' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
neg :
  ∀ (h₀' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
⊢ ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)

Tactic:
by_cases h₀' : μ tᶜ = 0

Premises used: Compl.compl, 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 α
f : α → E
inst_3 : IsFiniteMeasure μ
hfi : Integrable f μ
H :
  ∀ (t : Set α) (_ : MeasurableSet t) (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞))
    (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
t : Set α
ht : MeasurableSet t
h₀ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h₀' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ t =ᶠ[ae μ] univ

Tactic:
rw [← ae_eq_univ] at h₀'

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 α
f : α → E
inst_3 : IsFiniteMeasure μ
hfi : Integrable f μ
H :
  ∀ (t : Set α) (_ : MeasurableSet t) (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞))
    (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
t : Set α
ht : MeasurableSet t
h₀ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h₀' : t =ᶠ[ae μ] univ
pos : ∫ (x : α) in univ, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
pos₁ : ∫ (x : α), f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
pos₂ : ∫ (x : α), f x ∂μ = HSMul.hSMul (β := E) (μ.real univ) (⨍ (x : α), f x ∂μ)
pos₃ pos₄ : Eq.{u_2 + 1} (α := E) (∫ (x : α), f x ∂μ) (∫ (x : α), f x ∂μ)
⊢ ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)

Tactic:
rw [restrict_congr_set h₀', restrict_univ, measureReal_congr h₀', measure_smul_average]

Premises used: MeasureTheory.Measure.restrict_congr_set, MeasureTheory.measure_smul_average, MeasureTheory.measureReal_congr, 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 α
f : α → E
inst_3 : IsFiniteMeasure μ
hfi : Integrable f μ
H :
  ∀ (t : Set α) (_ : MeasurableSet t) (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞))
    (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
t : Set α
ht : MeasurableSet t
h₀ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h₀' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Membership.mem (γ := Set E) (openSegment ℝ (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)) (⨍ (x : α), f x ∂μ)

Tactic:
have := average_mem_openSegment_compl_self ht.nullMeasurableSet h₀ h₀' hfi
-- 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 α
f : α → E
inst_3 : IsFiniteMeasure μ
hfi : Integrable f μ
H :
  ∀ (t : Set α) (_ : MeasurableSet t) (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞))
    (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
t : Set α
ht : MeasurableSet t
h₀ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h₀' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
this :
  Membership.mem (γ := Set E) (openSegment ℝ (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)) (⨍ (x : α), f x ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (⨍ (x : α), f x ∂μ) (⨍ (x : α) in t, f x ∂μ)

Tactic:
rw [← H t ht h₀ h₀', openSegment_same, mem_singleton_iff] at this

Premises used: Set.mem_singleton_iff, openSegment_same
-- 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 α
f : α → E
inst_3 : IsFiniteMeasure μ
hfi : Integrable f μ
H :
  ∀ (t : Set α) (_ : MeasurableSet t) (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞))
    (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
t : Set α
ht : MeasurableSet t
h₀ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h₀' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
this : Eq.{u_2 + 1} (α := E) (⨍ (x : α), f x ∂μ) (⨍ (x : α) in t, f x ∂μ)
⊢ 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 α
f : α → E
inst_3 : IsFiniteMeasure μ
hfi : Integrable f μ
H :
  ∀ (t : Set α) (_ : MeasurableSet t) (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞))
    (_ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq.{u_2 + 1} (α := E) (⨍ (x : α) in t, f x ∂μ) (⨍ (x : α) in tᶜ, f x ∂μ)
t : Set α
ht : MeasurableSet t
h₀ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
h₀' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
this : Eq.{u_2 + 1} (α := E) (⨍ (x : α), f x ∂μ) (⨍ (x : α) in t, f x ∂μ)
neg : ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α) in t, f x ∂μ)
neg₁ neg₂ : Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, f x ∂μ) (∫ (x : α) in t, f x ∂μ)
⊢ ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)

Tactic:
rw [this, measure_smul_setAverage _ (by finiteness)]

Premises used: MeasureTheory.measure_smul_setAverage
-- 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
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ t) : ℝ≥0∞) (0 : ℝ≥0∞)

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∞) 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∞)
⊢ ∀ᵐ (x : α) ∂μ, f x ∈ 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∞) 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
⊢ Integrable f μ

Tactic:
rw [← measure_toMeasurable] at h0

Premises used: MeasureTheory.measure_toMeasurable