mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ ConcaveOn ℝ D f

Tactic:
by

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

Goal state before:
pp: ⊢ π / 4 ∈ Ioo (-(π / 2)) (π / 2)

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : |x| ≤ π
⊢ cos x ≤ 1 - 2 / π ^ 2 * 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'' : ∀ 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.Bounds

Goal state before:
pp: x : ℝ
hx : 0 < x
f : ℝ → ℝ := fun t ↦ sin t - (t - t ^ 3 / 6)
t : ℝ
⊢ deriv f t = cos t - 1 + t ^ 2 / 2

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : 0 < x
f : ℝ → ℝ := fun t ↦ sin t - (t - t ^ 3 / 6)
hderiv : ∀ (t : ℝ), deriv f t = cos t - 1 + t ^ 2 / 2
⊢ ContinuousOn f (Ici 0)

Tactic:
by

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

Goal state before:
pp: ⊢ arctan √3 = π / 3

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : 0 < x
f : ℝ → ℝ := fun t ↦ sin t - (t - t ^ 3 / 6)
hderiv : ∀ (t : ℝ), deriv f t = cos t - 1 + t ^ 2 / 2
⊢ StrictMonoOn f (Ici 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'' : ∀ 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.Bounds

Goal state before:
pp: x : ℝ
hx : 0 < x
f : ℝ → ℝ := fun t ↦ sin t - (t - t ^ 3 / 6)
hderiv : ∀ (t : ℝ), deriv f t = cos t - 1 + t ^ 2 / 2
hmono : StrictMonoOn f (Ici 0)
⊢ 0 ∈ Ici 0

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ x - x ^ 3 / 6 < sin x

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
⊢ x - x ^ 3 / 6 ≤ sin x

Tactic:
by

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

Goal state before:
pp: ⊢ arctan (√3)⁻¹ = π / 6

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ arctan (-x) = -arctan x

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ arctan (-1) = -(π / 4)

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
hfc : ConcaveOn 𝕜 s f
hx : x ∈ s
⊢ AntitoneOn (slope f x) (s \ {x})

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by
  simpa only [arctan_zero] using arctan_lt_arctan_iff (x := 0)

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

Goal state before:
pp: x : ℝ
⊢ |x - sin x| ≤ |x| ^ 3 / 6

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x : ℝ
h : cos x ≠ 0
⊢ HasDerivAt (fun y ↦ tan y - y) (1 / cos x ^ 2 - 1) x

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
y : ℝ
hy : y ∈ U
⊢ 0 < cos y

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
y : ℝ
hy : y ∈ interior U
⊢ 0 < sin y

Tactic:
by

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

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
⊢ ContinuousOn tan U

Tactic:
by

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

Goal state before:
pp: x : ℝ
h : 0 ≤ x
⊢ arctan x = arccos (√(1 + x ^ 2))⁻¹

Tactic:
by

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

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y ↦ tan y - y) U
y : ℝ
hy : y ∈ interior U
this : 0 < cos y
⊢ cos y ^ 2 < 1

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
hfc : ConvexOn 𝕜 s f
hxs : x ∈ interior s
⊢ BddBelow (slope f x '' {y | y ∈ s ∧ x < y})

Tactic:
by

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

Goal state before:
pp: x : ℝ
h : 0 < x
⊢ arccos x = arctan (√(1 - x ^ 2) / x)

Tactic:
by

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

Goal state before:
pp: x : ℝ
h : 0 < x
⊢ arctan x⁻¹ = π / 2 - arctan x

Tactic:
by

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
x : 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
hfc : ConvexOn 𝕜 s f
hxs : x ∈ interior s
⊢ BddAbove (slope f x '' {y | y ∈ s ∧ y < x})

Tactic:
by

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

Goal state before:
pp: x : ℝ
h : x < 0
⊢ arctan x⁻¹ = -(π / 2) - arctan x

Tactic:
by

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

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y ↦ tan y - y) U
y : ℝ
hy : y ∈ interior U
⊢ 0 < deriv (fun y' ↦ tan y' - y') y

Tactic:
by

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

Goal state before:
pp: x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
lb : -1 * (π / 2) < (2 * ↑k + 1) * (π / 2)
ub : arctan x < π / 2
⊢ 0 < π / 2

Tactic:
by

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
h : Ioo x b ⊆ {y | y ∈ S ∧ x < y}
⊢ (Ioo x b).Nonempty

Tactic:
by

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

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x < π / 2
U : Set ℝ := Ico 0 (π / 2)
intU : interior U = Ioo 0 (π / 2)
half_pi_pos : 0 < π / 2
cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y
sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y
tan_cts_U : ContinuousOn tan U
tan_minus_id_cts : ContinuousOn (fun y ↦ tan y - y) U
deriv_pos : ∀ y ∈ interior U, 0 < deriv (fun y' ↦ tan y' - y') y
mono : StrictMonoOn (fun y ↦ tan y - y) (Ico 0 (π / 2))
⊢ 0 ∈ U

Tactic:
by

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
h : Ioo x b ⊆ {y | y ∈ S ∧ x < y}
h_Ioo : Tendsto (slope f x) (𝓝[>] x) (𝓝 (sInf (slope f x '' Ioo x b)))
this : sInf (slope f x '' Ioo x b) = sInf (slope f x '' {y | y ∈ S ∧ x < y})
⊢ Tendsto (slope f x) (𝓝[>] x) (𝓝 (sInf (slope f x '' {y | y ∈ S ∧ x < y})))

Tactic:
by

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

Goal state before:
pp: x : ℝ
k : ℤ
h : arctan x = (2 * ↑k + 1) * π / 2
lb : -1 < 2 * ↑k + 1
ub : (2 * ↑k + 1) * (π / 2) < 1 * (π / 2)
⊢ 0 < π / 2

Tactic:
by

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

Goal state before:
pp: x : ℝ
h1 : 0 < x
h2 : x < π / 2
⊢ x < tan x

Tactic:
by

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
⊢ HasDerivWithinAt f (sInf (slope f x '' {y | y ∈ S ∧ x < y})) (Ioi x) x

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ ∀ (k : ℤ), arctan x ≠ (2 * ↑k + 1) * π / 2

Tactic:
by

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

Goal state before:
pp: x : ℝ
h1 : 0 ≤ x
h2 : x < π / 2
⊢ x ≤ tan x

Tactic:
by

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
h : Ioo a x ⊆ {y | y ∈ S ∧ y < x}
⊢ (Ioo a x).Nonempty

Tactic:
by

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

Goal state before:
pp: x y : ℝ
h : x * y < 1
⊢ arctan x + arctan y < π / 2

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
this : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / √(y ^ 2 + 1)
h✝ : x < 0
⊢ 0 < -x

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
this : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / √(y ^ 2 + 1)
h✝ : x < 0
⊢ -x ≤ 3 * π / 2

Tactic:
by

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
h : Ioo a x ⊆ {y | y ∈ S ∧ y < x}
h_Ioo : Tendsto (slope f x) (𝓝[<] x) (𝓝 (sSup (slope f x '' Ioo a x)))
this : sSup (slope f x '' Ioo a x) = sSup (slope f x '' {y | y ∈ S ∧ y < x})
⊢ Tendsto (slope f x) (𝓝[<] x) (𝓝 (sSup (slope f x '' {y | y ∈ S ∧ y < x})))

Tactic:
by

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

Goal state before:
pp: x y : ℝ
h : x * y < 1
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y))

Tactic:
by

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

Goal state before:
pp: x y : ℝ
h : 1 < x * y
hx : 0 < x
⊢ 0 < y

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
this : ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / √(y ^ 2 + 1)
⊢ cos x < 1 / √(x ^ 2 + 1)

Tactic:
by

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
⊢ HasDerivWithinAt f (sSup (slope f x '' {y | y ∈ S ∧ y < x})) (Iio x) x

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
⊢ 0 < y ^ 2 + 1

Tactic:
by

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

Goal state before:
pp: x y : ℝ
h : 1 < x * y
hx : 0 < x
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y)) + π

Tactic:
by

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ y ∈ {y | y ∈ S ∧ x < y} ∧ slope f x y = slope f x y

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy2' : y < π / 2
⊢ -(π / 2) < y

Tactic:
by

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

Goal state before:
pp: x y : ℝ
h : 1 < x * y
hx : x < 0
⊢ arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - π

Tactic:
by

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

Goal state before:
pp: x : ℝ
h₁ : -1 < x
h₂ : x < 1
⊢ x * x < 1

Tactic:
by

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

Goal state before:
pp: x : ℝ
h₁ : -1 < x
h₂ : x < 1
⊢ 2 * arctan x = arctan (2 * x / (1 - x ^ 2))

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy2' : y < π / 2
hy4 : 0 < cos y
⊢ -(π / 2) ≤ y

Tactic:
by

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

Goal state before:
pp: x : ℝ
h : 1 < x
⊢ 1 < x * x

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x : ℝ
h : 1 < x
⊢ 2 * arctan x = arctan (2 * x / (1 - x ^ 2)) + π

Tactic:
by

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

Goal state before:
pp: x : ℝ
h : x < -1
⊢ 1 < x * x

Tactic:
by

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

Goal state before:
pp: x : ℝ
h : x < -1
⊢ x < 0

Tactic:
by

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

Goal state before:
pp: x : ℝ
h : x < -1
⊢ 2 * arctan x = arctan (2 * x / (1 - x ^ 2)) - π

Tactic:
by

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
⊢ MonotoneOn (fun x ↦ derivWithin f (Ioi x) x) (interior S)

Tactic:
by

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

Goal state before:
pp: ⊢ arctan 2⁻¹ + arctan 3⁻¹ = π / 4

Tactic:
by

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

Goal state before:
pp: ⊢ 2 * arctan 2⁻¹ - arctan 7⁻¹ = π / 4

Tactic:
by

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

Goal state before:
pp: ⊢ 2 * arctan 3⁻¹ + arctan 7⁻¹ = π / 4

Tactic:
by

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

Goal state before:
pp: ⊢ 4 * arctan 5⁻¹ - arctan 239⁻¹ = π / 4

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ 0 < sin (arctan x) ↔ 0 < x

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ sin (arctan x) < 0 ↔ x < 0

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ sin (arctan 0) = 0

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ 0 ≤ sin (arctan x) ↔ 0 ≤ x

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ sin (arctan x) ≤ 0 ↔ x ≤ 0

Tactic:
by

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

Goal state before:
pp: case inl
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy2' : y < π / 2
hy4 : 0 < cos y
⊢ cos y < 1 / √(y ^ 2 + 1)

Tactic:
rw [← abs_of_nonneg (cos_nonneg_of_mem_Icc ⟨by linarith, hy2'.le⟩), ←
      abs_of_nonneg (one_div_nonneg.mpr (sqrt_nonneg _)), ← sq_lt_sq, div_pow, one_pow,
      sq_sqrt hy3.le, lt_one_div (pow_pos hy4 _) hy3, ← inv_one_add_tan_sq hy4.ne', one_div,
      inv_inv, add_comm, add_lt_add_iff_left, sq_lt_sq, abs_of_pos hy1,
      abs_of_nonneg (tan_nonneg_of_nonneg_of_le_pi_div_two hy1.le hy2'.le)]

Goal state after:
case inl
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy2' : y < π / 2
hy4 : 0 < cos y
⊢ y < tan y
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ x ∈ {y_1 | y_1 ∈ S ∧ y_1 < y} ∧ slope f y x = slope f x y

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < y ^ 2 + 1
hy1' : π / 2 ≤ y
⊢ y ≤ π + π / 2

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
⊢ cos x < 1 / √(x ^ 2 + 1)

Tactic:
by

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

Goal state before:
pp: x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
⊢ cos x ≤ 1 / √(x ^ 2 + 1)

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (x : ℝ), ‖deriv sin x‖₊ ≤ 1

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (x : ℝ), ‖deriv cos x‖₊ ≤ 1

Tactic:
by

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

Goal state before:
pp: x y : ℝ
⊢ |sin x - sin y| ≤ |x - y|

Tactic:
by

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

Goal state before:
pp: x y : ℝ
⊢ |cos x - cos y| ≤ |x - y|

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ ‖2 * sin (x / 2)‖ = 2 * |sin (x / 2)|

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ 2 * |x / 2| = ‖x‖

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ ‖Complex.exp (Complex.I * ↑x) - 1‖ ≤ ‖x‖

Tactic:
by

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

Goal state before:
pp: x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ angle x y = |(x / y).arg|

Tactic:
by

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

Goal state before:
pp: y : ℂ
hy : y ≠ 0
⊢ angle 1 y = |y.arg|

Tactic:
by

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

Goal state before:
pp: x : ℂ
hx : x ≠ 0
⊢ angle x 1 = |x.arg|

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ ‖Complex.exp (Complex.I * ↑x) - 1‖ₑ ≤ ‖x‖ₑ

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ ‖Complex.exp (Complex.I * ↑x) - 1‖₊ ≤ ‖x‖₊

Tactic:
by

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
⊢ MonotoneOn (fun x ↦ derivWithin f (Iio x) x) (interior S)

Tactic:
by

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

Goal state before:
pp: a : ℂ
ha : a ≠ 0
x y : ℂ
⊢ angle (a * x) (a * y) = angle x y

Tactic:
by

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

Goal state before:
pp: a : ℂ
ha : a ≠ 0
x y : ℂ
⊢ angle (x * a) (y * a) = angle x y

Tactic:
by

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

Goal state before:
pp: a x y : ℂ
⊢ angle (x / a) y = angle x (y * a)

Tactic:
by

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

Goal state before:
pp: x y : ℂ
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg

Tactic:
by

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

Goal state before:
pp: a x y : ℂ
⊢ angle x (y / a) = angle (x * a) y

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V × V
hx1 : x.1 ≠ 0
hx2 : x.2 ≠ 0
⊢ ContinuousAt (fun y ↦ angle y.1 y.2) x

Tactic:
by

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

Goal state before:
pp: x y : ℂ
⊢ SameRay ℝ x y ↔ (x / y).arg = 0

Tactic:
by

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

Goal state before:
pp: x y : ℝ
⊢ angle (cexp (↑x * I)) (cexp (↑y * I)) = |toIocMod Real.two_pi_pos (-π) (x - y)|

Tactic:
by

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

Goal state before:
pp: x : ℝ
⊢ angle (cexp (↑x * I)) 1 = |toIocMod Real.two_pi_pos (-π) x|

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
c : ℝ
hc : c ≠ 0
x y : V
⊢ angle (c • x) (c • y) = angle x y

Tactic:
by

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

Goal state before:
pp: x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
this : ∀ {x y : ℂ}, ‖x‖ = 1 → ‖y‖ = 1 → y = 1 → ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)
h : ¬y = 1
⊢ ‖x / y‖ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →ₗᵢ[ℝ] F
u v : E
⊢ angle (f u) (f v) = angle u v

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ angle x y = angle y x

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ angle (-x) (-y) = angle x y

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ angle x (-y) = π - angle x y

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ angle (-x) y = π - angle x y

Tactic:
by

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

Goal state before:
pp: S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
⊢ derivWithin f (Iio x) x ≤ derivWithin f (Ioi x) x

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V
⊢ angle 0 x = π / 2

Tactic:
by

Goal state after: