awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
rw : tanh ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑x : ℂ)) = tanh (↑x : ℂ)
⊢ (starRingEnd ℂ : (a : ℂ) → ℂ) (tanh (↑x : ℂ)) = tanh (↑x : ℂ)
have rw₁ : tanh (↑x : ℂ) = tanh (↑x : ℂ)
Tactic: rw [← tanh_conj, conj_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ (tanh (↑x : ℂ)).im = 0
have rw : (↑(tanh (↑x : ℂ)).re : ℂ).im = 0
Tactic: rw [← ofReal_tanh_ofReal_re, ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
rw : (↑(tanh (↑x : ℂ)).re : ℂ).im = 0
⊢ (tanh (↑x : ℂ)).im = 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [← ofReal_tanh_ofReal_re, ofReal_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ cosh x + sinh x = cexp x
have rw : 2 * (cosh x + sinh x) = 2 * cexp x
Tactic: rw [← mul_right_inj' (two_ne_zero' ℂ), mul_add, two_cosh, two_sinh, add_add_sub_cancel, two_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : 2 * (cosh x + sinh x) = 2 * cexp x
⊢ cosh x + sinh x = cexp x
have rw₁ : 2 * cosh x + 2 * sinh x = 2 * cexp x
Tactic: rw [← mul_right_inj' (two_ne_zero' ℂ), mul_add, two_cosh, two_sinh, add_add_sub_cancel, two_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : 2 * (cosh x + sinh x) = 2 * cexp x
rw₁ : 2 * cosh x + 2 * sinh x = 2 * cexp x
⊢ cosh x + sinh x = cexp x
have rw₂ : cexp x + cexp (-x) + 2 * sinh x = 2 * cexp x
Tactic: rw [← mul_right_inj' (two_ne_zero' ℂ), mul_add, two_cosh, two_sinh, add_add_sub_cancel, two_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ cosh x + sinh x = cexp x
have rw₃ : cexp x + cexp (-x) + (cexp x - cexp (-x)) = 2 * cexp x
Tactic: rw [← mul_right_inj' (two_ne_zero' ℂ), mul_add, two_cosh, two_sinh, add_add_sub_cancel, two_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ cosh x + sinh x = cexp x
have rw₄ : cexp x + cexp x = 2 * cexp x
Tactic: rw [← mul_right_inj' (two_ne_zero' ℂ), mul_add, two_cosh, two_sinh, add_add_sub_cancel, two_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ cosh x + sinh x = cexp x
have rw₅ : cexp x + cexp x = cexp x + cexp x
Tactic: rw [← mul_right_inj' (two_ne_zero' ℂ), mul_add, two_cosh, two_sinh, add_add_sub_cancel, two_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ sinh x + cosh x = cexp x
have rw : cosh x + sinh x = cexp x
Tactic: rw [add_comm, cosh_add_sinh]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : cosh x + sinh x = cexp x
⊢ sinh x + cosh x = cexp x
have rw₁ : cexp x = cexp x
Tactic: rw [add_comm, cosh_add_sinh]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ cosh x - sinh x = cexp (-x)
have rw : 2 * (cosh x - sinh x) = 2 * cexp (-x)
Tactic: rw [← mul_right_inj' (two_ne_zero' ℂ), mul_sub, two_cosh, two_sinh, add_sub_sub_cancel, two_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : 2 * (cosh x - sinh x) = 2 * cexp (-x)
⊢ cosh x - sinh x = cexp (-x)
have rw₁ : 2 * cosh x - 2 * sinh x = 2 * cexp (-x)
Tactic: rw [← mul_right_inj' (two_ne_zero' ℂ), mul_sub, two_cosh, two_sinh, add_sub_sub_cancel, two_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : 2 * (cosh x - sinh x) = 2 * cexp (-x)
rw₁ : 2 * cosh x - 2 * sinh x = 2 * cexp (-x)
⊢ cosh x - sinh x = cexp (-x)
have rw₂ : cexp x + cexp (-x) - 2 * sinh x = 2 * cexp (-x)
Tactic: rw [← mul_right_inj' (two_ne_zero' ℂ), mul_sub, two_cosh, two_sinh, add_sub_sub_cancel, two_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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)
⊢ cosh x - sinh x = cexp (-x)
have rw₃ : cexp x + cexp (-x) - (cexp x - cexp (-x)) = 2 * cexp (-x)
Tactic: rw [← mul_right_inj' (two_ne_zero' ℂ), mul_sub, two_cosh, two_sinh, add_sub_sub_cancel, two_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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)
⊢ cosh x - sinh x = cexp (-x)
have rw₄ : cexp (-x) + cexp (-x) = 2 * cexp (-x)
Tactic: rw [← mul_right_inj' (two_ne_zero' ℂ), mul_sub, two_cosh, two_sinh, add_sub_sub_cancel, two_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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)
⊢ cosh x - sinh x = cexp (-x)
have rw₅ : cexp (-x) + cexp (-x) = cexp (-x) + cexp (-x)
Tactic: rw [← mul_right_inj' (two_ne_zero' ℂ), mul_sub, two_cosh, two_sinh, add_sub_sub_cancel, two_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ sinh x - cosh x = -cexp (-x)
have rw : -(cosh x - sinh x) = -cexp (-x)
Tactic: rw [← neg_sub, cosh_sub_sinh]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : -(cosh x - sinh x) = -cexp (-x)
⊢ sinh x - cosh x = -cexp (-x)
have rw₁ : -cexp (-x) = -cexp (-x)
Tactic: rw [← neg_sub, cosh_sub_sinh]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ HPow.hPow (β := ℕ) (cosh x) 2 - HPow.hPow (β := ℕ) (sinh x) 2 = 1
have rw : (cosh x + sinh x) * (cosh x - sinh x) = 1
Tactic: rw [sq_sub_sq, cosh_add_sinh, cosh_sub_sinh, ← exp_add, add_neg_cancel, exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : (cosh x + sinh x) * (cosh x - sinh x) = 1
⊢ HPow.hPow (β := ℕ) (cosh x) 2 - HPow.hPow (β := ℕ) (sinh x) 2 = 1
have rw₁ : cexp x * (cosh x - sinh x) = 1
Tactic: rw [sq_sub_sq, cosh_add_sinh, cosh_sub_sinh, ← exp_add, add_neg_cancel, exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : (cosh x + sinh x) * (cosh x - sinh x) = 1
rw₁ : cexp x * (cosh x - sinh x) = 1
⊢ HPow.hPow (β := ℕ) (cosh x) 2 - HPow.hPow (β := ℕ) (sinh x) 2 = 1
have rw₂ : cexp x * cexp (-x) = 1
Tactic: rw [sq_sub_sq, cosh_add_sinh, cosh_sub_sinh, ← exp_add, add_neg_cancel, exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ HPow.hPow (β := ℕ) (cosh x) 2 - HPow.hPow (β := ℕ) (sinh x) 2 = 1
have rw₃ : cexp (x + -x) = 1
Tactic: rw [sq_sub_sq, cosh_add_sinh, cosh_sub_sinh, ← exp_add, add_neg_cancel, exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ HPow.hPow (β := ℕ) (cosh x) 2 - HPow.hPow (β := ℕ) (sinh x) 2 = 1
have rw₄ : cexp 0 = 1
Tactic: rw [sq_sub_sq, cosh_add_sinh, cosh_sub_sinh, ← exp_add, add_neg_cancel, exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ HPow.hPow (β := ℕ) (cosh x) 2 - HPow.hPow (β := ℕ) (sinh x) 2 = 1
have rw₅ : Eq (α := ℂ) 1 1
Tactic: rw [sq_sub_sq, cosh_add_sinh, cosh_sub_sinh, ← exp_add, add_neg_cancel, exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ HPow.hPow (β := ℕ) (cosh x) 2 = HPow.hPow (β := ℕ) (sinh x) 2 + 1
have rw : HPow.hPow (β := ℕ) (cosh x) 2 =
  HPow.hPow (β := ℕ) (sinh x) 2 + (HPow.hPow (β := ℕ) (cosh x) 2 - HPow.hPow (β := ℕ) (sinh x) 2)
Tactic: rw [← cosh_sq_sub_sinh_sq x]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ HPow.hPow (β := ℕ) (sinh x) 2 = HPow.hPow (β := ℕ) (cosh x) 2 - 1
have rw : HPow.hPow (β := ℕ) (sinh x) 2 =
  HPow.hPow (β := ℕ) (cosh x) 2 - (HPow.hPow (β := ℕ) (cosh x) 2 - HPow.hPow (β := ℕ) (sinh x) 2)
Tactic: rw [← cosh_sq_sub_sinh_sq x]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ cosh (2 * x) = HPow.hPow (β := ℕ) (cosh x) 2 + HPow.hPow (β := ℕ) (sinh x) 2
have rw : cosh (x + x) = HPow.hPow (β := ℕ) (cosh x) 2 + HPow.hPow (β := ℕ) (sinh x) 2
Tactic: rw [two_mul, cosh_add, sq, sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : cosh (x + x) = HPow.hPow (β := ℕ) (cosh x) 2 + HPow.hPow (β := ℕ) (sinh x) 2
⊢ cosh (2 * x) = HPow.hPow (β := ℕ) (cosh x) 2 + HPow.hPow (β := ℕ) (sinh x) 2
have rw₁ : cosh x * cosh x + sinh x * sinh x = HPow.hPow (β := ℕ) (cosh x) 2 + HPow.hPow (β := ℕ) (sinh x) 2
Tactic: rw [two_mul, cosh_add, sq, sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ cosh (2 * x) = HPow.hPow (β := ℕ) (cosh x) 2 + HPow.hPow (β := ℕ) (sinh x) 2
have rw₂ : cosh x * cosh x + sinh x * sinh x = cosh x * cosh x + HPow.hPow (β := ℕ) (sinh x) 2
Tactic: rw [two_mul, cosh_add, sq, sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ cosh (2 * x) = HPow.hPow (β := ℕ) (cosh x) 2 + HPow.hPow (β := ℕ) (sinh x) 2
have rw₃ : cosh x * cosh x + sinh x * sinh x = cosh x * cosh x + sinh x * sinh x
Tactic: rw [two_mul, cosh_add, sq, sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ sinh (2 * x) = 2 * sinh x * cosh x
have rw : sinh x * cosh x + cosh x * sinh x = 2 * sinh x * cosh x
Tactic: rw [two_mul, sinh_add]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (hypothesis)
Goal:
x : ℂ
⊢ cosh (3 * x) = 4 * HPow.hPow (β := ℕ) (cosh x) 3 - 3 * cosh x
have h1 : x + 2 * x = 3 * x
Tactic: have h1 : x + 2 * x = 3 * x := by ring
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ cosh (3 * x) = 4 * HPow.hPow (β := ℕ) (cosh x) 3 - 3 * cosh x
have rw : cosh x * cosh (2 * x) + sinh x * sinh (2 * x) = 4 * HPow.hPow (β := ℕ) (cosh x) 3 - 3 * cosh x
Tactic: rw [← h1, cosh_add x (2 * x)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ cosh x * cosh (2 * x) + sinh x * sinh (2 * x) = 4 * HPow.hPow (β := ℕ) (cosh x) 3 - 3 * cosh x
have 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
Tactic: simp only [cosh_two_mul, sinh_two_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (hypothesis)
Goal:
x : ℂ
h1 : x + 2 * x = 3 * 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
have h2 : 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
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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 (β := ℕ) (sinh x) 2) + sinh x * (2 * sinh x * cosh x) =
    4 * HPow.hPow (β := ℕ) (cosh x) 3 - 3 * cosh x
have 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
Tactic: rw [h2, sinh_sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (hypothesis)
Goal:
x : ℂ
⊢ sinh (3 * x) = 4 * HPow.hPow (β := ℕ) (sinh x) 3 + 3 * sinh x
have h1 : x + 2 * x = 3 * x
Tactic: have h1 : x + 2 * x = 3 * x := by ring
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ sinh (3 * x) = 4 * HPow.hPow (β := ℕ) (sinh x) 3 + 3 * sinh x
have rw : sinh x * cosh (2 * x) + cosh x * sinh (2 * x) = 4 * HPow.hPow (β := ℕ) (sinh x) 3 + 3 * sinh x
Tactic: rw [← h1, sinh_add x (2 * x)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
h1 : x + 2 * x = 3 * x
⊢ sinh x * cosh (2 * x) + cosh x * sinh (2 * x) = 4 * HPow.hPow (β := ℕ) (sinh x) 3 + 3 * sinh x
have 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
Tactic: simp only [cosh_two_mul, sinh_two_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (hypothesis)
Goal:
x : ℂ
h1 : x + 2 * x = 3 * 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
have h2 : 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
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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 (β := ℕ) (cosh x) 2 + HPow.hPow (β := ℕ) (sinh x) 2) + cosh x * (2 * sinh x * cosh x) =
    4 * HPow.hPow (β := ℕ) (sinh x) 3 + 3 * sinh x
have 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
Tactic: rw [h2, cosh_sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ sinh (x * I) = sin x * I
have rw : 2 * sinh (x * I) = 2 * (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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : 2 * sinh (x * I) = 2 * (sin x * I)
⊢ sinh (x * I) = sin x * I
have rw₁ : cexp (x * I) - cexp (-(x * I)) = 2 * (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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : 2 * sinh (x * I) = 2 * (sin x * I)
rw₁ : cexp (x * I) - cexp (-(x * I)) = 2 * (sin x * I)
⊢ sinh (x * I) = sin x * I
have rw₂ : cexp (x * I) - cexp (-(x * I)) = 2 * 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ sinh (x * I) = sin x * I
have rw₃ : cexp (x * I) - cexp (-(x * I)) = (cexp (-x * I) - cexp (x * I)) * I * 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ sinh (x * I) = sin x * I
have rw₄ : cexp (x * I) - cexp (-(x * I)) = (cexp (-x * I) - cexp (x * I)) * (I * 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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)
⊢ sinh (x * I) = sin x * I
have rw₅ : cexp (x * I) - cexp (-(x * I)) = (cexp (-x * I) - cexp (x * I)) * -1
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ sinh (x * I) = sin x * I
have rw₆ : cexp (x * I) - cexp (-(x * I)) = -(cexp (-x * I) - cexp (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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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))
⊢ sinh (x * I) = sin x * I
have rw₇ : cexp (x * I) - cexp (-(x * I)) = cexp (x * I) - cexp (-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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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)
⊢ sinh (x * I) = sin x * I
have rw₈ : cexp (x * I) - cexp (-x * I) = cexp (x * I) - cexp (-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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ cosh (x * I) = cos x
have rw : 2 * cosh (x * I) = 2 * cos x
Tactic: rw [← mul_right_inj' (two_ne_zero' ℂ), two_cosh, two_cos, neg_mul_eq_neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : 2 * cosh (x * I) = 2 * cos x
⊢ cosh (x * I) = cos x
have rw₁ : cexp (x * I) + cexp (-(x * I)) = 2 * cos x
Tactic: rw [← mul_right_inj' (two_ne_zero' ℂ), two_cosh, two_cos, neg_mul_eq_neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : 2 * cosh (x * I) = 2 * cos x
rw₁ : cexp (x * I) + cexp (-(x * I)) = 2 * cos x
⊢ cosh (x * I) = cos x
have rw₂ : cexp (x * I) + cexp (-(x * I)) = cexp (x * I) + cexp (-x * I)
Tactic: rw [← mul_right_inj' (two_ne_zero' ℂ), two_cosh, two_cos, neg_mul_eq_neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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)
⊢ cosh (x * I) = cos x
have rw₃ : cexp (x * I) + cexp (-x * I) = cexp (x * I) + cexp (-x * I)
Tactic: rw [← mul_right_inj' (two_ne_zero' ℂ), two_cosh, two_cos, neg_mul_eq_neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ tanh (x * I) = tan x * I
have rw : sinh (x * I) / cosh (x * I) = tan x * I
Tactic: rw [tanh_eq_sinh_div_cosh, cosh_mul_I, sinh_mul_I, mul_div_right_comm, tan]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : sinh (x * I) / cosh (x * I) = tan x * I
⊢ tanh (x * I) = tan x * I
have rw₁ : sinh (x * I) / cos x = tan x * I
Tactic: rw [tanh_eq_sinh_div_cosh, cosh_mul_I, sinh_mul_I, mul_div_right_comm, tan]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : sinh (x * I) / cosh (x * I) = tan x * I
rw₁ : sinh (x * I) / cos x = tan x * I
⊢ tanh (x * I) = tan x * I
have rw₂ : sin x * I / cos x = tan x * I
Tactic: rw [tanh_eq_sinh_div_cosh, cosh_mul_I, sinh_mul_I, mul_div_right_comm, tan]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ tanh (x * I) = tan x * I
have rw₃ : sin x / cos x * I = tan x * I
Tactic: rw [tanh_eq_sinh_div_cosh, cosh_mul_I, sinh_mul_I, mul_div_right_comm, tan]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
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
⊢ tanh (x * I) = tan x * I
have rw₄ : sin x / cos x * I = sin x / cos x * I
Tactic: rw [tanh_eq_sinh_div_cosh, cosh_mul_I, sinh_mul_I, mul_div_right_comm, tan]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ cos (x * I) = cosh x
have rw : cosh (x * I * I) = cosh x
Tactic: rw [← cosh_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ cosh (x * I * I) = cosh x
have ring_nf : cosh (x * HPow.hPow (β := ℕ) I 2) = cosh x
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ I * sin (x * I) = -sinh x
have rw : sinh (x * I * I) = -sinh x
Tactic: rw [mul_comm, ← sinh_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ sinh (x * I * I) = -sinh x
have ring_nf : sinh (x * HPow.hPow (β := ℕ) I 2) = -sinh x
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (hypothesis)
Goal:
x : ℂ
⊢ sin (x * I) = sinh x * I
have h : 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
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
h : I * sin (x * I) = -sinh x
⊢ sin (x * I) = sinh x * I
have rw : sin (x * I) = -(I * sin (x * I)) * I
Tactic: rw [← neg_neg (sinh x), ← h]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
h : I * sin (x * I) = -sinh x
⊢ sin (x * I) = -(I * sin (x * I)) * I
have a : (sin (x * I)).re = (-(I * sin (x * I)) * I).re
Tactic: apply Complex.ext