awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw₃ : sin x * cos x + cos x * sin x = sin x * cos x + sin x * cos x
⊢ sin (2 * x) = 2 * sin x * cos x
have rw₄ : cos x * sin x + cos x * sin x = cos x * sin x + cos x * sin 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 : ℂ
⊢ HPow.hPow (β := ℕ) (cos x) 2 = 1 - 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 [← sin_sq_add_cos_sq x, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw :
  HPow.hPow (β := ℕ) (cos x) 2 =
    HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sin x) 2
⊢ HPow.hPow (β := ℕ) (cos x) 2 = 1 - HPow.hPow (β := ℕ) (sin x) 2
have rw₁ : HPow.hPow (β := ℕ) (cos x) 2 = HPow.hPow (β := ℕ) (cos x) 2
Tactic: rw [← sin_sq_add_cos_sq x, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ HPow.hPow (β := ℕ) (sin x) 2 = 1 - HPow.hPow (β := ℕ) (cos x) 2
have rw : HPow.hPow (β := ℕ) (sin x) 2 =
  HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (cos x) 2
Tactic: rw [← sin_sq_add_cos_sq x, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw :
  HPow.hPow (β := ℕ) (sin x) 2 =
    HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (cos x) 2
⊢ HPow.hPow (β := ℕ) (sin x) 2 = 1 - HPow.hPow (β := ℕ) (cos x) 2
have rw₁ : HPow.hPow (β := ℕ) (sin x) 2 = HPow.hPow (β := ℕ) (sin x) 2
Tactic: rw [← sin_sq_add_cos_sq x, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
h : cos x ≠ 0
| 1
have rw : HPow.hPow (β := ℕ) (tan x * cos x) 2 + HPow.hPow (β := ℕ) (cos x) 2
Tactic: rw [← sin_sq_add_cos_sq x, ← tan_mul_cos h]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
h : cos x ≠ 0
⊢ (1 + HPow.hPow (β := ℕ) (tan x) 2) * HPow.hPow (β := ℕ) (cos x) 2 = 1
have conv_rhs : (1 + HPow.hPow (β := ℕ) (tan x) 2) * HPow.hPow (β := ℕ) (cos x) 2 =
  HPow.hPow (β := ℕ) (tan x * cos x) 2 + HPow.hPow (β := ℕ) (cos x) 2
Tactic: conv_rhs => rw [← sin_sq_add_cos_sq x, ← tan_mul_cos h]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
hx : cos x ≠ 0
⊢ (1 + HPow.hPow (β := ℕ) (tan x) 2)⁻¹ = HPow.hPow (β := ℕ) (cos x) 2
have rw : (1 + HPow.hPow (β := ℕ) (sin x) 2 / HPow.hPow (β := ℕ) (cos x) 2)⁻¹ = HPow.hPow (β := ℕ) (cos x) 2
Tactic: rw [tan_eq_sin_div_cos, div_pow]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ cos (3 * x) = 4 * HPow.hPow (β := ℕ) (cos x) 3 - 3 * cos x
have rw : cosh (3 * x * I) = 4 * HPow.hPow (β := ℕ) (cos x) 3 - 3 * cos x
Tactic: rw [← cosh_mul_I, mul_assoc, cosh_three_mul, cosh_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : cosh (3 * x * I) = 4 * HPow.hPow (β := ℕ) (cos x) 3 - 3 * cos x
⊢ cos (3 * x) = 4 * HPow.hPow (β := ℕ) (cos x) 3 - 3 * cos x
have rw₁ : cosh (3 * (x * I)) = 4 * HPow.hPow (β := ℕ) (cos x) 3 - 3 * cos x
Tactic: rw [← cosh_mul_I, mul_assoc, cosh_three_mul, cosh_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : cosh (3 * x * I) = 4 * HPow.hPow (β := ℕ) (cos x) 3 - 3 * cos x
rw₁ : cosh (3 * (x * I)) = 4 * HPow.hPow (β := ℕ) (cos x) 3 - 3 * cos x
⊢ cos (3 * x) = 4 * HPow.hPow (β := ℕ) (cos x) 3 - 3 * cos x
have rw₂ : 4 * HPow.hPow (β := ℕ) (cosh (x * I)) 3 - 3 * cosh (x * I) = 4 * HPow.hPow (β := ℕ) (cos x) 3 - 3 * cos x
Tactic: rw [← cosh_mul_I, mul_assoc, cosh_three_mul, cosh_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : cosh (3 * x * I) = 4 * HPow.hPow (β := ℕ) (cos x) 3 - 3 * cos x
rw₁ : cosh (3 * (x * I)) = 4 * HPow.hPow (β := ℕ) (cos x) 3 - 3 * cos x
rw₂ : 4 * HPow.hPow (β := ℕ) (cosh (x * I)) 3 - 3 * cosh (x * I) = 4 * HPow.hPow (β := ℕ) (cos x) 3 - 3 * cos x
⊢ cos (3 * x) = 4 * HPow.hPow (β := ℕ) (cos x) 3 - 3 * cos x
have rw₃ : 4 * HPow.hPow (β := ℕ) (cos x) 3 - 3 * cos x = 4 * HPow.hPow (β := ℕ) (cos x) 3 - 3 * cos x
Tactic: rw [← cosh_mul_I, mul_assoc, cosh_three_mul, cosh_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ sin (3 * x) = 3 * sin x - 4 * HPow.hPow (β := ℕ) (sin x) 3
have rw : sin (2 * x) * cos x + cos (2 * x) * sin x = HAdd.hAdd (α := ℂ) 2 1 * sin x - 4 * HPow.hPow (β := ℕ) (sin x) 3
Tactic: rw [← two_add_one_eq_three, add_one_mul, sin_add (2 * x) x]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ sin (2 * x) * cos x + cos (2 * x) * sin x = HAdd.hAdd (α := ℂ) 2 1 * sin x - 4 * HPow.hPow (β := ℕ) (sin x) 3
have simp : 2 * (sin x * (1 - HPow.hPow (β := ℕ) (sin x) 2)) + (2 * (1 - HPow.hPow (β := ℕ) (sin x) 2) - 1) * sin x =
  HAdd.hAdd (α := ℂ) 2 1 * sin x - 4 * HPow.hPow (β := ℕ) (sin x) 3
Tactic: simp only [cos_two_mul, sin_two_mul, cos_sq', mul_assoc, ← sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x y : ℂ
⊢ cexp (x + y * I) = cexp x * (cos y + sin y * I)
have rw : cexp x * cexp (y * I) = cexp x * (cos y + sin y * I)
Tactic: rw [exp_add, exp_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x y : ℂ
rw : cexp x * cexp (y * I) = cexp x * (cos y + sin y * I)
⊢ cexp (x + y * I) = cexp x * (cos y + sin y * I)
have rw₁ : cexp x * (cos y + sin y * I) = cexp x * (cos y + sin y * I)
Tactic: rw [exp_add, exp_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ cexp x = cexp (↑x.re : ℂ) * (cos (↑x.im : ℂ) + sin (↑x.im : ℂ) * I)
have rw : cexp x = cexp ((↑x.re : ℂ) + (↑x.im : ℂ) * I)
Tactic: rw [← exp_add_mul_I, re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
rw : cexp x = cexp ((↑x.re : ℂ) + (↑x.im : ℂ) * I)
⊢ cexp x = cexp (↑x.re : ℂ) * (cos (↑x.im : ℂ) + sin (↑x.im : ℂ) * I)
have rw₁ : cexp x = cexp x
Tactic: rw [← exp_add_mul_I, re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ (cexp x).re = Real.exp x.re * Real.cos x.im
have rw : (cexp (↑x.re : ℂ) * (cos (↑x.im : ℂ) + sin (↑x.im : ℂ) * I)).re = Real.exp x.re * Real.cos x.im
Tactic: rw [exp_eq_exp_re_mul_sin_add_cos]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
⊢ (cexp x).im = Real.exp x.re * Real.sin x.im
have rw : (cexp (↑x.re : ℂ) * (cos (↑x.im : ℂ) + sin (↑x.im : ℂ) * I)).im = Real.exp x.re * Real.sin x.im
Tactic: rw [exp_eq_exp_re_mul_sin_add_cos]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
n : ℕ
z : ℂ
⊢ (cos z + sin z * I) ^ n = cos ((↑n : ℂ) * z) + sin ((↑n : ℂ) * z) * I
have rw : cexp (z * I) ^ n = cos ((↑n : ℂ) * z) + sin ((↑n : ℂ) * z) * I
Tactic: rw [← exp_mul_I, ← exp_mul_I, ← exp_nat_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
n : ℕ
z : ℂ
rw : cexp (z * I) ^ n = cos ((↑n : ℂ) * z) + sin ((↑n : ℂ) * z) * I
⊢ (cos z + sin z * I) ^ n = cos ((↑n : ℂ) * z) + sin ((↑n : ℂ) * z) * I
have rw₁ : cexp (z * I) ^ n = cexp ((↑n : ℂ) * z * I)
Tactic: rw [← exp_mul_I, ← exp_mul_I, ← exp_nat_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
n : ℕ
z : ℂ
rw : cexp (z * I) ^ n = cos ((↑n : ℂ) * z) + sin ((↑n : ℂ) * z) * I
rw₁ : cexp (z * I) ^ n = cexp ((↑n : ℂ) * z * I)
⊢ (cos z + sin z * I) ^ n = cos ((↑n : ℂ) * z) + sin ((↑n : ℂ) * z) * I
have rw₂ : cexp ((↑n : ℂ) * (z * I)) = cexp ((↑n : ℂ) * z * I)
Tactic: rw [← exp_mul_I, ← exp_mul_I, ← exp_nat_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
n : ℕ
z : ℂ
rw : cexp (z * I) ^ n = cos ((↑n : ℂ) * z) + sin ((↑n : ℂ) * z) * I
rw₁ : cexp (z * I) ^ n = cexp ((↑n : ℂ) * z * I)
rw₂ : cexp ((↑n : ℂ) * (z * I)) = cexp ((↑n : ℂ) * z * I)
⊢ (cos z + sin z * I) ^ n = cos ((↑n : ℂ) * z) + sin ((↑n : ℂ) * z) * I
have rw₃ : cexp ((↑n : ℂ) * (z * I)) = cexp ((↑n : ℂ) * (z * I))
Tactic: rw [← exp_mul_I, ← exp_mul_I, ← exp_nat_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖cos x - (1 - HPow.hPow (β := ℕ) x 2 / 2)‖ =
    ‖(cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / (↑m.factorial : ℂ)) / 2 +
        (cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)) / 2‖
have simp : ‖(cexp (x * I) + cexp (-(x * I))) / 2 - (1 - HPow.hPow (β := ℕ) x 2 / 2)‖ =
  ‖(cexp (-(x * I)) - (1 + -(x * I) + HPow.hPow (β := ℕ) (x * I) 2 / 2 + HPow.hPow (β := ℕ) (-(x * I)) 3 / 6)) / 2 +
      (cexp (x * I) - (1 + x * I + HPow.hPow (β := ℕ) (x * I) 2 / 2 + HPow.hPow (β := ℕ) (x * I) 3 / 6)) / 2‖
Tactic: simp [cos, field, Finset.sum_range_succ, Nat.factorial]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖(cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / (↑m.factorial : ℂ)) / 2 +
        (cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)) / 2‖ ≤
    ‖cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / (↑m.factorial : ℂ)‖ / 2 +
      ‖cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)‖ / 2
have grw : ‖(cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / (↑m.factorial : ℂ)) / 2‖ +
    ‖(cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)) / 2‖ ≤
  ‖cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / (↑m.factorial : ℂ)‖ / 2 +
    ‖cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)‖ / 2
Tactic: grw [norm_add_le]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / (↑m.factorial : ℂ)‖ / 2 +
      ‖cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)‖ / 2 ≤
    HPow.hPow (β := ℕ) ‖-x * I‖ 4 * ((↑(Nat.succ 4) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 4) : ℝ) (↑4 : ℝ))⁻¹) /
        2 +
      HPow.hPow (β := ℕ) ‖x * I‖ 4 * ((↑(Nat.succ 4) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 4) : ℝ) (↑4 : ℝ))⁻¹) /
        2
have h₁ : LE.le (α := ℝ) 0 2
Tactic: grw [exp_bound (by simpa) (by simp), exp_bound (by simpa) (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
h₁ : LE.le (α := ℝ) 0 2
⊢ ‖cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / (↑m.factorial : ℂ)‖ / 2 +
      ‖cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)‖ / 2 ≤
    HPow.hPow (β := ℕ) ‖-x * I‖ 4 * ((↑(Nat.succ 4) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 4) : ℝ) (↑4 : ℝ))⁻¹) /
        2 +
      HPow.hPow (β := ℕ) ‖x * I‖ 4 * ((↑(Nat.succ 4) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 4) : ℝ) (↑4 : ℝ))⁻¹) /
        2
have grw : HPow.hPow (β := ℕ) ‖-x * I‖ 4 * ((↑(Nat.succ 4) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 4) : ℝ) (↑4 : ℝ))⁻¹) / 2 +
    ‖cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)‖ / 2 ≤
  HPow.hPow (β := ℕ) ‖-x * I‖ 4 * ((↑(Nat.succ 4) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 4) : ℝ) (↑4 : ℝ))⁻¹) / 2 +
    HPow.hPow (β := ℕ) ‖x * I‖ 4 * ((↑(Nat.succ 4) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 4) : ℝ) (↑4 : ℝ))⁻¹) / 2
Tactic: grw [exp_bound (by simpa) (by simp), exp_bound (by simpa) (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
h₁ : LE.le (α := ℝ) 0 2
grw :
  HPow.hPow (β := ℕ) ‖-x * I‖ 4 * ((↑(Nat.succ 4) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 4) : ℝ) (↑4 : ℝ))⁻¹) / 2 +
      ‖cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)‖ / 2 ≤
    HPow.hPow (β := ℕ) ‖-x * I‖ 4 * ((↑(Nat.succ 4) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 4) : ℝ) (↑4 : ℝ))⁻¹) /
        2 +
      HPow.hPow (β := ℕ) ‖x * I‖ 4 * ((↑(Nat.succ 4) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 4) : ℝ) (↑4 : ℝ))⁻¹) /
        2
⊢ ‖cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / (↑m.factorial : ℂ)‖ / 2 +
      ‖cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)‖ / 2 ≤
    HPow.hPow (β := ℕ) ‖-x * I‖ 4 * ((↑(Nat.succ 4) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 4) : ℝ) (↑4 : ℝ))⁻¹) /
        2 +
      HPow.hPow (β := ℕ) ‖x * I‖ 4 * ((↑(Nat.succ 4) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 4) : ℝ) (↑4 : ℝ))⁻¹) /
        2
have grw₁ : HPow.hPow (β := ℕ) ‖-x * I‖ 4 * ((↑(Nat.succ 4) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 4) : ℝ) (↑4 : ℝ))⁻¹) / 2 +
    HPow.hPow (β := ℕ) ‖x * I‖ 4 * ((↑(Nat.succ 4) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 4) : ℝ) (↑4 : ℝ))⁻¹) /
      2 ≤
  HPow.hPow (β := ℕ) ‖-x * I‖ 4 * ((↑(Nat.succ 4) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 4) : ℝ) (↑4 : ℝ))⁻¹) / 2 +
    HPow.hPow (β := ℕ) ‖x * I‖ 4 * ((↑(Nat.succ 4) : ℝ) * (HMul.hMul (α := ℝ) (↑(Nat.factorial 4) : ℝ) (↑4 : ℝ))⁻¹) / 2
Tactic: grw [exp_bound (by simpa) (by simp), exp_bound (by simpa) (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖sin x - (x - HPow.hPow (β := ℕ) x 3 / 6)‖ =
    ‖(cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / (↑m.factorial : ℂ)) * I / 2 -
        (cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)) * I / 2‖
have simp : ‖(cexp (-(x * I)) - cexp (x * I)) * I / 2 - (x - HPow.hPow (β := ℕ) x 3 / 6)‖ =
  ‖(cexp (-(x * I)) - (1 + -(x * I) + HPow.hPow (β := ℕ) (x * I) 2 / 2 + HPow.hPow (β := ℕ) (-(x * I)) 3 / 6)) * I / 2 -
      (cexp (x * I) - (1 + x * I + HPow.hPow (β := ℕ) (x * I) 2 / 2 + HPow.hPow (β := ℕ) (x * I) 3 / 6)) * I / 2‖
Tactic: simp [sin, field, Finset.sum_range_succ, Nat.factorial]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖(cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / (↑m.factorial : ℂ)) * I / 2 -
        (cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)) * I / 2‖ ≤
    ‖cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / (↑m.factorial : ℂ)‖ / 2 +
      ‖cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)‖ / 2
have grw : ‖(cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / (↑m.factorial : ℂ)) * I / 2‖ +
    ‖(cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)) * I / 2‖ ≤
  ‖cexp (-x * I) - ∑ m ∈ range 4, (-x * I) ^ m / (↑m.factorial : ℂ)‖ / 2 +
    ‖cexp (x * I) - ∑ m ∈ range 4, (x * I) ^ m / (↑m.factorial : ℂ)‖ / 2
Tactic: grw [norm_sub_le]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ cos |x| = cos x
have inl : x ≤ 0 → cos |x| = cos x
Tactic: cases le_total x 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
inl : x ≤ 0 → cos |x| = cos x
⊢ cos |x| = cos x
have inr : 0 ≤ x → cos |x| = cos x
Tactic: cases le_total x 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x y : ℝ
⊢ 2 * sin x * sin y = cos (x - y) - cos (x + y)
have simp : 2 * sin x * sin y = sin x * sin y + sin x * sin y
Tactic: simp [cos_add, cos_sub]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x y : ℝ
⊢ 2 * cos x * cos y = cos (x - y) + cos (x + y)
have simp : 2 * cos x * cos y = cos x * cos y + cos x * cos y
Tactic: simp [cos_add, cos_sub]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x y : ℝ
⊢ 2 * sin x * cos y = sin (x - y) + sin (x + y)
have simp : 2 * sin x * cos y = sin x * cos y + sin x * cos y
Tactic: simp [sin_add, sin_sub]
-- 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 : ℝ
⊢ 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 : ℝ
⊢ HPow.hPow (β := ℕ) (sin x) 2 ≤ 1
have rw : HPow.hPow (β := ℕ) (sin x) 2 ≤ HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2
Tactic: rw [← sin_sq_add_cos_sq x]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ HPow.hPow (β := ℕ) (cos x) 2 ≤ 1
have rw : HPow.hPow (β := ℕ) (cos x) 2 ≤ HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2
Tactic: rw [← sin_sq_add_cos_sq x]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ HPow.hPow (β := ℕ) (cos x) 2 = 1 - 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 [← sin_sq_add_cos_sq x, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
rw :
  HPow.hPow (β := ℕ) (cos x) 2 =
    HPow.hPow (β := ℕ) (sin x) 2 + HPow.hPow (β := ℕ) (cos x) 2 - HPow.hPow (β := ℕ) (sin x) 2
⊢ HPow.hPow (β := ℕ) (cos x) 2 = 1 - HPow.hPow (β := ℕ) (sin x) 2
have rw₁ : HPow.hPow (β := ℕ) (cos x) 2 = HPow.hPow (β := ℕ) (cos x) 2
Tactic: rw [← sin_sq_add_cos_sq x, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ HPow.hPow (β := ℕ) (sin x) 2 = 1 / 2 - cos (2 * x) / 2
have rw : 1 - HPow.hPow (β := ℕ) (cos x) 2 = 1 / 2 - cos (2 * x) / 2
Tactic: rw [sin_sq, cos_sq, ← sub_sub, sub_half]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
rw : 1 - HPow.hPow (β := ℕ) (cos x) 2 = 1 / 2 - cos (2 * x) / 2
⊢ HPow.hPow (β := ℕ) (sin x) 2 = 1 / 2 - cos (2 * x) / 2
have rw₁ : 1 - (1 / 2 + cos (2 * x) / 2) = 1 / 2 - cos (2 * x) / 2
Tactic: rw [sin_sq, cos_sq, ← sub_sub, sub_half]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
rw : 1 - HPow.hPow (β := ℕ) (cos x) 2 = 1 / 2 - cos (2 * x) / 2
rw₁ : 1 - (1 / 2 + cos (2 * x) / 2) = 1 / 2 - cos (2 * x) / 2
⊢ HPow.hPow (β := ℕ) (sin x) 2 = 1 / 2 - cos (2 * x) / 2
have rw₂ : 1 - 1 / 2 - cos (2 * x) / 2 = 1 / 2 - cos (2 * x) / 2
Tactic: rw [sin_sq, cos_sq, ← sub_sub, sub_half]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
rw : 1 - HPow.hPow (β := ℕ) (cos x) 2 = 1 / 2 - cos (2 * x) / 2
rw₁ : 1 - (1 / 2 + cos (2 * x) / 2) = 1 / 2 - cos (2 * x) / 2
rw₂ : 1 - 1 / 2 - cos (2 * x) / 2 = 1 / 2 - cos (2 * x) / 2
⊢ HPow.hPow (β := ℕ) (sin x) 2 = 1 / 2 - cos (2 * x) / 2
have rw₃ : 1 / 2 - cos (2 * x) / 2 = 1 / 2 - cos (2 * x) / 2
Tactic: rw [sin_sq, cos_sq, ← sub_sub, sub_half]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ |sin x| = √(1 - HPow.hPow (β := ℕ) (cos x) 2)
have rw : |sin x| = √(HPow.hPow (β := ℕ) (sin x) 2)
Tactic: rw [← sin_sq, sqrt_sq_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
rw : |sin x| = √(HPow.hPow (β := ℕ) (sin x) 2)
⊢ |sin x| = √(1 - HPow.hPow (β := ℕ) (cos x) 2)
have rw₁ : |sin x| = |sin x|
Tactic: rw [← sin_sq, sqrt_sq_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ |cos x| = √(1 - HPow.hPow (β := ℕ) (sin x) 2)
have rw : |cos x| = √(HPow.hPow (β := ℕ) (cos x) 2)
Tactic: rw [← cos_sq', sqrt_sq_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
rw : |cos x| = √(HPow.hPow (β := ℕ) (cos x) 2)
⊢ |cos x| = √(1 - HPow.hPow (β := ℕ) (sin x) 2)
have rw₁ : |cos x| = |cos x|
Tactic: rw [← cos_sq', sqrt_sq_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
hx : 0 < cos x
⊢ (√(1 + HPow.hPow (β := ℕ) (tan x) 2))⁻¹ = cos x
have rw : (√(1 + HPow.hPow (β := ℕ) (tan x) 2))⁻¹ = √(HPow.hPow (β := ℕ) (cos x) 2)
Tactic: rw [← sqrt_sq hx.le, ← sqrt_inv, inv_one_add_tan_sq hx.ne']
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
hx : 0 < cos x
rw : (√(1 + HPow.hPow (β := ℕ) (tan x) 2))⁻¹ = √(HPow.hPow (β := ℕ) (cos x) 2)
⊢ (√(1 + HPow.hPow (β := ℕ) (tan x) 2))⁻¹ = cos x
have rw₁ : √(1 + HPow.hPow (β := ℕ) (tan x) 2)⁻¹ = √(HPow.hPow (β := ℕ) (cos x) 2)
Tactic: rw [← sqrt_sq hx.le, ← sqrt_inv, inv_one_add_tan_sq hx.ne']
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
hx : 0 < cos x
rw : (√(1 + HPow.hPow (β := ℕ) (tan x) 2))⁻¹ = √(HPow.hPow (β := ℕ) (cos x) 2)
rw₁ : √(1 + HPow.hPow (β := ℕ) (tan x) 2)⁻¹ = √(HPow.hPow (β := ℕ) (cos x) 2)
⊢ (√(1 + HPow.hPow (β := ℕ) (tan x) 2))⁻¹ = cos x
have rw₂ : √(HPow.hPow (β := ℕ) (cos x) 2) = √(HPow.hPow (β := ℕ) (cos x) 2)
Tactic: rw [← sqrt_sq hx.le, ← sqrt_inv, inv_one_add_tan_sq hx.ne']
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
hx : 0 < cos x
⊢ tan x / √(1 + HPow.hPow (β := ℕ) (tan x) 2) = sin x
have rw : tan x / √(1 + HPow.hPow (β := ℕ) (tan x) 2) = tan x * cos x
Tactic: rw [← tan_mul_cos hx.ne', ← inv_sqrt_one_add_tan_sq hx, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
hx : 0 < cos x
rw : tan x / √(1 + HPow.hPow (β := ℕ) (tan x) 2) = tan x * cos x
⊢ tan x / √(1 + HPow.hPow (β := ℕ) (tan x) 2) = sin x
have rw₁ : tan x / √(1 + HPow.hPow (β := ℕ) (tan x) 2) = tan x * (√(1 + HPow.hPow (β := ℕ) (tan x) 2))⁻¹
Tactic: rw [← tan_mul_cos hx.ne', ← inv_sqrt_one_add_tan_sq hx, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
hx : 0 < cos x
rw : tan x / √(1 + HPow.hPow (β := ℕ) (tan x) 2) = tan x * cos x
rw₁ : tan x / √(1 + HPow.hPow (β := ℕ) (tan x) 2) = tan x * (√(1 + HPow.hPow (β := ℕ) (tan x) 2))⁻¹
⊢ tan x / √(1 + HPow.hPow (β := ℕ) (tan x) 2) = sin x
have rw₂ : tan x * (√(1 + HPow.hPow (β := ℕ) (tan x) 2))⁻¹ = tan x * (√(1 + HPow.hPow (β := ℕ) (tan x) 2))⁻¹
Tactic: rw [← tan_mul_cos hx.ne', ← inv_sqrt_one_add_tan_sq hx, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ cos (3 * x) = 4 * HPow.hPow (β := ℕ) (cos x) 3 - 3 * cos x
have rw : (↑(cos (3 * x)) : ℂ) = (↑(4 * HPow.hPow (β := ℕ) (cos x) 3 - 3 * cos x) : ℂ)
Tactic: rw [← ofReal_inj]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ sin (3 * x) = 3 * sin x - 4 * HPow.hPow (β := ℕ) (sin x) 3
have rw : (↑(sin (3 * x)) : ℂ) = (↑(3 * sin x - 4 * HPow.hPow (β := ℕ) (sin x) 3) : ℂ)
Tactic: rw [← ofReal_inj]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x y : ℝ
⊢ sinh (x + y) = sinh x * cosh y + cosh x * sinh y
have rw : (↑(sinh (x + y)) : ℂ) = (↑(sinh x * cosh y + cosh x * sinh y) : ℂ)
Tactic: rw [← ofReal_inj]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ cosh x * 2 = rexp x + rexp (-x)
have rw : (Complex.cosh (↑x : ℂ)).re * 2 = rexp x + rexp (-x)
Tactic: rw [cosh, exp, exp, Complex.ofReal_neg, Complex.cosh, mul_two, ← Complex.add_re, ← mul_two,
      div_mul_cancel₀ _ (two_ne_zero' ℂ), Complex.add_re]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
rw : (Complex.cosh (↑x : ℂ)).re * 2 = rexp x + rexp (-x)
⊢ cosh x * 2 = rexp x + rexp (-x)
have rw₁ : (Complex.cosh (↑x : ℂ)).re * 2 = (cexp (↑x : ℂ)).re + rexp (-x)
Tactic: rw [cosh, exp, exp, Complex.ofReal_neg, Complex.cosh, mul_two, ← Complex.add_re, ← mul_two,
      div_mul_cancel₀ _ (two_ne_zero' ℂ), Complex.add_re]