awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
hx : cos x ≠ 0
⊢ HPow.hPow (β := ℕ) (tan x) 2 / (1 + HPow.hPow (β := ℕ) (tan x) 2) = HPow.hPow (β := ℕ) (sin x) 2

Tactic:
simp only [← tan_mul_cos hx, mul_pow, ← inv_one_add_tan_sq hx, div_eq_mul_inv]

Premises used: Real.inv_one_add_tan_sq, div_eq_mul_inv, Real.tan_mul_cos, mul_pow
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
hx : 0 < cos x
rw : (√(1 + HPow.hPow (β := ℕ) (tan x) 2))⁻¹ = √(HPow.hPow (β := ℕ) (cos x) 2)
rw₁ : √(1 + HPow.hPow (β := ℕ) (tan x) 2)⁻¹ = √(HPow.hPow (β := ℕ) (cos x) 2)
rw₂ rw₃ : √(HPow.hPow (β := ℕ) (cos x) 2) = √(HPow.hPow (β := ℕ) (cos x) 2)
⊢ (√(1 + HPow.hPow (β := ℕ) (tan x) 2))⁻¹ = cos x

Tactic:
rw [← sqrt_sq hx.le, ← sqrt_inv, inv_one_add_tan_sq hx.ne']

Premises used: Real.sqrt_inv, Real.inv_one_add_tan_sq, LT.lt.le, LT.lt.ne', Real.sqrt_sq
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
hx : 0 < cos x
rw : tan x / √(1 + HPow.hPow (β := ℕ) (tan x) 2) = tan x * cos x
rw₁ : tan x / √(1 + HPow.hPow (β := ℕ) (tan x) 2) = tan x * (√(1 + HPow.hPow (β := ℕ) (tan x) 2))⁻¹
rw₂ rw₃ : tan x * (√(1 + HPow.hPow (β := ℕ) (tan x) 2))⁻¹ = tan x * (√(1 + HPow.hPow (β := ℕ) (tan x) 2))⁻¹
⊢ tan x / √(1 + HPow.hPow (β := ℕ) (tan x) 2) = sin x

Tactic:
rw [← tan_mul_cos hx.ne', ← inv_sqrt_one_add_tan_sq hx, div_eq_mul_inv]

Premises used: div_eq_mul_inv, LT.lt.ne', Real.inv_sqrt_one_add_tan_sq, Real.tan_mul_cos
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : (↑(cos (3 * x)) : ℂ) = (↑(4 * HPow.hPow (β := ℕ) (cos x) 3 - 3 * cos x) : ℂ)
⊢ cos (3 * x) = 4 * HPow.hPow (β := ℕ) (cos x) 3 - 3 * cos x

Tactic:
rw [← ofReal_inj]

Premises used: Complex.ofReal_inj
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (↑(cos (3 * x)) : ℂ) = (↑(4 * HPow.hPow (β := ℕ) (cos x) 3 - 3 * cos x) : ℂ)

Tactic:
simp [cos_three_mul]

Premises used: Real.cos_three_mul
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : (↑(sin (3 * x)) : ℂ) = (↑(3 * sin x - 4 * HPow.hPow (β := ℕ) (sin x) 3) : ℂ)
⊢ sin (3 * x) = 3 * sin x - 4 * HPow.hPow (β := ℕ) (sin x) 3

Tactic:
rw [← ofReal_inj]

Premises used: Complex.ofReal_inj
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (↑(sin (3 * x)) : ℂ) = (↑(3 * sin x - 4 * HPow.hPow (β := ℕ) (sin x) 3) : ℂ)

Tactic:
simp [sin_three_mul]

Premises used: Real.sin_three_mul
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (↑(sinh x) : ℂ) = (↑((rexp x - rexp (-x)) / 2) : ℂ)

Tactic:
simp [Complex.sinh]

Premises used: Complex.sinh
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
⊢ sinh 0 = 0

Tactic:
simp [sinh]

Premises used: Real.sinh
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ sinh (-x) = -sinh x

Tactic:
simp [sinh]

Premises used: Real.sinh
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℝ
rw : (↑(sinh (x + y)) : ℂ) = (↑(sinh x * cosh y + cosh x * sinh y) : ℂ)
⊢ sinh (x + y) = sinh x * cosh y + cosh x * sinh y

Tactic:
rw [← ofReal_inj]

Premises used: Complex.ofReal_inj
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℝ
⊢ (↑(sinh (x + y)) : ℂ) = (↑(sinh x * cosh y + cosh x * sinh y) : ℂ)

Tactic:
simp [sinh_add]

Premises used: Real.sinh_add
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : (Complex.cosh (↑x : ℂ)).re * 2 = rexp x + rexp (-x)
rw₁ : (Complex.cosh (↑x : ℂ)).re * 2 = (cexp (↑x : ℂ)).re + rexp (-x)
rw₂ : (Complex.cosh (↑x : ℂ)).re * 2 = (cexp (↑x : ℂ)).re + (cexp (↑(-x) : ℂ)).re
rw₃ : (Complex.cosh (↑x : ℂ)).re * 2 = (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
rw₄ : ((cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2).re * 2 = (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
rw₅ :
  ((cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2).re + ((cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2).re =
    (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
rw₆ :
  ((cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2 + (cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2).re =
    (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
rw₇ : ((cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2 * 2).re = (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
rw₈ : (cexp (↑x : ℂ) + cexp (-(↑x : ℂ))).re = (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
rw₉ rw₁₀ : (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re = (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
⊢ cosh x * 2 = rexp x + rexp (-x)

Tactic:
rw [cosh, exp, exp, Complex.ofReal_neg, Complex.cosh, mul_two, ← Complex.add_re, ← mul_two,
      div_mul_cancel₀ _ (two_ne_zero' ℂ), Complex.add_re]

Premises used: div_mul_cancel₀, Complex.ofReal_neg, Complex.add_re, Real.exp, two_ne_zero', Real.cosh, Complex, mul_two, Complex.cosh
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
⊢ cosh 0 = 1

Tactic:
simp [cosh]

Premises used: Real.cosh
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (↑(cosh (-x)) : ℂ) = (↑(cosh x) : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
inl : x ≤ 0 → cosh |x| = cosh x
inr : 0 ≤ x → cosh |x| = cosh x
⊢ cosh |x| = cosh x

Tactic:
cases le_total x 0

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
h : x ≤ 0
⊢ cosh |x| = cosh x

Tactic:
simp [*, abs_of_nonneg, abs_of_nonpos]

Premises used: abs_of_nonpos, abs_of_nonneg
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
h : 0 ≤ x
⊢ cosh |x| = cosh x

Tactic:
simp [*, abs_of_nonneg, abs_of_nonpos]

Premises used: abs_of_nonpos, abs_of_nonneg
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℝ
rw : (↑(cosh (x + y)) : ℂ) = (↑(cosh x * cosh y + sinh x * sinh y) : ℂ)
⊢ cosh (x + y) = cosh x * cosh y + sinh x * sinh y

Tactic:
rw [← ofReal_inj]

Premises used: Complex.ofReal_inj
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℝ
⊢ (↑(cosh (x + y)) : ℂ) = (↑(cosh x * cosh y + sinh x * sinh y) : ℂ)

Tactic:
simp [cosh_add]

Premises used: Real.cosh_add
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℝ
⊢ sinh (x - y) = sinh x * cosh y - cosh x * sinh y

Tactic:
simp [sub_eq_add_neg, sinh_add, sinh_neg, cosh_neg]

Premises used: Real.sinh_add, sub_eq_add_neg, Real.sinh_neg, Real.cosh_neg
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℝ
⊢ cosh (x - y) = cosh x * cosh y - sinh x * sinh y

Tactic:
simp [sub_eq_add_neg, cosh_add, sinh_neg, cosh_neg]

Premises used: sub_eq_add_neg, Real.sinh_neg, Real.cosh_add, Real.cosh_neg
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (↑(tanh x) : ℂ) = (↑(sinh x / cosh x) : ℂ)

Tactic:
simp [tanh_eq_sinh_div_cosh]

Premises used: Real.tanh_eq_sinh_div_cosh
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : sinh x / cosh x = (rexp x - rexp (-x)) / (rexp x + rexp (-x))
rw₁ : (rexp x - rexp (-x)) / 2 / cosh x = (rexp x - rexp (-x)) / (rexp x + rexp (-x))
rw₂ : (rexp x - rexp (-x)) / 2 / ((rexp x + rexp (-x)) / 2) = (rexp x - rexp (-x)) / (rexp x + rexp (-x))
rw₃ rw₄ : (rexp x - rexp (-x)) / (rexp x + rexp (-x)) = (rexp x - rexp (-x)) / (rexp x + rexp (-x))
⊢ tanh x = (rexp x - rexp (-x)) / (rexp x + rexp (-x))

Tactic:
rw [tanh_eq_sinh_div_cosh, sinh_eq, cosh_eq, div_div_div_cancel_right₀ two_ne_zero]

Premises used: Real.sinh_eq, div_div_div_cancel_right₀, Real.tanh_eq_sinh_div_cosh, two_ne_zero, Real.cosh_eq
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
⊢ tanh 0 = 0

Tactic:
simp [tanh]

Premises used: Real.tanh
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ tanh (-x) = -tanh x

Tactic:
simp [tanh]

Premises used: Real.tanh
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : (↑(cosh x + sinh x) : ℂ) = (↑(rexp x) : ℂ)
⊢ cosh x + sinh x = rexp x

Tactic:
rw [← ofReal_inj]

Premises used: Complex.ofReal_inj
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (↑(cosh x + sinh x) : ℂ) = (↑(rexp x) : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : cosh x + sinh x = rexp x
rw₁ rw₂ : rexp x = rexp x
⊢ sinh x + cosh x = rexp x

Tactic:
rw [add_comm, cosh_add_sinh]

Premises used: add_comm, Real.cosh_add_sinh
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ rexp x - cosh x = sinh x

Tactic:
sub_eq_iff_eq_add.2 (sinh_add_cosh x).symm

Premises used: Iff.mpr, sub_eq_iff_eq_add, Real.sinh_add_cosh, Eq.symm
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ rexp x - sinh x = cosh x

Tactic:
sub_eq_iff_eq_add.2 (cosh_add_sinh x).symm

Premises used: Iff.mpr, Real.cosh_add_sinh, sub_eq_iff_eq_add, Eq.symm
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : (↑(cosh x - sinh x) : ℂ) = (↑(rexp (-x)) : ℂ)
⊢ cosh x - sinh x = rexp (-x)

Tactic:
rw [← ofReal_inj]

Premises used: Complex.ofReal_inj
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (↑(cosh x - sinh x) : ℂ) = (↑(rexp (-x)) : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : -(cosh x - sinh x) = -rexp (-x)
rw₁ rw₂ : -rexp (-x) = -rexp (-x)
⊢ sinh x - cosh x = -rexp (-x)

Tactic:
rw [← neg_sub, cosh_sub_sinh]

Premises used: neg_sub, Real.cosh_sub_sinh
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : (↑(HPow.hPow (β := ℕ) (cosh x) 2 - HPow.hPow (β := ℕ) (sinh x) 2) : ℂ) = (↑1 : ℂ)
⊢ HPow.hPow (β := ℕ) (cosh x) 2 - HPow.hPow (β := ℕ) (sinh x) 2 = 1

Tactic:
rw [← ofReal_inj]

Premises used: Complex.ofReal_inj
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (↑(HPow.hPow (β := ℕ) (cosh x) 2 - HPow.hPow (β := ℕ) (sinh x) 2) : ℂ) = (↑1 : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : (↑(HPow.hPow (β := ℕ) (cosh x) 2) : ℂ) = (↑(HPow.hPow (β := ℕ) (sinh x) 2 + 1) : ℂ)
⊢ HPow.hPow (β := ℕ) (cosh x) 2 = HPow.hPow (β := ℕ) (sinh x) 2 + 1

Tactic:
rw [← ofReal_inj]

Premises used: Complex.ofReal_inj
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (↑(HPow.hPow (β := ℕ) (cosh x) 2) : ℂ) = (↑(HPow.hPow (β := ℕ) (sinh x) 2 + 1) : ℂ)

Tactic:
simp [cosh_sq]

Premises used: Real.cosh_sq
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ HPow.hPow (β := ℕ) (cosh x) 2 = 1 + HPow.hPow (β := ℕ) (sinh x) 2

Tactic:
(cosh_sq x).trans (add_comm _ _)

Premises used: Real.cosh_sq, add_comm, Eq.trans
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : (↑(HPow.hPow (β := ℕ) (sinh x) 2) : ℂ) = (↑(HPow.hPow (β := ℕ) (cosh x) 2 - 1) : ℂ)
⊢ HPow.hPow (β := ℕ) (sinh x) 2 = HPow.hPow (β := ℕ) (cosh x) 2 - 1

Tactic:
rw [← ofReal_inj]

Premises used: Complex.ofReal_inj
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (↑(HPow.hPow (β := ℕ) (sinh x) 2) : ℂ) = (↑(HPow.hPow (β := ℕ) (cosh x) 2 - 1) : ℂ)

Tactic:
simp [sinh_sq]

Premises used: Real.sinh_sq
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : (↑(cosh (2 * x)) : ℂ) = (↑(HPow.hPow (β := ℕ) (cosh x) 2 + HPow.hPow (β := ℕ) (sinh x) 2) : ℂ)
⊢ cosh (2 * x) = HPow.hPow (β := ℕ) (cosh x) 2 + HPow.hPow (β := ℕ) (sinh x) 2

Tactic:
rw [← ofReal_inj]

Premises used: Complex.ofReal_inj
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (↑(cosh (2 * x)) : ℂ) = (↑(HPow.hPow (β := ℕ) (cosh x) 2 + HPow.hPow (β := ℕ) (sinh x) 2) : ℂ)

Tactic:
simp [cosh_two_mul]

Premises used: Real.cosh_two_mul
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : (↑(sinh (2 * x)) : ℂ) = (↑(2 * sinh x * cosh x) : ℂ)
⊢ sinh (2 * x) = 2 * sinh x * cosh x

Tactic:
rw [← ofReal_inj]

Premises used: Complex.ofReal_inj
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (↑(sinh (2 * x)) : ℂ) = (↑(2 * sinh x * cosh x) : ℂ)

Tactic:
simp [sinh_two_mul]

Premises used: Real.sinh_two_mul
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : (↑(cosh (3 * x)) : ℂ) = (↑(4 * HPow.hPow (β := ℕ) (cosh x) 3 - 3 * cosh x) : ℂ)
⊢ cosh (3 * x) = 4 * HPow.hPow (β := ℕ) (cosh x) 3 - 3 * cosh x

Tactic:
rw [← ofReal_inj]

Premises used: Complex.ofReal_inj
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (↑(cosh (3 * x)) : ℂ) = (↑(4 * HPow.hPow (β := ℕ) (cosh x) 3 - 3 * cosh x) : ℂ)

Tactic:
simp [cosh_three_mul]

Premises used: Real.cosh_three_mul
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : (↑(sinh (3 * x)) : ℂ) = (↑(4 * HPow.hPow (β := ℕ) (sinh x) 3 + 3 * sinh x) : ℂ)
⊢ sinh (3 * x) = 4 * HPow.hPow (β := ℕ) (sinh x) 3 + 3 * sinh x

Tactic:
rw [← ofReal_inj]

Premises used: Complex.ofReal_inj
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (↑(sinh (3 * x)) : ℂ) = (↑(4 * HPow.hPow (β := ℕ) (sinh x) 3 + 3 * sinh x) : ℂ)

Tactic:
simp [sinh_three_mul]

Premises used: Real.sinh_three_mul
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ 0 < cosh x

Tactic:
(cosh_eq x).symm ▸ half_pos (add_pos (exp_pos x) (exp_pos (-x)))

Premises used: half_pos, add_pos, Eq.rec, Real.cosh_eq, Eq.symm, Neg.neg, Real.exp_pos
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ sinh x < cosh x

Tactic:
lt_of_pow_lt_pow_left₀ 2 (cosh_pos _).le <| (cosh_sq x).symm ▸ lt_add_one _

Premises used: lt_of_pow_lt_pow_left₀, lt_add_one, Eq.rec, LT.lt.le, Real.cosh_sq, Real.cosh_pos, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : (rexp x - rexp (-x)) / (rexp x + rexp (-x)) < 1
⊢ tanh x < 1

Tactic:
rw [tanh_eq]

Premises used: Real.tanh_eq
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
field_simp : rexp x - rexp (-x) < rexp x + rexp (-x)
⊢ (rexp x - rexp (-x)) / (rexp x + rexp (-x)) < 1

Tactic:
field_simp
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ rexp x - rexp (-x) < rexp x + rexp (-x)

Tactic:
grind [exp_pos]

Premises used: Real.exp_pos
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : -1 < (rexp x - rexp (-x)) / (rexp x + rexp (-x))
⊢ -1 < tanh x

Tactic:
rw [tanh_eq]

Premises used: Real.tanh_eq
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
field_simp : -(rexp x + rexp (-x)) < rexp x - rexp (-x)
⊢ -1 < (rexp x - rexp (-x)) / (rexp x + rexp (-x))

Tactic:
field_simp
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ -(rexp x + rexp (-x)) < rexp x - rexp (-x)

Tactic:
grind [exp_pos]

Premises used: Real.exp_pos
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ |tanh x| < 1

Tactic:
abs_lt.mpr ⟨neg_one_lt_tanh x, tanh_lt_one x⟩

Premises used: Iff.mpr, Real.neg_one_lt_tanh, And.intro, Real.tanh_lt_one, abs_lt
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ HPow.hPow (β := ℕ) (tanh x) 2 < 1

Tactic:
(sq_lt_one_iff_abs_lt_one (tanh x)).mpr (abs_tanh_lt_one x)

Premises used: Iff.mpr, Real.abs_tanh_lt_one, Real.tanh, sq_lt_one_iff_abs_lt_one
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
hx : |x| ≤ 1
⊢ ‖(↑x : ℂ)‖ ≤ 1

Tactic:
simpa
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
hx : |x| ≤ 1
⊢ |cos x - (1 - HPow.hPow (β := ℕ) x 2 / 2)| ≤ HPow.hPow (β := ℕ) |x| 4 * (5 / 96)

Tactic:
simpa [← ofReal_cos, ← norm_eq_abs, ← norm_real] using Complex.cos_bound (x := x) (by simpa)

Premises used: Complex.norm_real, Complex.cos_bound, Complex.ofReal_cos, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
hx : |x| ≤ 1
⊢ |sin x - (x - HPow.hPow (β := ℕ) x 3 / 6)| ≤ HPow.hPow (β := ℕ) |x| 4 * (5 / 96)

Tactic:
simpa [← ofReal_sin, ← norm_eq_abs, ← norm_real] using Complex.sin_bound (x := x) (by simpa)

Premises used: Complex.sin_bound, Complex.norm_real, Complex.ofReal_sin, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
hx : |x| ≤ 1
h₁ : HPow.hPow (β := ℕ) |x| 4 ≤ 1
h₂ : HPow.hPow (β := ℕ) x 2 ≤ 1
⊢ HPow.hPow (β := ℕ) |x| 4 * (5 / 96) + HPow.hPow (β := ℕ) x 2 / 2 ≤ 1 * (5 / 96) + 1 / 2

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
hx : |x| ≤ 1
⊢ HPow.hPow (β := ℕ) |x| 4 ≤ 1

Tactic:
pow_le_one₀ (abs_nonneg _) hx

Premises used: abs_nonneg, pow_le_one₀
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
hx : |x| ≤ 1
⊢ HPow.hPow (β := ℕ) |x| 4 ≤ 1

Tactic:
exact pow_le_one₀ (abs_nonneg _) hx

Premises used: pow_le_one₀
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
hx : |x| ≤ 1
h₂ : |x| * |x| ≤ 1
⊢ HPow.hPow (β := ℕ) x 2 ≤ 1

Tactic:
rw [sq, ← abs_mul_self, abs_mul]

Premises used: abs_mul, abs_mul_self, sq
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
hx : |x| ≤ 1
⊢ |x| * |x| ≤ 1

Tactic:
mul_le_one₀ hx (abs_nonneg _) hx

Premises used: mul_le_one₀, abs_nonneg
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
hx : |x| ≤ 1
⊢ |x| * |x| ≤ 1

Tactic:
exact mul_le_one₀ hx (abs_nonneg _) hx

Premises used: mul_le_one₀, abs_nonneg
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
hx : |x| ≤ 1
⊢ 1 * (5 / 96) + 1 / 2 < 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
h₁ : HPow.hPow (β := ℕ) |x| 4 ≤ x
h₂ : HPow.hPow (β := ℕ) x 3 ≤ x
⊢ HPow.hPow (β := ℕ) |x| 4 * (5 / 96) + HPow.hPow (β := ℕ) x 3 / 6 ≤ x * (5 / 96) + x / 6

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
rwa rwa₁ rwa₂ rwa₃ : x ≤ 1
⊢ |x| ≤ 1

Tactic:
rwa [abs_of_nonneg (le_of_lt hx0)]

Premises used: le_of_lt, abs_of_nonneg
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ LE.le (α := ℕ) 1 4

Tactic:
decide
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ HPow.hPow (β := ℕ) |x| 1 = x

Tactic:
simp [abs_of_nonneg (le_of_lt hx0)]

Premises used: le_of_lt, abs_of_nonneg
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
pow_le_pow_of_le_one : HPow.hPow (β := ℕ) |x| 1 = x
⊢ HPow.hPow (β := ℕ) |x| 4 ≤ x

Tactic:
calc
                    |x| ^ 4 ≤ |x| ^ 1 :=
                      pow_le_pow_of_le_one (abs_nonneg _)
                        (by rwa [abs_of_nonneg (le_of_lt hx0)]) (by decide)
                    _ = x := by simp [abs_of_nonneg (le_of_lt hx0)]

Premises used: pow_le_pow_of_le_one
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ LE.le (α := ℕ) 1 3

Tactic:
decide
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ HPow.hPow (β := ℕ) x 1 = x

Tactic:
pow_one _

Premises used: pow_one
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ HPow.hPow (β := ℕ) x 3 ≤ x

Tactic:
calc
                    x ^ 3 ≤ x ^ 1 := pow_le_pow_of_le_one (le_of_lt hx0) hx (by decide)
                    _ = x := pow_one _

Premises used: le_of_lt, pow_le_pow_of_le_one, pow_one
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
linarith : x ≤ x * (5 / 96) + x / 6 → 96 / 96 = 1
linarith₁ linarith₂ : x ≤ x * (5 / 96) + x / 6 → HMul.hMul (α := ℝ) 1 96 = 96
linarith₃ : x ≤ x * (5 / 96) + x / 6 → 6 / 6 = 1
linarith₄ : x ≤ x * (5 / 96) + x / 6 → HMul.hMul (α := ℝ) 16 6 = 96
linarith₅ : x ≤ x * (5 / 96) + x / 6 → GT.gt (α := ℝ) 96 0
linarith₆ : x ≤ x * (5 / 96) + x / 6 → 75 * (0 - x) + (96 * x - (1 * x * HMul.hMul (α := ℝ) 1 5 + 16 * x)) = 0
linarith₇ : x ≤ x * (5 / 96) + x / 6 → GT.gt (α := ℝ) 75 0
⊢ x * (5 / 96) + x / 6 < x

Tactic:
linarith
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
hx0 : 0 < x
hx rwa rwa₁ rwa₂ rwa₃ : x ≤ 1
⊢ |x| ≤ 1

Tactic:
rwa [abs_of_nonneg (le_of_lt hx0)]

Premises used: le_of_lt, abs_of_nonneg
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
hx0 : 0 < x
hx : x ≤ 2
⊢ LT.lt (α := ℝ) 0 2

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
hx0 : 0 < x
hx : x ≤ 2
⊢ x ≤ HMul.hMul (α := ℝ) 1 2

Tactic:
simpa
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
hx0 : 0 < x
hx : x ≤ 2
this : x / 2 ≤ 1
⊢ LT.lt (α := ℝ) 0 2

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
hx0 : 0 < x
hx : x ≤ 2
this : x / 2 ≤ 1
rwa rwa₁ rwa₂ rwa₃ : x / 2 ≤ 1
⊢ |x / 2| ≤ 1

Tactic:
rwa [abs_of_nonneg (le_of_lt (half_pos hx0))]

Premises used: half_pos, le_of_lt, abs_of_nonneg
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
hx0 : 0 < x
hx : x ≤ 2
this : x / 2 ≤ 1
rw : sin (2 * (x / 2)) = sin x
rw₁ : sin (x / 2 + x / 2) = sin x
rw₂ rw₃ : sin x = sin x
⊢ 2 * sin (x / 2) * cos (x / 2) = sin x

Tactic:
rw [← sin_two_mul, two_mul, add_halves]

Premises used: add_halves, two_mul, Real.sin_two_mul
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
⊢ LE.le (α := ℝ) |1| 1

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
⊢ HPow.hPow (α := ℝ) (β := ℕ) |1| 4 * (5 / 96) + (1 - HPow.hPow (α := ℝ) (β := ℕ) 1 2 / 2) ≤ 5 / 9

Tactic:
norm_num
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
⊢ 0 < cos 1

Tactic:
cos_pos_of_le_one (le_of_eq abs_one)

Premises used: abs_one, le_of_eq, Real.cos_pos_of_le_one
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
h : 0 ≤ cos 1
h₁ : cos 1 ≤ 5 / 9
⊢ 2 * HPow.hPow (β := ℕ) (cos 1) 2 - 1 ≤ 2 * HPow.hPow (β := ℕ) (5 / 9) 2 - 1

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
⊢ 0 ≤ cos 1

Tactic:
cos_one_pos.le

Premises used: LT.lt.le, Real.cos_one_pos
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
⊢ 0 ≤ cos 1

Tactic:
exact cos_one_pos.le

Premises used: LT.lt.le, Real.cos_one_pos
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
⊢ cos 1 ≤ 5 / 9

Tactic:
apply cos_one_le

Premises used: Real.cos_one_le
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
⊢ 2 * HPow.hPow (β := ℕ) (5 / 9) 2 - 1 < 0

Tactic:
norm_num
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ 0 < Real.cosh x

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ HPow.hPow (β := ℕ) (Real.sin x) 2 + HPow.hPow (β := ℕ) (Real.cos x) 2 = 1

Tactic:
have := Real.sin_sq_add_cos_sq x
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
this : HPow.hPow (β := ℕ) (Real.sin x) 2 + HPow.hPow (β := ℕ) (Real.cos x) 2 = 1
⊢ ‖cos (↑x : ℂ) + sin (↑x : ℂ) * I‖ = 1

Tactic:
simp_all [add_comm, norm_def, normSq, sq, sin_ofReal_re, cos_ofReal_re, mul_re]

Premises used: Complex.cos_ofReal_re, Complex.mul_re, Complex.normSq, sq, add_comm, Complex.sin_ofReal_re, Complex.norm_def
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : ‖cos (↑x : ℂ) + sin (↑x : ℂ) * I‖ = 1
rw₁ rw₂ : Eq (α := ℝ) 1 1
⊢ ‖cexp ((↑x : ℂ) * I)‖ = 1

Tactic:
rw [exp_mul_I, norm_cos_add_sin_mul_I]

Premises used: Complex.norm_cos_add_sin_mul_I, Complex.exp_mul_I
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : ‖cexp ((↑x : ℂ) * I)‖ = 1
rw₁ rw₂ : Eq (α := ℝ) 1 1
⊢ ‖cexp (I * (↑x : ℂ))‖ = 1

Tactic:
rw [mul_comm, norm_exp_ofReal_mul_I]

Premises used: mul_comm, Complex.norm_exp_ofReal_mul_I
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : (↑(nnnorm (E := ℝ) 1) : ℝ) = 1
⊢ ‖cexp ((↑x : ℂ) * I)‖₊ = 1

Tactic:
rw [← nnnorm_norm, norm_exp_ofReal_mul_I, ← NNReal.coe_eq_one]

Premises used: nnnorm_norm, Complex.norm_exp_ofReal_mul_I, NNReal.coe_eq_one
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (↑(nnnorm (E := ℝ) 1) : ℝ) = 1

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : (↑(nnnorm (E := ℝ) 1) : ℝ) = 1
⊢ ‖cexp (I * (↑x : ℂ))‖₊ = 1

Tactic:
rw [← nnnorm_norm, norm_exp_I_mul_ofReal, ← NNReal.coe_eq_one]

Premises used: nnnorm_norm, Complex.norm_exp_I_mul_ofReal, NNReal.coe_eq_one
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ ‖cexp ((↑x : ℂ) * I)‖ₑ = 1

Tactic:
simp [← ENNReal.toReal_eq_one_iff]

Premises used: ENNReal.toReal_eq_one_iff
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ ‖cexp (I * (↑x : ℂ))‖ₑ = 1

Tactic:
simp [← ENNReal.toReal_eq_one_iff]

Premises used: ENNReal.toReal_eq_one_iff
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ‖2 * Real.sin (x / 2)‖ = ‖2 * Real.sin (x / 2)‖
⊢ ‖2 * Real.sin (x / 2)‖ = ‖2 * sin ((↑x : ℂ) / 2)‖

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖(cexp (-((↑x : ℂ) / 2) * I) - cexp ((↑x : ℂ) / 2 * I)) * I‖
⊢ ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖2 * Real.sin (x / 2)‖

Tactic:
rw [show ‖2 * Real.sin (x / 2)‖ = ‖2 * sin (x / 2)‖ by norm_cast, two_sin]

Premises used: Complex.two_sin