[GOAL]
⊢ ∀ ⦃x : ℂ⦄, x ∈ {z | z.im ∈ Ioo (-π) π} → exp x ∈ {z | 0 < z.re} ∪ {z | z.im ≠ 0}
[PROOFSTEP]
rintro ⟨x, y⟩ ⟨h₁ : -π < y, h₂ : y < π⟩
[GOAL]
case mk.intro
x y : ℝ
h₁ : -π < y
h₂ : y < π
⊢ exp { re := x, im := y } ∈ {z | 0 < z.re} ∪ {z | z.im ≠ 0}
[PROOFSTEP]
refine' (not_or_of_imp fun hz => _).symm
[GOAL]
case mk.intro
x y : ℝ
h₁ : -π < y
h₂ : y < π
hz : (exp { re := x, im := y }).im = 0
⊢ exp { re := x, im := y } ∈ {z | 0 < z.re}
[PROOFSTEP]
obtain rfl : y = 0 := by
  rw [exp_im] at hz 
  simpa [(Real.exp_pos _).ne', Real.sin_eq_zero_iff_of_lt_of_lt h₁ h₂] using hz
[GOAL]
x y : ℝ
h₁ : -π < y
h₂ : y < π
hz : (exp { re := x, im := y }).im = 0
⊢ y = 0
[PROOFSTEP]
rw [exp_im] at hz 
[GOAL]
x y : ℝ
h₁ : -π < y
h₂ : y < π
hz : Real.exp { re := x, im := y }.re * Real.sin { re := x, im := y }.im = 0
⊢ y = 0
[PROOFSTEP]
simpa [(Real.exp_pos _).ne', Real.sin_eq_zero_iff_of_lt_of_lt h₁ h₂] using hz
[GOAL]
case mk.intro
x : ℝ
h₁ : -π < 0
h₂ : 0 < π
hz : (exp { re := x, im := 0 }).im = 0
⊢ exp { re := x, im := 0 } ∈ {z | 0 < z.re}
[PROOFSTEP]
rw [mem_setOf_eq, ← ofReal_def, exp_ofReal_re]
[GOAL]
case mk.intro
x : ℝ
h₁ : -π < 0
h₂ : 0 < π
hz : (exp { re := x, im := 0 }).im = 0
⊢ 0 < Real.exp x
[PROOFSTEP]
exact Real.exp_pos x
[GOAL]
z : ℂ
h : z ∈ {z | 0 < z.re} ∪ {z | z.im ≠ 0}
⊢ log z ∈ {z | z.im ∈ Ioo (-π) π}
[PROOFSTEP]
simp only [mem_setOf, log_im, mem_Ioo, neg_pi_lt_arg, arg_lt_pi_iff, true_and]
[GOAL]
z : ℂ
h : z ∈ {z | 0 < z.re} ∪ {z | z.im ≠ 0}
⊢ 0 ≤ z.re ∨ z.im ≠ 0
[PROOFSTEP]
exact h.imp_left le_of_lt
[GOAL]
x : ℂ
hx : x ∈ {z | 0 < z.re} ∪ {z | z.im ≠ 0}
⊢ x ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
hx : 0 ∈ {z | 0 < z.re} ∪ {z | z.im ≠ 0}
⊢ False
[PROOFSTEP]
simp [lt_irrefl] at hx 
[GOAL]
x : ℂ
h : 0 < x.re ∨ x.im ≠ 0
⊢ x ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
h : 0 < 0.re ∨ 0.im ≠ 0
⊢ False
[PROOFSTEP]
simp [lt_irrefl] at h 
[GOAL]
x : ℂ
h : 0 < x.re ∨ x.im ≠ 0
h0 : x ≠ 0
⊢ HasStrictDerivAt (↑expLocalHomeomorph) x (↑(LocalHomeomorph.symm expLocalHomeomorph) x)
[PROOFSTEP]
simpa [exp_log h0] using hasStrictDerivAt_exp (log x)
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → ℂ
f' x : ℂ
h₁ : HasStrictDerivAt f f' x
h₂ : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasStrictDerivAt (fun t => log (f t)) (f' / f x) x
[PROOFSTEP]
rw [div_eq_inv_mul]
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → ℂ
f' x : ℂ
h₁ : HasStrictDerivAt f f' x
h₂ : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasStrictDerivAt (fun t => log (f t)) ((f x)⁻¹ * f') x
[PROOFSTEP]
exact (hasStrictDerivAt_log h₂).comp x h₁
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → ℂ
x : ℝ
f' : ℂ
h₁ : HasStrictDerivAt f f' x
h₂ : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasStrictDerivAt (fun t => log (f t)) (f' / f x) x
[PROOFSTEP]
simpa only [div_eq_inv_mul] using (hasStrictFDerivAt_log_real h₂).comp_hasStrictDerivAt x h₁
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → ℂ
f' x : ℂ
h₁ : HasDerivAt f f' x
h₂ : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasDerivAt (fun t => log (f t)) (f' / f x) x
[PROOFSTEP]
rw [div_eq_inv_mul]
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → ℂ
f' x : ℂ
h₁ : HasDerivAt f f' x
h₂ : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasDerivAt (fun t => log (f t)) ((f x)⁻¹ * f') x
[PROOFSTEP]
exact (hasStrictDerivAt_log h₂).hasDerivAt.comp x h₁
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → ℂ
x : ℝ
f' : ℂ
h₁ : HasDerivAt f f' x
h₂ : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasDerivAt (fun t => log (f t)) (f' / f x) x
[PROOFSTEP]
simpa only [div_eq_inv_mul] using (hasStrictFDerivAt_log_real h₂).hasFDerivAt.comp_hasDerivAt x h₁
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → ℂ
f' x : ℂ
s : Set ℂ
h₁ : HasDerivWithinAt f f' s x
h₂ : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasDerivWithinAt (fun t => log (f t)) (f' / f x) s x
[PROOFSTEP]
rw [div_eq_inv_mul]
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → ℂ
f' x : ℂ
s : Set ℂ
h₁ : HasDerivWithinAt f f' s x
h₂ : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasDerivWithinAt (fun t => log (f t)) ((f x)⁻¹ * f') s x
[PROOFSTEP]
exact (hasStrictDerivAt_log h₂).hasDerivAt.comp_hasDerivWithinAt x h₁
[GOAL]
α : Type u_1
inst✝² : TopologicalSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → ℂ
s : Set ℝ
x : ℝ
f' : ℂ
h₁ : HasDerivWithinAt f f' s x
h₂ : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasDerivWithinAt (fun t => log (f t)) (f' / f x) s x
[PROOFSTEP]
simpa only [div_eq_inv_mul] using (hasStrictFDerivAt_log_real h₂).hasFDerivAt.comp_hasDerivWithinAt x h₁
