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