awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
linarith : HPow.hPow (β := ℕ) y 2 + 1 ≤ 0 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁ : HPow.hPow (β := ℕ) y 2 + 1 ≤ 0 → 2 / 2 = 1
linarith₂ : HPow.hPow (β := ℕ) y 2 + 1 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₃ : HPow.hPow (β := ℕ) y 2 + 1 ≤ 0 → GT.gt (α := ℝ) 2 0
linarith₄ : HPow.hPow (β := ℕ) y 2 + 1 ≤ 0 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₅ : HPow.hPow (β := ℕ) y 2 + 1 ≤ 0 → 2 / 2 = 1
linarith₆ : HPow.hPow (β := ℕ) y 2 + 1 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₇ : HPow.hPow (β := ℕ) y 2 + 1 ≤ 0 → GT.gt (α := ℝ) 2 0
linarith₈ : HPow.hPow (β := ℕ) y 2 + 1 ≤ 0 → HMul.hMul (α := ℝ) 1 1 = 1
linarith₉ : HPow.hPow (β := ℕ) y 2 + 1 ≤ 0 → 2 / 2 = 1
linarith₁₀ : HPow.hPow (β := ℕ) y 2 + 1 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₁ : HPow.hPow (β := ℕ) y 2 + 1 ≤ 0 → GT.gt (α := ℝ) 2 0
linarith₁₂ : HPow.hPow (β := ℕ) y 2 + 1 ≤ 0 → -1 + (HPow.hPow (β := ℕ) y 2 + 1 - 0) + (0 - HPow.hPow (β := ℕ) y 2) = 0
⊢ 0 < HPow.hPow (β := ℕ) y 2 + 1

Tactic:
linarith [sq_nonneg y]

Premises used: sq_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
⊢ 0 < HPow.hPow (β := ℕ) y 2 + 1

Tactic:
have hy3 : ↑0 < y ^ 2 + 1 := by linarith [sq_nonneg y]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < HPow.hPow (β := ℕ) y 2 + 1
inl : ∀ (hy2' : y < π / 2), cos y < 1 / √(HPow.hPow (β := ℕ) y 2 + 1)
inr : ∀ (hy1' : π / 2 ≤ y), cos y < 1 / √(HPow.hPow (β := ℕ) y 2 + 1)
⊢ cos y < 1 / √(HPow.hPow (β := ℕ) y 2 + 1)

Tactic:
rcases lt_or_ge y (π / 2) with (hy2' | hy1')

Premises used: Real.pi, HDiv.hDiv, lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < HPow.hPow (β := ℕ) y 2 + 1
hy2' : y < π / 2
linarith : y ≤ -(π / 2) → 2 / 2 = 1
linarith₁ : y ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : y ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₃ : y ≤ -(π / 2) → 2 / 2 = 1
linarith₄ : y ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : y ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₆ : y ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 1 = 1
linarith₇ : y ≤ -(π / 2) → 2 / 2 = 1
linarith₈ : y ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₉ : y ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₁₀ : y ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁₁ : y ≤ -(π / 2) → 2 / 2 = 1
linarith₁₂ : y ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₃ : y ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₁₄ : y ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁₅ : y ≤ -(π / 2) → 2 / 2 = 1
linarith₁₆ : y ≤ -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₇ : y ≤ -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₁₈ : y ≤ -(π / 2) → 4 * (0 - y) + (2 * y - 1 * π) + (2 * y - -(1 * π)) = 0
linarith₁₉ : y ≤ -(π / 2) → GT.gt (α := ℝ) 4 0
⊢ -(π / 2) < y

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < HPow.hPow (β := ℕ) y 2 + 1
hy2' : y < π / 2
⊢ 0 < cos y

Tactic:
have hy4 : 0 < cos y := cos_pos_of_mem_Ioo ⟨by linarith, hy2'⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < HPow.hPow (β := ℕ) y 2 + 1
hy2' : y < π / 2
hy4 : 0 < cos y
linarith : y < -(π / 2) → 2 / 2 = 1
linarith₁ : y < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : y < -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₃ : y < -(π / 2) → 2 / 2 = 1
linarith₄ : y < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : y < -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₆ : y < -(π / 2) → HMul.hMul (α := ℝ) 1 1 = 1
linarith₇ : y < -(π / 2) → 2 / 2 = 1
linarith₈ : y < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₉ : y < -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₁₀ : y < -(π / 2) → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁₁ : y < -(π / 2) → 2 / 2 = 1
linarith₁₂ : y < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₃ : y < -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₁₄ : y < -(π / 2) → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁₅ : y < -(π / 2) → 2 / 2 = 1
linarith₁₆ : y < -(π / 2) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₇ : y < -(π / 2) → GT.gt (α := ℝ) 2 0
linarith₁₈ : y < -(π / 2) → 4 * (0 - y) + (2 * y - 1 * π) + (2 * y - -(1 * π)) = 0
linarith₁₉ : y < -(π / 2) → GT.gt (α := ℝ) 4 0
⊢ -(π / 2) ≤ y

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < HPow.hPow (β := ℕ) y 2 + 1
hy2' : y < π / 2
hy4 : 0 < cos y
inl : y < tan y
⊢ cos y < 1 / √(HPow.hPow (β := ℕ) 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)]

Premises used: Iff.mpr, one_pow, pow_pos, lt_one_div, Real.inv_one_add_tan_sq, Real.cos_nonneg_of_mem_Icc, one_div_nonneg, LT.lt.le, Real.sq_sqrt, add_comm, LT.lt.ne', sq_lt_sq, Real.tan_nonneg_of_nonneg_of_le_pi_div_two, inv_inv, div_pow, And.intro, one_div, abs_of_nonneg, abs_of_pos, Real.sqrt_nonneg, add_lt_add_iff_left
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < HPow.hPow (β := ℕ) y 2 + 1
hy2' : y < π / 2
hy4 : 0 < cos y
⊢ y < tan y

Tactic:
Real.lt_tan hy1 hy2'

Premises used: Real.lt_tan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < HPow.hPow (β := ℕ) y 2 + 1
hy2' : y < π / 2
hy4 : 0 < cos y
⊢ y < tan y

Tactic:
exact Real.lt_tan hy1 hy2'

Premises used: Real.lt_tan
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < HPow.hPow (β := ℕ) y 2 + 1
hy1' : π / 2 ≤ y
⊢ cos y < 1 / √(HPow.hPow (β := ℕ) y 2 + 1)

Tactic:
lt_of_le_of_lt ?_ (one_div_pos.mpr <| sqrt_pos_of_pos hy3)

Premises used: Iff.mpr, lt_of_le_of_lt, Real.sqrt_pos_of_pos, one_div_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < HPow.hPow (β := ℕ) y 2 + 1
hy1' : π / 2 ≤ y
inr : cos y ≤ 0
⊢ cos y < 1 / √(HPow.hPow (β := ℕ) y 2 + 1)

Tactic:
refine lt_of_le_of_lt ?_ (one_div_pos.mpr <| sqrt_pos_of_pos hy3)

Premises used: Iff.mpr, lt_of_le_of_lt, Real.sqrt_pos_of_pos, one_div_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < HPow.hPow (β := ℕ) y 2 + 1
hy1' : π / 2 ≤ y
linarith : π + π / 2 < y → 2 / 2 = 1
linarith₁ : π + π / 2 < y → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : π + π / 2 < y → GT.gt (α := ℝ) 2 0
linarith₃ : π + π / 2 < y → 2 / 2 = 1
linarith₄ : π + π / 2 < y → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : π + π / 2 < y → GT.gt (α := ℝ) 2 0
linarith₆ : π + π / 2 < y → HMul.hMul (α := ℝ) 1 1 = 1
linarith₇ : π + π / 2 < y → 2 / 2 = 1
linarith₈ : π + π / 2 < y → HMul.hMul (α := ℝ) 1 2 = 2
linarith₉ : π + π / 2 < y → GT.gt (α := ℝ) 2 0
linarith₁₀ : π + π / 2 < y → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁₁ : π + π / 2 < y → 2 / 2 = 1
linarith₁₂ : π + π / 2 < y → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₃ : π + π / 2 < y → GT.gt (α := ℝ) 2 0
linarith₁₄ : π + π / 2 < y → HMul.hMul (α := ℝ) 1 1 = 1
linarith₁₅ : π + π / 2 < y → 2 / 2 = 1
linarith₁₆ : π + π / 2 < y → HMul.hMul (α := ℝ) 1 2 = 2
linarith₁₇ : π + π / 2 < y → GT.gt (α := ℝ) 2 0
linarith₁₈ : π + π / 2 < y → 2 * y - HMul.hMul (α := ℝ) 1 3 * (1 * π) + (2 * π + 1 * π - 2 * y) = 0
⊢ y ≤ π + π / 2

Tactic:
linarith [pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
y : ℝ
hy1 : 0 < y
hy2 : y ≤ 3 * π / 2
hy3 : 0 < HPow.hPow (β := ℕ) y 2 + 1
hy1' : π / 2 ≤ y
⊢ cos y ≤ 0

Tactic:
exact cos_nonpos_of_pi_div_two_le_of_le hy1' (by linarith [pi_pos])

Premises used: Real.cos_nonpos_of_pi_div_two_le_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
inl : ∀ (hx1 : -(3 * π / 2) ≤ 0) (hx2 : 0 ≤ 3 * π / 2), cos 0 ≤ 1 / √(HPow.hPow (α := ℝ) (β := ℕ) 0 2 + 1)
inr : ∀ (hx3 : x ≠ 0), cos x ≤ 1 / √(HPow.hPow (β := ℕ) x 2 + 1)
⊢ cos x ≤ 1 / √(HPow.hPow (β := ℕ) x 2 + 1)

Tactic:
rcases eq_or_ne x 0 with (rfl | hx3)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
hx1 : -(3 * π / 2) ≤ 0
hx2 : 0 ≤ 3 * π / 2
⊢ cos 0 ≤ 1 / √(HPow.hPow (α := ℝ) (β := ℕ) 0 2 + 1)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
⊢ cos x ≤ 1 / √(HPow.hPow (β := ℕ) x 2 + 1)

Tactic:
(cos_lt_one_div_sqrt_sq_add_one hx1 hx2 hx3).le

Premises used: LT.lt.le, Real.cos_lt_one_div_sqrt_sq_add_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
⊢ cos x ≤ 1 / √(HPow.hPow (β := ℕ) x 2 + 1)

Tactic:
exact (cos_lt_one_div_sqrt_sq_add_one hx1 hx2 hx3).le

Premises used: LT.lt.le, Real.cos_lt_one_div_sqrt_sq_add_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
⊢ ∀ (x : ℝ), ‖deriv sin x‖₊ ≤ 1

Tactic:
simpa using abs_cos_le_one

Premises used: Real.abs_cos_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
⊢ ∀ (x : ℝ), ‖deriv cos x‖₊ ≤ 1

Tactic:
simpa using abs_sin_le_one

Premises used: Real.abs_sin_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x y : ℝ
⊢ |sin x - sin y| ≤ |x - y|

Tactic:
simpa [edist_dist] using lipschitzWith_sin x y

Premises used: Real.lipschitzWith_sin, edist_dist
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x y : ℝ
⊢ |cos x - cos y| ≤ |x - y|

Tactic:
simpa [edist_dist] using lipschitzWith_cos x y

Premises used: edist_dist, Real.lipschitzWith_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
rw : ‖2 * sin (x / 2)‖ ≤ ‖x‖
⊢ ‖Complex.exp (Complex.I * (↑x : ℂ)) - 1‖ ≤ ‖x‖

Tactic:
rw [Complex.norm_exp_I_mul_ofReal_sub_one]

Premises used: Complex.norm_exp_I_mul_ofReal_sub_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
⊢ ‖2 * sin (x / 2)‖ = 2 * |sin (x / 2)|

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
⊢ 2 * |sin (x / 2)| ≤ 2 * |x / 2|

Tactic:
(mul_le_mul_iff_of_pos_left zero_lt_two).mpr Real.abs_sin_le_abs

Premises used: Iff.mpr, mul_le_mul_iff_of_pos_left, Real.abs_sin_le_abs, zero_lt_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
rw : 2 * (|x| / 2) = |x|
⊢ 2 * |x / 2| = ‖x‖

Tactic:
rw [abs_div, Nat.abs_ofNat, Real.norm_eq_abs]

Premises used: abs_div, Nat.abs_ofNat, Real.norm_eq_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
⊢ 2 * (|x| / 2) = |x|

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
_ : ‖2 * sin (x / 2)‖ = 2 * |sin (x / 2)|
_₁ : 2 * |x / 2| = ‖x‖
⊢ ‖2 * sin (x / 2)‖ ≤ ‖x‖

Tactic:
calc
    _ = 2 * |Real.sin (x / 2)| := by simp
    _ ≤ 2 * |x / 2| := (mul_le_mul_iff_of_pos_left zero_lt_two).mpr Real.abs_sin_le_abs
    _ = _ := by rw [abs_div, Nat.abs_ofNat, Real.norm_eq_abs]; ring

Premises used: Iff.mpr, mul_le_mul_iff_of_pos_left, HDiv.hDiv, Real.abs_sin_le_abs, zero_lt_two, OfNat.ofNat, Real.sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
rw : ENNReal.ofReal ‖Complex.exp (Complex.I * (↑x : ℂ)) - 1‖ ≤ ‖x‖ₑ
⊢ ‖Complex.exp (Complex.I * (↑x : ℂ)) - 1‖ₑ ≤ ‖x‖ₑ

Tactic:
rw [← enorm_norm, Real.enorm_of_nonneg (norm_nonneg _)]

Premises used: Real.enorm_of_nonneg, enorm_norm, norm_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
rw : ENNReal.ofReal ‖Complex.exp (Complex.I * (↑x : ℂ)) - 1‖ ≤ ENNReal.ofReal ‖x‖
⊢ ENNReal.ofReal ‖Complex.exp (Complex.I * (↑x : ℂ)) - 1‖ ≤ ‖x‖ₑ

Tactic:
rw [← enorm_norm, Real.enorm_of_nonneg (norm_nonneg _)]

Premises used: Real.enorm_of_nonneg, enorm_norm, norm_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
iterate : ENNReal.ofReal ‖Complex.exp (Complex.I * (↑x : ℂ)) - 1‖ ≤ ENNReal.ofReal ‖x‖
⊢ ‖Complex.exp (Complex.I * (↑x : ℂ)) - 1‖ₑ ≤ ‖x‖ₑ

Tactic:
iterate 2 rw [← enorm_norm, Real.enorm_of_nonneg (norm_nonneg _)]

Premises used: Real.enorm_of_nonneg, enorm_norm, norm_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
⊢ ENNReal.ofReal ‖Complex.exp (Complex.I * (↑x : ℂ)) - 1‖ ≤ ENNReal.ofReal ‖x‖

Tactic:
ENNReal.ofReal_le_ofReal norm_exp_I_mul_ofReal_sub_one_le

Premises used: Real.norm_exp_I_mul_ofReal_sub_one_le, ENNReal.ofReal_le_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
⊢ ENNReal.ofReal ‖Complex.exp (Complex.I * (↑x : ℂ)) - 1‖ ≤ ENNReal.ofReal ‖x‖

Tactic:
exact ENNReal.ofReal_le_ofReal norm_exp_I_mul_ofReal_sub_one_le

Premises used: Real.norm_exp_I_mul_ofReal_sub_one_le, ENNReal.ofReal_le_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
rw : (↑‖Complex.exp (Complex.I * (↑x : ℂ)) - 1‖₊ : ENNReal) ≤ (↑‖x‖₊ : ENNReal)
⊢ ‖Complex.exp (Complex.I * (↑x : ℂ)) - 1‖₊ ≤ ‖x‖₊

Tactic:
rw [← ENNReal.coe_le_coe]

Premises used: ENNReal.coe_le_coe
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
⊢ (↑‖Complex.exp (Complex.I * (↑x : ℂ)) - 1‖₊ : ENNReal) ≤ (↑‖x‖₊ : ENNReal)

Tactic:
enorm_exp_I_mul_ofReal_sub_one_le

Premises used: Real.enorm_exp_I_mul_ofReal_sub_one_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
⊢ (↑‖Complex.exp (Complex.I * (↑x : ℂ)) - 1‖₊ : ENNReal) ≤ (↑‖x‖₊ : ENNReal)

Tactic:
exact enorm_exp_I_mul_ofReal_sub_one_le

Premises used: Real.enorm_exp_I_mul_ofReal_sub_one_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
⊢ ∀ (x : ℝ) (n : ℤ), (↑(eval x (T ℝ n)) : ℂ) = eval (↑x : ℂ) (T ℂ n)

Tactic:
@algebraMap_eval_T ℝ ℂ _ _ _

Premises used: Polynomial.eval, Polynomial.Chebyshev.algebraMap_eval_T
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
⊢ ∀ (x : ℝ) (n : ℤ), (↑(eval x (U ℝ n)) : ℂ) = eval (↑x : ℂ) (U ℂ n)

Tactic:
@algebraMap_eval_U ℝ ℂ _ _ _

Premises used: Polynomial.eval, Polynomial.Chebyshev.algebraMap_eval_U
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
⊢ ∀ (x : ℝ) (n : ℤ), (↑(eval x (C ℝ n)) : ℂ) = eval (↑x : ℂ) (C ℂ n)

Tactic:
@algebraMap_eval_C ℝ ℂ _ _ _

Premises used: Polynomial.eval, Polynomial.Chebyshev.algebraMap_eval_C
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
⊢ ∀ (x : ℝ) (n : ℤ), (↑(eval x (S ℝ n)) : ℂ) = eval (↑x : ℂ) (S ℂ n)

Tactic:
@algebraMap_eval_S ℝ ℂ _ _ _

Premises used: Polynomial.eval, Polynomial.Chebyshev.algebraMap_eval_S
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
θ : ℂ
⊢ eval (cos θ) (T ℂ 0) = cos ((↑0 : ℂ) * θ)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
θ : ℂ
⊢ eval (cos θ) (T ℂ 1) = cos ((↑1 : ℂ) * θ)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (T ℂ (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = cos ((↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℂ) * θ)
ih2 : eval (cos θ) (T ℂ (↑n : ℤ)) = cos ((↑(↑n : ℤ) : ℂ) * θ)
add_two :
  2 * cos θ * cos ((↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℂ) * θ) =
    2 * cos (((↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : ℂ) * θ + (↑(↑n : ℤ) : ℂ) * θ) / 2) *
      cos (((↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : ℂ) * θ - (↑(↑n : ℤ) : ℂ) * θ) / 2)
⊢ eval (cos θ) (T ℂ (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = cos ((↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : ℂ) * θ)

Tactic:
simp only [T_add_two, eval_sub, eval_mul, eval_X, eval_ofNat, ih1, ih2, sub_eq_iff_eq_add,
      cos_add_cos]

Premises used: Polynomial.eval_X, Polynomial.eval_mul, Complex.cos_add_cos, sub_eq_iff_eq_add, Polynomial.eval_ofNat, Polynomial.Chebyshev.T_add_two, Polynomial.eval_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (T ℂ (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = cos ((↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℂ) * θ)
ih2 : eval (cos θ) (T ℂ (↑n : ℤ)) = cos ((↑(↑n : ℤ) : ℂ) * θ)
add_two :
  2 * cos θ * cos (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ) =
    2 * cos ((HAdd.hAdd (α := ℂ) (↑n : ℂ) 2 * θ + (↑n : ℂ) * θ) / 2) *
      cos ((HAdd.hAdd (α := ℂ) (↑n : ℂ) 2 * θ - (↑n : ℂ) * θ) / 2)
⊢ 2 * cos θ * cos ((↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℂ) * θ) =
    2 * cos (((↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : ℂ) * θ + (↑(↑n : ℤ) : ℂ) * θ) / 2) *
      cos (((↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : ℂ) * θ - (↑(↑n : ℤ) : ℂ) * θ) / 2)

Tactic:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (T ℂ (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = cos ((↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℂ) * θ)
ih2 : eval (cos θ) (T ℂ (↑n : ℤ)) = cos ((↑(↑n : ℤ) : ℂ) * θ)
⊢ 2 * cos θ * cos (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * θ) =
    2 * cos ((HAdd.hAdd (α := ℂ) (↑n : ℂ) 2 * θ + (↑n : ℂ) * θ) / 2) *
      cos ((HAdd.hAdd (α := ℂ) (↑n : ℂ) 2 * θ - (↑n : ℂ) * θ) / 2)

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (T ℂ (-(↑n : ℤ))) = cos ((↑(-(↑n : ℤ)) : ℂ) * θ)
ih2 : eval (cos θ) (T ℂ (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = cos ((↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) * θ)
neg_add_one :
  2 * cos θ * cos ((↑(-(↑n : ℤ)) : ℂ) * θ) =
    2 * cos (((↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) * θ + (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) * θ) / 2) *
      cos (((↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) * θ - (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) * θ) / 2)
⊢ eval (cos θ) (T ℂ (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = cos ((↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) * θ)

Tactic:
simp only [T_sub_one, eval_sub, eval_mul, eval_X, eval_ofNat, ih1, ih2, sub_eq_iff_eq_add',
      cos_add_cos]

Premises used: Polynomial.eval_X, Polynomial.eval_mul, Complex.cos_add_cos, Polynomial.Chebyshev.T_sub_one, Polynomial.eval_ofNat, Polynomial.eval_sub, sub_eq_iff_eq_add'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (T ℂ (-(↑n : ℤ))) = cos ((↑(-(↑n : ℤ)) : ℂ) * θ)
ih2 : eval (cos θ) (T ℂ (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = cos ((↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) * θ)
neg_add_one :
  2 * cos θ * cos (-(↑n : ℂ) * θ) =
    2 * cos ((HAdd.hAdd (α := ℂ) (-(↑n : ℂ)) 1 * θ + HSub.hSub (α := ℂ) (-(↑n : ℂ)) 1 * θ) / 2) *
      cos ((HAdd.hAdd (α := ℂ) (-(↑n : ℂ)) 1 * θ - HSub.hSub (α := ℂ) (-(↑n : ℂ)) 1 * θ) / 2)
⊢ 2 * cos θ * cos ((↑(-(↑n : ℤ)) : ℂ) * θ) =
    2 * cos (((↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) * θ + (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) * θ) / 2) *
      cos (((↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) * θ - (↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) * θ) / 2)

Tactic:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (T ℂ (-(↑n : ℤ))) = cos ((↑(-(↑n : ℤ)) : ℂ) * θ)
ih2 : eval (cos θ) (T ℂ (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = cos ((↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) * θ)
⊢ 2 * cos θ * cos (-(↑n : ℂ) * θ) =
    2 * cos ((HAdd.hAdd (α := ℂ) (-(↑n : ℂ)) 1 * θ + HSub.hSub (α := ℂ) (-(↑n : ℂ)) 1 * θ) / 2) *
      cos ((HAdd.hAdd (α := ℂ) (-(↑n : ℂ)) 1 * θ - HSub.hSub (α := ℂ) (-(↑n : ℂ)) 1 * θ) / 2)

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
θ : ℂ
n : ℤ
zero : eval (cos θ) (T ℂ 0) = cos ((↑0 : ℂ) * θ)
one : eval (cos θ) (T ℂ 1) = cos ((↑1 : ℂ) * θ)
add_two :
  ∀ (n : ℕ)
    (ih1 : eval (cos θ) (T ℂ (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) = cos ((↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℂ) * θ))
    (ih2 : eval (cos θ) (T ℂ (↑n : ℤ)) = cos ((↑(↑n : ℤ) : ℂ) * θ)),
    eval (cos θ) (T ℂ (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) = cos ((↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : ℂ) * θ)
neg_add_one :
  ∀ (n : ℕ) (ih1 : eval (cos θ) (T ℂ (-(↑n : ℤ))) = cos ((↑(-(↑n : ℤ)) : ℂ) * θ))
    (ih2 : eval (cos θ) (T ℂ (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1)) = cos ((↑(HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) * θ)),
    eval (cos θ) (T ℂ (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)) = cos ((↑(HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) : ℂ) * θ)
⊢ eval (cos θ) (T ℂ n) = cos ((↑n : ℂ) * θ)

Tactic:
induction n using Polynomial.Chebyshev.induct with
  | zero => simp
  | one => simp
  | add_two n ih1 ih2 =>
    simp only [T_add_two, eval_sub, eval_mul, eval_X, eval_ofNat, ih1, ih2, sub_eq_iff_eq_add,
      cos_add_cos]
    push_cast
    ring_nf
  | neg_add_one n ih1 ih2 =>
    simp only [T_sub_one, eval_sub, eval_mul, eval_X, eval_ofNat, ih1, ih2, sub_eq_iff_eq_add',
      cos_add_cos]
    push_cast
    ring_nf

Premises used: Polynomial.eval_X, Polynomial.eval_mul, Complex.cos_add_cos, sub_eq_iff_eq_add, Polynomial.Chebyshev.T_sub_one, Polynomial.eval_ofNat, Polynomial.Chebyshev.T_add_two, Polynomial.eval_sub, sub_eq_iff_eq_add'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
θ : ℂ
⊢ eval (cos θ) (U ℂ 0) * sin θ = sin (HAdd.hAdd (α := ℂ) (↑0 : ℂ) 1 * θ)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
θ : ℂ
one : 2 * cos θ * sin θ = 2 * sin θ * cos θ
⊢ eval (cos θ) (U ℂ 1) * sin θ = sin (HAdd.hAdd (α := ℂ) (↑1 : ℂ) 1 * θ)

Tactic:
simp [one_add_one_eq_two, sin_two_mul]

Premises used: Complex.sin_two_mul, one_add_one_eq_two
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
θ : ℂ
⊢ 2 * cos θ * sin θ = 2 * sin θ * cos θ

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
Goal:
θ : ℂ
n : ℕ
ih1 :
  eval (cos θ) (U ℂ (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) * sin θ =
    sin (HAdd.hAdd (α := ℂ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℂ) 1 * θ)
ih2 : eval (cos θ) (U ℂ (↑n : ℤ)) * sin θ = sin (HAdd.hAdd (α := ℂ) (↑(↑n : ℤ) : ℂ) 1 * θ)
add_two :
  2 * (cos θ * sin (HAdd.hAdd (α := ℂ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) : ℂ) 1 * θ)) =
    2 *
      (sin
          ((HAdd.hAdd (α := ℂ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : ℂ) 1 * θ +
              HAdd.hAdd (α := ℂ) (↑(↑n : ℤ) : ℂ) 1 * θ) /
            2) *
        cos
          ((HAdd.hAdd (α := ℂ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : ℂ) 1 * θ -
              HAdd.hAdd (α := ℂ) (↑(↑n : ℤ) : ℂ) 1 * θ) /
            2))
⊢ eval (cos θ) (U ℂ (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2)) * sin θ =
    sin (HAdd.hAdd (α := ℂ) (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) : ℂ) 1 * θ)

Tactic:
simp only [U_add_two, eval_sub, eval_mul, eval_X, eval_ofNat, sub_mul,
      mul_assoc, ih1, ih2, sub_eq_iff_eq_add, sin_add_sin]

Premises used: Polynomial.eval_X, mul_assoc, Polynomial.eval_mul, sub_mul, Polynomial.Chebyshev.U_add_two, sub_eq_iff_eq_add, Complex.sin_add_sin, Polynomial.eval_ofNat, Polynomial.eval_sub