-- Module: Mathlib.RingTheory.Extension.Cotangent.BaseChange
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 : TensorProduct.{u, u_2, u} P.Ring S Ω[P.Ring⁄R]
zero :
  (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) (t ⊗ₜ[R] 0) =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) 0)
add :
  ∀ (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)),
    (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)
tmul :
  ∀ (s : S) (y : Ω[P.Ring⁄R]),
    (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace)
        (t ⊗ₜ[R] (s ⊗ₜ[P.Ring] y)) =
      HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
        ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) (s ⊗ₜ[P.Ring] y) :
          CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
⊢ (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)

Tactic:
induction x with
  | zero => rw [tmul_zero, LinearEquiv.map_zero, LinearMap.map_zero, smul_zero]
  | add x y hx hy => rw [tmul_add, LinearEquiv.map_add, LinearMap.map_add, smul_add, hx, hy]
  | tmul s y =>
  simp [tensorCotangentSpace_tmul_tmul, CotangentSpace.map_tmul_eq_tmul_map,
    smul_tmul', Algebra.smul_def, RingHom.algebraMap_toAlgebra]

Premises used: LinearMap.map_add, LinearEquiv.map_zero, Algebra.Extension.tensorCotangentSpace_tmul_tmul, smul_zero, LinearMap.map_zero, TensorProduct.tmul_zero, Algebra.Extension.CotangentSpace.map_tmul_eq_tmul_map, LinearEquiv.map_add, TensorProduct.smul_tmul', TensorProduct.tmul_add, Algebra.smul_def, RingHom.algebraMap_toAlgebra, TensorProduct.tmul, smul_add