mathlib-initiative/mathlib-tactics huggingface dataset:
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
hf : ∀ t ∈ Set.uIcc 0 1, ContDiffAt ℝ (↑0 + 1) f (x + t • y)
t : ℝ
ht : t ∈ Set.uIcc 0 1
⊢ ↑0 + 1 ≠ 0

Tactic:
by

Goal state after:
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
hf : ∀ t ∈ Set.uIcc 0 1, ContDiffAt ℝ (↑0 + 1) f (x + t • y)
⊢ Set.EqOn (fun t ↦ (fderiv ℝ f (x + t • y)) y) (deriv fun s ↦ f (x + s • y)) (Set.uIcc 0 1)

Tactic:
by

Goal state after:
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
hf : ∀ t ∈ Set.uIcc 0 1, ContDiffAt ℝ (↑0 + 1) f (x + t • y)
h_eq : Set.EqOn (fun t ↦ (fderiv ℝ f (x + t • y)) y) (deriv fun s ↦ f (x + s • y)) (Set.uIcc 0 1)
t : ℝ
ht : t ∈ Set.uIcc 0 1
⊢ ↑0 + 1 ≠ 0

Tactic:
by

Goal state after:
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
hf : ∀ t ∈ Set.uIcc 0 1, ContDiffAt ℝ (↑0 + 1) f (x + t • y)
h_eq : Set.EqOn (fun t ↦ (fderiv ℝ f (x + t • y)) y) (deriv fun s ↦ f (x + s • y)) (Set.uIcc 0 1)
t : ℝ
ht : t ∈ Set.uIcc 0 1
⊢ DifferentiableAt ℝ (fun s ↦ x + s • y) t

Tactic:
by

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

Goal state before:
pp: 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
⊢ n + 1 ≤ n + 1

Tactic:
by

Goal state after:
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
hf : ∀ t ∈ Set.uIcc 0 1, ContDiffAt ℝ (↑0 + 1) f (x + t • y)
h_eq : Set.EqOn (fun t ↦ (fderiv ℝ f (x + t • y)) y) (deriv fun s ↦ f (x + s • y)) (Set.uIcc 0 1)
hf' : ∀ t ∈ Set.uIcc 0 1, DifferentiableAt ℝ (fun s ↦ f (x + s • y)) t
⊢ ContinuousOn (fderiv ℝ f) ((fun t ↦ x + t • y) '' Set.uIcc 0 1)

Tactic:
by

Goal state after:
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
hf : ∀ t ∈ Set.uIcc 0 1, ContDiffAt ℝ (↑0 + 1) f (x + t • y)
h_eq : Set.EqOn (fun t ↦ (fderiv ℝ f (x + t • y)) y) (deriv fun s ↦ f (x + s • y)) (Set.uIcc 0 1)
hf' : ∀ t ∈ Set.uIcc 0 1, DifferentiableAt ℝ (fun s ↦ f (x + s • y)) t
h₁ : ContinuousOn (fderiv ℝ f) ((fun t ↦ x + t • y) '' Set.uIcc 0 1)
⊢ ContinuousOn (fun x_1 ↦ x + x_1 • y) (Set.uIcc 0 1)

Tactic:
by

Goal state after:
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
hf : ∀ t ∈ Set.uIcc 0 1, ContDiffAt ℝ (↑0 + 1) f (x + t • y)
h_eq : Set.EqOn (fun t ↦ (fderiv ℝ f (x + t • y)) y) (deriv fun s ↦ f (x + s • y)) (Set.uIcc 0 1)
hf' : ∀ t ∈ Set.uIcc 0 1, DifferentiableAt ℝ (fun s ↦ f (x + s • y)) t
h₁ : ContinuousOn (fderiv ℝ f) ((fun t ↦ x + t • y) '' Set.uIcc 0 1)
⊢ ContinuousOn (fun x_1 ↦ fderiv ℝ f (x + x_1 • y)) (Set.uIcc 0 1)

Tactic:
by

Goal state after:
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
hf : ∀ t ∈ Set.uIcc 0 1, ContDiffAt ℝ (↑0 + 1) f (x + t • y)
h_eq : Set.EqOn (fun t ↦ (fderiv ℝ f (x + t • y)) y) (deriv fun s ↦ f (x + s • y)) (Set.uIcc 0 1)
hf' : ∀ t ∈ Set.uIcc 0 1, DifferentiableAt ℝ (fun s ↦ f (x + s • y)) t
⊢ IntervalIntegrable (deriv fun s ↦ f (x + s • y)) MeasureTheory.volume 0 1

Tactic:
by

Goal state after:
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 :
  (∀ t ∈ Set.uIcc 0 1, ContDiffAt ℝ (↑n + 1) f (x + t • y)) →
    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)
t : ℝ
ht : t ∈ Set.uIcc 0 1
⊢ ↑n + 1 ≤ ↑(n + 1) + 1

Tactic:
by

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

Goal state before:
pp: 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 : ℝ
⊢ DifferentiableAt ℝ (HSub.hSub x) t

Tactic:
by

Goal state after:
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 : ℝ
⊢ -((↑n !)⁻¹ * (1 - t) ^ n) = (↑(n + 1)!)⁻¹ * ((↑n + 1) * (1 - t) ^ n * -1)

Tactic:
by

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
x✝ : ℕ
⊢ x✝ ≤ x✝ + 1

Tactic:
by

Goal state after:
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 : ℝ), HasDerivAt (u (n + 1)) (-u n t) t

Tactic:
by

Goal state after:
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)
δ' : ℝ := ⋯
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)).PairwiseDisjoint 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:
rw [PairwiseDisjoint]
          convert! hp₁.pairwise_disjoint_on_Ioc_succ.set_pairwise (Finset.range p.1) using 3
          rw [uIoc_of_le (hp₁ (by lia)), Nat.succ_eq_succ]

Goal state after:
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
⊢ Continuous (u n)

Tactic:
by

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) ≤
    ∑ i ∈ Finset.range (T s).1, dist (f ((T s).2 i).1) (f ((T s).2 i).2) + ∑ b ∈ u_coe s, dist (f b.1) (f b.2)

Tactic:
by

Goal state after:
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
⊢ DifferentiableAt ℝ (iteratedFDeriv ℝ (n + 1) f) (x + t • y)

Tactic:
by

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)
dist_le_sum :
  ∀ (s : Finset ↑u),
    dist (f d) (f b) ≤
      ∑ i ∈ Finset.range (T s).1, dist (f ((T s).2 i).1) (f ((T s).2 i).2) + ∑ b ∈ u_coe s, dist (f b.1) (f b.2)
⊢ Tendsto (fun x ↦ dist (f d) (f b)) atTop (𝓝 (dist (f d) (f b)))

Tactic:
by

Goal state after:
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 ∈ Set.uIcc 0 1, HasDerivAt (v (n + 1)) (v (n + 1 + 1) t) t

Tactic:
by

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 (ℝ × ℝ)
hu₁ : ∀ z ∈ u, d < z.1 ∧ z.1 < z.2 ∧ z.2 < b
hu₂ : u.PairwiseDisjoint fun z ↦ Icc z.1 z.2
hu₃ : HasSum (fun z ↦ (↑z).2 - (↑z).1) (b - d)
hu₄ : HasSum (fun z ↦ dist (f (↑z).1) (f (↑z).2)) y
⊢ dist (f d) (f b) ≤ y

Tactic:
by

Goal state after:
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
hv : ∀ t ∈ Set.uIcc 0 1, HasDerivAt (v (n + 1)) (v (n + 1 + 1) t) t
t : ℝ
ht : t ∈ Set.uIcc 0 1
⊢ 0 + ↑(n + 1 + 1) ≤ ↑(n + 1) + 1

Tactic:
by

Goal state after:
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
hv : ∀ t ∈ Set.uIcc 0 1, HasDerivAt (v (n + 1)) (v (n + 1 + 1) t) t
t : ℝ
ht : t ∈ Set.uIcc 0 1
h_cont : ContinuousAt (iteratedFDeriv ℝ (n + 1 + 1) f) (x + t • y)
⊢ ContinuousAt (fun t ↦ x + t • y) t

Tactic:
by

Goal state after:
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
hv : ∀ t ∈ Set.uIcc 0 1, HasDerivAt (v (n + 1)) (v (n + 1 + 1) t) t
⊢ ContinuousOn (v (n + 1 + 1)) (Set.uIcc 0 1)

Tactic:
by

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
a b : ℝ
hf : AbsolutelyContinuousOnInterval f a b
hf₀ : ∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt f 0 x
this :
  ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {f : ℝ → F} {a b : ℝ},
    AbsolutelyContinuousOnInterval f a b →
      (∀ᵐ (x : ℝ), x ∈ uIcc a b → HasDerivAt f 0 x) → a ≤ b → ∃ C, ∀ x ∈ uIcc a b, f x = C
hab : ¬a ≤ b
⊢ b ≤ a

Tactic:
by

Goal state after:
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 ∈ uIcc a b → HasDerivAt f 0 x
hab : a ≤ b
this : ∀ x ∈ uIcc a b, f x = f b
⊢ ∃ C, ∀ x ∈ uIcc a b, f x = C

Tactic:
by

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

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf :
  ∀ k ≤ n,
    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
⊢ f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / ↑n !) • iteratedDerivWithin (n + 1) f [[x₀, x]] t

Tactic:
by

Goal state after:
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 : d ∈ Icc a b
this : ∀ r > 0, dist (f d) (f b) ≤ r
⊢ f d = f b

Tactic:
by

Goal state after:
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
hf : ∀ t ∈ Set.Icc 0 1, ContDiffAt ℝ (↑n + 1) f (x + t • y)
⊢ 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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: M : ℝ
hM : M ≤ 1
⊢ stolzSet M = ∅

Tactic:
by

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

Goal state before:
pp: M : ℝ
hM : 1 < M
⊢ 1 ∈ Set.Ioo 0 2

Tactic:
by

Goal state after:
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
⊢ a ≤ d

Tactic:
by

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

Goal state before:
pp: f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hf₁ : ContDiffOn ℝ (↑n) f [[x₀, x]]
hf₂ : AbsolutelyContinuousOnInterval (iteratedDerivWithin n f [[x₀, x]]) x₀ x
this : x₀ ≠ x
k : ℕ
hk✝ : k ≤ n
hk : k < n
⊢ ↑k.succ ≤ ↑n

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: s : ℝ
⊢ 0 < 2 * √(1 + s ^ 2) + 1

Tactic:
by

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

Goal state before:
pp: s : ℝ
⊢ 0 < 1 / (1 + s ^ 2)

Tactic:
by

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

Goal state before:
pp: f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hf₁ : ContDiffOn ℝ (↑n) f [[x₀, x]]
hf₂ : AbsolutelyContinuousOnInterval (iteratedDerivWithin n f [[x₀, x]]) x₀ x
⊢ f x - taylorWithinEval f n [[x₀, x]] x₀ x =
    ∫ (t : ℝ) in x₀..x, (x - t) ^ n / ↑n ! * iteratedDerivWithin (n + 1) f [[x₀, x]] t

Tactic:
by

Goal state after: