-- 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]
this :
  Membership.mem (γ := Submodule P.Ring Ω[P.Ring⁄R])
    (Submodule.span P.Ring (Set.range (ι := P.Ring) (⇑(KaehlerDifferential.D R P.Ring) : (a : P.Ring) → Ω[P.Ring⁄R]))) x
zero :
  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] 0) :
      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])
          0 :
      T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange] Ω[Ring (R := T) (S := T ⊗[R] S) P.baseChange⁄T])
add :
  ∀ (x y : Ω[P.Ring⁄R]),
    Membership.mem (γ := Submodule P.Ring Ω[P.Ring⁄R])
        (Submodule.span P.Ring
          (Set.range (ι := P.Ring) (⇑(KaehlerDifferential.D R P.Ring) : (a : P.Ring) → Ω[P.Ring⁄R])))
        x →
      Membership.mem (γ := Submodule P.Ring Ω[P.Ring⁄R])
          (Submodule.span P.Ring
            (Set.range (ι := P.Ring) (⇑(KaehlerDifferential.D R P.Ring) : (a : P.Ring) → Ω[P.Ring⁄R])))
          y →
        ∀
          (hx :
            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]))
          (hy :
            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] y) :
                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])
                    y :
                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)
            (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 + y)) :
              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 + y) :
              T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange] Ω[Ring (R := T) (S := T ⊗[R] S) P.baseChange⁄T])
mem :
  ∀ (y : Ω[P.Ring⁄R])
    (hy :
      Membership.mem (γ := Set Ω[P.Ring⁄R])
        (Set.range (ι := P.Ring) (⇑(KaehlerDifferential.D R P.Ring) : (a : P.Ring) → Ω[P.Ring⁄R])) y),
    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] y) :
        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])
            y :
        T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange] Ω[Ring (R := T) (S := T ⊗[R] S) P.baseChange⁄T])
smul :
  ∀ (a : P.Ring) (x : Ω[P.Ring⁄R]),
    Membership.mem (γ := Submodule P.Ring Ω[P.Ring⁄R])
        (Submodule.span P.Ring
          (Set.range (ι := P.Ring) (⇑(KaehlerDifferential.D R P.Ring) : (a : P.Ring) → Ω[P.Ring⁄R])))
        x →
      ∀
        (hx :
          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)
          (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] (a • 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])
                (a • 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)
    (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])

Tactic:
induction this using Submodule.span_induction with
  | zero => simp
  | add x y _ _ hx hy => simp [tmul_add, hx, hy]
  | mem y hy =>
    obtain ⟨y, rfl⟩ := hy
    simp
  | smul a x _ hx =>
    rw [tmul_smul, ← algebraMap_smul (P.baseChange (T := T)).Ring a, LinearEquiv.map_smul,
      tmul_smul, hx, LinearMap.map_smul, ← algebraMap_smul (P.baseChange (T := T)).Ring a,
      tmul_smul]

Premises used: TensorProduct.tmul_smul, LinearMap.map_smul, LinearEquiv.map_smul, TensorProduct.tmul_add, rfl