Theorem: ExpPiMulIHalf (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
⊢ cexp (↑(π / 2) * I) = I
Tactic:
rw [exp_mul_I]
State after:
⊢ (↑(π / 2)).cos + (↑(π / 2)).sin * I = I

State before:
⊢ (↑(π / 2)).cos + (↑(π / 2)).sin * I = I
Tactic:
simp only [ofReal_div, ofReal_ofNat, Complex.cos_pi_div_two, Complex.sin_pi_div_two, one_mul,
  zero_add]
State after:
no goals