-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem integrableOn_Ioc_of_intervalIntegral_norm_bounded {I a₀ b₀ : ℝ}
    (hfi : ∀ i, IntegrableOn f <| Ioc (a i) (b i)) (ha : Tendsto a l <| 𝓝 a₀)
    (hb : Tendsto b l <| 𝓝 b₀) (h : ∀ᶠ i in l, (∫ x in Ioc (a i) (b i), ‖f x‖) ≤ I) :
    IntegrableOn f (Ioc a₀ b₀)

Proof state:
case refine_1.a
ι : Type u_1
E : Type u_2
l : Filter ι
inst✝² : l.NeBot
inst✝¹ : l.IsCountablyGenerated
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) volume
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
i : ι
hi : ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
⊢ ∀ (a : ℝ), 0 a ≤ (fun x => ‖f x‖) a

Tactic:
simp only [Pi.zero_apply, norm_nonneg, forall_const]

Result:
no goals

Proof state:
ι : Type u_1
E : Type u_2
l : Filter ι
inst✝² : l.NeBot
inst✝¹ : l.IsCountablyGenerated
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) volume
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
i : ι
hi : ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
⊢ ∫ (x : ℝ) in Ioc (a i) (b i) ∩ Ioc a₀ b₀, ‖f x‖ ∂volume ≤ I

Tactic:
refine le_trans (setIntegral_mono_set (hfi i).norm ?_ ?_) hi <;> apply ae_of_all

Result:
case refine_1.a
ι : Type u_1
E : Type u_2
l : Filter ι
inst✝² : l.NeBot
inst✝¹ : l.IsCountablyGenerated
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) volume
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
i : ι
hi : ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
⊢ ∀ (a : ℝ), 0 a ≤ (fun x => ‖f x‖) a

case refine_2.a
ι : Type u_1
E : Type u_2
l : Filter ι
inst✝² : l.NeBot
inst✝¹ : l.IsCountablyGenerated
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) volume
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
i : ι
hi : ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
⊢ ∀ (a_1 : ℝ), (Ioc (a i) (b i) ∩ Ioc a₀ b₀) a_1 ≤ Ioc (a i) (b i) a_1

Proof state:
case refine_2.a
ι : Type u_1
E : Type u_2
l : Filter ι
inst✝² : l.NeBot
inst✝¹ : l.IsCountablyGenerated
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) volume
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
i : ι
hi : ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
⊢ ∀ (a_1 : ℝ), (Ioc (a i) (b i) ∩ Ioc a₀ b₀) a_1 ≤ Ioc (a i) (b i) a_1

Tactic:
intro c hc

Result:
case refine_2.a
ι : Type u_1
E : Type u_2
l : Filter ι
inst✝² : l.NeBot
inst✝¹ : l.IsCountablyGenerated
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) volume
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
i : ι
hi : ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
c : ℝ
hc : (Ioc (a i) (b i) ∩ Ioc a₀ b₀) c
⊢ Ioc (a i) (b i) c

Proof state:
ι : Type u_1
E : Type u_2
l : Filter ι
inst✝² : l.NeBot
inst✝¹ : l.IsCountablyGenerated
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) volume
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
i : ι
hi : ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
⊢ ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ∂volume.restrict (Ioc a₀ b₀) ≤ I

Tactic:
rw [Measure.restrict_restrict measurableSet_Ioc]

Result:
ι : Type u_1
E : Type u_2
l : Filter ι
inst✝² : l.NeBot
inst✝¹ : l.IsCountablyGenerated
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) volume
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
i : ι
hi : ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
⊢ ∫ (x : ℝ) in Ioc (a i) (b i) ∩ Ioc a₀ b₀, ‖f x‖ ∂volume ≤ I

Proof state:
ι : Type u_1
E : Type u_2
l : Filter ι
inst✝² : l.NeBot
inst✝¹ : l.IsCountablyGenerated
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) volume
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
⊢ IntegrableOn f (Ioc a₀ b₀) volume

Tactic:
refine (aecover_Ioc_of_Ioc ha hb).integrable_of_integral_norm_bounded I
  (fun i => (hfi i).restrict measurableSet_Ioc) (h.mono fun i hi ↦ ?_)

Result:
ι : Type u_1
E : Type u_2
l : Filter ι
inst✝² : l.NeBot
inst✝¹ : l.IsCountablyGenerated
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) volume
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
i : ι
hi : ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
⊢ ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ∂volume.restrict (Ioc a₀ b₀) ≤ I

Proof state:
case refine_2.a
ι : Type u_1
E : Type u_2
l : Filter ι
inst✝² : l.NeBot
inst✝¹ : l.IsCountablyGenerated
inst✝ : NormedAddCommGroup E
a b : ι → ℝ
f : ℝ → E
I a₀ b₀ : ℝ
hfi : ∀ (i : ι), IntegrableOn f (Ioc (a i) (b i)) volume
ha : Tendsto a l (𝓝 a₀)
hb : Tendsto b l (𝓝 b₀)
h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
i : ι
hi : ∫ (x : ℝ) in Ioc (a i) (b i), ‖f x‖ ≤ I
c : ℝ
hc : (Ioc (a i) (b i) ∩ Ioc a₀ b₀) c
⊢ Ioc (a i) (b i) c

Tactic:
exact hc.1

Result:
no goals