-- Lean 4 proof step from Mathlib.RingTheory.Ideal.CotangentBaseChange (goal)
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
inst_5 : Module.Flat R T
a : S →+* T ⊗[R] S := AlgHom.toRingHom Algebra.TensorProduct.includeRight
f : Cotangent (R := T ⊗[R] S) (map a I) →ₗ[T] T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2 := sorry
g : TensorProduct.{u_1, u_3, u_2} R T I.Cotangent →ₗ[T]
  TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2) :=
  ((AlgebraTensorModule.lTensor T T :
        (I.Cotangent →ₗ[R] S ⧸ HPow.hPow (β := ℕ) I 2) →ₗ[R]
          TensorProduct.{u_1, u_3, u_2} R T I.Cotangent →ₗ[T]
            TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2)) :
      (a : I.Cotangent →ₗ[R] S ⧸ I ^ 2) → T ⊗[R] I.Cotangent →ₗ[T] T ⊗[R] (S ⧸ I ^ 2))
    ((↑R :
        {S M M₂ : Type u_2} →
          [inst : Semiring R] →
            [inst_6 : Semiring S] →
              [inst_7 : AddCommMonoid M] →
                [inst_8 : AddCommMonoid M₂] →
                  [inst_9 : Module R M] →
                    [inst_10 : Module R M₂] →
                      [inst_11 : Module S M] →
                        [inst_12 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      I.cotangentToQuotientSquare)
hₐ : TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2) ≃ₐ[T]
  T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2 :=
  AlgEquiv.trans
    (Algebra.TensorProduct.tensorQuotientEquiv T S T (HPow.hPow (β := ℕ) I 2) :
      TensorProduct.{u_1, u_3, u_2} R T (S ⧸ HPow.hPow (β := ℕ) I 2) ≃ₐ[T]
        HasQuotient.Quotient (T ⊗[R] S) (B := Ideal (T ⊗[R] S))
          (map (F := S →ₐ[R] T ⊗[R] S) Algebra.TensorProduct.includeRight (HPow.hPow (β := ℕ) I 2)))
    (quotientEquivAlgOfEq T ⋯ :
      HasQuotient.Quotient (T ⊗[R] S) (B := Ideal (T ⊗[R] S))
          (map (F := S →ₐ[R] T ⊗[R] S) Algebra.TensorProduct.includeRight (HPow.hPow (β := ℕ) I 2)) ≃ₐ[T]
        T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2)
x : ↥I
⊢ Eq (α := T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2)
    ((sorry () : (a_1 : (map a I).Cotangent) → T ⊗[R] S ⧸ map a I ^ 2)
        ((tensorCotangentHom R T I : (a_1 : T ⊗[R] I.Cotangent) → (map a I).Cotangent)
          (1 ⊗ₜ[R] (I.toCotangent : (a : ↥I) → I.Cotangent) x)) :
      T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2)
    ((Quotient.mk (HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2) : (a_1 : T ⊗[R] S) → T ⊗[R] S ⧸ map a I ^ 2)
        (1 ⊗ₜ[R] (↑x : S)) :
      T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2)
have a₁ : Eq (α := T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2)
  ((sorry () : (a_1 : (map a I).Cotangent) → T ⊗[R] S ⧸ map a 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)
          (1 ⊗ₜ[R] (↑x : S)) sorry)) :
    T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2)
  ((Quotient.mk (HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2) : (a_1 : T ⊗[R] S) → T ⊗[R] S ⧸ map a I ^ 2)
      (1 ⊗ₜ[R] (↑x : S)) :
    T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2)
Tactic: rw [tensorCotangentHom_tmul, one_smul, Ideal.toCotangent_to_quotient_square]