mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case e'_2.x
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this✝ : x₀ ≠ x
n : ℕ
ih :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / ↑n !) • iteratedDerivWithin (n + 1) f [[x₀, x]] t
hf :
  ∀ k ≤ n + 1,
    let u := fun t ↦ (x - t) ^ k / ↑k !;
    let v := fun t ↦ iteratedDerivWithin k f [[x₀, x]] t;
    ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
this :
  let u := fun t ↦ (x - t) ^ (n + 1) / ↑(n + 1)!;
  let v := fun t ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t;
  ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
⊢ ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / ↑n !) • iteratedDerivWithin (n + 1) f [[x₀, x]] t =
    ∫ (x_1 : ℝ) in x₀..x,
      -((deriv (fun x_2 ↦ (x - x_2) ^ (n + 1)) x_1 / ↑(n.succ * n !)) • iteratedDerivWithin (n + 1) f [[x₀, x]] x_1)

Tactic:
]

Goal state after:
case e'_2.x
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this✝ : x₀ ≠ x
n : ℕ
ih :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / ↑n !) • iteratedDerivWithin (n + 1) f [[x₀, x]] t
hf :
  ∀ k ≤ n + 1,
    let u := fun t ↦ (x - t) ^ k / ↑k !;
    let v := fun t ↦ iteratedDerivWithin k f [[x₀, x]] t;
    ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
this :
  let u := fun t ↦ (x - t) ^ (n + 1) / ↑(n + 1)!;
  let v := fun t ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t;
  ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
⊢ ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / ↑n !) • iteratedDerivWithin (n + 1) f [[x₀, x]] t =
    ∫ (x_1 : ℝ) in x₀..x,
      -((deriv (fun x_2 ↦ (x - x_2) ^ (n + 1)) x_1 / ↑(n.succ * n !)) • iteratedDerivWithin (n + 1) f [[x₀, x]] x_1)
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case a.right
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 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) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ 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) < 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / (↑n + 1) < δ / (b - a)
δ' : ℝ := (b - a) / (↑n + 1)
hδ₃ : δ' < δ
h_mono : Monotone fun i ↦ a + ↑i * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
x y : ℝ
x✝³ : a ≤ x
x✝² : x ≤ y
x✝¹ : y < x + δ
x✝ : y ≤ b
p : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone ↑p.2
hp₂ : ∀ (i : ℕ), ↑p.2 i ∈ Icc x y
⊢ (↑(Finset.range (p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))).1)).Pairwise
    (Disjoint on fun i ↦
      uIoc ((p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))).2 i).1 ((p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))).2 i).2)

Tactic:
]

Goal state after:
case a.right
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 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) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ 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) < 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / (↑n + 1) < δ / (b - a)
δ' : ℝ := (b - a) / (↑n + 1)
hδ₃ : δ' < δ
h_mono : Monotone fun i ↦ a + ↑i * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
x y : ℝ
x✝³ : a ≤ x
x✝² : x ≤ y
x✝¹ : y < x + δ
x✝ : y ≤ b
p : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone ↑p.2
hp₂ : ∀ (i : ℕ), ↑p.2 i ∈ Icc x y
⊢ (↑(Finset.range (p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))).1)).Pairwise
    (Disjoint on fun i ↦
      uIoc ((p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))).2 i).1 ((p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))).2 i).2)
Module: Mathlib.Analysis.Calculus.TaylorIntegral

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
f : E → F
x y : E
n✝ : ℕ
inst✝ : CompleteSpace F
n : ℕ
ih :
  f (x + y) =
    (∑ k ∈ Finset.range (n + 1), (↑k !)⁻¹ • (iteratedFDeriv ℝ k f x) fun x ↦ y) +
      (↑n !)⁻¹ • ∫ (t : ℝ) in 0..1, (1 - t) ^ n • (iteratedFDeriv ℝ (n + 1) f (x + t • y)) fun x ↦ y
hf : ∀ t ∈ Set.uIcc 0 1, ContDiffAt ℝ (↑(n + 1) + 1) f (x + t • y)
u : ℕ → ℝ → ℝ := fun k t ↦ (↑k !)⁻¹ * (1 - t) ^ k
t : ℝ
⊢ (1 - t) ^ n * ↑((n + 1) * n !) = ↑n ! * (1 - t) ^ n * (↑n + 1)

Tactic:
]

Goal state after:
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
f : E → F
x y : E
n✝ : ℕ
inst✝ : CompleteSpace F
n : ℕ
ih :
  f (x + y) =
    (∑ k ∈ Finset.range (n + 1), (↑k !)⁻¹ • (iteratedFDeriv ℝ k f x) fun x ↦ y) +
      (↑n !)⁻¹ • ∫ (t : ℝ) in 0..1, (1 - t) ^ n • (iteratedFDeriv ℝ (n + 1) f (x + t • y)) fun x ↦ y
hf : ∀ t ∈ Set.uIcc 0 1, ContDiffAt ℝ (↑(n + 1) + 1) f (x + t • y)
u : ℕ → ℝ → ℝ := fun k t ↦ (↑k !)⁻¹ * (1 - t) ^ k
t : ℝ
⊢ (1 - t) ^ n * ↑((n + 1) * n !) = ↑n ! * (1 - t) ^ n * (↑n + 1)
Module: Mathlib.Analysis.Calculus.TaylorIntegral

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
f : E → F
x y : E
n✝ : ℕ
inst✝ : CompleteSpace F
n : ℕ
ih :
  f (x + y) =
    (∑ k ∈ Finset.range (n + 1), (↑k !)⁻¹ • (iteratedFDeriv ℝ k f x) fun x ↦ y) +
      (↑n !)⁻¹ • ∫ (t : ℝ) in 0..1, (1 - t) ^ n • (iteratedFDeriv ℝ (n + 1) f (x + t • y)) fun x ↦ y
hf : ∀ t ∈ Set.uIcc 0 1, ContDiffAt ℝ (↑(n + 1) + 1) f (x + t • y)
u : ℕ → ℝ → ℝ := fun k t ↦ (↑k !)⁻¹ * (1 - t) ^ k
t : ℝ
this : -((↑n !)⁻¹ * (1 - t) ^ n) = (↑(n + 1)!)⁻¹ * ((↑n + 1) * (1 - t) ^ n * -1)
⊢ HasDerivAt (fun t ↦ (↑(n + 1)!)⁻¹ * (1 - t) ^ (n + 1)) ((↑(n + 1)!)⁻¹ * ((↑n + 1) * (1 - t) ^ n * -1)) t

Tactic:
]

Goal state after:
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
f : E → F
x y : E
n✝ : ℕ
inst✝ : CompleteSpace F
n : ℕ
ih :
  f (x + y) =
    (∑ k ∈ Finset.range (n + 1), (↑k !)⁻¹ • (iteratedFDeriv ℝ k f x) fun x ↦ y) +
      (↑n !)⁻¹ • ∫ (t : ℝ) in 0..1, (1 - t) ^ n • (iteratedFDeriv ℝ (n + 1) f (x + t • y)) fun x ↦ y
hf : ∀ t ∈ Set.uIcc 0 1, ContDiffAt ℝ (↑(n + 1) + 1) f (x + t • y)
u : ℕ → ℝ → ℝ := fun k t ↦ (↑k !)⁻¹ * (1 - t) ^ k
t : ℝ
this : -((↑n !)⁻¹ * (1 - t) ^ n) = (↑(n + 1)!)⁻¹ * ((↑n + 1) * (1 - t) ^ n * -1)
⊢ HasDerivAt (fun t ↦ (↑(n + 1)!)⁻¹ * (1 - t) ^ (n + 1)) ((↑(n + 1)!)⁻¹ * ((↑n + 1) * (1 - t) ^ n * -1)) t
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case e'_2.x.e_f
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this✝ : x₀ ≠ x
n : ℕ
ih :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / ↑n !) • iteratedDerivWithin (n + 1) f [[x₀, x]] t
hf :
  ∀ k ≤ n + 1,
    let u := fun t ↦ (x - t) ^ k / ↑k !;
    let v := fun t ↦ iteratedDerivWithin k f [[x₀, x]] t;
    ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
this :
  let u := fun t ↦ (x - t) ^ (n + 1) / ↑(n + 1)!;
  let v := fun t ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t;
  ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
t : ℝ
⊢ ((x - t) ^ n / ↑n !) • iteratedDerivWithin (n + 1) f [[x₀, x]] t =
    -(↑(n + 1) * (x - t) ^ (n + 1 - 1) * -(fun x ↦ 1) t / ↑(n.succ * n !)) • iteratedDerivWithin (n + 1) f [[x₀, x]] t

Tactic:
]

Goal state after:
case e'_2.x.e_f
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this✝ : x₀ ≠ x
n : ℕ
ih :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / ↑n !) • iteratedDerivWithin (n + 1) f [[x₀, x]] t
hf :
  ∀ k ≤ n + 1,
    let u := fun t ↦ (x - t) ^ k / ↑k !;
    let v := fun t ↦ iteratedDerivWithin k f [[x₀, x]] t;
    ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
this :
  let u := fun t ↦ (x - t) ^ (n + 1) / ↑(n + 1)!;
  let v := fun t ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t;
  ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
t : ℝ
⊢ ((x - t) ^ n / ↑n !) • iteratedDerivWithin (n + 1) f [[x₀, x]] t =
    -(↑(n + 1) * (x - t) ^ (n + 1 - 1) * -(fun x ↦ 1) t / ↑(n.succ * n !)) • iteratedDerivWithin (n + 1) f [[x₀, x]] t
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 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) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ 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) < 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / (↑n + 1) < δ / (b - a)
δ' : ℝ := (b - a) / (↑n + 1)
hδ₃ : δ' < δ
h_mono : Monotone fun i ↦ a + ↑i * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
x y : ℝ
x✝⁴ : a ≤ x
x✝³ : x ≤ y
x✝² : y < x + δ
x✝¹ : y ≤ b
p : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone ↑p.2
hp₂ : ∀ (i : ℕ), ↑p.2 i ∈ Icc x y
x✝ : ℕ
⊢ Ioc (↑p.2 x✝) (↑p.2 (x✝ + 1)) = Ioc (↑p.2 x✝) (↑p.2 x✝.succ)

Tactic:
]

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
u_coe : Finset ↑u → Finset (ℝ × ℝ) := fun s ↦ Finset.image Subtype.val s
hu₁ : ∀ (s : Finset ↑u) ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hu₂ : ∀ (s : Finset ↑u), (↑(u_coe s)).PairwiseDisjoint fun z ↦ Icc z.1 z.2
T : Finset ↑u → ℕ × (ℕ → ℝ × ℝ) := fun s ↦ ((u_coe s).card + 1, fun i ↦ (u_coe s).intervalGapsWithin ⋯ d b ↑i)
hT₁ : ∀ (s : Finset ↑u) (i : ℕ), d ≤ ((u_coe s).intervalGapsWithin ⋯ d b ↑i).1
hT₂ : ∀ (s : Finset ↑u) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b ↑i).1 ≤ ((u_coe s).intervalGapsWithin ⋯ d b ↑i).2
hT₃ : ∀ (s : Finset ↑u) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b ↑i).2 ≤ b
hT₄ :
  ∀ (s : Finset ↑u),
    (Iio ((u_coe s).card + 1)).PairwiseDisjoint fun j ↦
      Ioc ((u_coe s).intervalGapsWithin ⋯ d b ↑j).1 ((u_coe s).intervalGapsWithin ⋯ d b ↑j).2
hT : MapsTo T univ (disjWithin d b)
u_coe_sum : ∀ (s : Finset ↑u) (g : ℝ → ℝ → ℝ), ∑ b ∈ s, g (↑b).1 (↑b).2 = ∑ z ∈ u_coe s, g z.1 z.2
hu₃ : Tendsto T atTop (totalLengthFilter ⊓ 𝓟 (disjWithin d b))
hu₄ : Tendsto (fun s ↦ ∑ z ∈ u_coe s, dist (f z.1) (f z.2)) (SummationFilter.unconditional ↑u).filter (𝓝 y)
sum_tendsto :
  Tendsto
    (fun x ↦ ∑ i ∈ Finset.range (T x).1, dist (f ((T x).2 i).1) (f ((T x).2 i).2) + ∑ z ∈ u_coe x, dist (f z.1) (f z.2))
    atTop (𝓝 y)
s : Finset ↑u
⊢ dist (f d) (f b) ≤ dist (f ((T s).2 0).1) (f ((T s).2 (u_coe s).card).2)

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
f : ℝ → X
d b y : ℝ
hdb : d ≤ b
hf : AbsolutelyContinuousOnInterval f d b
u : Set (ℝ × ℝ)
u_coe : Finset ↑u → Finset (ℝ × ℝ) := fun s ↦ Finset.image Subtype.val s
hu₁ : ∀ (s : Finset ↑u) ⦃z : ℝ × ℝ⦄, z ∈ u_coe s → d ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
hu₂ : ∀ (s : Finset ↑u), (↑(u_coe s)).PairwiseDisjoint fun z ↦ Icc z.1 z.2
T : Finset ↑u → ℕ × (ℕ → ℝ × ℝ) := fun s ↦ ((u_coe s).card + 1, fun i ↦ (u_coe s).intervalGapsWithin ⋯ d b ↑i)
hT₁ : ∀ (s : Finset ↑u) (i : ℕ), d ≤ ((u_coe s).intervalGapsWithin ⋯ d b ↑i).1
hT₂ : ∀ (s : Finset ↑u) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b ↑i).1 ≤ ((u_coe s).intervalGapsWithin ⋯ d b ↑i).2
hT₃ : ∀ (s : Finset ↑u) (i : ℕ), ((u_coe s).intervalGapsWithin ⋯ d b ↑i).2 ≤ b
hT₄ :
  ∀ (s : Finset ↑u),
    (Iio ((u_coe s).card + 1)).PairwiseDisjoint fun j ↦
      Ioc ((u_coe s).intervalGapsWithin ⋯ d b ↑j).1 ((u_coe s).intervalGapsWithin ⋯ d b ↑j).2
hT : MapsTo T univ (disjWithin d b)
u_coe_sum : ∀ (s : Finset ↑u) (g : ℝ → ℝ → ℝ), ∑ b ∈ s, g (↑b).1 (↑b).2 = ∑ z ∈ u_coe s, g z.1 z.2
hu₃ : Tendsto T atTop (totalLengthFilter ⊓ 𝓟 (disjWithin d b))
hu₄ : Tendsto (fun s ↦ ∑ z ∈ u_coe s, dist (f z.1) (f z.2)) (SummationFilter.unconditional ↑u).filter (𝓝 y)
sum_tendsto :
  Tendsto
    (fun x ↦ ∑ i ∈ Finset.range (T x).1, dist (f ((T x).2 i).1) (f ((T x).2 i).2) + ∑ z ∈ u_coe x, dist (f z.1) (f z.2))
    atTop (𝓝 y)
s : Finset ↑u
⊢ dist (f d) (f b) ≤ dist (f ((T s).2 0).1) (f ((T s).2 (u_coe s).card).2)
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case e'_3
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this✝ : x₀ ≠ x
n : ℕ
ih :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / ↑n !) • iteratedDerivWithin (n + 1) f [[x₀, x]] t
hf :
  ∀ k ≤ n + 1,
    let u := fun t ↦ (x - t) ^ k / ↑k !;
    let v := fun t ↦ iteratedDerivWithin k f [[x₀, x]] t;
    ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
this :
  let u := fun t ↦ (x - t) ^ (n + 1) / ↑(n + 1)!;
  let v := fun t ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t;
  ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
x✝¹ : ℝ
x✝ : x✝¹ ∈ uIoo x₀ x
h1 : min x₀ x < x✝¹
h2 : x✝¹ < max x₀ x
⊢ ((x - x✝¹) ^ (n + 1) / ((↑n + 1) * ↑n !)) • derivWithin (iteratedDerivWithin (n + 1) f [[x₀, x]]) [[x₀, x]] x✝¹ =
    (fun t ↦ (x - t) ^ (n + 1) / ↑(n + 1)!) x✝¹ • deriv (fun t ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) x✝¹

Tactic:
]

Goal state after:
case e'_3
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this✝ : x₀ ≠ x
n : ℕ
ih :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / ↑n !) • iteratedDerivWithin (n + 1) f [[x₀, x]] t
hf :
  ∀ k ≤ n + 1,
    let u := fun t ↦ (x - t) ^ k / ↑k !;
    let v := fun t ↦ iteratedDerivWithin k f [[x₀, x]] t;
    ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
this :
  let u := fun t ↦ (x - t) ^ (n + 1) / ↑(n + 1)!;
  let v := fun t ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t;
  ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
x✝¹ : ℝ
x✝ : x✝¹ ∈ uIoo x₀ x
h1 : min x₀ x < x✝¹
h2 : x✝¹ < max x₀ x
⊢ ((x - x✝¹) ^ (n + 1) / ((↑n + 1) * ↑n !)) • derivWithin (iteratedDerivWithin (n + 1) f [[x₀, x]]) [[x₀, x]] x✝¹ =
    (fun t ↦ (x - t) ^ (n + 1) / ↑(n + 1)!) x✝¹ • deriv (fun t ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) x✝¹
Module: Mathlib.Analysis.Calculus.TaylorIntegral

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
f : E → F
x y : E
n✝ : ℕ
inst✝ : CompleteSpace F
n : ℕ
ih :
  f (x + y) =
    (∑ k ∈ Finset.range (n + 1), (↑k !)⁻¹ • (iteratedFDeriv ℝ k f x) fun x ↦ y) +
      (↑n !)⁻¹ • ∫ (t : ℝ) in 0..1, (1 - t) ^ n • (iteratedFDeriv ℝ (n + 1) f (x + t • y)) fun x ↦ y
hf : ∀ t ∈ Set.uIcc 0 1, ContDiffAt ℝ (↑(n + 1) + 1) f (x + t • y)
u : ℕ → ℝ → ℝ := fun k t ↦ (↑k !)⁻¹ * (1 - t) ^ k
hu : ∀ (t : ℝ), HasDerivAt (u (n + 1)) (-u n t) t
hu' : Continuous (u n)
v : ℕ → ℝ → F := fun k t ↦ (iteratedFDeriv ℝ k f (x + t • y)) fun x ↦ y
t : ℝ
ht : t ∈ Set.uIcc 0 1
⊢ HasDerivAt (fun t ↦ (iteratedFDeriv ℝ (n + 1) f (x + t • y)) fun x ↦ y)
    (deriv (fun s ↦ (iteratedFDeriv ℝ (n + 1) f (x + s • y)) fun x ↦ y) t) t

Tactic:
]

Goal state after:
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
f : E → F
x y : E
n✝ : ℕ
inst✝ : CompleteSpace F
n : ℕ
ih :
  f (x + y) =
    (∑ k ∈ Finset.range (n + 1), (↑k !)⁻¹ • (iteratedFDeriv ℝ k f x) fun x ↦ y) +
      (↑n !)⁻¹ • ∫ (t : ℝ) in 0..1, (1 - t) ^ n • (iteratedFDeriv ℝ (n + 1) f (x + t • y)) fun x ↦ y
hf : ∀ t ∈ Set.uIcc 0 1, ContDiffAt ℝ (↑(n + 1) + 1) f (x + t • y)
u : ℕ → ℝ → ℝ := fun k t ↦ (↑k !)⁻¹ * (1 - t) ^ k
hu : ∀ (t : ℝ), HasDerivAt (u (n + 1)) (-u n t) t
hu' : Continuous (u n)
v : ℕ → ℝ → F := fun k t ↦ (iteratedFDeriv ℝ k f (x + t • y)) fun x ↦ y
t : ℝ
ht : t ∈ Set.uIcc 0 1
⊢ HasDerivAt (fun t ↦ (iteratedFDeriv ℝ (n + 1) f (x + t • y)) fun x ↦ y)
    (deriv (fun s ↦ (iteratedFDeriv ℝ (n + 1) f (x + s • y)) fun x ↦ y) t) t
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case e'_3.e_a.e_a
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this✝ : x₀ ≠ x
n : ℕ
ih :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / ↑n !) • iteratedDerivWithin (n + 1) f [[x₀, x]] t
hf :
  ∀ k ≤ n + 1,
    let u := fun t ↦ (x - t) ^ k / ↑k !;
    let v := fun t ↦ iteratedDerivWithin k f [[x₀, x]] t;
    ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
this :
  let u := fun t ↦ (x - t) ^ (n + 1) / ↑(n + 1)!;
  let v := fun t ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t;
  ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
x✝¹ : ℝ
x✝ : x✝¹ ∈ uIoo x₀ x
h1 : min x₀ x < x✝¹
h2 : x✝¹ < max x₀ x
⊢ (↑n + 1) * ↑n ! = (↑n + 1) * ↑n !

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 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) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ 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) < 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / (↑n + 1) < δ / (b - a)
δ' : ℝ := (b - a) / (↑n + 1)
hδ₃ : δ' < δ
h_mono : Monotone fun i ↦ a + ↑i * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
x y : ℝ
x✝³ : a ≤ x
x✝² : x ≤ y
x✝¹ : y < x + δ
x✝ : y ≤ b
p : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone ↑p.2
hp₂ : ∀ (i : ℕ), ↑p.2 i ∈ Icc x y
this : ↑p.2 p.1 - ↑p.2 0 < δ
⊢ ∑ i ∈ Finset.range (p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))).1,
      dist ((p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))).2 i).1 ((p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))).2 i).2 =
    ∑ i ∈ Finset.range p.1, (↑p.2 (i + 1) - ↑p.2 i)

Tactic:
]

Goal state after:
F : Type u_2
inst✝ : SeminormedAddCommGroup F
a✝ b✝ : ℝ
f : ℝ → F
a b : ℝ
hf :
  ∀ ε > 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) < ε
hab₀ : a ≤ b
hab : a < b
δ : ℝ
hδ₁ : δ > 0
hδ₂ :
  ∀ 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) < 1
hab₁ : 0 < b - a
n : ℕ
hn : 1 / (↑n + 1) < δ / (b - a)
δ' : ℝ := (b - a) / (↑n + 1)
hδ₃ : δ' < δ
h_mono : Monotone fun i ↦ a + ↑i * δ'
v_sum : eVariationOn f (Icc a b) = ∑ i ∈ Finset.range (n + 1), eVariationOn f (Icc (a + ↑i * δ') (a + (↑i + 1) * δ'))
x y : ℝ
x✝³ : a ≤ x
x✝² : x ≤ y
x✝¹ : y < x + δ
x✝ : y ≤ b
p : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ Icc x y }
hp₁ : Monotone ↑p.2
hp₂ : ∀ (i : ℕ), ↑p.2 i ∈ Icc x y
this : ↑p.2 p.1 - ↑p.2 0 < δ
⊢ ∑ i ∈ Finset.range (p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))).1,
      dist ((p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))).2 i).1 ((p.1, fun i ↦ (↑p.2 i, ↑p.2 (i + 1))).2 i).2 =
    ∑ i ∈ Finset.range p.1, (↑p.2 (i + 1) - ↑p.2 i)
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: case e'_3.e_a
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this✝ : x₀ ≠ x
n : ℕ
ih :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / ↑n !) • iteratedDerivWithin (n + 1) f [[x₀, x]] t
hf :
  ∀ k ≤ n + 1,
    let u := fun t ↦ (x - t) ^ k / ↑k !;
    let v := fun t ↦ iteratedDerivWithin k f [[x₀, x]] t;
    ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
this :
  let u := fun t ↦ (x - t) ^ (n + 1) / ↑(n + 1)!;
  let v := fun t ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t;
  ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
x✝¹ : ℝ
x✝ : x✝¹ ∈ uIoo x₀ x
h1 : min x₀ x < x✝¹
h2 : x✝¹ < max x₀ x
⊢ derivWithin (iteratedDerivWithin (n + 1) f [[x₀, x]]) [[x₀, x]] x✝¹ =
    derivWithin (fun t ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) (Icc (min x₀ x) (max x₀ x)) x✝¹

Tactic:
]

Goal state after:
case e'_3.e_a
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
this✝ : x₀ ≠ x
n : ℕ
ih :
  f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / ↑n !) • iteratedDerivWithin (n + 1) f [[x₀, x]] t
hf :
  ∀ k ≤ n + 1,
    let u := fun t ↦ (x - t) ^ k / ↑k !;
    let v := fun t ↦ iteratedDerivWithin k f [[x₀, x]] t;
    ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
this :
  let u := fun t ↦ (x - t) ^ (n + 1) / ↑(n + 1)!;
  let v := fun t ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t;
  ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t
x✝¹ : ℝ
x✝ : x✝¹ ∈ uIoo x₀ x
h1 : min x₀ x < x✝¹
h2 : x✝¹ < max x₀ x
⊢ derivWithin (iteratedDerivWithin (n + 1) f [[x₀, x]]) [[x₀, x]] x✝¹ =
    derivWithin (fun t ↦ iteratedDerivWithin (n + 1) f [[x₀, x]] t) (Icc (min x₀ x) (max x₀ x)) x✝¹
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: F✝ : Type u_2
inst✝³ : NormedAddCommGroup F✝
inst✝² : NormedSpace ℝ F✝
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Icc a b → HasDerivAt f 0 x
hab : a ≤ b
⊢ ∀ x ∈ Icc a b, f x = f b

Tactic:
]

Goal state after:
F✝ : Type u_2
inst✝³ : NormedAddCommGroup F✝
inst✝² : NormedSpace ℝ F✝
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Icc a b → HasDerivAt f 0 x
hab : a ≤ b
⊢ ∀ x ∈ Icc a b, f x = f b
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: F✝ : Type u_2
inst✝³ : NormedAddCommGroup F✝
inst✝² : NormedSpace ℝ F✝
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Icc a b → HasDerivAt f 0 x
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
⊢ dist (f d) (f b) ≤ r

Tactic:
]

Goal state after:
F✝ : Type u_2
inst✝³ : NormedAddCommGroup F✝
inst✝² : NormedSpace ℝ F✝
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Icc a b → HasDerivAt f 0 x
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
⊢ dist (f d) (f b) ≤ r
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: M : ℝ
hM : M ≤ 1
z : ℂ
⊢ 0 < 1 - ‖z‖ → M * (1 - ‖z‖) ≤ ‖1 - z‖

Tactic:
]

Goal state after:
M : ℝ
hM : M ≤ 1
z : ℂ
⊢ 0 < 1 - ‖z‖ → M * (1 - ‖z‖) ≤ ‖1 - z‖
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: M : ℝ
hM : M ≤ 1
z : ℂ
zn : 0 < 1 - ‖z‖
⊢ 1 - ‖z‖ = 1 - ‖z‖

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: M : ℝ
hM : 1 < M
⊢ Tendsto id (Filter.map ofReal (𝓝[<] 1)) (𝓝[stolzSet M] 1)

Tactic:
]

Goal state after:
M : ℝ
hM : 1 < M
⊢ Tendsto id (Filter.map ofReal (𝓝[<] 1)) (𝓝[stolzSet M] 1)