∀ {R : Type u_2} [inst : CommRing R] (S : Type u_1) [inst_1 : CommRing S] [inst_2 : Algebra R S] {I : Ideal R},
  Function.LeftInverse
    (((TensorProduct.tensorQuotEquivQuotSMul S I).trans
              ((I • ⊤).quotEquivOfEq (Submodule.restrictScalars R (Ideal.map (algebraMap R S) I)) ⋯)).trans
          (Submodule.Quotient.restrictScalarsEquiv R (Ideal.map (algebraMap R S) I))).symm.invFun
    (↑(((TensorProduct.tensorQuotEquivQuotSMul S I).trans
                ((I • ⊤).quotEquivOfEq (Submodule.restrictScalars R (Ideal.map (algebraMap R S) I)) ⋯)).trans
            (Submodule.Quotient.restrictScalarsEquiv R (Ideal.map (algebraMap R S) I))).symm).toFun