-- 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
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
R : ℝ
hs : s ⊆ closedBall 0 R
ε : ℝ≥0
εpos : 0 < ε
h'f' : ∀ x ∈ s, (f' x).det = 0
h's : s.Nonempty
δ : (A : E →L[ℝ] E) → ℝ≥0
hδ :
  ∀ (A : E →L[ℝ] E),
    0 < δ A ∧
      ∀ (t : Set E),
        ApproximatesLinearOn f A t (δ A) →
          (μ : (a : Set E) → ℝ≥0∞) (f '' t) ≤
            HMul.hMul (β := ℝ≥0∞) (↑(|A.det|.toNNReal + ε) : ℝ≥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))
Af' : s.Nonempty → ∀ (n : ℕ), ∃ y ∈ s, A n = f' y
μ₁ :
  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∞) (↑(|(A n).det|.toNNReal + ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ t n) : ℝ≥0∞))
μ₃ :
  Eq (α := ℝ≥0∞)
    (∑' (n : ℕ), HMul.hMul (β := ℝ≥0∞) (↑(|(A n).det|.toNNReal + ε) : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ t n) : ℝ≥0∞))
    (∑' (n : ℕ), HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ t n) : ℝ≥0∞))
μ₄ :
  ∑' (n : ℕ), HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (s ∩ t n) : ℝ≥0∞) ≤
    (↑ε : ℝ≥0∞) * ∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R ∩ t n)
μ₅ :
  (↑ε : ℝ≥0∞) * ∑' (n : ℕ), (μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R ∩ t n) =
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (⋃ (n : ℕ), closedBall 0 R ∩ t n) : ℝ≥0∞)
μ₆ :
  HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (⋃ (n : ℕ), closedBall 0 R ∩ t n) : ℝ≥0∞) ≤
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) (f '' s) ≤
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 R) : ℝ≥0∞)

Tactic:
calc
    μ (f '' s) ≤ μ (⋃ n, f '' (s ∩ t n)) := by
      rw [← image_iUnion, ← inter_iUnion]
      gcongr
      exact subset_inter Subset.rfl t_cover
    _ ≤ ∑' n, μ (f '' (s ∩ t n)) := measure_iUnion_le _
    _ ≤ ∑' n, (Real.toNNReal |(A n).det| + ε : ℝ≥0) * μ (s ∩ t n) := by
      gcongr
      exact (hδ (A _)).2 _ (ht _)
    _ = ∑' n, ε * μ (s ∩ t n) := by
      congr with n
      rcases Af' h's n with ⟨y, ys, hy⟩
      simp only [hy, h'f' y ys, Real.toNNReal_zero, abs_zero, zero_add]
    _ ≤ ε * ∑' n, μ (closedBall 0 R ∩ t n) := by
      rw [ENNReal.tsum_mul_left]
      gcongr
    _ = ε * μ (⋃ n, closedBall 0 R ∩ t n) := by
      rw [measure_iUnion]
      · exact pairwise_disjoint_mono t_disj fun n => inter_subset_right
      · intro n
        exact measurableSet_closedBall.inter (t_meas n)
    _ ≤ ε * μ (closedBall 0 R) := by grw [← inter_iUnion, inter_subset_left]

Premises used: Inter.inter, MeasureTheory.measure_iUnion_le, Set.image, Metric.closedBall, OfNat.ofNat, DFunLike.coe, Set.iUnion