[GOAL]
x : ℂ
⊢ (log x).re = Real.log (↑abs x)
[PROOFSTEP]
simp [log]
[GOAL]
x : ℂ
⊢ (log x).im = arg x
[PROOFSTEP]
simp [log]
[GOAL]
x : ℂ
⊢ -π < (log x).im
[PROOFSTEP]
simp only [log_im, neg_pi_lt_arg]
[GOAL]
x : ℂ
⊢ (log x).im ≤ π
[PROOFSTEP]
simp only [log_im, arg_le_pi]
[GOAL]
x : ℂ
hx : x ≠ 0
⊢ exp (log x) = x
[PROOFSTEP]
rw [log, exp_add_mul_I, ← ofReal_sin, sin_arg, ← ofReal_cos, cos_arg hx, ← ofReal_exp, Real.exp_log (abs.pos hx),
  mul_add, ofReal_div, ofReal_div, mul_div_cancel' _ (ofReal_ne_zero.2 <| abs.ne_zero hx), ← mul_assoc,
  mul_div_cancel' _ (ofReal_ne_zero.2 <| abs.ne_zero hx), re_add_im]
[GOAL]
x : ℂ
⊢ x ∈ Set.range exp → x ∈ {0}ᶜ
[PROOFSTEP]
rintro ⟨x, rfl⟩
[GOAL]
case intro
x : ℂ
⊢ exp x ∈ {0}ᶜ
[PROOFSTEP]
exact exp_ne_zero x
[GOAL]
x : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
⊢ log (exp x) = x
[PROOFSTEP]
rw [log, abs_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]
[GOAL]
x y : ℂ
hx₁ : -π < x.im
hx₂ : x.im ≤ π
hy₁ : -π < y.im
hy₂ : y.im ≤ π
hxy : exp x = exp y
⊢ x = y
[PROOFSTEP]
rw [← log_exp hx₁ hx₂, ← log_exp hy₁ hy₂, hxy]
[GOAL]
x : ℝ
hx : 0 ≤ x
⊢ (↑(Real.log x)).re = (log ↑x).re
[PROOFSTEP]
rw [log_re, ofReal_re, abs_of_nonneg hx]
[GOAL]
x : ℝ
hx : 0 ≤ x
⊢ (↑(Real.log x)).im = (log ↑x).im
[PROOFSTEP]
rw [ofReal_im, log_im, arg_ofReal_of_nonneg hx]
[GOAL]
x : ℝ
⊢ (log ↑x).re = Real.log x
[PROOFSTEP]
simp [log_re]
[GOAL]
r : ℝ
hr : 0 < r
x : ℂ
hx : x ≠ 0
⊢ log (↑r * x) = ↑(Real.log r) + log x
[PROOFSTEP]
replace hx := Complex.abs.ne_zero_iff.mpr hx
[GOAL]
r : ℝ
hr : 0 < r
x : ℂ
hx : ↑abs x ≠ 0
⊢ log (↑r * x) = ↑(Real.log r) + log x
[PROOFSTEP]
simp_rw [log, map_mul, abs_ofReal, arg_real_mul _ hr, abs_of_pos hr, Real.log_mul hr.ne' hx, ofReal_add, add_assoc]
[GOAL]
r : ℝ
hr : 0 < r
x : ℂ
hx : x ≠ 0
⊢ log (x * ↑r) = ↑(Real.log r) + log x
[PROOFSTEP]
rw [mul_comm, log_ofReal_mul hr hx, add_comm]
[GOAL]
⊢ log 0 = 0
[PROOFSTEP]
simp [log]
[GOAL]
⊢ log 1 = 0
[PROOFSTEP]
simp [log]
[GOAL]
⊢ log (-1) = ↑π * I
[PROOFSTEP]
simp [log]
[GOAL]
⊢ log I = ↑π / 2 * I
[PROOFSTEP]
simp [log]
[GOAL]
⊢ log (-I) = -(↑π / 2) * I
[PROOFSTEP]
simp [log]
[GOAL]
x : ℂ
⊢ log (↑(starRingEnd ℂ) x) = if arg x = π then log x else ↑(starRingEnd ℂ) (log x)
[PROOFSTEP]
simp_rw [log, abs_conj, arg_conj, map_add, map_mul, conj_ofReal]
[GOAL]
x : ℂ
⊢ ↑(Real.log (↑abs x)) + ↑(if arg x = π then π else -arg x) * I =
    if arg x = π then ↑(Real.log (↑abs x)) + ↑(arg x) * I else ↑(Real.log (↑abs x)) + ↑(arg x) * ↑(starRingEnd ℂ) I
[PROOFSTEP]
split_ifs with hx
[GOAL]
case pos
x : ℂ
hx : arg x = π
⊢ ↑(Real.log (↑abs x)) + ↑π * I = ↑(Real.log (↑abs x)) + ↑(arg x) * I
[PROOFSTEP]
rw [hx]
[GOAL]
case neg
x : ℂ
hx : ¬arg x = π
⊢ ↑(Real.log (↑abs x)) + ↑(-arg x) * I = ↑(Real.log (↑abs x)) + ↑(arg x) * ↑(starRingEnd ℂ) I
[PROOFSTEP]
simp_rw [ofReal_neg, conj_I, mul_neg, neg_mul]
[GOAL]
x : ℂ
h : arg x ≠ π
⊢ log (↑(starRingEnd ℂ) x) = ↑(starRingEnd ℂ) (log x)
[PROOFSTEP]
rw [log_conj_eq_ite, if_neg h]
[GOAL]
x : ℂ
⊢ log x⁻¹ = if arg x = π then -↑(starRingEnd ℂ) (log x) else -log x
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
x : ℂ
hx : x = 0
⊢ log x⁻¹ = if arg x = π then -↑(starRingEnd ℂ) (log x) else -log x
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
x : ℂ
hx : ¬x = 0
⊢ log x⁻¹ = if arg x = π then -↑(starRingEnd ℂ) (log x) else -log x
[PROOFSTEP]
rw [inv_def, log_mul_ofReal, Real.log_inv, ofReal_neg, ← sub_eq_neg_add, log_conj_eq_ite]
[GOAL]
case neg
x : ℂ
hx : ¬x = 0
⊢ (if arg x = π then log x else ↑(starRingEnd ℂ) (log x)) - ↑(Real.log (↑normSq x)) =
    if arg x = π then -↑(starRingEnd ℂ) (log x) else -log x
[PROOFSTEP]
simp_rw [log, map_add, map_mul, conj_ofReal, conj_I, normSq_eq_abs, Real.log_pow, Nat.cast_two, ofReal_mul, neg_add,
  mul_neg, neg_neg]
[GOAL]
case neg
x : ℂ
hx : ¬x = 0
⊢ (if arg x = π then ↑(Real.log (↑abs x)) + ↑(arg x) * I else ↑(Real.log (↑abs x)) + -(↑(arg x) * I)) -
      ↑2 * ↑(Real.log (↑abs x)) =
    if arg x = π then -↑(Real.log (↑abs x)) + ↑(arg x) * I else -↑(Real.log (↑abs x)) + -(↑(arg x) * I)
[PROOFSTEP]
norm_num
[GOAL]
case neg
x : ℂ
hx : ¬x = 0
⊢ (if arg x = π then ↑(Real.log (↑abs x)) + ↑(arg x) * I else ↑(Real.log (↑abs x)) + -(↑(arg x) * I)) -
      2 * ↑(Real.log (↑abs x)) =
    if arg x = π then -↑(Real.log (↑abs x)) + ↑(arg x) * I else -↑(Real.log (↑abs x)) + -(↑(arg x) * I)
[PROOFSTEP]
rw [two_mul]
  -- Porting note: added to simplify `↑2`
[GOAL]
case neg
x : ℂ
hx : ¬x = 0
⊢ (if arg x = π then ↑(Real.log (↑abs x)) + ↑(arg x) * I else ↑(Real.log (↑abs x)) + -(↑(arg x) * I)) -
      (↑(Real.log (↑abs x)) + ↑(Real.log (↑abs x))) =
    if arg x = π then -↑(Real.log (↑abs x)) + ↑(arg x) * I else -↑(Real.log (↑abs x)) + -(↑(arg x) * I)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
x : ℂ
hx : ¬x = 0
h✝ : arg x = π
⊢ ↑(Real.log (↑abs x)) + ↑(arg x) * I - (↑(Real.log (↑abs x)) + ↑(Real.log (↑abs x))) =
    -↑(Real.log (↑abs x)) + ↑(arg x) * I
[PROOFSTEP]
rw [add_sub_right_comm, sub_add_cancel']
[GOAL]
case neg
x : ℂ
hx : ¬x = 0
h✝ : ¬arg x = π
⊢ ↑(Real.log (↑abs x)) + -(↑(arg x) * I) - (↑(Real.log (↑abs x)) + ↑(Real.log (↑abs x))) =
    -↑(Real.log (↑abs x)) + -(↑(arg x) * I)
[PROOFSTEP]
rw [add_sub_right_comm, sub_add_cancel']
[GOAL]
case neg.hr
x : ℂ
hx : ¬x = 0
⊢ 0 < (↑normSq x)⁻¹
[PROOFSTEP]
rwa [inv_pos, Complex.normSq_pos]
[GOAL]
case neg.hx
x : ℂ
hx : ¬x = 0
⊢ ↑(starRingEnd ℂ) x ≠ 0
[PROOFSTEP]
rwa [map_ne_zero]
[GOAL]
x : ℂ
hx : arg x ≠ π
⊢ log x⁻¹ = -log x
[PROOFSTEP]
rw [log_inv_eq_ite, if_neg hx]
[GOAL]
⊢ 2 * ↑π * I ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
⊢ ¬(π = 0 ∨ I = 0)
[PROOFSTEP]
simp [Real.pi_ne_zero, I_ne_zero]
[GOAL]
x : ℂ
⊢ exp x = 1 ↔ ∃ n, x = ↑n * (2 * ↑π * I)
[PROOFSTEP]
constructor
[GOAL]
case mp
x : ℂ
⊢ exp x = 1 → ∃ n, x = ↑n * (2 * ↑π * I)
[PROOFSTEP]
intro h
[GOAL]
case mp
x : ℂ
h : exp x = 1
⊢ ∃ n, x = ↑n * (2 * ↑π * I)
[PROOFSTEP]
rcases existsUnique_add_zsmul_mem_Ioc Real.two_pi_pos x.im (-π) with ⟨n, hn, -⟩
[GOAL]
case mp.intro.intro
x : ℂ
h : exp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
⊢ ∃ n, x = ↑n * (2 * ↑π * I)
[PROOFSTEP]
use-n
[GOAL]
case h
x : ℂ
h : exp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
⊢ x = ↑(-n) * (2 * ↑π * I)
[PROOFSTEP]
rw [Int.cast_neg, neg_mul, eq_neg_iff_add_eq_zero]
[GOAL]
case h
x : ℂ
h : exp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
⊢ x + ↑n * (2 * ↑π * I) = 0
[PROOFSTEP]
have : (x + n * (2 * π * I)).im ∈ Set.Ioc (-π) π := by simpa [two_mul, mul_add] using hn
[GOAL]
x : ℂ
h : exp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
⊢ (x + ↑n * (2 * ↑π * I)).im ∈ Set.Ioc (-π) π
[PROOFSTEP]
simpa [two_mul, mul_add] using hn
[GOAL]
case h
x : ℂ
h : exp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
this : (x + ↑n * (2 * ↑π * I)).im ∈ Set.Ioc (-π) π
⊢ x + ↑n * (2 * ↑π * I) = 0
[PROOFSTEP]
rw [← log_exp this.1 this.2, exp_periodic.int_mul n, h, log_one]
[GOAL]
case mpr
x : ℂ
⊢ (∃ n, x = ↑n * (2 * ↑π * I)) → exp x = 1
[PROOFSTEP]
rintro ⟨n, rfl⟩
[GOAL]
case mpr.intro
n : ℤ
⊢ exp (↑n * (2 * ↑π * I)) = 1
[PROOFSTEP]
exact (exp_periodic.int_mul n).eq.trans exp_zero
[GOAL]
x y : ℂ
⊢ exp x = exp y ↔ exp (x - y) = 1
[PROOFSTEP]
rw [exp_sub, div_eq_one_iff_eq (exp_ne_zero _)]
[GOAL]
x y : ℂ
⊢ exp x = exp y ↔ ∃ n, x = y + ↑n * (2 * ↑π * I)
[PROOFSTEP]
simp only [exp_eq_exp_iff_exp_sub_eq_one, exp_eq_one_iff, sub_eq_iff_eq_add']
[GOAL]
s : Set ℂ
⊢ Set.Countable (exp ⁻¹' s) ↔ Set.Countable s
[PROOFSTEP]
refine' ⟨fun hs => _, fun hs => _⟩
[GOAL]
case refine'_1
s : Set ℂ
hs : Set.Countable (exp ⁻¹' s)
⊢ Set.Countable s
[PROOFSTEP]
refine' ((hs.image exp).insert 0).mono _
[GOAL]
case refine'_1
s : Set ℂ
hs : Set.Countable (exp ⁻¹' s)
⊢ s ⊆ insert 0 (exp '' (exp ⁻¹' s))
[PROOFSTEP]
rw [Set.image_preimage_eq_inter_range, range_exp, ← Set.diff_eq, ← Set.union_singleton, Set.diff_union_self]
[GOAL]
case refine'_1
s : Set ℂ
hs : Set.Countable (exp ⁻¹' s)
⊢ s ⊆ s ∪ {0}
[PROOFSTEP]
exact Set.subset_union_left _ _
[GOAL]
case refine'_2
s : Set ℂ
hs : Set.Countable s
⊢ Set.Countable (exp ⁻¹' s)
[PROOFSTEP]
rw [← Set.biUnion_preimage_singleton]
[GOAL]
case refine'_2
s : Set ℂ
hs : Set.Countable s
⊢ Set.Countable (⋃ (y : ℂ) (_ : y ∈ s), exp ⁻¹' {y})
[PROOFSTEP]
refine' hs.biUnion fun z hz => _
[GOAL]
case refine'_2
s : Set ℂ
hs : Set.Countable s
z : ℂ
hz : z ∈ s
⊢ Set.Countable (exp ⁻¹' {z})
[PROOFSTEP]
rcases em (∃ w, exp w = z) with (⟨w, rfl⟩ | hne)
[GOAL]
case refine'_2.inl.intro
s : Set ℂ
hs : Set.Countable s
w : ℂ
hz : exp w ∈ s
⊢ Set.Countable (exp ⁻¹' {exp w})
[PROOFSTEP]
simp only [Set.preimage, Set.mem_singleton_iff, exp_eq_exp_iff_exists_int, Set.setOf_exists]
[GOAL]
case refine'_2.inl.intro
s : Set ℂ
hs : Set.Countable s
w : ℂ
hz : exp w ∈ s
⊢ Set.Countable (⋃ (i : ℤ), {x | x = w + ↑i * (2 * ↑π * I)})
[PROOFSTEP]
exact Set.countable_iUnion fun m => Set.countable_singleton _
[GOAL]
case refine'_2.inr
s : Set ℂ
hs : Set.Countable s
z : ℂ
hz : z ∈ s
hne : ¬∃ w, exp w = z
⊢ Set.Countable (exp ⁻¹' {z})
[PROOFSTEP]
push_neg at hne 
[GOAL]
case refine'_2.inr
s : Set ℂ
hs : Set.Countable s
z : ℂ
hz : z ∈ s
hne : ∀ (w : ℂ), exp w ≠ z
⊢ Set.Countable (exp ⁻¹' {z})
[PROOFSTEP]
simp [Set.preimage, hne]
[GOAL]
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto log (𝓝[{z | z.im < 0}] z) (𝓝 (↑(Real.log (↑abs z)) - ↑π * I))
[PROOFSTEP]
convert
  (continuous_ofReal.continuousAt.comp_continuousWithinAt (continuous_abs.continuousWithinAt.log _)).tendsto.add
    (((continuous_ofReal.tendsto _).comp <| tendsto_arg_nhdsWithin_im_neg_of_re_neg_of_im_zero hre him).mul
      tendsto_const_nhds) using
  1
[GOAL]
case h.e'_5
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ 𝓝 (↑(Real.log (↑abs z)) - ↑π * I) = 𝓝 ((ofReal' ∘ fun x => Real.log (↑abs x)) z + ↑(-π) * I)
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
case convert_1
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ↑abs z ≠ 0
[PROOFSTEP]
lift z to ℝ using him
[GOAL]
case convert_1.intro
z : ℝ
hre : (↑z).re < 0
⊢ ↑abs ↑z ≠ 0
[PROOFSTEP]
simpa using hre.ne
[GOAL]
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ContinuousWithinAt log {z | 0 ≤ z.im} z
[PROOFSTEP]
convert
  (continuous_ofReal.continuousAt.comp_continuousWithinAt (continuous_abs.continuousWithinAt.log _)).tendsto.add
    ((continuous_ofReal.continuousAt.comp_continuousWithinAt <| continuousWithinAt_arg_of_re_neg_of_im_zero hre him).mul
      tendsto_const_nhds) using
  1
[GOAL]
case convert_1
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ↑abs z ≠ 0
[PROOFSTEP]
lift z to ℝ using him
[GOAL]
case convert_1.intro
z : ℝ
hre : (↑z).re < 0
⊢ ↑abs ↑z ≠ 0
[PROOFSTEP]
simpa using hre.ne
[GOAL]
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto log (𝓝[{z | 0 ≤ z.im}] z) (𝓝 (↑(Real.log (↑abs z)) + ↑π * I))
[PROOFSTEP]
simpa only [log, arg_eq_pi_iff.2 ⟨hre, him⟩] using (continuousWithinAt_log_of_re_neg_of_im_zero hre him).tendsto
[GOAL]
⊢ map exp (comap re atBot) = 𝓝[{0}ᶜ] 0
[PROOFSTEP]
rw [← comap_exp_nhds_zero, map_comap, range_exp, nhdsWithin]
[GOAL]
⊢ map exp (comap re atTop) = comap (↑abs) atTop
[PROOFSTEP]
rw [← comap_exp_comap_abs_atTop, map_comap, range_exp, inf_eq_left, le_principal_iff]
[GOAL]
⊢ {0}ᶜ ∈ comap (↑abs) atTop
[PROOFSTEP]
exact eventually_ne_of_tendsto_norm_atTop tendsto_comap 0
[GOAL]
α : Type u_1
x : ℂ
h : 0 < x.re ∨ x.im ≠ 0
⊢ ContinuousAt log x
[PROOFSTEP]
refine' ContinuousAt.add _ _
[GOAL]
case refine'_1
α : Type u_1
x : ℂ
h : 0 < x.re ∨ x.im ≠ 0
⊢ ContinuousAt (fun x => ↑(Real.log (↑Complex.abs x))) x
[PROOFSTEP]
refine' continuous_ofReal.continuousAt.comp _
[GOAL]
case refine'_1
α : Type u_1
x : ℂ
h : 0 < x.re ∨ x.im ≠ 0
⊢ ContinuousAt (fun x => Real.log (↑Complex.abs x)) x
[PROOFSTEP]
refine' (Real.continuousAt_log _).comp Complex.continuous_abs.continuousAt
[GOAL]
case refine'_1
α : Type u_1
x : ℂ
h : 0 < x.re ∨ x.im ≠ 0
⊢ ↑Complex.abs x ≠ 0
[PROOFSTEP]
rw [Complex.abs.ne_zero_iff]
[GOAL]
case refine'_1
α : Type u_1
x : ℂ
h : 0 < x.re ∨ x.im ≠ 0
⊢ x ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_1
α : Type u_1
h : 0 < 0.re ∨ 0.im ≠ 0
⊢ False
[PROOFSTEP]
simp at h 
[GOAL]
case refine'_2
α : Type u_1
x : ℂ
h : 0 < x.re ∨ x.im ≠ 0
⊢ ContinuousAt (fun x => ↑(arg x) * I) x
[PROOFSTEP]
have h_cont_mul : Continuous fun x : ℂ => x * I := continuous_id'.mul continuous_const
[GOAL]
case refine'_2
α : Type u_1
x : ℂ
h : 0 < x.re ∨ x.im ≠ 0
h_cont_mul : Continuous fun x => x * I
⊢ ContinuousAt (fun x => ↑(arg x) * I) x
[PROOFSTEP]
refine' h_cont_mul.continuousAt.comp (continuous_ofReal.continuousAt.comp _)
[GOAL]
case refine'_2
α : Type u_1
x : ℂ
h : 0 < x.re ∨ x.im ≠ 0
h_cont_mul : Continuous fun x => x * I
⊢ ContinuousAt (fun x => arg x) x
[PROOFSTEP]
exact continuousAt_arg h
