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

Tactic:
simp [field]
-- 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: Complex.tan_mul_cos, div_eq_mul_inv, Complex.inv_one_add_tan_sq, mul_pow
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
rw : cosh (3 * x * I) = 4 * HPow.hPow (β := ℕ) (cos x) 3 - 3 * cos x
rw₁ : cosh (3 * (x * I)) = 4 * HPow.hPow (β := ℕ) (cos x) 3 - 3 * cos x
rw₂ : 4 * HPow.hPow (β := ℕ) (cosh (x * I)) 3 - 3 * cosh (x * I) = 4 * HPow.hPow (β := ℕ) (cos x) 3 - 3 * cos x
rw₃ rw₄ : 4 * HPow.hPow (β := ℕ) (cos x) 3 - 3 * cos x = 4 * HPow.hPow (β := ℕ) (cos x) 3 - 3 * cos x
⊢ cos (3 * x) = 4 * HPow.hPow (β := ℕ) (cos x) 3 - 3 * cos x

Tactic:
rw [← cosh_mul_I, mul_assoc, cosh_three_mul, cosh_mul_I]

Premises used: Complex.cosh_three_mul, mul_assoc, Complex.cosh_mul_I
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
rw : sin (2 * x) * cos x + cos (2 * x) * sin x = HAdd.hAdd (α := ℂ) 2 1 * sin x - 4 * HPow.hPow (β := ℕ) (sin x) 3
⊢ sin (3 * x) = 3 * sin x - 4 * HPow.hPow (β := ℕ) (sin x) 3

Tactic:
rw [← two_add_one_eq_three, add_one_mul, sin_add (2 * x) x]

Premises used: HMul.hMul, add_one_mul, Complex.sin_add, OfNat.ofNat, two_add_one_eq_three
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
simp :
  2 * (sin x * (1 - HPow.hPow (β := ℕ) (sin x) 2)) + (2 * (1 - HPow.hPow (β := ℕ) (sin x) 2) - 1) * sin x =
    HAdd.hAdd (α := ℂ) 2 1 * sin x - 4 * HPow.hPow (β := ℕ) (sin x) 3
⊢ sin (2 * x) * cos x + cos (2 * x) * sin x = HAdd.hAdd (α := ℂ) 2 1 * sin x - 4 * HPow.hPow (β := ℕ) (sin x) 3

Tactic:
simp only [cos_two_mul, sin_two_mul, cos_sq', mul_assoc, ← sq]

Premises used: Complex.sin_two_mul, mul_assoc, Complex.cos_two_mul, sq, Complex.cos_sq'
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
⊢ 2 * (sin x * (1 - HPow.hPow (β := ℕ) (sin x) 2)) + (2 * (1 - HPow.hPow (β := ℕ) (sin x) 2) - 1) * sin x =
    HAdd.hAdd (α := ℂ) 2 1 * sin x - 4 * HPow.hPow (β := ℕ) (sin x) 3

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
⊢ cexp (x * I) = cos x + sin x * I

Tactic:
(cos_add_sin_I _).symm

Premises used: Complex.cos_add_sin_I, Eq.symm
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℂ
rw : cexp x * cexp (y * I) = cexp x * (cos y + sin y * I)
rw₁ rw₂ : cexp x * (cos y + sin y * I) = cexp x * (cos y + sin y * I)
⊢ cexp (x + y * I) = cexp x * (cos y + sin y * I)

Tactic:
rw [exp_add, exp_mul_I]

Premises used: Complex.exp_add, Complex.exp_mul_I
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
rw : cexp x = cexp ((↑x.re : ℂ) + (↑x.im : ℂ) * I)
rw₁ rw₂ : cexp x = cexp x
⊢ cexp x = cexp (↑x.re : ℂ) * (cos (↑x.im : ℂ) + sin (↑x.im : ℂ) * I)

Tactic:
rw [← exp_add_mul_I, re_add_im]

Premises used: Complex.exp_add_mul_I, Complex.re_add_im
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
rw : (cexp (↑x.re : ℂ) * (cos (↑x.im : ℂ) + sin (↑x.im : ℂ) * I)).re = Real.exp x.re * Real.cos x.im
⊢ (cexp x).re = Real.exp x.re * Real.cos x.im

Tactic:
rw [exp_eq_exp_re_mul_sin_add_cos]

Premises used: Complex.exp_eq_exp_re_mul_sin_add_cos
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
⊢ (cexp (↑x.re : ℂ) * (cos (↑x.im : ℂ) + sin (↑x.im : ℂ) * I)).re = Real.exp x.re * Real.cos x.im

Tactic:
simp [exp_ofReal_re, cos_ofReal_re]

Premises used: Complex.cos_ofReal_re, Complex.exp_ofReal_re
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
rw : (cexp (↑x.re : ℂ) * (cos (↑x.im : ℂ) + sin (↑x.im : ℂ) * I)).im = Real.exp x.re * Real.sin x.im
⊢ (cexp x).im = Real.exp x.re * Real.sin x.im

Tactic:
rw [exp_eq_exp_re_mul_sin_add_cos]

Premises used: Complex.exp_eq_exp_re_mul_sin_add_cos
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
⊢ (cexp (↑x.re : ℂ) * (cos (↑x.im : ℂ) + sin (↑x.im : ℂ) * I)).im = Real.exp x.re * Real.sin x.im

Tactic:
simp [exp_ofReal_re, sin_ofReal_re]

Premises used: Complex.exp_ofReal_re, Complex.sin_ofReal_re
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (cexp ((↑x : ℂ) * I)).re = Real.cos x

Tactic:
simp [exp_mul_I, cos_ofReal_re]

Premises used: Complex.cos_ofReal_re, Complex.exp_mul_I
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (cexp ((↑x : ℂ) * I)).im = Real.sin x

Tactic:
simp [exp_mul_I, sin_ofReal_re]

Premises used: Complex.sin_ofReal_re, Complex.exp_mul_I
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ cexp ((↑x : ℂ) * I) = (↑(Real.cos x) : ℂ) + (↑(Real.sin x) : ℂ) * I

Tactic:
simp [exp_mul_I]

Premises used: Complex.exp_mul_I
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
n : ℕ
z : ℂ
rw : cexp (z * I) ^ n = cos ((↑n : ℂ) * z) + sin ((↑n : ℂ) * z) * I
rw₁ : cexp (z * I) ^ n = cexp ((↑n : ℂ) * z * I)
rw₂ : cexp ((↑n : ℂ) * (z * I)) = cexp ((↑n : ℂ) * z * I)
rw₃ rw₄ : cexp ((↑n : ℂ) * (z * I)) = cexp ((↑n : ℂ) * (z * I))
⊢ (cos z + sin z * I) ^ n = cos ((↑n : ℂ) * z) + sin ((↑n : ℂ) * z) * I

Tactic:
rw [← exp_mul_I, ← exp_mul_I, ← exp_nat_mul, mul_assoc]

Premises used: mul_assoc, Complex.exp_nat_mul, Complex.exp_mul_I
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
simp :
  ‖(cexp (x * I) + cexp (-(x * I))) / 2 - (1 - HPow.hPow (β := ℕ) x 2 / 2)‖ =
    ‖(cexp (-(x * I)) - (1 + -(x * I) + HPow.hPow (β := ℕ) (x * I) 2 / 2 + HPow.hPow (β := ℕ) (-(x * I)) 3 / 6)) / 2 +
        (cexp (x * I) - (1 + x * I + HPow.hPow (β := ℕ) (x * I) 2 / 2 + HPow.hPow (β := ℕ) (x * I) 3 / 6)) / 2‖
⊢ ‖cos x - (1 - HPow.hPow (β := ℕ) x 2 / 2)‖ =
    ‖(cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / (↑m.factorial : ℂ)) / 2 +
        (cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)) / 2‖

Tactic:
simp [cos, field, Finset.sum_range_succ, Nat.factorial]

Premises used: Complex.cos, Nat.factorial, Finset.sum_range_succ
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖(cexp (x * I) + cexp (-(x * I))) / 2 - (1 - HPow.hPow (β := ℕ) x 2 / 2)‖ =
    ‖(cexp (-(x * I)) - (1 + -(x * I) + HPow.hPow (β := ℕ) (x * I) 2 / 2 + HPow.hPow (β := ℕ) (-(x * I)) 3 / 6)) / 2 +
        (cexp (x * I) - (1 + x * I + HPow.hPow (β := ℕ) (x * I) 2 / 2 + HPow.hPow (β := ℕ) (x * I) 3 / 6)) / 2‖

Tactic:
grind [I_sq, two_ne_zero]

Premises used: two_ne_zero, Complex.I_sq
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
grw :
  ‖(cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / (↑m.factorial : ℂ)) / 2‖ +
      ‖(cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)) / 2‖ ≤
    ‖cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / (↑m.factorial : ℂ)‖ / 2 +
      ‖cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)‖ / 2
⊢ ‖(cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / (↑m.factorial : ℂ)) / 2 +
        (cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)) / 2‖ ≤
    ‖cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / (↑m.factorial : ℂ)‖ / 2 +
      ‖cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)‖ / 2

Tactic:
grw [norm_add_le]

Premises used: norm_add_le
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖(cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / (↑m.factorial : ℂ)) / 2‖ +
      ‖(cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)) / 2‖ ≤
    ‖cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / (↑m.factorial : ℂ)‖ / 2 +
      ‖cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)‖ / 2

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖-x * I‖ ≤ 1

Tactic:
simpa
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ LT.lt (α := ℕ) 0 4

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖x * I‖ ≤ 1

Tactic:
simpa
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
h₁ : LE.le (α := ℝ) 0 2
grw :
  HPow.hPow (β := ℕ) ‖-x * I‖ 4 * ((↑(Nat.succ 4) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 4) : ℝ) (↑4 : ℝ))⁻¹) / 2 +
      ‖cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)‖ / 2 ≤
    HPow.hPow (β := ℕ) ‖-x * I‖ 4 * ((↑(Nat.succ 4) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 4) : ℝ) (↑4 : ℝ))⁻¹) /
        2 +
      HPow.hPow (β := ℕ) ‖x * I‖ 4 * ((↑(Nat.succ 4) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 4) : ℝ) (↑4 : ℝ))⁻¹) /
        2
grw₁ grw₂ :
  HPow.hPow (β := ℕ) ‖-x * I‖ 4 * ((↑(Nat.succ 4) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 4) : ℝ) (↑4 : ℝ))⁻¹) / 2 +
      HPow.hPow (β := ℕ) ‖x * I‖ 4 * ((↑(Nat.succ 4) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 4) : ℝ) (↑4 : ℝ))⁻¹) /
        2 ≤
    HPow.hPow (β := ℕ) ‖-x * I‖ 4 * ((↑(Nat.succ 4) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 4) : ℝ) (↑4 : ℝ))⁻¹) /
        2 +
      HPow.hPow (β := ℕ) ‖x * I‖ 4 * ((↑(Nat.succ 4) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 4) : ℝ) (↑4 : ℝ))⁻¹) /
        2
⊢ ‖cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / (↑m.factorial : ℂ)‖ / 2 +
      ‖cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)‖ / 2 ≤
    HPow.hPow (β := ℕ) ‖-x * I‖ 4 * ((↑(Nat.succ 4) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 4) : ℝ) (↑4 : ℝ))⁻¹) /
        2 +
      HPow.hPow (β := ℕ) ‖x * I‖ 4 * ((↑(Nat.succ 4) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 4) : ℝ) (↑4 : ℝ))⁻¹) /
        2

Tactic:
grw [exp_bound (by simpa) (by simp), exp_bound (by simpa) (by simp)]

Premises used: Complex.exp_bound
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ HPow.hPow (β := ℕ) ‖-x * I‖ 4 * ((↑(Nat.succ 4) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 4) : ℝ) (↑4 : ℝ))⁻¹) / 2 +
      HPow.hPow (β := ℕ) ‖x * I‖ 4 * ((↑(Nat.succ 4) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 4) : ℝ) (↑4 : ℝ))⁻¹) /
        2 ≤
    HPow.hPow (β := ℕ) ‖x‖ 4 * (5 / 96)

Tactic:
norm_num
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
simp :
  ‖(cexp (-(x * I)) - cexp (x * I)) * I / 2 - (x - HPow.hPow (β := ℕ) x 3 / 6)‖ =
    ‖(cexp (-(x * I)) - (1 + -(x * I) + HPow.hPow (β := ℕ) (x * I) 2 / 2 + HPow.hPow (β := ℕ) (-(x * I)) 3 / 6)) * I /
          2 -
        (cexp (x * I) - (1 + x * I + HPow.hPow (β := ℕ) (x * I) 2 / 2 + HPow.hPow (β := ℕ) (x * I) 3 / 6)) * I / 2‖
⊢ ‖sin x - (x - HPow.hPow (β := ℕ) x 3 / 6)‖ =
    ‖(cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / (↑m.factorial : ℂ)) * I / 2 -
        (cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)) * I / 2‖

Tactic:
simp [sin, field, Finset.sum_range_succ, Nat.factorial]

Premises used: Complex.sin, Nat.factorial, Finset.sum_range_succ
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖(cexp (-(x * I)) - cexp (x * I)) * I / 2 - (x - HPow.hPow (β := ℕ) x 3 / 6)‖ =
    ‖(cexp (-(x * I)) - (1 + -(x * I) + HPow.hPow (β := ℕ) (x * I) 2 / 2 + HPow.hPow (β := ℕ) (-(x * I)) 3 / 6)) * I /
          2 -
        (cexp (x * I) - (1 + x * I + HPow.hPow (β := ℕ) (x * I) 2 / 2 + HPow.hPow (β := ℕ) (x * I) 3 / 6)) * I / 2‖

Tactic:
grind [I_sq, two_ne_zero]

Premises used: two_ne_zero, Complex.I_sq
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
grw :
  ‖(cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / (↑m.factorial : ℂ)) * I / 2‖ +
      ‖(cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)) * I / 2‖ ≤
    ‖cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / (↑m.factorial : ℂ)‖ / 2 +
      ‖cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)‖ / 2
⊢ ‖(cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / (↑m.factorial : ℂ)) * I / 2 -
        (cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)) * I / 2‖ ≤
    ‖cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / (↑m.factorial : ℂ)‖ / 2 +
      ‖cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)‖ / 2

Tactic:
grw [norm_sub_le]

Premises used: norm_sub_le
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖(cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / (↑m.factorial : ℂ)) * I / 2‖ +
      ‖(cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)) * I / 2‖ ≤
    ‖cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / (↑m.factorial : ℂ)‖ / 2 +
      ‖cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)‖ / 2

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
⊢ sin 0 = 0

Tactic:
simp [sin]

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

Tactic:
simp [sin]

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

Tactic:
simp [sin_add]

Premises used: Real.sin_add
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
⊢ cos 0 = 1

Tactic:
simp [cos]

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

Tactic:
simp [cos]

Premises used: Real.cos
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
inl : x ≤ 0 → cos |x| = cos x
inr : 0 ≤ x → cos |x| = cos x
⊢ cos |x| = cos x

Tactic:
cases le_total x 0

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

Tactic:
simp only [*, abs_of_nonneg, abs_of_nonpos, cos_neg]

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

Tactic:
simp only [*, abs_of_nonneg, abs_of_nonpos, cos_neg]

Premises used: abs_of_nonpos, Real.cos_neg, abs_of_nonneg
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℝ
⊢ (↑(cos (x + y)) : ℂ) = (↑(cos x * cos y - sin x * sin y) : ℂ)

Tactic:
simp [cos_add]

Premises used: Real.cos_add
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℝ
⊢ sin (x - y) = sin x * cos y - cos x * sin y

Tactic:
simp [sub_eq_add_neg, sin_add, sin_neg, cos_neg]

Premises used: sub_eq_add_neg, Real.sin_add, Real.sin_neg, Real.cos_neg
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℝ
⊢ cos (x - y) = cos x * cos y + sin x * sin y

Tactic:
simp [sub_eq_add_neg, cos_add, sin_neg, cos_neg]

Premises used: sub_eq_add_neg, Real.sin_neg, Real.cos_add, Real.cos_neg
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℝ
⊢ (↑(sin x + sin y) : ℂ) = (↑(2 * sin ((x + y) / 2) * cos ((x - y) / 2)) : ℂ)

Tactic:
simp [sin_add_sin]

Premises used: Real.sin_add_sin
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℝ
⊢ (↑(sin x - sin y) : ℂ) = (↑(2 * sin ((x - y) / 2) * cos ((x + y) / 2)) : ℂ)

Tactic:
simp [sin_sub_sin]

Premises used: Real.sin_sub_sin
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℝ
⊢ (↑(cos x + cos y) : ℂ) = (↑(2 * cos ((x + y) / 2) * cos ((x - y) / 2)) : ℂ)

Tactic:
simp [cos_add_cos]

Premises used: Real.cos_add_cos
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℝ
⊢ (↑(cos x - cos y) : ℂ) = (↑(-2 * sin ((x + y) / 2) * sin ((x - y) / 2)) : ℂ)

Tactic:
simp [cos_sub_cos]

Premises used: Real.cos_sub_cos
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℝ
simp : 2 * sin x * sin y = sin x * sin y + sin x * sin y
⊢ 2 * sin x * sin y = cos (x - y) - cos (x + y)

Tactic:
simp [cos_add, cos_sub]

Premises used: Real.cos_add, Real.cos_sub
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℝ
⊢ 2 * sin x * sin y = sin x * sin y + sin x * sin y

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℝ
simp : 2 * cos x * cos y = cos x * cos y + cos x * cos y
⊢ 2 * cos x * cos y = cos (x - y) + cos (x + y)

Tactic:
simp [cos_add, cos_sub]

Premises used: Real.cos_add, Real.cos_sub
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℝ
⊢ 2 * cos x * cos y = cos x * cos y + cos x * cos y

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℝ
simp : 2 * sin x * cos y = sin x * cos y + sin x * cos y
⊢ 2 * sin x * cos y = sin (x - y) + sin (x + y)

Tactic:
simp [sin_add, sin_sub]

Premises used: Real.sin_sub, Real.sin_add
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℝ
⊢ 2 * sin x * cos y = sin x * cos y + sin x * cos y

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (↑(tan x) : ℂ) = (↑(sin x / cos x) : ℂ)

Tactic:
simp only [ofReal_tan, tan_eq_sin_div_cos, ofReal_div, ofReal_sin,
    ofReal_cos]

Premises used: Complex.ofReal_cos, Complex.ofReal_div, Complex.ofReal_sin, Real.tan_eq_sin_div_cos, Complex.ofReal_tan
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (↑x.cot : ℂ) = (↑(cos x / sin x) : ℂ)

Tactic:
simp [cot_eq_cos_div_sin]

Premises used: Real.cot_eq_cos_div_sin
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
hx : cos x ≠ 0
rw : sin x / cos x * cos x = sin x
rw₁ rw₂ : sin x = sin x
⊢ tan x * cos x = sin x

Tactic:
rw [tan_eq_sin_div_cos, div_mul_cancel₀ _ hx]

Premises used: div_mul_cancel₀, Real.tan_eq_sin_div_cos
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (↑(tan x)⁻¹ : ℂ) = (↑x.cot : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (↑x.cot⁻¹ : ℂ) = (↑(tan x) : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
⊢ tan 0 = 0

Tactic:
simp [tan]

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

Tactic:
simp [tan]

Premises used: Real.tan
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (↑(HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2) : ℂ) = (↑1 : ℂ)

Tactic:
simp [sin_sq_add_cos_sq]

Premises used: Real.sin_sq_add_cos_sq
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 = 1
rw₁ rw₂ : Eq (α := ℝ) 1 1
⊢ HPow.hPow (β := ℕ) (cos x) 2 + HPow.hPow (β := ℕ) (sin x) 2 = 1

Tactic:
rw [add_comm, sin_sq_add_cos_sq]

Premises used: add_comm, Real.sin_sq_add_cos_sq
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : HPow.hPow (β := ℕ) (sin x) 2 ≤ HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2
⊢ HPow.hPow (β := ℕ) (sin x) 2 ≤ 1

Tactic:
rw [← sin_sq_add_cos_sq x]

Premises used: Real.sin_sq_add_cos_sq
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ HPow.hPow (β := ℕ) (sin x) 2 ≤ HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2

Tactic:
le_add_of_nonneg_right (sq_nonneg _)

Premises used: le_add_of_nonneg_right, sq_nonneg
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ HPow.hPow (β := ℕ) (sin x) 2 ≤ HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2

Tactic:
exact le_add_of_nonneg_right (sq_nonneg _)

Premises used: le_add_of_nonneg_right
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : HPow.hPow (β := ℕ) (cos x) 2 ≤ HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2
⊢ HPow.hPow (β := ℕ) (cos x) 2 ≤ 1

Tactic:
rw [← sin_sq_add_cos_sq x]

Premises used: Real.sin_sq_add_cos_sq
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ HPow.hPow (β := ℕ) (cos x) 2 ≤ HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2

Tactic:
le_add_of_nonneg_left (sq_nonneg _)

Premises used: sq_nonneg, le_add_of_nonneg_left
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ HPow.hPow (β := ℕ) (cos x) 2 ≤ HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2

Tactic:
exact le_add_of_nonneg_left (sq_nonneg _)

Premises used: le_add_of_nonneg_left
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ sin x * sin x ≤ 1

Tactic:
simp only [← sq, sin_sq_le_one]

Premises used: sq, Real.sin_sq_le_one
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ cos x * cos x ≤ 1

Tactic:
simp only [← sq, cos_sq_le_one]

Premises used: sq, Real.cos_sq_le_one
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ sin x ≤ 1

Tactic:
(abs_le.1 (abs_sin_le_one _)).2

Premises used: abs_le, And.right, Iff.mp, Real.abs_sin_le_one
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ cos x ≤ 1

Tactic:
(abs_le.1 (abs_cos_le_one _)).2

Premises used: Real.abs_cos_le_one, abs_le, And.right, Iff.mp
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ -1 ≤ sin x

Tactic:
(abs_le.1 (abs_sin_le_one _)).1

Premises used: abs_le, And.left, Iff.mp, Real.abs_sin_le_one
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ -1 ≤ cos x

Tactic:
(abs_le.1 (abs_cos_le_one _)).1

Premises used: Real.abs_cos_le_one, abs_le, And.left, Iff.mp
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (↑(cos (2 * x)) : ℂ) = (↑(2 * HPow.hPow (β := ℕ) (cos x) 2 - 1) : ℂ)

Tactic:
simp [cos_two_mul]

Premises used: Real.cos_two_mul
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (↑(cos (2 * x)) : ℂ) = (↑(HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sin x) 2) : ℂ)

Tactic:
simp [cos_two_mul']

Premises used: Real.cos_two_mul'
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (↑(cos (2 * x)) : ℂ) = (↑(1 - 2 * HPow.hPow (β := ℕ) (sin x) 2) : ℂ)

Tactic:
simp [cos_two_mul_eq_one_sub]

Premises used: Real.cos_two_mul_eq_one_sub
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (↑(sin (2 * x)) : ℂ) = (↑(2 * sin x * cos x) : ℂ)

Tactic:
simp [sin_two_mul]

Premises used: Real.sin_two_mul
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (↑(HPow.hPow (β := ℕ) (cos x) 2) : ℂ) = (↑(1 / 2 + cos (2 * x) / 2) : ℂ)

Tactic:
simp [cos_sq]

Premises used: Real.cos_sq
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw :
  HPow.hPow (β := ℕ) (cos x) 2 =
    HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sin x) 2
rw₁ rw₂ : HPow.hPow (β := ℕ) (cos x) 2 = HPow.hPow (β := ℕ) (cos x) 2
⊢ HPow.hPow (β := ℕ) (cos x) 2 = 1 - HPow.hPow (β := ℕ) (sin x) 2

Tactic:
rw [← sin_sq_add_cos_sq x, add_sub_cancel_left]

Premises used: add_sub_cancel_left, Real.sin_sq_add_cos_sq
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ HPow.hPow (β := ℕ) (sin x) 2 = 1 - HPow.hPow (β := ℕ) (cos x) 2

Tactic:
eq_sub_iff_add_eq.2 <| sin_sq_add_cos_sq _

Premises used: Iff.mpr, eq_sub_iff_add_eq, Real.sin_sq_add_cos_sq
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : 1 - HPow.hPow (β := ℕ) (cos x) 2 = 1 / 2 - cos (2 * x) / 2
rw₁ : 1 - (1 / 2 + cos (2 * x) / 2) = 1 / 2 - cos (2 * x) / 2
rw₂ : 1 - 1 / 2 - cos (2 * x) / 2 = 1 / 2 - cos (2 * x) / 2
rw₃ rw₄ : 1 / 2 - cos (2 * x) / 2 = 1 / 2 - cos (2 * x) / 2
⊢ HPow.hPow (β := ℕ) (sin x) 2 = 1 / 2 - cos (2 * x) / 2

Tactic:
rw [sin_sq, cos_sq, ← sub_sub, sub_half]

Premises used: Real.sin_sq, sub_sub, sub_half, Real.cos_sq
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : |sin x| = √(HPow.hPow (β := ℕ) (sin x) 2)
rw₁ rw₂ : |sin x| = |sin x|
⊢ |sin x| = √(1 - HPow.hPow (β := ℕ) (cos x) 2)

Tactic:
rw [← sin_sq, sqrt_sq_eq_abs]

Premises used: Real.sqrt_sq_eq_abs, Real.sin_sq
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : |cos x| = √(HPow.hPow (β := ℕ) (cos x) 2)
rw₁ rw₂ : |cos x| = |cos x|
⊢ |cos x| = √(1 - HPow.hPow (β := ℕ) (sin x) 2)

Tactic:
rw [← cos_sq', sqrt_sq_eq_abs]

Premises used: Real.sqrt_sq_eq_abs, Real.cos_sq'
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
h : cos x ≠ 0
⊢ (1 + HPow.hPow (β := ℕ) (tan x) 2) * HPow.hPow (β := ℕ) (cos x) 2 = 1

Tactic:
mod_cast @Complex.one_add_tan_sq_mul_cos_sq_eq_one x (mod_cast h)

Premises used: Complex.one_add_tan_sq_mul_cos_sq_eq_one, HMul.hMul, Complex.cos, Real.cos, congrArg, cast, Ne, Complex.ofReal_pow._simp_1, Complex.ofReal, Nat.cast, Complex.ofReal_mul._simp_1, HPow.hPow, Complex.ofReal_cos._simp_1, HAdd.hAdd, Complex.tan, congr, congrFun', Nat.cast_zero, Complex.ofReal_tan._simp_1, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Not, Complex.ofReal_add._simp_1, Complex.ofReal_inj._simp_1, Eq.trans, Real.tan
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
hx : cos x ≠ 0
this : Complex.cos (↑x : ℂ) ≠ 0
⊢ (↑(1 + HPow.hPow (β := ℕ) (tan x) 2)⁻¹ : ℂ) = (↑(HPow.hPow (β := ℕ) (cos x) 2) : ℂ)

Tactic:
simpa using Complex.inv_one_add_tan_sq this

Premises used: Complex.inv_one_add_tan_sq