MWE.lean

import Mathlib

namespace TensorProduct

variable {R P Q M : Type*} [CommRing R] [AddCommGroup P] [AddCommGroup Q]
    [AddCommGroup M] [Module R P] [Module R Q] [Module R M]

open LinearMap

theorem map₂_eq_range_lift_comp_mapIncl (f : P →ₗ[R] Q →ₗ[R] M)
    (p : Submodule R P) (q : Submodule R Q) :
    Submodule.map₂ f p q = LinearMap.range (lift f ∘ₗ mapIncl p q) := by
  simp_rw [LinearMap.range_comp, range_mapIncl, Submodule.map_span,
    Set.image_image2, Submodule.map₂_eq_span_image2, lift.tmul]

noncomputable def lTensor_ring_mod_ideal_equiv_mod_ideal_smul (I : Ideal R) :
    ((R⧸I) ⊗[R] M) ≃ₗ[R] M⧸(I • (⊤ : Submodule R M)) :=
  (rTensor.equiv _ (exact_subtype_mkQ I) I.mkQ_surjective).symm.trans <|
    Submodule.Quotient.equiv _ _ (TensorProduct.lid R M) <| by
      refine Eq.trans (LinearMap.range_comp _ _).symm ?_
      refine Eq.trans ?_ (map₂_eq_range_lift_comp_mapIncl _ _ _).symm
      refine Eq.trans ?_ (Submodule.map_top _)
      refine Eq.trans ?_ <| congrArg _ <|
        range_eq_top.mpr (Submodule.topEquiv.lTensor I).symm.surjective
      refine Eq.trans (congrArg range ?_) (LinearMap.range_comp _ _)
      ext; rfl

lemma lTensor_ring_mod_ideal_equiv_mod_ideal_smul_apply
    (I : Ideal R) (r : R) (x : M) :
    lTensor_ring_mod_ideal_equiv_mod_ideal_smul I
      (Ideal.Quotient.mk I r ⊗ₜ[R] _) = Submodule.mkQ (I • ⊤) (r • x) :=
  sorry

end TensorProduct