-- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
theorem integral_hasStrictFDerivAt_of_tendsto_ae (hf : IntervalIntegrable f volume a b)
    (hmeas_a : StronglyMeasurableAtFilter f (𝓝 a)) (hmeas_b : StronglyMeasurableAtFilter f (𝓝 b))
    (ha : Tendsto f (𝓝 a ⊓ ae volume) (𝓝 ca)) (hb : Tendsto f (𝓝 b ⊓ ae volume) (𝓝 cb)) :
    HasStrictFDerivAt (fun p : ℝ × ℝ => ∫ x in p.1..p.2, f x)
      ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca) (a, b)

Proof state:
case refine_1
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
ca cb : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter f (𝓝 a) volume
hmeas_b : StronglyMeasurableAtFilter f (𝓝 b) volume
ha : Tendsto f (𝓝 a ⊓ ae volume) (𝓝 ca)
hb : Tendsto f (𝓝 b ⊓ ae volume) (𝓝 cb)
this :
  (fun t =>
      ((∫ (x : ℝ) in t.1.1 ..t.1.2, f x) - ∫ (x : ℝ) in t.2.1 ..t.2.2, f x) -
        ((t.1.2 - t.2.2) • cb - (t.1.1 - t.2.1) • ca)) =o[𝓝 ((a, b), a, b)]
    fun t => ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖
⊢ ∀ (x : (ℝ × ℝ) × ℝ × ℝ),
    ((∫ (x : ℝ) in x.1.1 ..x.1.2, f x) - ∫ (x : ℝ) in x.2.1 ..x.2.2, f x) -
        ((x.1.2 - x.2.2) • cb - (x.1.1 - x.2.1) • ca) =
      ((∫ (x : ℝ) in x.1.1 ..x.1.2, f x) - ∫ (x : ℝ) in x.2.1 ..x.2.2, f x) -
        ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca) (x.1 - x.2)

Tactic:
intro x

Result:
case refine_1
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
ca cb : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter f (𝓝 a) volume
hmeas_b : StronglyMeasurableAtFilter f (𝓝 b) volume
ha : Tendsto f (𝓝 a ⊓ ae volume) (𝓝 ca)
hb : Tendsto f (𝓝 b ⊓ ae volume) (𝓝 cb)
this :
  (fun t =>
      ((∫ (x : ℝ) in t.1.1 ..t.1.2, f x) - ∫ (x : ℝ) in t.2.1 ..t.2.2, f x) -
        ((t.1.2 - t.2.2) • cb - (t.1.1 - t.2.1) • ca)) =o[𝓝 ((a, b), a, b)]
    fun t => ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖
x : (ℝ × ℝ) × ℝ × ℝ
⊢ ((∫ (x : ℝ) in x.1.1 ..x.1.2, f x) - ∫ (x : ℝ) in x.2.1 ..x.2.2, f x) -
      ((x.1.2 - x.2.2) • cb - (x.1.1 - x.2.1) • ca) =
    ((∫ (x : ℝ) in x.1.1 ..x.1.2, f x) - ∫ (x : ℝ) in x.2.1 ..x.2.2, f x) -
      ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca) (x.1 - x.2)

Proof state:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
ca cb : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter f (𝓝 a) volume
hmeas_b : StronglyMeasurableAtFilter f (𝓝 b) volume
ha : Tendsto f (𝓝 a ⊓ ae volume) (𝓝 ca)
hb : Tendsto f (𝓝 b ⊓ ae volume) (𝓝 cb)
⊢ HasStrictFDerivAt (fun p => ∫ (x : ℝ) in p.1 ..p.2, f x) ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca) (a, b)

Tactic:
have :=
  integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae hf hmeas_a hmeas_b ha hb
    (continuous_snd.fst.tendsto ((a, b), (a, b)))
    (continuous_fst.fst.tendsto ((a, b), (a, b)))
    (continuous_snd.snd.tendsto ((a, b), (a, b)))
    (continuous_fst.snd.tendsto ((a, b), (a, b)))

Result:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
ca cb : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter f (𝓝 a) volume
hmeas_b : StronglyMeasurableAtFilter f (𝓝 b) volume
ha : Tendsto f (𝓝 a ⊓ ae volume) (𝓝 ca)
hb : Tendsto f (𝓝 b ⊓ ae volume) (𝓝 cb)
this :
  (fun t =>
      ((∫ (x : ℝ) in t.1.1 ..t.1.2, f x) - ∫ (x : ℝ) in t.2.1 ..t.2.2, f x) -
        ((t.1.2 - t.2.2) • cb - (t.1.1 - t.2.1) • ca)) =o[𝓝 ((a, b), a, b)]
    fun t => ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖
⊢ HasStrictFDerivAt (fun p => ∫ (x : ℝ) in p.1 ..p.2, f x) ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca) (a, b)

Proof state:
case refine_2
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
ca cb : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter f (𝓝 a) volume
hmeas_b : StronglyMeasurableAtFilter f (𝓝 b) volume
ha : Tendsto f (𝓝 a ⊓ ae volume) (𝓝 ca)
hb : Tendsto f (𝓝 b ⊓ ae volume) (𝓝 cb)
this :
  (fun t =>
      ((∫ (x : ℝ) in t.1.1 ..t.1.2, f x) - ∫ (x : ℝ) in t.2.1 ..t.2.2, f x) -
        ((t.1.2 - t.2.2) • cb - (t.1.1 - t.2.1) • ca)) =o[𝓝 ((a, b), a, b)]
    fun t => ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖
⊢ (fun t => ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖) =O[𝓝 ((a, b), a, b)] fun p => p.1 - p.2

Tactic:
exact isBigO_fst_prod.norm_left.add isBigO_snd_prod.norm_left

Result:
no goals

Proof state:
case refine_1
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
ca cb : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter f (𝓝 a) volume
hmeas_b : StronglyMeasurableAtFilter f (𝓝 b) volume
ha : Tendsto f (𝓝 a ⊓ ae volume) (𝓝 ca)
hb : Tendsto f (𝓝 b ⊓ ae volume) (𝓝 cb)
this :
  (fun t =>
      ((∫ (x : ℝ) in t.1.1 ..t.1.2, f x) - ∫ (x : ℝ) in t.2.1 ..t.2.2, f x) -
        ((t.1.2 - t.2.2) • cb - (t.1.1 - t.2.1) • ca)) =o[𝓝 ((a, b), a, b)]
    fun t => ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖
x : (ℝ × ℝ) × ℝ × ℝ
⊢ ((∫ (x : ℝ) in x.1.1 ..x.1.2, f x) - ∫ (x : ℝ) in x.2.1 ..x.2.2, f x) -
      ((x.1.2 - x.2.2) • cb - (x.1.1 - x.2.1) • ca) =
    ((∫ (x : ℝ) in x.1.1 ..x.1.2, f x) - ∫ (x : ℝ) in x.2.1 ..x.2.2, f x) -
      ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca) (x.1 - x.2)

Tactic:
simp [sub_smul]

Result:
no goals

Proof state:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
ca cb : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter f (𝓝 a) volume
hmeas_b : StronglyMeasurableAtFilter f (𝓝 b) volume
ha : Tendsto f (𝓝 a ⊓ ae volume) (𝓝 ca)
hb : Tendsto f (𝓝 b ⊓ ae volume) (𝓝 cb)
this :
  (fun t =>
      ((∫ (x : ℝ) in t.1.1 ..t.1.2, f x) - ∫ (x : ℝ) in t.2.1 ..t.2.2, f x) -
        ((t.1.2 - t.2.2) • cb - (t.1.1 - t.2.1) • ca)) =o[𝓝 ((a, b), a, b)]
    fun t => ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖
⊢ HasStrictFDerivAt (fun p => ∫ (x : ℝ) in p.1 ..p.2, f x) ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca) (a, b)

Tactic:
refine .of_isLittleO <| (this.congr_left ?_).trans_isBigO ?_

Result:
case refine_1
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
ca cb : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter f (𝓝 a) volume
hmeas_b : StronglyMeasurableAtFilter f (𝓝 b) volume
ha : Tendsto f (𝓝 a ⊓ ae volume) (𝓝 ca)
hb : Tendsto f (𝓝 b ⊓ ae volume) (𝓝 cb)
this :
  (fun t =>
      ((∫ (x : ℝ) in t.1.1 ..t.1.2, f x) - ∫ (x : ℝ) in t.2.1 ..t.2.2, f x) -
        ((t.1.2 - t.2.2) • cb - (t.1.1 - t.2.1) • ca)) =o[𝓝 ((a, b), a, b)]
    fun t => ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖
⊢ ∀ (x : (ℝ × ℝ) × ℝ × ℝ),
    ((∫ (x : ℝ) in x.1.1 ..x.1.2, f x) - ∫ (x : ℝ) in x.2.1 ..x.2.2, f x) -
        ((x.1.2 - x.2.2) • cb - (x.1.1 - x.2.1) • ca) =
      ((∫ (x : ℝ) in x.1.1 ..x.1.2, f x) - ∫ (x : ℝ) in x.2.1 ..x.2.2, f x) -
        ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca) (x.1 - x.2)

case refine_2
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
ca cb : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter f (𝓝 a) volume
hmeas_b : StronglyMeasurableAtFilter f (𝓝 b) volume
ha : Tendsto f (𝓝 a ⊓ ae volume) (𝓝 ca)
hb : Tendsto f (𝓝 b ⊓ ae volume) (𝓝 cb)
this :
  (fun t =>
      ((∫ (x : ℝ) in t.1.1 ..t.1.2, f x) - ∫ (x : ℝ) in t.2.1 ..t.2.2, f x) -
        ((t.1.2 - t.2.2) • cb - (t.1.1 - t.2.1) • ca)) =o[𝓝 ((a, b), a, b)]
    fun t => ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖
⊢ (fun t => ‖t.1.1 - t.2.1‖ + ‖t.1.2 - t.2.2‖) =O[𝓝 ((a, b), a, b)] fun p => p.1 - p.2