Mathlib: moving between sphere (0 : ℂ) 1 and Circle without an equivalence

Circle is defined as Submonoid.unitSphere ℂ, whose carrier is definitionally Metric.sphere (0 : ℂ) 1. So from u : sphere (0 : ℂ) 1 you get a Circle element by the anonymous constructor ⟨(u : ℂ), u.2⟩ : Circle, with no lemma needed. To compare Circle elements use Circle.ext on the ℂ coercions, together with Circle.coe_inv_eq_conj : ↑z⁻¹ = conj ↑z and Circle.norm_coe. This let me state that a sphere-valued map (the clutching function of the Hopf bundle along the equator) equals the loop ζ ↦ ζ ^ (-1 : ℤ) as a C(Circle, Circle): ext ζ, then change (… : ℂ) = ((ζ ^ (-1 : ℤ) : Circle) : ℂ), then rw [zpow_neg_one, Circle.coe_inv_eq_conj] and Complex.ext <;> simp. Continuity of the bundled map is easiest to get by first proving the function equals fun ζ ↦ ζ⁻¹ and using continuous_inv.