-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Jacobian (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
A : E →L[ℝ] E
m : ℝ≥0
hm : ENNReal.ofReal |A.det| < (↑m : ℝ≥0∞)
d : ℝ≥0∞ := ENNReal.ofReal |A.det|
ε : ℝ
hε :
  (μ : (a : Set E) → ℝ≥0∞)
      (HAdd.hAdd (α := Set E) (closedBall 0 ε) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1))) <
    HMul.hMul (β := ℝ≥0∞) (↑m : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (closedBall 0 1) : ℝ≥0∞)
εpos : 0 < ε
this : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) (Iio (NNReal.mk ε ⋯))
δ : ℝ≥0
s : Set E
f : E → E
hf : ApproximatesLinearOn f A s δ
hδ : (↑δ : ℝ) < ε
x : E
r : ℝ
xs : x ∈ s
r0 : 0 ≤ r
K : f '' (s ∩ closedBall x r) ⊆ image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r)
rw :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    {f x} +
      (HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
        HSMul.hSMul (β := Set E) r (closedBall 0 ε))
rw₁ :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    {f x} + HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
      HSMul.hSMul (β := Set E) r (closedBall 0 ε)
rw₂ :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) + {f x} +
      HSMul.hSMul (β := Set E) r (closedBall 0 ε)
rw₃ :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
      ({f x} + HSMul.hSMul (β := Set E) r (closedBall 0 ε))
rw₄ :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
      ({f x} + closedBall (HSMul.hSMul (β := E) r 0) (‖r‖ * ε))
rw₅ :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) +
      HAdd.hAdd (α := Set E) {f x} (closedBall 0 (‖r‖ * ε))
rw₆ :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    HSMul.hSMul (β := Set E) r (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) + closedBall (f x) (‖r‖ * ε)
rw₇ :
  image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    (⇑A : (a : E) → E) '' HSMul.hSMul (β := Set E) r (closedBall 0 1) + closedBall (f x) (‖r‖ * ε)
⊢ image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
    {f x} + r • HAdd.hAdd (α := Set E) (image (α := E) (⇑A : (a : E) → E) (closedBall 0 1)) (closedBall 0 ε)
have rw₈ : image (α := E) (⇑A : (a : E) → E) (closedBall 0 r) + closedBall (f x) (ε * r) =
  (⇑A : (a : E) → E) '' closedBall (HSMul.hSMul (β := E) r 0) (‖r‖ * 1) + closedBall (f x) (‖r‖ * ε)
Tactic: rw [smul_add, ← add_assoc, add_comm {f x}, add_assoc, smul_closedBall _ _ εpos.le, smul_zero,
        singleton_add_closedBall_zero, ← image_smul_set, _root_.smul_closedBall _ _ zero_le_one,
        smul_zero, Real.norm_eq_abs, abs_of_nonneg r0, mul_one, mul_comm]