mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : deriv f a < (f w - f x) / (w - x)
hxa : x < a
haw : a < w
⊢ ∃ b ∈ Ioo w y, deriv f b < (f y - f w) / (y - w)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: n : ℕ
a b : ℂ
⊢ ∑ x ∈ Finset.range n, (cos (a * (↑(x + 1) - 1 / 2) + b) - cos (-(a * (↑x - 1 / 2) + b))) =
    -2 * sin (↑n * a / 2) * sin ((↑n - 1) * a / 2 + b)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: n : ℕ
a b : ℂ
⊢ sin (a / 2) * ∑ i ∈ Finset.range n, sin (a * ↑i + b) = sin (↑n * a / 2) * sin ((↑n - 1) * a / 2 + b)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: n : ℕ
a : ℂ
h : ∀ (k : ℤ), a ≠ ↑k * (2 * ↑π)
b : ℂ
⊢ ∑ i ∈ Finset.range n, sin (a * ↑i + b) = sin (↑n * a / 2) * sin ((↑n - 1) * a / 2 + b) / sin (a / 2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: n : ℕ
a b : ℂ
⊢ ∑ i ∈ Finset.range n, 2 * sin (a / 2) * cos (a * ↑i + b) =
    ∑ x ∈ Finset.range n, (sin (a * (↑(x + 1) - 1 / 2) + b) - sin (a * (↑x - 1 / 2) + b))

Tactic:
by

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

Goal state before:
pp: E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : ℂ → E := ⇑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
⊢ 0 ∈ e ⁻¹' U

Tactic:
by

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

Goal state before:
pp: f : ℕ → ℝ
l : ℝ
h : Tendsto (fun n ↦ ∑ i ∈ range n, f i) atTop (𝓝 l)
⊢ Tendsto (fun x ↦ ∑' (n : ℕ), f n * x ^ n) (𝓝[<] 1) (𝓝 l)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
hxa : x < a
haw : a < w
b : ℝ
hwb : w < b
hby : b < y
ha : deriv f a * (w - x) < f w - f x
hb : deriv f b * (y - w) < f y - f w
⊢ deriv f a * (y - w) < deriv f b * (y - w)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: n : ℕ
a b : ℂ
⊢ ∑ x ∈ Finset.range n, (sin (a * (↑(x + 1) - 1 / 2) + b) - sin (a * (↑x - 1 / 2) + b)) =
    2 * sin (↑n * a / 2) * cos ((↑n - 1) * a / 2 + b)

Tactic:
by

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

Goal state before:
pp: E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ U
w : E
hne : w ≠ z
e : ℂ → E := ⇑(lineMap z w)
hde : Differentiable ℂ e
hL : AntilipschitzWith (nndist z w)⁻¹ e
hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)
h₀ : 0 ∈ e ⁻¹' U
ζ : ℂ
hζU : ζ ∈ frontier (e ⁻¹' U)
hζ : IsMaxOn (norm ∘ f ∘ e) (closure (e ⁻¹' U)) ζ
⊢ ‖f z‖ = ‖f (e 0)‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: n : ℕ
a b : ℂ
⊢ sin (a / 2) * ∑ i ∈ Finset.range n, cos (a * ↑i + b) = sin (↑n * a / 2) * cos ((↑n - 1) * a / 2 + b)

Tactic:
by

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

Goal state before:
pp: E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f : E → F
U : Set E
hU : Bornology.IsBounded U
hd : DiffContOnCl ℂ f U
C : ℝ
hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C
z : E
hz : z ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
⊢ ‖f z‖ ≤ C

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
⊢ ∃ a ∈ Ioo x y, deriv f a < (f y - f x) / (y - x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: n : ℕ
a : ℂ
h : ∀ (k : ℤ), a ≠ ↑k * (2 * ↑π)
b : ℂ
⊢ ∑ i ∈ Finset.range n, cos (a * ↑i + b) = sin (↑n * a / 2) * cos ((↑n - 1) * a / 2 + b) / sin (a / 2)

Tactic:
by

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

Goal state before:
pp: E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f g : E → F
U : Set E
hU : Bornology.IsBounded U
hf : DiffContOnCl ℂ f U
hg : DiffContOnCl ℂ g U
hfg : EqOn f g (frontier U)
H : ∀ z ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U, ‖(f - g) z‖ ≤ 0
⊢ EqOn f g (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * π / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * π / 2) ∧ ∃ l, y = (2 * ↑l + 1) * π / 2
⊢ ((∀ (k : ℤ), ↑x ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), ↑y ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, ↑x = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, ↑y = (2 * ↑l + 1) * ↑π / 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * π / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * π / 2) ∧ ∃ l, y = (2 * ↑l + 1) * π / 2
⊢ tan (x + y) = (tan x + tan y) / (1 - tan x * tan y)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x : ℝ
n : ℤ
h : ↑n * (2 * π) = x
⊢ ↑(2 * n) * π = x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x : ℝ
n : ℤ
h : π + ↑n * (2 * π) = x
⊢ ↑(1 + n * 2) * π = x

Tactic:
by

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

Goal state before:
pp: E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : Nontrivial E
f g : E → F
U : Set E
hU : Bornology.IsBounded U
hf : DiffContOnCl ℂ f U
hg : DiffContOnCl ℂ g U
hfg : EqOn f g (frontier U)
⊢ EqOn f g (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x : ℝ
n : ℤ
h : ↑(n + n) * π = x
⊢ ↑n * (2 * π) = x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x : ℝ
n : ℤ
h : ↑(2 * n + 1) * π = x
⊢ π + ↑n * (2 * π) = x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv

Goal state before:
pp: x : ℂ
h : cos x ≠ 0
⊢ HasStrictDerivAt tan (1 / cos x ^ 2) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv

Goal state before:
pp: x : ℂ
hx : cos x = 0
h : sin x = 0
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv

Goal state before:
pp: x : ℂ
hx : cos x = 0
⊢ Tendsto (fun x ↦ ‖tan x‖) (𝓝[≠] x) atTop

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv

Goal state before:
pp: x : ℂ
⊢ ContinuousAt tan x ↔ cos x ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x : ℝ
⊢ |cos x| = 1 ↔ ∃ k, ↑k * π = x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv

Goal state before:
pp: x : ℂ
h : cos x = 0
⊢ deriv tan x = 1 / cos x ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : StrictMonoOn (deriv f) (interior D)
x y z : ℝ
hx : x ∈ D
hz : z ∈ D
hxy : x < y
hyz : y < z
⊢ (f y - f x) / (y - x) < (f z - f y) / (z - y)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
h_anti : StrictAntiOn (deriv f) (interior D)
⊢ StrictMonoOn (deriv (-f)) (interior D)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv

Goal state before:
pp: x : ℝ
h : cos x ≠ 0
⊢ Complex.cos ↑x ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv

Goal state before:
pp: x : ℝ
hx : cos x = 0
⊢ Tendsto (fun x ↦ |tan x|) (𝓝[≠] x) atTop

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv

Goal state before:
pp: x : ℝ
⊢ ContinuousAt tan x ↔ cos x ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv

Goal state before:
pp: x : ℝ
h : cos x = 0
⊢ deriv tan x = 1 / cos x ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * π / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * π / 2) ∧ ∃ l, y = (2 * ↑l + 1) * π / 2
⊢ tan (x - y) = (tan x - tan y) / (1 + tan x * tan y)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'' : DifferentiableOn ℝ (deriv f) (interior D)
hf''_nonneg : ∀ x ∈ interior D, 0 ≤ deriv^[2] f x
⊢ DifferentiableOn ℝ (deriv f) (interior (interior D))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv

Goal state before:
pp: x : ℝ
A : cos (arctan x) ≠ 0
⊢ 1 / cos (↑tanPartialHomeomorph.symm x) ^ 2 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
⊢ tan (2 * x) = 2 * tan x / (1 - tan x ^ 2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: n : ℤ
⊢ ∃ k, ↑k * π / 2 = ↑n * π / 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv

Goal state before:
pp: x : ℝ
⊢ HasStrictDerivAt arctan (1 / (1 + x ^ 2)) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x : ℝ
n : ℤ
h : π / 2 + ↑n * (2 * π) = x
⊢ π / 2 + ↑(2 * n) * π = x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv

Goal state before:
pp: n : WithTop ℕ∞
x : ℝ
this : cos (arctan x) ≠ 0
⊢ 1 / cos (↑tanPartialHomeomorph.symm x) ^ 2 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: this : ContinuousOn (fun x ↦ sin x / cos x) {x | cos x ≠ 0}
⊢ (fun x ↦ sin x / cos x) = tan

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'' : DifferentiableOn ℝ (deriv f) (interior D)
hf''_nonneg : ∀ x ∈ interior D, 0 ≤ deriv^[2] f x
⊢ ∀ x ∈ interior (interior D), 0 ≤ deriv (deriv f) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x : ℝ
n : ℤ
h : -(π / 2) + ↑n * (2 * π) = x
⊢ π / 2 + ↑(-1 + n * 2) * π = x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: this : ContinuousOn (fun x ↦ sin x / cos x) {x | cos x ≠ 0}
⊢ ContinuousOn tan {x | cos x ≠ 0}

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: ⊢ ContinuousOn tan {x | cos x ≠ 0}

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'' : DifferentiableOn ℝ (deriv f) (interior D)
hf''_nonpos : ∀ x ∈ interior D, deriv^[2] f x ≤ 0
⊢ DifferentiableOn ℝ (deriv f) (interior (interior D))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x : ℝ
n : ℤ
h : π / 2 + ↑(n + n) * π = x
⊢ π / 2 + ↑n * (2 * π) = x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x : ℝ
n : ℤ
h : π / 2 + ↑(2 * n + 1) * π = x
⊢ -(π / 2) + ↑(n + 1) * (2 * π) = x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'' : DifferentiableOn ℝ (deriv f) (interior D)
hf''_nonpos : ∀ x ∈ interior D, deriv^[2] f x ≤ 0
⊢ ∀ x ∈ interior (interior D), deriv (deriv f) x ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: x : ℝ
⊢ |sin x| = 1 ↔ ∃ k, π / 2 + ↑k * π = x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: θ : ℝ
hθ : cos θ ≠ 0
⊢ tan θ = 0 ↔ ∃ k, ↑k * π = θ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: n : ℕ
a b : ℝ
⊢ sin (a / 2) * ∑ i ∈ range n, sin (a * ↑i + b) = sin (↑n * a / 2) * sin ((↑n - 1) * a / 2 + b)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: n : ℕ
a : ℝ
h : ∀ (k : ℤ), a ≠ ↑k * (2 * π)
b : ℝ
⊢ ∀ (k : ℤ), ↑a ≠ ↑k * (2 * ↑π)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: n : ℕ
a : ℝ
h : ∀ (k : ℤ), a ≠ ↑k * (2 * π)
b : ℝ
⊢ ∑ i ∈ range n, sin (a * ↑i + b) = sin (↑n * a / 2) * sin ((↑n - 1) * a / 2 + b) / sin (a / 2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: n : ℕ
a b : ℝ
⊢ sin (a / 2) * ∑ i ∈ range n, cos (a * ↑i + b) = sin (↑n * a / 2) * cos ((↑n - 1) * a / 2 + b)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex

Goal state before:
pp: n : ℕ
a : ℝ
h : ∀ (k : ℤ), a ≠ ↑k * (2 * π)
b : ℝ
⊢ ∑ i ∈ range n, cos (a * ↑i + b) = sin (↑n * a / 2) * cos ((↑n - 1) * a / 2 + b) / sin (a / 2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 5 / 100
⊢ 100⁻¹ < 6⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
hx_gt : ¬x ≤ -(π / 2)
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
⊢ r ≤ -1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 5 / 100
⊢ 0 ≤ 100⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
h : 0 < x
⊢ sin x < x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ sin x ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx : x < 0
⊢ x < sin x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx : x ≤ 0
⊢ x ≤ sin x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx : 0 < x
hx' : x < 1
⊢ x < sin (π / 2 * x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
hx' : x ≤ 1
⊢ x ≤ sin (π / 2 * x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx : 0 < x
hx' : x < π / 2
⊢ (π / 2)⁻¹ * x < 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx : 0 < x
hx' : x < π / 2
⊢ 2 / π * x < sin x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, 0 ≤ f'' x
this : EqOn (deriv f) f' (interior D)
x : ℝ
hx : x ∈ interior D
y : ℝ
hy : y ∈ interior D
⊢ deriv f y = f' y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
hx' : x ≤ π / 2
⊢ (π / 2)⁻¹ * x ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, 0 ≤ f'' x
⊢ ConvexOn ℝ D f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
hx' : x ≤ π / 2
⊢ 2 / π * x ≤ sin x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: ⊢ ContinuousOn tan (Ioo (-(π / 2)) (π / 2))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx : -(π / 2) ≤ x
hx₀ : x ≤ 0
⊢ sin x ≤ 2 / π * x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: this : -(π / 2) < π / 2
⊢ Tendsto (fun x ↦ tan ↑x) atBot atBot

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: this : -(π / 2) < π / 2
⊢ Tendsto (fun x ↦ tan ↑x) atTop atTop

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
⊢ sin (arctan x) ^ 2 = x ^ 2 / (1 + x ^ 2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx : |x| ≤ π / 2
this : ∀ {x : ℝ}, |x| ≤ π / 2 → 0 ≤ x → 2 / π * |x| ≤ |sin x|
hx₀ : ¬0 ≤ x
⊢ |(-x)| ≤ π / 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
⊢ cos (arctan x) ^ 2 = 1 / (1 + x ^ 2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
⊢ sin (arctan x) = x / √(1 + x ^ 2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
⊢ cos (arctan x) = 1 / √(1 + x ^ 2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx : |x| ≤ π / 2
⊢ 2 / π * |x| ≤ |sin x|

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x✝ x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
hxπ : x ≤ 1
⊢ x ≤ π

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x✝ x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
hxπ : x ≤ 1
⊢ 2 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x✝ x : ℝ
hx : x ≠ 0
hx₀ : 0 < x
hxπ : 1 < x
⊢ 1 < x ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ sin x ^ 2 < x ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
⊢ sin x ^ 2 ≤ x ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ x / 2 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ 1 - x ^ 2 / 2 < cos x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
⊢ 1 - x ^ 2 / 2 ≤ cos x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx₀ : 0 ≤ x
hx : x ≤ π / 2
⊢ 0 ≤ π / 2 - x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx₀ : 0 ≤ x
hx : x ≤ π / 2
⊢ π / 2 - x ≤ π / 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx₀ : 0 ≤ x
hx : x ≤ π / 2
⊢ 1 - 2 / π * x ≤ cos x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx₀ : -(π / 2) ≤ x
hx : x ≤ 0
⊢ 0 ≤ -x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx₀ : -(π / 2) ≤ x
hx : x ≤ 0
⊢ -x ≤ π / 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx₀ : -(π / 2) ≤ x
hx : x ≤ 0
⊢ 1 + 2 / π * x ≤ cos x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x : ℝ
hx : |x| ≤ π
this : ∀ {x : ℝ}, |x| ≤ π → 0 ≤ x → cos x ≤ 1 - 2 / π ^ 2 * x ^ 2
hx₀ : ¬0 ≤ x
⊢ |(-x)| ≤ π

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
h : x ∈ Ioo (-1) 1
⊢ arcsin x = arctan (x / √(1 - x ^ 2))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f f' f'' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x
hf''₀ : ∀ x ∈ interior D, f'' x ≤ 0
this : EqOn (deriv f) f' (interior D)
x : ℝ
hx : x ∈ interior D
y : ℝ
hy : y ∈ interior D
⊢ deriv f y = f' y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: ⊢ arctan 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x✝ x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
⊢ 0 ≤ x / 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x : ℝ
⊢ arctan x = 0 ↔ arctan x = arctan 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: ⊢ Order.IsSuccPrelimit (π / 2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x✝ x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
⊢ x / 2 ≤ π / 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: ⊢ Order.IsPredPrelimit (-(π / 2))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x✝ x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
⊢ x / π ≤ sin (x / 2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: x✝ x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
this : x / π ≤ sin (x / 2)
⊢ 0 ≤ x / π

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: x y : ℝ
h : tan x = y
hx : x ∈ Ioo (-(π / 2)) (π / 2)
⊢ tan (arctan y) = tan x

Tactic:
by

Goal state after: