-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem intervalIntegral_tendsto_integral_Iic (b : ℝ) (hfi : IntegrableOn f (Iic b) μ)
    (ha : Tendsto a l atBot) :
    Tendsto (fun i => ∫ x in a i..b, f x ∂μ) l (𝓝 <| ∫ x in Iic b, f x ∂μ)

Proof state:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
b : ℝ
hfi : IntegrableOn f (Iic b) μ
ha : Tendsto a l atBot
φ : ι → Set ℝ := fun i => Ioi (a i)
hφ : AECover (μ.restrict (Iic b)) l φ
⊢ (fun i => ∫ (x : ℝ) in φ i, f x ∂μ.restrict (Iic b)) =ᶠ[l] fun i => ∫ (x : ℝ) in a i..b, f x ∂μ

Tactic:
filter_upwards [ha.eventually (eventually_le_atBot <| b)] with i hai

Result:
case h
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
b : ℝ
hfi : IntegrableOn f (Iic b) μ
ha : Tendsto a l atBot
φ : ι → Set ℝ := fun i => Ioi (a i)
hφ : AECover (μ.restrict (Iic b)) l φ
i : ι
hai : a i ≤ b
⊢ ∫ (x : ℝ) in φ i, f x ∂μ.restrict (Iic b) = ∫ (x : ℝ) in a i..b, f x ∂μ

Proof state:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
b : ℝ
hfi : IntegrableOn f (Iic b) μ
ha : Tendsto a l atBot
φ : ι → Set ℝ := fun i => Ioi (a i)
⊢ Tendsto (fun i => ∫ (x : ℝ) in a i..b, f x ∂μ) l (𝓝 (∫ (x : ℝ) in Iic b, f x ∂μ))

Tactic:
have hφ : AECover (μ.restrict <| Iic b) l φ := aecover_Ioi ha

Result:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
b : ℝ
hfi : IntegrableOn f (Iic b) μ
ha : Tendsto a l atBot
φ : ι → Set ℝ := fun i => Ioi (a i)
hφ : AECover (μ.restrict (Iic b)) l φ
⊢ Tendsto (fun i => ∫ (x : ℝ) in a i..b, f x ∂μ) l (𝓝 (∫ (x : ℝ) in Iic b, f x ∂μ))

Proof state:
case h
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
b : ℝ
hfi : IntegrableOn f (Iic b) μ
ha : Tendsto a l atBot
φ : ι → Set ℝ := fun i => Ioi (a i)
hφ : AECover (μ.restrict (Iic b)) l φ
i : ι
hai : a i ≤ b
⊢ ∫ (x : ℝ) in φ i ∩ Iic b, f x ∂μ = ∫ (x : ℝ) in Ioc (a i) b, f x ∂μ

Tactic:
rfl

Result:
no goals

Proof state:
case h
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
b : ℝ
hfi : IntegrableOn f (Iic b) μ
ha : Tendsto a l atBot
φ : ι → Set ℝ := fun i => Ioi (a i)
hφ : AECover (μ.restrict (Iic b)) l φ
i : ι
hai : a i ≤ b
⊢ ∫ (x : ℝ) in φ i, f x ∂μ.restrict (Iic b) = ∫ (x : ℝ) in a i..b, f x ∂μ

Tactic:
rw [intervalIntegral.integral_of_le hai, Measure.restrict_restrict (hφ.measurableSet i)]

Result:
case h
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
b : ℝ
hfi : IntegrableOn f (Iic b) μ
ha : Tendsto a l atBot
φ : ι → Set ℝ := fun i => Ioi (a i)
hφ : AECover (μ.restrict (Iic b)) l φ
i : ι
hai : a i ≤ b
⊢ ∫ (x : ℝ) in φ i ∩ Iic b, f x ∂μ = ∫ (x : ℝ) in Ioc (a i) b, f x ∂μ

Proof state:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
b : ℝ
hfi : IntegrableOn f (Iic b) μ
ha : Tendsto a l atBot
φ : ι → Set ℝ := fun i => Ioi (a i)
hφ : AECover (μ.restrict (Iic b)) l φ
⊢ Tendsto (fun i => ∫ (x : ℝ) in a i..b, f x ∂μ) l (𝓝 (∫ (x : ℝ) in Iic b, f x ∂μ))

Tactic:
refine (hφ.integral_tendsto_of_countably_generated hfi).congr' ?_

Result:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
b : ℝ
hfi : IntegrableOn f (Iic b) μ
ha : Tendsto a l atBot
φ : ι → Set ℝ := fun i => Ioi (a i)
hφ : AECover (μ.restrict (Iic b)) l φ
⊢ (fun i => ∫ (x : ℝ) in φ i, f x ∂μ.restrict (Iic b)) =ᶠ[l] fun i => ∫ (x : ℝ) in a i..b, f x ∂μ

Proof state:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
b : ℝ
hfi : IntegrableOn f (Iic b) μ
ha : Tendsto a l atBot
⊢ Tendsto (fun i => ∫ (x : ℝ) in a i..b, f x ∂μ) l (𝓝 (∫ (x : ℝ) in Iic b, f x ∂μ))

Tactic:
let φ i := Ioi (a i)

Result:
ι : Type u_1
E : Type u_2
μ : Measure ℝ
l : Filter ι
inst✝² : l.IsCountablyGenerated
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a : ι → ℝ
f : ℝ → E
b : ℝ
hfi : IntegrableOn f (Iic b) μ
ha : Tendsto a l atBot
φ : ι → Set ℝ := fun i => Ioi (a i)
⊢ Tendsto (fun i => ∫ (x : ℝ) in a i..b, f x ∂μ) l (𝓝 (∫ (x : ℝ) in Iic b, f x ∂μ))