∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {v : E} (hv : ‖v‖ = 1),
  stereographic hv =
    { toFun := stereoToFun v ∘ Subtype.val, invFun := stereoInvFun hv, source := {⟨v, ⋯⟩}ᶜ, target := Set.univ,
      map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯, open_source := ⋯, open_target := ⋯,
      continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ }