∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (S T : Submodule R M)
  (h : S ≤ T) (x : M ⧸ S),
  (S.quotientQuotientEquivQuotientAux T h) (Submodule.Quotient.mk x) = (S.mapQ T LinearMap.id h) x