-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b c : E
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
H₁ :
  (𝓝 t).EventuallyEq (β := E) (⇑(γab.trans γbc).extend : (a : ℝ) → E) fun (s : ℝ) ↦ (γab.extend : (a : ℝ) → E) (2 * s)
H₂ : HSMul.hSMul (α := ℝ) 2 I =ᶠ[𝓝 (2 * t)] I
rw :
  (ω (((γab.trans γbc).extend : (a : ℝ) → E) t) : (a : E) → F)
      (derivWithin (⇑(γab.trans γbc).extend : (a : ℝ) → E) I t) =
    HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
rw₁ :
  (ω ((fun (s : ℝ) ↦ ((γab.extend : (a : ℝ) → E) (2 * s) : E)) t) : (a : E) → F)
      (derivWithin (⇑(γab.trans γbc).extend : (a : ℝ) → E) I t) =
    HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
rw₂ :
  (ω ((fun (s : ℝ) ↦ ((γab.extend : (a : ℝ) → E) (2 * s) : E)) t) : (a : E) → F)
      (derivWithin (fun (s : ℝ) ↦ (γab.extend : (a : ℝ) → E) (2 * s)) I t) =
    HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
rw₃ :
  (ω ((fun (s : ℝ) ↦ ((γab.extend : (a : ℝ) → E) (2 * s) : E)) t) : (a : E) → F)
      (derivWithin (fun (s : ℝ) ↦ (γab.extend : (a : ℝ) → E) (2 * s)) I t) =
    HSMul.hSMul (α := ℕ) (β := F) 2
      ((ω ((γab.extend : (a : ℝ) → E) (2 * t)) : (a : E) → F) (derivWithin (⇑γab.extend : (a : ℝ) → E) I (2 * t)) : F)
rw₄ :
  (ω ((fun (s : ℝ) ↦ ((γab.extend : (a : ℝ) → E) (2 * s) : E)) t) : (a : E) → F)
      (HSMul.hSMul (α := ℝ) (β := E) 2 (derivWithin (⇑γab.extend : (a : ℝ) → E) (HSMul.hSMul (α := ℝ) 2 I) (2 * t))) =
    HSMul.hSMul (α := ℕ) (β := F) 2
      ((ω ((γab.extend : (a : ℝ) → E) (2 * t)) : (a : E) → F) (derivWithin (⇑γab.extend : (a : ℝ) → E) I (2 * t)) : F)
rw₅ :
  (ω ((fun (s : ℝ) ↦ ((γab.extend : (a : ℝ) → E) (2 * s) : E)) t) : (a : E) → F)
      (HSMul.hSMul (α := ℕ) (β := E) 2 (derivWithin (⇑γab.extend : (a : ℝ) → E) (HSMul.hSMul (α := ℝ) 2 I) (2 * t))) =
    HSMul.hSMul (α := ℕ) (β := F) 2
      ((ω ((γab.extend : (a : ℝ) → E) (2 * t)) : (a : E) → F) (derivWithin (⇑γab.extend : (a : ℝ) → E) I (2 * t)) : F)
rw₆ :
  HSMul.hSMul (α := ℕ) (β := F) 2
      ((ω ((fun (s : ℝ) ↦ ((γab.extend : (a : ℝ) → E) (2 * s) : E)) t) : (a : E) → F)
          (derivWithin (⇑γab.extend : (a : ℝ) → E) (HSMul.hSMul (α := ℝ) 2 I) (2 * t)) :
        F) =
    HSMul.hSMul (α := ℕ) (β := F) 2
      ((ω ((γab.extend : (a : ℝ) → E) (2 * t)) : (a : E) → F) (derivWithin (⇑γab.extend : (a : ℝ) → E) I (2 * t)) : F)
⊢ curveIntegralFun ω (γab.trans γbc) t = HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
have rw₇ : HSMul.hSMul (α := ℕ) (β := F) 2
    ((ω ((fun (s : ℝ) ↦ ((γab.extend : (a : ℝ) → E) (2 * s) : E)) t) : (a : E) → F)
        (derivWithin (⇑γab.extend : (a : ℝ) → E) I (2 * t)) :
      F) =
  HSMul.hSMul (α := ℕ) (β := F) 2
    ((ω ((γab.extend : (a : ℝ) → E) (2 * t)) : (a : E) → F) (derivWithin (⇑γab.extend : (a : ℝ) → E) I (2 * t)) : F)
Tactic: rw [curveIntegralFun_def, H₁.self_of_nhds, H₁.derivWithin_eq_of_nhds, curveIntegralFun_def,
    derivWithin_comp_mul_left, ofNat_smul_eq_nsmul, map_nsmul, derivWithin_congr_set H₂]