awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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‖)) : ℂ) + (↑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)
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‖)) : ℂ) + (↑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‖)) : ℂ) + (↑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)
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‖)) : ℂ) + (↑x.arg : ℂ) * I = (↑(Real.log r) : ℂ) + ((↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I)
simp_rw₄ :
  (↑(Real.log (r * ‖x‖)) : ℂ) + (↑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 + Real.log ‖x‖) : ℂ) + (↑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)
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‖)) : ℂ) + (↑x.arg : ℂ) * I = (↑(Real.log r) : ℂ) + ((↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I)
simp_rw₄ :
  (↑(Real.log (r * ‖x‖)) : ℂ) + (↑x.arg : ℂ) * I = (↑(Real.log r) : ℂ) + ((↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I)
simp_rw₅ :
  (↑(Real.log r + Real.log ‖x‖) : ℂ) + (↑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) : ℂ) + (↑(Real.log ‖x‖) : ℂ) + (↑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
⊢ log (x * (↑r : ℂ)) = (↑(Real.log r) : ℂ) + log x
have rw : log ((↑r : ℂ) * x) = (↑(Real.log r) : ℂ) + log x
Tactic: rw [mul_comm, log_ofReal_mul hr hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
r : ℝ
hr : 0 < r
x : ℂ
hx : x ≠ 0
rw : log ((↑r : ℂ) * x) = (↑(Real.log r) : ℂ) + log x
⊢ log (x * (↑r : ℂ)) = (↑(Real.log r) : ℂ) + log x
have rw₁ : (↑(Real.log r) : ℂ) + log x = (↑(Real.log r) : ℂ) + log x
Tactic: rw [mul_comm, log_ofReal_mul hr hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x y : ℂ
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ log (x * y) = log x + log y ↔ x.arg + y.arg ∈ Ioc (-π) π
have refine : (log (x * y)).re = (log x + log y).re ∧ (log (x * y)).im = (log x + log y).im ↔ (x * y).arg = x.arg + y.arg
Tactic: refine Complex.ext_iff.trans <| Iff.trans ?_ <| arg_mul_eq_add_arg_iff hx₀ hy₀
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x y : ℂ
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ (log (x * y)).re = (log x + log y).re ∧ (log (x * y)).im = (log x + log y).im ↔ (x * y).arg = x.arg + y.arg
have simp_rw : (log (x * y)).re = (log x).re + (log y).re ∧ (log (x * y)).im = (log x + log y).im ↔ (x * y).arg = x.arg + y.arg
Tactic: simp_rw [add_re, add_im, log_re, log_im, norm_mul,
    Real.log_mul (norm_ne_zero_iff.mpr hx₀) (norm_ne_zero_iff.mpr hy₀), true_and]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x y : ℂ
hx₀ : x ≠ 0
hy₀ : y ≠ 0
simp_rw :
  (log (x * y)).re = (log x).re + (log y).re ∧ (log (x * y)).im = (log x + log y).im ↔ (x * y).arg = x.arg + y.arg
⊢ (log (x * y)).re = (log x + log y).re ∧ (log (x * y)).im = (log x + log y).im ↔ (x * y).arg = x.arg + y.arg
have simp_rw₁ : (log (x * y)).re = (log x).re + (log y).re ∧ (log (x * y)).im = (log x).im + (log y).im ↔ (x * y).arg = x.arg + y.arg
Tactic: simp_rw [add_re, add_im, log_re, log_im, norm_mul,
    Real.log_mul (norm_ne_zero_iff.mpr hx₀) (norm_ne_zero_iff.mpr hy₀), true_and]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x y : ℂ
hx₀ : x ≠ 0
hy₀ : y ≠ 0
simp_rw :
  (log (x * y)).re = (log x).re + (log y).re ∧ (log (x * y)).im = (log x + log y).im ↔ (x * y).arg = x.arg + y.arg
simp_rw₁ :
  (log (x * y)).re = (log x).re + (log y).re ∧ (log (x * y)).im = (log x).im + (log y).im ↔ (x * y).arg = x.arg + y.arg
⊢ (log (x * y)).re = (log x + log y).re ∧ (log (x * y)).im = (log x + log y).im ↔ (x * y).arg = x.arg + y.arg
have simp_rw₂ : Real.log ‖x * y‖ = Real.log ‖x‖ + Real.log ‖y‖ ∧ (log (x * y)).im = (log x).im + (log y).im ↔
  (x * y).arg = x.arg + y.arg
Tactic: simp_rw [add_re, add_im, log_re, log_im, norm_mul,
    Real.log_mul (norm_ne_zero_iff.mpr hx₀) (norm_ne_zero_iff.mpr hy₀), true_and]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x y : ℂ
hx₀ : x ≠ 0
hy₀ : y ≠ 0
simp_rw :
  (log (x * y)).re = (log x).re + (log y).re ∧ (log (x * y)).im = (log x + log y).im ↔ (x * y).arg = x.arg + y.arg
simp_rw₁ :
  (log (x * y)).re = (log x).re + (log y).re ∧ (log (x * y)).im = (log x).im + (log y).im ↔ (x * y).arg = x.arg + y.arg
simp_rw₂ :
  Real.log ‖x * y‖ = Real.log ‖x‖ + Real.log ‖y‖ ∧ (log (x * y)).im = (log x).im + (log y).im ↔
    (x * y).arg = x.arg + y.arg
⊢ (log (x * y)).re = (log x + log y).re ∧ (log (x * y)).im = (log x + log y).im ↔ (x * y).arg = x.arg + y.arg
have simp_rw₃ : Real.log ‖x * y‖ = Real.log ‖x‖ + Real.log ‖y‖ ∧ (x * y).arg = x.arg + y.arg ↔ (x * y).arg = x.arg + y.arg
Tactic: simp_rw [add_re, add_im, log_re, log_im, norm_mul,
    Real.log_mul (norm_ne_zero_iff.mpr hx₀) (norm_ne_zero_iff.mpr hy₀), true_and]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x y : ℂ
hx₀ : x ≠ 0
hy₀ : y ≠ 0
simp_rw :
  (log (x * y)).re = (log x).re + (log y).re ∧ (log (x * y)).im = (log x + log y).im ↔ (x * y).arg = x.arg + y.arg
simp_rw₁ :
  (log (x * y)).re = (log x).re + (log y).re ∧ (log (x * y)).im = (log x).im + (log y).im ↔ (x * y).arg = x.arg + y.arg
simp_rw₂ :
  Real.log ‖x * y‖ = Real.log ‖x‖ + Real.log ‖y‖ ∧ (log (x * y)).im = (log x).im + (log y).im ↔
    (x * y).arg = x.arg + y.arg
simp_rw₃ : Real.log ‖x * y‖ = Real.log ‖x‖ + Real.log ‖y‖ ∧ (x * y).arg = x.arg + y.arg ↔ (x * y).arg = x.arg + y.arg
⊢ (log (x * y)).re = (log x + log y).re ∧ (log (x * y)).im = (log x + log y).im ↔ (x * y).arg = x.arg + y.arg
have simp_rw₄ : Real.log (‖x‖ * ‖y‖) = Real.log ‖x‖ + Real.log ‖y‖ ∧ (x * y).arg = x.arg + y.arg ↔ (x * y).arg = x.arg + y.arg
Tactic: simp_rw [add_re, add_im, log_re, log_im, norm_mul,
    Real.log_mul (norm_ne_zero_iff.mpr hx₀) (norm_ne_zero_iff.mpr hy₀), true_and]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x y : ℂ
hx₀ : x ≠ 0
hy₀ : y ≠ 0
simp_rw :
  (log (x * y)).re = (log x).re + (log y).re ∧ (log (x * y)).im = (log x + log y).im ↔ (x * y).arg = x.arg + y.arg
simp_rw₁ :
  (log (x * y)).re = (log x).re + (log y).re ∧ (log (x * y)).im = (log x).im + (log y).im ↔ (x * y).arg = x.arg + y.arg
simp_rw₂ :
  Real.log ‖x * y‖ = Real.log ‖x‖ + Real.log ‖y‖ ∧ (log (x * y)).im = (log x).im + (log y).im ↔
    (x * y).arg = x.arg + y.arg
simp_rw₃ : Real.log ‖x * y‖ = Real.log ‖x‖ + Real.log ‖y‖ ∧ (x * y).arg = x.arg + y.arg ↔ (x * y).arg = x.arg + y.arg
simp_rw₄ :
  Real.log (‖x‖ * ‖y‖) = Real.log ‖x‖ + Real.log ‖y‖ ∧ (x * y).arg = x.arg + y.arg ↔ (x * y).arg = x.arg + y.arg
⊢ (log (x * y)).re = (log x + log y).re ∧ (log (x * y)).im = (log x + log y).im ↔ (x * y).arg = x.arg + y.arg
have simp_rw₅ : True ∧ (x * y).arg = x.arg + y.arg ↔ (x * y).arg = x.arg + y.arg
Tactic: simp_rw [add_re, add_im, log_re, log_im, norm_mul,
    Real.log_mul (norm_ne_zero_iff.mpr hx₀) (norm_ne_zero_iff.mpr hy₀), true_and]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
⊢ log ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = if x.arg = π then log x else (starRingEnd ℂ : (a : ℂ) → ℂ) (log x)
have simp_rw : (↑(Real.log ‖x‖) : ℂ) + (↑(if x.arg = π then π else -x.arg) : ℂ) * I =
  if x.arg = π then (↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I
  else (↑(Real.log ‖x‖) : ℂ) + HMul.hMul (β := ℂ) (↑x.arg : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) I : ℂ)
Tactic: simp_rw [log, norm_conj, arg_conj, map_add, map_mul, conj_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
⊢ (↑(Real.log ‖x‖) : ℂ) + (↑(if x.arg = π then π else -x.arg) : ℂ) * I =
    if x.arg = π then (↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I
    else (↑(Real.log ‖x‖) : ℂ) + HMul.hMul (β := ℂ) (↑x.arg : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) I : ℂ)
have pos : ∀ (hx : x.arg = π), (↑(Real.log ‖x‖) : ℂ) + (↑π : ℂ) * I = (↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I
Tactic: split_ifs with hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
pos : ∀ (hx : x.arg = π), (↑(Real.log ‖x‖) : ℂ) + (↑π : ℂ) * I = (↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I
⊢ (↑(Real.log ‖x‖) : ℂ) + (↑(if x.arg = π then π else -x.arg) : ℂ) * I =
    if x.arg = π then (↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I
    else (↑(Real.log ‖x‖) : ℂ) + HMul.hMul (β := ℂ) (↑x.arg : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) I : ℂ)
have neg : ∀ (hx : ¬x.arg = π),
  (↑(Real.log ‖x‖) : ℂ) + (↑(-x.arg) : ℂ) * I =
    (↑(Real.log ‖x‖) : ℂ) + HMul.hMul (β := ℂ) (↑x.arg : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) I : ℂ)
Tactic: split_ifs with hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx : x.arg = π
⊢ (↑(Real.log ‖x‖) : ℂ) + (↑π : ℂ) * I = (↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I
have pos : (↑(Real.log ‖x‖) : ℂ) + (↑π : ℂ) * I = (↑(Real.log ‖x‖) : ℂ) + (↑π : ℂ) * I
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx : ¬x.arg = π
⊢ (↑(Real.log ‖x‖) : ℂ) + (↑(-x.arg) : ℂ) * I =
    (↑(Real.log ‖x‖) : ℂ) + HMul.hMul (β := ℂ) (↑x.arg : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) I : ℂ)
have neg : (↑(Real.log ‖x‖) : ℂ) + -(↑x.arg : ℂ) * I =
  (↑(Real.log ‖x‖) : ℂ) + HMul.hMul (β := ℂ) (↑x.arg : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) I : ℂ)
Tactic: simp_rw [ofReal_neg, conj_I, mul_neg, neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx : ¬x.arg = π
neg :
  (↑(Real.log ‖x‖) : ℂ) + -(↑x.arg : ℂ) * I =
    (↑(Real.log ‖x‖) : ℂ) + HMul.hMul (β := ℂ) (↑x.arg : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) I : ℂ)
⊢ (↑(Real.log ‖x‖) : ℂ) + (↑(-x.arg) : ℂ) * I =
    (↑(Real.log ‖x‖) : ℂ) + HMul.hMul (β := ℂ) (↑x.arg : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) I : ℂ)
have neg₁ : (↑(Real.log ‖x‖) : ℂ) + -(↑x.arg : ℂ) * I = (↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * -I
Tactic: simp_rw [ofReal_neg, conj_I, mul_neg, neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx : ¬x.arg = π
neg :
  (↑(Real.log ‖x‖) : ℂ) + -(↑x.arg : ℂ) * I =
    (↑(Real.log ‖x‖) : ℂ) + HMul.hMul (β := ℂ) (↑x.arg : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) I : ℂ)
neg₁ : (↑(Real.log ‖x‖) : ℂ) + -(↑x.arg : ℂ) * I = (↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * -I
⊢ (↑(Real.log ‖x‖) : ℂ) + (↑(-x.arg) : ℂ) * I =
    (↑(Real.log ‖x‖) : ℂ) + HMul.hMul (β := ℂ) (↑x.arg : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) I : ℂ)
have neg₂ : (↑(Real.log ‖x‖) : ℂ) + -(↑x.arg : ℂ) * I = (↑(Real.log ‖x‖) : ℂ) + -((↑x.arg : ℂ) * I)
Tactic: simp_rw [ofReal_neg, conj_I, mul_neg, neg_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
h : x.arg ≠ π
⊢ log ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (log x)
have rw : (if x.arg = π then log x else (starRingEnd ℂ : (a : ℂ) → ℂ) (log x)) = (starRingEnd ℂ : (a : ℂ) → ℂ) (log x)
Tactic: rw [log_conj_eq_ite, if_neg h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
h : x.arg ≠ π
rw : (if x.arg = π then log x else (starRingEnd ℂ : (a : ℂ) → ℂ) (log x)) = (starRingEnd ℂ : (a : ℂ) → ℂ) (log x)
⊢ log ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (log x)
have rw₁ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ)
Tactic: rw [log_conj_eq_ite, if_neg h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
⊢ log x⁻¹ = if x.arg = π then -(starRingEnd ℂ : (a : ℂ) → ℂ) (log x) else -log x
have pos : ∀ (hx : x = 0), log x⁻¹ = if x.arg = π then -(starRingEnd ℂ : (a : ℂ) → ℂ) (log x) else -log x
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
pos : ∀ (hx : x = 0), log x⁻¹ = if x.arg = π then -(starRingEnd ℂ : (a : ℂ) → ℂ) (log x) else -log x
⊢ log x⁻¹ = if x.arg = π then -(starRingEnd ℂ : (a : ℂ) → ℂ) (log x) else -log x
have neg : ∀ (hx : ¬x = 0), log x⁻¹ = if x.arg = π then -(starRingEnd ℂ : (a : ℂ) → ℂ) (log x) else -log x
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx : ¬x = 0
⊢ log x⁻¹ = if x.arg = π then -(starRingEnd ℂ : (a : ℂ) → ℂ) (log x) else -log x
have neg : (if x.arg = π then log x else (starRingEnd ℂ : (a : ℂ) → ℂ) (log x)) - (↑(Real.log ((normSq : (a : ℂ) → ℝ) x)) : ℂ) =
  if x.arg = π then -(starRingEnd ℂ : (a : ℂ) → ℂ) (log x) else -log x
Tactic: rw [inv_def, log_mul_ofReal, Real.log_inv, ofReal_neg, ← sub_eq_neg_add, log_conj_eq_ite]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx : ¬x = 0
neg :
  (if x.arg = π then log x else (starRingEnd ℂ : (a : ℂ) → ℂ) (log x)) - (↑(Real.log ((normSq : (a : ℂ) → ℝ) x)) : ℂ) =
    if x.arg = π then -(starRingEnd ℂ : (a : ℂ) → ℂ) (log x) else -log x
⊢ log x⁻¹ = if x.arg = π then -(starRingEnd ℂ : (a : ℂ) → ℂ) (log x) else -log x
have neg₁ : LT.lt (α := ℝ) (0 : ℝ) (((normSq : (a : ℂ) → ℝ) x)⁻¹ : ℝ)
Tactic: rw [inv_def, log_mul_ofReal, Real.log_inv, ofReal_neg, ← sub_eq_neg_add, log_conj_eq_ite]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx : ¬x = 0
neg :
  (if x.arg = π then log x else (starRingEnd ℂ : (a : ℂ) → ℂ) (log x)) - (↑(Real.log ((normSq : (a : ℂ) → ℝ) x)) : ℂ) =
    if x.arg = π then -(starRingEnd ℂ : (a : ℂ) → ℂ) (log x) else -log x
neg₁ : LT.lt (α := ℝ) (0 : ℝ) (((normSq : (a : ℂ) → ℝ) x)⁻¹ : ℝ)
⊢ log x⁻¹ = if x.arg = π then -(starRingEnd ℂ : (a : ℂ) → ℂ) (log x) else -log x
have neg₂ : Ne (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) (0 : ℂ)
Tactic: rw [inv_def, log_mul_ofReal, Real.log_inv, ofReal_neg, ← sub_eq_neg_add, log_conj_eq_ite]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx : ¬x = 0
⊢ (if x.arg = π then log x else (starRingEnd ℂ : (a : ℂ) → ℂ) (log x)) - (↑(Real.log ((normSq : (a : ℂ) → ℝ) x)) : ℂ) =
    if x.arg = π then -(starRingEnd ℂ : (a : ℂ) → ℂ) (log x) else -log x
have neg : (if x.arg = π then (↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I else (↑(Real.log ‖x‖) : ℂ) + -((↑x.arg : ℂ) * I)) -
    (↑2 : ℂ) * (↑(Real.log ‖x‖) : ℂ) =
  if x.arg = π then -(↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I else -(↑(Real.log ‖x‖) : ℂ) + -((↑x.arg : ℂ) * I)
Tactic: simp_rw [log, map_add, map_mul, conj_ofReal, conj_I, normSq_eq_norm_sq, Real.log_pow,
      Nat.cast_two, ofReal_mul, neg_add, mul_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx : ¬x = 0
⊢ LT.lt (α := ℝ) (0 : ℝ) (((normSq : (a : ℂ) → ℝ) x)⁻¹ : ℝ)
have neg : LT.lt (α := ℝ) (0 : ℝ) ((normSq : (a : ℂ) → ℝ) x : ℝ)
Tactic: rwa [inv_pos, Complex.normSq_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx : ¬x = 0
neg : LT.lt (α := ℝ) (0 : ℝ) ((normSq : (a : ℂ) → ℝ) x : ℝ)
⊢ LT.lt (α := ℝ) (0 : ℝ) (((normSq : (a : ℂ) → ℝ) x)⁻¹ : ℝ)
have neg₁ : x ≠ 0
Tactic: rwa [inv_pos, Complex.normSq_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx : ¬x = 0
⊢ Ne (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) (0 : ℂ)
have neg : x ≠ 0
Tactic: rwa [map_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx : x.arg ≠ π
⊢ log x⁻¹ = -log x
have rw : (if x.arg = π then -(starRingEnd ℂ : (a : ℂ) → ℂ) (log x) else -log x) = -log x
Tactic: rw [log_inv_eq_ite, if_neg hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx : x.arg ≠ π
rw : (if x.arg = π then -(starRingEnd ℂ : (a : ℂ) → ℂ) (log x) else -log x) = -log x
⊢ log x⁻¹ = -log x
have rw₁ : -log x = -log x
Tactic: rw [log_inv_eq_ite, if_neg hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
⊢ cexp x = 1 ↔ ∃ (n : ℤ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
have mp : cexp x = 1 → ∃ (n : ℤ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
mp : cexp x = 1 → ∃ (n : ℤ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
⊢ cexp x = 1 ↔ ∃ (n : ℤ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
have mpr : (∃ (n : ℤ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)) → cexp x = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
h : cexp x = 1
⊢ ∃ (n : ℤ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
have mp : ∀ (n : ℤ) (hn : x.im + n • (2 * π) ∈ Ioc (-π) (-π + 2 * π)), ∃ (n : ℤ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
Tactic: rcases existsUnique_add_zsmul_mem_Ioc Real.two_pi_pos x.im (-π) with ⟨n, hn, -⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
⊢ ∃ (n : ℤ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
have h₁ : x = (↑(-n) : ℂ) * (2 * (↑π : ℂ) * I)
Tactic: use -n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
⊢ x = (↑(-n) : ℂ) * (2 * (↑π : ℂ) * I)
have h₁ : x + (↑n : ℂ) * (2 * (↑π : ℂ) * I) = 0
Tactic: rw [Int.cast_neg, neg_mul, eq_neg_iff_add_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (hypothesis)
Goal:
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
⊢ x + (↑n : ℂ) * (2 * (↑π : ℂ) * I) = 0
have this : (x + (↑n : ℂ) * (2 * (↑π : ℂ) * I)).im ∈ Ioc (-π) π
Tactic: have : (x + n * (2 * π * I)).im ∈ Set.Ioc (-π) π := by simpa [two_mul, mul_add] using hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
this : (x + (↑n : ℂ) * (2 * (↑π : ℂ) * I)).im ∈ Ioc (-π) π
⊢ x + (↑n : ℂ) * (2 * (↑π : ℂ) * I) = 0
have h₁ : log (cexp (x + (↑n : ℂ) * (2 * (↑π : ℂ) * I))) = 0
Tactic: rw [← log_exp this.1 this.2, exp_periodic.int_mul n, h, log_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
this : (x + (↑n : ℂ) * (2 * (↑π : ℂ) * I)).im ∈ Ioc (-π) π
h₁ : log (cexp (x + (↑n : ℂ) * (2 * (↑π : ℂ) * I))) = 0
⊢ x + (↑n : ℂ) * (2 * (↑π : ℂ) * I) = 0
have h₂ : log (cexp x) = 0
Tactic: rw [← log_exp this.1 this.2, exp_periodic.int_mul n, h, log_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
this : (x + (↑n : ℂ) * (2 * (↑π : ℂ) * I)).im ∈ Ioc (-π) π
h₁ : log (cexp (x + (↑n : ℂ) * (2 * (↑π : ℂ) * I))) = 0
h₂ : log (cexp x) = 0
⊢ x + (↑n : ℂ) * (2 * (↑π : ℂ) * I) = 0
have h₃ : log 1 = 0
Tactic: rw [← log_exp this.1 this.2, exp_periodic.int_mul n, h, log_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
this : (x + (↑n : ℂ) * (2 * (↑π : ℂ) * I)).im ∈ Ioc (-π) π
h₁ : log (cexp (x + (↑n : ℂ) * (2 * (↑π : ℂ) * I))) = 0
h₂ : log (cexp x) = 0
h₃ : log 1 = 0
⊢ x + (↑n : ℂ) * (2 * (↑π : ℂ) * I) = 0
have h₄ : Eq (α := ℂ) 0 0
Tactic: rw [← log_exp this.1 this.2, exp_periodic.int_mul n, h, log_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx : 0 ≤ x.im
⊢ cexp x = 1 ↔ ∃ (n : ℕ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
have rw : (∃ (n : ℤ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)) ↔ ∃ (n : ℕ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
Tactic: rw [exp_eq_one_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx : 0 ≤ x.im
h : ∃ (n : ℕ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
n : ℕ
hn : x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
⊢ x = (↑(↑n : ℤ) : ℂ) * (2 * (↑π : ℂ) * I)
have rw : (↑n : ℂ) * (2 * (↑π : ℂ) * I) = (↑(↑n : ℤ) : ℂ) * (2 * (↑π : ℂ) * I)
Tactic: rw [hn]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx : 0 ≤ x.im
h : ∃ (n : ℕ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
n : ℕ
hn : x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
⊢ (↑n : ℂ) * (2 * (↑π : ℂ) * I) = (↑(↑n : ℤ) : ℂ) * (2 * (↑π : ℂ) * I)
have norm_cast : (↑n : ℂ) * ((↑(2 * π) : ℂ) * I) = (↑n : ℂ) * ((↑(2 * π) : ℂ) * I)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (goal)
Goal:
x : ℂ
hx : 0 ≤ x.im
⊢ (∃ (n : ℤ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)) ↔ ∃ (n : ℕ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
have refine : (∃ (n : ℤ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)) →
  ∀ (n : ℤ) (hn : x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)), ∃ (n : ℕ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
Tactic: refine ⟨fun ⟨n, hn⟩ ↦ ?_, fun ⟨n, hn⟩ ↦ ⟨n, by rw [hn]; norm_cast⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Complex.Log (hypothesis)
Goal:
x : ℂ
hx : 0 ≤ x.im
h : ∃ (n : ℤ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
n : ℤ
hn : x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
⊢ ∃ (n : ℕ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
have this : 0 ≤ (↑n : ℝ) * (2 * π)
Tactic: have : 0 ≤ n * (2 * π) := by simpa [hn] using hx