awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
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) ∂μ
⊢ 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) ∂μ
have h₂ : g (⨍ (x : α) in tᶜ, f x ∂μ) ≤ ⨍ (x : α) in tᶜ, g (f x) ∂μ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
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 ∂μ)) <
    HSMul.hSMul (β := ℝ) a (⨍ (x : α) in t, g (f x) ∂μ) + HSMul.hSMul (β := ℝ) b (⨍ (x : α) in tᶜ, g (f x) ∂μ)
have 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) ∂μ
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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
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
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (⨍ (x : α), f x ∂μ) < C
have inl : ∀ (hC0 : C ≤ 0), 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
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
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
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (⨍ (x : α), f x ∂μ) < C
have inr : ∀ (hC0 : 0 < 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
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (hypothesis)
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 μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (⨍ (x : α), f x ∂μ) < C
have this : f =ᶠ[ae μ] 0
Tactic: have : f =ᵐ[μ] 0 := h_le.mono fun x hx => norm_le_zero_iff.1 (hx.trans hC0)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
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 α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (⨍ (x : α), f x ∂μ) < C
have inl : f =ᶠ[ae μ] const α 0 ∨ norm.{u_2} (E := E) 0 < C
Tactic: simp only [average_congr this, Pi.zero_apply, average_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
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
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (⨍ (x : α), f x ∂μ) < C
have pos : ∀ (hfi : Integrable f μ), f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (⨍ (x : α), f x ∂μ) < C
Tactic: by_cases hfi : Integrable f μ
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
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
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (⨍ (x : α), f x ∂μ) < C
have neg : ∀ (hfi : ¬Integrable f μ), f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (⨍ (x : α), f x ∂μ) < C
Tactic: by_cases hfi : Integrable f μ
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
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
have 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
Tactic: rcases (le_top : μ univ ≤ ∞).eq_or_lt with hμt | hμt
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
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
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (⨍ (x : α), f x ∂μ) < C
have 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
Tactic: rcases (le_top : μ univ ≤ ∞).eq_or_lt with hμt | hμt
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (hypothesis)
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∞)
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (⨍ (x : α), f x ∂μ) < C
have this : IsFiniteMeasure μ
Tactic: haveI : IsFiniteMeasure μ := ⟨hμt⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (hypothesis)
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 μ
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (⨍ (x : α), f x ∂μ) < C
have h_le₁ : ∀ᵐ (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]
Cleared hypotheses: h_le
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
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
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < μ.real univ * C
have inl : ∀ (h₀ : μ = 0), 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₀
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
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
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < μ.real univ * C
have inr : ∀ (h₀ : μ ≠ 0), 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₀
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (hypothesis)
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
have hμ : 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
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
have inr : ∀ (H : norm.{u_2} (E := E) (⨍ (x : α), f x ∂μ) < C), 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 => ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
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
⊢ norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < μ.real univ * C
have inr : ∀ (H : ‖HSMul.hSMul (β := E) (μ.real univ)⁻¹ (∫ (x : α), f x ∂μ)‖ < 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
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
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
⊢ norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < μ.real univ * C
have inr₁ : ∀ (H : ‖(μ.real univ)⁻¹‖ * norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < 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
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
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
⊢ norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < μ.real univ * C
have inr₂ : ∀ (H : ‖μ.real univ‖⁻¹ * norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < 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
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
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
⊢ norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < μ.real univ * C
have inr₃ : ∀ (H : |μ.real univ|⁻¹ * norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < 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
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
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
⊢ norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < μ.real univ * C
have inr₄ : ∀ (H : (μ.real univ)⁻¹ * norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < 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
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
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
⊢ norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < μ.real univ * C
have inr₅ : ∀ (H : 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
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
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
⊢ norm.{u_2} (E := E) (∫ (x : α), f x ∂μ) < μ.real univ * C
have inr₆ : ∀ (H : 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
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (hypothesis)
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
⊢ f =ᶠ[ae (μ.restrict t)] const α (⨍ (x : α) in t, f x ∂μ) ∨ norm.{u_2} (E := E) (∫ (x : α) in t, f x ∂μ) < μ.real t * C
have this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞))
Tactic: haveI := Fact.mk ht.lt_top
-- Lean 4 proof step from Mathlib.Analysis.Convex.Integral (goal)
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 ∂μ) < μ.real t * C
have 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
Tactic: rw [← measureReal_restrict_apply_univ]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
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
⊢ (intrinsicClosure 𝕜 s).Nonempty → s.Nonempty
have simp_rw : intrinsicClosure 𝕜 s ≠ ∅ → s ≠ ∅
Tactic: simp_rw [nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
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
x : P
⊢ Eq (α := Set P) (intrinsicFrontier 𝕜 {x}) ∅
have rw : Eq (α := Set P)
  (image (α := ↥(affineSpan 𝕜 {x}))
    (Subtype.val (p := fun (x_1 : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {x}) x_1))
    (frontier
      (Subtype.val (p := fun (x_1 : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {x}) x_1) ⁻¹' {x})))
  ∅
Tactic: rw [intrinsicFrontier, preimage_coe_affineSpan_singleton, frontier_univ, image_empty]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Intrinsic (goal)
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
x : P
rw :
  Eq (α := Set P)
    (image (α := ↥(affineSpan 𝕜 {x}))
      (Subtype.val (p := fun (x_1 : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {x}) x_1))
      (frontier
        (Subtype.val (p := fun (x_1 : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {x}) x_1) ⁻¹' {x})))
    ∅
⊢ Eq (α := Set P) (intrinsicFrontier 𝕜 {x}) ∅
have rw₁ : Eq.{u_5 + 1} (α := Set P)
  (image (α := ↥(affineSpan 𝕜 {x}))
    (Subtype.val (p := fun (x_1 : P) ↦ Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {x}) x_1))
    (frontier univ))
  ∅
Tactic: rw [intrinsicFrontier, preimage_coe_affineSpan_singleton, frontier_univ, image_empty]