-- 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
a_1 : S →+* T ⊗[R] S := AlgHom.toRingHom Algebra.TensorProduct.includeRight
x y : TensorProduct.{u_1, u_3, u_2} R T ↥(Submodule.restrictScalars R I)
a : TensorProduct.{u_1, u_3, u_2} R T I.Cotangent
ha :
  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))
b : TensorProduct.{u_1, u_3, u_2} R T I.Cotangent
hb :
  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)
        b :
      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))
⊢ 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 + b) :
      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))
have simp : HAdd.hAdd (α :=
    Cotangent (R := T ⊗[R] S) (map (F := S →+* T ⊗[R] S) (AlgHom.toRingHom Algebra.TensorProduct.includeRight) I)) (β :=
    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)
          sorry) :
      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)
          sorry) :
      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)
      (HAdd.hAdd (α := T ⊗[R] S) (β := T ⊗[R] S)
        ((LinearMap.lTensor T (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : T ⊗[R] ↥(Submodule.restrictScalars R I)) → T ⊗[R] S)
            x :
          T ⊗[R] S)
        ((LinearMap.lTensor T (Submodule.subtype (Submodule.restrictScalars R I)) :
              (a : T ⊗[R] ↥(Submodule.restrictScalars R I)) → T ⊗[R] S)
            y :
          T ⊗[R] S))
      sorry)
Tactic: simp only [map_add, ha, hb]