∀ {R : Type u_2} [inst : CommRing R] {O : Type u_1} [inst_1 : CommRing O] [inst_2 : Algebra O R] (u : Rˣ)
  (motive : (∃ x, (algebraMap O R) x = ↑u⁻¹) → Prop) (x : ∃ x, (algebraMap O R) x = ↑u⁻¹),
  (∀ (r2 : O) (hr2 : (algebraMap O R) r2 = ↑u⁻¹), motive ⋯) → motive x