-- Mathlib/Analysis/Convex/Integral.lean
theorem Convex.average_mem_interior_of_set [IsFiniteMeasure μ] (hs : Convex ℝ s) (h0 : μ t ≠ 0)
    (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : Integrable f μ) (ht : (⨍ x in t, f x ∂μ) ∈ interior s) :
    (⨍ x, f x ∂μ) ∈ interior s

Proof state:
case neg
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
t : Set α
f : α → E
inst✝ : IsFiniteMeasure μ
hs : Convex ℝ s
h0 : μ (toMeasurable μ t) ≠ 0
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
ht : ⨍ (x : α) in toMeasurable μ t, f x ∂μ ∈ interior s
h0' : ¬μ (toMeasurable μ t)ᶜ = 0
⊢ ⨍ (x : α), f x ∂μ ∈ interior s

Tactic:
exact
  hs.openSegment_interior_closure_subset_interior ht
    (hs.set_average_mem_closure h0' (measure_ne_top _ _) (ae_restrict_of_ae hfs)
      hfi.integrableOn)
    (average_mem_openSegment_compl_self (measurableSet_toMeasurable μ t).nullMeasurableSet h0
      h0' hfi)

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
t : Set α
f : α → E
inst✝ : IsFiniteMeasure μ
hs : Convex ℝ s
h0 : μ (toMeasurable μ t) ≠ 0
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
ht : ⨍ (x : α) in t, f x ∂μ ∈ interior s
⊢ ⨍ (x : α), f x ∂μ ∈ interior s

Tactic:
rw [← restrict_toMeasurable (measure_ne_top μ t)] at ht

Result:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
t : Set α
f : α → E
inst✝ : IsFiniteMeasure μ
hs : Convex ℝ s
h0 : μ (toMeasurable μ t) ≠ 0
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
ht : ⨍ (x : α) in toMeasurable μ t, f x ∂μ ∈ interior s
⊢ ⨍ (x : α), f x ∂μ ∈ interior 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
t : Set α
f : α → E
inst✝ : IsFiniteMeasure μ
hs : Convex ℝ s
h0 : μ (toMeasurable μ t) ≠ 0
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
ht : ⨍ (x : α) in toMeasurable μ t, f x ∂μ ∈ interior s
⊢ ⨍ (x : α), f x ∂μ ∈ interior s

Tactic:
by_cases h0' : μ (toMeasurable μ t)ᶜ = 0

Result:
case pos
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
t : Set α
f : α → E
inst✝ : IsFiniteMeasure μ
hs : Convex ℝ s
h0 : μ (toMeasurable μ t) ≠ 0
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
ht : ⨍ (x : α) in toMeasurable μ t, f x ∂μ ∈ interior s
h0' : μ (toMeasurable μ t)ᶜ = 0
⊢ ⨍ (x : α), f x ∂μ ∈ interior s

case neg
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
t : Set α
f : α → E
inst✝ : IsFiniteMeasure μ
hs : Convex ℝ s
h0 : μ (toMeasurable μ t) ≠ 0
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
ht : ⨍ (x : α) in toMeasurable μ t, f x ∂μ ∈ interior s
h0' : ¬μ (toMeasurable μ t)ᶜ = 0
⊢ ⨍ (x : α), f x ∂μ ∈ interior 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
t : Set α
f : α → E
inst✝ : IsFiniteMeasure μ
hs : Convex ℝ s
h0 : μ t ≠ 0
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
ht : ⨍ (x : α) in t, f x ∂μ ∈ interior s
⊢ ⨍ (x : α), f x ∂μ ∈ interior s

Tactic:
rw [← measure_toMeasurable] at h0

Result:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
t : Set α
f : α → E
inst✝ : IsFiniteMeasure μ
hs : Convex ℝ s
h0 : μ (toMeasurable μ t) ≠ 0
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
ht : ⨍ (x : α) in t, f x ∂μ ∈ interior s
⊢ ⨍ (x : α), f x ∂μ ∈ interior s

Proof state:
case pos
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
t : Set α
f : α → E
inst✝ : IsFiniteMeasure μ
hs : Convex ℝ s
h0 : μ (toMeasurable μ t) ≠ 0
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
ht : ⨍ (x : α) in toMeasurable μ t, f x ∂μ ∈ interior s
h0' : μ (toMeasurable μ t)ᶜ = 0
⊢ ⨍ (x : α), f x ∂μ ∈ interior s

Tactic:
rw [← ae_eq_univ] at h0'

Result:
case pos
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
t : Set α
f : α → E
inst✝ : IsFiniteMeasure μ
hs : Convex ℝ s
h0 : μ (toMeasurable μ t) ≠ 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

Proof state:
case pos
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
t : Set α
f : α → E
inst✝ : IsFiniteMeasure μ
hs : Convex ℝ s
h0 : μ (toMeasurable μ t) ≠ 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

Tactic:
rwa [restrict_congr_set h0', restrict_univ] at ht

Result:
no goals