awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx : x ≠ 0
rw : cexp ((↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I) = x
rw₁ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + sin (↑x.arg : ℂ) * I) = x
rw₂ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + (↑(Real.sin x.arg) : ℂ) * I) = x
rw₃ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₄ : cexp (↑(Real.log ‖x‖) : ℂ) * ((↑(Real.cos x.arg) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
⊢ cexp (log x) = x
have rw₅ : cexp (↑(Real.log ‖x‖) : ℂ) * ((↑(x.re / ‖x‖) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
Tactic: rw [log, exp_add_mul_I, ← ofReal_sin, sin_arg, ← ofReal_cos, cos_arg hx, ← ofReal_exp,
    Real.exp_log (norm_pos_iff.mpr hx), mul_add, ofReal_div, ofReal_div,
    mul_div_cancel₀ _ (ofReal_ne_zero.2 <| norm_ne_zero_iff.mpr hx), ← mul_assoc,
    mul_div_cancel₀ _ (ofReal_ne_zero.2 <| norm_ne_zero_iff.mpr hx), re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx : x ≠ 0
rw : cexp ((↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I) = x
rw₁ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + sin (↑x.arg : ℂ) * I) = x
rw₂ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + (↑(Real.sin x.arg) : ℂ) * I) = x
rw₃ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₄ : cexp (↑(Real.log ‖x‖) : ℂ) * ((↑(Real.cos x.arg) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₅ : cexp (↑(Real.log ‖x‖) : ℂ) * ((↑(x.re / ‖x‖) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
⊢ cexp (log x) = x
have rw₆ : (↑(rexp (Real.log ‖x‖)) : ℂ) * ((↑(x.re / ‖x‖) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
Tactic: rw [log, exp_add_mul_I, ← ofReal_sin, sin_arg, ← ofReal_cos, cos_arg hx, ← ofReal_exp,
    Real.exp_log (norm_pos_iff.mpr hx), mul_add, ofReal_div, ofReal_div,
    mul_div_cancel₀ _ (ofReal_ne_zero.2 <| norm_ne_zero_iff.mpr hx), ← mul_assoc,
    mul_div_cancel₀ _ (ofReal_ne_zero.2 <| norm_ne_zero_iff.mpr hx), re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx : x ≠ 0
rw : cexp ((↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I) = x
rw₁ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + sin (↑x.arg : ℂ) * I) = x
rw₂ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + (↑(Real.sin x.arg) : ℂ) * I) = x
rw₃ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₄ : cexp (↑(Real.log ‖x‖) : ℂ) * ((↑(Real.cos x.arg) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₅ : cexp (↑(Real.log ‖x‖) : ℂ) * ((↑(x.re / ‖x‖) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₆ : (↑(rexp (Real.log ‖x‖)) : ℂ) * ((↑(x.re / ‖x‖) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
⊢ cexp (log x) = x
have rw₇ : (↑‖x‖ : ℂ) * ((↑(x.re / ‖x‖) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
Tactic: rw [log, exp_add_mul_I, ← ofReal_sin, sin_arg, ← ofReal_cos, cos_arg hx, ← ofReal_exp,
    Real.exp_log (norm_pos_iff.mpr hx), mul_add, ofReal_div, ofReal_div,
    mul_div_cancel₀ _ (ofReal_ne_zero.2 <| norm_ne_zero_iff.mpr hx), ← mul_assoc,
    mul_div_cancel₀ _ (ofReal_ne_zero.2 <| norm_ne_zero_iff.mpr hx), re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx : x ≠ 0
rw : cexp ((↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I) = x
rw₁ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + sin (↑x.arg : ℂ) * I) = x
rw₂ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + (↑(Real.sin x.arg) : ℂ) * I) = x
rw₃ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₄ : cexp (↑(Real.log ‖x‖) : ℂ) * ((↑(Real.cos x.arg) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₅ : cexp (↑(Real.log ‖x‖) : ℂ) * ((↑(x.re / ‖x‖) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₆ : (↑(rexp (Real.log ‖x‖)) : ℂ) * ((↑(x.re / ‖x‖) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₇ : (↑‖x‖ : ℂ) * ((↑(x.re / ‖x‖) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
⊢ cexp (log x) = x
have rw₈ : (↑‖x‖ : ℂ) * (↑(x.re / ‖x‖) : ℂ) + (↑‖x‖ : ℂ) * ((↑(x.im / ‖x‖) : ℂ) * I) = x
Tactic: rw [log, exp_add_mul_I, ← ofReal_sin, sin_arg, ← ofReal_cos, cos_arg hx, ← ofReal_exp,
    Real.exp_log (norm_pos_iff.mpr hx), mul_add, ofReal_div, ofReal_div,
    mul_div_cancel₀ _ (ofReal_ne_zero.2 <| norm_ne_zero_iff.mpr hx), ← mul_assoc,
    mul_div_cancel₀ _ (ofReal_ne_zero.2 <| norm_ne_zero_iff.mpr hx), re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx : x ≠ 0
rw : cexp ((↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I) = x
rw₁ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + sin (↑x.arg : ℂ) * I) = x
rw₂ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + (↑(Real.sin x.arg) : ℂ) * I) = x
rw₃ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₄ : cexp (↑(Real.log ‖x‖) : ℂ) * ((↑(Real.cos x.arg) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₅ : cexp (↑(Real.log ‖x‖) : ℂ) * ((↑(x.re / ‖x‖) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₆ : (↑(rexp (Real.log ‖x‖)) : ℂ) * ((↑(x.re / ‖x‖) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₇ : (↑‖x‖ : ℂ) * ((↑(x.re / ‖x‖) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₈ : (↑‖x‖ : ℂ) * (↑(x.re / ‖x‖) : ℂ) + (↑‖x‖ : ℂ) * ((↑(x.im / ‖x‖) : ℂ) * I) = x
⊢ cexp (log x) = x
have rw₉ : (↑‖x‖ : ℂ) * ((↑x.re : ℂ) / (↑‖x‖ : ℂ)) + (↑‖x‖ : ℂ) * ((↑(x.im / ‖x‖) : ℂ) * I) = x
Tactic: rw [log, exp_add_mul_I, ← ofReal_sin, sin_arg, ← ofReal_cos, cos_arg hx, ← ofReal_exp,
    Real.exp_log (norm_pos_iff.mpr hx), mul_add, ofReal_div, ofReal_div,
    mul_div_cancel₀ _ (ofReal_ne_zero.2 <| norm_ne_zero_iff.mpr hx), ← mul_assoc,
    mul_div_cancel₀ _ (ofReal_ne_zero.2 <| norm_ne_zero_iff.mpr hx), re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx : x ≠ 0
rw : cexp ((↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I) = x
rw₁ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + sin (↑x.arg : ℂ) * I) = x
rw₂ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + (↑(Real.sin x.arg) : ℂ) * I) = x
rw₃ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₄ : cexp (↑(Real.log ‖x‖) : ℂ) * ((↑(Real.cos x.arg) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₅ : cexp (↑(Real.log ‖x‖) : ℂ) * ((↑(x.re / ‖x‖) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₆ : (↑(rexp (Real.log ‖x‖)) : ℂ) * ((↑(x.re / ‖x‖) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₇ : (↑‖x‖ : ℂ) * ((↑(x.re / ‖x‖) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₈ : (↑‖x‖ : ℂ) * (↑(x.re / ‖x‖) : ℂ) + (↑‖x‖ : ℂ) * ((↑(x.im / ‖x‖) : ℂ) * I) = x
rw₉ : (↑‖x‖ : ℂ) * ((↑x.re : ℂ) / (↑‖x‖ : ℂ)) + (↑‖x‖ : ℂ) * ((↑(x.im / ‖x‖) : ℂ) * I) = x
⊢ cexp (log x) = x
have rw₁₀ : (↑‖x‖ : ℂ) * ((↑x.re : ℂ) / (↑‖x‖ : ℂ)) + (↑‖x‖ : ℂ) * ((↑x.im : ℂ) / (↑‖x‖ : ℂ) * I) = x
Tactic: rw [log, exp_add_mul_I, ← ofReal_sin, sin_arg, ← ofReal_cos, cos_arg hx, ← ofReal_exp,
    Real.exp_log (norm_pos_iff.mpr hx), mul_add, ofReal_div, ofReal_div,
    mul_div_cancel₀ _ (ofReal_ne_zero.2 <| norm_ne_zero_iff.mpr hx), ← mul_assoc,
    mul_div_cancel₀ _ (ofReal_ne_zero.2 <| norm_ne_zero_iff.mpr hx), re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx : x ≠ 0
rw : cexp ((↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I) = x
rw₁ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + sin (↑x.arg : ℂ) * I) = x
rw₂ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + (↑(Real.sin x.arg) : ℂ) * I) = x
rw₃ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₄ : cexp (↑(Real.log ‖x‖) : ℂ) * ((↑(Real.cos x.arg) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₅ : cexp (↑(Real.log ‖x‖) : ℂ) * ((↑(x.re / ‖x‖) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₆ : (↑(rexp (Real.log ‖x‖)) : ℂ) * ((↑(x.re / ‖x‖) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₇ : (↑‖x‖ : ℂ) * ((↑(x.re / ‖x‖) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₈ : (↑‖x‖ : ℂ) * (↑(x.re / ‖x‖) : ℂ) + (↑‖x‖ : ℂ) * ((↑(x.im / ‖x‖) : ℂ) * I) = x
rw₉ : (↑‖x‖ : ℂ) * ((↑x.re : ℂ) / (↑‖x‖ : ℂ)) + (↑‖x‖ : ℂ) * ((↑(x.im / ‖x‖) : ℂ) * I) = x
rw₁₀ : (↑‖x‖ : ℂ) * ((↑x.re : ℂ) / (↑‖x‖ : ℂ)) + (↑‖x‖ : ℂ) * ((↑x.im : ℂ) / (↑‖x‖ : ℂ) * I) = x
⊢ cexp (log x) = x
have rw₁₁ : (↑x.re : ℂ) + (↑‖x‖ : ℂ) * ((↑x.im : ℂ) / (↑‖x‖ : ℂ) * I) = x
Tactic: rw [log, exp_add_mul_I, ← ofReal_sin, sin_arg, ← ofReal_cos, cos_arg hx, ← ofReal_exp,
    Real.exp_log (norm_pos_iff.mpr hx), mul_add, ofReal_div, ofReal_div,
    mul_div_cancel₀ _ (ofReal_ne_zero.2 <| norm_ne_zero_iff.mpr hx), ← mul_assoc,
    mul_div_cancel₀ _ (ofReal_ne_zero.2 <| norm_ne_zero_iff.mpr hx), re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx : x ≠ 0
rw : cexp ((↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I) = x
rw₁ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + sin (↑x.arg : ℂ) * I) = x
rw₂ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + (↑(Real.sin x.arg) : ℂ) * I) = x
rw₃ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₄ : cexp (↑(Real.log ‖x‖) : ℂ) * ((↑(Real.cos x.arg) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₅ : cexp (↑(Real.log ‖x‖) : ℂ) * ((↑(x.re / ‖x‖) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₆ : (↑(rexp (Real.log ‖x‖)) : ℂ) * ((↑(x.re / ‖x‖) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₇ : (↑‖x‖ : ℂ) * ((↑(x.re / ‖x‖) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₈ : (↑‖x‖ : ℂ) * (↑(x.re / ‖x‖) : ℂ) + (↑‖x‖ : ℂ) * ((↑(x.im / ‖x‖) : ℂ) * I) = x
rw₉ : (↑‖x‖ : ℂ) * ((↑x.re : ℂ) / (↑‖x‖ : ℂ)) + (↑‖x‖ : ℂ) * ((↑(x.im / ‖x‖) : ℂ) * I) = x
rw₁₀ : (↑‖x‖ : ℂ) * ((↑x.re : ℂ) / (↑‖x‖ : ℂ)) + (↑‖x‖ : ℂ) * ((↑x.im : ℂ) / (↑‖x‖ : ℂ) * I) = x
rw₁₁ : (↑x.re : ℂ) + (↑‖x‖ : ℂ) * ((↑x.im : ℂ) / (↑‖x‖ : ℂ) * I) = x
⊢ cexp (log x) = x
have rw₁₂ : (↑x.re : ℂ) + (↑‖x‖ : ℂ) * ((↑x.im : ℂ) / (↑‖x‖ : ℂ)) * I = x
Tactic: rw [log, exp_add_mul_I, ← ofReal_sin, sin_arg, ← ofReal_cos, cos_arg hx, ← ofReal_exp,
    Real.exp_log (norm_pos_iff.mpr hx), mul_add, ofReal_div, ofReal_div,
    mul_div_cancel₀ _ (ofReal_ne_zero.2 <| norm_ne_zero_iff.mpr hx), ← mul_assoc,
    mul_div_cancel₀ _ (ofReal_ne_zero.2 <| norm_ne_zero_iff.mpr hx), re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx : x ≠ 0
rw : cexp ((↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I) = x
rw₁ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + sin (↑x.arg : ℂ) * I) = x
rw₂ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + (↑(Real.sin x.arg) : ℂ) * I) = x
rw₃ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₄ : cexp (↑(Real.log ‖x‖) : ℂ) * ((↑(Real.cos x.arg) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₅ : cexp (↑(Real.log ‖x‖) : ℂ) * ((↑(x.re / ‖x‖) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₆ : (↑(rexp (Real.log ‖x‖)) : ℂ) * ((↑(x.re / ‖x‖) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₇ : (↑‖x‖ : ℂ) * ((↑(x.re / ‖x‖) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₈ : (↑‖x‖ : ℂ) * (↑(x.re / ‖x‖) : ℂ) + (↑‖x‖ : ℂ) * ((↑(x.im / ‖x‖) : ℂ) * I) = x
rw₉ : (↑‖x‖ : ℂ) * ((↑x.re : ℂ) / (↑‖x‖ : ℂ)) + (↑‖x‖ : ℂ) * ((↑(x.im / ‖x‖) : ℂ) * I) = x
rw₁₀ : (↑‖x‖ : ℂ) * ((↑x.re : ℂ) / (↑‖x‖ : ℂ)) + (↑‖x‖ : ℂ) * ((↑x.im : ℂ) / (↑‖x‖ : ℂ) * I) = x
rw₁₁ : (↑x.re : ℂ) + (↑‖x‖ : ℂ) * ((↑x.im : ℂ) / (↑‖x‖ : ℂ) * I) = x
rw₁₂ : (↑x.re : ℂ) + (↑‖x‖ : ℂ) * ((↑x.im : ℂ) / (↑‖x‖ : ℂ)) * I = x
⊢ cexp (log x) = x
have rw₁₃ : (↑x.re : ℂ) + (↑x.im : ℂ) * I = x
Tactic: rw [log, exp_add_mul_I, ← ofReal_sin, sin_arg, ← ofReal_cos, cos_arg hx, ← ofReal_exp,
    Real.exp_log (norm_pos_iff.mpr hx), mul_add, ofReal_div, ofReal_div,
    mul_div_cancel₀ _ (ofReal_ne_zero.2 <| norm_ne_zero_iff.mpr hx), ← mul_assoc,
    mul_div_cancel₀ _ (ofReal_ne_zero.2 <| norm_ne_zero_iff.mpr hx), re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx : x ≠ 0
rw : cexp ((↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I) = x
rw₁ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + sin (↑x.arg : ℂ) * I) = x
rw₂ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + (↑(Real.sin x.arg) : ℂ) * I) = x
rw₃ : cexp (↑(Real.log ‖x‖) : ℂ) * (cos (↑x.arg : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₄ : cexp (↑(Real.log ‖x‖) : ℂ) * ((↑(Real.cos x.arg) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₅ : cexp (↑(Real.log ‖x‖) : ℂ) * ((↑(x.re / ‖x‖) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₆ : (↑(rexp (Real.log ‖x‖)) : ℂ) * ((↑(x.re / ‖x‖) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₇ : (↑‖x‖ : ℂ) * ((↑(x.re / ‖x‖) : ℂ) + (↑(x.im / ‖x‖) : ℂ) * I) = x
rw₈ : (↑‖x‖ : ℂ) * (↑(x.re / ‖x‖) : ℂ) + (↑‖x‖ : ℂ) * ((↑(x.im / ‖x‖) : ℂ) * I) = x
rw₉ : (↑‖x‖ : ℂ) * ((↑x.re : ℂ) / (↑‖x‖ : ℂ)) + (↑‖x‖ : ℂ) * ((↑(x.im / ‖x‖) : ℂ) * I) = x
rw₁₀ : (↑‖x‖ : ℂ) * ((↑x.re : ℂ) / (↑‖x‖ : ℂ)) + (↑‖x‖ : ℂ) * ((↑x.im : ℂ) / (↑‖x‖ : ℂ) * I) = x
rw₁₁ : (↑x.re : ℂ) + (↑‖x‖ : ℂ) * ((↑x.im : ℂ) / (↑‖x‖ : ℂ) * I) = x
rw₁₂ : (↑x.re : ℂ) + (↑‖x‖ : ℂ) * ((↑x.im : ℂ) / (↑‖x‖ : ℂ)) * I = x
rw₁₃ : (↑x.re : ℂ) + (↑x.im : ℂ) * I = x
⊢ cexp (log x) = x
have rw₁₄ : x = x
Tactic: rw [log, exp_add_mul_I, ← ofReal_sin, sin_arg, ← ofReal_cos, cos_arg hx, ← ofReal_exp,
    Real.exp_log (norm_pos_iff.mpr hx), mul_add, ofReal_div, ofReal_div,
    mul_div_cancel₀ _ (ofReal_ne_zero.2 <| norm_ne_zero_iff.mpr hx), ← mul_assoc,
    mul_div_cancel₀ _ (ofReal_ne_zero.2 <| norm_ne_zero_iff.mpr hx), re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
⊢ log (cexp x) = x
have rw : (↑(Real.log ‖cexp x‖) : ℂ) + (↑(cexp x).arg : ℂ) * I = x
Tactic: rw [log, norm_exp, Real.log_exp, exp_eq_exp_re_mul_sin_add_cos, ← ofReal_exp,
    arg_mul_cos_add_sin_mul_I (Real.exp_pos _) ⟨hx₁, hx₂⟩, re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
rw : (↑(Real.log ‖cexp x‖) : ℂ) + (↑(cexp x).arg : ℂ) * I = x
⊢ log (cexp x) = x
have rw₁ : (↑(Real.log (rexp x.re)) : ℂ) + (↑(cexp x).arg : ℂ) * I = x
Tactic: rw [log, norm_exp, Real.log_exp, exp_eq_exp_re_mul_sin_add_cos, ← ofReal_exp,
    arg_mul_cos_add_sin_mul_I (Real.exp_pos _) ⟨hx₁, hx₂⟩, re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
rw : (↑(Real.log ‖cexp x‖) : ℂ) + (↑(cexp x).arg : ℂ) * I = x
rw₁ : (↑(Real.log (rexp x.re)) : ℂ) + (↑(cexp x).arg : ℂ) * I = x
⊢ log (cexp x) = x
have rw₂ : (↑x.re : ℂ) + (↑(cexp x).arg : ℂ) * I = x
Tactic: rw [log, norm_exp, Real.log_exp, exp_eq_exp_re_mul_sin_add_cos, ← ofReal_exp,
    arg_mul_cos_add_sin_mul_I (Real.exp_pos _) ⟨hx₁, hx₂⟩, re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
rw : (↑(Real.log ‖cexp x‖) : ℂ) + (↑(cexp x).arg : ℂ) * I = x
rw₁ : (↑(Real.log (rexp x.re)) : ℂ) + (↑(cexp x).arg : ℂ) * I = x
rw₂ : (↑x.re : ℂ) + (↑(cexp x).arg : ℂ) * I = x
⊢ log (cexp x) = x
have rw₃ : (↑x.re : ℂ) + (↑(cexp (↑x.re : ℂ) * (cos (↑x.im : ℂ) + sin (↑x.im : ℂ) * I)).arg : ℂ) * I = x
Tactic: rw [log, norm_exp, Real.log_exp, exp_eq_exp_re_mul_sin_add_cos, ← ofReal_exp,
    arg_mul_cos_add_sin_mul_I (Real.exp_pos _) ⟨hx₁, hx₂⟩, re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
rw : (↑(Real.log ‖cexp x‖) : ℂ) + (↑(cexp x).arg : ℂ) * I = x
rw₁ : (↑(Real.log (rexp x.re)) : ℂ) + (↑(cexp x).arg : ℂ) * I = x
rw₂ : (↑x.re : ℂ) + (↑(cexp x).arg : ℂ) * I = x
rw₃ : (↑x.re : ℂ) + (↑(cexp (↑x.re : ℂ) * (cos (↑x.im : ℂ) + sin (↑x.im : ℂ) * I)).arg : ℂ) * I = x
⊢ log (cexp x) = x
have rw₄ : (↑x.re : ℂ) + (↑((↑(rexp x.re) : ℂ) * (cos (↑x.im : ℂ) + sin (↑x.im : ℂ) * I)).arg : ℂ) * I = x
Tactic: rw [log, norm_exp, Real.log_exp, exp_eq_exp_re_mul_sin_add_cos, ← ofReal_exp,
    arg_mul_cos_add_sin_mul_I (Real.exp_pos _) ⟨hx₁, hx₂⟩, re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
rw : (↑(Real.log ‖cexp x‖) : ℂ) + (↑(cexp x).arg : ℂ) * I = x
rw₁ : (↑(Real.log (rexp x.re)) : ℂ) + (↑(cexp x).arg : ℂ) * I = x
rw₂ : (↑x.re : ℂ) + (↑(cexp x).arg : ℂ) * I = x
rw₃ : (↑x.re : ℂ) + (↑(cexp (↑x.re : ℂ) * (cos (↑x.im : ℂ) + sin (↑x.im : ℂ) * I)).arg : ℂ) * I = x
rw₄ : (↑x.re : ℂ) + (↑((↑(rexp x.re) : ℂ) * (cos (↑x.im : ℂ) + sin (↑x.im : ℂ) * I)).arg : ℂ) * I = x
⊢ log (cexp x) = x
have rw₅ : (↑x.re : ℂ) + (↑x.im : ℂ) * I = x
Tactic: rw [log, norm_exp, Real.log_exp, exp_eq_exp_re_mul_sin_add_cos, ← ofReal_exp,
    arg_mul_cos_add_sin_mul_I (Real.exp_pos _) ⟨hx₁, hx₂⟩, re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
rw : (↑(Real.log ‖cexp x‖) : ℂ) + (↑(cexp x).arg : ℂ) * I = x
rw₁ : (↑(Real.log (rexp x.re)) : ℂ) + (↑(cexp x).arg : ℂ) * I = x
rw₂ : (↑x.re : ℂ) + (↑(cexp x).arg : ℂ) * I = x
rw₃ : (↑x.re : ℂ) + (↑(cexp (↑x.re : ℂ) * (cos (↑x.im : ℂ) + sin (↑x.im : ℂ) * I)).arg : ℂ) * I = x
rw₄ : (↑x.re : ℂ) + (↑((↑(rexp x.re) : ℂ) * (cos (↑x.im : ℂ) + sin (↑x.im : ℂ) * I)).arg : ℂ) * I = x
rw₅ : (↑x.re : ℂ) + (↑x.im : ℂ) * I = x
⊢ log (cexp x) = x
have rw₆ : x = x
Tactic: rw [log, norm_exp, Real.log_exp, exp_eq_exp_re_mul_sin_add_cos, ← ofReal_exp,
    arg_mul_cos_add_sin_mul_I (Real.exp_pos _) ⟨hx₁, hx₂⟩, re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
⊢ log (cexp x) = (↑x.re : ℂ) + (↑(toIocMod Real.two_pi_pos (-π) x.im) : ℂ) * I
have rw : (↑(Real.log ‖cexp x‖) : ℂ) + (↑(cexp x).arg : ℂ) * I = (↑x.re : ℂ) + (↑(toIocMod Real.two_pi_pos (-π) x.im) : ℂ) * I
Tactic: rw [log, norm_exp, Real.log_exp, arg_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
rw :
  (↑(Real.log ‖cexp x‖) : ℂ) + (↑(cexp x).arg : ℂ) * I = (↑x.re : ℂ) + (↑(toIocMod Real.two_pi_pos (-π) x.im) : ℂ) * I
⊢ log (cexp x) = (↑x.re : ℂ) + (↑(toIocMod Real.two_pi_pos (-π) x.im) : ℂ) * I
have rw₁ : (↑(Real.log (rexp x.re)) : ℂ) + (↑(cexp x).arg : ℂ) * I = (↑x.re : ℂ) + (↑(toIocMod Real.two_pi_pos (-π) x.im) : ℂ) * I
Tactic: rw [log, norm_exp, Real.log_exp, arg_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
rw :
  (↑(Real.log ‖cexp x‖) : ℂ) + (↑(cexp x).arg : ℂ) * I = (↑x.re : ℂ) + (↑(toIocMod Real.two_pi_pos (-π) x.im) : ℂ) * I
rw₁ :
  (↑(Real.log (rexp x.re)) : ℂ) + (↑(cexp x).arg : ℂ) * I =
    (↑x.re : ℂ) + (↑(toIocMod Real.two_pi_pos (-π) x.im) : ℂ) * I
⊢ log (cexp x) = (↑x.re : ℂ) + (↑(toIocMod Real.two_pi_pos (-π) x.im) : ℂ) * I
have rw₂ : (↑x.re : ℂ) + (↑(cexp x).arg : ℂ) * I = (↑x.re : ℂ) + (↑(toIocMod Real.two_pi_pos (-π) x.im) : ℂ) * I
Tactic: rw [log, norm_exp, Real.log_exp, arg_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
rw :
  (↑(Real.log ‖cexp x‖) : ℂ) + (↑(cexp x).arg : ℂ) * I = (↑x.re : ℂ) + (↑(toIocMod Real.two_pi_pos (-π) x.im) : ℂ) * I
rw₁ :
  (↑(Real.log (rexp x.re)) : ℂ) + (↑(cexp x).arg : ℂ) * I =
    (↑x.re : ℂ) + (↑(toIocMod Real.two_pi_pos (-π) x.im) : ℂ) * I
rw₂ : (↑x.re : ℂ) + (↑(cexp x).arg : ℂ) * I = (↑x.re : ℂ) + (↑(toIocMod Real.two_pi_pos (-π) x.im) : ℂ) * I
⊢ log (cexp x) = (↑x.re : ℂ) + (↑(toIocMod Real.two_pi_pos (-π) x.im) : ℂ) * I
have rw₃ : (↑x.re : ℂ) + (↑(toIocMod Real.two_pi_pos (-π) x.im) : ℂ) * I =
  (↑x.re : ℂ) + (↑(toIocMod Real.two_pi_pos (-π) x.im) : ℂ) * I
Tactic: rw [log, norm_exp, Real.log_exp, arg_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
⊢ log (cexp x) = x - (↑(toIocDiv Real.two_pi_pos (-π) x.im) : ℂ) * (2 * (↑π : ℂ) * I)
have rw : (↑x.re : ℂ) + (↑x.im : ℂ) * I - (↑(toIocDiv Real.two_pi_pos (-π) x.im • (2 * π)) : ℂ) * I =
  x - (↑(toIocDiv Real.two_pi_pos (-π) x.im) : ℂ) * (2 * (↑π : ℂ) * I)
Tactic: rw [log_exp_eq_re_add_toIocMod, toIocMod, ofReal_sub, sub_mul, ← add_sub_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x y : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
hy₁ : -π < y.im
hy₂ : y.im ≤ π
hxy : cexp x = cexp y
⊢ x = y
have rw : log (cexp x) = y
Tactic: rw [← log_exp hx₁ hx₂, ← log_exp hy₁ hy₂, hxy]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x y : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
hy₁ : -π < y.im
hy₂ : y.im ≤ π
hxy : cexp x = cexp y
rw : log (cexp x) = y
⊢ x = y
have rw₁ : log (cexp x) = log (cexp y)
Tactic: rw [← log_exp hx₁ hx₂, ← log_exp hy₁ hy₂, hxy]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x y : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
hy₁ : -π < y.im
hy₂ : y.im ≤ π
hxy : cexp x = cexp y
rw : log (cexp x) = y
rw₁ : log (cexp x) = log (cexp y)
⊢ x = y
have rw₂ : log (cexp y) = log (cexp y)
Tactic: rw [← log_exp hx₁ hx₂, ← log_exp hy₁ hy₂, hxy]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℝ
hx : 0 ≤ x
⊢ (↑(Real.log x) : ℂ).re = (log (↑x : ℂ)).re
have rw : (↑(Real.log x) : ℂ).re = Real.log ‖(↑x : ℂ)‖
Tactic: rw [log_re, ofReal_re, Complex.norm_of_nonneg hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℝ
hx : 0 ≤ x
rw : (↑(Real.log x) : ℂ).re = Real.log ‖(↑x : ℂ)‖
⊢ (↑(Real.log x) : ℂ).re = (log (↑x : ℂ)).re
have rw₁ : Real.log x = Real.log ‖(↑x : ℂ)‖
Tactic: rw [log_re, ofReal_re, Complex.norm_of_nonneg hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℝ
hx : 0 ≤ x
rw : (↑(Real.log x) : ℂ).re = Real.log ‖(↑x : ℂ)‖
rw₁ : Real.log x = Real.log ‖(↑x : ℂ)‖
⊢ (↑(Real.log x) : ℂ).re = (log (↑x : ℂ)).re
have rw₂ : Real.log x = Real.log x
Tactic: rw [log_re, ofReal_re, Complex.norm_of_nonneg hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℝ
hx : 0 ≤ x
⊢ (↑(Real.log x) : ℂ).im = (log (↑x : ℂ)).im
have rw : 0 = (log (↑x : ℂ)).im
Tactic: rw [ofReal_im, log_im, arg_ofReal_of_nonneg hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℝ
hx : 0 ≤ x
rw : 0 = (log (↑x : ℂ)).im
⊢ (↑(Real.log x) : ℂ).im = (log (↑x : ℂ)).im
have rw₁ : 0 = (↑x : ℂ).arg
Tactic: rw [ofReal_im, log_im, arg_ofReal_of_nonneg hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℝ
hx : 0 ≤ x
rw : 0 = (log (↑x : ℂ)).im
rw₁ : 0 = (↑x : ℂ).arg
⊢ (↑(Real.log x) : ℂ).im = (log (↑x : ℂ)).im
have rw₂ : Eq (α := ℝ) 0 0
Tactic: rw [ofReal_im, log_im, arg_ofReal_of_nonneg hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (hypothesis)
Goal:
r : ℝ
hr : 0 < r
x : ℂ
hx : x ≠ 0
⊢ log ((↑r : ℂ) * x) = (↑(Real.log r) : ℂ) + log x
have hx₁ : ‖x‖ ≠ 0
Tactic: replace hx := norm_ne_zero_iff.mpr hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
r : ℝ
hr : 0 < r
x : ℂ
hx : ‖x‖ ≠ 0
⊢ log ((↑r : ℂ) * x) = (↑(Real.log r) : ℂ) + log x
have simp_rw : (↑(Real.log ‖(↑r : ℂ) * x‖) : ℂ) + (↑((↑r : ℂ) * x).arg : ℂ) * I =
  (↑(Real.log r) : ℂ) + ((↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I)
Tactic: simp_rw [log, norm_mul, norm_real, arg_real_mul _ hr, Real.norm_of_nonneg hr.le,
    Real.log_mul hr.ne' hx, ofReal_add, add_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
r : ℝ
hr : 0 < r
x : ℂ
hx : ‖x‖ ≠ 0
simp_rw :
  (↑(Real.log ‖(↑r : ℂ) * x‖) : ℂ) + (↑((↑r : ℂ) * x).arg : ℂ) * I =
    (↑(Real.log r) : ℂ) + ((↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I)
⊢ log ((↑r : ℂ) * x) = (↑(Real.log r) : ℂ) + log x
have simp_rw₁ : (↑(Real.log (‖(↑r : ℂ)‖ * ‖x‖)) : ℂ) + (↑((↑r : ℂ) * x).arg : ℂ) * I =
  (↑(Real.log r) : ℂ) + ((↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I)
Tactic: simp_rw [log, norm_mul, norm_real, arg_real_mul _ hr, Real.norm_of_nonneg hr.le,
    Real.log_mul hr.ne' hx, ofReal_add, add_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
r : ℝ
hr : 0 < r
x : ℂ
hx : ‖x‖ ≠ 0
simp_rw :
  (↑(Real.log ‖(↑r : ℂ) * x‖) : ℂ) + (↑((↑r : ℂ) * x).arg : ℂ) * I =
    (↑(Real.log r) : ℂ) + ((↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I)
simp_rw₁ :
  (↑(Real.log (‖(↑r : ℂ)‖ * ‖x‖)) : ℂ) + (↑((↑r : ℂ) * x).arg : ℂ) * I =
    (↑(Real.log r) : ℂ) + ((↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I)
⊢ log ((↑r : ℂ) * x) = (↑(Real.log r) : ℂ) + log x
have simp_rw₂ : (↑(Real.log (‖r‖ * ‖x‖)) : ℂ) + (↑((↑r : ℂ) * x).arg : ℂ) * I =
  (↑(Real.log r) : ℂ) + ((↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I)
Tactic: simp_rw [log, norm_mul, norm_real, arg_real_mul _ hr, Real.norm_of_nonneg hr.le,
    Real.log_mul hr.ne' hx, ofReal_add, add_assoc]