-- Mathlib/Probability/Moments/IntegrableExpMul.lean
/-- If the interior of the interval `integrableExpSet X μ` is nonempty,
then `X` is a.e. measurable. -/
lemma aemeasurable_of_mem_interior_integrableExpSet (hv : v ∈ interior (integrableExpSet X μ)) :
    AEMeasurable X μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : ∃ l u, v ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ integrableExpSet X μ
⊢ AEMeasurable X μ

Tactic:
obtain ⟨l, u, hvlu, h_subset⟩ := hv

Result:
case intro.intro.intro
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
⊢ AEMeasurable X μ

Proof state:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((v - l) ⊓ (u - v)) / 2
h_pos : 0 < (v - l) ⊓ (u - v)
ht : 0 < t
hvt : ¬v + t = 0
⊢ AEMeasurable X μ

Tactic:
exact aemeasurable_of_aemeasurable_exp_mul hvt
  (h_subset (add_half_inf_sub_mem_Ioo hvlu)).aemeasurable

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((v - l) ⊓ (u - v)) / 2
h_pos : 0 < (v - l) ⊓ (u - v)
ht : 0 < t
hvt : v + t = 0
⊢ v ≠ t

Tactic:
refine fun h_eq ↦ ht.ne' ?_

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((v - l) ⊓ (u - v)) / 2
h_pos : 0 < (v - l) ⊓ (u - v)
ht : 0 < t
hvt : v + t = 0
h_eq : v = t
⊢ t = 0

Proof state:
case intro.intro.intro
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
⊢ AEMeasurable X μ

Tactic:
let t := ((v - l) ⊓ (u - v)) / 2

Result:
case intro.intro.intro
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((v - l) ⊓ (u - v)) / 2
⊢ AEMeasurable X μ

Proof state:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((v - l) ⊓ (u - v)) / 2
h_pos : 0 < (v - l) ⊓ (u - v)
ht : 0 < t
hvt : v + t = 0
hvt' : v - t ≠ 0
⊢ AEMeasurable X μ

Tactic:
exact aemeasurable_of_aemeasurable_exp_mul hvt'
  (h_subset (sub_half_inf_sub_mem_Ioo hvlu)).aemeasurable

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((v - l) ⊓ (u - v)) / 2
⊢ 0 < (v - l) ⊓ (u - v)

Tactic:
simp [hvlu.1, hvlu.2]

Result:
no goals

Proof state:
case intro.intro.intro
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((v - l) ⊓ (u - v)) / 2
h_pos : 0 < (v - l) ⊓ (u - v)
ht : 0 < t
⊢ AEMeasurable X μ

Tactic:
by_cases hvt : v + t = 0

Result:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((v - l) ⊓ (u - v)) / 2
h_pos : 0 < (v - l) ⊓ (u - v)
ht : 0 < t
hvt : v + t = 0
⊢ AEMeasurable X μ

case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((v - l) ⊓ (u - v)) / 2
h_pos : 0 < (v - l) ⊓ (u - v)
ht : 0 < t
hvt : ¬v + t = 0
⊢ AEMeasurable X μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((v - l) ⊓ (u - v)) / 2
h_pos : 0 < (v - l) ⊓ (u - v)
ht : 0 < t
hvt : v + t = 0
h_eq : v = t
⊢ t = 0

Tactic:
simpa [h_eq] using hvt

Result:
no goals

Proof state:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((v - l) ⊓ (u - v)) / 2
h_pos : 0 < (v - l) ⊓ (u - v)
ht : 0 < t
hvt : v + t = 0
⊢ AEMeasurable X μ

Tactic:
have hvt' : v - t ≠ 0 := by
  rw [sub_ne_zero]
  refine fun h_eq ↦ ht.ne' ?_
  simpa [h_eq] using hvt

Result:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((v - l) ⊓ (u - v)) / 2
h_pos : 0 < (v - l) ⊓ (u - v)
ht : 0 < t
hvt : v + t = 0
hvt' : v - t ≠ 0
⊢ AEMeasurable X μ

Proof state:
case intro.intro.intro
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((v - l) ⊓ (u - v)) / 2
⊢ AEMeasurable X μ

Tactic:
have h_pos : 0 < (v - l) ⊓ (u - v) := by simp [hvlu.1, hvlu.2]

Result:
case intro.intro.intro
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((v - l) ⊓ (u - v)) / 2
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ AEMeasurable X μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
⊢ AEMeasurable X μ

Tactic:
rw [mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset] at hv

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : ∃ l u, v ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ integrableExpSet X μ
⊢ AEMeasurable X μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((v - l) ⊓ (u - v)) / 2
h_pos : 0 < (v - l) ⊓ (u - v)
ht : 0 < t
hvt : v + t = 0
⊢ v - t ≠ 0

Tactic:
rw [sub_ne_zero]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((v - l) ⊓ (u - v)) / 2
h_pos : 0 < (v - l) ⊓ (u - v)
ht : 0 < t
hvt : v + t = 0
⊢ v ≠ t

Proof state:
case intro.intro.intro
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((v - l) ⊓ (u - v)) / 2
h_pos : 0 < (v - l) ⊓ (u - v)
⊢ AEMeasurable X μ

Tactic:
have ht : 0 < t := half_pos h_pos

Result:
case intro.intro.intro
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := ((v - l) ⊓ (u - v)) / 2
h_pos : 0 < (v - l) ⊓ (u - v)
ht : 0 < t
⊢ AEMeasurable X μ