-- Module: Mathlib.RingTheory.Ideal.CotangentBaseChange
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
I : Ideal S
a : S →+* T ⊗[R] S := AlgHom.toRingHom Algebra.TensorProduct.includeRight
t : T
x : ↥(Submodule.restrictScalars R I)
h :
  Eq (α :=
    T ⊗[R] S ⧸
      HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ)
        (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I) 2)
    ((cotangentToQuotientSquare (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I) :
          (a : (map Algebra.TensorProduct.includeRight.toRingHom I).Cotangent) →
            T ⊗[R] S ⧸ map Algebra.TensorProduct.includeRight.toRingHom I ^ 2)
        ((tensorCotangentHom R T I :
            (a : T ⊗[R] I.Cotangent) → (map Algebra.TensorProduct.includeRight.toRingHom I).Cotangent)
          (t ⊗ₜ[R] (I.toCotangent : (a : ↥I) → I.Cotangent) x)) :
      T ⊗[R] S ⧸
        HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ)
          (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I) 2)
    ((cotangentToQuotientSquare (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I) :
          (a : (map Algebra.TensorProduct.includeRight.toRingHom I).Cotangent) →
            T ⊗[R] S ⧸ map Algebra.TensorProduct.includeRight.toRingHom I ^ 2)
        ((toCotangent (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I) :
            (a : ↥(map Algebra.TensorProduct.includeRight.toRingHom I)) →
              (map Algebra.TensorProduct.includeRight.toRingHom I).Cotangent)
          (Subtype.mk (p := fun (x : T ⊗[R] S) ↦
            Membership.mem (γ := Ideal (T ⊗[R] S))
              (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I) x)
            ((LinearMap.lTensor T (Submodule.subtype (Submodule.restrictScalars R I)) :
                (a : T ⊗[R] ↥(Submodule.restrictScalars R I)) → T ⊗[R] S)
              (t ⊗ₜ[R] x))
            ⋯)) :
      T ⊗[R] S ⧸
        HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ)
          (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I) 2)
⊢ Eq (α :=
    Cotangent (R := T ⊗[R] S) (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I))
    ((tensorCotangentHom R T I :
          (a : T ⊗[R] I.Cotangent) → (map Algebra.TensorProduct.includeRight.toRingHom I).Cotangent)
        (t ⊗ₜ[R] (I.toCotangent : (a : ↥I) → I.Cotangent) x) :
      Cotangent (R := T ⊗[R] S) (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I))
    ((toCotangent (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I) :
          (a : ↥(map Algebra.TensorProduct.includeRight.toRingHom I)) →
            (map Algebra.TensorProduct.includeRight.toRingHom I).Cotangent)
        (Subtype.mk (p := fun (x : T ⊗[R] S) ↦
          Membership.mem (γ := Ideal (T ⊗[R] S))
            (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I) x)
          ((LinearMap.lTensor T (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : T ⊗[R] ↥(Submodule.restrictScalars R I)) → T ⊗[R] S)
            (t ⊗ₜ[R] x))
          ⋯) :
      Cotangent (R := T ⊗[R] S) (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I))

Tactic:
apply Ideal.cotangentToQuotientSquare_injective

Premises used: Ideal.cotangentToQuotientSquare_injective