awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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‖
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 - 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‖
rw₁ :
  ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp (0 * I) - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₂ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp 0 - 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)) * (1 - 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‖
rw₁ :
  ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp (0 * I) - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₂ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp 0 - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₃ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (1 - 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)) * (1 - cexp ((↑x : ℂ) * 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‖
rw₁ :
  ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp (0 * I) - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₂ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp 0 - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₃ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (1 - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₄ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (1 - cexp ((↑x : ℂ) * 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) * (1 - cexp ((↑x : ℂ) * 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‖
rw₁ :
  ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp (0 * I) - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₂ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp 0 - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₃ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (1 - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₄ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (1 - cexp ((↑x : ℂ) * I)) * I‖
rw₅ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * 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) * (1 - cexp ((↑x : ℂ) * 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‖
rw₁ :
  ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp (0 * I) - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₂ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp 0 - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₃ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (1 - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₄ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (1 - cexp ((↑x : ℂ) * I)) * I‖
rw₅ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I)) * I‖
rw₆ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * 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) * (1 - cexp ((↑x : ℂ) * I))‖ * 1
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‖
rw₁ :
  ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp (0 * I) - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₂ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp 0 - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₃ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (1 - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₄ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (1 - cexp ((↑x : ℂ) * I)) * I‖
rw₅ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I)) * I‖
rw₆ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I))‖ * ‖I‖
rw₇ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I))‖ * 1
⊢ ‖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) * (1 - cexp ((↑x : ℂ) * 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‖
rw₁ :
  ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp (0 * I) - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₂ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp 0 - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₃ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (1 - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₄ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (1 - cexp ((↑x : ℂ) * I)) * I‖
rw₅ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I)) * I‖
rw₆ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I))‖ * ‖I‖
rw₇ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I))‖ * 1
rw₈ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * 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)‖ * ‖1 - cexp ((↑x : ℂ) * 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‖
rw₁ :
  ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp (0 * I) - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₂ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp 0 - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₃ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (1 - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₄ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (1 - cexp ((↑x : ℂ) * I)) * I‖
rw₅ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I)) * I‖
rw₆ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I))‖ * ‖I‖
rw₇ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I))‖ * 1
rw₈ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I))‖
rw₉ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I)‖ * ‖1 - cexp ((↑x : ℂ) * 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)‖ * ‖1 - cexp ((↑x : ℂ) * 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‖
rw₁ :
  ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp (0 * I) - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₂ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp 0 - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₃ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (1 - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₄ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (1 - cexp ((↑x : ℂ) * I)) * I‖
rw₅ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I)) * I‖
rw₆ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I))‖ * ‖I‖
rw₇ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I))‖ * 1
rw₈ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I))‖
rw₉ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I)‖ * ‖1 - cexp ((↑x : ℂ) * I)‖
rw₁₀ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp ((↑(-x / 2) : ℂ) * I)‖ * ‖1 - cexp ((↑x : ℂ) * 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‖ = 1 * ‖1 - cexp ((↑x : ℂ) * 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‖
rw₁ :
  ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp (0 * I) - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₂ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp 0 - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₃ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (1 - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₄ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (1 - cexp ((↑x : ℂ) * I)) * I‖
rw₅ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I)) * I‖
rw₆ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I))‖ * ‖I‖
rw₇ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I))‖ * 1
rw₈ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I))‖
rw₉ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I)‖ * ‖1 - cexp ((↑x : ℂ) * I)‖
rw₁₀ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp ((↑(-x / 2) : ℂ) * I)‖ * ‖1 - cexp ((↑x : ℂ) * I)‖
rw₁₁ : ‖cexp (I * (↑x : ℂ)) - 1‖ = 1 * ‖1 - cexp ((↑x : ℂ) * 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‖ = ‖1 - cexp ((↑x : ℂ) * 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‖
rw₁ :
  ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp (0 * I) - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₂ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp 0 - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₃ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (1 - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₄ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (1 - cexp ((↑x : ℂ) * I)) * I‖
rw₅ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I)) * I‖
rw₆ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I))‖ * ‖I‖
rw₇ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I))‖ * 1
rw₈ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I))‖
rw₉ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I)‖ * ‖1 - cexp ((↑x : ℂ) * I)‖
rw₁₀ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp ((↑(-x / 2) : ℂ) * I)‖ * ‖1 - cexp ((↑x : ℂ) * I)‖
rw₁₁ : ‖cexp (I * (↑x : ℂ)) - 1‖ = 1 * ‖1 - cexp ((↑x : ℂ) * I)‖
rw₁₂ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖1 - cexp ((↑x : ℂ) * 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)‖ = ‖1 - cexp ((↑x : ℂ) * 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‖
rw₁ :
  ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp (0 * I) - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₂ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp 0 - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₃ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (1 - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₄ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (1 - cexp ((↑x : ℂ) * I)) * I‖
rw₅ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I)) * I‖
rw₆ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I))‖ * ‖I‖
rw₇ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I))‖ * 1
rw₈ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I))‖
rw₉ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I)‖ * ‖1 - cexp ((↑x : ℂ) * I)‖
rw₁₀ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp ((↑(-x / 2) : ℂ) * I)‖ * ‖1 - cexp ((↑x : ℂ) * I)‖
rw₁₁ : ‖cexp (I * (↑x : ℂ)) - 1‖ = 1 * ‖1 - cexp ((↑x : ℂ) * I)‖
rw₁₂ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖1 - cexp ((↑x : ℂ) * I)‖
rw₁₃ : ‖-(cexp (I * (↑x : ℂ)) - 1)‖ = ‖1 - cexp ((↑x : ℂ) * I)‖
⊢ ‖cexp (I * (↑x : ℂ)) - 1‖ =
    ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp ((↑(x / 2 + -(x / 2)) : ℂ) * I) - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
have rw₁₄ : ‖1 - cexp (I * (↑x : ℂ))‖ = ‖1 - cexp ((↑x : ℂ) * 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‖
rw₁ :
  ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp (0 * I) - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₂ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp 0 - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₃ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (1 - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
rw₄ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-((↑(x / 2) : ℂ) * I)) * (1 - cexp ((↑x : ℂ) * I)) * I‖
rw₅ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I)) * I‖
rw₆ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I))‖ * ‖I‖
rw₇ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I))‖ * 1
rw₈ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I) * (1 - cexp ((↑x : ℂ) * I))‖
rw₉ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp (-(↑(x / 2) : ℂ) * I)‖ * ‖1 - cexp ((↑x : ℂ) * I)‖
rw₁₀ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖cexp ((↑(-x / 2) : ℂ) * I)‖ * ‖1 - cexp ((↑x : ℂ) * I)‖
rw₁₁ : ‖cexp (I * (↑x : ℂ)) - 1‖ = 1 * ‖1 - cexp ((↑x : ℂ) * I)‖
rw₁₂ : ‖cexp (I * (↑x : ℂ)) - 1‖ = ‖1 - cexp ((↑x : ℂ) * I)‖
rw₁₃ : ‖-(cexp (I * (↑x : ℂ)) - 1)‖ = ‖1 - cexp ((↑x : ℂ) * I)‖
rw₁₄ : ‖1 - cexp (I * (↑x : ℂ))‖ = ‖1 - cexp ((↑x : ℂ) * I)‖
⊢ ‖cexp (I * (↑x : ℂ)) - 1‖ =
    ‖cexp (-((↑(x / 2) : ℂ) * I)) * (cexp ((↑(x / 2 + -(x / 2)) : ℂ) * I) - cexp ((↑(x / 2 + x / 2) : ℂ) * I)) * I‖
have rw₁₅ : ‖1 - cexp ((↑x : ℂ) * I)‖ = ‖1 - cexp ((↑x : ℂ) * 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:
z : ℂ
⊢ ‖cexp z‖ = Real.exp z.re
have rw : ‖cexp (↑z.re : ℂ) * (cos (↑z.im : ℂ) + sin (↑z.im : ℂ) * I)‖ = Real.exp z.re
Tactic: rw [exp_eq_exp_re_mul_sin_add_cos, Complex.norm_mul, norm_exp_ofReal, norm_cos_add_sin_mul_I,
    mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
z : ℂ
rw : ‖cexp (↑z.re : ℂ) * (cos (↑z.im : ℂ) + sin (↑z.im : ℂ) * I)‖ = Real.exp z.re
⊢ ‖cexp z‖ = Real.exp z.re
have rw₁ : ‖cexp (↑z.re : ℂ)‖ * ‖cos (↑z.im : ℂ) + sin (↑z.im : ℂ) * I‖ = Real.exp z.re
Tactic: rw [exp_eq_exp_re_mul_sin_add_cos, Complex.norm_mul, norm_exp_ofReal, norm_cos_add_sin_mul_I,
    mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
z : ℂ
rw : ‖cexp (↑z.re : ℂ) * (cos (↑z.im : ℂ) + sin (↑z.im : ℂ) * I)‖ = Real.exp z.re
rw₁ : ‖cexp (↑z.re : ℂ)‖ * ‖cos (↑z.im : ℂ) + sin (↑z.im : ℂ) * I‖ = Real.exp z.re
⊢ ‖cexp z‖ = Real.exp z.re
have rw₂ : Real.exp z.re * ‖cos (↑z.im : ℂ) + sin (↑z.im : ℂ) * I‖ = Real.exp z.re
Tactic: rw [exp_eq_exp_re_mul_sin_add_cos, Complex.norm_mul, norm_exp_ofReal, norm_cos_add_sin_mul_I,
    mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
z : ℂ
rw : ‖cexp (↑z.re : ℂ) * (cos (↑z.im : ℂ) + sin (↑z.im : ℂ) * I)‖ = Real.exp z.re
rw₁ : ‖cexp (↑z.re : ℂ)‖ * ‖cos (↑z.im : ℂ) + sin (↑z.im : ℂ) * I‖ = Real.exp z.re
rw₂ : Real.exp z.re * ‖cos (↑z.im : ℂ) + sin (↑z.im : ℂ) * I‖ = Real.exp z.re
⊢ ‖cexp z‖ = Real.exp z.re
have rw₃ : Real.exp z.re * 1 = Real.exp z.re
Tactic: rw [exp_eq_exp_re_mul_sin_add_cos, Complex.norm_mul, norm_exp_ofReal, norm_cos_add_sin_mul_I,
    mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
z : ℂ
rw : ‖cexp (↑z.re : ℂ) * (cos (↑z.im : ℂ) + sin (↑z.im : ℂ) * I)‖ = Real.exp z.re
rw₁ : ‖cexp (↑z.re : ℂ)‖ * ‖cos (↑z.im : ℂ) + sin (↑z.im : ℂ) * I‖ = Real.exp z.re
rw₂ : Real.exp z.re * ‖cos (↑z.im : ℂ) + sin (↑z.im : ℂ) * I‖ = Real.exp z.re
rw₃ : Real.exp z.re * 1 = Real.exp z.re
⊢ ‖cexp z‖ = Real.exp z.re
have rw₄ : Real.exp z.re = Real.exp z.re
Tactic: rw [exp_eq_exp_re_mul_sin_add_cos, Complex.norm_mul, norm_exp_ofReal, norm_cos_add_sin_mul_I,
    mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x y : ℂ
⊢ ‖cexp x‖ = ‖cexp y‖ ↔ x.re = y.re
have rw : Real.exp x.re = ‖cexp y‖ ↔ x.re = y.re
Tactic: rw [norm_exp, norm_exp, Real.exp_eq_exp]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x y : ℂ
rw : Real.exp x.re = ‖cexp y‖ ↔ x.re = y.re
⊢ ‖cexp x‖ = ‖cexp y‖ ↔ x.re = y.re
have rw₁ : Real.exp x.re = Real.exp y.re ↔ x.re = y.re
Tactic: rw [norm_exp, norm_exp, Real.exp_eq_exp]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Trigonometric (goal)
Goal:
x y : ℂ
rw : Real.exp x.re = ‖cexp y‖ ↔ x.re = y.re
rw₁ : Real.exp x.re = Real.exp y.re ↔ x.re = y.re
⊢ ‖cexp x‖ = ‖cexp y‖ ↔ x.re = y.re
have rw₂ : x.re = y.re ↔ x.re = y.re
Tactic: rw [norm_exp, norm_exp, Real.exp_eq_exp]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UnitDisc.Basic (goal)
Goal:
z : 𝔻
⊢ HPow.hPow (β := ℕ) ‖(↑z : ℂ)‖ 2 < 1
have rw : ‖(↑z : ℂ)‖ < 1
Tactic: rw [sq_lt_one_iff_abs_lt_one, abs_norm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UnitDisc.Basic (goal)
Goal:
z : 𝔻
⊢ LT.lt (α := ℝ) ((normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ) (1 : ℝ)
have rw : HPow.hPow (β := ℕ) ‖(↑z : ℂ)‖ 2 < 1
Tactic: rw [← Complex.norm_mul_self_eq_normSq, ← sq]