mathlib-initiative/mathlib-tactics huggingface dataset:
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‖ < δ
this : ‖y - w‖ < δ
⊢ ↑C * (ρ * ‖w - y‖) + ρ * (‖L‖ * ‖y - w‖) + δ * ρ ≤ ↑C * (ρ * δ) + ρ * (‖L‖ * δ) + δ * ρ

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‖ < δ
this : ‖y - w‖ < δ
⊢ ↑C * (ρ * ‖w - y‖) + ρ * (‖L‖ * ‖y - w‖) + δ * ρ ≤ ↑C * (ρ * δ) + ρ * (‖L‖ * δ) + δ * ρ
Module: Mathlib.Analysis.Calculus.Rademacher

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
s : Set E
s_count : s.Countable
s_dense : Dense s
⊢ sphere 0 1 ⊆ univ

Tactic:
;

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
C : ℝ≥0
f : E → ℝ
μ : Measure E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
hf : LipschitzWith C f
s : Set E
s_count : s.Countable
s_dense : Dense s
⊢ sphere 0 1 ⊆ univ
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
⊢ Icc x y ⊆ Icc a b

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
⊢ Icc x y ⊆ Icc a b
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
z : E
t : ℝ
ht : t ∈ Set.uIcc 0 1
hz : (fun t ↦ x + t • y) t = z
⊢ ContinuousWithinAt (fderiv ℝ f) ((fun t ↦ x + t • y) '' Set.uIcc 0 1) ((fun t ↦ x + t • y) t)

Tactic:
exact (((hf t ht).fderiv_right (le_refl _)).continuousAt (n := 0)).continuousWithinAt

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

Goal state before:
pp: case e_f
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 < δ
⊢ (fun i ↦ 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) = fun i ↦
    ↑p.2 (i + 1) - ↑p.2 i

Tactic:
;

Goal state after:
case e_f
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 < δ
⊢ (fun i ↦ 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) = fun i ↦
    ↑p.2 (i + 1) - ↑p.2 i
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
⊢ ∀ r > 0, dist (f d) (f b) ≤ r

Tactic:
intro r

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 : d ∈ Icc a b
r : ℝ
⊢ r > 0 → dist (f d) (f b) ≤ r
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ (1 - x) ^ 2 + |y| ^ 2 ≤ (1 - x) ^ 2 + (s * x) ^ 2

Tactic:
;

Goal state after:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ (1 - x) ^ 2 + |y| ^ 2 ≤ (1 - x) ^ 2 + (s * x) ^ 2
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ (1 - x) ^ 2 + (s * x) ^ 2 = 1 - 2 * x + (1 + s ^ 2) * x * x

Tactic:
;

Goal state after:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ (1 - x) ^ 2 + (s * x) ^ 2 = 1 - 2 * x + (1 + s ^ 2) * x * x
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ 1 - 2 * x + (1 + s ^ 2) * (1 / (1 + s ^ 2)) * x = 1 - x

Tactic:
;

Goal state after:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
⊢ 1 - 2 * x + (1 + s ^ 2) * (1 / (1 + s ^ 2)) * x = 1 - x
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Goal state before:
pp: case inr
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
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
⊢ dist (f d) (f b) ≤ r

Tactic:
have hfdb' : 0 < r / (b - d) := by apply div_pos <;> linarith

Goal state after:
case inr
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
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
⊢ dist (f d) (f b) ≤ r
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2
⊢ √(x ^ 2 + |y| ^ 2) ≤ √(x ^ 2 + (s * x) ^ 2)

Tactic:
;

Goal state after:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2
⊢ √(x ^ 2 + |y| ^ 2) ≤ √(x ^ 2 + (s * x) ^ 2)
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2
⊢ x ^ 2 + (s * x) ^ 2 = (1 + s ^ 2) * x ^ 2

Tactic:
;

Goal state after:
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2
⊢ x ^ 2 + (s * x) ^ 2 = (1 + s ^ 2) * x ^ 2
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
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint fun z ↦ Icc z.1 z.2
hu₃ : HasSum (fun z ↦ (↑z).2 - (↑z).1) (b - d)
g : ↑u → ℝ := fun z ↦ dist (f (↑z).1) (f (↑z).2)
i✝ : ↑u
⊢ 0 i✝ ≤ g i✝

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
hab : a ≤ b
d : ℝ
hd : a ≤ d ∧ d ≤ b
r : ℝ
hr : r > 0
had : a ≤ d
hdb : d < b
hf₀ : ∀ᵐ (x : ℝ), x ∈ Ioo d b → HasDerivAt f 0 x
hfdb' : 0 < r / (b - d)
u : Set (ℝ × ℝ)
hu₁ : ∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) 0 < r / (b - d)
hu₂ : u.PairwiseDisjoint fun z ↦ Icc z.1 z.2
hu₃ : HasSum (fun z ↦ (↑z).2 - (↑z).1) (b - d)
g : ↑u → ℝ := fun z ↦ dist (f (↑z).1) (f (↑z).2)
i✝ : ↑u
⊢ 0 i✝ ≤ g i✝
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ k ≤ n + 1

Tactic:
;

Goal state after:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ k ≤ n + 1
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: case hbc
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2
⊢ 2 * √(1 + s ^ 2) < 2 * √(1 + s ^ 2) + 1

Tactic:
;

Goal state after:
case hbc
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2
⊢ 2 * √(1 + s ^ 2) < 2 * √(1 + s ^ 2) + 1
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: case hbc
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2
⊢ x / 2 ≤ 1 - √((1 - x) ^ 2 + y ^ 2)

Tactic:
;

Goal state after:
case hbc
s x y : ℝ
hx₀ : 0 < x
hx₁ : x < 1 / (1 + s ^ 2)
hy : |y| < s * x
H : √((1 - x) ^ 2 + y ^ 2) ≤ 1 - x / 2
⊢ x / 2 ≤ 1 - √((1 - x) ^ 2 + y ^ 2)
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
vf : ∑ i ∈ Finset.range p.1, dist (f (↑p.2 i)) (f (↑p.2 (i + 1))) < 1
⊢ ∑ x_1 ∈ Finset.range p.1, dist (f (↑p.2 (x_1 + 1))) (f (↑p.2 x_1)) =
    ∑ i ∈ Finset.range p.1, dist (f (↑p.2 i)) (f (↑p.2 (i + 1)))

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
vf : ∑ i ∈ Finset.range p.1, dist (f (↑p.2 i)) (f (↑p.2 (i + 1))) < 1
⊢ ∑ x_1 ∈ Finset.range p.1, dist (f (↑p.2 (x_1 + 1))) (f (↑p.2 x_1)) =
    ∑ i ∈ Finset.range p.1, dist (f (↑p.2 i)) (f (↑p.2 (i + 1)))
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case e_f
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
vf : ∑ i ∈ Finset.range p.1, dist (f (↑p.2 i)) (f (↑p.2 (i + 1))) < 1
⊢ (fun x_1 ↦ dist (f (↑p.2 (x_1 + 1))) (f (↑p.2 x_1))) = fun i ↦ dist (f (↑p.2 i)) (f (↑p.2 (i + 1)))

Tactic:
;

Goal state after:
case e_f
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
vf : ∑ i ∈ Finset.range p.1, dist (f (↑p.2 i)) (f (↑p.2 (i + 1))) < 1
⊢ (fun x_1 ↦ dist (f (↑p.2 (x_1 + 1))) (f (↑p.2 x_1))) = fun i ↦ dist (f (↑p.2 i)) (f (↑p.2 (i + 1)))
Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Goal state before:
pp: case e_f
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
vf : ∑ i ∈ Finset.range p.1, dist (f (↑p.2 i)) (f (↑p.2 (i + 1))) < 1
i : ℕ
⊢ dist (f (↑p.2 (i + 1))) (f (↑p.2 i)) = dist (f (↑p.2 i)) (f (↑p.2 (i + 1)))

Tactic:
;

Goal state after:
case e_f
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
vf : ∑ i ∈ Finset.range p.1, dist (f (↑p.2 i)) (f (↑p.2 (i + 1))) < 1
i : ℕ
⊢ dist (f (↑p.2 (i + 1))) (f (↑p.2 i)) = dist (f (↑p.2 i)) (f (↑p.2 (i + 1)))
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
t : ℝ
ht : t ∈ Ioo (min x₀ x) (max x₀ x)
⊢ k < n + 1

Tactic:
;

Goal state after:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
t : ℝ
ht : t ∈ Ioo (min x₀ x) (max x₀ x)
⊢ k < n + 1
Module: Mathlib.Analysis.Calculus.Taylor

Goal state before:
pp: F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ k + 1 ≤ n + 1

Tactic:
;

Goal state after:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : ℝ → F
x x₀ : ℝ
n : ℕ
hf : ContDiffOn ℝ (↑(n + 1)) f [[x₀, x]]
this✝ : x₀ ≠ x
this : UniqueDiffOn ℝ [[x₀, x]]
k : ℕ
hk : k ≤ n
⊢ k + 1 ≤ n + 1
Module: Mathlib.Analysis.Complex.AbelLimit

Goal state before:
pp: case e_a
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
k :
  Tendsto (fun x ↦ (1 - z) * ∑ x_1 ∈ range x, (∑ i ∈ Ico (x_1 + 1) x, f i) * z ^ x_1) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
n j : ℕ
hj : j ∈ range n
⊢ ∑ i ∈ Ico (j + 1) n, f i = ∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k

Tactic:
;

Goal state after:
case e_a
f : ℕ → ℂ
l : ℂ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
z : ℂ
hz : ‖z‖ < 1
s : ℕ → ℂ := fun n ↦ ∑ i ∈ range n, f i
k :
  Tendsto (fun x ↦ (1 - z) * ∑ x_1 ∈ range x, (∑ i ∈ Ico (x_1 + 1) x, f i) * z ^ x_1) atTop
    (𝓝 (l - ∑' (i : ℕ), f i * z ^ i))
n j : ℕ
hj : j ∈ range n
⊢ ∑ i ∈ Ico (j + 1) n, f i = ∑ k ∈ range n, f k - ∑ k ∈ range (j + 1), f k
Module: Mathlib.Analysis.Normed.Module.Ray

Goal state before:
pp: case inl
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
y : F
⊢ SameRay ℝ 0 y ↔ 0 = 0 ∨ y = 0 ∨ ‖0‖⁻¹ • 0 = ‖y‖⁻¹ • y

pp: case inr
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y

Tactic:
;

Goal state after:
case inl
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
y : F
⊢ SameRay ℝ 0 y ↔ 0 = 0 ∨ y = 0 ∨ ‖0‖⁻¹ • 0 = ‖y‖⁻¹ • y

case inr
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y
Module: Mathlib.Analysis.Normed.Module.Ray

Goal state before:
pp: case inr.inl
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
hx : x ≠ 0
⊢ SameRay ℝ x 0 ↔ x = 0 ∨ 0 = 0 ∨ ‖x‖⁻¹ • x = ‖0‖⁻¹ • 0

pp: case inr.inr
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y

Tactic:
;

Goal state after:
case inr.inl
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
hx : x ≠ 0
⊢ SameRay ℝ x 0 ↔ x = 0 ∨ 0 = 0 ∨ ‖x‖⁻¹ • x = ‖0‖⁻¹ • 0

case inr.inr
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y