∀ {R : Type u_2} {M : Type u_1} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : Submodule R M) (Q : Submodule R N) (f : M ≃ₗ[R] N)
  (hf : Submodule.map (↑f) P = Q) (x : M ⧸ P), (Q.mapQ P ↑f.symm ⋯) ((P.mapQ Q ↑f ⋯) x) = x