-- 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
s : S
x : Ω[P.Ring⁄R]
simp :
  Eq (α := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
    (t ⊗ₜ[R] s ⊗ₜ[Ring (R := T) (S := T ⊗[R] S) P.baseChange]
        (KaehlerDifferential.tensorKaehlerEquiv R T P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange) :
            (a : P.baseChange.Ring ⊗[P.Ring] Ω[P.Ring⁄R]) → Ω[P.baseChange.Ring⁄T])
          (1 ⊗ₜ[P.Ring] x) :
      T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange] Ω[Ring (R := T) (S := T ⊗[R] S) P.baseChange⁄T])
    (t ⊗ₜ[R] s ⊗ₜ[Ring (R := T) (S := T ⊗[R] S) P.baseChange]
        (KaehlerDifferential.map R T P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange) :
            (a : Ω[P.Ring⁄R]) → Ω[P.baseChange.Ring⁄T])
          x :
      T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange] Ω[Ring (R := T) (S := T ⊗[R] S) P.baseChange⁄T])
⊢ Eq (α := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
    (((AlgebraTensorModule.congr (LinearEquiv.refl (Ring (R := T) (S := T ⊗[R] S) P.baseChange) (T ⊗[R] S))
              (KaehlerDifferential.tensorKaehlerEquiv R T P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange)) :
            T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange]
                (Ring (R := T) (S := T ⊗[R] S) P.baseChange ⊗[P.Ring]
                  Ω[P.Ring⁄R]) ≃ₗ[Ring (R := T) (S := T ⊗[R] S) P.baseChange]
              T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange] Ω[Ring (R := T) (S := T ⊗[R] S) P.baseChange⁄T]) :
          (a : T ⊗[R] S ⊗[P.baseChange.Ring] (P.baseChange.Ring ⊗[P.Ring] Ω[P.Ring⁄R])) →
            T ⊗[R] S ⊗[P.baseChange.Ring] Ω[P.baseChange.Ring⁄T])
        (((LinearEquiv.symm
                (AlgebraTensorModule.cancelBaseChange P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange)
                  (Ring (R := T) (S := T ⊗[R] S) P.baseChange) (T ⊗[R] S) Ω[P.Ring⁄R]) :
              T ⊗[R] S ⊗[P.Ring] Ω[P.Ring⁄R] ≃ₗ[Ring (R := T) (S := T ⊗[R] S) P.baseChange]
                T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange]
                  (Ring (R := T) (S := T ⊗[R] S) P.baseChange ⊗[P.Ring] Ω[P.Ring⁄R])) :
            (a : T ⊗[R] S ⊗[P.Ring] Ω[P.Ring⁄R]) →
              T ⊗[R] S ⊗[P.baseChange.Ring] (P.baseChange.Ring ⊗[P.Ring] Ω[P.Ring⁄R]))
          ((((TensorProduct.mk R T S : (a : T) → S →ₗ[R] T ⊗[R] S) t : S →ₗ[R] T ⊗[R] S) : (a : S) → T ⊗[R] S)
              s ⊗ₜ[P.Ring]
            x)) :
      T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange] Ω[Ring (R := T) (S := T ⊗[R] S) P.baseChange⁄T])
    (t ⊗ₜ[R] s ⊗ₜ[Ring (R := T) (S := T ⊗[R] S) P.baseChange]
        (KaehlerDifferential.map R T P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange) :
            (a : Ω[P.Ring⁄R]) → Ω[P.baseChange.Ring⁄T])
          x :
      T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange] Ω[Ring (R := T) (S := T ⊗[R] S) P.baseChange⁄T])

Tactic:
simp only [mk_apply, AlgebraTensorModule.cancelBaseChange_symm_tmul,
    AlgebraTensorModule.congr_tmul, LinearEquiv.refl_apply]

Premises used: TensorProduct.mk_apply, LinearEquiv.refl_apply, TensorProduct.AlgebraTensorModule.cancelBaseChange_symm_tmul, TensorProduct.AlgebraTensorModule.congr_tmul