mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: case refine_1
x : ℝ
h : 0 < x
⊢ tan (π / 2 - arcsin x) = √(1 - x ^ 2) / x

pp: case refine_2
x : ℝ
h : 0 < x
⊢ -(π / 2) < π / 2 - arcsin x

pp: case refine_3
x : ℝ
h : 0 < x
⊢ π / 2 - arcsin x < π / 2

Tactic:
·

Goal state after:
case refine_1
x : ℝ
h : 0 < x
⊢ tan (π / 2 - arcsin x) = √(1 - x ^ 2) / x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: case refine_2
x : ℝ
h : 0 < x
⊢ -(π / 2) < π / 2 - arcsin x

pp: case refine_3
x : ℝ
h : 0 < x
⊢ π / 2 - arcsin x < π / 2

Tactic:
·

Goal state after:
case refine_2
x : ℝ
h : 0 < x
⊢ -(π / 2) < π / 2 - arcsin x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: case refine_3
x : ℝ
h : 0 < x
⊢ π / 2 - arcsin x < π / 2

Tactic:
·

Goal state after:
case refine_3
x : ℝ
h : 0 < x
⊢ π / 2 - arcsin x < π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: case hx₁
x : ℝ
h : 0 < x
⊢ -(π / 2) < π / 2 - arctan x

pp: case hx₂
x : ℝ
h : 0 < x
⊢ π / 2 - arctan x < π / 2

Tactic:
·

Goal state after:
case hx₁
x : ℝ
h : 0 < x
⊢ -(π / 2) < π / 2 - arctan x
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: case refine_1
𝕜 : 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
y : 𝕜
hyx : x < y
hys : y ∈ s
y' : 𝕜
x✝ : y' ∈ slope f x '' {y | y ∈ s ∧ y < x}
z : 𝕜
hz : z ∈ {y | y ∈ s ∧ y < x}
hz' : slope f x z = y'
⊢ z ∈ s \ {x}

pp: case refine_2
𝕜 : 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
y : 𝕜
hyx : x < y
hys : y ∈ s
y' : 𝕜
x✝ : y' ∈ slope f x '' {y | y ∈ s ∧ y < x}
z : 𝕜
hz : z ∈ {y | y ∈ s ∧ y < x}
hz' : slope f x z = y'
⊢ y ∈ s \ {x}

Tactic:
·

Goal state after:
case refine_1
𝕜 : 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
y : 𝕜
hyx : x < y
hys : y ∈ s
y' : 𝕜
x✝ : y' ∈ slope f x '' {y | y ∈ s ∧ y < x}
z : 𝕜
hz : z ∈ {y | y ∈ s ∧ y < x}
hz' : slope f x z = y'
⊢ z ∈ s \ {x}
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: case hx₂
x : ℝ
h : 0 < x
⊢ π / 2 - arctan x < π / 2

Tactic:
·

Goal state after:
case hx₂
x : ℝ
h : 0 < x
⊢ π / 2 - arctan x < π / 2
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: case refine_2
𝕜 : 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
y : 𝕜
hyx : x < y
hys : y ∈ s
y' : 𝕜
x✝ : y' ∈ slope f x '' {y | y ∈ s ∧ y < x}
z : 𝕜
hz : z ∈ {y | y ∈ s ∧ y < x}
hz' : slope f x z = y'
⊢ y ∈ s \ {x}

Tactic:
·

Goal state after:
case refine_2
𝕜 : 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
y : 𝕜
hyx : x < y
hys : y ∈ s
y' : 𝕜
x✝ : y' ∈ slope f x '' {y | y ∈ s ∧ y < x}
z : 𝕜
hz : z ∈ {y | y ∈ s ∧ y < x}
hz' : slope f x z = y'
⊢ y ∈ s \ {x}
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: case ha
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
bd2 : cos y ^ 2 < 1
⊢ 0 < 1

pp: case hb
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
bd2 : cos y ^ 2 < 1
⊢ 0 < cos y ^ 2

Tactic:
·

Goal state after:
case ha
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
bd2 : cos y ^ 2 < 1
⊢ 0 < 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: case inl
h1 : 0 ≤ 0
h2 : 0 < π / 2
⊢ 0 ≤ tan 0

pp: case inr
x : ℝ
h1 : 0 ≤ x
h2 : x < π / 2
h1' : 0 < x
⊢ x ≤ tan x

Tactic:
·

Goal state after:
case inl
h1 : 0 ≤ 0
h2 : 0 < π / 2
⊢ 0 ≤ tan 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

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

Tactic:
·

Goal state after:
case inr
x : ℝ
h1 : 0 ≤ x
h2 : x < π / 2
h1' : 0 < x
⊢ x ≤ tan x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

Goal state before:
pp: case inl
x y : ℝ
h : x * y < 1
hy : y ≤ 0
⊢ arctan x + arctan y < π / 2

pp: case inr
x y : ℝ
h : x * y < 1
hy : 0 < y
⊢ arctan x + arctan y < π / 2

Tactic:
·

Goal state after:
case inl
x y : ℝ
h : x * y < 1
hy : y ≤ 0
⊢ arctan x + arctan y < π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

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

Tactic:
·

Goal state after:
case inr
x y : ℝ
h : x * y < 1
hy : 0 < y
⊢ arctan x + arctan y < π / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: case inl
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 : 0 < x
⊢ cos x < 1 / √(x ^ 2 + 1)

pp: case inr
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
⊢ cos x < 1 / √(x ^ 2 + 1)

Tactic:
·

Goal state after:
case inl
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 : 0 < x
⊢ cos x < 1 / √(x ^ 2 + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: case inr
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
⊢ cos x < 1 / √(x ^ 2 + 1)

Tactic:
·

Goal state after:
case inr
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
⊢ cos x < 1 / √(x ^ 2 + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

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

pp: case hx₁
x y : ℝ
h : x * y < 1
⊢ -(π / 2) < arctan x + arctan y

pp: case hx₂
x y : ℝ
h : x * y < 1
⊢ arctan x + arctan y < π / 2

Tactic:
·

Goal state after:
x y : ℝ
h : x * y < 1
⊢ arctan (tan (arctan x + arctan y)) = arctan ((x + y) / (1 - x * y))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: case e'_3
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
⊢ cos x = cos (-x)

pp: case e'_4
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
⊢ 1 / √(x ^ 2 + 1) = 1 / √((-x) ^ 2 + 1)

Tactic:
·

Goal state after:
case e'_3
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
⊢ cos x = cos (-x)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

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

pp: case hx₂
x y : ℝ
h : x * y < 1
⊢ arctan x + arctan y < π / 2

Tactic:
·

Goal state after:
case hx₁
x y : ℝ
h : x * y < 1
⊢ -(π / 2) < arctan x + arctan y
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: case e'_4
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
⊢ 1 / √(x ^ 2 + 1) = 1 / √((-x) ^ 2 + 1)

Tactic:
·

Goal state after:
case e'_4
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
⊢ 1 / √(x ^ 2 + 1) = 1 / √((-x) ^ 2 + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan

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

Tactic:
·

Goal state after:
case hx₂
x y : ℝ
h : x * y < 1
⊢ arctan x + arctan y < π / 2
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: case inl
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs hys : x ∈ interior S
hxy : x ≤ x
⊢ (fun x ↦ derivWithin f (Ioi x) x) x ≤ (fun x ↦ derivWithin f (Ioi x) x) x

pp: case inr
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ (fun x ↦ derivWithin f (Ioi x) x) x ≤ (fun x ↦ derivWithin f (Ioi x) x) y

Tactic:
·

Goal state after:
case inl
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs hys : x ∈ interior S
hxy : x ≤ x
⊢ (fun x ↦ derivWithin f (Ioi x) x) x ≤ (fun x ↦ derivWithin f (Ioi x) x) x
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
⊢ cos y < 1 / √(y ^ 2 + 1)

pp: case inr
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
⊢ cos y < 1 / √(y ^ 2 + 1)

Tactic:
·

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
⊢ cos y < 1 / √(y ^ 2 + 1)
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: case inr.refine_1
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ (slope f y '' {y_1 | y_1 ∈ S ∧ y < y_1}).Nonempty

pp: case inr.refine_2
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ ∀ b ∈ slope f y '' {y_1 | y_1 ∈ S ∧ y < y_1}, slope f x y ≤ b

Tactic:
·

Goal state after:
case inr.refine_1
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ (slope f y '' {y_1 | y_1 ∈ S ∧ y < y_1}).Nonempty
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: case inr.refine_2
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ ∀ b ∈ slope f y '' {y_1 | y_1 ∈ S ∧ y < y_1}, slope f x y ≤ b

Tactic:
·

Goal state after:
case inr.refine_2
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ ∀ b ∈ slope f y '' {y_1 | y_1 ∈ S ∧ y < y_1}, slope f x y ≤ b
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: case inl
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs hys : x ∈ interior S
hxy : x ≤ x
⊢ (fun x ↦ derivWithin f (Iio x) x) x ≤ (fun x ↦ derivWithin f (Iio x) x) x

pp: case inr
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ (fun x ↦ derivWithin f (Iio x) x) x ≤ (fun x ↦ derivWithin f (Iio x) x) y

Tactic:
·

Goal state after:
case inl
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs hys : x ∈ interior S
hxy : x ≤ x
⊢ (fun x ↦ derivWithin f (Iio x) x) x ≤ (fun x ↦ derivWithin f (Iio x) x) x
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: case inr.refine_1
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ (slope f x '' {y | y ∈ S ∧ y < x}).Nonempty

pp: case inr.refine_2
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ ∀ b ∈ slope f x '' {y | y ∈ S ∧ y < x}, b ≤ slope f x y

Tactic:
·

Goal state after:
case inr.refine_1
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ (slope f x '' {y | y ∈ S ∧ y < x}).Nonempty
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

Goal state before:
pp: case inr
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
⊢ cos y < 1 / √(y ^ 2 + 1)

Tactic:
·

Goal state after:
case inr
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
⊢ cos y < 1 / √(y ^ 2 + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

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

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

Tactic:
·

Goal state after:
case inl
hx1 : -(3 * π / 2) ≤ 0
hx2 : 0 ≤ 3 * π / 2
⊢ cos 0 ≤ 1 / √(0 ^ 2 + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

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

Tactic:
·

Goal state after:
case inr
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
⊢ cos x ≤ 1 / √(x ^ 2 + 1)
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: case inr.refine_2
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ ∀ b ∈ slope f x '' {y | y ∈ S ∧ y < x}, b ≤ slope f x y

Tactic:
·

Goal state after:
case inr.refine_2
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
x : ℝ
hxs : x ∈ interior S
y : ℝ
hys : y ∈ interior S
hxy✝ : x ≤ y
hxy : x < y
⊢ ∀ b ∈ slope f x '' {y | y ∈ S ∧ y < x}, b ≤ slope f x y
Module: Mathlib.Analysis.Complex.Angle

Goal state before:
pp: case inl
x y : ℂ
⊢ angle (x / 0) y = angle x (y * 0)

pp: case inr
a x y : ℂ
ha : a ≠ 0
⊢ angle (x / a) y = angle x (y * a)

Tactic:
·

Goal state after:
case inl
x y : ℂ
⊢ angle (x / 0) y = angle x (y * 0)
Module: Mathlib.Analysis.Complex.Angle

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

Tactic:
·

Goal state after:
case inr
a x y : ℂ
ha : a ≠ 0
⊢ angle (x / a) y = angle x (y * a)
Module: Mathlib.Analysis.Complex.Arg

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

pp: case inr
x y : ℂ
hx : x ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg

Tactic:
·

Goal state after:
case inl
y : ℂ
⊢ SameRay ℝ 0 y ↔ 0 = 0 ∨ y = 0 ∨ arg 0 = y.arg
Module: Mathlib.Analysis.Complex.Arg

Goal state before:
pp: case inr.inl
x : ℂ
hx : x ≠ 0
⊢ SameRay ℝ x 0 ↔ x = 0 ∨ 0 = 0 ∨ x.arg = arg 0

pp: case inr.inr
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg

Tactic:
·

Goal state after:
case inr.inl
x : ℂ
hx : x ≠ 0
⊢ SameRay ℝ x 0 ↔ x = 0 ∨ 0 = 0 ∨ x.arg = arg 0
Module: Mathlib.Analysis.Complex.Arg

Goal state before:
pp: case pos
x y : ℂ
hx : x = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0

pp: case neg
x y : ℂ
hx : ¬x = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0

Tactic:
·

Goal state after:
case pos
x y : ℂ
hx : x = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0
Module: Mathlib.Analysis.Complex.Arg

Goal state before:
pp: case pos
x y : ℂ
hx : ¬x = 0
hy : y = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0

pp: case neg
x y : ℂ
hx : ¬x = 0
hy : ¬y = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0

Tactic:
·

Goal state after:
case pos
x y : ℂ
hx : ¬x = 0
hy : y = 0
⊢ x = 0 ∨ y = 0 ∨ x.arg = y.arg ↔ ↑(x / y).arg = 0
Module: Mathlib.Analysis.Complex.Angle

Goal state before:
pp: case inr
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‖ ∈ Icc (2 / π * angle x y) (angle x y)

pp: x✝ y✝ x y : ℂ
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h : y = 1
⊢ ‖x - y‖ ∈ Icc (2 / π * angle x y) (angle x y)

Tactic:
·

Goal state after:
case inr
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‖ ∈ Icc (2 / π * angle x y) (angle x y)
Module: Mathlib.Analysis.Convex.Deriv

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

pp: case refine_2
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
⊢ ∀ b ∈ slope f x '' {y | y ∈ S ∧ y < x}, b ≤ sInf (slope f x '' {y | y ∈ S ∧ x < y})

Tactic:
·

Goal state after:
case refine_1
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
⊢ (slope f x '' {y | y ∈ S ∧ y < x}).Nonempty
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: case refine_2.refine_1
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
z : ℝ
hzs : z ∈ S
hzx : z < x
⊢ (slope f x '' {y | y ∈ S ∧ x < y}).Nonempty

pp: case refine_2.refine_2
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
z : ℝ
hzs : z ∈ S
hzx : z < x
⊢ ∀ b ∈ slope f x '' {y | y ∈ S ∧ x < y}, slope f x z ≤ b

Tactic:
·

Goal state after:
case refine_2.refine_1
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hfc : ConvexOn ℝ S f
hxs : x ∈ interior S
a b : ℝ
hxab : x ∈ Ioo a b
habs : Ioo a b ⊆ S
z : ℝ
hzs : z ∈ S
hzx : z < x
⊢ (slope f x '' {y | y ∈ S ∧ x < y}).Nonempty
Module: Mathlib.Analysis.Complex.Angle

Goal state before:
pp: x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ ‖cos ↑θ - 1 + sin ↑θ * I‖ ∈ Icc (2 / π * |θ|) |θ|

pp: x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ θ ∈ Ioc (-π) (-π + 2 * π)

Tactic:
·

Goal state after:
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ ‖cos ↑θ - 1 + sin ↑θ * I‖ ∈ Icc (2 / π * |θ|) |θ|
Module: Mathlib.Analysis.Complex.Angle

Goal state before:
pp: case refine_1
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ (2 / π * |θ|) ^ 2 ≤ (Real.cos θ - 1) ^ 2 + Real.sin θ ^ 2

pp: case refine_2
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ √((Real.cos θ - 1) ^ 2 + Real.sin θ ^ 2) ≤ |θ|

Tactic:
·

Goal state after:
case refine_1
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ (2 / π * |θ|) ^ 2 ≤ (Real.cos θ - 1) ^ 2 + Real.sin θ ^ 2
Module: Mathlib.Analysis.Complex.Angle

Goal state before:
pp: case refine_2
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ √((Real.cos θ - 1) ^ 2 + Real.sin θ ^ 2) ≤ |θ|

Tactic:
·

Goal state after:
case refine_2
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ √((Real.cos θ - 1) ^ 2 + Real.sin θ ^ 2) ≤ |θ|
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
y : V
⊢ √((1 - ⟪0, y⟫ / (‖0‖ * ‖y‖) * (⟪0, y⟫ / (‖0‖ * ‖y‖))) * (‖0‖ * ‖y‖) ^ 2) = √(⟪0, 0⟫ * ⟪y, y⟫ - ⟪0, y⟫ * ⟪0, y⟫)

pp: case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
⊢ √((1 - ⟪x, y⟫ / (‖x‖ * ‖y‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))) * (‖x‖ * ‖y‖) ^ 2) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)

Tactic:
·

Goal state after:
case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
y : V
⊢ √((1 - ⟪0, y⟫ / (‖0‖ * ‖y‖) * (⟪0, y⟫ / (‖0‖ * ‖y‖))) * (‖0‖ * ‖y‖) ^ 2) = √(⟪0, 0⟫ * ⟪y, y⟫ - ⟪0, y⟫ * ⟪0, y⟫)
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: case inl
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx hy : x ∈ S
hxy : x ≤ x
⊢ derivWithin f S x ≤ derivWithin f S x

pp: case inr
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x ≤ y
hxy' : x < y
⊢ derivWithin f S x ≤ derivWithin f S y

Tactic:
·

Goal state after:
case inl
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx hy : x ∈ S
hxy : x ≤ x
⊢ derivWithin f S x ≤ derivWithin f S x
Module: Mathlib.Analysis.Complex.Angle

Goal state before:
pp: x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ θ ∈ Ioc (-π) (-π + 2 * π)

Tactic:
·

Goal state after:
x y : ℂ
hy : ‖1‖ = 1
θ : ℝ
hθ : θ ∈ Ioc (-π) π
⊢ θ ∈ Ioc (-π) (-π + 2 * π)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

Goal state before:
pp: case inr.inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V
hx : x ≠ 0
⊢ √((1 - ⟪x, 0⟫ / (‖x‖ * ‖0‖) * (⟪x, 0⟫ / (‖x‖ * ‖0‖))) * (‖x‖ * ‖0‖) ^ 2) = √(⟪x, x⟫ * ⟪0, 0⟫ - ⟪x, 0⟫ * ⟪x, 0⟫)

pp: case inr.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ √((1 - ⟪x, y⟫ / (‖x‖ * ‖y‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))) * (‖x‖ * ‖y‖) ^ 2) = √(⟪x, x⟫ * ⟪y, y⟫ - ⟪x, y⟫ * ⟪x, y⟫)

Tactic:
·

Goal state after:
case inr.inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V
hx : x ≠ 0
⊢ √((1 - ⟪x, 0⟫ / (‖x‖ * ‖0‖) * (⟪x, 0⟫ / (‖x‖ * ‖0‖))) * (‖x‖ * ‖0‖) ^ 2) = √(⟪x, x⟫ * ⟪0, 0⟫ - ⟪x, 0⟫ * ⟪x, 0⟫)
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: case inl
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
x : ℝ
hx hy : x ∈ S
hxy : x ≤ x
⊢ deriv f x ≤ deriv f x

pp: case inr
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x ≤ y
hxy' : x < y
⊢ deriv f x ≤ deriv f y

Tactic:
·

Goal state after:
case inl
S : Set ℝ
f : ℝ → ℝ
hfc : ConvexOn ℝ S f
hfd : ∀ x ∈ S, DifferentiableAt ℝ f x
x : ℝ
hx hy : x ∈ S
hxy : x ≤ x
⊢ deriv f x ≤ deriv f x
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: case inl
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ y ∈ {x_1 | (fun x_2 ↦ f x ≤ f x_2) x_1}

pp: case inr.inl
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
h_eq : x = y
⊢ y ∈ {x_1 | (fun x_2 ↦ f x ≤ f x_2) x_1}

pp: case inr.inr
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
hyx : y < x
⊢ y ∈ {x_1 | (fun x_2 ↦ f x ≤ f x_2) x_1}

Tactic:
·

Goal state after:
case inl
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ y ∈ {x_1 | (fun x_2 ↦ f x ≤ f x_2) x_1}
Module: Mathlib.Analysis.Convex.Deriv

Goal state before:
pp: case inr.inl
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
h_eq : x = y
⊢ y ∈ {x_1 | (fun x_2 ↦ f x ≤ f x_2) x_1}

pp: case inr.inr
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
hyx : y < x
⊢ y ∈ {x_1 | (fun x_2 ↦ f x ≤ f x_2) x_1}

Tactic:
·

Goal state after:
case inr.inl
S : Set ℝ
f : ℝ → ℝ
x : ℝ
hf : ConvexOn ℝ S f
hx : x ∈ interior S
hf_ld : derivWithin f (Iio x) x ≤ 0
hf_rd : 0 ≤ derivWithin f (Ioi x) x
y : ℝ
hy : y ∈ S
h_eq : x = y
⊢ y ∈ {x_1 | (fun x_2 ↦ f x ≤ f x_2) x_1}