-- 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
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.Cotangent
a₁ :
  ∀ (x : ↥I),
    Eq (α := T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2)
      ((((AlgebraTensorModule.curry (f ∘ₗ tensorCotangentHom R T I) :
                  T →ₗ[T] I.Cotangent →ₗ[R] T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2) :
                (a_1 : T) → I.Cotangent →ₗ[R] T ⊗[R] S ⧸ map a I ^ 2)
              1 :
            (a_1 : I.Cotangent) → T ⊗[R] S ⧸ map a I ^ 2)
          ((I.toCotangent : (a : ↥I) → I.Cotangent) x) :
        T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2)
      ((((AlgebraTensorModule.curry (hₐ.toLinearMap ∘ₗ g) :
                  T →ₗ[T] I.Cotangent →ₗ[R] T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2) :
                (a_1 : T) → I.Cotangent →ₗ[R] T ⊗[R] S ⧸ map a I ^ 2)
              1 :
            (a_1 : I.Cotangent) → T ⊗[R] S ⧸ map a I ^ 2)
          ((I.toCotangent : (a : ↥I) → I.Cotangent) x) :
        T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2)
⊢ Eq (α := T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2)
    ((((AlgebraTensorModule.curry (f ∘ₗ tensorCotangentHom R T I) :
                T →ₗ[T] I.Cotangent →ₗ[R] T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2) :
              (a_1 : T) → I.Cotangent →ₗ[R] T ⊗[R] S ⧸ map a I ^ 2)
            1 :
          (a_1 : I.Cotangent) → T ⊗[R] S ⧸ map a I ^ 2)
        x :
      T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2)
    ((((AlgebraTensorModule.curry (hₐ.toLinearMap ∘ₗ g) :
                T →ₗ[T] I.Cotangent →ₗ[R] T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2) :
              (a_1 : T) → I.Cotangent →ₗ[R] T ⊗[R] S ⧸ map a I ^ 2)
            1 :
          (a_1 : I.Cotangent) → T ⊗[R] S ⧸ map a I ^ 2)
        x :
      T ⊗[R] S ⧸ HPow.hPow (α := Ideal (T ⊗[R] S)) (β := ℕ) (map a I) 2)

Tactic:
obtain ⟨x, rfl⟩ := I.toCotangent_surjective x

Premises used: Ideal.toCotangent_surjective, rfl