awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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∞)
⊢ ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
have h₀'₁ : t =ᶠ[ae μ] univ
Tactic: rw [← ae_eq_univ] 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
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
⊢ ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
have pos : ∫ (x : α) in univ, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
Tactic: rw [restrict_congr_set h₀', restrict_univ, measureReal_congr h₀', measure_smul_average]
-- 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
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 ∂μ)
⊢ ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
have pos₁ : ∫ (x : α), f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
Tactic: rw [restrict_congr_set h₀', restrict_univ, measureReal_congr h₀', measure_smul_average]
-- 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
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 ∂μ)
⊢ ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
have pos₂ : ∫ (x : α), f x ∂μ = HSMul.hSMul (β := E) (μ.real univ) (⨍ (x : α), f x ∂μ)
Tactic: rw [restrict_congr_set h₀', restrict_univ, measureReal_congr h₀', measure_smul_average]
-- 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
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 ∂μ)
⊢ ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
have pos₃ : Eq.{u_2 + 1} (α := E) (∫ (x : α), f x ∂μ) (∫ (x : α), f x ∂μ)
Tactic: rw [restrict_congr_set h₀', restrict_univ, measureReal_congr h₀', measure_smul_average]
-- 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
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∞)
⊢ ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
have this : 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
-- 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
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 ∂μ)
⊢ ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
have this₁ : 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
Cleared hypotheses: this
-- 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
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 ∂μ)
⊢ ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
have neg : ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α) in t, f x ∂μ)
Tactic: rw [this, measure_smul_setAverage _ (by finiteness)]
-- 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
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 ∂μ)
⊢ ∫ (x : α) in t, f x ∂μ = HSMul.hSMul (β := E) (μ.real t) (⨍ (x : α), f x ∂μ)
have neg₁ : Eq.{u_2 + 1} (α := E) (∫ (x : α) in t, f x ∂μ) (∫ (x : α) in t, f x ∂μ)
Tactic: rw [this, measure_smul_setAverage _ (by finiteness)]
-- 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 α
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
⊢ ⨍ (x : α), f x ∂μ ∈ interior s
have h0₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ t) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← measure_toMeasurable] at h0
Cleared hypotheses: h0, hfs, hfi, ht
-- 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 α
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 : α), f x ∂μ ∈ interior s
have ht₁ : ⨍ (x : α) in toMeasurable μ t, f x ∂μ ∈ interior s
Tactic: rw [← restrict_toMeasurable (by finiteness)] at ht
Cleared hypotheses: ht
-- 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
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
⊢ ⨍ (x : α), f x ∂μ ∈ interior s
have pos : ∀ (h0' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ t)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
  ⨍ (x : α), f x ∂μ ∈ interior s
Tactic: by_cases h0' : μ (toMeasurable μ t)ᶜ = 0
-- 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
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
⊢ ⨍ (x : α), f x ∂μ ∈ interior s
have neg : ∀ (h0' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ t)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
  ⨍ (x : α), f x ∂μ ∈ interior s
Tactic: by_cases h0' : μ (toMeasurable μ t)ᶜ = 0
-- 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 α
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
have h0'₁ : toMeasurable μ t =ᶠ[ae μ] univ
Tactic: rw [← ae_eq_univ] at h0'
Cleared hypotheses: h0'
-- 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
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
⊢ ⨍ (x : α), f x ∂μ ∈ interior s
have pos : ∀ (ht : ⨍ (x : α) in univ, f x ∂μ ∈ interior s) (h0' : toMeasurable μ t =ᶠ[ae μ] univ), ⨍ (x : α), f x ∂μ ∈ interior s
Tactic: rwa [restrict_congr_set h0', restrict_univ] at ht
Cleared hypotheses: ht, h0'
-- 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
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
⊢ ⨍ (x : α), f x ∂μ ∈ interior s
have pos₁ : ∀ (ht : ⨍ (x : α), f x ∂μ ∈ interior s) (h0' : toMeasurable μ t =ᶠ[ae μ] univ), ⨍ (x : α), f x ∂μ ∈ interior s
Tactic: rwa [restrict_congr_set h0', restrict_univ] at ht
Cleared hypotheses: ht, h0'
-- 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 α
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 μ
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ ⨍ (x : α), f x ∂μ ∈ interior s
have this : ∀ {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
-- 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
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
have 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
Tactic: refine (ae_eq_const_or_exists_average_ne_compl hfi).imp_right ?_
-- 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 α
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) μ
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ g (⨍ (x : α), f x ∂μ) < ⨍ (x : α), g (f x) ∂μ
have 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) ∂μ
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
-- 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) ∂μ
⊢ f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ g (⨍ (x : α), f x ∂μ) < ⨍ (x : α), g (f x) ∂μ
have 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) ∂μ
Tactic: refine (ae_eq_const_or_exists_average_ne_compl hfi).imp_right ?_
-- 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 ∂μ)
⊢ g (⨍ (x : α), f x ∂μ) < ⨍ (x : α), g (f x) ∂μ
have 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) ∂μ
Tactic: rcases average_mem_openSegment_compl_self hm.nullMeasurableSet h₀ h₀' (hfi.prodMk hgi) with
    ⟨a, b, ha, hb, hab, h_avg⟩
-- 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 α
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) ∂μ
⊢ g (⨍ (x : α), f x ∂μ) < ⨍ (x : α), g (f x) ∂μ
have 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 ∂μ
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
Cleared hypotheses: h_avg
-- 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 (⨍ (x : α), f x ∂μ) < ⨍ (x : α), g (f x) ∂μ
have 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) ∂μ)
Tactic: rw [← h_avg.1, ← h_avg.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 α
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) ∂μ
⊢ 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