∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {Ms : ι → Type u_3} [inst_1 : (i : ι) → AddCommGroup (Ms i)]
  [inst_2 : (i : ι) → Module R (Ms i)] {N : Type u_4} [inst_3 : AddCommGroup N] [inst_4 : Module R N]
  [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] (p : (i : ι) → Submodule R (Ms i)) (q : Submodule R N)
  (f : (i : ι) → Ms i →ₗ[R] N) (hf : ∀ (i : ι), p i ≤ Submodule.comap (f i) q) (i : ι) (x : Ms i ⧸ p i),
  (Submodule.piQuotientLift p q f hf) (Pi.single i x) = ((p i).mapQ q (f i) ⋯) x