awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℝ
⊢ (↑(Real.tanh x) : ℂ) = tanh (↑x : ℂ)

Tactic:
ofReal_tanh_ofReal_re _

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

Tactic:
rw [← ofReal_tanh_ofReal_re, ofReal_im]

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

Tactic:
rfl

Premises used: Real.tanh, rfl
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
rw : 2 * (cosh x + sinh x) = 2 * cexp x
rw₁ : 2 * cosh x + 2 * sinh x = 2 * cexp x
rw₂ : cexp x + cexp (-x) + 2 * sinh x = 2 * cexp x
rw₃ : cexp x + cexp (-x) + (cexp x - cexp (-x)) = 2 * cexp x
rw₄ : cexp x + cexp x = 2 * cexp x
rw₅ rw₆ : cexp x + cexp x = cexp x + cexp x
⊢ cosh x + sinh x = cexp x

Tactic:
rw [← mul_right_inj' (two_ne_zero' ℂ), mul_add, two_cosh, two_sinh, add_add_sub_cancel, two_mul]

Premises used: Complex.two_sinh, two_mul, add_add_sub_cancel, Complex.two_cosh, two_ne_zero', mul_add, mul_right_inj', Complex
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
rw : cosh x + sinh x = cexp x
rw₁ rw₂ : cexp x = cexp x
⊢ sinh x + cosh x = cexp x

Tactic:
rw [add_comm, cosh_add_sinh]

Premises used: add_comm, Complex.cosh_add_sinh
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
⊢ cexp x - cosh x = sinh x

Tactic:
sub_eq_iff_eq_add.2 (sinh_add_cosh x).symm

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

Tactic:
sub_eq_iff_eq_add.2 (cosh_add_sinh x).symm

Premises used: Iff.mpr, sub_eq_iff_eq_add, Eq.symm, Complex.cosh_add_sinh
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
rw : 2 * (cosh x - sinh x) = 2 * cexp (-x)
rw₁ : 2 * cosh x - 2 * sinh x = 2 * cexp (-x)
rw₂ : cexp x + cexp (-x) - 2 * sinh x = 2 * cexp (-x)
rw₃ : cexp x + cexp (-x) - (cexp x - cexp (-x)) = 2 * cexp (-x)
rw₄ : cexp (-x) + cexp (-x) = 2 * cexp (-x)
rw₅ rw₆ : cexp (-x) + cexp (-x) = cexp (-x) + cexp (-x)
⊢ cosh x - sinh x = cexp (-x)

Tactic:
rw [← mul_right_inj' (two_ne_zero' ℂ), mul_sub, two_cosh, two_sinh, add_sub_sub_cancel, two_mul]

Premises used: mul_sub, Complex.two_sinh, add_sub_sub_cancel, two_mul, Complex.two_cosh, two_ne_zero', mul_right_inj', Complex
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
rw : -(cosh x - sinh x) = -cexp (-x)
rw₁ rw₂ : -cexp (-x) = -cexp (-x)
⊢ sinh x - cosh x = -cexp (-x)

Tactic:
rw [← neg_sub, cosh_sub_sinh]

Premises used: neg_sub, Complex.cosh_sub_sinh
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
rw : (cosh x + sinh x) * (cosh x - sinh x) = 1
rw₁ : cexp x * (cosh x - sinh x) = 1
rw₂ : cexp x * cexp (-x) = 1
rw₃ : cexp (x + -x) = 1
rw₄ : cexp 0 = 1
rw₅ rw₆ : Eq (α := ℂ) 1 1
⊢ HPow.hPow (β := ℕ) (cosh x) 2 - HPow.hPow (β := ℕ) (sinh x) 2 = 1

Tactic:
rw [sq_sub_sq, cosh_add_sinh, cosh_sub_sinh, ← exp_add, add_neg_cancel, exp_zero]

Premises used: add_neg_cancel, Complex.exp_add, Complex.exp_zero, sq_sub_sq, Complex.cosh_sub_sinh, Complex.cosh_add_sinh
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
rw :
  HPow.hPow (β := ℕ) (cosh x) 2 =
    HPow.hPow (β := ℕ) (sinh x) 2 + (HPow.hPow (β := ℕ) (cosh x) 2 - HPow.hPow (β := ℕ) (sinh x) 2)
⊢ HPow.hPow (β := ℕ) (cosh x) 2 = HPow.hPow (β := ℕ) (sinh x) 2 + 1

Tactic:
rw [← cosh_sq_sub_sinh_sq x]

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

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

Tactic:
rw [← cosh_sq_sub_sinh_sq x]

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

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
rw : cosh (x + x) = HPow.hPow (β := ℕ) (cosh x) 2 + HPow.hPow (β := ℕ) (sinh x) 2
rw₁ : cosh x * cosh x + sinh x * sinh x = HPow.hPow (β := ℕ) (cosh x) 2 + HPow.hPow (β := ℕ) (sinh x) 2
rw₂ : cosh x * cosh x + sinh x * sinh x = cosh x * cosh x + HPow.hPow (β := ℕ) (sinh x) 2
rw₃ rw₄ : cosh x * cosh x + sinh x * sinh x = cosh x * cosh x + sinh x * sinh x
⊢ cosh (2 * x) = HPow.hPow (β := ℕ) (cosh x) 2 + HPow.hPow (β := ℕ) (sinh x) 2

Tactic:
rw [two_mul, cosh_add, sq, sq]

Premises used: two_mul, sq, Complex.cosh_add
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
rw : sinh x * cosh x + cosh x * sinh x = 2 * sinh x * cosh x
⊢ sinh (2 * x) = 2 * sinh x * cosh x

Tactic:
rw [two_mul, sinh_add]

Premises used: two_mul, Complex.sinh_add
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
⊢ sinh x * cosh x + cosh x * sinh x = 2 * sinh x * cosh x

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
⊢ x + 2 * x = 3 * x

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
⊢ x + 2 * x = 3 * x

Tactic:
have h1 : x + 2 * x = 3 * x := by ring
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
h1 : x + 2 * x = 3 * x
rw : cosh x * cosh (2 * x) + sinh x * sinh (2 * x) = 4 * HPow.hPow (β := ℕ) (cosh x) 3 - 3 * cosh x
⊢ cosh (3 * x) = 4 * HPow.hPow (β := ℕ) (cosh x) 3 - 3 * cosh x

Tactic:
rw [← h1, cosh_add x (2 * x)]

Premises used: HMul.hMul, Complex.cosh_add, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
h1 : x + 2 * x = 3 * x
simp :
  cosh x * (HPow.hPow (β := ℕ) (cosh x) 2 + HPow.hPow (β := ℕ) (sinh x) 2) + sinh x * (2 * sinh x * cosh x) =
    4 * HPow.hPow (β := ℕ) (cosh x) 3 - 3 * cosh x
⊢ cosh x * cosh (2 * x) + sinh x * sinh (2 * x) = 4 * HPow.hPow (β := ℕ) (cosh x) 3 - 3 * cosh x

Tactic:
simp only [cosh_two_mul, sinh_two_mul]

Premises used: Complex.sinh_two_mul, Complex.cosh_two_mul
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ sinh x * (2 * sinh x * cosh x) = 2 * cosh x * HPow.hPow (β := ℕ) (sinh x) 2

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ sinh x * (2 * sinh x * cosh x) = 2 * cosh x * HPow.hPow (β := ℕ) (sinh x) 2

Tactic:
have h2 : sinh x * (2 * sinh x * cosh x) = 2 * cosh x * sinh x ^ 2 := by ring
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
h1 : x + 2 * x = 3 * x
h2 : sinh x * (2 * sinh x * cosh x) = 2 * cosh x * HPow.hPow (β := ℕ) (sinh x) 2
rw :
  cosh x * (HPow.hPow (β := ℕ) (cosh x) 2 + (HPow.hPow (β := ℕ) (cosh x) 2 - 1)) +
      2 * cosh x * (HPow.hPow (β := ℕ) (cosh x) 2 - 1) =
    4 * HPow.hPow (β := ℕ) (cosh x) 3 - 3 * cosh x
⊢ cosh x * (HPow.hPow (β := ℕ) (cosh x) 2 + HPow.hPow (β := ℕ) (sinh x) 2) + sinh x * (2 * sinh x * cosh x) =
    4 * HPow.hPow (β := ℕ) (cosh x) 3 - 3 * cosh x

Tactic:
rw [h2, sinh_sq]

Premises used: Complex.sinh_sq
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
h1 : x + 2 * x = 3 * x
h2 : sinh x * (2 * sinh x * cosh x) = 2 * cosh x * HPow.hPow (β := ℕ) (sinh x) 2
⊢ cosh x * (HPow.hPow (β := ℕ) (cosh x) 2 + (HPow.hPow (β := ℕ) (cosh x) 2 - 1)) +
      2 * cosh x * (HPow.hPow (β := ℕ) (cosh x) 2 - 1) =
    4 * HPow.hPow (β := ℕ) (cosh x) 3 - 3 * cosh x

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
h1 : x + 2 * x = 3 * x
rw : sinh x * cosh (2 * x) + cosh x * sinh (2 * x) = 4 * HPow.hPow (β := ℕ) (sinh x) 3 + 3 * sinh x
⊢ sinh (3 * x) = 4 * HPow.hPow (β := ℕ) (sinh x) 3 + 3 * sinh x

Tactic:
rw [← h1, sinh_add x (2 * x)]

Premises used: HMul.hMul, Complex.sinh_add, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
h1 : x + 2 * x = 3 * x
simp :
  sinh x * (HPow.hPow (β := ℕ) (cosh x) 2 + HPow.hPow (β := ℕ) (sinh x) 2) + cosh x * (2 * sinh x * cosh x) =
    4 * HPow.hPow (β := ℕ) (sinh x) 3 + 3 * sinh x
⊢ sinh x * cosh (2 * x) + cosh x * sinh (2 * x) = 4 * HPow.hPow (β := ℕ) (sinh x) 3 + 3 * sinh x

Tactic:
simp only [cosh_two_mul, sinh_two_mul]

Premises used: Complex.sinh_two_mul, Complex.cosh_two_mul
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ cosh x * (2 * sinh x * cosh x) = 2 * sinh x * HPow.hPow (β := ℕ) (cosh x) 2

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ cosh x * (2 * sinh x * cosh x) = 2 * sinh x * HPow.hPow (β := ℕ) (cosh x) 2

Tactic:
have h2 : cosh x * (2 * sinh x * cosh x) = 2 * sinh x * cosh x ^ 2 := by ring
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
h1 : x + 2 * x = 3 * x
h2 : cosh x * (2 * sinh x * cosh x) = 2 * sinh x * HPow.hPow (β := ℕ) (cosh x) 2
rw :
  sinh x * (HPow.hPow (β := ℕ) (sinh x) 2 + 1 + HPow.hPow (β := ℕ) (sinh x) 2) +
      2 * sinh x * (HPow.hPow (β := ℕ) (sinh x) 2 + 1) =
    4 * HPow.hPow (β := ℕ) (sinh x) 3 + 3 * sinh x
⊢ sinh x * (HPow.hPow (β := ℕ) (cosh x) 2 + HPow.hPow (β := ℕ) (sinh x) 2) + cosh x * (2 * sinh x * cosh x) =
    4 * HPow.hPow (β := ℕ) (sinh x) 3 + 3 * sinh x

Tactic:
rw [h2, cosh_sq]

Premises used: Complex.cosh_sq
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
h1 : x + 2 * x = 3 * x
h2 : cosh x * (2 * sinh x * cosh x) = 2 * sinh x * HPow.hPow (β := ℕ) (cosh x) 2
⊢ sinh x * (HPow.hPow (β := ℕ) (sinh x) 2 + 1 + HPow.hPow (β := ℕ) (sinh x) 2) +
      2 * sinh x * (HPow.hPow (β := ℕ) (sinh x) 2 + 1) =
    4 * HPow.hPow (β := ℕ) (sinh x) 3 + 3 * sinh x

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

Tactic:
simp [sin]

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

Tactic:
simp [sin, sub_eq_add_neg, exp_neg, (neg_div _ _).symm, add_mul]

Premises used: add_mul, neg_div, Complex.sin, sub_eq_add_neg, Complex.exp_neg, Eq.symm
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
⊢ 2 * sin x = (cexp (-x * I) - cexp (x * I)) * I

Tactic:
mul_div_cancel₀ _ two_ne_zero

Premises used: Complex.sin, mul_div_cancel₀, two_ne_zero
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
⊢ 2 * cos x = cexp (x * I) + cexp (-x * I)

Tactic:
mul_div_cancel₀ _ two_ne_zero

Premises used: Complex.cos, mul_div_cancel₀, two_ne_zero
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
rw : 2 * sinh (x * I) = 2 * (sin x * I)
rw₁ : cexp (x * I) - cexp (-(x * I)) = 2 * (sin x * I)
rw₂ : cexp (x * I) - cexp (-(x * I)) = 2 * sin x * I
rw₃ : cexp (x * I) - cexp (-(x * I)) = (cexp (-x * I) - cexp (x * I)) * I * I
rw₄ : cexp (x * I) - cexp (-(x * I)) = (cexp (-x * I) - cexp (x * I)) * (I * I)
rw₅ : cexp (x * I) - cexp (-(x * I)) = (cexp (-x * I) - cexp (x * I)) * -1
rw₆ : cexp (x * I) - cexp (-(x * I)) = -(cexp (-x * I) - cexp (x * I))
rw₇ : cexp (x * I) - cexp (-(x * I)) = cexp (x * I) - cexp (-x * I)
rw₈ rw₉ : cexp (x * I) - cexp (-x * I) = cexp (x * I) - cexp (-x * I)
⊢ sinh (x * I) = sin x * I

Tactic:
rw [← mul_right_inj' (two_ne_zero' ℂ), two_sinh, ← mul_assoc, two_sin, mul_assoc, I_mul_I,
    mul_neg_one, neg_sub, neg_mul_eq_neg_mul]

Premises used: neg_sub, Complex.two_sinh, mul_assoc, two_ne_zero', Complex.I_mul_I, neg_mul_eq_neg_mul, mul_right_inj', mul_neg_one, Complex, Complex.two_sin
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
rw : 2 * cosh (x * I) = 2 * cos x
rw₁ : cexp (x * I) + cexp (-(x * I)) = 2 * cos x
rw₂ : cexp (x * I) + cexp (-(x * I)) = cexp (x * I) + cexp (-x * I)
rw₃ rw₄ : cexp (x * I) + cexp (-x * I) = cexp (x * I) + cexp (-x * I)
⊢ cosh (x * I) = cos x

Tactic:
rw [← mul_right_inj' (two_ne_zero' ℂ), two_cosh, two_cos, neg_mul_eq_neg_mul]

Premises used: Complex.two_cosh, two_ne_zero', neg_mul_eq_neg_mul, mul_right_inj', Complex, Complex.two_cos
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
rw : sinh (x * I) / cosh (x * I) = tan x * I
rw₁ : sinh (x * I) / cos x = tan x * I
rw₂ : sin x * I / cos x = tan x * I
rw₃ : sin x / cos x * I = tan x * I
rw₄ rw₅ : sin x / cos x * I = sin x / cos x * I
⊢ tanh (x * I) = tan x * I

Tactic:
rw [tanh_eq_sinh_div_cosh, cosh_mul_I, sinh_mul_I, mul_div_right_comm, tan]

Premises used: Complex.tanh_eq_sinh_div_cosh, mul_div_right_comm, Complex.tan, Complex.sinh_mul_I, Complex.cosh_mul_I
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
rw : cosh (x * I * I) = cosh x
⊢ cos (x * I) = cosh x

Tactic:
rw [← cosh_mul_I]

Premises used: Complex.cosh_mul_I
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
ring_nf : cosh (x * HPow.hPow (β := ℕ) I 2) = cosh x
⊢ cosh (x * I * I) = cosh x

Tactic:
ring_nf
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
⊢ cosh (x * HPow.hPow (β := ℕ) I 2) = cosh x

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
rw : sinh (x * I * I) = -sinh x
⊢ I * sin (x * I) = -sinh x

Tactic:
rw [mul_comm, ← sinh_mul_I]

Premises used: mul_comm, Complex.sinh_mul_I
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
ring_nf : sinh (x * HPow.hPow (β := ℕ) I 2) = -sinh x
⊢ sinh (x * I * I) = -sinh x

Tactic:
ring_nf
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
⊢ sinh (x * HPow.hPow (β := ℕ) I 2) = -sinh x

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
⊢ I * sin (x * I) = -sinh x

Tactic:
have h : I * sin (x * I) = -sinh x := by
    rw [mul_comm, ← sinh_mul_I]
    ring_nf
    simp
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
h : I * sin (x * I) = -sinh x
rw : sin (x * I) = -(I * sin (x * I)) * I
⊢ sin (x * I) = sinh x * I

Tactic:
rw [← neg_neg (sinh x), ← h]

Premises used: Complex.sinh, neg_neg
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
h : I * sin (x * I) = -sinh x
a : (sin (x * I)).re = (-(I * sin (x * I)) * I).re
a₁ : (sin (x * I)).im = (-(I * sin (x * I)) * I).im
⊢ sin (x * I) = -(I * sin (x * I)) * I

Tactic:
apply Complex.ext

Premises used: Complex.ext
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
h : I * sin (x * I) = -sinh x
⊢ (sin (x * I)).re = (-(I * sin (x * I)) * I).re

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
h : I * sin (x * I) = -sinh x
⊢ (sin (x * I)).im = (-(I * sin (x * I)) * I).im

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x : ℂ
rw : sin (x * I) / cos (x * I) = tanh x * I
rw₁ : sinh x * I / cos (x * I) = tanh x * I
rw₂ : sinh x * I / cosh x = tanh x * I
rw₃ : sinh x / cosh x * I = tanh x * I
rw₄ rw₅ : sinh x / cosh x * I = sinh x / cosh x * I
⊢ tan (x * I) = tanh x * I

Tactic:
rw [tan, sin_mul_I, cos_mul_I, mul_div_right_comm, tanh_eq_sinh_div_cosh]

Premises used: Complex.cos_mul_I, Complex.tanh_eq_sinh_div_cosh, mul_div_right_comm, Complex.tan, Complex.sin_mul_I
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℂ
rw : sin (x + y) * I = (sin x * cos y + cos x * sin y) * I
rw₁ : sinh ((x + y) * I) = (sin x * cos y + cos x * sin y) * I
rw₂ : sinh (x * I + y * I) = (sin x * cos y + cos x * sin y) * I
rw₃ : sinh (x * I + y * I) = sin x * cos y * I + cos x * sin y * I
rw₄ : sinh (x * I + y * I) = sin x * I * cos y + cos x * sin y * I
rw₅ : sinh (x * I + y * I) = sinh (x * I) * cos y + cos x * sin y * I
rw₆ : sinh (x * I + y * I) = sinh (x * I) * cos y + cos x * (sin y * I)
rw₇ : sinh (x * I + y * I) = sinh (x * I) * cos y + cos x * sinh (y * I)
rw₈ : sinh (x * I + y * I) = sinh (x * I) * cosh (y * I) + cos x * sinh (y * I)
rw₉ : sinh (x * I + y * I) = sinh (x * I) * cosh (y * I) + cosh (x * I) * sinh (y * I)
rw₁₀ rw₁₁ :
  sinh (x * I) * cosh (y * I) + cosh (x * I) * sinh (y * I) = sinh (x * I) * cosh (y * I) + cosh (x * I) * sinh (y * I)
⊢ sin (x + y) = sin x * cos y + cos x * sin y

Tactic:
rw [← mul_left_inj' I_ne_zero, ← sinh_mul_I, add_mul, add_mul, mul_right_comm, ← sinh_mul_I,
    mul_assoc, ← sinh_mul_I, ← cosh_mul_I, ← cosh_mul_I, sinh_add]

Premises used: add_mul, mul_assoc, Complex.I_ne_zero, Complex.sinh_add, mul_right_comm, mul_left_inj', Complex.sinh_mul_I, Complex.cosh_mul_I
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
⊢ cos 0 = 1

Tactic:
simp [cos]

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

Tactic:
simp [cos, exp_neg, add_comm]

Premises used: Complex.cos, Complex.exp_neg, add_comm
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℂ
rw : cosh ((x + y) * I) = cos x * cos y - sin x * sin y
rw₁ : cosh (x * I + y * I) = cos x * cos y - sin x * sin y
rw₂ : cosh (x * I) * cosh (y * I) + sinh (x * I) * sinh (y * I) = cos x * cos y - sin x * sin y
rw₃ : cos x * cosh (y * I) + sinh (x * I) * sinh (y * I) = cos x * cos y - sin x * sin y
rw₄ : cos x * cos y + sinh (x * I) * sinh (y * I) = cos x * cos y - sin x * sin y
rw₅ : cos x * cos y + sin x * I * sinh (y * I) = cos x * cos y - sin x * sin y
rw₆ : cos x * cos y + sin x * I * (sin y * I) = cos x * cos y - sin x * sin y
rw₇ : cos x * cos y + sin x * sin y * (I * I) = cos x * cos y - sin x * sin y
rw₈ : cos x * cos y + sin x * sin y * -1 = cos x * cos y - sin x * sin y
rw₉ : cos x * cos y + -(sin x * sin y) = cos x * cos y - sin x * sin y
rw₁₀ rw₁₁ : cos x * cos y + -(sin x * sin y) = cos x * cos y + -(sin x * sin y)
⊢ cos (x + y) = cos x * cos y - sin x * sin y

Tactic:
rw [← cosh_mul_I, add_mul, cosh_add, cosh_mul_I, cosh_mul_I, sinh_mul_I, sinh_mul_I,
    mul_mul_mul_comm, I_mul_I, mul_neg_one, sub_eq_add_neg]

Premises used: add_mul, mul_mul_mul_comm, sub_eq_add_neg, Complex.I_mul_I, Complex.cosh_add, mul_neg_one, Complex.sinh_mul_I, Complex.cosh_mul_I
-- 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, Complex.sin_add, Complex.cos_neg, Complex.sin_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, Complex.cos_add, Complex.cos_neg, Complex.sin_neg
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℂ
rw : sin x * cos (y * I) + cos x * sin (y * I) = sin x * cosh y + cos x * sinh y * I
rw₁ : sin x * cosh y + cos x * sin (y * I) = sin x * cosh y + cos x * sinh y * I
rw₂ : sin x * cosh y + cos x * (sinh y * I) = sin x * cosh y + cos x * sinh y * I
rw₃ rw₄ : sin x * cosh y + cos x * (sinh y * I) = sin x * cosh y + cos x * (sinh y * I)
⊢ sin (x + y * I) = sin x * cosh y + cos x * sinh y * I

Tactic:
rw [sin_add, cos_mul_I, sin_mul_I, mul_assoc]

Premises used: Complex.cos_mul_I, mul_assoc, Complex.sin_add, Complex.sin_mul_I
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
z : ℂ
⊢ sin ((↑z.re : ℂ) + (↑z.im : ℂ) * I) = sin (↑z.re : ℂ) * cosh (↑z.im : ℂ) + cos (↑z.re : ℂ) * sinh (↑z.im : ℂ) * I

Tactic:
sin_add_mul_I z.re z.im

Premises used: Complex.im, Complex.ofReal, Complex.re, Complex.sin_add_mul_I
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
z : ℂ
h : z = (↑z.re : ℂ) + (↑z.im : ℂ) * I
⊢ sin z = sin (↑z.re : ℂ) * cosh (↑z.im : ℂ) + cos (↑z.re : ℂ) * sinh (↑z.im : ℂ) * I

Tactic:
convert! sin_add_mul_I z.re z.im

Premises used: Complex.im, Complex.ofReal, Complex.re, Complex.sin_add_mul_I
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
z : ℂ
⊢ z = (↑z.re : ℂ) + (↑z.im : ℂ) * I

Tactic:
(re_add_im z).symm

Premises used: Complex.re_add_im, Eq.symm
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
z : ℂ
⊢ z = (↑z.re : ℂ) + (↑z.im : ℂ) * I

Tactic:
exact (re_add_im z).symm

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

Tactic:
rw [cos_add, cos_mul_I, sin_mul_I, mul_assoc]

Premises used: Complex.cos_mul_I, mul_assoc, Complex.cos_add, Complex.sin_mul_I
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
z : ℂ
⊢ cos ((↑z.re : ℂ) + (↑z.im : ℂ) * I) = cos (↑z.re : ℂ) * cosh (↑z.im : ℂ) - sin (↑z.re : ℂ) * sinh (↑z.im : ℂ) * I

Tactic:
cos_add_mul_I z.re z.im

Premises used: Complex.im, Complex.ofReal, Complex.re, Complex.cos_add_mul_I
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
z : ℂ
h : z = (↑z.re : ℂ) + (↑z.im : ℂ) * I
⊢ cos z = cos (↑z.re : ℂ) * cosh (↑z.im : ℂ) - sin (↑z.re : ℂ) * sinh (↑z.im : ℂ) * I

Tactic:
convert! cos_add_mul_I z.re z.im

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

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

Tactic:
have s2 := sin_sub ((x + y) / 2) ((x - y) / 2)
-- Module: Mathlib.Analysis.Complex.Trigonometric
Goal:
x y : ℂ
s1 : sin ((x + y) / 2 + (x - y) / 2) = sin ((x + y) / 2) * cos ((x - y) / 2) + cos ((x + y) / 2) * sin ((x - y) / 2)
s2 : sin ((x + y) / 2 - (x - y) / 2) = sin ((x + y) / 2) * cos ((x - y) / 2) - cos ((x + y) / 2) * sin ((x - y) / 2)
⊢ sin x = sin ((x + y) / 2) * cos ((x - y) / 2) + cos ((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 : sin ((x + y) / 2 + (x - y) / 2) = sin ((x + y) / 2) * cos ((x - y) / 2) + cos ((x + y) / 2) * sin ((x - y) / 2)
s2 : sin ((x + y) / 2 - (x - y) / 2) = sin ((x + y) / 2) * cos ((x - y) / 2) - cos ((x + y) / 2) * sin ((x - y) / 2)
s1₁ : sin x = sin ((x + y) / 2) * cos ((x - y) / 2) + cos ((x + y) / 2) * sin ((x - y) / 2)
⊢ sin ((x + y) / 2 - (x - y) / 2) = sin ((x + y) / 2) * cos ((x - y) / 2) - cos ((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 : sin x = sin ((x + y) / 2) * cos ((x - y) / 2) + cos ((x + y) / 2) * sin ((x - y) / 2)
s2 : sin ((x + y) / 2 - (x - y) / 2) = sin ((x + y) / 2) * cos ((x - y) / 2) - cos ((x + y) / 2) * sin ((x - y) / 2)
⊢ sin y = sin ((x + y) / 2) * cos ((x - y) / 2) - cos ((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 : 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)
rw :
  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)
⊢ sin x - sin y = 2 * sin ((x - y) / 2) * cos ((x + y) / 2)

Tactic:
rw [s1, s2]