-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_2} R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
t : T
x y : TensorProduct.{u, u_2, u} P.Ring S Ω[P.Ring⁄R]
hx :
  (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] x) =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) x :
        CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
hy :
  (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] y) =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) y :
        CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
add :
  (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace)
      (HAdd.hAdd (α := T ⊗[R] P.CotangentSpace) (t ⊗ₜ[R] x) (t ⊗ₜ[R] y)) =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) (x + y) :
        CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
add₁ :
  HAdd.hAdd (α := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) (β :=
      CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
      ((P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] x) :
        CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
      ((P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] y) :
        CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) (x + y) :
        CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
add₂ :
  HAdd.hAdd (α := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) (β :=
      CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
      ((P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] x) :
        CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
      ((P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] y) :
        CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) =
    t •
      HAdd.hAdd (α := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) (β :=
        CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
        ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) x :
          CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
        ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) y :
          CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
add₃ :
  HAdd.hAdd (α := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) (β :=
      CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
      ((P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] x) :
        CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
      ((P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] y) :
        CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
        ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) x :
          CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) +
      HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
        ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) y :
          CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
⊢ (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] (x + y)) =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) (x + y) :
        CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
have add₄ : HAdd.hAdd (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
    (HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) x :
        CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange))
    ((P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] y) :
      CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) =
  HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) x :
        CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) +
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) y :
        CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
Tactic: rw [tmul_add, LinearEquiv.map_add, LinearMap.map_add, smul_add, hx, hy]