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 μ
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
-- 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:
exacts [(this h₀).2, (this h₀').2]

Premises used: 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 μ
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₁ :
  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) ∂μ
⊢ 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) ∂μ)

Tactic:
calc
    g ((a • ⨍ x in t, f x ∂μ) + b • ⨍ x in tᶜ, f x ∂μ) <
        a * g (⨍ x in t, f x ∂μ) + b * g (⨍ x in tᶜ, f x ∂μ) :=
      hg.2 (this h₀).1 (this h₀').1 hne ha hb hab
    _ ≤ (a * ⨍ x in t, g (f x) ∂μ) + b * ⨍ x in tᶜ, g (f x) ∂μ := by
      gcongr
      exacts [(this h₀).2, (this h₀').2]

Premises used: HMul.hMul, Compl.compl, MeasureTheory.Measure.restrict, MeasureTheory.average, And.right, And.left, HAdd.hAdd, HSMul.hSMul
-- 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 : StrictConcaveOn ℝ s g
hgc : ContinuousOn g s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
hgi : Integrable (g ∘ f) μ
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ ⨍ (x : α), g (f x) ∂μ < g (⨍ (x : α), f x ∂μ)

Tactic:
simpa only [Pi.neg_apply, average_neg, neg_lt_neg_iff] using
    hg.neg.ae_eq_const_or_map_average_lt hgc.neg hsc hfs hfi hgi.neg

Premises used: neg_lt_neg_iff, ContinuousOn.neg, MeasureTheory.Integrable.neg, StrictConcaveOn.neg, MeasureTheory.average_neg, Pi.neg_apply, StrictConvexOn.ae_eq_const_or_map_average_lt
-- 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
C : ℝ
inst_3 : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
inl : ∀ (hC0 : C ≤ 0), f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (⨍ (x : α), f x ∂μ) < C
inr : ∀ (hC0 : 0 < C), f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (⨍ (x : α), f x ∂μ) < C
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (⨍ (x : α), f x ∂μ) < C

Tactic:
rcases le_or_gt C 0 with hC0 | hC0

Premises used: le_or_gt, OfNat.ofNat
-- 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
C : ℝ
inst_3 : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : C ≤ 0
⊢ f =ᶠ[ae μ] 0

Tactic:
have : f =ᵐ[μ] 0 := h_le.mono fun x hx => norm_le_zero_iff.1 (hx.trans hC0)
-- 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
C : ℝ
inst_3 : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : C ≤ 0
this : f =ᶠ[ae μ] 0
inl : f =ᶠ[ae μ] const α 0 ∨ norm.{u_2} (E := E) 0 < C
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (⨍ (x : α), f x ∂μ) < C

Tactic:
simp only [average_congr this, Pi.zero_apply, average_zero]

Premises used: Pi.zero_apply, MeasureTheory.average_zero, MeasureTheory.average_congr
-- 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
C : ℝ
inst_3 : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : C ≤ 0
this : f =ᶠ[ae μ] 0
⊢ f =ᶠ[ae μ] const α 0 ∨ norm.{u_2} (E := E) 0 < C

Tactic:
Or.inl this

Premises used: Or.inl
-- 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
C : ℝ
inst_3 : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : C ≤ 0
this : f =ᶠ[ae μ] 0
⊢ f =ᶠ[ae μ] const α 0 ∨ norm.{u_2} (E := E) 0 < C

Tactic:
exact Or.inl this

Premises used: Or.inl
-- 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
C : ℝ
inst_3 : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : 0 < C
pos : ∀ (hfi : Integrable f μ), f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (⨍ (x : α), f x ∂μ) < C
neg : ∀ (hfi : ¬Integrable f μ), f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (⨍ (x : α), f x ∂μ) < C
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (⨍ (x : α), f x ∂μ) < C

Tactic:
by_cases hfi : Integrable f μ

Premises used: MeasureTheory.Integrable
-- 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
C : ℝ
inst_3 : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : 0 < C
hfi : ¬Integrable f μ
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (⨍ (x : α), f x ∂μ) < C

Tactic:
simp [average_eq, integral_undef hfi, hC0]

Premises used: MeasureTheory.integral_undef, MeasureTheory.average_eq
-- 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
C : ℝ
inst_3 : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : 0 < C
hfi : Integrable f μ
pos :
  ∀ (hμt : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)),
    f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (⨍ (x : α), f x ∂μ) < C
pos₁ :
  ∀ (hμt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)),
    f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (⨍ (x : α), f x ∂μ) < C
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (⨍ (x : α), f x ∂μ) < C

Tactic:
rcases (le_top : μ univ ≤ ∞).eq_or_lt with hμt | hμt

Premises used: LE.le.eq_or_lt, le_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 α
f : α → E
C : ℝ
inst_3 : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : 0 < C
hfi : Integrable f μ
hμt : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (⨍ (x : α), f x ∂μ) < C

Tactic:
simp [average_eq, measureReal_def, hμt, hC0]

Premises used: MeasureTheory.measureReal_def, MeasureTheory.average_eq
-- 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
C : ℝ
inst_3 : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : 0 < C
hfi : Integrable f μ
hμt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IsFiniteMeasure μ

Tactic:
haveI : IsFiniteMeasure μ := ⟨hμt⟩
-- 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
C : ℝ
inst_3 : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : 0 < C
hfi : Integrable f μ
hμt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
this : IsFiniteMeasure μ
⊢ ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set E) (closedBall 0 C) (f x)

Tactic:
simpa only [mem_closedBall_zero_iff]

Premises used: mem_closedBall_zero_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 α
f : α → E
C : ℝ
inst_3 : StrictConvexSpace ℝ E
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
hC0 : 0 < C
hfi : Integrable f μ
hμt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
this : IsFiniteMeasure μ
⊢ ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set E) (closedBall 0 C) (f x)

Tactic:
replace h_le : ∀ᵐ x ∂μ, f x ∈ closedBall (0 : E) C := by simpa only [mem_closedBall_zero_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 α
f : α → E
C : ℝ
inst_3 : StrictConvexSpace ℝ E
hC0 : 0 < C
hfi : Integrable f μ
hμt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
this : IsFiniteMeasure μ
h_le : ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set E) (closedBall 0 C) (f x)
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (⨍ (x : α), f x ∂μ) < C

Tactic:
simpa only [interior_closedBall _ hC0.ne', mem_ball_zero_iff] using
    (strictConvex_closedBall ℝ (0 : E) C).ae_eq_const_or_average_mem_interior isClosed_closedBall
      h_le hfi

Premises used: Real, interior_closedBall, Metric.isClosed_closedBall, strictConvex_closedBall, LT.lt.ne', StrictConvex.ae_eq_const_or_average_mem_interior, OfNat.ofNat, mem_ball_zero_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 α
f : α → E
C : ℝ
inst_3 : StrictConvexSpace ℝ E
inst_4 : IsFiniteMeasure μ
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
inl : ∀ (h₀ : μ = 0), f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < μ.real univ * C
inr : ∀ (h₀ : μ ≠ 0), f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < μ.real univ * C
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < μ.real univ * C

Tactic:
rcases eq_or_ne μ 0 with h₀ | h₀

Premises used: eq_or_ne, OfNat.ofNat
-- 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
C : ℝ
inst_3 : StrictConvexSpace ℝ E
inst_4 : IsFiniteMeasure μ
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
h₀ : μ = 0
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < μ.real univ * C

Tactic:
simp [h₀, EventuallyEq]

Premises used: Filter.EventuallyEq
-- 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
C : ℝ
inst_3 : StrictConvexSpace ℝ E
inst_4 : IsFiniteMeasure μ
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
h₀ : μ ≠ 0
⊢ 0 < μ.real univ

Tactic:
simp [measureReal_def, ENNReal.toReal_pos_iff, pos_iff_ne_zero, h₀, measure_lt_top]

Premises used: ENNReal.toReal_pos_iff, MeasureTheory.measure_lt_top, MeasureTheory.measureReal_def, pos_iff_ne_zero
-- 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
C : ℝ
inst_3 : StrictConvexSpace ℝ E
inst_4 : IsFiniteMeasure μ
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
h₀ : μ ≠ 0
⊢ 0 < μ.real univ

Tactic:
have hμ : 0 < μ.real univ := by
    simp [measureReal_def, ENNReal.toReal_pos_iff, pos_iff_ne_zero, h₀, measure_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 α
f : α → E
C : ℝ
inst_3 : StrictConvexSpace ℝ E
inst_4 : IsFiniteMeasure μ
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
h₀ : μ ≠ 0
hμ : 0 < μ.real univ
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < μ.real univ * C

Tactic:
(ae_eq_const_or_norm_average_lt_of_norm_le_const h_le).imp_right fun H => ?_

Premises used: ae_eq_const_or_norm_average_lt_of_norm_le_const, 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 α
f : α → E
C : ℝ
inst_3 : StrictConvexSpace ℝ E
inst_4 : IsFiniteMeasure μ
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
h₀ : μ ≠ 0
hμ : 0 < μ.real univ
inr : ∀ (H : norm.{u_2} (E := E) (⨍ (x : α), f x ∂μ) < C), norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < μ.real univ * C
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < μ.real univ * C

Tactic:
refine (ae_eq_const_or_norm_average_lt_of_norm_le_const h_le).imp_right fun H => ?_

Premises used: ae_eq_const_or_norm_average_lt_of_norm_le_const, 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 α
f : α → E
C : ℝ
inst_3 : StrictConvexSpace ℝ E
inst_4 : IsFiniteMeasure μ
h_le : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
h₀ : μ ≠ 0
hμ : 0 < μ.real univ
H : norm.{u_2} (E := E) (⨍ (x : α), f x ∂μ) < C
inr :
  ∀ (H : ‖HSMul.hSMul (β := E) (μ.real univ)⁻¹ (∫ (x : α), f x ∂μ)‖ < C),
    norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < μ.real univ * C
inr₁ :
  ∀ (H : ‖(μ.real univ)⁻¹‖ * norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < C),
    norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < μ.real univ * C
inr₂ :
  ∀ (H : ‖μ.real univ‖⁻¹ * norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < C),
    norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < μ.real univ * C
inr₃ :
  ∀ (H : |μ.real univ|⁻¹ * norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < C),
    norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < μ.real univ * C
inr₄ :
  ∀ (H : (μ.real univ)⁻¹ * norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < C),
    norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < μ.real univ * C
inr₅ :
  ∀ (H : norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) / μ.real univ < C),
    norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < μ.real univ * C
inr₆ inr₇ inr₈ inr₉ :
  ∀ (H : norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < μ.real univ * C),
    norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < μ.real univ * C
⊢ norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < μ.real univ * C

Tactic:
rwa [average_eq, norm_smul, norm_inv, Real.norm_eq_abs, abs_of_pos hμ, ← div_eq_inv_mul,
    div_lt_iff₀' hμ] at H

Premises used: norm_smul, norm_inv, div_lt_iff₀', abs_of_pos, div_eq_inv_mul, Real.norm_eq_abs, MeasureTheory.average_eq
-- 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 α
t : Set α
f : α → E
C : ℝ
inst_3 : StrictConvexSpace ℝ E
ht : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h_le : ∀ᵐ (x : α) ∂μ.restrict t, ‖f x‖ ≤ C
⊢ Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞))

Tactic:
haveI := Fact.mk ht.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 α
t : Set α
f : α → E
C : ℝ
inst_3 : StrictConvexSpace ℝ E
ht : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h_le : ∀ᵐ (x : α) ∂μ.restrict t, ‖f x‖ ≤ C
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞))
rw :
  f =ᶠ[ae (μ.restrict t)] const α (⨍ (x : α) in t, f x ∂μ) ∨
    norm.{u_2} (E := E) (∫ (x : α) in t, f x ∂μ) < (μ.restrict t).real univ * C
⊢ f =ᶠ[ae (μ.restrict t)] const α (⨍ (x : α) in t, f x ∂μ) ∨ norm.{u_2} (E := E) (∫ (x : α) in t, f x ∂μ) < μ.real t * C

Tactic:
rw [← measureReal_restrict_apply_univ]

Premises used: MeasureTheory.measureReal_restrict_apply_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 α
t : Set α
f : α → E
C : ℝ
inst_3 : StrictConvexSpace ℝ E
ht : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h_le : ∀ᵐ (x : α) ∂μ.restrict t, ‖f x‖ ≤ C
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ f =ᶠ[ae (μ.restrict t)] const α (⨍ (x : α) in t, f x ∂μ) ∨
    norm.{u_2} (E := E) (∫ (x : α) in t, f x ∂μ) < (μ.restrict t).real univ * C

Tactic:
ae_eq_const_or_norm_integral_lt_of_norm_le_const h_le

Premises used: ae_eq_const_or_norm_integral_lt_of_norm_le_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 α
t : Set α
f : α → E
C : ℝ
inst_3 : StrictConvexSpace ℝ E
ht : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h_le : ∀ᵐ (x : α) ∂μ.restrict t, ‖f x‖ ≤ C
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ f =ᶠ[ae (μ.restrict t)] const α (⨍ (x : α) in t, f x ∂μ) ∨
    norm.{u_2} (E := E) (∫ (x : α) in t, f x ∂μ) < (μ.restrict t).real univ * C

Tactic:
exact ae_eq_const_or_norm_integral_lt_of_norm_le_const h_le

Premises used: ae_eq_const_or_norm_integral_lt_of_norm_le_const
-- Module: Mathlib.Analysis.Convex.Intrinsic
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : Ring 𝕜
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
s : Set P
x : P
⊢ x ∈ intrinsicInterior 𝕜 s ↔
    ∃ (y : ↥(affineSpan 𝕜 s)),
      Membership.mem (γ := Set ↥(affineSpan 𝕜 s))
          (interior
            (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s))
          y ∧
        (↑y : P) = x

Tactic:
mem_image _ _ _

Premises used: Set.Mem, intrinsicInterior, Set.mem_image
-- Module: Mathlib.Analysis.Convex.Intrinsic
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : Ring 𝕜
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
s : Set P
x : P
⊢ x ∈ intrinsicFrontier 𝕜 s ↔
    ∃ (y : ↥(affineSpan 𝕜 s)),
      Membership.mem (γ := Set ↥(affineSpan 𝕜 s))
          (frontier
            (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s))
          y ∧
        (↑y : P) = x

Tactic:
mem_image _ _ _

Premises used: intrinsicFrontier, Set.Mem, Set.mem_image
-- Module: Mathlib.Analysis.Convex.Intrinsic
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : Ring 𝕜
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
s : Set P
x : P
⊢ x ∈ intrinsicClosure 𝕜 s ↔
    ∃ (y : ↥(affineSpan 𝕜 s)),
      Membership.mem (γ := Set ↥(affineSpan 𝕜 s))
          (closure[instTopologicalSpaceSubtype]
            (Subtype.val (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 s) x) ⁻¹' s))
          y ∧
        (↑y : P) = x

Tactic:
mem_image _ _ _

Premises used: intrinsicClosure, Set.Mem, Set.mem_image
-- Module: Mathlib.Analysis.Convex.Intrinsic
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : Ring 𝕜
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
s : Set P
⊢ intrinsicInterior 𝕜 s ⊆ s

Tactic:
image_subset_iff.2 interior_subset

Premises used: Iff.mpr, interior_subset, intrinsicInterior, Set.image_subset_iff
-- Module: Mathlib.Analysis.Convex.Intrinsic
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : Ring 𝕜
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
s : Set P
hs : IsClosed[inst_3] s
⊢ intrinsicFrontier 𝕜 s ⊆ s

Tactic:
image_subset_iff.2 (hs.preimage continuous_induced_dom).frontier_subset

Premises used: Iff.mpr, intrinsicFrontier, IsClosed.frontier_subset, continuous_induced_dom, IsClosed.preimage, Set.image_subset_iff
-- Module: Mathlib.Analysis.Convex.Intrinsic
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : Ring 𝕜
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
s : Set P
⊢ intrinsicFrontier 𝕜 s ⊆ intrinsicClosure 𝕜 s

Tactic:
image_mono frontier_subset_closure

Premises used: intrinsicFrontier, intrinsicClosure, Set.image_mono, frontier_subset_closure
-- Module: Mathlib.Analysis.Convex.Intrinsic
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst : Ring 𝕜
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
s : Set P
⊢ s ⊆ intrinsicClosure 𝕜 s

Tactic:
fun x hx => ⟨⟨x, subset_affineSpan _ _ hx⟩, subset_closure hx, rfl⟩

Premises used: intrinsicClosure, Set.Mem, subset_closure, setOf, Set.Subset, Subtype.mk, subset_affineSpan, And.intro, Exists.intro, Set.image, rfl