-- Mathlib/Analysis/Convex/Integral.lean
theorem Convex.integral_mem [IsProbabilityMeasure μ] (hs : Convex ℝ s) (hsc : IsClosed s)
    (hf : ∀ᵐ x ∂μ, f x ∈ s) (hfi : Integrable f μ) : (∫ x, f x ∂μ) ∈ s

Proof state:
case intro.intro.intro
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst✝ : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this✝ : SeparableSpace ↑(range g ∩ s)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure (range g ∩ s)
G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀
this : Tendsto (fun n => SimpleFunc.integral μ (G n)) atTop (𝓝 (∫ (x : α), g x ∂μ))
⊢ ∫ (a : α), g a ∂μ ∈ s

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

Result:
case intro.intro.intro.refine_1
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst✝ : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this✝ : SeparableSpace ↑(range g ∩ s)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure (range g ∩ s)
G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀
this : Tendsto (fun n => SimpleFunc.integral μ (G n)) atTop (𝓝 (∫ (x : α), g x ∂μ))
n : ℕ
⊢ ∀ i ∈ (G n).range, 0 ≤ (μ (⇑(G n) ⁻¹' {i})).toReal

case intro.intro.intro.refine_2
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst✝ : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this✝ : SeparableSpace ↑(range g ∩ s)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure (range g ∩ s)
G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀
this : Tendsto (fun n => SimpleFunc.integral μ (G n)) atTop (𝓝 (∫ (x : α), g x ∂μ))
n : ℕ
⊢ ∑ i ∈ (G n).range, (μ (⇑(G n) ⁻¹' {i})).toReal = 1

case intro.intro.intro.refine_3
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst✝ : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
g : α → E
hfi : Integrable g μ
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this✝ : SeparableSpace ↑(range g ∩ s)
y₀ : E
h₀ : y₀ ∈ range g ∩ s
hg : ∀ᵐ (x : α) ∂μ, g x ∈ closure (range g ∩ s)
G : ℕ → SimpleFunc α E := SimpleFunc.approxOn g ⋯ (range g ∩ s) y₀ h₀
this : Tendsto (fun n => SimpleFunc.integral μ (G n)) atTop (𝓝 (∫ (x : α), g x ∂μ))
n : ℕ
⊢ ∀ i ∈ (G n).range, ↑(ContinuousLinearMap.id ℝ E) i ∈ s

Proof state:
case intro.intro
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst✝ : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : α → E
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
⊢ ∫ (x : α), f x ∂μ ∈ s

Tactic:
haveI : SeparableSpace (range g ∩ s : Set E) :=
  (hgm.isSeparable_range.mono inter_subset_left).separableSpace

Result:
case intro.intro
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst✝ : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : α → E
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this : SeparableSpace ↑(range g ∩ s)
⊢ ∫ (x : α), f x ∂μ ∈ s

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
f : α → E
inst✝ : IsProbabilityMeasure μ
hs : Convex ℝ s
hsc : IsClosed s
hf : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : α → E
hgm : StronglyMeasurable g
hfg : f =ᶠ[ae μ] g
this : SeparableSpace ↑(range g ∩ s)
x₀ : α
h₀ : f x₀ ∈ s ∧ f x₀ = g x₀
⊢ f x₀ ∈ range g

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

Result:
no goals