mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
hg :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
⊢ ∀ᶠ (x : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter,
    x ∈ disjWithin a b →
      ∑ i ∈ Finset.range x.1, dist ((f • g) (x.2 i).1) ((f • g) (x.2 i).2) ≤
        C * ∑ i ∈ Finset.range x.1, dist (g (x.2 i).1) (g (x.2 i).2) +
          D * ∑ i ∈ Finset.range x.1, dist (f (x.2 i).1) (f (x.2 i).2)

Tactic:
]

Goal state after:
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
hg :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
⊢ ∀ᶠ (x : ℕ × (ℕ → ℝ × ℝ)) in totalLengthFilter,
    x ∈ disjWithin a b →
      ∑ i ∈ Finset.range x.1, dist ((f • g) (x.2 i).1) ((f • g) (x.2 i).2) ≤
        C * ∑ i ∈ Finset.range x.1, dist (g (x.2 i).1) (g (x.2 i).2) +
          D * ∑ i ∈ Finset.range x.1, dist (f (x.2 i).1) (f (x.2 i).2)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable

Goal state before:
pp: case e'_3
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun n ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (G n) (volume.restrict (uIcc a b))
hG' : liminf (fun n ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
hG'₀ : liminf (fun n ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≠ ⊤
integrable_f_deriv : Integrable (deriv f) (volume.restrict (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ}, x ∈ Ioo a b → 0 ≤ deriv f x
ebound : ∫ (x : ℝ) in a..b, ‖deriv f x‖ ≤ f b - f a
⊢ EqOn (deriv f) (fun x ↦ ‖deriv f x‖) (Ioo a b)

Tactic:
]

Goal state after:
case e'_3
f : ℝ → ℝ
a b : ℝ
hf : MonotoneOn f (Icc a b)
hab : a ≤ b
G : ℕ → ℝ → ℝ
hGf : ∀ᵐ (x : ℝ), x ∈ uIcc a b → Tendsto (fun n ↦ G n x) atTop (𝓝 (deriv f x))
hG : ∀ (n : ℕ), AEStronglyMeasurable (G n) (volume.restrict (uIcc a b))
hG' : liminf (fun n ↦ ∫⁻ (x : ℝ) in uIcc a b, ‖G n x‖ₑ) atTop ≤ ENNReal.ofReal (f b - f a)
hG'₀ : liminf (fun n ↦ ∫⁻ (x : ℝ) in Icc a b, ‖G n x‖ₑ) atTop ≠ ⊤
integrable_f_deriv : Integrable (deriv f) (volume.restrict (Icc a b))
this : f a ≤ f b
f_deriv_nonneg : ∀ {x : ℝ}, x ∈ Ioo a b → 0 ≤ deriv f x
ebound : ∫ (x : ℝ) in a..b, ‖deriv f x‖ ≤ f b - f a
⊢ EqOn (deriv f) (fun x ↦ ‖deriv f x‖) (Ioo a b)
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable

Goal state before:
pp: a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
⊢ ∀ᵐ (x : ℝ), x ∈ uIoc a b → deriv p x - deriv q x = deriv (p - q) x

Tactic:
]

Goal state after:
a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
⊢ ∀ᵐ (x : ℝ), x ∈ uIoc a b → deriv p x - deriv q x = deriv (p - q) x
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable

Goal state before:
pp: a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableWithinAt ℝ p (uIcc a b) x
hx₂ : x ∈ uIcc a b → DifferentiableWithinAt ℝ q (uIcc a b) x
hx₃ : x ≠ max a b
hx₄ : min a b < x ∧ x ≤ max a b
hx₅ : x ∈ uIcc a b
⊢ deriv p x - deriv q x = deriv (p - q) x

Tactic:
]

Goal state after:
a b : ℝ
p q : ℝ → ℝ
hp : MonotoneOn p (uIcc a b)
hq : MonotoneOn q (uIcc a b)
hf : BoundedVariationOn (p - q) (uIcc a b)
h₂ : ∀ᵐ (x : ℝ), x ≠ max a b
x : ℝ
hx₁ : x ∈ uIcc a b → DifferentiableWithinAt ℝ p (uIcc a b) x
hx₂ : x ∈ uIcc a b → DifferentiableWithinAt ℝ q (uIcc a b) x
hx₃ : x ≠ max a b
hx₄ : min a b < x ∧ x ≤ max a b
hx₅ : x ∈ uIcc a b
⊢ deriv p x - deriv q x = deriv (p - q) x
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
C : ℝ≥0
inst✝ : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : (↑C + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
v : E
hv : v ∈ ball 0 r
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : w ∈ sphere 0 1
hvw : v = ρ • w
hρ : ρ = ‖v‖
⊢ ‖v‖ = ‖v‖

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: case μB
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb✝ : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
A : ℝ × ℝ
hA : A ∈ t
⊢ 2 * (3 * (A.2 - A.1)) ≤ 6 * (A.2 - A.1)

Tactic:
]

Goal state after:
case μB
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb✝ : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
A : ℝ × ℝ
hA : A ∈ t
⊢ 2 * (3 * (A.2 - A.1)) ≤ 6 * (A.2 - A.1)
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case h₁
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
hg :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
n : ℕ
I : ℕ → ℝ × ℝ
hnI :
  (∀ i ∈ Finset.range n, (I i).1 ∈ uIcc a b ∧ (I i).2 ∈ uIcc a b) ∧
    (↑(Finset.range n)).PairwiseDisjoint fun i ↦ uIoc (I i).1 (I i).2
i : ℕ
hi : i ∈ Finset.range n
⊢ ‖f (I i).1‖ * dist (g (I i).1) (g (I i).2) ≤ C * dist (g (I i).1) (g (I i).2)

Tactic:
]

Goal state after:
case h₁
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
hg :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
n : ℕ
I : ℕ → ℝ × ℝ
hnI :
  (∀ i ∈ Finset.range n, (I i).1 ∈ uIcc a b ∧ (I i).2 ∈ uIcc a b) ∧
    (↑(Finset.range n)).PairwiseDisjoint fun i ↦ uIoc (I i).1 (I i).2
i : ℕ
hi : i ∈ Finset.range n
⊢ ‖f (I i).1‖ * dist (g (I i).1) (g (I i).2) ≤ C * dist (g (I i).1) (g (I i).2)
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ : ℝ
⊢ ∑ x ∈ Finset.range (n + 1),
        (PolynomialModule.comp (Polynomial.X - Polynomial.C x₀))
          (PolynomialModule.single ℝ x (taylorCoeffWithin f x s x₀)) +
      (PolynomialModule.comp (Polynomial.X - Polynomial.C x₀))
        (PolynomialModule.single ℝ (n + 1) (taylorCoeffWithin f (n + 1) s x₀)) =
    ∑ k ∈ Finset.range (n + 1),
        (PolynomialModule.comp (Polynomial.X - Polynomial.C x₀))
          (PolynomialModule.single ℝ k (taylorCoeffWithin f k s x₀)) +
      (PolynomialModule.comp (Polynomial.X - Polynomial.C x₀))
        (PolynomialModule.single ℝ (n + 1) (taylorCoeffWithin f (n + 1) s x₀))

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb✝ : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
x : ℝ
hx : x ∈ s
this : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (f' x))
δ : ℝ
hδ₁ : δ > 0
hδ₂ : ∀ ⦃x_1 : ℝ⦄, x_1 ∈ {x}ᶜ → dist x_1 x < δ → dist (slope f x x_1) (f' x) < η
α : ℝ
hα : 0 < α
⊢ ∃ t, (∀ y ∈ t, y ∈ Ioi 0 → y < α) ∧ IsOpen t ∧ 0 ∈ t

Tactic:
]

Goal state after:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb✝ : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
x : ℝ
hx : x ∈ s
this : Tendsto (slope f x) (𝓝[≠] x) (𝓝 (f' x))
δ : ℝ
hδ₁ : δ > 0
hδ₂ : ∀ ⦃x_1 : ℝ⦄, x_1 ∈ {x}ᶜ → dist x_1 x < δ → dist (slope f x x_1) (f' x) < η
α : ℝ
hα : 0 < α
⊢ ∃ t, (∀ y ∈ t, y ∈ Ioi 0 → y < α) ∧ IsOpen t ∧ 0 ∈ t
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case e_a
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ x : ℝ
⊢ ((↑n !)⁻¹ * (↑n + 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀ =
    ((↑n !)⁻¹ * (↑n + 1)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
C : ℝ≥0
inst✝ : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : (↑C + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
v : E
hv : v ∈ ball 0 r
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : w ∈ sphere 0 1
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
⊢ ‖w - y‖ < δ

Tactic:
]

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
C : ℝ≥0
inst✝ : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f (L v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : (↑C + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : sphere 0 1 ⊆ ⋃ y ∈ q, ball y δ
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖
v : E
hv : v ∈ ball 0 r
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : w ∈ sphere 0 1
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
⊢ ‖w - y‖ < δ
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case h₂
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
hg :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
n : ℕ
I : ℕ → ℝ × ℝ
hnI :
  (∀ i ∈ Finset.range n, (I i).1 ∈ uIcc a b ∧ (I i).2 ∈ uIcc a b) ∧
    (↑(Finset.range n)).PairwiseDisjoint fun i ↦ uIoc (I i).1 (I i).2
i : ℕ
hi : i ∈ Finset.range n
⊢ dist (f (I i).1 • g (I i).2) (f (I i).2 • g (I i).2) ≤ dist (f (I i).1) (f (I i).2) * D

Tactic:
]

Goal state after:
case h₂
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
hg :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
n : ℕ
I : ℕ → ℝ × ℝ
hnI :
  (∀ i ∈ Finset.range n, (I i).1 ∈ uIcc a b ∧ (I i).2 ∈ uIcc a b) ∧
    (↑(Finset.range n)).PairwiseDisjoint fun i ↦ uIoc (I i).1 (I i).2
i : ℕ
hi : i ∈ Finset.range n
⊢ dist (f (I i).1 • g (I i).2) (f (I i).2 • g (I i).2) ≤ dist (f (I i).1) (f (I i).2) * D
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case succ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
k : ℕ
hk : taylorWithinEval f k s x₀ x = ∑ k ∈ Finset.range (k + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀
⊢ ∑ k ∈ Finset.range (k + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀ +
      (((↑k + 1) * ↑k !)⁻¹ * (x - x₀) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s x₀ =
    ∑ x_1 ∈ Finset.range (k + 1), ((↑x_1 !)⁻¹ * (x - x₀) ^ x_1) • iteratedDerivWithin x_1 f s x₀ +
      ((↑(k + 1)!)⁻¹ * (x - x₀) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s x₀

Tactic:
]

Goal state after:
case succ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
k : ℕ
hk : taylorWithinEval f k s x₀ x = ∑ k ∈ Finset.range (k + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀
⊢ ∑ k ∈ Finset.range (k + 1), ((↑k !)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀ +
      (((↑k + 1) * ↑k !)⁻¹ * (x - x₀) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s x₀ =
    ∑ x_1 ∈ Finset.range (k + 1), ((↑x_1 !)⁻¹ * (x - x₀) ^ x_1) • iteratedDerivWithin x_1 f s x₀ +
      ((↑(k + 1)!)⁻¹ * (x - x₀) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s x₀
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case h₂
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
hg :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
n : ℕ
I : ℕ → ℝ × ℝ
hnI :
  (∀ i ∈ Finset.range n, (I i).1 ∈ uIcc a b ∧ (I i).2 ∈ uIcc a b) ∧
    (↑(Finset.range n)).PairwiseDisjoint fun i ↦ uIoc (I i).1 (I i).2
i : ℕ
hi : i ∈ Finset.range n
⊢ dist (f (I i).1) (f (I i).2) * dist (g (I i).2) 0 ≤ dist (f (I i).1) (f (I i).2) * D

Tactic:
]

Goal state after:
case h₂
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
hg :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
n : ℕ
I : ℕ → ℝ × ℝ
hnI :
  (∀ i ∈ Finset.range n, (I i).1 ∈ uIcc a b ∧ (I i).2 ∈ uIcc a b) ∧
    (↑(Finset.range n)).PairwiseDisjoint fun i ↦ uIoc (I i).1 (I i).2
i : ℕ
hi : i ∈ Finset.range n
⊢ dist (f (I i).1) (f (I i).2) * dist (g (I i).2) 0 ≤ dist (f (I i).1) (f (I i).2) * D
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
n : ℕ
s : Set ℝ
hs : UniqueDiffOn ℝ s
hf : (∀ m ≤ n, ContinuousOn (iteratedDerivWithin m f s) s) ∧ ∀ m < n, DifferentiableOn ℝ (iteratedDerivWithin m f s) s
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ ContinuousOn (iteratedDerivWithin i f s) s

Tactic:
]

Goal state after:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
n : ℕ
s : Set ℝ
hs : UniqueDiffOn ℝ s
hf : (∀ m ≤ n, ContinuousOn (iteratedDerivWithin m f s) s) ∧ ∀ m < n, DifferentiableOn ℝ (iteratedDerivWithin m f s) s
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ ContinuousOn (iteratedDerivWithin i f s) s
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case hbc
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
hg :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
n : ℕ
I : ℕ → ℝ × ℝ
hnI :
  (∀ i ∈ Finset.range n, (I i).1 ∈ uIcc a b ∧ (I i).2 ∈ uIcc a b) ∧
    (↑(Finset.range n)).PairwiseDisjoint fun i ↦ uIoc (I i).1 (I i).2
i : ℕ
hi : i ∈ Finset.range n
⊢ ‖g (I i).2‖ ≤ D

Tactic:
]

Goal state after:
case hbc
F : Type u_2
inst✝³ : SeminormedAddCommGroup F
a b : ℝ
M : Type u_3
inst✝² : SeminormedRing M
inst✝¹ : Module M F
inst✝ : NormSMulClass M F
f : ℝ → M
g : ℝ → F
hf :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
hg :
  Tendsto (fun E ↦ ∑ i ∈ Finset.range E.1, dist (g (E.2 i).1) (g (E.2 i).2)) (totalLengthFilter ⊓ 𝓟 (disjWithin a b))
    (𝓝 0)
C : ℝ
hC : ∀ x ∈ uIcc a b, ‖f x‖ ≤ C
D : ℝ
hD : ∀ x ∈ uIcc a b, ‖g x‖ ≤ D
n : ℕ
I : ℕ → ℝ × ℝ
hnI :
  (∀ i ∈ Finset.range n, (I i).1 ∈ uIcc a b ∧ (I i).2 ∈ uIcc a b) ∧
    (↑(Finset.range n)).PairwiseDisjoint fun i ↦ uIoc (I i).1 (I i).2
i : ℕ
hi : i ∈ Finset.range n
⊢ ‖g (I i).2‖ ≤ D
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: t x : ℝ
n : ℕ
⊢ HasDerivAt (fun y ↦ (-y + x) ^ (n + 1)) ((↑n + 1) * (-t + x) ^ n * -1) t

Tactic:
]

Goal state after:
t x : ℝ
n : ℕ
⊢ HasDerivAt (fun y ↦ (-y + x) ^ (n + 1)) ((↑n + 1) * (-t + x) ^ n * -1) t
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y
⊢ derivWithin (iteratedDerivWithin (k + 1) f s) s y = derivWithin (iteratedDerivWithin (k + 1) f s) t y

Tactic:
]

Goal state after:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y
⊢ derivWithin (iteratedDerivWithin (k + 1) f s) s y = derivWithin (iteratedDerivWithin (k + 1) f s) t y
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
⊢ ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
a b : ℝ
f : ℝ → X
K : ℝ≥0
hfK : LipschitzOnWith K f (uIcc a b)
⊢ ∀ ε > 0,
    ∃ δ > 0,
      ∀ E ∈ disjWithin a b,
        ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
          ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
this : -((↑k !)⁻¹ * (x - y) ^ k) = ((↑k + 1) * ↑k !)⁻¹ * (-(↑k + 1) * (x - y) ^ k)
⊢ HasDerivWithinAt (fun t ↦ ((↑k + 1) * ↑k !)⁻¹ * (x - t) ^ (k + 1)) (((↑k + 1) * ↑k !)⁻¹ * (-(↑k + 1) * (x - y) ^ k)) t
    y

Tactic:
]

Goal state after:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
k : ℕ
s t : Set ℝ
ht : UniqueDiffWithinAt ℝ t y
hs : s ∈ 𝓝[t] y
hf : HasDerivWithinAt (iteratedDerivWithin (k + 1) f s) (iteratedDerivWithin (k + 2) f s y) t y
this : -((↑k !)⁻¹ * (x - y) ^ k) = ((↑k + 1) * ↑k !)⁻¹ * (-(↑k + 1) * (x - y) ^ k)
⊢ HasDerivWithinAt (fun t ↦ ((↑k + 1) * ↑k !)⁻¹ * (x - t) ^ (k + 1)) (((↑k + 1) * ↑k !)⁻¹ * (-(↑k + 1) * (x - y) ^ k)) t
    y
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb✝ : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
u : Set (ℝ × ℝ)
hu₁ : ∀ x ∈ u, (d < x.1 ∧ x.1 < x.2 ∧ x.2 < b) ∧ dist (slope f x.1 x.2) (f' x.1) < η
hu₂ : u.Countable
hu₃ : u.PairwiseDisjoint fun z ↦ Icc z.1 z.2
hu₄ : ∀ᵐ (a : ℝ), a ∉ s \ ⋃ z ∈ u, Icc z.1 z.2
this✝ : Countable ↑u
this : Pairwise (Disjoint on fun z ↦ Icc (↑z).1 (↑z).2)
⊢ ∀ᵐ (a : ℝ), a ∉ Ioo d b \ ⋃ z ∈ u, Icc z.1 z.2

Tactic:
]

Goal state after:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → F
d b η : ℝ
hdb✝ : d ≤ b
hf : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f (f' x) x
hη : 0 < η
hdb : d < b
t : Set (ℝ × ℝ) := {z | (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η}
s : Set ℝ := {x | x ∈ Ioo d b ∧ HasDerivAt f (f' x) x}
u : Set (ℝ × ℝ)
hu₁ : ∀ x ∈ u, (d < x.1 ∧ x.1 < x.2 ∧ x.2 < b) ∧ dist (slope f x.1 x.2) (f' x.1) < η
hu₂ : u.Countable
hu₃ : u.PairwiseDisjoint fun z ↦ Icc z.1 z.2
hu₄ : ∀ᵐ (a : ℝ), a ∉ s \ ⋃ z ∈ u, Icc z.1 z.2
this✝ : Countable ↑u
this : Pairwise (Disjoint on fun z ↦ Icc (↑z).1 (↑z).2)
⊢ ∀ᵐ (a : ℝ), a ∉ Ioo d b \ ⋃ z ∈ u, Icc z.1 z.2
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case zero
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
s s' : Set ℝ
hs_unique : UniqueDiffOn ℝ s
hs' : s' ∈ 𝓝[s] y
hy : y ∈ s'
h : s' ⊆ s
hs'_unique : UniqueDiffWithinAt ℝ s' y
hf : ContDiffOn ℝ (↑0) f s
hf' : DifferentiableWithinAt ℝ f s y
⊢ HasDerivWithinAt (fun t ↦ f t) (derivWithin f s y) s' y

Tactic:
]

Goal state after:
case zero
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x y : ℝ
s s' : Set ℝ
hs_unique : UniqueDiffOn ℝ s
hs' : s' ∈ 𝓝[s] y
hy : y ∈ s'
h : s' ⊆ s
hs'_unique : UniqueDiffWithinAt ℝ s' y
hf : ContDiffOn ℝ (↑0) f s
hf' : DifferentiableWithinAt ℝ f s y
⊢ HasDerivWithinAt (fun t ↦ f t) (derivWithin f s y) s' y