-- Module: Mathlib.MeasureTheory.Integral.DominatedConvergence
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this_1 : IsCompact (SProd.sprod (α := Set X) {q} (Icc a b))
M : ℝ
hM :
  Membership.mem (γ := Set ℝ)
    (upperBounds ((fun (x : X × ℝ) ↦ ‖Function.uncurry f x‖) '' SProd.sprod (α := Set X) {q} (Icc a b))) M
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
t :
  ‖HSub.hSub (α := E) (∫ (t : ℝ) in a₀..s, f p t ∂μ) (∫ (t : ℝ) in a₀..b₀, f q t ∂μ)‖ =
    ‖HSub.hSub (α := E) (∫ (t : ℝ) in a₀..s, f p t ∂μ) (∫ (t : ℝ) in a₀..b₀, f p t ∂μ) +
        HSub.hSub (α := E) (∫ (t : ℝ) in a₀..b₀, f p t ∂μ) (∫ (t : ℝ) in a₀..b₀, f q t ∂μ)‖
t₁ :
  ‖HSub.hSub (α := E) (∫ (t : ℝ) in a₀..s, f p t ∂μ) (∫ (t : ℝ) in a₀..b₀, f p t ∂μ)‖ +
      ‖HSub.hSub (α := E) (∫ (t : ℝ) in a₀..b₀, f p t ∂μ) (∫ (t : ℝ) in a₀..b₀, f q t ∂μ)‖ =
    norm.{u_1} (E := E) (∫ (t : ℝ) in b₀..s, f p t ∂μ) + norm.{u_1} (E := E) (∫ (t : ℝ) in a₀..b₀, f p t - f q t ∂μ)
t₂ :
  norm.{u_1} (E := E) (∫ (t : ℝ) in b₀..s, f p t ∂μ) + norm.{u_1} (E := E) (∫ (t : ℝ) in a₀..b₀, f p t - f q t ∂μ) ≤
    HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Ι b₀ s, ‖f p t‖ ∂μ) (∫ (t : ℝ) in Ι a₀ b₀, ‖f p t - f q t‖ ∂μ)
t₃ :
  HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Ι b₀ s, ‖f p t‖ ∂μ) (∫ (t : ℝ) in Ι a₀ b₀, ‖f p t - f q t‖ ∂μ) ≤
    HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), ‖f p t‖ ∂μ) (∫ (t : ℝ) in Icc a b, ‖f p t - f q t‖ ∂μ)
t₄ :
  HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), ‖f p t‖ ∂μ) (∫ (t : ℝ) in Icc a b, ‖f p t - f q t‖ ∂μ) ≤
    HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), M + 1 ∂μ) (∫ (_t : ℝ) in Icc a b, δ ∂μ)
t₅ :
  HAdd.hAdd (α := ℝ) (∫ (t : ℝ) in Icc (b₀ - δ) (b₀ + δ), M + 1 ∂μ) (∫ (_t : ℝ) in Icc a b, δ ∂μ) =
    (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b)
⊢ ‖HSub.hSub (α := E) (∫ (t : ℝ) in a₀..s, f p t ∂μ) (∫ (t : ℝ) in a₀..b₀, f q t ∂μ)‖ < ε

Tactic:
calc
  ‖∫ t in a₀..s, f p t ∂μ - ∫ t in a₀..b₀, f q t ∂μ‖
    = ‖(∫ t in a₀..s, f p t ∂μ - ∫ t in a₀..b₀, f p t ∂μ)
        + (∫ t in a₀..b₀, f p t ∂μ - ∫ t in a₀..b₀, f q t ∂μ)‖ := by congr 1; abel
  _ ≤ ‖∫ t in a₀..s, f p t ∂μ - ∫ t in a₀..b₀, f p t ∂μ‖
        + ‖∫ t in a₀..b₀, f p t ∂μ - ∫ t in a₀..b₀, f q t ∂μ‖ := norm_add_le _ _
  _ = ‖∫ t in b₀..s, f p t ∂μ‖ + ‖∫ t in a₀..b₀, (f p t - f q t) ∂μ‖ := by
      congr 2
      · rw [integral_interval_sub_left (J _ _ _) (J _ _ _)]
      · rw [integral_sub (J _ _ _) (J _ _ _)]
  _ ≤ ∫ t in Ι b₀ s, ‖f p t‖ ∂μ + ∫ t in Ι a₀ b₀, ‖f p t - f q t‖ ∂μ := by
      gcongr
      · exact norm_integral_le_integral_norm_uIoc
      · exact norm_integral_le_integral_norm_uIoc
  _ ≤ ∫ t in Icc (b₀ - δ) (b₀ + δ), ‖f p t‖ ∂μ + ∫ t in Icc a b, ‖f p t - f q t‖ ∂μ := by
      gcongr
      · exact Eventually.of_forall (fun x ↦ norm_nonneg _)
      · exact (hf.uncurry_left _).norm.integrableOn_Icc
      · apply uIoc_subset_uIcc.trans (uIcc_subset_Icc ?_ ⟨hs.1.le, hs.2.le⟩ )
        simp [δpos.le]
      · exact Eventually.of_forall (fun x ↦ norm_nonneg _)
      · exact ((hf.uncurry_left _).sub (hf.uncurry_left _)).norm.integrableOn_Icc
      · exact uIoc_subset_uIcc.trans (uIcc_subset_Icc ⟨a_lt.1.le, lt_b.1.le⟩ ⟨a_lt.2.le, lt_b.2.le⟩)
  _ ≤ ∫ t in Icc (b₀ - δ) (b₀ + δ), M + 1 ∂μ + ∫ _t in Icc a b, δ ∂μ := by
      gcongr with x hx x hx
      · exact (hf.uncurry_left _).norm.integrableOn_Icc
      · exact continuous_const.integrableOn_Icc
      · exact nullMeasurableSet_Icc
      · calc ‖f p x‖ = ‖f q x + (f p x - f q x)‖ := by congr; abel
        _ ≤ ‖f q x‖ + ‖f p x - f q x‖ := norm_add_le _ _
        _ ≤ M + δ := by
            gcongr
            · apply hM
              change (fun x ↦ ‖Function.uncurry f x‖) (q, x) ∈ _
              apply mem_image_of_mem
              simp only [singleton_prod, mem_image, Prod.mk.injEq, true_and, exists_eq_right]
              exact h'δ hx
            · exact le_of_lt (hv _ hp _ (h'δ hx))
        _ ≤ M + 1 := by linarith
      · exact ((hf.uncurry_left _).sub (hf.uncurry_left _)).norm.integrableOn_Icc
      · exact continuous_const.integrableOn_Icc
      · exact nullMeasurableSet_Icc
      · exact le_of_lt (hv _ hp _ hx)
  _ = (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) := by simp [mul_comm]
  _ < ε := h''δ

Premises used: Set.uIoc, MeasureTheory.Measure.real, HSub.hSub, intervalIntegral, norm_add_le, Set.Icc, HAdd.hAdd, OfNat.ofNat