{K : Type u_1} →
  [inst : DivisionRing K] →
    [inst_1 : TopologicalSpace K] →
      {motive : IsTopologicalDivisionRing K → Sort u} →
        ([toIsTopologicalRing : IsTopologicalRing K] → [toContinuousInv₀ : ContinuousInv₀ K] → motive ⋯) →
          (t : IsTopologicalDivisionRing K) → motive t