awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 : Extension.{u, u_1, u_2} R S
T_1 : Type u_3
inst_3 : CommRing T_1
inst_4 : Algebra R T_1
P : Extension.{u, u_1, u_2} R S
T : Type u_4
inst_5 : CommRing T
inst_6 : Algebra R T
this_1 : Algebra P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange) := P.algebraBaseChange T
this_2 : Algebra S (T ⊗[R] S) := TensorProduct.rightAlgebra
this : Algebra P.Ring (T ⊗[R] S) := compHom (T ⊗[R] S) (algebraMap P.Ring S)
x : R
⊢ Eq (α := T ⊗[R] S)
    (1 ⊗ₜ[R] (algebraMap P.Ring S : (a : P.Ring) → S) ((algebraMap R P.Ring : (a : R) → P.Ring) x : P.Ring) : T ⊗[R] S)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (T ⊗[R] S)) (algebraMap P.Ring S) :
          (a : P.Ring) → T ⊗[R] S)
        ((algebraMap R P.Ring : (a : R) → P.Ring) x) :
      T ⊗[R] S)

Tactic:
rfl
-- 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_1 : Extension.{u, u_1, u_2} R S
T_1 : Type u_3
inst_3 : CommRing T_1
inst_4 : Algebra R T_1
P : Extension.{u, u_1, u_2} R S
T : Type u_4
inst_5 : CommRing T
inst_6 : Algebra R T
this_1 : Algebra P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange) := P.algebraBaseChange T
this_2 : Algebra S (T ⊗[R] S) := TensorProduct.rightAlgebra
this_3 : Algebra P.Ring (T ⊗[R] S) := compHom (T ⊗[R] S) (algebraMap P.Ring S)
this : IsScalarTower R P.Ring (T ⊗[R] S)
PT : Extension T (T ⊗[R] S) := P.baseChange
⊢ IsPushout R T P.Ring (TensorProduct.{u_1, u_4, u} R T P.Ring)

Tactic:
TensorProduct.isPushout (R := R) (T := P.Ring) (S := T)

Premises used: TensorProduct.isPushout
-- 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_1 : Extension.{u, u_1, u_2} R S
T_1 : Type u_3
inst_3 : CommRing T_1
inst_4 : Algebra R T_1
P : Extension.{u, u_1, u_2} R S
T : Type u_4
inst_5 : CommRing T
inst_6 : Algebra R T
this_1 : Algebra P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange) := P.algebraBaseChange T
this_2 : Algebra S (T ⊗[R] S) := TensorProduct.rightAlgebra
this_3 : Algebra P.Ring (T ⊗[R] S) := compHom (T ⊗[R] S) (algebraMap P.Ring S)
this : IsScalarTower R P.Ring (T ⊗[R] S)
PT : Extension T (T ⊗[R] S) := P.baseChange
h :
  PT.Ring = TensorProduct.{u_1, u_4, u} R T P.Ring →
    HEq (α := CommSemiring PT.Ring) CommRing.toCommSemiring (β := CommSemiring (TensorProduct.{u_1, u_4, u} R T P.Ring))
        TensorProduct.instCommSemiring →
      PT.instRingOfIsScalarTower = TensorProduct.instAlgebra
⊢ IsPushout R T P.Ring PT.Ring

Tactic:
convert! TensorProduct.isPushout (R := R) (T := P.Ring) (S := T)

Premises used: TensorProduct.isPushout
-- 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_1 : Extension.{u, u_1, u_2} R S
T_1 : Type u_3
inst_3 : CommRing T_1
inst_4 : Algebra R T_1
P : Extension.{u, u_1, u_2} R S
T : Type u_4
inst_5 : CommRing T
inst_6 : Algebra R T
this_1 : Algebra P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange) := P.algebraBaseChange T
this_2 : Algebra S (T ⊗[R] S) := TensorProduct.rightAlgebra
this_3 : Algebra P.Ring (T ⊗[R] S) := compHom (T ⊗[R] S) (algebraMap P.Ring S)
this : IsScalarTower R P.Ring (T ⊗[R] S)
PT : Extension T (T ⊗[R] S) := P.baseChange
e_7 : PT.Ring = TensorProduct.{u_1, u_4, u} R T P.Ring
e_9 :
  HEq (α := CommSemiring PT.Ring) CommRing.toCommSemiring (β := CommSemiring (TensorProduct.{u_1, u_4, u} R T P.Ring))
    TensorProduct.instCommSemiring
⊢ PT.instRingOfIsScalarTower = TensorProduct.instAlgebra

Tactic:
Algebra.algebra_ext _ _ fun _ ↦ rfl

Premises used: Algebra.algebra_ext, rfl
-- 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_1 : Extension.{u, u_1, u_2} R S
T_1 : Type u_3
inst_3 : CommRing T_1
inst_4 : Algebra R T_1
P : Extension.{u, u_1, u_2} R S
T : Type u_4
inst_5 : CommRing T
inst_6 : Algebra R T
this_1 : Algebra P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange) := P.algebraBaseChange T
this_2 : Algebra S (T ⊗[R] S) := TensorProduct.rightAlgebra
this_3 : Algebra P.Ring (T ⊗[R] S) := compHom (T ⊗[R] S) (algebraMap P.Ring S)
this : IsScalarTower R P.Ring (T ⊗[R] S)
PT : Extension T (T ⊗[R] S) := P.baseChange
e_7 : PT.Ring = TensorProduct.{u_1, u_4, u} R T P.Ring
e_9 :
  HEq (α := CommSemiring PT.Ring) CommRing.toCommSemiring (β := CommSemiring (TensorProduct.{u_1, u_4, u} R T P.Ring))
    TensorProduct.instCommSemiring
⊢ PT.instRingOfIsScalarTower = TensorProduct.instAlgebra

Tactic:
exact Algebra.algebra_ext _ _ fun _ ↦ rfl

Premises used: Algebra.algebra_ext, rfl
-- 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_1 : Extension.{u, u_1, u_2} R S
T_1 : Type u_3
inst_3 : CommRing T_1
inst_4 : Algebra R T_1
P : Extension.{u, u_1, u_2} R S
T : Type u_4
inst_5 : CommRing T
inst_6 : Algebra R T
this_1 : Algebra P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange) := P.algebraBaseChange T
this_2 : Algebra S (T ⊗[R] S) := TensorProduct.rightAlgebra
this_3 : Algebra P.Ring (T ⊗[R] S) := compHom (T ⊗[R] S) (algebraMap P.Ring S)
this_4 : IsScalarTower R P.Ring (T ⊗[R] S)
PT : Extension T (T ⊗[R] S) := P.baseChange
this_5 : IsPushout R T P.Ring PT.Ring
this : IsScalarTower P.Ring PT.Ring (T ⊗[R] S)
⊢ ∀ (t x : T) (y : S),
    (((TensorProduct.mk R T S : (a : T) → S →ₗ[R] T ⊗[R] S) (t • x) : S →ₗ[R] T ⊗[R] S) : (a : S) → T ⊗[R] S) y =
      HSMul.hSMul (β := T ⊗[R] S) t
        ((((TensorProduct.mk R T S : (a : T) → S →ₗ[R] T ⊗[R] S) x : S →ₗ[R] T ⊗[R] S) : (a : S) → T ⊗[R] S) y :
          T ⊗[R] S)

Tactic:
simp [Algebra.smul_def]

Premises used: Algebra.smul_def
-- 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_1 : Extension.{u, u_1, u_2} R S
T_1 : Type u_3
inst_3 : CommRing T_1
inst_4 : Algebra R T_1
P : Extension.{u, u_1, u_2} R S
T : Type u_4
inst_5 : CommRing T
inst_6 : Algebra R T
this_1 : Algebra P.Ring (Ring (R := T) (S := T ⊗[R] S) P.baseChange) := P.algebraBaseChange T
this_2 : Algebra S (T ⊗[R] S) := TensorProduct.rightAlgebra
this_3 : Algebra P.Ring (T ⊗[R] S) := compHom (T ⊗[R] S) (algebraMap P.Ring S)
this_4 : IsScalarTower R P.Ring (T ⊗[R] S)
PT : Extension T (T ⊗[R] S) := P.baseChange
this_5 : IsPushout R T P.Ring PT.Ring
this : IsScalarTower P.Ring PT.Ring (T ⊗[R] S)
⊢ ∀ (s : P.Ring) (x : T) (y : S),
    (((TensorProduct.mk R T S : (a : T) → S →ₗ[R] T ⊗[R] S) x : S →ₗ[R] T ⊗[R] S) : (a : S) → T ⊗[R] S) (s • y) =
      HSMul.hSMul (β := T ⊗[R] S) s
        ((((TensorProduct.mk R T S : (a : T) → S →ₗ[R] T ⊗[R] S) x : S →ₗ[R] T ⊗[R] S) : (a : S) → T ⊗[R] S) y :
          T ⊗[R] S)

Tactic:
simp [Algebra.smul_def, RingHom.algebraMap_toAlgebra]

Premises used: Algebra.smul_def, RingHom.algebraMap_toAlgebra
-- 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)
    (((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])
⊢ Eq (α := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
    ((P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace)
        (t ⊗ₜ[R] (s ⊗ₜ[P.Ring] x)) :
      CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange)
    (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 [tensorCotangentSpace, LinearEquiv.trans_apply, LinearEquiv.restrictScalars_apply,
    ← mk_apply s x, IsTensorProduct.assocOfMapSMul_symm_tmul]

Premises used: LinearEquiv.restrictScalars_apply, Algebra.Extension.tensorCotangentSpace, TensorProduct.mk_apply, IsTensorProduct.assocOfMapSMul_symm_tmul, LinearEquiv.trans_apply
-- 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]
rw : Membership.mem (γ := Submodule 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]))) x

Tactic:
rw [KaehlerDifferential.span_range_derivation]

Premises used: KaehlerDifferential.span_range_derivation
-- 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]
⊢ Membership.mem (γ := Submodule P.Ring Ω[P.Ring⁄R]) ⊤ x

Tactic:
trivial
-- 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]
⊢ 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

Tactic:
have this : x ∈ Submodule.span P.Ring (Set.range (KaehlerDifferential.D R P.Ring)) := by
    rw [KaehlerDifferential.span_range_derivation]
    trivial
-- 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]
⊢ 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])

Tactic:
simp
-- 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_1 x y : Ω[P.Ring⁄R]
hx_1 :
  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
hy_1 :
  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])

Tactic:
simp [tmul_add, hx, hy]

Premises used: TensorProduct.tmul_add
-- 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 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
mem :
  ∀ (y : P.Ring),
    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] (KaehlerDifferential.D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) 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])
            ((KaehlerDifferential.D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) 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] 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])

Tactic:
obtain ⟨y, rfl⟩ := hy

Premises used: rfl
-- 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]
y : P.Ring
⊢ 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] (KaehlerDifferential.D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) 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])
          ((KaehlerDifferential.D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) y) :
      T ⊗[R] S ⊗[Ring (R := T) (S := T ⊗[R] S) P.baseChange] Ω[Ring (R := T) (S := T ⊗[R] S) P.baseChange⁄T])

Tactic:
simp
-- 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
zero :
  (P.tensorCotangentSpace T : (a : T ⊗[R] P.CotangentSpace) → P.baseChange.CotangentSpace) 0 =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) 0)
zero₁ :
  0 =
    HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((CotangentSpace.map (toBaseChange T) : (a : P.CotangentSpace) → P.baseChange.CotangentSpace) 0)
zero₂ : 0 = HSMul.hSMul (β := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) t 0
zero₃ zero₄ : Eq (α := CotangentSpace (R := T) (S := T ⊗[R] S) P.baseChange) 0 0
⊢ (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)

Tactic:
rw [tmul_zero, LinearEquiv.map_zero, LinearMap.map_zero, smul_zero]

Premises used: LinearEquiv.map_zero, smul_zero, LinearMap.map_zero, TensorProduct.tmul_zero
-- 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
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)

Tactic:
simp [tensorCotangentSpace_tmul_tmul, CotangentSpace.map_tmul_eq_tmul_map,
    smul_tmul', Algebra.smul_def, RingHom.algebraMap_toAlgebra]

Premises used: Algebra.Extension.tensorCotangentSpace_tmul_tmul, Algebra.Extension.CotangentSpace.map_tmul_eq_tmul_map, TensorProduct.smul_tmul', Algebra.smul_def, RingHom.algebraMap_toAlgebra
-- 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
inst_5 : Module.Flat R T
t : T
x : P.Cotangent
obtain :
  ∀ (x : ↥P.ker),
    (P.tensorCotangentOfFlat T : (a : T ⊗[R] P.Cotangent) → P.baseChange.Cotangent)
        (t ⊗ₜ[R] (Cotangent.mk : (a : ↥P.ker) → P.Cotangent) x) =
      HSMul.hSMul (β := Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) t
        ((Cotangent.map (toBaseChange T) : (a : P.Cotangent) → P.baseChange.Cotangent)
            ((Cotangent.mk : (a : ↥P.ker) → P.Cotangent) x) :
          Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)
⊢ (P.tensorCotangentOfFlat T : (a : T ⊗[R] P.Cotangent) → P.baseChange.Cotangent) (t ⊗ₜ[R] x) =
    HSMul.hSMul (β := Cotangent (R := T) (S := T ⊗[R] S) P.baseChange) t
      ((Cotangent.map (toBaseChange T) : (a : P.Cotangent) → P.baseChange.Cotangent) x :
        Cotangent (R := T) (S := T ⊗[R] S) P.baseChange)

Tactic:
obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x

Premises used: Algebra.Extension.Cotangent.mk_surjective, rfl