Theorem: Rectangle.symm_re (PrimeNumberTheoremAnd/Rectangle.lean)

State before:
z w : ℂ
c : ℝ
⊢ Rectangle (↑w.re + ↑z.im * I) (↑z.re + ↑w.im * I) = Rectangle z w
Tactic:
simp [Rectangle, uIcc_comm]
State after:
no goals