Real scalar as a ContinuousLinearEquiv on ℂ: smulLeft (Units.mk0 r h)

To get z ↦ R * z as an ℂ ≃L[ℝ] ℂ (for change-of-variables or degree lemmas that take an E ≃L[ℝ] E), use ContinuousLinearEquiv.smulLeft (Units.mk0 (R : ℂ) hR') with hR' : (R : ℂ) ≠ 0. Its application A z = ↑R * z holds by rfl. Downstream statements written as F (A z + c) and as F (R * z + c) are therefore defeq, and a final rfl closes goals that differ only in that respect. Getting (A : ℂ →L[ℝ] ℂ).det = normSq R: apply the holomorphic Jacobian lemma to (hasDerivAt_id 0).const_mul R. Rewrite the function to ⇑A with funext fun z ↦ rfl, then use A.fderiv (the ContinuousLinearEquiv version, not ContinuousLinearMap.fderiv, because the coercion is ⇑A). Separately, the inverse affine map x ↦ A.symm (x - b) is easiest to handle as an explicit function. Use A.toHomeomorph.trans (Homeomorph.addRight b) only for preimage_closure, preimage_frontier and isCompact_preimage.