ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>ca cb : E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>hmeas_a : StronglyMeasurableAtFilter f (𝓝 a) MeasureTheory.volume<VAR>hmeas_b : StronglyMeasurableAtFilter f (𝓝 b) MeasureTheory.volume<VAR>ha : Filter.Tendsto f (𝓝 a ⊓ MeasureTheory.ae MeasureTheory.volume) (𝓝 ca)<VAR>hb : Filter.Tendsto f (𝓝 b ⊓ MeasureTheory.ae MeasureTheory.volume) (𝓝 cb)<GOAL>HasFDerivAt (fun p => ∫ (x : ℝ) in p.1 ..p.2, f x) ((ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight cb - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight ca) (a, b)
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>hmeas_a : StronglyMeasurableAtFilter f (𝓝 a) MeasureTheory.volume<VAR>hmeas_b : StronglyMeasurableAtFilter f (𝓝 b) MeasureTheory.volume<VAR>ha : ContinuousAt f a<VAR>hb : ContinuousAt f b<GOAL>HasFDerivAt (fun p => ∫ (x : ℝ) in p.1 ..p.2, f x) ((ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight (f b) - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight (f a)) (a, b)
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>ca cb : E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>hmeas_a : StronglyMeasurableAtFilter f (𝓝 a) MeasureTheory.volume<VAR>hmeas_b : StronglyMeasurableAtFilter f (𝓝 b) MeasureTheory.volume<VAR>ha : Filter.Tendsto f (𝓝 a ⊓ MeasureTheory.ae MeasureTheory.volume) (𝓝 ca)<VAR>hb : Filter.Tendsto f (𝓝 b ⊓ MeasureTheory.ae MeasureTheory.volume) (𝓝 cb)<GOAL>fderiv ℝ (fun p => ∫ (x : ℝ) in p.1 ..p.2, f x) (a, b) = (ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight cb - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight ca
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>hmeas_a : StronglyMeasurableAtFilter f (𝓝 a) MeasureTheory.volume<VAR>hmeas_b : StronglyMeasurableAtFilter f (𝓝 b) MeasureTheory.volume<VAR>ha : ContinuousAt f a<VAR>hb : ContinuousAt f b<GOAL>fderiv ℝ (fun p => ∫ (x : ℝ) in p.1 ..p.2, f x) (a, b) = (ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight (f b) - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight (f a)
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>c : E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>hmeas : StronglyMeasurableAtFilter f (𝓝 b) MeasureTheory.volume<VAR>hb : Filter.Tendsto f (𝓝 b ⊓ MeasureTheory.ae MeasureTheory.volume) (𝓝 c)<GOAL>HasDerivAt (fun u => ∫ (x : ℝ) in a..u, f x) c b
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>hmeas : StronglyMeasurableAtFilter f (𝓝 b) MeasureTheory.volume<VAR>hb : ContinuousAt f b<GOAL>HasDerivAt (fun u => ∫ (x : ℝ) in a..u, f x) (f b) b
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>c : E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>hmeas : StronglyMeasurableAtFilter f (𝓝 b) MeasureTheory.volume<VAR>hb : Filter.Tendsto f (𝓝 b ⊓ MeasureTheory.ae MeasureTheory.volume) (𝓝 c)<GOAL>deriv (fun u => ∫ (x : ℝ) in a..u, f x) b = c
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>hmeas : StronglyMeasurableAtFilter f (𝓝 b) MeasureTheory.volume<VAR>hb : ContinuousAt f b<GOAL>deriv (fun u => ∫ (x : ℝ) in a..u, f x) b = f b
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>c : E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>hmeas : StronglyMeasurableAtFilter f (𝓝 a) MeasureTheory.volume<VAR>ha : Filter.Tendsto f (𝓝 a ⊓ MeasureTheory.ae MeasureTheory.volume) (𝓝 c)<GOAL>HasDerivAt (fun u => ∫ (x : ℝ) in u..b, f x) (-c) a
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>hmeas : StronglyMeasurableAtFilter f (𝓝 a) MeasureTheory.volume<VAR>ha : ContinuousAt f a<GOAL>HasDerivAt (fun u => ∫ (x : ℝ) in u..b, f x) (-f a) a
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>c : E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>hmeas : StronglyMeasurableAtFilter f (𝓝 a) MeasureTheory.volume<VAR>hb : Filter.Tendsto f (𝓝 a ⊓ MeasureTheory.ae MeasureTheory.volume) (𝓝 c)<GOAL>deriv (fun u => ∫ (x : ℝ) in u..b, f x) a = -c
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>hmeas : StronglyMeasurableAtFilter f (𝓝 a) MeasureTheory.volume<VAR>hb : ContinuousAt f a<GOAL>deriv (fun u => ∫ (x : ℝ) in u..b, f x) a = -f a
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>ca cb : E<VAR>la lb : Filter ℝ<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>s t : Set ℝ<VAR>intervalIntegral.FTCFilter a (𝓝[s] a) la<VAR>intervalIntegral.FTCFilter b (𝓝[t] b) lb<VAR>hmeas_a : StronglyMeasurableAtFilter f la MeasureTheory.volume<VAR>hmeas_b : StronglyMeasurableAtFilter f lb MeasureTheory.volume<VAR>ha : Filter.Tendsto f (la ⊓ MeasureTheory.ae MeasureTheory.volume) (𝓝 ca)<VAR>hb : Filter.Tendsto f (lb ⊓ MeasureTheory.ae MeasureTheory.volume) (𝓝 cb)<GOAL>HasFDerivWithinAt (fun p => ∫ (x : ℝ) in p.1 ..p.2, f x) ((ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight cb - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight ca) (s ×ˢ t) (a, b)
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>la lb : Filter ℝ<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>hmeas_a : StronglyMeasurableAtFilter f la MeasureTheory.volume<VAR>hmeas_b : StronglyMeasurableAtFilter f lb MeasureTheory.volume<VAR>s t : Set ℝ<VAR>intervalIntegral.FTCFilter a (𝓝[s] a) la<VAR>intervalIntegral.FTCFilter b (𝓝[t] b) lb<VAR>ha : Filter.Tendsto f la (𝓝 (f a))<VAR>hb : Filter.Tendsto f lb (𝓝 (f b))<GOAL>HasFDerivWithinAt (fun p => ∫ (x : ℝ) in p.1 ..p.2, f x) ((ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight (f b) - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight (f a)) (s ×ˢ t) (a, b)
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>ca cb : E<VAR>la lb : Filter ℝ<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>hmeas_a : StronglyMeasurableAtFilter f la MeasureTheory.volume<VAR>hmeas_b : StronglyMeasurableAtFilter f lb MeasureTheory.volume<VAR>s t : Set ℝ<VAR>intervalIntegral.FTCFilter a (𝓝[s] a) la<VAR>intervalIntegral.FTCFilter b (𝓝[t] b) lb<VAR>ha : Filter.Tendsto f (la ⊓ MeasureTheory.ae MeasureTheory.volume) (𝓝 ca)<VAR>hb : Filter.Tendsto f (lb ⊓ MeasureTheory.ae MeasureTheory.volume) (𝓝 cb)<VAR>hs : UniqueDiffWithinAt ℝ s a := by uniqueDiffWithinAt_Ici_Iic_univ<VAR>ht : UniqueDiffWithinAt ℝ t b := by uniqueDiffWithinAt_Ici_Iic_univ<GOAL>fderivWithin ℝ (fun p => ∫ (x : ℝ) in p.1 ..p.2, f x) (s ×ˢ t) (a, b) = (ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight cb - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight ca
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>c : E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>s t : Set ℝ<VAR>intervalIntegral.FTCFilter b (𝓝[s] b) (𝓝[t] b)<VAR>hmeas : StronglyMeasurableAtFilter f (𝓝[t] b) MeasureTheory.volume<VAR>hb : Filter.Tendsto f (𝓝[t] b ⊓ MeasureTheory.ae MeasureTheory.volume) (𝓝 c)<GOAL>HasDerivWithinAt (fun u => ∫ (x : ℝ) in a..u, f x) c s b
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>s t : Set ℝ<VAR>intervalIntegral.FTCFilter b (𝓝[s] b) (𝓝[t] b)<VAR>hmeas : StronglyMeasurableAtFilter f (𝓝[t] b) MeasureTheory.volume<VAR>hb : ContinuousWithinAt f t b<GOAL>HasDerivWithinAt (fun u => ∫ (x : ℝ) in a..u, f x) (f b) s b
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>c : E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>s t : Set ℝ<VAR>intervalIntegral.FTCFilter b (𝓝[s] b) (𝓝[t] b)<VAR>hmeas : StronglyMeasurableAtFilter f (𝓝[t] b) MeasureTheory.volume<VAR>hb : Filter.Tendsto f (𝓝[t] b ⊓ MeasureTheory.ae MeasureTheory.volume) (𝓝 c)<VAR>hs : UniqueDiffWithinAt ℝ s b := by uniqueDiffWithinAt_Ici_Iic_univ<GOAL>derivWithin (fun u => ∫ (x : ℝ) in a..u, f x) s b = c
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>s t : Set ℝ<VAR>intervalIntegral.FTCFilter b (𝓝[s] b) (𝓝[t] b)<VAR>hmeas : StronglyMeasurableAtFilter f (𝓝[t] b) MeasureTheory.volume<VAR>hb : ContinuousWithinAt f t b<VAR>hs : UniqueDiffWithinAt ℝ s b := by uniqueDiffWithinAt_Ici_Iic_univ<GOAL>derivWithin (fun u => ∫ (x : ℝ) in a..u, f x) s b = f b
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>c : E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>s t : Set ℝ<VAR>intervalIntegral.FTCFilter a (𝓝[s] a) (𝓝[t] a)<VAR>hmeas : StronglyMeasurableAtFilter f (𝓝[t] a) MeasureTheory.volume<VAR>ha : Filter.Tendsto f (𝓝[t] a ⊓ MeasureTheory.ae MeasureTheory.volume) (𝓝 c)<GOAL>HasDerivWithinAt (fun u => ∫ (x : ℝ) in u..b, f x) (-c) s a
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>s t : Set ℝ<VAR>intervalIntegral.FTCFilter a (𝓝[s] a) (𝓝[t] a)<VAR>hmeas : StronglyMeasurableAtFilter f (𝓝[t] a) MeasureTheory.volume<VAR>ha : ContinuousWithinAt f t a<GOAL>HasDerivWithinAt (fun u => ∫ (x : ℝ) in u..b, f x) (-f a) s a
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>c : E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>s t : Set ℝ<VAR>intervalIntegral.FTCFilter a (𝓝[s] a) (𝓝[t] a)<VAR>hmeas : StronglyMeasurableAtFilter f (𝓝[t] a) MeasureTheory.volume<VAR>ha : Filter.Tendsto f (𝓝[t] a ⊓ MeasureTheory.ae MeasureTheory.volume) (𝓝 c)<VAR>hs : UniqueDiffWithinAt ℝ s a := by uniqueDiffWithinAt_Ici_Iic_univ<GOAL>derivWithin (fun u => ∫ (x : ℝ) in u..b, f x) s a = -c
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>hf : IntervalIntegrable f MeasureTheory.volume a b<VAR>s t : Set ℝ<VAR>intervalIntegral.FTCFilter a (𝓝[s] a) (𝓝[t] a)<VAR>hmeas : StronglyMeasurableAtFilter f (𝓝[t] a) MeasureTheory.volume<VAR>ha : ContinuousWithinAt f t a<VAR>hs : UniqueDiffWithinAt ℝ s a := by uniqueDiffWithinAt_Ici_Iic_univ<GOAL>derivWithin (fun u => ∫ (x : ℝ) in u..b, f x) s a = -f a
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>a : ℝ<VAR>s : Set ℝ<VAR>hintg : ∀ x ∈ s, IntervalIntegrable f MeasureTheory.volume a x<VAR>hcont : Continuous f<GOAL>DifferentiableOn ℝ (fun u => ∫ (x : ℝ) in a..u, f x) s
<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a ≤ b<VAR>hcont : ContinuousOn g (Set.Icc a b)<VAR>hderiv : ∀ x ∈ Set.Ico a b, HasDerivWithinAt g (g' x) (Set.Ioi x) x<VAR>φint : MeasureTheory.IntegrableOn φ (Set.Icc a b) MeasureTheory.volume<VAR>hφg : ∀ x ∈ Set.Ico a b, g' x ≤ φ x<GOAL>g b - g a ≤ ∫ (y : ℝ) in a..b, φ y
<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a ≤ b<VAR>hcont : ContinuousOn g (Set.Icc a b)<VAR>hderiv : ∀ x ∈ Set.Ioo a b, HasDerivWithinAt g (g' x) (Set.Ioi x) x<VAR>φint : MeasureTheory.IntegrableOn φ (Set.Icc a b) MeasureTheory.volume<VAR>hφg : ∀ x ∈ Set.Ioo a b, g' x ≤ φ x<GOAL>g b - g a ≤ ∫ (y : ℝ) in a..b, φ y
<VAR>g' g φ : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a ≤ b<VAR>hcont : ContinuousOn g (Set.Icc a b)<VAR>hderiv : ∀ x ∈ Set.Ioo a b, HasDerivWithinAt g (g' x) (Set.Ioi x) x<VAR>φint : MeasureTheory.IntegrableOn φ (Set.Icc a b) MeasureTheory.volume<VAR>hφg : ∀ x ∈ Set.Ioo a b, φ x ≤ g' x<GOAL>∫ (y : ℝ) in a..b, φ y ≤ g b - g a
<VAR>g' g : ℝ → ℝ<VAR>a b : ℝ<VAR>hab : a ≤ b<VAR>hcont : ContinuousOn g (Set.Icc a b)<VAR>hderiv : ∀ x ∈ Set.Ioo a b, HasDerivWithinAt g (g' x) (Set.Ioi x) x<VAR>g'int : MeasureTheory.IntegrableOn g' (Set.Icc a b) MeasureTheory.volume<GOAL>∫ (y : ℝ) in a..b, g' y = g b - g a
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>CompleteSpace E<VAR>f f' : ℝ → E<VAR>hab : a ≤ b<VAR>hcont : ContinuousOn f (Set.Icc a b)<VAR>hderiv : ∀ x ∈ Set.Ioo a b, HasDerivWithinAt f (f' x) (Set.Ioi x) x<VAR>f'int : IntervalIntegrable f' MeasureTheory.volume a b<GOAL>∫ (y : ℝ) in a..b, f' y = f b - f a
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>CompleteSpace E<VAR>f f' : ℝ → E<VAR>hcont : ContinuousOn f [[a, b]]<VAR>hderiv : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x<VAR>hint : IntervalIntegrable f' MeasureTheory.volume a b<GOAL>∫ (y : ℝ) in a..b, f' y = f b - f a
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>CompleteSpace E<VAR>f f' : ℝ → E<VAR>hab : a ≤ b<VAR>hcont : ContinuousOn f (Set.Icc a b)<VAR>hderiv : ∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x<VAR>hint : IntervalIntegrable f' MeasureTheory.volume a b<GOAL>∫ (y : ℝ) in a..b, f' y = f b - f a
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>CompleteSpace E<VAR>f f' : ℝ → E<VAR>hderiv : ∀ x ∈ [[a, b]], HasDerivAt f (f' x) x<VAR>hint : IntervalIntegrable f' MeasureTheory.volume a b<GOAL>∫ (y : ℝ) in a..b, f' y = f b - f a
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>CompleteSpace E<VAR>f f' : ℝ → E<VAR>hab : a < b<VAR>fa fb : E<VAR>hderiv : ∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x<VAR>hint : IntervalIntegrable f' MeasureTheory.volume a b<VAR>ha : Filter.Tendsto f (𝓝[>] a) (𝓝 fa)<VAR>hb : Filter.Tendsto f (𝓝[<] b) (𝓝 fb)<GOAL>∫ (y : ℝ) in a..b, f' y = fb - fa
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>CompleteSpace E<VAR>f : ℝ → E<VAR>hderiv : ∀ x ∈ [[a, b]], DifferentiableAt ℝ f x<VAR>hint : IntervalIntegrable (deriv f) MeasureTheory.volume a b<GOAL>∫ (y : ℝ) in a..b, deriv f y = f b - f a
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>CompleteSpace E<VAR>f' : ℝ → E<VAR>f : ℝ → E<VAR>hderiv : deriv f = f'<VAR>hdiff : ∀ x ∈ [[a, b]], DifferentiableAt ℝ f x<VAR>hcont : ContinuousOn f' [[a, b]]<GOAL>∫ (y : ℝ) in a..b, f' y = f b - f a
<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>RCLike 𝕜<VAR>NormedSpace 𝕜 E<VAR>IsScalarTower ℝ 𝕜 E<VAR>f f' : 𝕜 → E<VAR>z₀ z₁ : 𝕜<VAR>hcont : ContinuousOn (fun t => f' (z₀ + t • z₁)) (Set.Icc 0 1)<VAR>hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (z₀ + t • z₁)) (z₀ + t • z₁)<GOAL>z₁ • ∫ (t : ℝ) in 0 ..1, f' (z₀ + t • z₁) = f (z₀ + z₁) - f z₀
<VAR>g' g : ℝ → ℝ<VAR>a b : ℝ<VAR>hcont : ContinuousOn g (Set.Icc a b)<VAR>hderiv : ∀ x ∈ Set.Ioo a b, HasDerivWithinAt g (g' x) (Set.Ioi x) x<VAR>g'pos : ∀ x ∈ Set.Ioo a b, 0 ≤ g' x<GOAL>MeasureTheory.IntegrableOn g' (Set.Ioc a b) MeasureTheory.volume
<VAR>g' g : ℝ → ℝ<VAR>a b : ℝ<VAR>hcont : ContinuousOn g (Set.Icc a b)<VAR>hderiv : ∀ x ∈ Set.Ioo a b, HasDerivAt g (g' x) x<VAR>g'pos : ∀ x ∈ Set.Ioo a b, 0 ≤ g' x<GOAL>MeasureTheory.IntegrableOn g' (Set.Ioc a b) MeasureTheory.volume
<VAR>g' g : ℝ → ℝ<VAR>a b : ℝ<VAR>hcont : ContinuousOn g [[a, b]]<VAR>hderiv : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt g (g' x) x<VAR>hpos : ∀ x ∈ Set.Ioo (min a b) (max a b), 0 ≤ g' x<GOAL>IntervalIntegrable g' MeasureTheory.volume a b
<VAR>A : Type u_5<VAR>a b : ℝ<VAR>NormedRing A<VAR>NormedAlgebra ℝ A<VAR>CompleteSpace A<VAR>u v u' v' : ℝ → A<VAR>hu : ContinuousOn u [[a, b]]<VAR>hv : ContinuousOn v [[a, b]]<VAR>huu' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Set.Ioi x) x<VAR>hvv' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Set.Ioi x) x<VAR>hu' : IntervalIntegrable u' MeasureTheory.volume a b<VAR>hv' : IntervalIntegrable v' MeasureTheory.volume a b<GOAL>∫ (x : ℝ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a
<VAR>A : Type u_5<VAR>a b : ℝ<VAR>NormedRing A<VAR>NormedAlgebra ℝ A<VAR>CompleteSpace A<VAR>u v u' v' : ℝ → A<VAR>hu : ContinuousOn u [[a, b]]<VAR>hv : ContinuousOn v [[a, b]]<VAR>huu' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt u (u' x) x<VAR>hvv' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt v (v' x) x<VAR>hu' : IntervalIntegrable u' MeasureTheory.volume a b<VAR>hv' : IntervalIntegrable v' MeasureTheory.volume a b<GOAL>∫ (x : ℝ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a
<VAR>A : Type u_5<VAR>a b : ℝ<VAR>NormedRing A<VAR>NormedAlgebra ℝ A<VAR>CompleteSpace A<VAR>u v u' v' : ℝ → A<VAR>hu : ∀ x ∈ [[a, b]], HasDerivWithinAt u (u' x) [[a, b]] x<VAR>hv : ∀ x ∈ [[a, b]], HasDerivWithinAt v (v' x) [[a, b]] x<VAR>hu' : IntervalIntegrable u' MeasureTheory.volume a b<VAR>hv' : IntervalIntegrable v' MeasureTheory.volume a b<GOAL>∫ (x : ℝ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a
<VAR>A : Type u_5<VAR>a b : ℝ<VAR>NormedRing A<VAR>NormedAlgebra ℝ A<VAR>CompleteSpace A<VAR>u v u' v' : ℝ → A<VAR>hu : ∀ x ∈ [[a, b]], HasDerivAt u (u' x) x<VAR>hv : ∀ x ∈ [[a, b]], HasDerivAt v (v' x) x<VAR>hu' : IntervalIntegrable u' MeasureTheory.volume a b<VAR>hv' : IntervalIntegrable v' MeasureTheory.volume a b<GOAL>∫ (x : ℝ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a
<VAR>A : Type u_5<VAR>a b : ℝ<VAR>NormedRing A<VAR>NormedAlgebra ℝ A<VAR>CompleteSpace A<VAR>u v u' v' : ℝ → A<VAR>hu : ContinuousOn u [[a, b]]<VAR>hv : ContinuousOn v [[a, b]]<VAR>huu' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Set.Ioi x) x<VAR>hvv' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Set.Ioi x) x<VAR>hu' : IntervalIntegrable u' MeasureTheory.volume a b<VAR>hv' : IntervalIntegrable v' MeasureTheory.volume a b<GOAL>∫ (x : ℝ) in a..b, u x * v' x = u b * v b - u a * v a - ∫ (x : ℝ) in a..b, u' x * v x
<VAR>A : Type u_5<VAR>a b : ℝ<VAR>NormedRing A<VAR>NormedAlgebra ℝ A<VAR>CompleteSpace A<VAR>u v u' v' : ℝ → A<VAR>hu : ContinuousOn u [[a, b]]<VAR>hv : ContinuousOn v [[a, b]]<VAR>huu' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt u (u' x) x<VAR>hvv' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt v (v' x) x<VAR>hu' : IntervalIntegrable u' MeasureTheory.volume a b<VAR>hv' : IntervalIntegrable v' MeasureTheory.volume a b<GOAL>∫ (x : ℝ) in a..b, u x * v' x = u b * v b - u a * v a - ∫ (x : ℝ) in a..b, u' x * v x
<VAR>A : Type u_5<VAR>a b : ℝ<VAR>NormedRing A<VAR>NormedAlgebra ℝ A<VAR>CompleteSpace A<VAR>u v u' v' : ℝ → A<VAR>hu : ∀ x ∈ [[a, b]], HasDerivWithinAt u (u' x) [[a, b]] x<VAR>hv : ∀ x ∈ [[a, b]], HasDerivWithinAt v (v' x) [[a, b]] x<VAR>hu' : IntervalIntegrable u' MeasureTheory.volume a b<VAR>hv' : IntervalIntegrable v' MeasureTheory.volume a b<GOAL>∫ (x : ℝ) in a..b, u x * v' x = u b * v b - u a * v a - ∫ (x : ℝ) in a..b, u' x * v x
<VAR>A : Type u_5<VAR>a b : ℝ<VAR>NormedRing A<VAR>NormedAlgebra ℝ A<VAR>CompleteSpace A<VAR>u v u' v' : ℝ → A<VAR>hu : ∀ x ∈ [[a, b]], HasDerivAt u (u' x) x<VAR>hv : ∀ x ∈ [[a, b]], HasDerivAt v (v' x) x<VAR>hu' : IntervalIntegrable u' MeasureTheory.volume a b<VAR>hv' : IntervalIntegrable v' MeasureTheory.volume a b<GOAL>∫ (x : ℝ) in a..b, u x * v' x = u b * v b - u a * v a - ∫ (x : ℝ) in a..b, u' x * v x
<VAR>a b : ℝ<VAR>G : Type u_6<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f f' : ℝ → ℝ<VAR>g : ℝ → G<VAR>hf : ContinuousOn f [[a, b]]<VAR>hff' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x<VAR>hg_cont : ContinuousOn g (f '' Set.Ioo (min a b) (max a b))<VAR>hg1 : MeasureTheory.IntegrableOn g (f '' [[a, b]]) MeasureTheory.volume<VAR>hg2 : MeasureTheory.IntegrableOn (fun x => f' x • (g ∘ f) x) [[a, b]] MeasureTheory.volume<GOAL>∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u
<VAR>a b : ℝ<VAR>G : Type u_6<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f f' : ℝ → ℝ<VAR>g : ℝ → G<VAR>hf : ContinuousOn f [[a, b]]<VAR>hff' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x<VAR>hf' : ContinuousOn f' [[a, b]]<VAR>hg : ContinuousOn g (f '' [[a, b]])<GOAL>∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (u : ℝ) in f a..f b, g u
<VAR>a b : ℝ<VAR>G : Type u_6<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f f' : ℝ → ℝ<VAR>g : ℝ → G<VAR>h : ∀ x ∈ [[a, b]], HasDerivAt f (f' x) x<VAR>h' : ContinuousOn f' [[a, b]]<VAR>hg : ContinuousOn g (f '' [[a, b]])<GOAL>∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (x : ℝ) in f a..f b, g x
<VAR>a b : ℝ<VAR>G : Type u_6<VAR>NormedAddCommGroup G<VAR>NormedSpace ℝ G<VAR>f f' : ℝ → ℝ<VAR>g : ℝ → G<VAR>h : ∀ x ∈ [[a, b]], HasDerivAt f (f' x) x<VAR>h' : ContinuousOn f' [[a, b]]<VAR>hg : Continuous g<GOAL>∫ (x : ℝ) in a..b, f' x • (g ∘ f) x = ∫ (x : ℝ) in f a..f b, g x
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>CompleteSpace E<VAR>f f' : ℝ → ℝ<VAR>g g' : ℝ → E<VAR>hf : ContinuousOn f [[a, b]]<VAR>hff' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x<VAR>hf' : ContinuousOn f' [[a, b]]<VAR>hg : ContinuousOn g [[f a, f b]]<VAR>hgg' : ∀ x ∈ Set.Ioo (min (f a) (f b)) (max (f a) (f b)), HasDerivWithinAt g (g' x) (Set.Ioi x) x<VAR>hg' : ContinuousOn g' (f '' [[a, b]])<GOAL>∫ (x : ℝ) in a..b, f' x • (g' ∘ f) x = (g ∘ f) b - (g ∘ f) a
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ℝ<VAR>CompleteSpace E<VAR>f f' : ℝ → ℝ<VAR>g g' : ℝ → E<VAR>hf : ∀ x ∈ [[a, b]], HasDerivAt f (f' x) x<VAR>hg : ∀ x ∈ [[a, b]], HasDerivAt g (g' (f x)) (f x)<VAR>hf' : ContinuousOn f' [[a, b]]<VAR>hg' : Continuous g'<GOAL>∫ (x : ℝ) in a..b, f' x • (g' ∘ f) x = (g ∘ f) b - (g ∘ f) a
<VAR>a b : ℝ<VAR>f f' g : ℝ → ℝ<VAR>hf : ContinuousOn f [[a, b]]<VAR>hff' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x<VAR>hg_cont : ContinuousOn g (f '' Set.Ioo (min a b) (max a b))<VAR>hg1 : MeasureTheory.IntegrableOn g (f '' [[a, b]]) MeasureTheory.volume<VAR>hg2 : MeasureTheory.IntegrableOn (fun x => (g ∘ f) x * f' x) [[a, b]] MeasureTheory.volume<GOAL>∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (u : ℝ) in f a..f b, g u
<VAR>a b : ℝ<VAR>f f' g : ℝ → ℝ<VAR>hf : ContinuousOn f [[a, b]]<VAR>hff' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x<VAR>hf' : ContinuousOn f' [[a, b]]<VAR>hg : ContinuousOn g (f '' [[a, b]])<GOAL>∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (u : ℝ) in f a..f b, g u
<VAR>a b : ℝ<VAR>f f' g : ℝ → ℝ<VAR>h : ∀ x ∈ [[a, b]], HasDerivAt f (f' x) x<VAR>h' : ContinuousOn f' [[a, b]]<VAR>hg : ContinuousOn g (f '' [[a, b]])<GOAL>∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (x : ℝ) in f a..f b, g x
<VAR>a b : ℝ<VAR>f f' g : ℝ → ℝ<VAR>h : ∀ x ∈ [[a, b]], HasDerivAt f (f' x) x<VAR>h' : ContinuousOn f' [[a, b]]<VAR>hg : Continuous g<GOAL>∫ (x : ℝ) in a..b, (g ∘ f) x * f' x = ∫ (x : ℝ) in f a..f b, g x
<VAR>a b : ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hf : ContinuousOn f [[a, b]]<VAR>hff' : ∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x<VAR>hf' : ContinuousOn f' [[a, b]]<VAR>hg : ContinuousOn g [[f a, f b]]<VAR>hgg' : ∀ x ∈ Set.Ioo (min (f a) (f b)) (max (f a) (f b)), HasDerivWithinAt g (g' x) (Set.Ioi x) x<VAR>hg' : ContinuousOn g' (f '' [[a, b]])<GOAL>∫ (x : ℝ) in a..b, (g' ∘ f) x * f' x = (g ∘ f) b - (g ∘ f) a
<VAR>a b : ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hf : ∀ x ∈ [[a, b]], HasDerivAt f (f' x) x<VAR>hg : ∀ x ∈ [[a, b]], HasDerivAt g (g' (f x)) (f x)<VAR>hf' : ContinuousOn f' [[a, b]]<VAR>hg' : Continuous g'<GOAL>∫ (x : ℝ) in a..b, (g' ∘ f) x * f' x = (g ∘ f) b - (g ∘ f) a
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : Besicovitch.SatelliteConfig E N τ<GOAL>a.centerAndRescale.c (Fin.last N) = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>N : ℕ<VAR>τ : ℝ<VAR>a : Besicovitch.SatelliteConfig E N τ<GOAL>a.centerAndRescale.r (Fin.last N) = 1