h : 0 < 0.re ∨ 0.im ≠ 0
⊢ False
x : ℂ
h : 0 < x.re ∨ x.im ≠ 0
⊢ x ≠ 0
rintro rfl
no goals
h : 0 < 0.re ∨ 0.im ≠ 0
⊢ False
simp [lt_irrefl] at h
no goals
x : ℂ
h : 0 < x.re ∨ x.im ≠ 0
h0 : x ≠ 0
⊢ HasStrictDerivAt (↑expLocalHomeomorph) x (↑(LocalHomeomorph.symm expLocalHomeomorph) x)
simpa [exp_log h0] using hasStrictDerivAt_exp (log x)