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
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
rcases : ∀ (x₀ : α) (h₀ : f x₀ ∈ s ∧ f x₀ = g x₀), (range g ∩ s).Nonempty
⊢ (range g ∩ s).Nonempty

Tactic:
rcases (hf.and hfg).exists with ⟨x₀, h₀⟩

Premises used: Filter.Eventually.and, Filter.Eventually.exists
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
x₀ : α
h₀ : f x₀ ∈ s ∧ f x₀ = g x₀
⊢ f x₀ ∈ range g

Tactic:
simp only [h₀.2, mem_range_self]

Premises used: Set.mem_range_self, 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
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
x₀ : α
h₀ : f x₀ ∈ s ∧ f x₀ = g x₀
⊢ (range g ∩ s).Nonempty

Tactic:
exact ⟨f x₀, by simp only [h₀.2, mem_range_self], h₀.1⟩
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
obtain : ∀ (y₀ : E) (h₀ : y₀ ∈ range g ∩ s), ∫ (x : α), f x ∂μ ∈ s
⊢ ∫ (x : α), f x ∂μ ∈ s

Tactic:
obtain ⟨y₀, h₀⟩ : (range g ∩ s).Nonempty := by
    rcases (hf.and hfg).exists with ⟨x₀, h₀⟩
    exact ⟨f x₀, by simp only [h₀.2, mem_range_self], h₀.1⟩

Premises used: Inter.inter, Set.Nonempty, Set.range
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
rw : ∫ (a : α), g a ∂μ ∈ s
⊢ ∫ (x : α), f x ∂μ ∈ s

Tactic:
rw [integral_congr_ae hfg]

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
rw :
  ∀ (hfi : Integrable g μ) (hgm : StronglyMeasurable g) (hfg : f =ᶠ[ae μ] g)
    (this : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)) (y₀ : E) (h₀ : y₀ ∈ range g ∩ s), ∫ (a : α), g a ∂μ ∈ s
⊢ ∫ (a : α), g a ∂μ ∈ s

Tactic:
rw [integrable_congr hfg] at hfi

Premises used: MeasureTheory.integrable_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 α
s : Set E
f : α → E
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
h : ∀ (x : α) (hx : g x ∈ s), g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)
⊢ ∀ᵐ (x : α) ∂μ, g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)

Tactic:
filter_upwards [hfg.rw (fun _ y => y ∈ s) hf] with x hx

Premises used: Membership.mem, Filter.EventuallyEq.rw
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
x : α
hx : g x ∈ s
h : g x ∈ range g ∩ s
⊢ g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)

Tactic:
apply subset_closure

Premises used: subset_closure
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
x : α
hx : g x ∈ s
⊢ g x ∈ range g ∩ s

Tactic:
⟨mem_range_self _, hx⟩

Premises used: Set.mem_range_self, Set.Mem, setOf, Set.inter, And.intro
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
x : α
hx : g x ∈ s
⊢ g x ∈ range g ∩ s

Tactic:
exact ⟨mem_range_self _, hx⟩
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
⊢ ∀ᵐ (x : α) ∂μ, g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)

Tactic:
have hg : ∀ᵐ x ∂μ, g x ∈ closure (range g ∩ s) := by
    filter_upwards [hfg.rw (fun _ y => y ∈ s) hf] with x hx
    apply subset_closure
    exact ⟨mem_range_self _, hx⟩
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this_3 : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)
G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀
this : Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral μ (G n)) atTop (𝓝 (∫ (x : α), g x ∂μ))
⊢ ∫ (a : α), g a ∂μ ∈ s

Tactic:
hsc.mem_of_tendsto this (Eventually.of_forall fun n => hs.sum_mem ?_ ?_ ?_)

Premises used: IsClosed.mem_of_tendsto, Filter.Eventually.of_forall, Convex.sum_mem
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this_3 : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)
G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀
this : Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral μ (G n)) atTop (𝓝 (∫ (x : α), g x ∂μ))
refine_1 : ∀ (n : ℕ), ∀ i ∈ (G n).range, 0 ≤ μ.real (preimage (β := E) (⇑(G n) : (a : α) → E) {i})
refine_2 : ∀ (n : ℕ), Eq (α := ℝ) (∑ i ∈ (G n).range, μ.real (preimage (β := E) (⇑(G n) : (a : α) → E) {i})) 1
refine_3 :
  ∀ (n : ℕ),
    ∀ i ∈ (G n).range, Membership.mem (α := E) s (((↑(ContinuousLinearMap.id ℝ E) : E →ₗ[ℝ] E) : (a : E) → E) i : E)
⊢ ∫ (a : α), g a ∂μ ∈ s

Tactic:
refine hsc.mem_of_tendsto this (Eventually.of_forall fun n => hs.sum_mem ?_ ?_ ?_)

Premises used: IsClosed.mem_of_tendsto, Filter.Eventually.of_forall, Convex.sum_mem
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this_3 : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)
G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀
this : Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral μ (G n)) atTop (𝓝 (∫ (x : α), g x ∂μ))
n : ℕ
⊢ ∀ i ∈ (G n).range, 0 ≤ μ.real (preimage (β := E) (⇑(G n) : (a : α) → E) {i})

Tactic:
fun _ _ => ENNReal.toReal_nonneg

Premises used: MeasureTheory.Measure.real, ENNReal.toReal_nonneg
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this_3 : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)
G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀
this : Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral μ (G n)) atTop (𝓝 (∫ (x : α), g x ∂μ))
n : ℕ
⊢ ∀ i ∈ (G n).range, 0 ≤ μ.real (preimage (β := E) (⇑(G n) : (a : α) → E) {i})

Tactic:
exact fun _ _ => ENNReal.toReal_nonneg

Premises used: ENNReal.toReal_nonneg
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this_3 : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)
G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀
this : Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral μ (G n)) atTop (𝓝 (∫ (x : α), g x ∂μ))
n : ℕ
refine_2 :
  ∀ a ∈ (G n).range,
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := E) (⇑(G n) : (a : α) → E) {a}) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ)
    (∑ x ∈ (G n).range, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := E) (⇑(G n) : (a : α) → E) {x}))) 1

Tactic:
rw [← ENNReal.toReal_sum, (G n).sum_range_measure_preimage_singleton, measure_univ,
      ENNReal.toReal_one]

Premises used: ENNReal.toReal_one, MeasureTheory.IsProbabilityMeasure.measure_univ, ENNReal.toReal_sum, MeasureTheory.SimpleFunc.sum_range_measure_preimage_singleton
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this_3 : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)
G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀
this : Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral μ (G n)) atTop (𝓝 (∫ (x : α), g x ∂μ))
n : ℕ
⊢ ∀ a ∈ (G n).range,
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := E) (⇑(G n) : (a : α) → E) {a}) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this_3 : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)
G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀
this : Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral μ (G n)) atTop (𝓝 (∫ (x : α), g x ∂μ))
n : ℕ
refine_3 :
  ∀ (i : α),
    Membership.mem (α := E) s
      (((↑(ContinuousLinearMap.id ℝ E) : E →ₗ[ℝ] E) : (a : E) → E) ((G n : (a : α) → E) i : E) : E)
⊢ ∀ i ∈ (G n).range, Membership.mem (α := E) s (((↑(ContinuousLinearMap.id ℝ E) : E →ₗ[ℝ] E) : (a : E) → E) i : E)

Tactic:
simp only [SimpleFunc.mem_range, forall_mem_range]

Premises used: Set.forall_mem_range, MeasureTheory.SimpleFunc.mem_range
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this_3 : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)
G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀
this : Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral μ (G n)) atTop (𝓝 (∫ (x : α), g x ∂μ))
n : ℕ
x : α
refine_3 :
  Membership.mem (α := E) (range g ∩ s)
    (((↑(ContinuousLinearMap.id ℝ E) : E →ₗ[ℝ] E) : (a : E) → E) ((G n : (a : α) → E) x : E) : E)
⊢ Membership.mem (α := E) s
    (((↑(ContinuousLinearMap.id ℝ E) : E →ₗ[ℝ] E) : (a : E) → E) ((G n : (a : α) → E) x : E) : E)

Tactic:
apply (range g).inter_subset_right

Premises used: Set.inter_subset_right
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this_3 : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)
G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀
this : Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral μ (G n)) atTop (𝓝 (∫ (x : α), g x ∂μ))
n : ℕ
x : α
⊢ Membership.mem (α := E) (range g ∩ s)
    (((↑(ContinuousLinearMap.id ℝ E) : E →ₗ[ℝ] E) : (a : E) → E) ((G n : (a : α) → E) x : E) : E)

Tactic:
SimpleFunc.approxOn_mem hgm.measurable h₀ _ _

Premises used: Set.Mem, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.SimpleFunc.approxOn_mem
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this_3 : SeparableSpace.{u_2} (↑(range g ∩ s) : Type u_2)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range g ∩ s)
G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀
this : Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ SimpleFunc.integral μ (G n)) atTop (𝓝 (∫ (x : α), g x ∂μ))
n : ℕ
x : α
⊢ Membership.mem (α := E) (range g ∩ s)
    (((↑(ContinuousLinearMap.id ℝ E) : E →ₗ[ℝ] E) : (a : E) → E) ((G n : (a : α) → E) x : E) : E)

Tactic:
exact SimpleFunc.approxOn_mem hgm.measurable h₀ _ _

Premises used: MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.SimpleFunc.approxOn_mem
-- Module: Mathlib.Analysis.Convex.Integral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst_3 : IsFiniteMeasure μ
inst_4 : NeZero μ
hs : Convex ℝ s
hsc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
⊢ ⨍ (x : α), f x ∂μ ∈ s

Tactic:
hs.integral_mem hsc (ae_mono' smul_absolutelyContinuous hfs) hfi.to_average

Premises used: Convex.integral_mem, Set.Mem, MeasureTheory.average, MeasureTheory.Integrable.to_average, MeasureTheory.Measure.smul_absolutelyContinuous, MeasureTheory.Measure.ae_mono'
-- 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
hs : Convex ℝ 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 μ
⊢ ⨍ (x : α) in t, f x ∂μ ∈ s

Tactic:
have := Fact.mk ht.lt_top
  have := NeZero.mk h0
  hs.average_mem hsc hfs hfi

Premises used: NeZero.mk, Fact.mk, Ne.lt_top, Convex.average_mem
-- 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
hs : Convex ℝ 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 μ
⊢ ⨍ (x : α) in t, f x ∂μ ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s

Tactic:
hs.closure.set_average_mem isClosed_closure h0 ht (hfs.mono fun _ hx => subset_closure hx) hfi

Premises used: subset_closure, Convex.closure, Filter.Eventually.mono, Convex.set_average_mem, isClosed_closure
-- 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) μ
⊢ ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set (E × ℝ)) {p : E × ℝ | p.1 ∈ s ∧ g p.1 ≤ p.2} (f x, g (f x))

Tactic:
have ht_mem : ∀ᵐ x ∂μ, (f x, g (f x)) ∈ {p : E × ℝ | p.1 ∈ s ∧ g p.1 ≤ p.2} :=
    hfs.mono fun x hx => ⟨hx, le_rfl⟩
-- 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:
average_pair hfi hgi ▸
    hg.convex_epigraph.average_mem (hsc.epigraph hgc) ht_mem (hfi.prodMk hgi)

Premises used: Set.Mem, setOf, Eq.rec, ConvexOn.convex_epigraph, IsClosed.epigraph, MeasureTheory.average_pair, Convex.average_mem, MeasureTheory.Integrable.prodMk