∀ (R : Type u_1) [inst : Ring R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R)
  (g : ↥I →ₗ[R] ULift.{u_3, u_2} M)
  (motive : (∃ g', ∀ (x : R) (mem : x ∈ I), g' x = (↑ULift.moduleEquiv ∘ₗ g) ⟨x, mem⟩) → Prop)
  (x : ∃ g', ∀ (x : R) (mem : x ∈ I), g' x = (↑ULift.moduleEquiv ∘ₗ g) ⟨x, mem⟩),
  (∀ (g' : R →ₗ[R] M) (hg' : ∀ (x : R) (mem : x ∈ I), g' x = (↑ULift.moduleEquiv ∘ₗ g) ⟨x, mem⟩), motive ⋯) → motive x