awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
h : I * sin (x * I) = -sinh x
a : (sin (x * I)).re = (-(I * sin (x * I)) * I).re
⊢ sin (x * I) = -(I * sin (x * I)) * I
have a₁ : (sin (x * I)).im = (-(I * sin (x * I)) * I).im
Tactic: apply Complex.ext
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ tan (x * I) = tanh x * I
have rw : sin (x * I) / cos (x * I) = tanh x * I
Tactic: rw [tan, sin_mul_I, cos_mul_I, mul_div_right_comm, tanh_eq_sinh_div_cosh]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : sin (x * I) / cos (x * I) = tanh x * I
⊢ tan (x * I) = tanh x * I
have rw₁ : sinh x * I / cos (x * I) = tanh x * I
Tactic: rw [tan, sin_mul_I, cos_mul_I, mul_div_right_comm, tanh_eq_sinh_div_cosh]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : sin (x * I) / cos (x * I) = tanh x * I
rw₁ : sinh x * I / cos (x * I) = tanh x * I
⊢ tan (x * I) = tanh x * I
have rw₂ : sinh x * I / cosh x = tanh x * I
Tactic: rw [tan, sin_mul_I, cos_mul_I, mul_div_right_comm, tanh_eq_sinh_div_cosh]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ tan (x * I) = tanh x * I
have rw₃ : sinh x / cosh x * I = tanh x * I
Tactic: rw [tan, sin_mul_I, cos_mul_I, mul_div_right_comm, tanh_eq_sinh_div_cosh]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ tan (x * I) = tanh x * I
have rw₄ : sinh x / cosh x * I = sinh x / cosh x * I
Tactic: rw [tan, sin_mul_I, cos_mul_I, mul_div_right_comm, tanh_eq_sinh_div_cosh]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x y : ℂ
⊢ sin (x + y) = sin x * cos y + cos x * sin y
have rw : sin (x + y) * I = (sin x * cos y + cos x * sin y) * I
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x y : ℂ
rw : sin (x + y) * I = (sin x * cos y + cos x * sin y) * I
⊢ sin (x + y) = sin x * cos y + cos x * sin y
have rw₁ : sinh ((x + y) * I) = (sin x * cos y + cos x * sin y) * I
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ sin (x + y) = sin x * cos y + cos x * sin y
have rw₂ : sinh (x * I + y * I) = (sin x * cos y + cos x * sin y) * I
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ sin (x + y) = sin x * cos y + cos x * sin y
have rw₃ : sinh (x * I + y * I) = sin x * cos y * I + cos x * sin y * I
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ sin (x + y) = sin x * cos y + cos x * sin y
have rw₄ : sinh (x * I + y * I) = sin x * I * cos y + cos x * sin y * I
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ sin (x + y) = sin x * cos y + cos x * sin y
have rw₅ : sinh (x * I + y * I) = sinh (x * I) * cos y + cos x * sin y * I
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ sin (x + y) = sin x * cos y + cos x * sin y
have rw₆ : sinh (x * I + y * I) = sinh (x * I) * cos y + cos x * (sin y * I)
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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)
⊢ sin (x + y) = sin x * cos y + cos x * sin y
have rw₇ : sinh (x * I + y * I) = sinh (x * I) * cos y + cos x * sinh (y * I)
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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)
⊢ sin (x + y) = sin x * cos y + cos x * sin y
have rw₈ : sinh (x * I + y * I) = sinh (x * I) * cosh (y * I) + cos x * sinh (y * I)
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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)
⊢ sin (x + y) = sin x * cos y + cos x * sin y
have rw₉ : sinh (x * I + y * I) = sinh (x * I) * cosh (y * I) + cosh (x * I) * sinh (y * I)
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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)
⊢ sin (x + y) = sin x * cos y + cos x * sin y
have 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)
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x y : ℂ
⊢ cos (x + y) = cos x * cos y - sin x * sin y
have rw : cosh ((x + y) * I) = 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x y : ℂ
rw : cosh ((x + y) * I) = cos x * cos y - sin x * sin y
⊢ cos (x + y) = cos x * cos y - sin x * sin y
have rw₁ : cosh (x * I + y * I) = 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ cos (x + y) = cos x * cos y - sin x * sin y
have rw₂ : cosh (x * I) * cosh (y * I) + sinh (x * I) * sinh (y * I) = 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ cos (x + y) = cos x * cos y - sin x * sin y
have rw₃ : cos x * cosh (y * I) + sinh (x * I) * sinh (y * I) = 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ cos (x + y) = cos x * cos y - sin x * sin y
have rw₄ : cos x * cos y + sinh (x * I) * sinh (y * I) = 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ cos (x + y) = cos x * cos y - sin x * sin y
have rw₅ : cos x * cos y + sin x * I * sinh (y * I) = 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ cos (x + y) = cos x * cos y - sin x * sin y
have rw₆ : cos x * cos y + sin x * I * (sin y * I) = 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ cos (x + y) = cos x * cos y - sin x * sin y
have rw₇ : cos x * cos y + sin x * sin y * (I * I) = 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ cos (x + y) = cos x * cos y - sin x * sin y
have rw₈ : cos x * cos y + sin x * sin y * -1 = 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ cos (x + y) = cos x * cos y - sin x * sin y
have rw₉ : cos x * cos y + -(sin x * sin 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ cos (x + y) = cos x * cos y - sin x * sin y
have rw₁₀ : cos x * cos y + -(sin x * sin 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x y : ℂ
⊢ sin (x + y * I) = sin x * cosh y + cos x * sinh y * I
have rw : sin x * cos (y * I) + cos x * sin (y * I) = sin x * cosh y + cos x * sinh y * I
Tactic: rw [sin_add, cos_mul_I, sin_mul_I, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x y : ℂ
rw : sin x * cos (y * I) + cos x * sin (y * I) = sin x * cosh y + cos x * sinh y * I
⊢ sin (x + y * I) = sin x * cosh y + cos x * sinh y * I
have rw₁ : sin x * cosh y + cos x * sin (y * I) = sin x * cosh y + cos x * sinh y * I
Tactic: rw [sin_add, cos_mul_I, sin_mul_I, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ sin (x + y * I) = sin x * cosh y + cos x * sinh y * I
have rw₂ : sin x * cosh y + cos x * (sinh y * I) = sin x * cosh y + cos x * sinh y * I
Tactic: rw [sin_add, cos_mul_I, sin_mul_I, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ sin (x + y * I) = sin x * cosh y + cos x * sinh y * I
have rw₃ : sin x * cosh y + cos x * (sinh y * I) = sin x * cosh y + cos x * (sinh y * I)
Tactic: rw [sin_add, cos_mul_I, sin_mul_I, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
z : ℂ
⊢ sin z = sin (↑z.re : ℂ) * cosh (↑z.im : ℂ) + cos (↑z.re : ℂ) * sinh (↑z.im : ℂ) * I
have h : z = (↑z.re : ℂ) + (↑z.im : ℂ) * I
Tactic: convert! sin_add_mul_I z.re z.im
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x y : ℂ
⊢ cos (x + y * I) = cos x * cosh y - sin x * sinh y * I
have rw : cos x * cos (y * I) - sin x * sin (y * I) = cos x * cosh y - sin x * sinh y * I
Tactic: rw [cos_add, cos_mul_I, sin_mul_I, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x y : ℂ
rw : cos x * cos (y * I) - sin x * sin (y * I) = cos x * cosh y - sin x * sinh y * I
⊢ cos (x + y * I) = cos x * cosh y - sin x * sinh y * I
have rw₁ : cos x * cosh y - sin x * sin (y * I) = cos x * cosh y - sin x * sinh y * I
Tactic: rw [cos_add, cos_mul_I, sin_mul_I, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ cos (x + y * I) = cos x * cosh y - sin x * sinh y * I
have rw₂ : cos x * cosh y - sin x * (sinh y * I) = cos x * cosh y - sin x * sinh y * I
Tactic: rw [cos_add, cos_mul_I, sin_mul_I, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ cos (x + y * I) = cos x * cosh y - sin x * sinh y * I
have rw₃ : cos x * cosh y - sin x * (sinh y * I) = cos x * cosh y - sin x * (sinh y * I)
Tactic: rw [cos_add, cos_mul_I, sin_mul_I, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
z : ℂ
⊢ cos z = cos (↑z.re : ℂ) * cosh (↑z.im : ℂ) - sin (↑z.re : ℂ) * sinh (↑z.im : ℂ) * I
have h : z = (↑z.re : ℂ) + (↑z.im : ℂ) * I
Tactic: convert! cos_add_mul_I z.re z.im
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (hypothesis)
Goal:
x y : ℂ
⊢ sin x - sin y = 2 * sin ((x - y) / 2) * cos ((x + y) / 2)
have s1 : 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)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (hypothesis)
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 - sin y = 2 * sin ((x - y) / 2) * cos ((x + y) / 2)
have s2 : 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)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (hypothesis)
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 y = 2 * sin ((x - y) / 2) * cos ((x + y) / 2)
have s1₁ : 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
Cleared hypotheses: s1, s2
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (hypothesis)
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 x - sin y = 2 * sin ((x - y) / 2) * cos ((x + y) / 2)
have s2₁ : 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
Cleared hypotheses: s2
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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 - sin y = 2 * sin ((x - y) / 2) * cos ((x + y) / 2)
have 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)
Tactic: rw [s1, s2]