x y : ℝ
h : ↑(Complex.exp ↑x).re = ↑0
⊢ Complex.exp ↑x = 0
x y : ℝ
h : exp x = 0
⊢ Complex.exp ↑x = 0
rw [exp, ← ofReal_inj] at h
no goals
x y : ℝ
h : ↑(Complex.exp ↑x).re = ↑0
⊢ Complex.exp ↑x = 0
simp_all