awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℂ
s1 : sin x = sin ((x + y) / 2) * cos ((x - y) / 2) + cos ((x + y) / 2) * sin ((x - y) / 2)
s2 : sin y = sin ((x + y) / 2) * cos ((x - y) / 2) - cos ((x + y) / 2) * sin ((x - y) / 2)
⊢ sin ((x + y) / 2) * cos ((x - y) / 2) + cos ((x + y) / 2) * sin ((x - y) / 2) -
      (sin ((x + y) / 2) * cos ((x - y) / 2) - cos ((x + y) / 2) * sin ((x - y) / 2)) =
    2 * sin ((x - y) / 2) * cos ((x + y) / 2)

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

Tactic:
have s1 := cos_add ((x + y) / 2) ((x - y) / 2)
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℂ
s1 : cos ((x + y) / 2 + (x - y) / 2) = cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2)
⊢ cos ((x + y) / 2 - (x - y) / 2) = cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)

Tactic:
have s2 := cos_sub ((x + y) / 2) ((x - y) / 2)
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℂ
s1 : cos ((x + y) / 2 + (x - y) / 2) = cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2)
s2 : cos ((x + y) / 2 - (x - y) / 2) = cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)
⊢ cos x = cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2)

Tactic:
rw [← add_div, add_sub, add_right_comm, add_sub_cancel_right, add_self_div_two] at s1

Premises used: add_sub, add_right_comm, add_sub_cancel_right, add_div, add_self_div_two
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℂ
s1 : cos ((x + y) / 2 + (x - y) / 2) = cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2)
s2 : cos ((x + y) / 2 - (x - y) / 2) = cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)
s1₁ : cos x = cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2)
⊢ cos ((x + y) / 2 - (x - y) / 2) = cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)

Tactic:
rw [← add_div, add_sub, add_right_comm, add_sub_cancel_right, add_self_div_two] at s1

Premises used: add_sub, add_right_comm, add_sub_cancel_right, add_div, add_self_div_two
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℂ
s1 : cos x = cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2)
s2 : cos ((x + y) / 2 - (x - y) / 2) = cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)
⊢ cos y = cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)

Tactic:
rw [div_sub_div_same, ← sub_add, add_sub_cancel_left, add_self_div_two] at s2

Premises used: sub_add, add_sub_cancel_left, div_sub_div_same, add_self_div_two
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℂ
s1 : cos x = cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2)
s2 : cos y = cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)
rw :
  cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) -
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) =
    -2 * sin ((x + y) / 2) * sin ((x - y) / 2)
⊢ cos x - cos y = -2 * sin ((x + y) / 2) * sin ((x - y) / 2)

Tactic:
rw [s1, s2]
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℂ
s1 : cos x = cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2)
s2 : cos y = cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)
⊢ cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) -
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) =
    -2 * sin ((x + y) / 2) * sin ((x - y) / 2)

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

Tactic:
simpa using sin_sub_sin x (-y)

Premises used: Complex.sin_sub_sin, Neg.neg
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℂ
⊢ cos x + cos y = cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2)

Tactic:
?_
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℂ
⊢ cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) =
    cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2))

Tactic:
?_
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℂ
⊢ cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) =
    2 * cos ((x + y) / 2) * cos ((x - y) / 2)

Tactic:
?_
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℂ
calc_1 : cos x + cos y = cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2)
calc_2 :
  cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) =
    cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2))
calc_3 :
  cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) =
    2 * cos ((x + y) / 2) * cos ((x - y) / 2)
⊢ cos x + cos y = 2 * cos ((x + y) / 2) * cos ((x - y) / 2)

Tactic:
calc
    cos x + cos y = cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) := ?_
    _ =
        cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
          (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) :=
      ?_
    _ = 2 * cos ((x + y) / 2) * cos ((x - y) / 2) := ?_

Premises used: HMul.hMul, Complex.cos, Complex.sin, HSub.hSub, HDiv.hDiv, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℂ
calc_1 : x = (x + y) / 2 + (x - y) / 2
calc_1₁ : y = (x + y) / 2 - (x - y) / 2
⊢ cos x + cos y = cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2)

Tactic:
congr
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℂ
⊢ x = (x + y) / 2 + (x - y) / 2

Tactic:
field
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℂ
⊢ y = (x + y) / 2 - (x - y) / 2

Tactic:
field
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℂ
calc_2 :
  cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) =
    cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2))
calc_2₁ calc_2₂ :
  cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) =
    cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2))
⊢ cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2) =
    cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2))

Tactic:
rw [cos_add, cos_sub]

Premises used: Complex.cos_sub, Complex.cos_add
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℂ
⊢ cos ((x + y) / 2) * cos ((x - y) / 2) - sin ((x + y) / 2) * sin ((x - y) / 2) +
      (cos ((x + y) / 2) * cos ((x - y) / 2) + sin ((x + y) / 2) * sin ((x - y) / 2)) =
    2 * cos ((x + y) / 2) * cos ((x - y) / 2)

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
rw : sin ((starRingEnd ℂ : (a : ℂ) → ℂ) x) * I = HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) I
rw₁ :
  sinh (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) I) =
    HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) I
rw₂ :
  sinh (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)) =
    HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)
rw₃ :
  sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) (x * -I)) =
    HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)
rw₄ : sinh ((starRingEnd ℂ : (a : ℂ) → ℂ) (x * -I)) = (starRingEnd ℂ : (a : ℂ) → ℂ) (sin x * -I)
rw₅ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sinh (x * -I)) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x * -I) : ℂ)
rw₆ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sinh (-(x * I))) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x * -I) : ℂ)
rw₇ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-sinh (x * I)) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x * -I) : ℂ)
rw₈ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-(sin x * I)) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x * -I) : ℂ)
rw₉ rw₁₀ :
  Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-(sin x * I)) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-(sin x * I)) : ℂ)
⊢ sin ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (sin x)

Tactic:
rw [← mul_left_inj' I_ne_zero, ← sinh_mul_I, ← conj_neg_I, ← map_mul, ← map_mul,
    sinh_conj, mul_neg, sinh_neg, sinh_mul_I, mul_neg]

Premises used: Complex.sinh_conj, Complex.sinh_neg, Complex.I_ne_zero, map_mul, mul_left_inj', Complex.conj_neg_I, Complex.sinh_mul_I, mul_neg
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : sin ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑x : ℂ)) = sin (↑x : ℂ)
rw₁ rw₂ : sin (↑x : ℂ) = sin (↑x : ℂ)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (sin (↑x : ℂ)) = sin (↑x : ℂ)

Tactic:
rw [← sin_conj, conj_ofReal]

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

Tactic:
ofReal_sin_ofReal_re _

Premises used: Complex.ofReal_sin_ofReal_re, Real.sin
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : (↑(sin (↑x : ℂ)).re : ℂ).im = 0
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ (sin (↑x : ℂ)).im = 0

Tactic:
rw [← ofReal_sin_ofReal_re, ofReal_im]

Premises used: Complex.ofReal_sin_ofReal_re, Complex.ofReal_im
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (sin (↑x : ℂ)).re = Real.sin x

Tactic:
rfl

Premises used: Real.sin, rfl
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
rw : cosh (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) I) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cos x)
rw₁ :
  cosh (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (-I) : ℂ)) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (cos x)
rw₂ : cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) (x * -I)) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cos x)
rw₃ : cosh ((starRingEnd ℂ : (a : ℂ) → ℂ) (x * -I)) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cosh (x * I))
rw₄ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cosh (x * -I)) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cosh (x * I)) : ℂ)
rw₅ :
  Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cosh (-(x * I))) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cosh (x * I)) : ℂ)
rw₆ rw₇ :
  Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cosh (x * I)) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cosh (x * I)) : ℂ)
⊢ cos ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (cos x)

Tactic:
rw [← cosh_mul_I, ← conj_neg_I, ← map_mul, ← cosh_mul_I, cosh_conj, mul_neg, cosh_neg]

Premises used: Complex.cosh_conj, map_mul, Complex.cosh_neg, Complex.conj_neg_I, Complex.cosh_mul_I, mul_neg
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : cos ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑x : ℂ)) = cos (↑x : ℂ)
rw₁ rw₂ : cos (↑x : ℂ) = cos (↑x : ℂ)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (cos (↑x : ℂ)) = cos (↑x : ℂ)

Tactic:
rw [← cos_conj, conj_ofReal]

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

Tactic:
ofReal_cos_ofReal_re _

Premises used: Real.cos, Complex.ofReal_cos_ofReal_re
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : (↑(cos (↑x : ℂ)).re : ℂ).im = 0
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ (cos (↑x : ℂ)).im = 0

Tactic:
rw [← ofReal_cos_ofReal_re, ofReal_im]

Premises used: Complex.ofReal_cos_ofReal_re, Complex.ofReal_im
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (cos (↑x : ℂ)).re = Real.cos x

Tactic:
rfl

Premises used: Real.cos, rfl
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
⊢ tan 0 = 0

Tactic:
simp [tan]

Premises used: Complex.tan
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
⊢ tan x = sin x / cos x

Tactic:
rfl

Premises used: Complex.tan, rfl
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
⊢ x.cot = cos x / sin x

Tactic:
rfl

Premises used: Complex.cot, rfl
-- 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₀, Complex.tan_eq_sin_div_cos
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
⊢ (tan x)⁻¹ = x.cot

Tactic:
inv_div ..

Premises used: Complex.cot, Complex.tan, inv_div
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
⊢ x.cot⁻¹ = tan x

Tactic:
inv_div ..

Premises used: Complex.cot, Complex.tan, inv_div
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
⊢ tan (-x) = -tan x

Tactic:
simp [tan, neg_div]

Premises used: neg_div, Complex.tan
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
rw :
  sin ((starRingEnd ℂ : (a : ℂ) → ℂ) x) / cos ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (tan x)
rw₁ :
  HDiv.hDiv (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) (cos ((starRingEnd ℂ : (a : ℂ) → ℂ) x)) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (tan x)
rw₂ :
  HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cos x) : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) (tan x)
rw₃ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x / cos x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (tan x) : ℂ)
rw₄ rw₅ :
  Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x / cos x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x / cos x) : ℂ)
⊢ tan ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (tan x)

Tactic:
rw [tan, sin_conj, cos_conj, ← map_div₀, tan]

Premises used: Complex.cos_conj, Complex.sin_conj, map_div₀, Complex.tan
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
rw : cos ((starRingEnd ℂ : (a : ℂ) → ℂ) x) / sin ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) x.cot
rw₁ :
  HDiv.hDiv (β := ℂ) (cos ((starRingEnd ℂ : (a : ℂ) → ℂ) x)) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) x.cot
rw₂ :
  HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cos x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) x.cot
rw₃ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cos x / sin x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x.cot : ℂ)
rw₄ rw₅ :
  Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cos x / sin x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cos x / sin x) : ℂ)
⊢ cot ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) x.cot

Tactic:
rw [cot, sin_conj, cos_conj, ← map_div₀, cot]

Premises used: Complex.cos_conj, Complex.sin_conj, Complex.cot, map_div₀
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : tan ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑x : ℂ)) = tan (↑x : ℂ)
rw₁ rw₂ : tan (↑x : ℂ) = tan (↑x : ℂ)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (tan (↑x : ℂ)) = tan (↑x : ℂ)

Tactic:
rw [← tan_conj, conj_ofReal]

Premises used: Complex.conj_ofReal, Complex.tan_conj
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : cot ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑x : ℂ)) = (↑x : ℂ).cot
rw₁ rw₂ : (↑x : ℂ).cot = (↑x : ℂ).cot
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (↑x : ℂ).cot = (↑x : ℂ).cot

Tactic:
rw [← cot_conj, conj_ofReal]

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

Tactic:
ofReal_tan_ofReal_re _

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

Tactic:
ofReal_cot_ofReal_re _

Premises used: Complex.ofReal_cot_ofReal_re, Real.cot
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
rw : (↑(tan (↑x : ℂ)).re : ℂ).im = 0
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ (tan (↑x : ℂ)).im = 0

Tactic:
rw [← ofReal_tan_ofReal_re, ofReal_im]

Premises used: Complex.ofReal_tan_ofReal_re, Complex.ofReal_im
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (tan (↑x : ℂ)).re = Real.tan x

Tactic:
rfl

Premises used: rfl, Real.tan
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
rw : cos x + sin x * I = cosh (x * I) + sinh (x * I)
rw₁ : cos x + sin x * I = cosh (x * I) + sin x * I
rw₂ rw₃ : cos x + sin x * I = cos x + sin x * I
⊢ cos x + sin x * I = cexp (x * I)

Tactic:
rw [← cosh_add_sinh, sinh_mul_I, cosh_mul_I]

Premises used: Complex.sinh_mul_I, Complex.cosh_mul_I, Complex.cosh_add_sinh
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
rw : cos x - sin x * I = cexp (-(x * I))
rw₁ : cos x - sin x * I = cosh (x * I) - sinh (x * I)
rw₂ : cos x - sin x * I = cosh (x * I) - sin x * I
rw₃ rw₄ : cos x - sin x * I = cos x - sin x * I
⊢ cos x - sin x * I = cexp (-x * I)

Tactic:
rw [neg_mul, ← cosh_sub_sinh, sinh_mul_I, cosh_mul_I]

Premises used: neg_mul, Complex.sinh_mul_I, Complex.cosh_mul_I, Complex.cosh_sub_sinh
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
rw :
  HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 =
    HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sinh (x * I)) 2
rw₁ :
  HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 =
    HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sin x * I) 2
rw₂ :
  HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 =
    HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sin x) 2 * HPow.hPow (β := ℕ) I 2
rw₃ :
  HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 =
    HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sin x) 2 * -1
rw₄ :
  HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 =
    HPow.hPow (β := ℕ) (cos x) 2 - -HPow.hPow (β := ℕ) (sin x) 2
rw₅ :
  HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 =
    HPow.hPow (β := ℕ) (cos x) 2 + HPow.hPow (β := ℕ) (sin x) 2
rw₆ rw₇ :
  HPow.hPow (β := ℕ) (cos x) 2 + HPow.hPow (β := ℕ) (sin x) 2 =
    HPow.hPow (β := ℕ) (cos x) 2 + HPow.hPow (β := ℕ) (sin x) 2
⊢ HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 =
    HPow.hPow (β := ℕ) (cosh (x * I)) 2 - HPow.hPow (β := ℕ) (sinh (x * I)) 2

Tactic:
rw [cosh_mul_I, sinh_mul_I, mul_pow, I_sq, mul_neg_one, sub_neg_eq_add, add_comm]

Premises used: add_comm, Complex.I_sq, mul_neg_one, mul_pow, Complex.sinh_mul_I, Complex.cosh_mul_I, sub_neg_eq_add
-- 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, Complex.sin_sq_add_cos_sq
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
rw : cos (x + x) = HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sin x) 2
rw₁ : cos x * cos x - sin x * sin x = HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sin x) 2
rw₂ : HPow.hPow (β := ℕ) (cos x) 2 - sin x * sin x = HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sin x) 2
rw₃ rw₄ :
  HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sin x) 2 =
    HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sin x) 2
⊢ cos (2 * x) = HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sin x) 2

Tactic:
rw [two_mul, cos_add, ← sq, ← sq]

Premises used: two_mul, sq, Complex.cos_add
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
rw : HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sin x) 2 = 2 * HPow.hPow (β := ℕ) (cos x) 2 - 1
rw₁ : HPow.hPow (β := ℕ) (cos x) 2 - (1 - HPow.hPow (β := ℕ) (cos x) 2) = 2 * HPow.hPow (β := ℕ) (cos x) 2 - 1
rw₂ : HPow.hPow (β := ℕ) (cos x) 2 - 1 + HPow.hPow (β := ℕ) (cos x) 2 = 2 * HPow.hPow (β := ℕ) (cos x) 2 - 1
rw₃ : HPow.hPow (β := ℕ) (cos x) 2 + HPow.hPow (β := ℕ) (cos x) 2 - 1 = 2 * HPow.hPow (β := ℕ) (cos x) 2 - 1
rw₄ rw₅ :
  HPow.hPow (β := ℕ) (cos x) 2 + HPow.hPow (β := ℕ) (cos x) 2 - 1 =
    HPow.hPow (β := ℕ) (cos x) 2 + HPow.hPow (β := ℕ) (cos x) 2 - 1
⊢ cos (2 * x) = 2 * HPow.hPow (β := ℕ) (cos x) 2 - 1

Tactic:
rw [cos_two_mul', eq_sub_iff_add_eq.2 (sin_sq_add_cos_sq x), ← sub_add, sub_add_eq_add_sub,
    two_mul]

Premises used: sub_add, Iff.mpr, eq_sub_iff_add_eq, two_mul, Complex.cos_two_mul', Complex.sin_sq_add_cos_sq, sub_add_eq_add_sub
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
⊢ cos (2 * x) = 1 - 2 * HPow.hPow (β := ℕ) (sin x) 2

Tactic:
grind [cos_two_mul, sin_sq_add_cos_sq]

Premises used: Complex.cos_two_mul, Complex.sin_sq_add_cos_sq
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
rw : sin (x + x) = 2 * sin x * cos x
rw₁ : sin x * cos x + cos x * sin x = 2 * sin x * cos x
rw₂ : sin x * cos x + cos x * sin x = (sin x + sin x) * cos x
rw₃ : sin x * cos x + cos x * sin x = sin x * cos x + sin x * cos x
rw₄ rw₅ : cos x * sin x + cos x * sin x = cos x * sin x + cos x * sin x
⊢ sin (2 * x) = 2 * sin x * cos x

Tactic:
rw [two_mul, sin_add, two_mul, add_mul, mul_comm]

Premises used: add_mul, two_mul, Complex.sin_add, mul_comm
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
⊢ HPow.hPow (β := ℕ) (cos x) 2 = 1 / 2 + cos (2 * x) / 2

Tactic:
simp [cos_two_mul, ← add_div, mul_div_cancel_left₀, -one_div]

Premises used: Complex.cos_two_mul, mul_div_cancel_left₀, one_div, add_div
-- 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, Complex.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 (β := ℕ) (cos x) 2
rw₁ rw₂ : HPow.hPow (β := ℕ) (sin x) 2 = HPow.hPow (β := ℕ) (sin x) 2
⊢ HPow.hPow (β := ℕ) (sin x) 2 = 1 - HPow.hPow (β := ℕ) (cos x) 2

Tactic:
rw [← sin_sq_add_cos_sq x, add_sub_cancel_right]

Premises used: Complex.sin_sq_add_cos_sq, add_sub_cancel_right
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
h : cos x ≠ 0
rw : HPow.hPow (β := ℕ) (tan x * cos x) 2 + HPow.hPow (β := ℕ) (cos x) 2
| 1

Tactic:
rw [← sin_sq_add_cos_sq x, ← tan_mul_cos h]

Premises used: Complex.tan_mul_cos, Complex.sin_sq_add_cos_sq
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
h : cos x ≠ 0
conv_rhs :
  (1 + HPow.hPow (β := ℕ) (tan x) 2) * HPow.hPow (β := ℕ) (cos x) 2 =
    HPow.hPow (β := ℕ) (tan x * cos x) 2 + HPow.hPow (β := ℕ) (cos x) 2
⊢ (1 + HPow.hPow (β := ℕ) (tan x) 2) * HPow.hPow (β := ℕ) (cos x) 2 = 1

Tactic:
conv_rhs => rw [← sin_sq_add_cos_sq x, ← tan_mul_cos h]

Premises used: Complex.tan_mul_cos, Complex.sin_sq_add_cos_sq
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
h : cos x ≠ 0
⊢ (1 + HPow.hPow (β := ℕ) (tan x) 2) * HPow.hPow (β := ℕ) (cos x) 2 =
    HPow.hPow (β := ℕ) (tan x * cos x) 2 + HPow.hPow (β := ℕ) (cos x) 2

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
hx : cos x ≠ 0
rw : (1 + HPow.hPow (β := ℕ) (sin x) 2 / HPow.hPow (β := ℕ) (cos x) 2)⁻¹ = HPow.hPow (β := ℕ) (cos x) 2
⊢ (1 + HPow.hPow (β := ℕ) (tan x) 2)⁻¹ = HPow.hPow (β := ℕ) (cos x) 2

Tactic:
rw [tan_eq_sin_div_cos, div_pow]

Premises used: Complex.tan_eq_sin_div_cos, div_pow