Koqcl iso

lemma koqcl_iso {R : Type*} [CommRing R] [IsNoetherianRing R]{M : Type*} [Nontrivial M] [AddCommGroup M] [Module R M] [Module.Finite R M](I : {z: (ℒ R M) × (ℒ R M) // z.1 < z.2}) :∃ _ : LinearEquiv (RingHom.id R) (I.val.2⧸((ker_of_quot_comp_localization I).submoduleOf I.val.2))  ((I.val.2⧸(I.val.1.submoduleOf I.val.2))⧸ (LinearMap.ker (CP.f1 I))), True := by  unfold ker_of_quot_comp_localization  let S : Submodule R I.val.2 := I.val.1.submoduleOf I.val.2  let T : Submodule R I.val.2 := LinearMap.ker (CP.f1 I ∘ₗ CP.f2 I)  have hT_eq : T = Submodule.comap S.mkQ (LinearMap.ker (CP.f1 I)) := by    change LinearMap.ker (CP.f1 I ∘ₗ CP.f2 I) = _    rw [LinearMap.ker_comp]    rfl  have hST : S ≤ T := hT_eq ▸ Submodule.le_comap_mkQ _ _  have hsubT : T = (Submodule.map I.val.2.subtype T).submoduleOf I.val.2 :=    submoduleOf_map_subtype I.val.2 T  have hST' : S ≤ (Submodule.map I.val.2.subtype T).submoduleOf I.val.2 := hsubT ▸ hST  have hmap : Submodule.map S.mkQ ((Submodule.map I.val.2.subtype T).submoduleOf I.val.2) =      LinearMap.ker (CP.f1 I) := by    rw [← hsubT, hT_eq, Submodule.map_comap_eq_self (by rw [Submodule.range_mkQ]; exact le_top)]  exact ⟨hmap ▸ (Submodule.quotientQuotientEquivQuotient S _ hST').symm, trivial⟩