-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem integrableOn_Iio_iff_integrableAtFilter_atBot_nhdsWithin
    [LinearOrder X] [CompactIccSpace X] [NoMinOrder X] [OrderTopology X] :
    IntegrableOn f (Iio a) μ ↔ IntegrableAtFilter f atBot μ ∧
    IntegrableAtFilter f (𝓝[<] a) μ ∧ LocallyIntegrableOn f (Iio a) μ

Proof state:
case mpr.intro.intro
X : Type u_1
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝³ : LinearOrder X
inst✝² : CompactIccSpace X
inst✝¹ : NoMinOrder X
inst✝ : OrderTopology X
hbot : IntegrableAtFilter f atBot μ
s : Set X
hsl : s ∈ 𝓝[<] a
hs : IntegrableOn f s μ
hlocal : LocallyIntegrableOn f (Iio a) μ
s' : X
hs'_mono : s' ∈ Iio a
hs' : Ioo s' a ⊆ s
⊢ IntegrableOn f (Iic s') μ

Tactic:
exact integrableOn_Iic_iff_integrableAtFilter_atBot.mpr
  ⟨hbot, hlocal.mono_set (Iic_subset_Iio.mpr hs'_mono)⟩

Result:
no goals

Proof state:
case mp
X : Type u_1
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝³ : LinearOrder X
inst✝² : CompactIccSpace X
inst✝¹ : NoMinOrder X
inst✝ : OrderTopology X
h : IntegrableOn f (Iio a) μ
⊢ IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f (𝓝[<] a) μ ∧ LocallyIntegrableOn f (Iio a) μ

Tactic:
exact ⟨⟨Iio a, Iio_mem_atBot a, h⟩, ⟨Iio a, self_mem_nhdsWithin, h⟩, h.locallyIntegrableOn⟩

Result:
no goals

Proof state:
case mpr
X : Type u_1
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝³ : LinearOrder X
inst✝² : CompactIccSpace X
inst✝¹ : NoMinOrder X
inst✝ : OrderTopology X
⊢ IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f (𝓝[<] a) μ ∧ LocallyIntegrableOn f (Iio a) μ →
    IntegrableOn f (Iio a) μ

Tactic:
intro ⟨hbot, ⟨s, hsl, hs⟩, hlocal⟩

Result:
case mpr
X : Type u_1
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝³ : LinearOrder X
inst✝² : CompactIccSpace X
inst✝¹ : NoMinOrder X
inst✝ : OrderTopology X
hbot : IntegrableAtFilter f atBot μ
s : Set X
hsl : s ∈ 𝓝[<] a
hs : IntegrableOn f s μ
hlocal : LocallyIntegrableOn f (Iio a) μ
⊢ IntegrableOn f (Iio a) μ

Proof state:
case mpr
X : Type u_1
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝³ : LinearOrder X
inst✝² : CompactIccSpace X
inst✝¹ : NoMinOrder X
inst✝ : OrderTopology X
hbot : IntegrableAtFilter f atBot μ
s : Set X
hsl : s ∈ 𝓝[<] a
hs : IntegrableOn f s μ
hlocal : LocallyIntegrableOn f (Iio a) μ
⊢ IntegrableOn f (Iio a) μ

Tactic:
obtain ⟨s', ⟨hs'_mono, hs'⟩⟩ := mem_nhdsLT_iff_exists_Ioo_subset.mp hsl

Result:
case mpr.intro.intro
X : Type u_1
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝³ : LinearOrder X
inst✝² : CompactIccSpace X
inst✝¹ : NoMinOrder X
inst✝ : OrderTopology X
hbot : IntegrableAtFilter f atBot μ
s : Set X
hsl : s ∈ 𝓝[<] a
hs : IntegrableOn f s μ
hlocal : LocallyIntegrableOn f (Iio a) μ
s' : X
hs'_mono : s' ∈ Iio a
hs' : Ioo s' a ⊆ s
⊢ IntegrableOn f (Iio a) μ

Proof state:
case mp
X : Type u_1
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝³ : LinearOrder X
inst✝² : CompactIccSpace X
inst✝¹ : NoMinOrder X
inst✝ : OrderTopology X
⊢ IntegrableOn f (Iio a) μ →
    IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f (𝓝[<] a) μ ∧ LocallyIntegrableOn f (Iio a) μ

Tactic:
intro h

Result:
case mp
X : Type u_1
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝³ : LinearOrder X
inst✝² : CompactIccSpace X
inst✝¹ : NoMinOrder X
inst✝ : OrderTopology X
h : IntegrableOn f (Iio a) μ
⊢ IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f (𝓝[<] a) μ ∧ LocallyIntegrableOn f (Iio a) μ

Proof state:
X : Type u_1
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝³ : LinearOrder X
inst✝² : CompactIccSpace X
inst✝¹ : NoMinOrder X
inst✝ : OrderTopology X
⊢ IntegrableOn f (Iio a) μ ↔
    IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f (𝓝[<] a) μ ∧ LocallyIntegrableOn f (Iio a) μ

Tactic:
constructor

Result:
case mp
X : Type u_1
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝³ : LinearOrder X
inst✝² : CompactIccSpace X
inst✝¹ : NoMinOrder X
inst✝ : OrderTopology X
⊢ IntegrableOn f (Iio a) μ →
    IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f (𝓝[<] a) μ ∧ LocallyIntegrableOn f (Iio a) μ

case mpr
X : Type u_1
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝³ : LinearOrder X
inst✝² : CompactIccSpace X
inst✝¹ : NoMinOrder X
inst✝ : OrderTopology X
⊢ IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f (𝓝[<] a) μ ∧ LocallyIntegrableOn f (Iio a) μ →
    IntegrableOn f (Iio a) μ

Proof state:
case mpr.intro.intro
X : Type u_1
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝³ : LinearOrder X
inst✝² : CompactIccSpace X
inst✝¹ : NoMinOrder X
inst✝ : OrderTopology X
hbot : IntegrableAtFilter f atBot μ
s : Set X
hsl : s ∈ 𝓝[<] a
hs : IntegrableOn f s μ
hlocal : LocallyIntegrableOn f (Iio a) μ
s' : X
hs'_mono : s' ∈ Iio a
hs' : Ioo s' a ⊆ s
⊢ IntegrableOn f (Iio a) μ

Tactic:
refine (integrableOn_union.mpr ⟨?_, hs.mono hs' le_rfl⟩).mono Iio_subset_Iic_union_Ioo le_rfl

Result:
case mpr.intro.intro
X : Type u_1
E : Type u_3
inst✝⁶ : MeasurableSpace X
inst✝⁵ : TopologicalSpace X
inst✝⁴ : NormedAddCommGroup E
f : X → E
μ : Measure X
a : X
inst✝³ : LinearOrder X
inst✝² : CompactIccSpace X
inst✝¹ : NoMinOrder X
inst✝ : OrderTopology X
hbot : IntegrableAtFilter f atBot μ
s : Set X
hsl : s ∈ 𝓝[<] a
hs : IntegrableOn f s μ
hlocal : LocallyIntegrableOn f (Iio a) μ
s' : X
hs'_mono : s' ∈ Iio a
hs' : Ioo s' a ⊆ s
⊢ IntegrableOn f (Iic s') μ