Module: Mathlib.MeasureTheory.Integral.DominatedConvergence

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : TopologicalSpace X
μ : Measure ℝ
inst✝¹ : NullSingletonClass μ
inst✝ : 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✝ : IsCompact ({q} ×ˢ Icc a b)
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖Function.uncurry f x‖) '' {q} ×ˢ Icc a b)
δ : ℝ
δ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 : ℝ) 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''δ

Goal state after: