{ rw [mul_div_mul_left]
  rw [← Real.tan_eq_sin_div_cos]
  rw [Real.arctan_tan]
  all_goals aesop }
case mk.left
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.arctan (pmag * Real.sin pangle / (pmag * Real.cos pangle)) = pangle

case mk.right
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.sqrt ((pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2) = pmag
case mk.right
pangle pmag : ℝ
hpangle1 : -(Real.pi / 2) < { angle := pangle, magnitude := pmag }.angle
hpangle2 : { angle := pangle, magnitude := pmag }.angle < Real.pi / 2
hpmag : 0 < pmag
⊢ Real.sqrt ((pmag * Real.cos pangle) ^ 2 + (pmag * Real.sin pangle) ^ 2) = pmag