-- 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
y : TensorProduct.{u_1, u_3, u_2} R T ↥(Submodule.restrictScalars R I)
zero :
  ∃ (a : TensorProduct.{u_1, u_3, u_2} R T I.Cotangent),
    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)
          a :
        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)
              0)
            ⋯) :
        Cotangent (R := T ⊗[R] S) (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I))
add :
  ∀ (x y : TensorProduct.{u_1, u_3, u_2} R T ↥(Submodule.restrictScalars R I))
    (hx :
      ∃ (a : TensorProduct.{u_1, u_3, u_2} R T I.Cotangent),
        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)
              a :
            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)
                  x)
                ⋯) :
            Cotangent (R := T ⊗[R] S)
              (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I)))
    (hy :
      ∃ (a : TensorProduct.{u_1, u_3, u_2} R T I.Cotangent),
        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)
              a :
            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)
                  y)
                ⋯) :
            Cotangent (R := T ⊗[R] S)
              (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I))),
    ∃ (a : TensorProduct.{u_1, u_3, u_2} R T I.Cotangent),
      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)
            a :
          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)
                (x + y))
              ⋯) :
          Cotangent (R := T ⊗[R] S) (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I))
tmul :
  ∀ (t : T) (x : ↥(Submodule.restrictScalars R I)),
    ∃ (a : TensorProduct.{u_1, u_3, u_2} R T I.Cotangent),
      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)
            a :
          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))
⊢ ∃ (a : TensorProduct.{u_1, u_3, u_2} R T I.Cotangent),
    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)
          a :
        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)
              y)
            ⋯) :
        Cotangent (R := T ⊗[R] S) (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I))

Tactic:
induction y with
  | zero => exact ⟨0, by simp only [map_zero]; exact (map_zero _).symm⟩
  | add x y hx hy =>
    obtain ⟨a, ha⟩ := hx
    obtain ⟨b, hb⟩ := hy
    exact ⟨a + b, by simp only [map_add, ha, hb]; rfl⟩
  | tmul t x =>
    use t ⊗ₜ I.toCotangent x
    apply Ideal.cotangentToQuotientSquare_injective
    simp [-AlgHom.toRingHom_eq_coe, tensorCotangentHom_tmul, Algebra.smul_def,
      ← Ideal.Quotient.mk_algebraMap, ← map_mul]

Premises used: Ideal.tensorCotangentHom_tmul, map_mul, AlgHom.toRingHom_eq_coe, Ideal.cotangentToQuotientSquare_injective, Algebra.smul_def, TensorProduct.tmul, Ideal.Quotient.mk_algebraMap