-- Module: Mathlib.MeasureTheory.Function.Jacobian
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
ε : ℝ≥0
εpos : 0 < ε
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      (∀ (B : E →L[ℝ] E), ‖B - A‖ ≤ (↑(δ A) : ℝ) → |B.det - A.det| ≤ (↑ε : ℝ)) ∧
        ∀ (t : Set E) (g : E → E),
          ApproximatesLinearOn g A t (δ A) →
            (μ : (a : Set E) → ℝ≥0∞) (g '' t) ≤
              HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |A.det| + (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) t : ℝ≥0∞)
t : ℕ → Set E
A : ℕ → E →L[ℝ] E
t_disj : Pairwise (Disjoint on t)
t_meas : ∀ (n : ℕ), MeasurableSet (t n)
t_cover : s ⊆ ⋃ (n : ℕ), t n
ht : ∀ (n : ℕ), ApproximatesLinearOn f (A n) (s ∩ t n) (δ (A n))
μ₁ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) (⋃ (n : ℕ), f '' (s ∩ t n)) : ℝ≥0∞)
μ₂ :
  LE.le (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (f '' (s ∩ t n)))
    (∑' (n : ℕ),
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(A n).det| + (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ t n) : ℝ≥0∞))
μ₃ :
  Eq (α := ℝ≥0∞)
    (∑' (n : ℕ),
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(A n).det| + (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ t n) : ℝ≥0∞))
    (∑' (n : ℕ), ∫⁻ (x : E) in s ∩ t n, ENNReal.ofReal |(A n).det| + (↑ε : ℝ≥0∞) ∂μ)
μ₄ :
  LE.le (α := ℝ≥0∞) (∑' (n : ℕ), ∫⁻ (x : E) in s ∩ t n, ENNReal.ofReal |(A n).det| + (↑ε : ℝ≥0∞) ∂μ)
    (∑' (n : ℕ), ∫⁻ (x : E) in s ∩ t n, ENNReal.ofReal |(f' x).det| + 2 * (↑ε : ℝ≥0∞) ∂μ)
μ₅ :
  ∑' (n : ℕ), ∫⁻ (x : E) in s ∩ t n, ENNReal.ofReal |(f' x).det| + 2 * (↑ε : ℝ≥0∞) ∂μ =
    ∫⁻ (x : E) in ⋃ (n : ℕ), s ∩ t n, ENNReal.ofReal |(f' x).det| + 2 * (↑ε : ℝ≥0∞) ∂μ
μ₆ :
  ∫⁻ (x : E) in ⋃ (n : ℕ), s ∩ t n, ENNReal.ofReal |(f' x).det| + 2 * (↑ε : ℝ≥0∞) ∂μ =
    ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| + 2 * (↑ε : ℝ≥0∞) ∂μ
μ₇ :
  ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| + 2 * (↑ε : ℝ≥0∞) ∂μ =
    ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ +
      HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤
    ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ +
      HMul.hMul (β := ℝ≥0∞) (2 * (↑ε : ℝ≥0∞)) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
calc
    μ (f '' s) ≤ μ (⋃ n, f '' (s ∩ t n)) := by
      apply measure_mono
      rw [← image_iUnion, ← inter_iUnion]
      exact Set.image_mono (subset_inter Subset.rfl t_cover)
    _ ≤ ∑' n, μ (f '' (s ∩ t n)) := measure_iUnion_le _
    _ ≤ ∑' n, (ENNReal.ofReal |(A n).det| + ε) * μ (s ∩ t n) := by
      apply ENNReal.tsum_le_tsum fun n => ?_
      apply (hδ (A n)).2.2
      exact ht n
    _ = ∑' n, ∫⁻ _ in s ∩ t n, ENNReal.ofReal |(A n).det| + ε ∂μ := by
      simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter]
    _ ≤ ∑' n, ∫⁻ x in s ∩ t n, ENNReal.ofReal |(f' x).det| + 2 * ε ∂μ := by
      apply ENNReal.tsum_le_tsum fun n => ?_
      apply lintegral_mono_ae
      filter_upwards [(ht n).norm_fderiv_sub_le μ (hs.inter (t_meas n)) f' fun x hx =>
          (hf' x hx.1).mono inter_subset_left]
      intro x hx
      have I : |(A n).det| ≤ |(f' x).det| + ε :=
        calc
          |(A n).det| = |(f' x).det - ((f' x).det - (A n).det)| := by congr 1; abel
          _ ≤ |(f' x).det| + |(f' x).det - (A n).det| := abs_sub _ _
          _ ≤ |(f' x).det| + ε := add_le_add le_rfl ((hδ (A n)).2.1 _ hx)
      calc
        ENNReal.ofReal |(A n).det| + ε ≤ ENNReal.ofReal (|(f' x).det| + ε) + ε := by gcongr
        _ = ENNReal.ofReal |(f' x).det| + 2 * ε := by
          simp only [ENNReal.ofReal_add, abs_nonneg, two_mul, add_assoc, NNReal.zero_le_coe,
            ENNReal.ofReal_coe_nnreal]
    _ = ∫⁻ x in ⋃ n, s ∩ t n, ENNReal.ofReal |(f' x).det| + 2 * ε ∂μ := by
      have M : ∀ n : ℕ, MeasurableSet (s ∩ t n) := fun n => hs.inter (t_meas n)
      rw [lintegral_iUnion M]
      exact pairwise_disjoint_mono t_disj fun n => inter_subset_right
    _ = ∫⁻ x in s, ENNReal.ofReal |(f' x).det| + 2 * ε ∂μ := by
      rw [← inter_iUnion, inter_eq_self_of_subset_left t_cover]
    _ = (∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ) + 2 * ε * μ s := by
      simp only [lintegral_add_right' _ aemeasurable_const, setLIntegral_const]

Premises used: ENNReal.ofReal, abs, MeasureTheory.Measure.restrict, ContinuousLinearMap.det, Inter.inter, MeasureTheory.measure_iUnion_le, Set.image, DFunLike.coe, Set.iUnion, MeasureTheory.lintegral