awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
⊢ cos (x - 2 * (↑π : ℂ)) = cos x

Tactic:
cos_periodic.sub_eq x

Premises used: Complex.cos_periodic, Function.Periodic.sub_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
⊢ cos ((↑π : ℂ) - x) = -cos x

Tactic:
cos_neg x ▸ cos_antiperiodic.sub_eq'

Premises used: Complex.cos_antiperiodic, Eq.rec, Function.Antiperiodic.sub_eq', Complex.cos_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
⊢ cos (2 * (↑π : ℂ) - x) = cos x

Tactic:
cos_neg x ▸ cos_periodic.sub_eq'

Premises used: Eq.rec, Complex.cos_periodic, Function.Periodic.sub_eq', Complex.cos_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
⊢ cos ((↑n : ℂ) * (2 * (↑π : ℂ))) = 1

Tactic:
(cos_periodic.nat_mul_eq n).trans cos_zero

Premises used: Function.Periodic.nat_mul_eq, Complex.cos_periodic, Complex.cos_zero, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℤ
⊢ cos ((↑n : ℂ) * (2 * (↑π : ℂ))) = 1

Tactic:
(cos_periodic.int_mul_eq n).trans cos_zero

Premises used: Complex.cos_periodic, Complex.cos_zero, Function.Periodic.int_mul_eq, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
n : ℕ
⊢ cos (x + (↑n : ℂ) * (2 * (↑π : ℂ))) = cos x

Tactic:
cos_periodic.nat_mul n x

Premises used: Function.Periodic.nat_mul, Complex.cos_periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
n : ℤ
⊢ cos (x + (↑n : ℂ) * (2 * (↑π : ℂ))) = cos x

Tactic:
cos_periodic.int_mul n x

Premises used: Function.Periodic.int_mul, Complex.cos_periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
n : ℕ
⊢ cos (x - (↑n : ℂ) * (2 * (↑π : ℂ))) = cos x

Tactic:
cos_periodic.sub_nat_mul_eq n

Premises used: Complex.cos_periodic, Function.Periodic.sub_nat_mul_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
n : ℤ
⊢ cos (x - (↑n : ℂ) * (2 * (↑π : ℂ))) = cos x

Tactic:
cos_periodic.sub_int_mul_eq n

Premises used: Function.Periodic.sub_int_mul_eq, Complex.cos_periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
n : ℕ
⊢ cos ((↑n : ℂ) * (2 * (↑π : ℂ)) - x) = cos x

Tactic:
cos_neg x ▸ cos_periodic.nat_mul_sub_eq n

Premises used: Eq.rec, Function.Periodic.nat_mul_sub_eq, Complex.cos_periodic, Complex.cos_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
n : ℤ
⊢ cos ((↑n : ℂ) * (2 * (↑π : ℂ)) - x) = cos x

Tactic:
cos_neg x ▸ cos_periodic.int_mul_sub_eq n

Premises used: Eq.rec, Complex.cos_periodic, Complex.cos_neg, Function.Periodic.int_mul_sub_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
⊢ cos ((↑n : ℂ) * (2 * (↑π : ℂ)) + (↑π : ℂ)) = -1

Tactic:
simpa only [cos_zero] using (cos_periodic.nat_mul n).add_antiperiod_eq cos_antiperiodic

Premises used: Complex.cos_antiperiodic, Function.Periodic.nat_mul, Complex.cos_periodic, Complex.cos_zero, Function.Periodic.add_antiperiod_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℤ
⊢ cos ((↑n : ℂ) * (2 * (↑π : ℂ)) + (↑π : ℂ)) = -1

Tactic:
simpa only [cos_zero] using (cos_periodic.int_mul n).add_antiperiod_eq cos_antiperiodic

Premises used: Function.Periodic.int_mul, Complex.cos_antiperiodic, Complex.cos_periodic, Complex.cos_zero, Function.Periodic.add_antiperiod_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
⊢ cos ((↑n : ℂ) * (2 * (↑π : ℂ)) - (↑π : ℂ)) = -1

Tactic:
simpa only [cos_zero] using (cos_periodic.nat_mul n).sub_antiperiod_eq cos_antiperiodic

Premises used: Complex.cos_antiperiodic, Function.Periodic.nat_mul, Complex.cos_periodic, Function.Periodic.sub_antiperiod_eq, Complex.cos_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℤ
⊢ cos ((↑n : ℂ) * (2 * (↑π : ℂ)) - (↑π : ℂ)) = -1

Tactic:
simpa only [cos_zero] using (cos_periodic.int_mul n).sub_antiperiod_eq cos_antiperiodic

Premises used: Function.Periodic.int_mul, Complex.cos_antiperiodic, Complex.cos_periodic, Function.Periodic.sub_antiperiod_eq, Complex.cos_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
⊢ sin (x + (↑π : ℂ) / 2) = cos x

Tactic:
simp [sin_add]

Premises used: Complex.sin_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
⊢ sin (x - (↑π : ℂ) / 2) = -cos x

Tactic:
simp [sub_eq_add_neg, sin_add]

Premises used: sub_eq_add_neg, Complex.sin_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
⊢ sin ((↑π : ℂ) / 2 - x) = cos x

Tactic:
simp [sub_eq_add_neg, sin_add]

Premises used: sub_eq_add_neg, Complex.sin_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
⊢ cos (x + (↑π : ℂ) / 2) = -sin x

Tactic:
simp [cos_add]

Premises used: Complex.cos_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
⊢ cos (x - (↑π : ℂ) / 2) = sin x

Tactic:
simp [sub_eq_add_neg, cos_add]

Premises used: sub_eq_add_neg, Complex.cos_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
rw : cos (-((↑π : ℂ) / 2 - x)) = sin x
rw₁ : cos (x - (↑π : ℂ) / 2) = sin x
rw₂ rw₃ : sin x = sin x
⊢ cos ((↑π : ℂ) / 2 - x) = sin x

Tactic:
rw [← cos_neg, neg_sub, cos_sub_pi_div_two]

Premises used: neg_sub, Complex.cos_sub_pi_div_two, Complex.cos_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Function.Periodic tan (↑π : ℂ)

Tactic:
simpa only [tan_eq_sin_div_cos] using sin_antiperiodic.div cos_antiperiodic

Premises used: Function.Antiperiodic.div, Complex.cos_antiperiodic, Complex.sin_antiperiodic, Complex.tan_eq_sin_div_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
⊢ tan (x + (↑π : ℂ)) = tan x

Tactic:
tan_periodic x

Premises used: Complex.tan_periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
⊢ tan (x - (↑π : ℂ)) = tan x

Tactic:
tan_periodic.sub_eq x

Premises used: Complex.tan_periodic, Function.Periodic.sub_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
⊢ tan ((↑π : ℂ) - x) = -tan x

Tactic:
tan_neg x ▸ tan_periodic.sub_eq'

Premises used: Complex.tan_neg, Eq.rec, Function.Periodic.sub_eq', Complex.tan_periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
rw : sin ((↑π : ℂ) / 2 - x) / cos ((↑π : ℂ) / 2 - x) = (tan x)⁻¹
rw₁ : sin ((↑π : ℂ) / 2 - x) / cos ((↑π : ℂ) / 2 - x) = (sin x / cos x)⁻¹
rw₂ : sin ((↑π : ℂ) / 2 - x) / cos ((↑π : ℂ) / 2 - x) = cos x / sin x
rw₃ : cos x / cos ((↑π : ℂ) / 2 - x) = cos x / sin x
rw₄ rw₅ : cos x / sin x = cos x / sin x
⊢ tan ((↑π : ℂ) / 2 - x) = (tan x)⁻¹

Tactic:
rw [tan_eq_sin_div_cos, tan_eq_sin_div_cos, inv_div, sin_pi_div_two_sub, cos_pi_div_two_sub]

Premises used: Complex.sin_pi_div_two_sub, Complex.tan_eq_sin_div_cos, Complex.cos_pi_div_two_sub, inv_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
⊢ tan ((↑n : ℂ) * (↑π : ℂ)) = 0

Tactic:
tan_zero ▸ tan_periodic.nat_mul_eq n

Premises used: Eq.rec, Function.Periodic.nat_mul_eq, Complex.tan_zero, Complex.tan_periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℤ
⊢ tan ((↑n : ℂ) * (↑π : ℂ)) = 0

Tactic:
tan_zero ▸ tan_periodic.int_mul_eq n

Premises used: Eq.rec, Complex.tan_zero, Function.Periodic.int_mul_eq, Complex.tan_periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
n : ℕ
⊢ tan (x + (↑n : ℂ) * (↑π : ℂ)) = tan x

Tactic:
tan_periodic.nat_mul n x

Premises used: Function.Periodic.nat_mul, Complex.tan_periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
n : ℤ
⊢ tan (x + (↑n : ℂ) * (↑π : ℂ)) = tan x

Tactic:
tan_periodic.int_mul n x

Premises used: Function.Periodic.int_mul, Complex.tan_periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
n : ℕ
⊢ tan (x - (↑n : ℂ) * (↑π : ℂ)) = tan x

Tactic:
tan_periodic.sub_nat_mul_eq n

Premises used: Function.Periodic.sub_nat_mul_eq, Complex.tan_periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
n : ℤ
⊢ tan (x - (↑n : ℂ) * (↑π : ℂ)) = tan x

Tactic:
tan_periodic.sub_int_mul_eq n

Premises used: Function.Periodic.sub_int_mul_eq, Complex.tan_periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
n : ℕ
⊢ tan ((↑n : ℂ) * (↑π : ℂ) - x) = -tan x

Tactic:
tan_neg x ▸ tan_periodic.nat_mul_sub_eq n

Premises used: Complex.tan_neg, Eq.rec, Function.Periodic.nat_mul_sub_eq, Complex.tan_periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
x : ℂ
n : ℤ
⊢ tan ((↑n : ℂ) * (↑π : ℂ) - x) = -tan x

Tactic:
tan_neg x ▸ tan_periodic.int_mul_sub_eq n

Premises used: Complex.tan_neg, Eq.rec, Complex.tan_periodic, Function.Periodic.int_mul_sub_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Function.Antiperiodic cexp ((↑π : ℂ) * I)

Tactic:
simp [exp_add, exp_mul_I]

Premises used: Complex.exp_add, Complex.exp_mul_I
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Function.Periodic cexp (2 * (↑π : ℂ) * I)

Tactic:
(mul_assoc (2 : ℂ) π I).symm ▸ exp_antiperiodic.periodic_two_mul

Premises used: Function.Antiperiodic.periodic_two_mul, Real.pi, Complex.exp_antiperiodic, mul_assoc, Eq.rec, Complex.ofReal, OfNat.ofNat, Eq.symm, Complex.I
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Function.Antiperiodic (β := ℂ) (fun (x : ℂ) ↦ cexp (x * I)) (↑π : ℂ)

Tactic:
simpa only [mul_inv_cancel_right₀ I_ne_zero] using exp_antiperiodic.mul_const I_ne_zero

Premises used: Complex.exp_antiperiodic, Complex.I_ne_zero, mul_inv_cancel_right₀, Function.Antiperiodic.mul_const
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Function.Periodic (β := ℂ) (fun (x : ℂ) ↦ cexp (x * I)) (2 * (↑π : ℂ))

Tactic:
exp_mul_I_antiperiodic.periodic_two_mul

Premises used: Function.Antiperiodic.periodic_two_mul, Complex.exp_mul_I_antiperiodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ cexp ((↑π : ℂ) * I) = -1

Tactic:
exp_zero ▸ exp_antiperiodic.eq

Premises used: Function.Antiperiodic.eq, Complex.exp_zero, Complex.exp_antiperiodic, Eq.rec
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ cexp (-((↑π : ℂ) * I)) = -1

Tactic:
simp [Complex.exp_neg]

Premises used: Complex.exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ cexp (2 * (↑π : ℂ) * I) = 1

Tactic:
exp_periodic.eq.trans exp_zero

Premises used: Complex.exp_zero, Complex.exp_periodic, Function.Periodic.eq, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
rw : cos ((↑π : ℂ) / 2) + sin ((↑π : ℂ) / 2) * I = I
rw₁ : 0 + sin ((↑π : ℂ) / 2) * I = I
rw₂ : 0 + 1 * I = I
rw₃ : 0 + I = I
rw₄ rw₅ : I = I
⊢ cexp ((↑π : ℂ) / 2 * I) = I

Tactic:
rw [← cos_add_sin_I, cos_pi_div_two, sin_pi_div_two, one_mul, zero_add]

Premises used: Complex.cos_pi_div_two, Complex.cos_add_sin_I, zero_add, Complex.sin_pi_div_two, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
rw : cos (-(↑π : ℂ) / 2) + sin (-(↑π : ℂ) / 2) * I = -I
rw₁ : cos (-((↑π : ℂ) / 2)) + sin (-((↑π : ℂ) / 2)) * I = -I
rw₂ : cos ((↑π : ℂ) / 2) + sin (-((↑π : ℂ) / 2)) * I = -I
rw₃ : 0 + sin (-((↑π : ℂ) / 2)) * I = -I
rw₄ : 0 + -sin ((↑π : ℂ) / 2) * I = -I
rw₅ : 0 + -1 * I = -I
rw₆ : -1 * I = -I
rw₇ : -(1 * I) = -I
rw₈ rw₉ : -I = -I
⊢ cexp (-(↑π : ℂ) / 2 * I) = -I

Tactic:
rw [← cos_add_sin_I, neg_div, cos_neg, cos_pi_div_two, sin_neg, sin_pi_div_two, zero_add, neg_mul,
    one_mul]

Premises used: neg_div, Complex.cos_pi_div_two, Complex.cos_add_sin_I, zero_add, Complex.sin_pi_div_two, Complex.cos_neg, Complex.sin_neg, neg_mul, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℕ
⊢ cexp ((↑n : ℂ) * (2 * (↑π : ℂ) * I)) = 1

Tactic:
(exp_periodic.nat_mul_eq n).trans exp_zero

Premises used: Complex.exp_zero, Complex.exp_periodic, Function.Periodic.nat_mul_eq, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
n : ℤ
⊢ cexp ((↑n : ℂ) * (2 * (↑π : ℂ) * I)) = 1

Tactic:
(exp_periodic.int_mul_eq n).trans exp_zero

Premises used: Complex.exp_zero, Complex.exp_periodic, Function.Periodic.int_mul_eq, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
z : ℂ
⊢ cexp (z + (↑π : ℂ) * I) = -cexp z

Tactic:
exp_antiperiodic z

Premises used: Complex.exp_antiperiodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
z : ℂ
⊢ cexp (z - (↑π : ℂ) * I) = -cexp z

Tactic:
exp_antiperiodic.sub_eq z

Premises used: Function.Antiperiodic.sub_eq, Complex.exp_antiperiodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
simp : a * ((rexp z.re + rexp (-z.re)) * Real.cos |z.im|) ≤ a * (rexp |z.re| * Real.cos b)
⊢ ‖cexp ((↑a : ℂ) * (cexp z + cexp (-z)))‖ ≤ rexp (a * Real.cos b * rexp |z.re|)

Tactic:
simp only [norm_exp, Real.exp_le_exp, re_ofReal_mul, add_re, exp_re, neg_im, Real.cos_neg, ←
    add_mul, mul_assoc, mul_comm (Real.cos b), neg_re, ← Real.cos_abs z.im]

Premises used: add_mul, Complex.exp_re, Real.cos, Complex.im, mul_assoc, Complex.add_re, Real.exp_le_exp, Real.cos_neg, Complex.neg_re, Complex.norm_exp, mul_comm, Complex.neg_im, Real.cos_abs, Complex.re_ofReal_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
⊢ rexp |z.re| ≤ rexp z.re + rexp (-z.re)

Tactic:
have : Real.exp |z.re| ≤ Real.exp z.re + Real.exp (-z.re) :=
    apply_abs_le_add_of_nonneg (fun x => (Real.exp_pos x).le) z.re
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
this : rexp |z.re| ≤ rexp z.re + rexp (-z.re)
⊢ a * ((rexp z.re + rexp (-z.re)) * Real.cos |z.im|) ≤ a * (rexp |z.re| * Real.cos b)

Tactic:
mul_le_mul_of_nonpos_left (mul_le_mul this ?_ ?_ ((Real.exp_pos _).le.trans this)) ha

Premises used: mul_le_mul_of_nonpos_left, LT.lt.le, mul_le_mul, LE.le.trans, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
this : rexp |z.re| ≤ rexp z.re + rexp (-z.re)
refine_1 : Real.cos b ≤ Real.cos |z.im|
refine_2 : 0 ≤ Real.cos b
⊢ a * ((rexp z.re + rexp (-z.re)) * Real.cos |z.im|) ≤ a * (rexp |z.re| * Real.cos b)

Tactic:
refine mul_le_mul_of_nonpos_left (mul_le_mul this ?_ ?_ ((Real.exp_pos _).le.trans this)) ha

Premises used: mul_le_mul_of_nonpos_left, LT.lt.le, mul_le_mul, LE.le.trans, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
this : rexp |z.re| ≤ rexp z.re + rexp (-z.re)
⊢ Real.cos b ≤ Real.cos |z.im|

Tactic:
Real.cos_le_cos_of_nonneg_of_le_pi (_root_.abs_nonneg _)
        (hb.trans <| half_le_self <| Real.pi_pos.le) hz

Premises used: Real.pi_pos, LT.lt.le, half_le_self, LE.le.trans, abs_nonneg, Real.cos_le_cos_of_nonneg_of_le_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
this : rexp |z.re| ≤ rexp z.re + rexp (-z.re)
⊢ Real.cos b ≤ Real.cos |z.im|

Tactic:
exact
      Real.cos_le_cos_of_nonneg_of_le_pi (_root_.abs_nonneg _)
        (hb.trans <| half_le_self <| Real.pi_pos.le) hz

Premises used: Real.pi_pos, LT.lt.le, half_le_self, LE.le.trans, abs_nonneg, Real.cos_le_cos_of_nonneg_of_le_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
this : rexp |z.re| ≤ rexp z.re + rexp (-z.re)
⊢ 0 ≤ Real.cos b

Tactic:
Real.cos_nonneg_of_mem_Icc ⟨?_, hb⟩

Premises used: Real.cos_nonneg_of_mem_Icc, And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
this : rexp |z.re| ≤ rexp z.re + rexp (-z.re)
refine_2 : -(π / 2) ≤ b
⊢ 0 ≤ Real.cos b

Tactic:
refine Real.cos_nonneg_of_mem_Icc ⟨?_, hb⟩

Premises used: Real.cos_nonneg_of_mem_Icc, And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
this : rexp |z.re| ≤ rexp z.re + rexp (-z.re)
⊢ -(π / 2) ≤ b

Tactic:
(neg_nonpos.2 <| Real.pi_div_two_pos.le).trans ((_root_.abs_nonneg _).trans hz)

Premises used: Iff.mpr, Real.pi_div_two_pos, neg_nonpos, LT.lt.le, LE.le.trans, abs_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
a b : ℝ
ha : a ≤ 0
z : ℂ
hz : |z.im| ≤ b
hb : b ≤ π / 2
this : rexp |z.re| ≤ rexp z.re + rexp (-z.re)
⊢ -(π / 2) ≤ b

Tactic:
exact (neg_nonpos.2 <| Real.pi_div_two_pos.le).trans ((_root_.abs_nonneg _).trans hz)

Premises used: Iff.mpr, Real.pi_div_two_pos, neg_nonpos, LT.lt.le, LE.le.trans, abs_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Function.Antiperiodic sinh ((↑π : ℂ) * I)

Tactic:
simp [Complex.sinh_add, sinh_mul_I, cosh_mul_I]

Premises used: Complex.sinh_add, Complex.sinh_mul_I, Complex.cosh_mul_I
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
z : ℂ
⊢ sinh (z + (↑π : ℂ) * I) = -sinh z

Tactic:
sinh_antiperiodic z

Premises used: Complex.sinh_antiperiodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Function.Periodic sinh (2 * ((↑π : ℂ) * I))

Tactic:
sinh_antiperiodic.periodic_two_mul

Premises used: Function.Antiperiodic.periodic_two_mul, Complex.sinh_antiperiodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
h : 2 * (↑π : ℂ) * I = 2 * ((↑π : ℂ) * I)
⊢ Function.Periodic sinh (2 * (↑π : ℂ) * I)

Tactic:
convert! sinh_antiperiodic.periodic_two_mul using 1

Premises used: Function.Antiperiodic.periodic_two_mul, Complex.sinh_antiperiodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ 2 * (↑π : ℂ) * I = 2 * ((↑π : ℂ) * I)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
z : ℂ
⊢ sinh (z - (↑π : ℂ) * I) = -sinh z

Tactic:
sinh_antiperiodic.sub_eq z

Premises used: Function.Antiperiodic.sub_eq, Complex.sinh_antiperiodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Function.Antiperiodic cosh ((↑π : ℂ) * I)

Tactic:
simp [Complex.cosh_add, cosh_mul_I, sinh_mul_I]

Premises used: Complex.cosh_add, Complex.sinh_mul_I, Complex.cosh_mul_I
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
z : ℂ
⊢ cosh (z + (↑π : ℂ) * I) = -cosh z

Tactic:
cosh_antiperiodic z

Premises used: Complex.cosh_antiperiodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Function.Periodic cosh (2 * ((↑π : ℂ) * I))

Tactic:
cosh_antiperiodic.periodic_two_mul

Premises used: Function.Antiperiodic.periodic_two_mul, Complex.cosh_antiperiodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
h : 2 * (↑π : ℂ) * I = 2 * ((↑π : ℂ) * I)
⊢ Function.Periodic cosh (2 * (↑π : ℂ) * I)

Tactic:
convert! cosh_antiperiodic.periodic_two_mul using 1

Premises used: Function.Antiperiodic.periodic_two_mul, Complex.cosh_antiperiodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
z : ℂ
⊢ cosh (z - (↑π : ℂ) * I) = -cosh z

Tactic:
cosh_antiperiodic.sub_eq z

Premises used: Function.Antiperiodic.sub_eq, Complex.cosh_antiperiodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
⊢ Function.Periodic tanh ((↑π : ℂ) * I)

Tactic:
simp [tanh_eq_sinh_div_cosh]

Premises used: Complex.tanh_eq_sinh_div_cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
z : ℂ
⊢ tanh (z + (↑π : ℂ) * I) = tanh z

Tactic:
tanh_periodic z

Premises used: Complex.tanh_periodic
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Goal:
z : ℂ
⊢ tanh (z - (↑π : ℂ) * I) = tanh z

Tactic:
tanh_periodic.sub_eq z

Premises used: Complex.tanh_periodic, Function.Periodic.sub_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
h : 0 < x
inl : ∀ (h' : 1 < x), sin x < x
inr : ∀ (h' : x ≤ 1), sin x < x
⊢ sin x < x

Tactic:
rcases lt_or_ge 1 x with h' | h'

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
h : 0 < x
h' : 1 < x
⊢ sin x < x

Tactic:
(sin_le_one x).trans_lt h'

Premises used: Real.sin_le_one, LE.le.trans_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
h : 0 < x
h' : 1 < x
⊢ sin x < x

Tactic:
exact (sin_le_one x).trans_lt h'

Premises used: Real.sin_le_one, LE.le.trans_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
h : 0 < x
h' : x ≤ 1
⊢ |x| = x

Tactic:
have hx : |x| = x := abs_of_nonneg h.le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
rwa rwa₁ rwa₂ rwa₃ : x ≤ 1
⊢ |x| ≤ 1

Tactic:
rwa [hx]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
⊢ sin x - (x - HPow.hPow (β := ℕ) x 3 / 6) ≤ HPow.hPow (β := ℕ) |x| 4 * (5 / 96)

Tactic:
have := le_of_abs_le (sin_bound <| show |x| ≤ 1 by rwa [hx])
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x - (x - HPow.hPow (β := ℕ) x 3 / 6) ≤ HPow.hPow (β := ℕ) |x| 4 * (5 / 96)
⊢ sin x ≤ x - HPow.hPow (β := ℕ) x 3 / 6 + HPow.hPow (β := ℕ) x 4 * (5 / 96)

Tactic:
rw [sub_le_iff_le_add', hx] at this

Premises used: sub_le_iff_le_add'
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - HPow.hPow (β := ℕ) x 3 / 6 + HPow.hPow (β := ℕ) x 4 * (5 / 96)
inr : x - HPow.hPow (β := ℕ) x 3 / 6 + HPow.hPow (β := ℕ) x 4 * (5 / 96) < x
⊢ sin x < x

Tactic:
apply this.trans_lt

Premises used: LE.le.trans_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - HPow.hPow (β := ℕ) x 3 / 6 + HPow.hPow (β := ℕ) x 4 * (5 / 96)
inr : HPow.hPow (β := ℕ) x 4 * (5 / 96) < HPow.hPow (β := ℕ) x 3 * 6⁻¹
⊢ x - HPow.hPow (β := ℕ) x 3 / 6 + HPow.hPow (β := ℕ) x 4 * (5 / 96) < x

Tactic:
rw [sub_add, sub_lt_self_iff, sub_pos, div_eq_mul_inv (x ^ 3)]

Premises used: sub_add, sub_pos, div_eq_mul_inv, HPow.hPow, sub_lt_self_iff, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - HPow.hPow (β := ℕ) x 3 / 6 + HPow.hPow (β := ℕ) x 4 * (5 / 96)
⊢ 5 / 96 < 6⁻¹

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - HPow.hPow (β := ℕ) x 3 / 6 + HPow.hPow (β := ℕ) x 4 * (5 / 96)
⊢ 0 ≤ 5 / 96

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - HPow.hPow (β := ℕ) x 3 / 6 + HPow.hPow (β := ℕ) x 4 * (5 / 96)
inr : HPow.hPow (β := ℕ) x 4 ≤ HPow.hPow (β := ℕ) x 3
⊢ HPow.hPow (β := ℕ) x 4 * (5 / 96) < HPow.hPow (β := ℕ) x 3 * 6⁻¹

Tactic:
refine mul_lt_mul' ?_ (by norm_num) (by norm_num) (pow_pos h 3)

Premises used: pow_pos, mul_lt_mul', OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - HPow.hPow (β := ℕ) x 3 / 6 + HPow.hPow (β := ℕ) x 4 * (5 / 96)
inr : LE.le (α := ℕ) 3 4
⊢ HPow.hPow (β := ℕ) x 4 ≤ HPow.hPow (β := ℕ) x 3

Tactic:
apply pow_le_pow_of_le_one h.le h'

Premises used: LT.lt.le, pow_le_pow_of_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - HPow.hPow (β := ℕ) x 3 / 6 + HPow.hPow (β := ℕ) x 4 * (5 / 96)
⊢ LE.le (α := ℕ) 3 4

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
x : ℝ
hx : 0 ≤ x
inl : ∀ (hx : LE.le (α := ℝ) 0 0), sin 0 ≤ 0
inr : ∀ (hx : 0 < x), sin x ≤ x
⊢ sin x ≤ x

Tactic:
obtain rfl | hx := hx.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Goal:
hx : LE.le (α := ℝ) 0 0
⊢ sin 0 ≤ 0

Tactic:
simp