Exponential of reals are real - as a subset of complex

Stream: Is there code for X?

[Mark Gerads]

I would like [import all and librarysearch] to result in a solution for this problem. Here is a sorry minimal working example:

import data.complex.exponential

open complex

lemma expOfRealIsReal (z:ℂ) (zIsReal:z.im=0) : (exp z).im=0 :=
begin
  sorry,
end

[Heather Macbeth]

docs#complex.exp_of_real_im is this but with the hypothesis in a different format:

lemma expOfRealIsReal (b:ℂ) (bIsReal:b.im=0) : (exp b).im=0 :=
begin
  obtain ⟨x, y⟩ := b,
  have : y = 0 := bIsReal,
  rw this,
  exact exp_of_real_im x,
end

[Mark Gerads]

Thank you.