awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
rw : (Complex.cosh (↑x : ℂ)).re * 2 = rexp x + rexp (-x)
rw₁ : (Complex.cosh (↑x : ℂ)).re * 2 = (cexp (↑x : ℂ)).re + rexp (-x)
⊢ cosh x * 2 = rexp x + rexp (-x)
have rw₂ : (Complex.cosh (↑x : ℂ)).re * 2 = (cexp (↑x : ℂ)).re + (cexp (↑(-x) : ℂ)).re
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)
rw₁ : (Complex.cosh (↑x : ℂ)).re * 2 = (cexp (↑x : ℂ)).re + rexp (-x)
rw₂ : (Complex.cosh (↑x : ℂ)).re * 2 = (cexp (↑x : ℂ)).re + (cexp (↑(-x) : ℂ)).re
⊢ cosh x * 2 = rexp x + rexp (-x)
have rw₃ : (Complex.cosh (↑x : ℂ)).re * 2 = (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
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)
rw₁ : (Complex.cosh (↑x : ℂ)).re * 2 = (cexp (↑x : ℂ)).re + rexp (-x)
rw₂ : (Complex.cosh (↑x : ℂ)).re * 2 = (cexp (↑x : ℂ)).re + (cexp (↑(-x) : ℂ)).re
rw₃ : (Complex.cosh (↑x : ℂ)).re * 2 = (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
⊢ cosh x * 2 = rexp x + rexp (-x)
have rw₄ : ((cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2).re * 2 = (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
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)
rw₁ : (Complex.cosh (↑x : ℂ)).re * 2 = (cexp (↑x : ℂ)).re + rexp (-x)
rw₂ : (Complex.cosh (↑x : ℂ)).re * 2 = (cexp (↑x : ℂ)).re + (cexp (↑(-x) : ℂ)).re
rw₃ : (Complex.cosh (↑x : ℂ)).re * 2 = (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
rw₄ : ((cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2).re * 2 = (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
⊢ cosh x * 2 = rexp x + rexp (-x)
have rw₅ : ((cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2).re + ((cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2).re =
  (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
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)
rw₁ : (Complex.cosh (↑x : ℂ)).re * 2 = (cexp (↑x : ℂ)).re + rexp (-x)
rw₂ : (Complex.cosh (↑x : ℂ)).re * 2 = (cexp (↑x : ℂ)).re + (cexp (↑(-x) : ℂ)).re
rw₃ : (Complex.cosh (↑x : ℂ)).re * 2 = (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
rw₄ : ((cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2).re * 2 = (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
rw₅ :
  ((cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2).re + ((cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2).re =
    (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
⊢ cosh x * 2 = rexp x + rexp (-x)
have rw₆ : ((cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2 + (cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2).re =
  (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
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)
rw₁ : (Complex.cosh (↑x : ℂ)).re * 2 = (cexp (↑x : ℂ)).re + rexp (-x)
rw₂ : (Complex.cosh (↑x : ℂ)).re * 2 = (cexp (↑x : ℂ)).re + (cexp (↑(-x) : ℂ)).re
rw₃ : (Complex.cosh (↑x : ℂ)).re * 2 = (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
rw₄ : ((cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2).re * 2 = (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
rw₅ :
  ((cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2).re + ((cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2).re =
    (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
rw₆ :
  ((cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2 + (cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2).re =
    (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
⊢ cosh x * 2 = rexp x + rexp (-x)
have rw₇ : ((cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2 * 2).re = (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
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)
rw₁ : (Complex.cosh (↑x : ℂ)).re * 2 = (cexp (↑x : ℂ)).re + rexp (-x)
rw₂ : (Complex.cosh (↑x : ℂ)).re * 2 = (cexp (↑x : ℂ)).re + (cexp (↑(-x) : ℂ)).re
rw₃ : (Complex.cosh (↑x : ℂ)).re * 2 = (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
rw₄ : ((cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2).re * 2 = (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
rw₅ :
  ((cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2).re + ((cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2).re =
    (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
rw₆ :
  ((cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2 + (cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2).re =
    (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
rw₇ : ((cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2 * 2).re = (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
⊢ cosh x * 2 = rexp x + rexp (-x)
have rw₈ : (cexp (↑x : ℂ) + cexp (-(↑x : ℂ))).re = (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
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)
rw₁ : (Complex.cosh (↑x : ℂ)).re * 2 = (cexp (↑x : ℂ)).re + rexp (-x)
rw₂ : (Complex.cosh (↑x : ℂ)).re * 2 = (cexp (↑x : ℂ)).re + (cexp (↑(-x) : ℂ)).re
rw₃ : (Complex.cosh (↑x : ℂ)).re * 2 = (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
rw₄ : ((cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2).re * 2 = (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
rw₅ :
  ((cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2).re + ((cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2).re =
    (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
rw₆ :
  ((cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2 + (cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2).re =
    (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
rw₇ : ((cexp (↑x : ℂ) + cexp (-(↑x : ℂ))) / 2 * 2).re = (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
rw₈ : (cexp (↑x : ℂ) + cexp (-(↑x : ℂ))).re = (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
⊢ cosh x * 2 = rexp x + rexp (-x)
have rw₉ : (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re = (cexp (↑x : ℂ)).re + (cexp (-(↑x : ℂ))).re
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 : ℝ
⊢ cosh |x| = cosh x
have inl : x ≤ 0 → cosh |x| = cosh x
Tactic: cases le_total x 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
inl : x ≤ 0 → cosh |x| = cosh x
⊢ cosh |x| = cosh x
have inr : 0 ≤ x → cosh |x| = cosh x
Tactic: cases le_total x 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x y : ℝ
⊢ cosh (x + y) = cosh x * cosh y + sinh x * sinh y
have rw : (↑(cosh (x + y)) : ℂ) = (↑(cosh x * cosh y + sinh x * sinh y) : ℂ)
Tactic: rw [← ofReal_inj]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ tanh x = (rexp x - rexp (-x)) / (rexp x + rexp (-x))
have rw : sinh x / cosh x = (rexp x - rexp (-x)) / (rexp x + rexp (-x))
Tactic: rw [tanh_eq_sinh_div_cosh, sinh_eq, cosh_eq, div_div_div_cancel_right₀ two_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
rw : sinh x / cosh x = (rexp x - rexp (-x)) / (rexp x + rexp (-x))
⊢ tanh x = (rexp x - rexp (-x)) / (rexp x + rexp (-x))
have rw₁ : (rexp x - rexp (-x)) / 2 / cosh x = (rexp x - rexp (-x)) / (rexp x + rexp (-x))
Tactic: rw [tanh_eq_sinh_div_cosh, sinh_eq, cosh_eq, div_div_div_cancel_right₀ two_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
rw : sinh x / cosh x = (rexp x - rexp (-x)) / (rexp x + rexp (-x))
rw₁ : (rexp x - rexp (-x)) / 2 / cosh x = (rexp x - rexp (-x)) / (rexp x + rexp (-x))
⊢ tanh x = (rexp x - rexp (-x)) / (rexp x + rexp (-x))
have rw₂ : (rexp x - rexp (-x)) / 2 / ((rexp x + rexp (-x)) / 2) = (rexp x - rexp (-x)) / (rexp x + rexp (-x))
Tactic: rw [tanh_eq_sinh_div_cosh, sinh_eq, cosh_eq, div_div_div_cancel_right₀ two_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
rw : sinh x / cosh x = (rexp x - rexp (-x)) / (rexp x + rexp (-x))
rw₁ : (rexp x - rexp (-x)) / 2 / cosh x = (rexp x - rexp (-x)) / (rexp x + rexp (-x))
rw₂ : (rexp x - rexp (-x)) / 2 / ((rexp x + rexp (-x)) / 2) = (rexp x - rexp (-x)) / (rexp x + rexp (-x))
⊢ tanh x = (rexp x - rexp (-x)) / (rexp x + rexp (-x))
have rw₃ : (rexp x - rexp (-x)) / (rexp x + rexp (-x)) = (rexp x - rexp (-x)) / (rexp x + rexp (-x))
Tactic: rw [tanh_eq_sinh_div_cosh, sinh_eq, cosh_eq, div_div_div_cancel_right₀ two_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ cosh x + sinh x = rexp x
have rw : (↑(cosh x + sinh x) : ℂ) = (↑(rexp x) : ℂ)
Tactic: rw [← ofReal_inj]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ sinh x + cosh x = rexp x
have rw : cosh x + sinh x = rexp 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 = rexp x
⊢ sinh x + cosh x = rexp x
have rw₁ : rexp x = rexp x
Tactic: rw [add_comm, cosh_add_sinh]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ cosh x - sinh x = rexp (-x)
have rw : (↑(cosh x - sinh x) : ℂ) = (↑(rexp (-x)) : ℂ)
Tactic: rw [← ofReal_inj]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ sinh x - cosh x = -rexp (-x)
have rw : -(cosh x - sinh x) = -rexp (-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) = -rexp (-x)
⊢ sinh x - cosh x = -rexp (-x)
have rw₁ : -rexp (-x) = -rexp (-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 : (↑(HPow.hPow (β := ℕ) (cosh x) 2 - HPow.hPow (β := ℕ) (sinh x) 2) : ℂ) = (↑1 : ℂ)
Tactic: rw [← ofReal_inj]
-- 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 + 1) : ℂ)
Tactic: rw [← ofReal_inj]
-- 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 - 1) : ℂ)
Tactic: rw [← ofReal_inj]
-- 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 (2 * x)) : ℂ) = (↑(HPow.hPow (β := ℕ) (cosh x) 2 + HPow.hPow (β := ℕ) (sinh x) 2) : ℂ)
Tactic: rw [← ofReal_inj]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ sinh (2 * x) = 2 * sinh x * cosh x
have rw : (↑(sinh (2 * x)) : ℂ) = (↑(2 * sinh x * cosh x) : ℂ)
Tactic: rw [← ofReal_inj]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ cosh (3 * x) = 4 * HPow.hPow (β := ℕ) (cosh x) 3 - 3 * cosh x
have rw : (↑(cosh (3 * x)) : ℂ) = (↑(4 * HPow.hPow (β := ℕ) (cosh x) 3 - 3 * cosh x) : ℂ)
Tactic: rw [← ofReal_inj]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ sinh (3 * x) = 4 * HPow.hPow (β := ℕ) (sinh x) 3 + 3 * sinh x
have rw : (↑(sinh (3 * x)) : ℂ) = (↑(4 * HPow.hPow (β := ℕ) (sinh x) 3 + 3 * sinh x) : ℂ)
Tactic: rw [← ofReal_inj]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ tanh x < 1
have rw : (rexp x - rexp (-x)) / (rexp x + rexp (-x)) < 1
Tactic: rw [tanh_eq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ (rexp x - rexp (-x)) / (rexp x + rexp (-x)) < 1
have field_simp : rexp x - rexp (-x) < rexp x + rexp (-x)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ -1 < tanh x
have rw : -1 < (rexp x - rexp (-x)) / (rexp x + rexp (-x))
Tactic: rw [tanh_eq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ -1 < (rexp x - rexp (-x)) / (rexp x + rexp (-x))
have field_simp : -(rexp x + rexp (-x)) < rexp x - rexp (-x)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
hx : |x| ≤ 1
⊢ HPow.hPow (β := ℕ) |x| 4 * (5 / 96) + HPow.hPow (β := ℕ) x 2 / 2 ≤ 1 * (5 / 96) + 1 / 2
have h₁ : HPow.hPow (β := ℕ) |x| 4 ≤ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
hx : |x| ≤ 1
h₁ : HPow.hPow (β := ℕ) |x| 4 ≤ 1
⊢ HPow.hPow (β := ℕ) |x| 4 * (5 / 96) + HPow.hPow (β := ℕ) x 2 / 2 ≤ 1 * (5 / 96) + 1 / 2
have h₂ : HPow.hPow (β := ℕ) x 2 ≤ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
hx : |x| ≤ 1
⊢ HPow.hPow (β := ℕ) x 2 ≤ 1
have h₂ : |x| * |x| ≤ 1
Tactic: rw [sq, ← abs_mul_self, abs_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ HPow.hPow (β := ℕ) |x| 4 * (5 / 96) + HPow.hPow (β := ℕ) x 3 / 6 ≤ x * (5 / 96) + x / 6
have h₁ : HPow.hPow (β := ℕ) |x| 4 ≤ x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
h₁ : HPow.hPow (β := ℕ) |x| 4 ≤ x
⊢ HPow.hPow (β := ℕ) |x| 4 * (5 / 96) + HPow.hPow (β := ℕ) x 3 / 6 ≤ x * (5 / 96) + x / 6
have h₂ : HPow.hPow (β := ℕ) x 3 ≤ x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ HPow.hPow (β := ℕ) |x| 4 ≤ x
have pow_le_pow_of_le_one : HPow.hPow (β := ℕ) |x| 1 = x
Tactic: calc
                    |x| ^ 4 ≤ |x| ^ 1 :=
                      pow_le_pow_of_le_one (abs_nonneg _)
                        (by rwa [abs_of_nonneg (le_of_lt hx0)]) (by decide)
                    _ = x := by simp [abs_of_nonneg (le_of_lt hx0)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ x * (5 / 96) + x / 6 < x
have linarith : x ≤ x * (5 / 96) + x / 6 → 96 / 96 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
linarith : x ≤ x * (5 / 96) + x / 6 → 96 / 96 = 1
⊢ x * (5 / 96) + x / 6 < x
have linarith₁ : x ≤ x * (5 / 96) + x / 6 → HMul.hMul (α := ℝ) 1 96 = 96
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
linarith : x ≤ x * (5 / 96) + x / 6 → 96 / 96 = 1
linarith₁ linarith₂ : x ≤ x * (5 / 96) + x / 6 → HMul.hMul (α := ℝ) 1 96 = 96
⊢ x * (5 / 96) + x / 6 < x
have linarith₃ : x ≤ x * (5 / 96) + x / 6 → 6 / 6 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
linarith : x ≤ x * (5 / 96) + x / 6 → 96 / 96 = 1
linarith₁ linarith₂ : x ≤ x * (5 / 96) + x / 6 → HMul.hMul (α := ℝ) 1 96 = 96
linarith₃ : x ≤ x * (5 / 96) + x / 6 → 6 / 6 = 1
⊢ x * (5 / 96) + x / 6 < x
have linarith₄ : x ≤ x * (5 / 96) + x / 6 → HMul.hMul (α := ℝ) 16 6 = 96
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
linarith : x ≤ x * (5 / 96) + x / 6 → 96 / 96 = 1
linarith₁ linarith₂ : x ≤ x * (5 / 96) + x / 6 → HMul.hMul (α := ℝ) 1 96 = 96
linarith₃ : x ≤ x * (5 / 96) + x / 6 → 6 / 6 = 1
linarith₄ : x ≤ x * (5 / 96) + x / 6 → HMul.hMul (α := ℝ) 16 6 = 96
⊢ x * (5 / 96) + x / 6 < x
have linarith₅ : x ≤ x * (5 / 96) + x / 6 → GT.gt (α := ℝ) 96 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
linarith : x ≤ x * (5 / 96) + x / 6 → 96 / 96 = 1
linarith₁ linarith₂ : x ≤ x * (5 / 96) + x / 6 → HMul.hMul (α := ℝ) 1 96 = 96
linarith₃ : x ≤ x * (5 / 96) + x / 6 → 6 / 6 = 1
linarith₄ : x ≤ x * (5 / 96) + x / 6 → HMul.hMul (α := ℝ) 16 6 = 96
linarith₅ : x ≤ x * (5 / 96) + x / 6 → GT.gt (α := ℝ) 96 0
⊢ x * (5 / 96) + x / 6 < x
have linarith₆ : x ≤ x * (5 / 96) + x / 6 → 75 * (0 - x) + (96 * x - (1 * x * HMul.hMul (α := ℝ) 1 5 + 16 * x)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
linarith : x ≤ x * (5 / 96) + x / 6 → 96 / 96 = 1
linarith₁ linarith₂ : x ≤ x * (5 / 96) + x / 6 → HMul.hMul (α := ℝ) 1 96 = 96
linarith₃ : x ≤ x * (5 / 96) + x / 6 → 6 / 6 = 1
linarith₄ : x ≤ x * (5 / 96) + x / 6 → HMul.hMul (α := ℝ) 16 6 = 96
linarith₅ : x ≤ x * (5 / 96) + x / 6 → GT.gt (α := ℝ) 96 0
linarith₆ : x ≤ x * (5 / 96) + x / 6 → 75 * (0 - x) + (96 * x - (1 * x * HMul.hMul (α := ℝ) 1 5 + 16 * x)) = 0
⊢ x * (5 / 96) + x / 6 < x
have linarith₇ : x ≤ x * (5 / 96) + x / 6 → GT.gt (α := ℝ) 75 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
hx0 : 0 < x
hx : x ≤ 2
this : x / 2 ≤ 1
⊢ 2 * sin (x / 2) * cos (x / 2) = sin x
have rw : sin (2 * (x / 2)) = sin x
Tactic: rw [← sin_two_mul, two_mul, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
hx0 : 0 < x
hx : x ≤ 2
this : x / 2 ≤ 1
rw : sin (2 * (x / 2)) = sin x
⊢ 2 * sin (x / 2) * cos (x / 2) = sin x
have rw₁ : sin (x / 2 + x / 2) = sin x
Tactic: rw [← sin_two_mul, two_mul, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
hx0 : 0 < x
hx : x ≤ 2
this : x / 2 ≤ 1
rw : sin (2 * (x / 2)) = sin x
rw₁ : sin (x / 2 + x / 2) = sin x
⊢ 2 * sin (x / 2) * cos (x / 2) = sin x
have rw₂ : sin x = sin x
Tactic: rw [← sin_two_mul, two_mul, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
⊢ 2 * HPow.hPow (β := ℕ) (cos 1) 2 - 1 ≤ 2 * HPow.hPow (β := ℕ) (5 / 9) 2 - 1
have h : 0 ≤ cos 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
h : 0 ≤ cos 1
⊢ 2 * HPow.hPow (β := ℕ) (cos 1) 2 - 1 ≤ 2 * HPow.hPow (β := ℕ) (5 / 9) 2 - 1
have h₁ : cos 1 ≤ 5 / 9
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (hypothesis)
Goal:
x : ℝ
⊢ ‖cos (↑x : ℂ) + sin (↑x : ℂ) * I‖ = 1
have this : HPow.hPow (β := ℕ) (Real.sin x) 2 + HPow.hPow (β := ℕ) (Real.cos x) 2 = 1
Tactic: have := Real.sin_sq_add_cos_sq x
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ ‖cexp ((↑x : ℂ) * I)‖ = 1
have rw : ‖cos (↑x : ℂ) + sin (↑x : ℂ) * I‖ = 1
Tactic: rw [exp_mul_I, norm_cos_add_sin_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
rw : ‖cos (↑x : ℂ) + sin (↑x : ℂ) * I‖ = 1
⊢ ‖cexp ((↑x : ℂ) * I)‖ = 1
have rw₁ : Eq (α := ℝ) 1 1
Tactic: rw [exp_mul_I, norm_cos_add_sin_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ ‖cexp (I * (↑x : ℂ))‖ = 1
have rw : ‖cexp ((↑x : ℂ) * I)‖ = 1
Tactic: rw [mul_comm, norm_exp_ofReal_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
rw : ‖cexp ((↑x : ℂ) * I)‖ = 1
⊢ ‖cexp (I * (↑x : ℂ))‖ = 1
have rw₁ : Eq (α := ℝ) 1 1
Tactic: rw [mul_comm, norm_exp_ofReal_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ ‖cexp ((↑x : ℂ) * I)‖₊ = 1
have rw : (↑(nnnorm (E := ℝ) 1) : ℝ) = 1
Tactic: rw [← nnnorm_norm, norm_exp_ofReal_mul_I, ← NNReal.coe_eq_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ ‖cexp (I * (↑x : ℂ))‖₊ = 1
have rw : (↑(nnnorm (E := ℝ) 1) : ℝ) = 1
Tactic: rw [← nnnorm_norm, norm_exp_I_mul_ofReal, ← NNReal.coe_eq_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ ‖2 * Real.sin (x / 2)‖ = ‖2 * sin ((↑x : ℂ) / 2)‖
have norm_cast : ‖2 * Real.sin (x / 2)‖ = ‖2 * Real.sin (x / 2)‖
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖2 * Real.sin (x / 2)‖
have rw : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖(cexp (-((↑x : ℂ) / 2) * I) - cexp ((↑x : ℂ) / 2 * I)) * I‖
Tactic: rw [show ‖2 * Real.sin (x / 2)‖ = ‖2 * sin (x / 2)‖ by norm_cast, two_sin]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖(cexp (-((↑x : ℂ) / 2) * I) - cexp ((↑x : ℂ) / 2 * I)) * I‖
have nth_rw : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp 0 * (cexp (-((↑x : ℂ) / 2) * I) - cexp ((↑x : ℂ) / 2 * I)) * I‖
Tactic: nth_rw 2 [← one_mul (_ - _), ← exp_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp 0 * (cexp (-((↑x : ℂ) / 2) * I) - cexp ((↑x : ℂ) / 2 * I)) * I‖
have rw : ‖cexp (I * (↑x : ℂ)) - 1‖ =
  ‖cexp (-((↑x : ℂ) / 2 * I)) *
        (cexp (((↑x : ℂ) / 2 + -((↑x : ℂ) / 2)) * I) - cexp (((↑x : ℂ) / 2 + (↑x : ℂ) / 2) * I)) *
      I‖
Tactic: rw [← neg_add_cancel (x / 2 * I), exp_add, mul_assoc _ _ (_ - _), mul_sub, ← exp_add, ← exp_add,
    ← add_mul, ← add_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ ‖cexp (I * (↑x : ℂ)) - 1‖ =
    ‖cexp (-((↑x : ℂ) / 2 * I)) *
          (cexp (((↑x : ℂ) / 2 + -((↑x : ℂ) / 2)) * I) - cexp (((↑x : ℂ) / 2 + (↑x : ℂ) / 2) * I)) *
        I‖
have norm_cast : ‖cexp (I * (↑x : ℂ)) - 1‖ =
  ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp ((↑(x / 2 + -(x / 2)) : ℂ) * I) - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ -(↑(x / 2) : ℂ) = (↑(-x / 2) : ℂ)
have norm_cast : -(x / 2) = -x / 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
⊢ ‖cexp (I * (↑x : ℂ)) - 1‖ =
    ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp ((↑(x / 2 + -(x / 2)) : ℂ) * I) - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
have rw : ‖cexp (I * (↑x : ℂ)) - 1‖ =
  ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp ((↑0 : ℂ) * I) - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
Tactic: rw [add_neg_cancel, ofReal_zero, zero_mul, exp_zero, add_halves, ← neg_mul, Complex.norm_mul,
    norm_I, mul_one, Complex.norm_mul,
    show -(ofReal (x / 2)) = ofReal (-x / 2) by norm_cast; exact neg_div' 2 x,
    norm_exp_ofReal_mul_I, one_mul, ← norm_neg, neg_sub, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x : ℝ
rw :
  ‖cexp (I * (↑x : ℂ)) - 1‖ =
    ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp ((↑0 : ℂ) * I) - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
⊢ ‖cexp (I * (↑x : ℂ)) - 1‖ =
    ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp ((↑(x / 2 + -(x / 2)) : ℂ) * I) - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
have rw₁ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp (0 * I) - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
Tactic: rw [add_neg_cancel, ofReal_zero, zero_mul, exp_zero, add_halves, ← neg_mul, Complex.norm_mul,
    norm_I, mul_one, Complex.norm_mul,
    show -(ofReal (x / 2)) = ofReal (-x / 2) by norm_cast; exact neg_div' 2 x,
    norm_exp_ofReal_mul_I, one_mul, ← norm_neg, neg_sub, mul_comm]