cases' p with pangle pmag
p : Polar
hpmag : p.magnitude > 0
hpangle1 : -(Real.pi / 2) < p.angle
hpangle2 : p.angle < Real.pi / 2
⊢ Complex.toPolar (Polar.toComplex p) = p
case mk
pangle pmag : ℝ
hpmag : { angle := pangle, magnitude := pmag }.magnitude > 0
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
⊢ Complex.toPolar (Polar.toComplex { angle := pangle, magnitude := pmag }) = { angle := pangle, magnitude := pmag }