awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
c : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 b) volume
hb : Tendsto f (𝓝 b ⊓ ae (F := Measure ℝ) volume) (𝓝 c)
⊢ HasStrictDerivAt (fun (u : ℝ) ↦ ∫ (x : ℝ) in a..u, f x) c b

Tactic:
.of_isLittleO <|
    integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_right hf hmeas hb continuousAt_snd
      continuousAt_fst

Premises used: HasDerivAtFilter, HasFDerivAtFilter.of_isLittleO, HasStrictDerivAt, continuousAt_snd, continuousAt_fst, intervalIntegral.integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 b) volume
hb : ContinuousAt f b
⊢ HasStrictDerivAt (fun (u : ℝ) ↦ ∫ (x : ℝ) in a..u, f x) (f b) b

Tactic:
integral_hasStrictDerivAt_of_tendsto_ae_right hf hmeas (hb.mono_left inf_le_left)

Premises used: intervalIntegral.integral_hasStrictDerivAt_of_tendsto_ae_right, Filter.Tendsto.mono_left, inf_le_left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
c : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 a) volume
ha : Tendsto f (𝓝 a ⊓ ae (F := Measure ℝ) volume) (𝓝 c)
⊢ HasStrictDerivAt (fun (u : ℝ) ↦ ∫ (x : ℝ) in u..b, f x) (-c) a

Tactic:
simpa only [← integral_symm] using
    (integral_hasStrictDerivAt_of_tendsto_ae_right hf.symm hmeas ha).fun_neg

Premises used: intervalIntegral.integral_hasStrictDerivAt_of_tendsto_ae_right, intervalIntegral.integral_symm, IntervalIntegrable.symm, HasStrictDerivAt.fun_neg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 a) volume
ha : ContinuousAt f a
⊢ HasStrictDerivAt (fun (u : ℝ) ↦ ∫ (x : ℝ) in u..b, f x) (-f a) a

Tactic:
simpa only [← integral_symm] using (integral_hasStrictDerivAt_right hf.symm hmeas ha).fun_neg

Premises used: intervalIntegral.integral_symm, IntervalIntegrable.symm, HasStrictDerivAt.fun_neg, intervalIntegral.integral_hasStrictDerivAt_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
hf : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
a b : ℝ
⊢ HasStrictDerivAt (fun (u : ℝ) ↦ ∫ (x : ℝ) in a..u, f x) (f b) b

Tactic:
integral_hasStrictDerivAt_right (hf.intervalIntegrable _ _) (hf.stronglyMeasurableAtFilter _ _)
    hf.continuousAt

Premises used: Continuous.stronglyMeasurableAtFilter, Continuous.intervalIntegrable, Continuous.continuousAt, intervalIntegral.integral_hasStrictDerivAt_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
hf : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
a b : ℝ
⊢ deriv (fun (u : ℝ) ↦ ∫ (x : ℝ) in a..u, f x) b = f b

Tactic:
(hf.integral_hasStrictDerivAt a b).hasDerivAt.deriv

Premises used: Continuous.integral_hasStrictDerivAt, HasDerivAt.deriv, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
ca cb : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 a) volume
hmeas_b : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 b) volume
ha : Tendsto f (𝓝 a ⊓ ae (F := Measure ℝ) volume) (𝓝 ca)
hb : Tendsto f (𝓝 b ⊓ ae (F := Measure ℝ) volume) (𝓝 cb)
⊢ HasFDerivAt (fun (p : ℝ × ℝ) ↦ ∫ (x : ℝ) in p.1..p.2, f x)
    (HSub.hSub (α := ℝ × ℝ →L[ℝ] E) (smulRight (snd ℝ ℝ ℝ) cb) (smulRight (fst ℝ ℝ ℝ) ca)) (a, b)

Tactic:
(integral_hasStrictFDerivAt_of_tendsto_ae hf hmeas_a hmeas_b ha hb).hasFDerivAt

Premises used: intervalIntegral.integral_hasStrictFDerivAt_of_tendsto_ae, HasStrictFDerivAt.hasFDerivAt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 a) volume
hmeas_b : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 b) volume
ha : ContinuousAt f a
hb : ContinuousAt f b
⊢ HasFDerivAt (fun (p : ℝ × ℝ) ↦ ∫ (x : ℝ) in p.1..p.2, f x)
    (HSub.hSub (α := ℝ × ℝ →L[ℝ] E) (smulRight (snd ℝ ℝ ℝ) (f b)) (smulRight (fst ℝ ℝ ℝ) (f a))) (a, b)

Tactic:
(integral_hasStrictFDerivAt hf hmeas_a hmeas_b ha hb).hasFDerivAt

Premises used: intervalIntegral.integral_hasStrictFDerivAt, HasStrictFDerivAt.hasFDerivAt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
ca cb : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 a) volume
hmeas_b : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 b) volume
ha : Tendsto f (𝓝 a ⊓ ae (F := Measure ℝ) volume) (𝓝 ca)
hb : Tendsto f (𝓝 b ⊓ ae (F := Measure ℝ) volume) (𝓝 cb)
⊢ fderiv ℝ (fun (p : ℝ × ℝ) ↦ ∫ (x : ℝ) in p.1..p.2, f x) (a, b) =
    HSub.hSub (α := ℝ × ℝ →L[ℝ] E) (smulRight (snd ℝ ℝ ℝ) cb) (smulRight (fst ℝ ℝ ℝ) ca)

Tactic:
(integral_hasFDerivAt_of_tendsto_ae hf hmeas_a hmeas_b ha hb).fderiv

Premises used: intervalIntegral.integral_hasFDerivAt_of_tendsto_ae, HasFDerivAt.fderiv
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 a) volume
hmeas_b : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 b) volume
ha : ContinuousAt f a
hb : ContinuousAt f b
⊢ fderiv ℝ (fun (p : ℝ × ℝ) ↦ ∫ (x : ℝ) in p.1..p.2, f x) (a, b) =
    HSub.hSub (α := ℝ × ℝ →L[ℝ] E) (smulRight (snd ℝ ℝ ℝ) (f b)) (smulRight (fst ℝ ℝ ℝ) (f a))

Tactic:
(integral_hasFDerivAt hf hmeas_a hmeas_b ha hb).fderiv

Premises used: HasFDerivAt.fderiv, intervalIntegral.integral_hasFDerivAt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
c : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 b) volume
hb : Tendsto f (𝓝 b ⊓ ae (F := Measure ℝ) volume) (𝓝 c)
⊢ HasDerivAt (fun (u : ℝ) ↦ ∫ (x : ℝ) in a..u, f x) c b

Tactic:
(integral_hasStrictDerivAt_of_tendsto_ae_right hf hmeas hb).hasDerivAt

Premises used: intervalIntegral.integral_hasStrictDerivAt_of_tendsto_ae_right, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 b) volume
hb : ContinuousAt f b
⊢ HasDerivAt (fun (u : ℝ) ↦ ∫ (x : ℝ) in a..u, f x) (f b) b

Tactic:
(integral_hasStrictDerivAt_right hf hmeas hb).hasDerivAt

Premises used: HasStrictDerivAt.hasDerivAt, intervalIntegral.integral_hasStrictDerivAt_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
c : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 b) volume
hb : Tendsto f (𝓝 b ⊓ ae (F := Measure ℝ) volume) (𝓝 c)
⊢ deriv (fun (u : ℝ) ↦ ∫ (x : ℝ) in a..u, f x) b = c

Tactic:
(integral_hasDerivAt_of_tendsto_ae_right hf hmeas hb).deriv

Premises used: intervalIntegral.integral_hasDerivAt_of_tendsto_ae_right, HasDerivAt.deriv
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 b) volume
hb : ContinuousAt f b
⊢ deriv (fun (u : ℝ) ↦ ∫ (x : ℝ) in a..u, f x) b = f b

Tactic:
(integral_hasDerivAt_right hf hmeas hb).deriv

Premises used: HasDerivAt.deriv, intervalIntegral.integral_hasDerivAt_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
c : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 a) volume
ha : Tendsto f (𝓝 a ⊓ ae (F := Measure ℝ) volume) (𝓝 c)
⊢ HasDerivAt (fun (u : ℝ) ↦ ∫ (x : ℝ) in u..b, f x) (-c) a

Tactic:
(integral_hasStrictDerivAt_of_tendsto_ae_left hf hmeas ha).hasDerivAt

Premises used: intervalIntegral.integral_hasStrictDerivAt_of_tendsto_ae_left, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 a) volume
ha : ContinuousAt f a
⊢ HasDerivAt (fun (u : ℝ) ↦ ∫ (x : ℝ) in u..b, f x) (-f a) a

Tactic:
(integral_hasStrictDerivAt_left hf hmeas ha).hasDerivAt

Premises used: HasStrictDerivAt.hasDerivAt, intervalIntegral.integral_hasStrictDerivAt_left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
c : E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 a) volume
hb : Tendsto f (𝓝 a ⊓ ae (F := Measure ℝ) volume) (𝓝 c)
⊢ deriv (fun (u : ℝ) ↦ ∫ (x : ℝ) in u..b, f x) a = -c

Tactic:
(integral_hasDerivAt_of_tendsto_ae_left hf hmeas hb).deriv

Premises used: HasDerivAt.deriv, intervalIntegral.integral_hasDerivAt_of_tendsto_ae_left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝 a) volume
hb : ContinuousAt f a
⊢ deriv (fun (u : ℝ) ↦ ∫ (x : ℝ) in u..b, f x) a = -f a

Tactic:
(integral_hasDerivAt_left hf hmeas hb).deriv

Premises used: HasDerivAt.deriv, intervalIntegral.integral_hasDerivAt_left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
ca cb : E
la lb : Filter ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst_3 : FTCFilter a (𝓝[s] a) la
inst_4 : FTCFilter b (𝓝[t] b) lb
hmeas_a : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f la volume
hmeas_b : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f lb volume
ha : Tendsto f (la ⊓ ae (F := Measure ℝ) volume) (𝓝 ca)
hb : Tendsto f (lb ⊓ ae (F := Measure ℝ) volume) (𝓝 cb)
⊢ IsLittleO.{0, u_3, 0} (E := E) (F := ℝ) (𝓝[s] a ×ˢ 𝓝[t] b)
    (fun (t : ℝ × ℝ) ↦
      HSub.hSub (α := E) (∫ (x : ℝ) in t.1..t.2, f x) (∫ (x : ℝ) in a..b, f x) - ((t.2 - b) • cb - (t.1 - a) • ca))
    fun (t : ℝ × ℝ) ↦ ‖t.1 - a‖ + ‖t.2 - b‖

Tactic:
have :=
    integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae hf hmeas_a hmeas_b ha hb
      (tendsto_const_pure.mono_right FTCFilter.pure_le : Tendsto _ _ (𝓝[s] a)) tendsto_fst
      (tendsto_const_pure.mono_right FTCFilter.pure_le : Tendsto _ _ (𝓝[t] b)) tendsto_snd
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
ca cb : E
la lb : Filter ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst_3 : FTCFilter a (𝓝[s] a) la
inst_4 : FTCFilter b (𝓝[t] b) lb
hmeas_a : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f la volume
hmeas_b : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f lb volume
ha : Tendsto f (la ⊓ ae (F := Measure ℝ) volume) (𝓝 ca)
hb : Tendsto f (lb ⊓ ae (F := Measure ℝ) volume) (𝓝 cb)
this :
  IsLittleO.{0, u_3, 0} (E := E) (F := ℝ) (𝓝[s] a ×ˢ 𝓝[t] b)
    (fun (t : ℝ × ℝ) ↦
      HSub.hSub (α := E) (∫ (x : ℝ) in t.1..t.2, f x) (∫ (x : ℝ) in a..b, f x) - ((t.2 - b) • cb - (t.1 - a) • ca))
    fun (t : ℝ × ℝ) ↦ ‖t.1 - a‖ + ‖t.2 - b‖
⊢ IsLittleO.{0, u_3, 0} (E := E) (F := ℝ) (𝓝[s ×ˢ t] (a, b))
    (fun (t : ℝ × ℝ) ↦
      HSub.hSub (α := E) (∫ (x : ℝ) in t.1..t.2, f x) (∫ (x : ℝ) in a..b, f x) - ((t.2 - b) • cb - (t.1 - a) • ca))
    fun (t : ℝ × ℝ) ↦ ‖t.1 - a‖ + ‖t.2 - b‖

Tactic:
rw [← nhdsWithin_prod_eq] at this

Premises used: nhdsWithin_prod_eq
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
ca cb : E
la lb : Filter ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst_3 : FTCFilter a (𝓝[s] a) la
inst_4 : FTCFilter b (𝓝[t] b) lb
hmeas_a : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f la volume
hmeas_b : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f lb volume
ha : Tendsto f (la ⊓ ae (F := Measure ℝ) volume) (𝓝 ca)
hb : Tendsto f (lb ⊓ ae (F := Measure ℝ) volume) (𝓝 cb)
this :
  IsLittleO.{0, u_3, 0} (E := E) (F := ℝ) (𝓝[s ×ˢ t] (a, b))
    (fun (t : ℝ × ℝ) ↦
      HSub.hSub (α := E) (∫ (x : ℝ) in t.1..t.2, f x) (∫ (x : ℝ) in a..b, f x) - ((t.2 - b) • cb - (t.1 - a) • ca))
    fun (t : ℝ × ℝ) ↦ ‖t.1 - a‖ + ‖t.2 - b‖
⊢ HasFDerivWithinAt (fun (p : ℝ × ℝ) ↦ ∫ (x : ℝ) in p.1..p.2, f x)
    (HSub.hSub (α := ℝ × ℝ →L[ℝ] E) (smulRight (snd ℝ ℝ ℝ) cb) (smulRight (fst ℝ ℝ ℝ) ca)) (s ×ˢ t) (a, b)

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

Premises used: Asymptotics.IsLittleO.congr_left, setOf, HasFDerivWithinAt.of_isLittleO, Asymptotics.IsLittleO.trans_isBigO
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
ca cb : E
la lb : Filter ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst_3 : FTCFilter a (𝓝[s] a) la
inst_4 : FTCFilter b (𝓝[t] b) lb
hmeas_a : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f la volume
hmeas_b : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f lb volume
ha : Tendsto f (la ⊓ ae (F := Measure ℝ) volume) (𝓝 ca)
hb : Tendsto f (lb ⊓ ae (F := Measure ℝ) volume) (𝓝 cb)
this :
  IsLittleO.{0, u_3, 0} (E := E) (F := ℝ) (𝓝[s ×ˢ t] (a, b))
    (fun (t : ℝ × ℝ) ↦
      HSub.hSub (α := E) (∫ (x : ℝ) in t.1..t.2, f x) (∫ (x : ℝ) in a..b, f x) - ((t.2 - b) • cb - (t.1 - a) • ca))
    fun (t : ℝ × ℝ) ↦ ‖t.1 - a‖ + ‖t.2 - b‖
refine_1 :
  ∀ (x : ℝ × ℝ),
    HSub.hSub (α := E) (∫ (x : ℝ) in x.1..x.2, f x) (∫ (x : ℝ) in a..b, f x) - ((x.2 - b) • cb - (x.1 - a) • ca) =
      HSub.hSub (β := E) (HSub.hSub (α := E) (∫ (x : ℝ) in x.1..x.2, f x) (∫ (x : ℝ) in (a, b).1..(a, b).2, f x))
        ((HSub.hSub (α := ℝ × ℝ →L[ℝ] E) (smulRight (snd ℝ ℝ ℝ) cb) (smulRight (fst ℝ ℝ ℝ) ca) : (a : ℝ × ℝ) → E)
            (x - (a, b)) :
          E)
refine_2 :
  IsBigO (E := ℝ) (F := ℝ × ℝ) (𝓝[s ×ˢ t] (a, b)) (fun (t : ℝ × ℝ) ↦ ‖t.1 - a‖ + ‖t.2 - b‖) fun (x' : ℝ × ℝ) ↦
    x' - (a, b)
⊢ HasFDerivWithinAt (fun (p : ℝ × ℝ) ↦ ∫ (x : ℝ) in p.1..p.2, f x)
    (HSub.hSub (α := ℝ × ℝ →L[ℝ] E) (smulRight (snd ℝ ℝ ℝ) cb) (smulRight (fst ℝ ℝ ℝ) ca)) (s ×ˢ t) (a, b)

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

Premises used: Asymptotics.IsLittleO.congr_left, Asymptotics.IsLittleO.trans_isBigO
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
ca cb : E
la lb : Filter ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst_3 : FTCFilter a (𝓝[s] a) la
inst_4 : FTCFilter b (𝓝[t] b) lb
hmeas_a : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f la volume
hmeas_b : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f lb volume
ha : Tendsto f (la ⊓ ae (F := Measure ℝ) volume) (𝓝 ca)
hb : Tendsto f (lb ⊓ ae (F := Measure ℝ) volume) (𝓝 cb)
this :
  IsLittleO.{0, u_3, 0} (E := E) (F := ℝ) (𝓝[s ×ˢ t] (a, b))
    (fun (t : ℝ × ℝ) ↦
      HSub.hSub (α := E) (∫ (x : ℝ) in t.1..t.2, f x) (∫ (x : ℝ) in a..b, f x) - ((t.2 - b) • cb - (t.1 - a) • ca))
    fun (t : ℝ × ℝ) ↦ ‖t.1 - a‖ + ‖t.2 - b‖
⊢ ∀ (x : ℝ × ℝ),
    HSub.hSub (α := E) (∫ (x : ℝ) in x.1..x.2, f x) (∫ (x : ℝ) in a..b, f x) - ((x.2 - b) • cb - (x.1 - a) • ca) =
      HSub.hSub (β := E) (HSub.hSub (α := E) (∫ (x : ℝ) in x.1..x.2, f x) (∫ (x : ℝ) in (a, b).1..(a, b).2, f x))
        ((HSub.hSub (α := ℝ × ℝ →L[ℝ] E) (smulRight (snd ℝ ℝ ℝ) cb) (smulRight (fst ℝ ℝ ℝ) ca) : (a : ℝ × ℝ) → E)
            (x - (a, b)) :
          E)

Tactic:
simp [sub_smul]

Premises used: sub_smul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
ca cb : E
la lb : Filter ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst_3 : FTCFilter a (𝓝[s] a) la
inst_4 : FTCFilter b (𝓝[t] b) lb
hmeas_a : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f la volume
hmeas_b : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f lb volume
ha : Tendsto f (la ⊓ ae (F := Measure ℝ) volume) (𝓝 ca)
hb : Tendsto f (lb ⊓ ae (F := Measure ℝ) volume) (𝓝 cb)
this :
  IsLittleO.{0, u_3, 0} (E := E) (F := ℝ) (𝓝[s ×ˢ t] (a, b))
    (fun (t : ℝ × ℝ) ↦
      HSub.hSub (α := E) (∫ (x : ℝ) in t.1..t.2, f x) (∫ (x : ℝ) in a..b, f x) - ((t.2 - b) • cb - (t.1 - a) • ca))
    fun (t : ℝ × ℝ) ↦ ‖t.1 - a‖ + ‖t.2 - b‖
⊢ IsBigO (E := ℝ) (F := ℝ × ℝ) (𝓝[s ×ˢ t] (a, b)) (fun (t : ℝ × ℝ) ↦ ‖t.1 - a‖ + ‖t.2 - b‖) fun (x' : ℝ × ℝ) ↦
    x' - (a, b)

Tactic:
isBigO_fst_prod.norm_left.add isBigO_snd_prod.norm_left

Premises used: Asymptotics.IsBigO.norm_left, Asymptotics.isBigO_fst_prod, Asymptotics.IsBigO.add, Asymptotics.isBigO_snd_prod
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
ca cb : E
la lb : Filter ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst_3 : FTCFilter a (𝓝[s] a) la
inst_4 : FTCFilter b (𝓝[t] b) lb
hmeas_a : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f la volume
hmeas_b : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f lb volume
ha : Tendsto f (la ⊓ ae (F := Measure ℝ) volume) (𝓝 ca)
hb : Tendsto f (lb ⊓ ae (F := Measure ℝ) volume) (𝓝 cb)
this :
  IsLittleO.{0, u_3, 0} (E := E) (F := ℝ) (𝓝[s ×ˢ t] (a, b))
    (fun (t : ℝ × ℝ) ↦
      HSub.hSub (α := E) (∫ (x : ℝ) in t.1..t.2, f x) (∫ (x : ℝ) in a..b, f x) - ((t.2 - b) • cb - (t.1 - a) • ca))
    fun (t : ℝ × ℝ) ↦ ‖t.1 - a‖ + ‖t.2 - b‖
⊢ IsBigO (E := ℝ) (F := ℝ × ℝ) (𝓝[s ×ˢ t] (a, b)) (fun (t : ℝ × ℝ) ↦ ‖t.1 - a‖ + ‖t.2 - b‖) fun (x' : ℝ × ℝ) ↦
    x' - (a, b)

Tactic:
exact isBigO_fst_prod.norm_left.add isBigO_snd_prod.norm_left

Premises used: Asymptotics.IsBigO.norm_left, Asymptotics.isBigO_fst_prod, Asymptotics.IsBigO.add, Asymptotics.isBigO_snd_prod
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
la lb : Filter ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f la volume
hmeas_b : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f lb volume
s t : Set ℝ
inst_3 : FTCFilter a (𝓝[s] a) la
inst_4 : FTCFilter b (𝓝[t] b) lb
ha : Tendsto f la (𝓝 (f a))
hb : Tendsto f lb (𝓝 (f b))
⊢ HasFDerivWithinAt (fun (p : ℝ × ℝ) ↦ ∫ (x : ℝ) in p.1..p.2, f x)
    (HSub.hSub (α := ℝ × ℝ →L[ℝ] E) (smulRight (snd ℝ ℝ ℝ) (f b)) (smulRight (fst ℝ ℝ ℝ) (f a))) (s ×ˢ t) (a, b)

Tactic:
integral_hasFDerivWithinAt_of_tendsto_ae hf hmeas_a hmeas_b (ha.mono_left inf_le_left)
    (hb.mono_left inf_le_left)

Premises used: intervalIntegral.integral_hasFDerivWithinAt_of_tendsto_ae, Filter.Tendsto.mono_left, inf_le_left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
ca cb : E
la lb : Filter ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
hmeas_a : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f la volume
hmeas_b : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f lb volume
s t : Set ℝ
inst_3 : FTCFilter a (𝓝[s] a) la
inst_4 : FTCFilter b (𝓝[t] b) lb
ha : Tendsto f (la ⊓ ae (F := Measure ℝ) volume) (𝓝 ca)
hb : Tendsto f (lb ⊓ ae (F := Measure ℝ) volume) (𝓝 cb)
hs : UniqueDiffWithinAt ℝ s a
ht : UniqueDiffWithinAt ℝ t b
⊢ fderivWithin ℝ (fun (p : ℝ × ℝ) ↦ ∫ (x : ℝ) in p.1..p.2, f x) (s ×ˢ t) (a, b) =
    HSub.hSub (α := ℝ × ℝ →L[ℝ] E) (smulRight (snd ℝ ℝ ℝ) cb) (smulRight (fst ℝ ℝ ℝ) ca)

Tactic:
(integral_hasFDerivWithinAt_of_tendsto_ae hf hmeas_a hmeas_b ha hb).fderivWithin <| hs.prod ht

Premises used: HasFDerivWithinAt.fderivWithin, intervalIntegral.integral_hasFDerivWithinAt_of_tendsto_ae, UniqueDiffWithinAt.prod
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
c : E
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst_3 : FTCFilter b (𝓝[s] b) (𝓝[t] b)
hmeas : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝[t] b) volume
hb : Tendsto f (𝓝[t] b ⊓ ae (F := Measure ℝ) volume) (𝓝 c)
⊢ HasDerivWithinAt (fun (u : ℝ) ↦ ∫ (x : ℝ) in a..u, f x) c s b

Tactic:
.of_isLittleO <| integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_right hf hmeas hb
    (tendsto_const_pure.mono_right FTCFilter.pure_le) tendsto_id

Premises used: Filter.tendsto_id, HasDerivWithinAt.of_isLittleO, Filter.Tendsto.mono_right, Filter.tendsto_const_pure, intervalIntegral.FTCFilter.pure_le, intervalIntegral.integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst_3 : FTCFilter b (𝓝[s] b) (𝓝[t] b)
hmeas : StronglyMeasurableAtFilter (mα := MeasureSpace.toMeasurableSpace) f (𝓝[t] b) volume
hb : ContinuousWithinAt f t b
⊢ HasDerivWithinAt (fun (u : ℝ) ↦ ∫ (x : ℝ) in a..u, f x) (f b) s b

Tactic:
integral_hasDerivWithinAt_of_tendsto_ae_right hf hmeas (hb.mono_left inf_le_left)

Premises used: intervalIntegral.integral_hasDerivWithinAt_of_tendsto_ae_right, Filter.Tendsto.mono_left, inf_le_left