awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
⊢ (↑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:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
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)
rw₂ rw₃ : log (cexp y) = log (cexp y)
⊢ x = y

Tactic:
rw [← log_exp hx₁ hx₂, ← log_exp hy₁ hy₂, hxy]

Premises used: Complex.log_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℝ
hx : 0 ≤ x
rw : (↑(Real.log x) : ℂ).re = Real.log ‖(↑x : ℂ)‖
rw₁ : Real.log x = Real.log ‖(↑x : ℂ)‖
rw₂ rw₃ : Real.log x = Real.log x
⊢ (↑(Real.log x) : ℂ).re = (log (↑x : ℂ)).re

Tactic:
rw [log_re, ofReal_re, Complex.norm_of_nonneg hx]

Premises used: Complex.log_re, Complex.norm_of_nonneg, Complex.ofReal_re
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℝ
hx : 0 ≤ x
rw : 0 = (log (↑x : ℂ)).im
rw₁ : 0 = (↑x : ℂ).arg
rw₂ rw₃ : Eq (α := ℝ) 0 0
⊢ (↑(Real.log x) : ℂ).im = (log (↑x : ℂ)).im

Tactic:
rw [ofReal_im, log_im, arg_ofReal_of_nonneg hx]

Premises used: Complex.arg_ofReal_of_nonneg, Complex.log_im, Complex.ofReal_im
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
n : ℕ
⊢ (↑(Real.log (↑n : ℝ)) : ℂ) = log (↑n : ℂ)

Tactic:
ofReal_natCast n ▸ ofReal_log n.cast_nonneg

Premises used: Nat.cast_nonneg, Complex.ofReal_log, Eq.rec, Complex.ofReal_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ (↑(Real.log (OfNat.ofNat n)) : ℂ) = log (OfNat.ofNat n)

Tactic:
natCast_log

Premises used: Complex.natCast_log
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℝ
⊢ (log (↑x : ℂ)).re = Real.log x

Tactic:
simp [log_re]

Premises used: Complex.log_re
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
r : ℝ
hr : 0 < r
x : ℂ
hx : x ≠ 0
⊢ ‖x‖ ≠ 0

Tactic:
replace hx := norm_ne_zero_iff.mpr hx
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
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)
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

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]

Premises used: Complex.log, add_assoc, Complex.ofReal_add, LT.lt.le, norm_mul, Complex.norm_real, LT.lt.ne', Complex.arg_real_mul, Real.log_mul, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
r : ℝ
hr : 0 < r
x : ℂ
hx : x ≠ 0
rw : log ((↑r : ℂ) * x) = (↑(Real.log r) : ℂ) + log x
rw₁ rw₂ : (↑(Real.log r) : ℂ) + log x = (↑(Real.log r) : ℂ) + log x
⊢ log (x * (↑r : ℂ)) = (↑(Real.log r) : ℂ) + log x

Tactic:
rw [mul_comm, log_ofReal_mul hr hx]

Premises used: Complex.log_ofReal_mul, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x y : ℂ
hx₀ : x ≠ 0
hy₀ : y ≠ 0
⊢ log (x * y) = log x + log y ↔ x.arg + y.arg ∈ Ioc (-π) π

Tactic:
Complex.ext_iff.trans <| Iff.trans ?_ <| arg_mul_eq_add_arg_iff hx₀ hy₀

Premises used: Complex.arg_mul_eq_add_arg_iff, Complex.ext_iff, Iff.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x y : ℂ
hx₀ : x ≠ 0
hy₀ : y ≠ 0
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
⊢ log (x * y) = log x + log y ↔ x.arg + y.arg ∈ Ioc (-π) π

Tactic:
refine Complex.ext_iff.trans <| Iff.trans ?_ <| arg_mul_eq_add_arg_iff hx₀ hy₀

Premises used: Complex.arg_mul_eq_add_arg_iff, Complex.ext_iff, Iff.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
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
simp_rw₅ : True ∧ (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

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]

Premises used: Iff.mpr, Complex.log_re, Complex.add_im, Complex.add_re, norm_mul, norm_ne_zero_iff, Complex.log_im, Real.log_mul, true_and
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
⊢ log 0 = 0

Tactic:
simp [log]

Premises used: Complex.log
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
⊢ log 1 = 0

Tactic:
simp [log]

Premises used: Complex.log
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
⊢ log (x / x) = 0

Tactic:
simp [log]

Premises used: Complex.log
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
⊢ log (-1) = (↑π : ℂ) * I

Tactic:
simp [log]

Premises used: Complex.log
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
⊢ log I = (↑π : ℂ) / 2 * I

Tactic:
simp [log]

Premises used: Complex.log
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
⊢ log (-I) = -((↑π : ℂ) / 2) * I

Tactic:
simp [log]

Premises used: Complex.log
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
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 : ℂ)
⊢ log ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = if x.arg = π then log x else (starRingEnd ℂ : (a : ℂ) → ℂ) (log x)

Tactic:
simp_rw [log, norm_conj, arg_conj, map_add, map_mul, conj_ofReal]

Premises used: Complex.norm_conj, Complex.log, map_add, Complex.arg_conj, map_mul, Complex.conj_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
pos : ∀ (hx : x.arg = π), (↑(Real.log ‖x‖) : ℂ) + (↑π : ℂ) * I = (↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I
neg :
  ∀ (hx : ¬x.arg = π),
    (↑(Real.log ‖x‖) : ℂ) + (↑(-x.arg) : ℂ) * I =
      (↑(Real.log ‖x‖) : ℂ) + HMul.hMul (β := ℂ) (↑x.arg : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) 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 : ℂ)

Tactic:
split_ifs with hx
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
hx : x.arg = π
pos pos₁ : (↑(Real.log ‖x‖) : ℂ) + (↑π : ℂ) * I = (↑(Real.log ‖x‖) : ℂ) + (↑π : ℂ) * I
⊢ (↑(Real.log ‖x‖) : ℂ) + (↑π : ℂ) * I = (↑(Real.log ‖x‖) : ℂ) + (↑x.arg : ℂ) * I

Tactic:
rw [hx]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
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
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 : ℂ)

Tactic:
simp_rw [ofReal_neg, conj_I, mul_neg, neg_mul]

Premises used: Complex.ofReal_neg, neg_mul, Complex.conj_I, mul_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
h : x.arg ≠ π
rw : (if x.arg = π then log x else (starRingEnd ℂ : (a : ℂ) → ℂ) (log x)) = (starRingEnd ℂ : (a : ℂ) → ℂ) (log x)
rw₁ rw₂ : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log x) : ℂ)
⊢ log ((starRingEnd ℂ : (a : ℂ) → ℂ) x) = (starRingEnd ℂ : (a : ℂ) → ℂ) (log x)

Tactic:
rw [log_conj_eq_ite, if_neg h]

Premises used: Complex.log_conj_eq_ite, if_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
pos : ∀ (hx : x = 0), log x⁻¹ = if x.arg = π then -(starRingEnd ℂ : (a : ℂ) → ℂ) (log x) else -log x
neg : ∀ (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

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
hx : x = 0
⊢ log x⁻¹ = if x.arg = π then -(starRingEnd ℂ : (a : ℂ) → ℂ) (log x) else -log x

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
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)⁻¹ : ℝ)
neg₂ : Ne (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) (0 : ℂ)
⊢ log 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]

Premises used: Complex.log_conj_eq_ite, sub_eq_neg_add, Complex.ofReal_neg, Complex.inv_def, Complex.log_mul_ofReal, Real.log_inv
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
hx : ¬x = 0
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)
⊢ (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:
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]

Premises used: Complex.log, Complex.normSq_eq_norm_sq, neg_add, map_add, neg_neg, map_mul, Real.log_pow, Complex.conj_ofReal, Nat.cast_two, Complex.conj_I, Complex.ofReal_mul, mul_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
hx : ¬x = 0
⊢ (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:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
hx : ¬x = 0
neg : LT.lt (α := ℝ) (0 : ℝ) ((normSq : (a : ℂ) → ℝ) x : ℝ)
neg₁ neg₂ neg₃ neg₄ : x ≠ 0
⊢ LT.lt (α := ℝ) (0 : ℝ) (((normSq : (a : ℂ) → ℝ) x)⁻¹ : ℝ)

Tactic:
rwa [inv_pos, Complex.normSq_pos]

Premises used: Complex.normSq_pos, inv_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
hx : ¬x = 0
neg neg₁ neg₂ neg₃ : x ≠ 0
⊢ Ne (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) x : ℂ) (0 : ℂ)

Tactic:
rwa [map_ne_zero]

Premises used: map_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
hx : x.arg ≠ π
rw : (if x.arg = π then -(starRingEnd ℂ : (a : ℂ) → ℂ) (log x) else -log x) = -log x
rw₁ rw₂ : -log x = -log x
⊢ log x⁻¹ = -log x

Tactic:
rw [log_inv_eq_ite, if_neg hx]

Premises used: Complex.log_inv_eq_ite, if_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
⊢ 2 * (↑π : ℂ) * I ≠ 0

Tactic:
simp [Real.pi_ne_zero, I_ne_zero]

Premises used: Complex.I_ne_zero, Real.pi_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
mp : cexp x = 1 → ∃ (n : ℤ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
mpr : (∃ (n : ℤ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)) → cexp x = 1
⊢ cexp x = 1 ↔ ∃ (n : ℤ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
h : cexp x = 1
mp : ∀ (n : ℤ) (hn : x.im + n • (2 * π) ∈ Ioc (-π) (-π + 2 * π)), ∃ (n : ℤ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
⊢ ∃ (n : ℤ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)

Tactic:
rcases existsUnique_add_zsmul_mem_Ioc Real.two_pi_pos x.im (-π) with ⟨n, hn, -⟩

Premises used: Real.pi, existsUnique_add_zsmul_mem_Ioc, Complex.im, Real.two_pi_pos, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
h₁ : x = (↑(-n) : ℂ) * (2 * (↑π : ℂ) * I)
⊢ ∃ (n : ℤ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)

Tactic:
use -n
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
h₁ : x + (↑n : ℂ) * (2 * (↑π : ℂ) * I) = 0
⊢ x = (↑(-n) : ℂ) * (2 * (↑π : ℂ) * I)

Tactic:
rw [Int.cast_neg, neg_mul, eq_neg_iff_add_eq_zero]

Premises used: Int.cast_neg, neg_mul, eq_neg_iff_add_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
⊢ (x + (↑n : ℂ) * (2 * (↑π : ℂ) * I)).im ∈ Ioc (-π) π

Tactic:
simpa [two_mul, mul_add] using hn

Premises used: two_mul, mul_add
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
⊢ (x + (↑n : ℂ) * (2 * (↑π : ℂ) * I)).im ∈ Ioc (-π) π

Tactic:
have : (x + n * (2 * π * I)).im ∈ Set.Ioc (-π) π := by simpa [two_mul, mul_add] using hn
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
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
h₄ h₅ : Eq (α := ℂ) 0 0
⊢ x + (↑n : ℂ) * (2 * (↑π : ℂ) * I) = 0

Tactic:
rw [← log_exp this.1 this.2, exp_periodic.int_mul n, h, log_one]

Premises used: Complex.log_one, Function.Periodic.int_mul, Complex.exp_periodic, Complex.log_exp, And.right, And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
n : ℤ
⊢ cexp ((↑n : ℂ) * (2 * (↑π : ℂ) * I)) = 1

Tactic:
(exp_periodic.int_mul n).eq.trans exp_zero

Premises used: Function.Periodic.int_mul, Complex.exp_zero, Complex.exp_periodic, Function.Periodic.eq, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
n : ℤ
⊢ cexp ((↑n : ℂ) * (2 * (↑π : ℂ) * I)) = 1

Tactic:
exact (exp_periodic.int_mul n).eq.trans exp_zero

Premises used: Function.Periodic.int_mul, Complex.exp_zero, Complex.exp_periodic, Function.Periodic.eq, Eq.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
hx : 0 ≤ x.im
rw : (∃ (n : ℤ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)) ↔ ∃ (n : ℕ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
⊢ cexp x = 1 ↔ ∃ (n : ℕ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)

Tactic:
rw [exp_eq_one_iff]

Premises used: Complex.exp_eq_one_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
hx : 0 ≤ x.im
h : ∃ (n : ℕ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
n : ℕ
hn : x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
rw : (↑n : ℂ) * (2 * (↑π : ℂ) * I) = (↑(↑n : ℤ) : ℂ) * (2 * (↑π : ℂ) * I)
⊢ x = (↑(↑n : ℤ) : ℂ) * (2 * (↑π : ℂ) * I)

Tactic:
rw [hn]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
hx : 0 ≤ x.im
h : ∃ (n : ℕ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
n : ℕ
hn : x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : (↑n : ℂ) * ((↑(2 * π) : ℂ) * I) = (↑n : ℂ) * ((↑(2 * π) : ℂ) * I)
⊢ (↑n : ℂ) * (2 * (↑π : ℂ) * I) = (↑(↑n : ℤ) : ℂ) * (2 * (↑π : ℂ) * I)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
hx : 0 ≤ x.im
refine :
  (∃ (n : ℤ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)) →
    ∀ (n : ℤ) (hn : x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)), ∃ (n : ℕ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
⊢ (∃ (n : ℤ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)) ↔ ∃ (n : ℕ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)

Tactic:
refine ⟨fun ⟨n, hn⟩ ↦ ?_, fun ⟨n, hn⟩ ↦ ⟨n, by rw [hn]; norm_cast⟩⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
hx : 0 ≤ x.im
h : ∃ (n : ℤ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
n : ℤ
hn : x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
⊢ 0 ≤ (↑n : ℝ) * (2 * π)

Tactic:
simpa [hn] using hx
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
hx : 0 ≤ x.im
h : ∃ (n : ℤ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
n : ℤ
hn : x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
⊢ 0 ≤ (↑n : ℝ) * (2 * π)

Tactic:
have : 0 ≤ n * (2 * π) := by simpa [hn] using hx
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
hx : 0 ≤ x.im
h : ∃ (n : ℤ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
n : ℤ
hn : x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
this : 0 ≤ (↑n : ℝ) * (2 * π)
⊢ 0 < 2 * π

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
hx : 0 ≤ x.im
h : ∃ (n : ℤ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
n : ℤ
hn : x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
this : 0 ≤ (↑n : ℝ) * (2 * π)
⊢ 0 ≤ n

Tactic:
exact_mod_cast nonneg_of_mul_nonneg_left this (by positivity)

Premises used: nonneg_of_mul_nonneg_left
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
hx : 0 ≤ x.im
h : ∃ (n : ℤ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
n : ℤ
hn : x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
this : 0 ≤ (↑n : ℝ) * (2 * π)
lift :
  ∀ (n : ℕ) (hn : x = (↑(↑n : ℤ) : ℂ) * (2 * (↑π : ℂ) * I)) (this : 0 ≤ (↑(↑n : ℤ) : ℝ) * (2 * π)),
    ∃ (n : ℕ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
⊢ ∃ (n : ℕ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)

Tactic:
lift n to ℕ using by exact_mod_cast nonneg_of_mul_nonneg_left this (by positivity)
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
hx : 0 ≤ x.im
h : ∃ (n : ℤ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
n : ℕ
hn : x = (↑(↑n : ℤ) : ℂ) * (2 * (↑π : ℂ) * I)
this : 0 ≤ (↑(↑n : ℤ) : ℝ) * (2 * π)
⊢ ∃ (n : ℕ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)

Tactic:
⟨n, hn⟩

Premises used: Exists.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x : ℂ
hx : 0 ≤ x.im
h : ∃ (n : ℤ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)
n : ℕ
hn : x = (↑(↑n : ℤ) : ℂ) * (2 * (↑π : ℂ) * I)
this : 0 ≤ (↑(↑n : ℤ) : ℝ) * (2 * π)
⊢ ∃ (n : ℕ), x = (↑n : ℂ) * (2 * (↑π : ℂ) * I)

Tactic:
exact ⟨n, hn⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
k N : ℕ
hN : N ≠ 0
rw : (∃ (n : ℤ), 2 * (↑π : ℂ) * I * (↑k : ℂ) / (↑N : ℂ) = (↑n : ℂ) * (2 * (↑π : ℂ) * I)) ↔ N ∣ k
⊢ cexp (2 * (↑π : ℂ) * I * (↑k : ℂ) / (↑N : ℂ)) = 1 ↔ N ∣ k

Tactic:
rw [exp_eq_one_iff]

Premises used: Complex.exp_eq_one_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
k N : ℕ
hN : N ≠ 0
n : ℤ
⊢ 2 * (↑π : ℂ) * I ≠ 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
k N : ℕ
hN : N ≠ 0
n : ℤ
rw : HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑N : ℂ) = (↑n : ℂ)
| 2 * (↑π : ℂ) * I * (↑k : ℂ) / (↑N : ℂ) = (↑n : ℂ) * (2 * (↑π : ℂ) * I)

Tactic:
rw [← mul_comm (2 * π * I), mul_div_assoc, mul_right_inj' (by simp)]

Premises used: Real.pi, HMul.hMul, mul_div_assoc, Complex.ofReal, mul_comm, mul_right_inj', OfNat.ofNat, Complex.I
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
k N : ℕ
hN : N ≠ 0
conv : (∃ (n : ℤ), HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑N : ℂ) = (↑n : ℂ)) ↔ N ∣ k
⊢ (∃ (n : ℤ), 2 * (↑π : ℂ) * I * (↑k : ℂ) / (↑N : ℂ) = (↑n : ℂ) * (2 * (↑π : ℂ) * I)) ↔ N ∣ k

Tactic:
conv in _ = _ => rw [← mul_comm (2 * π * I), mul_div_assoc, mul_right_inj' (by simp)]

Premises used: Real.pi, HMul.hMul, mul_div_assoc, Complex.ofReal, mul_comm, mul_right_inj', OfNat.ofNat, Complex.I
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
k N : ℕ
hN : N ≠ 0
field_simp : (∃ (n : ℤ), (↑k : ℂ) = HMul.hMul (α := ℂ) (↑N : ℂ) (↑n : ℂ)) ↔ N ∣ k
⊢ (∃ (n : ℤ), HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑N : ℂ) = (↑n : ℂ)) ↔ N ∣ k

Tactic:
field_simp [Nat.cast_ne_zero.mpr hN]

Premises used: Iff.mpr, Nat.cast_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
k N : ℕ
hN : N ≠ 0
norm_cast : (∃ (n : ℤ), (↑k : ℤ) = (↑N : ℤ) * n) ↔ N ∣ k
⊢ (∃ (n : ℤ), (↑k : ℂ) = HMul.hMul (α := ℂ) (↑N : ℂ) (↑n : ℂ)) ↔ N ∣ k

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
k N : ℕ
hN : N ≠ 0
⊢ (∃ (n : ℤ), (↑k : ℤ) = (↑N : ℤ) * n) ↔ N ∣ k

Tactic:
simp [← dvd_def, Int.ofNat_dvd]

Premises used: dvd_def, Int.ofNat_dvd
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x y : ℂ
rw : cexp x = cexp y ↔ cexp x / cexp y = 1
rw₁ rw₂ : cexp x = cexp y ↔ cexp x = cexp y
⊢ cexp x = cexp y ↔ cexp (x - y) = 1

Tactic:
rw [exp_sub, div_eq_one_iff_eq (exp_ne_zero _)]

Premises used: Complex.exp_ne_zero, div_eq_one_iff_eq, Complex.exp_sub
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x y : ℂ
⊢ cexp x = cexp y ↔ ∃ (n : ℤ), x = y + (↑n : ℂ) * (2 * (↑π : ℂ) * I)

Tactic:
simp only [exp_eq_exp_iff_exp_sub_eq_one, exp_eq_one_iff, sub_eq_iff_eq_add']

Premises used: Complex.exp_eq_exp_iff_exp_sub_eq_one, Complex.exp_eq_one_iff, sub_eq_iff_eq_add'
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x y : ℂ
h : cexp x = cexp y
obtain : ∀ (n : ℤ) (hn : x = y + (↑n : ℂ) * (2 * (↑π : ℂ) * I)), x.re = y.re
⊢ x.re = y.re

Tactic:
obtain ⟨n, hn⟩ := exp_eq_exp_iff_exists_int.1 h

Premises used: Complex.exp_eq_exp_iff_exists_int, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
x y : ℂ
h : cexp x = cexp y
n : ℤ
hn : x = y + (↑n : ℂ) * (2 * (↑π : ℂ) * I)
⊢ x.re = y.re

Tactic:
simp [hn]
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
z : ℂ
rw : cexp z ≠ 0
⊢ ∃ (n : ℤ), log (cexp z) = z + (↑n : ℂ) * (2 * (↑π : ℂ) * I)

Tactic:
rw [← exp_eq_exp_iff_exists_int, exp_log]

Premises used: Complex.exp_eq_exp_iff_exists_int, Complex.exp_log
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
z : ℂ
⊢ cexp z ≠ 0

Tactic:
exp_ne_zero z

Premises used: Complex.exp_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
z : ℂ
⊢ cexp z ≠ 0

Tactic:
exact exp_ne_zero z

Premises used: Complex.exp_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
s : Set ℂ
⊢ (cexp ⁻¹' s).Countable ↔ s.Countable

Tactic:
⟨fun hs => ?_, fun hs => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
s : Set ℂ
refine_1 : ∀ (hs : (cexp ⁻¹' s).Countable), s.Countable
refine_2 : ∀ (hs : s.Countable), (cexp ⁻¹' s).Countable
⊢ (cexp ⁻¹' s).Countable ↔ s.Countable

Tactic:
refine ⟨fun hs => ?_, fun hs => ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
s : Set ℂ
hs : (cexp ⁻¹' s).Countable
⊢ s.Countable

Tactic:
((hs.image exp).insert 0).mono ?_

Premises used: Set.Countable.image, Set.Countable.mono, Set.Countable.insert, Complex.exp, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Complex.Log
Goal:
s : Set ℂ
hs : (cexp ⁻¹' s).Countable
refine_1 : s ⊆ insert 0 (cexp '' cexp ⁻¹' s)
⊢ s.Countable

Tactic:
refine ((hs.image exp).insert 0).mono ?_

Premises used: Set.Countable.image, Set.Countable.mono, Set.Countable.insert, Complex.exp, OfNat.ofNat