∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R]
  (motive : (¬IsField R ∧ ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical) → Prop)
  (x : ¬IsField R ∧ ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical),
  (∀ (hn : ¬IsField R) (h : ∀ (x : R), x ≠ 0 → IsLocalRing.maximalIdeal R ≤ (Ideal.span {x}).radical), motive ⋯) →
    motive x