∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R]
  (motive : (∃ x, R ∙ (Submodule.subtype (IsLocalRing.maximalIdeal R)) x = IsLocalRing.maximalIdeal R) → Prop)
  (x : ∃ x, R ∙ (Submodule.subtype (IsLocalRing.maximalIdeal R)) x = IsLocalRing.maximalIdeal R),
  (∀ (x : ↥(IsLocalRing.maximalIdeal R))
      (h : R ∙ (Submodule.subtype (IsLocalRing.maximalIdeal R)) x = IsLocalRing.maximalIdeal R), motive ⋯) →
    motive x