awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (cos (↑x : ℂ)) = cos (↑x : ℂ)
have rw : cos ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑x : ℂ)) = cos (↑x : ℂ)
Tactic: rw [← cos_conj, conj_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
rw : cos ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑x : ℂ)) = cos (↑x : ℂ)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (cos (↑x : ℂ)) = cos (↑x : ℂ)
have rw₁ : cos (↑x : ℂ) = cos (↑x : ℂ)
Tactic: rw [← cos_conj, conj_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ (cos (↑x : ℂ)).im = 0
have rw : (↑(cos (↑x : ℂ)).re : ℂ).im = 0
Tactic: rw [← ofReal_cos_ofReal_re, ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
rw : (↑(cos (↑x : ℂ)).re : ℂ).im = 0
⊢ (cos (↑x : ℂ)).im = 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [← ofReal_cos_ofReal_re, ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
hx : cos x ≠ 0
⊢ tan x * cos x = sin x
have rw : sin x / cos x * cos x = sin x
Tactic: rw [tan_eq_sin_div_cos, div_mul_cancel₀ _ hx]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
hx : cos x ≠ 0
rw : sin x / cos x * cos x = sin x
⊢ tan x * cos x = sin x
have rw₁ : sin x = sin x
Tactic: rw [tan_eq_sin_div_cos, div_mul_cancel₀ _ hx]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ tan ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (tan x)
have rw : sin ((starRingEnd ℂ : (a : ℂ) → ℂ) x) / cos ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (tan x)
Tactic: rw [tan, sin_conj, cos_conj, ← map_div₀, tan]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw :
  sin ((starRingEnd ℂ : (a : ℂ) → ℂ) x) / cos ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (tan x)
⊢ tan ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (tan x)
have rw₁ : HDiv.hDiv (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) (cos ((starRingEnd ℂ : (a : ℂ) → ℂ) x)) =
  (starRingEnd ℂ : (a : ℂ) → ℂ) (tan x)
Tactic: rw [tan, sin_conj, cos_conj, ← map_div₀, tan]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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)
⊢ tan ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (tan x)
have rw₂ : HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cos x) : ℂ) =
  (starRingEnd ℂ : (a : ℂ) → ℂ) (tan x)
Tactic: rw [tan, sin_conj, cos_conj, ← map_div₀, tan]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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)
⊢ tan ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (tan x)
have rw₃ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x / cos x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (tan x) : ℂ)
Tactic: rw [tan, sin_conj, cos_conj, ← map_div₀, tan]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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) : ℂ)
⊢ tan ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (tan x)
have rw₄ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x / cos x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x / cos x) : ℂ)
Tactic: rw [tan, sin_conj, cos_conj, ← map_div₀, tan]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ cot ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) x.cot
have rw : cos ((starRingEnd ℂ : (a : ℂ) → ℂ) x) / sin ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) x.cot
Tactic: rw [cot, sin_conj, cos_conj, ← map_div₀, cot]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : cos ((starRingEnd ℂ : (a : ℂ) → ℂ) x) / sin ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) x.cot
⊢ cot ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) x.cot
have rw₁ : HDiv.hDiv (β := ℂ) (cos ((starRingEnd ℂ : (a : ℂ) → ℂ) x)) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) =
  (starRingEnd ℂ : (a : ℂ) → ℂ) x.cot
Tactic: rw [cot, sin_conj, cos_conj, ← map_div₀, cot]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ cot ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) x.cot
have rw₂ : HDiv.hDiv (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cos x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (sin x) : ℂ) =
  (starRingEnd ℂ : (a : ℂ) → ℂ) x.cot
Tactic: rw [cot, sin_conj, cos_conj, ← map_div₀, cot]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ cot ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) x.cot
have rw₃ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cos x / sin x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x.cot : ℂ)
Tactic: rw [cot, sin_conj, cos_conj, ← map_div₀, cot]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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 : ℂ)
⊢ cot ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) x.cot
have rw₄ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cos x / sin x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cos x / sin x) : ℂ)
Tactic: rw [cot, sin_conj, cos_conj, ← map_div₀, cot]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (tan (↑x : ℂ)) = tan (↑x : ℂ)
have rw : tan ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑x : ℂ)) = tan (↑x : ℂ)
Tactic: rw [← tan_conj, conj_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
rw : tan ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑x : ℂ)) = tan (↑x : ℂ)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (tan (↑x : ℂ)) = tan (↑x : ℂ)
have rw₁ : tan (↑x : ℂ) = tan (↑x : ℂ)
Tactic: rw [← tan_conj, conj_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (↑x : ℂ).cot = (↑x : ℂ).cot
have rw : cot ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑x : ℂ)) = (↑x : ℂ).cot
Tactic: rw [← cot_conj, conj_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
rw : cot ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑x : ℂ)) = (↑x : ℂ).cot
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (↑x : ℂ).cot = (↑x : ℂ).cot
have rw₁ : (↑x : ℂ).cot = (↑x : ℂ).cot
Tactic: rw [← cot_conj, conj_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ (tan (↑x : ℂ)).im = 0
have rw : (↑(tan (↑x : ℂ)).re : ℂ).im = 0
Tactic: rw [← ofReal_tan_ofReal_re, ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
rw : (↑(tan (↑x : ℂ)).re : ℂ).im = 0
⊢ (tan (↑x : ℂ)).im = 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [← ofReal_tan_ofReal_re, ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ cos x + sin x * I = cexp (x * I)
have rw : cos x + sin x * I = cosh (x * I) + sinh (x * I)
Tactic: rw [← cosh_add_sinh, sinh_mul_I, cosh_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : cos x + sin x * I = cosh (x * I) + sinh (x * I)
⊢ cos x + sin x * I = cexp (x * I)
have rw₁ : cos x + sin x * I = cosh (x * I) + sin x * I
Tactic: rw [← cosh_add_sinh, sinh_mul_I, cosh_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ cos x + sin x * I = cexp (x * I)
have rw₂ : cos x + sin x * I = cos x + sin x * I
Tactic: rw [← cosh_add_sinh, sinh_mul_I, cosh_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ cos x - sin x * I = cexp (-x * I)
have rw : cos x - sin x * I = cexp (-(x * I))
Tactic: rw [neg_mul, ← cosh_sub_sinh, sinh_mul_I, cosh_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : cos x - sin x * I = cexp (-(x * I))
⊢ cos x - sin x * I = cexp (-x * I)
have rw₁ : cos x - sin x * I = cosh (x * I) - sinh (x * I)
Tactic: rw [neg_mul, ← cosh_sub_sinh, sinh_mul_I, cosh_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : cos x - sin x * I = cexp (-(x * I))
rw₁ : cos x - sin x * I = cosh (x * I) - sinh (x * I)
⊢ cos x - sin x * I = cexp (-x * I)
have rw₂ : cos x - sin x * I = cosh (x * I) - sin x * I
Tactic: rw [neg_mul, ← cosh_sub_sinh, sinh_mul_I, cosh_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ cos x - sin x * I = cexp (-x * I)
have rw₃ : cos x - sin x * I = cos x - sin x * I
Tactic: rw [neg_mul, ← cosh_sub_sinh, sinh_mul_I, cosh_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 =
    HPow.hPow (β := ℕ) (cosh (x * I)) 2 - HPow.hPow (β := ℕ) (sinh (x * I)) 2
have rw : HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 =
  HPow.hPow (β := ℕ) (cos x) 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw :
  HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 =
    HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sinh (x * I)) 2
⊢ HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 =
    HPow.hPow (β := ℕ) (cosh (x * I)) 2 - HPow.hPow (β := ℕ) (sinh (x * I)) 2
have rw₁ : HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 =
  HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sin x * I) 2
Tactic: rw [cosh_mul_I, sinh_mul_I, mul_pow, I_sq, mul_neg_one, sub_neg_eq_add, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 =
    HPow.hPow (β := ℕ) (cosh (x * I)) 2 - HPow.hPow (β := ℕ) (sinh (x * I)) 2
have 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
Tactic: rw [cosh_mul_I, sinh_mul_I, mul_pow, I_sq, mul_neg_one, sub_neg_eq_add, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 =
    HPow.hPow (β := ℕ) (cosh (x * I)) 2 - HPow.hPow (β := ℕ) (sinh (x * I)) 2
have rw₃ : HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 =
  HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sin x) 2 * -1
Tactic: rw [cosh_mul_I, sinh_mul_I, mul_pow, I_sq, mul_neg_one, sub_neg_eq_add, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 =
    HPow.hPow (β := ℕ) (cosh (x * I)) 2 - HPow.hPow (β := ℕ) (sinh (x * I)) 2
have rw₄ : HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 =
  HPow.hPow (β := ℕ) (cos x) 2 - -HPow.hPow (β := ℕ) (sin x) 2
Tactic: rw [cosh_mul_I, sinh_mul_I, mul_pow, I_sq, mul_neg_one, sub_neg_eq_add, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 =
    HPow.hPow (β := ℕ) (cosh (x * I)) 2 - HPow.hPow (β := ℕ) (sinh (x * I)) 2
have rw₅ : HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 =
  HPow.hPow (β := ℕ) (cos x) 2 + HPow.hPow (β := ℕ) (sin x) 2
Tactic: rw [cosh_mul_I, sinh_mul_I, mul_pow, I_sq, mul_neg_one, sub_neg_eq_add, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 =
    HPow.hPow (β := ℕ) (cosh (x * I)) 2 - HPow.hPow (β := ℕ) (sinh (x * I)) 2
have rw₆ : HPow.hPow (β := ℕ) (cos x) 2 + HPow.hPow (β := ℕ) (sin x) 2 =
  HPow.hPow (β := ℕ) (cos x) 2 + HPow.hPow (β := ℕ) (sin x) 2
Tactic: rw [cosh_mul_I, sinh_mul_I, mul_pow, I_sq, mul_neg_one, sub_neg_eq_add, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ HPow.hPow (β := ℕ) (cos x) 2 + HPow.hPow (β := ℕ) (sin x) 2 = 1
have rw : HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 = 1
Tactic: rw [add_comm, sin_sq_add_cos_sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 = 1
⊢ HPow.hPow (β := ℕ) (cos x) 2 + HPow.hPow (β := ℕ) (sin x) 2 = 1
have rw₁ : Eq (α := ℂ) 1 1
Tactic: rw [add_comm, sin_sq_add_cos_sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ cos (2 * x) = HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sin x) 2
have rw : cos (x + x) = HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sin x) 2
Tactic: rw [two_mul, cos_add, ← sq, ← sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : cos (x + x) = HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sin x) 2
⊢ cos (2 * x) = HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sin x) 2
have rw₁ : cos x * cos x - sin x * sin x = HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sin x) 2
Tactic: rw [two_mul, cos_add, ← sq, ← sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ cos (2 * x) = HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sin x) 2
have rw₂ : HPow.hPow (β := ℕ) (cos x) 2 - sin x * sin x = HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sin x) 2
Tactic: rw [two_mul, cos_add, ← sq, ← sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ cos (2 * x) = HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sin x) 2
have rw₃ : HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sin x) 2 =
  HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sin x) 2
Tactic: rw [two_mul, cos_add, ← sq, ← sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ cos (2 * x) = 2 * HPow.hPow (β := ℕ) (cos x) 2 - 1
have rw : HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sin x) 2 = 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sin x) 2 = 2 * HPow.hPow (β := ℕ) (cos x) 2 - 1
⊢ cos (2 * x) = 2 * HPow.hPow (β := ℕ) (cos x) 2 - 1
have rw₁ : HPow.hPow (β := ℕ) (cos x) 2 - (1 - HPow.hPow (β := ℕ) (cos x) 2) = 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ cos (2 * x) = 2 * HPow.hPow (β := ℕ) (cos x) 2 - 1
have rw₂ : HPow.hPow (β := ℕ) (cos x) 2 - 1 + HPow.hPow (β := ℕ) (cos x) 2 = 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ cos (2 * x) = 2 * HPow.hPow (β := ℕ) (cos x) 2 - 1
have rw₃ : HPow.hPow (β := ℕ) (cos x) 2 + HPow.hPow (β := ℕ) (cos x) 2 - 1 = 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ cos (2 * x) = 2 * HPow.hPow (β := ℕ) (cos x) 2 - 1
have rw₄ : HPow.hPow (β := ℕ) (cos x) 2 + HPow.hPow (β := ℕ) (cos x) 2 - 1 =
  HPow.hPow (β := ℕ) (cos 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ sin (2 * x) = 2 * sin x * cos x
have rw : sin (x + x) = 2 * sin x * cos x
Tactic: rw [two_mul, sin_add, two_mul, add_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : sin (x + x) = 2 * sin x * cos x
⊢ sin (2 * x) = 2 * sin x * cos x
have rw₁ : sin x * cos x + cos x * sin x = 2 * sin x * cos x
Tactic: rw [two_mul, sin_add, two_mul, add_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ sin (2 * x) = 2 * sin x * cos x
have rw₂ : sin x * cos x + cos x * sin x = (sin x + sin x) * cos x
Tactic: rw [two_mul, sin_add, two_mul, add_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ sin (2 * x) = 2 * sin x * cos x
have rw₃ : sin x * cos x + cos x * sin x = sin x * cos x + sin x * cos x
Tactic: rw [two_mul, sin_add, two_mul, add_mul, mul_comm]