awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
inst_23 : IsScalarTower R S S'
f g : P.Hom P'
this_1 : Algebra.{w, v'} P.Ring S' :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S))
this_2 : IsScalarTower.{w, v, v'} P.Ring S S'
this_3 : Algebra.{w, w'} P.Ring P'.Ring := (AlgHom.toRingHom f.toAlgHom).toAlgebra
this : IsScalarTower.{w, w', v'} P.Ring P'.Ring S'
x : R
rw :
  Eq.{v' + 1} (α := S') ((algebraMap R S' : (a : R) → S') x : S')
    ((algebraMap S S' : (a : S) → S') ((algebraMap R S : (a : R) → S) x : S) : S')
rw₁ rw₂ : Eq.{v' + 1} (α := S') ((algebraMap R S' : (a : R) → S') x : S') ((algebraMap R S' : (a : R) → S') x : S')
⊢ Eq.{v' + 1} (α := S') ((algebraMap R S' : (a : R) → S') x : S')
    ((algebraMap S S' : (a : S) → S')
        ((algebraMap P.Ring S : (a : P.Ring) → S) ((algebraMap R P.Ring : (a : R) → P.Ring) x : P.Ring) : S) :
      S')

Tactic:
rw [← IsScalarTower.algebraMap_apply R P.Ring S, ← IsScalarTower.algebraMap_apply]

Premises used: Algebra.Extension.Ring, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
inst_23 : IsScalarTower R S S'
f g : P.Hom P'
this_1 : Algebra.{w, v'} P.Ring S' :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S))
this_2 : IsScalarTower.{w, v, v'} P.Ring S S'
this_3 : Algebra.{w, w'} P.Ring P'.Ring := (AlgHom.toRingHom f.toAlgHom).toAlgebra
this : IsScalarTower.{w, w', v'} P.Ring P'.Ring S'
⊢ IsScalarTower.{u, w, v'} R P.Ring S'

Tactic:
haveI : IsScalarTower R P.Ring S' :=
    IsScalarTower.of_algebraMap_eq fun x ↦
      show algebraMap R S' x = algebraMap S S' (algebraMap P.Ring S (algebraMap R P.Ring x)) by
        rw [← IsScalarTower.algebraMap_apply R P.Ring S, ← IsScalarTower.algebraMap_apply]
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
inst_23 : IsScalarTower R S S'
f g : P.Hom P'
this_1 : Algebra.{w, v'} P.Ring S' :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S))
this_2 : IsScalarTower.{w, v, v'} P.Ring S S'
this_3 : Algebra.{w, w'} P.Ring P'.Ring := (AlgHom.toRingHom f.toAlgHom).toAlgebra
this_4 : IsScalarTower.{w, w', v'} P.Ring P'.Ring S'
this : IsScalarTower.{u, w, v'} R P.Ring S'
refine : Derivation.{u, w, w'} R P.Ring P'.Cotangent
⊢ P.CotangentSpace →ₗ[S] P'.Cotangent

Tactic:
refine (Derivation.liftKaehlerDifferential ?_).liftBaseChange S

Premises used: Derivation.liftKaehlerDifferential, LinearMap.liftBaseChange
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
inst_23 : IsScalarTower R S S'
f g : P.Hom P'
this_1 : Algebra.{w, v'} P.Ring S' :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S))
this_2 : IsScalarTower.{w, v, v'} P.Ring S S'
this_3 : Algebra.{w, w'} P.Ring P'.Ring := (AlgHom.toRingHom f.toAlgHom).toAlgebra
this_4 : IsScalarTower.{w, w', v'} P.Ring P'.Ring S'
this : IsScalarTower.{u, w, v'} R P.Ring S'
⊢ Eq.{w' + 1} (α := P'.ker.Cotangent)
    (Cotangent.val
      ((((↑R :
                  {S M M₂ : Type w'} →
                    [inst : Semiring R] →
                      [inst_24 : Semiring S] →
                        [inst_25 : AddCommMonoid M] →
                          [inst_26 : AddCommMonoid M₂] →
                            [inst_27 : Module R M] →
                              [inst_28 : Module R M₂] →
                                [inst_29 : Module S M] →
                                  [inst_30 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                Cotangent.mk ∘ₗ
              f.subToKer g :
            LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring P'.Cotangent) :
          (a : P.Ring) → P'.Cotangent)
        1))
    (Cotangent.val 0)

Tactic:
simp [Ideal.toCotangent_eq_zero]

Premises used: Ideal.toCotangent_eq_zero
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
inst_23 : IsScalarTower R S S'
f g : P.Hom P'
this_1 : Algebra.{w, v'} P.Ring S' :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S))
this_2 : IsScalarTower.{w, v, v'} P.Ring S S'
this_3 : Algebra.{w, w'} P.Ring P'.Ring := (AlgHom.toRingHom f.toAlgHom).toAlgebra
this_4 : IsScalarTower.{w, w', v'} P.Ring P'.Ring S'
this : IsScalarTower.{u, w, v'} R P.Ring S'
x y : P.Ring
⊢ (↑(((f.subToKer g : LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring ↥P'.ker) : (a : P.Ring) → ↥P'.ker) (x * y)) :
        P'.Ring) -
      (↑(HSMul.hSMul (β := ↥P'.ker) (P'.σ ((algebraMap P.Ring S' : (a : P.Ring) → S') x))
              (((f.subToKer g : LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring ↥P'.ker) : (a : P.Ring) → ↥P'.ker) y :
                ↥P'.ker) +
            HSMul.hSMul (β := ↥P'.ker) (P'.σ ((algebraMap P.Ring S' : (a : P.Ring) → S') y))
              (((f.subToKer g : LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring ↥P'.ker) : (a : P.Ring) → ↥P'.ker) x :
                ↥P'.ker)) :
        P'.Ring) ∈
    HPow.hPow (β := ℕ) P'.ker 2

Tactic:
Hom.sub_aux f g x y

Premises used: Set.Mem, Algebra.Extension.Hom.sub_aux
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst_10 : CommRing R''
inst_11 : CommRing S''
inst_12 : Algebra R'' S''
P'' : Extension.{w'', u'', v''} R'' S''
inst_13 : Algebra R R''
inst_14 : Algebra S S''
inst_15 : Algebra R S''
inst_16 : IsScalarTower R R'' S''
inst_17 : Algebra R' R''
inst_18 : Algebra S' S''
inst_19 : Algebra R' S''
inst_20 : IsScalarTower R' R'' S''
inst_21 : IsScalarTower R R' R''
inst_22 : IsScalarTower S S' S''
inst_23 : IsScalarTower R S S'
f g : P.Hom P'
this_1 : Algebra.{w, v'} P.Ring S' :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S))
this_2 : IsScalarTower.{w, v, v'} P.Ring S S'
this_3 : Algebra.{w, w'} P.Ring P'.Ring := (AlgHom.toRingHom f.toAlgHom).toAlgebra
this_4 : IsScalarTower.{w, w', v'} P.Ring P'.Ring S'
this : IsScalarTower.{u, w, v'} R P.Ring S'
x y : P.Ring
⊢ (↑(((f.subToKer g : LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring ↥P'.ker) : (a : P.Ring) → ↥P'.ker) (x * y)) :
        P'.Ring) -
      (↑(HSMul.hSMul (β := ↥P'.ker) (P'.σ ((algebraMap P.Ring S' : (a : P.Ring) → S') x))
              (((f.subToKer g : LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring ↥P'.ker) : (a : P.Ring) → ↥P'.ker) y :
                ↥P'.ker) +
            HSMul.hSMul (β := ↥P'.ker) (P'.σ ((algebraMap P.Ring S' : (a : P.Ring) → S') y))
              (((f.subToKer g : LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring ↥P'.ker) : (a : P.Ring) → ↥P'.ker) x :
                ↥P'.ker)) :
        P'.Ring) ∈
    HPow.hPow (β := ℕ) P'.ker 2

Tactic:
exact Hom.sub_aux f g x y

Premises used: Algebra.Extension.Hom.sub_aux
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
f g : P.Hom P'
x : P.Ring
⊢ Eq.{w' + 1} (α := P'.Cotangent)
    ((f.sub g : (a : P.CotangentSpace) → P'.Cotangent) (1 ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) x) :
      P'.Cotangent)
    ((Cotangent.mk : (a : ↥P'.ker) → P'.Cotangent)
        (((f.subToKer g : LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring ↥P'.ker) : (a : P.Ring) → ↥P'.ker) x) :
      P'.Cotangent)

Tactic:
simp only [sub, LinearMap.liftBaseChange_tmul, Derivation.liftKaehlerDifferential_comp_D,
    Derivation.mk_coe, LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply,
    one_smul]

Premises used: Algebra.Extension.Hom.sub, LinearMap.coe_restrictScalars, Derivation.mk_coe, Derivation.liftKaehlerDifferential_comp_D, one_smul, LinearMap.liftBaseChange_tmul, LinearMap.coe_comp, Function.comp_apply
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
f g : P.Hom P'
r : S
x : P.Ring
⊢ (f.sub g : (a : P.CotangentSpace) → P'.Cotangent) (r ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) x) =
    HSMul.hSMul (β := P'.Cotangent) r
      ((Cotangent.mk : (a : ↥P'.ker) → P'.Cotangent)
          (((f.subToKer g : LinearMap.{u, u, w, w'} (RingHom.id R) P.Ring ↥P'.ker) : (a : P.Ring) → ↥P'.ker) x) :
        P'.Cotangent)

Tactic:
simp only [sub, LinearMap.liftBaseChange_tmul, Derivation.liftKaehlerDifferential_comp_D,
    Derivation.mk_coe, LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply]

Premises used: Algebra.Extension.Hom.sub, LinearMap.coe_restrictScalars, Derivation.mk_coe, Derivation.liftKaehlerDifferential_comp_D, LinearMap.liftBaseChange_tmul, LinearMap.coe_comp, Function.comp_apply
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
f g : P.Hom P'
h :
  ∀ (x : P.CotangentSpace),
    Eq (α := P'.CotangentSpace)
      ((CotangentSpace.map f - CotangentSpace.map g : (a : P.CotangentSpace) → P'.CotangentSpace) x : P'.CotangentSpace)
      (((↑S :
                  {S_1 : Type v'} →
                    {M : Type w'} →
                      {M₂ : Type (max v' w')} →
                        [inst : Semiring S] →
                          [inst_11 : Semiring S_1] →
                            [inst_12 : AddCommMonoid M] →
                              [inst_13 : AddCommMonoid M₂] →
                                [inst_14 : Module S M] →
                                  [inst_15 : Module S M₂] →
                                    [inst_16 : Module S_1 M] →
                                      [inst_17 : Module S_1 M₂] →
                                        [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                P'.cotangentComplex ∘ₗ
              f.sub g :
            (a : P.CotangentSpace) → P'.CotangentSpace)
          x :
        P'.CotangentSpace)
⊢ CotangentSpace.map f - CotangentSpace.map g =
    (↑S :
          {S_1 : Type v'} →
            {M : Type w'} →
              {M₂ : Type (max v' w')} →
                [inst : Semiring S] →
                  [inst_11 : Semiring S_1] →
                    [inst_12 : AddCommMonoid M] →
                      [inst_13 : AddCommMonoid M₂] →
                        [inst_14 : Module S M] →
                          [inst_15 : Module S M₂] →
                            [inst_16 : Module S_1 M] →
                              [inst_17 : Module S_1 M₂] →
                                [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
        P'.cotangentComplex ∘ₗ
      f.sub g

Tactic:
ext x
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
f g : P.Hom P'
⊢ Eq (α := P'.CotangentSpace)
    ((CotangentSpace.map f - CotangentSpace.map g : (a : P.CotangentSpace) → P'.CotangentSpace) 0)
    (((↑S :
              {S_1 : Type v'} →
                {M : Type w'} →
                  {M₂ : Type (max v' w')} →
                    [inst : Semiring S] →
                      [inst_11 : Semiring S_1] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] →
                                [inst_16 : Module S_1 M] →
                                  [inst_17 : Module S_1 M₂] →
                                    [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            P'.cotangentComplex ∘ₗ
          f.sub g :
        (a : P.CotangentSpace) → P'.CotangentSpace)
      0)

Tactic:
simp only [map_zero]

Premises used: map_zero
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
f g : P.Hom P'
x : S
y : Ω[P.Ring⁄R]
h :
  ∀ (y : P.Ring ⊗[R] P.Ring),
    Eq (α := P'.CotangentSpace)
      ((CotangentSpace.map f - CotangentSpace.map g : (a : P.CotangentSpace) → P'.CotangentSpace)
          (x ⊗ₜ[P.Ring] (Derivation.tensorProductTo (D R P.Ring) : (a : P.Ring ⊗[R] P.Ring) → Ω[P.Ring⁄R]) y) :
        P'.CotangentSpace)
      (((↑S :
                  {S_1 : Type v'} →
                    {M : Type w'} →
                      {M₂ : Type (max v' w')} →
                        [inst : Semiring S] →
                          [inst_11 : Semiring S_1] →
                            [inst_12 : AddCommMonoid M] →
                              [inst_13 : AddCommMonoid M₂] →
                                [inst_14 : Module S M] →
                                  [inst_15 : Module S M₂] →
                                    [inst_16 : Module S_1 M] →
                                      [inst_17 : Module S_1 M₂] →
                                        [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                P'.cotangentComplex ∘ₗ
              f.sub g :
            (a : P.CotangentSpace) → P'.CotangentSpace)
          (x ⊗ₜ[P.Ring] (Derivation.tensorProductTo (D R P.Ring) : (a : P.Ring ⊗[R] P.Ring) → Ω[P.Ring⁄R]) y) :
        P'.CotangentSpace)
⊢ Eq (α := P'.CotangentSpace)
    ((CotangentSpace.map f - CotangentSpace.map g : (a : P.CotangentSpace) → P'.CotangentSpace) (x ⊗ₜ[P.Ring] y) :
      P'.CotangentSpace)
    (((↑S :
                {S_1 : Type v'} →
                  {M : Type w'} →
                    {M₂ : Type (max v' w')} →
                      [inst : Semiring S] →
                        [inst_11 : Semiring S_1] →
                          [inst_12 : AddCommMonoid M] →
                            [inst_13 : AddCommMonoid M₂] →
                              [inst_14 : Module S M] →
                                [inst_15 : Module S M₂] →
                                  [inst_16 : Module S_1 M] →
                                    [inst_17 : Module S_1 M₂] →
                                      [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
              P'.cotangentComplex ∘ₗ
            f.sub g :
          (a : P.CotangentSpace) → P'.CotangentSpace)
        (x ⊗ₜ[P.Ring] y) :
      P'.CotangentSpace)

Tactic:
obtain ⟨y, rfl⟩ := KaehlerDifferential.tensorProductTo_surjective _ _ y

Premises used: KaehlerDifferential.tensorProductTo_surjective, rfl
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
f g : P.Hom P'
x : S
⊢ Eq (α := P'.CotangentSpace)
    ((CotangentSpace.map f - CotangentSpace.map g : (a : P.CotangentSpace) → P'.CotangentSpace)
        (x ⊗ₜ[P.Ring] (Derivation.tensorProductTo (D R P.Ring) : (a : P.Ring ⊗[R] P.Ring) → Ω[P.Ring⁄R]) 0) :
      P'.CotangentSpace)
    (((↑S :
                {S_1 : Type v'} →
                  {M : Type w'} →
                    {M₂ : Type (max v' w')} →
                      [inst : Semiring S] →
                        [inst_11 : Semiring S_1] →
                          [inst_12 : AddCommMonoid M] →
                            [inst_13 : AddCommMonoid M₂] →
                              [inst_14 : Module S M] →
                                [inst_15 : Module S M₂] →
                                  [inst_16 : Module S_1 M] →
                                    [inst_17 : Module S_1 M₂] →
                                      [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
              P'.cotangentComplex ∘ₗ
            f.sub g :
          (a : P.CotangentSpace) → P'.CotangentSpace)
        (x ⊗ₜ[P.Ring] (Derivation.tensorProductTo (D R P.Ring) : (a : P.Ring ⊗[R] P.Ring) → Ω[P.Ring⁄R]) 0) :
      P'.CotangentSpace)

Tactic:
simp only [map_zero, tmul_zero]

Premises used: TensorProduct.tmul_zero, map_zero
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{w, u, v} R S
R' : Type u'
S' : Type v'
inst_3 : CommRing R'
inst_4 : CommRing S'
inst_5 : Algebra R' S'
P' : Extension.{w', u', v'} R' S'
inst_6 : Algebra R R'
inst_7 : Algebra S S'
inst_8 : Algebra R S'
inst_9 : IsScalarTower R R' S'
inst_10 : IsScalarTower R S S'
f g : P.Hom P'
x : S
x_1 y : P.Ring
⊢ Eq (α := P'.CotangentSpace)
    ((CotangentSpace.map f - CotangentSpace.map g : (a : P.CotangentSpace) → P'.CotangentSpace)
        (x ⊗ₜ[P.Ring]
          (Derivation.tensorProductTo (D R P.Ring) : (a : P.Ring ⊗[R] P.Ring) → Ω[P.Ring⁄R]) (x_1 ⊗ₜ[R] y)) :
      P'.CotangentSpace)
    (((↑S :
                {S_1 : Type v'} →
                  {M : Type w'} →
                    {M₂ : Type (max v' w')} →
                      [inst : Semiring S] →
                        [inst_11 : Semiring S_1] →
                          [inst_12 : AddCommMonoid M] →
                            [inst_13 : AddCommMonoid M₂] →
                              [inst_14 : Module S M] →
                                [inst_15 : Module S M₂] →
                                  [inst_16 : Module S_1 M] →
                                    [inst_17 : Module S_1 M₂] →
                                      [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
              P'.cotangentComplex ∘ₗ
            f.sub g :
          (a : P.CotangentSpace) → P'.CotangentSpace)
        (x ⊗ₜ[P.Ring]
          (Derivation.tensorProductTo (D R P.Ring) : (a : P.Ring ⊗[R] P.Ring) → Ω[P.Ring⁄R]) (x_1 ⊗ₜ[R] y)) :
      P'.CotangentSpace)

Tactic:
simp only [Derivation.tensorProductTo_tmul, tmul_smul, smul_tmul', LinearMap.sub_apply,
        map_tmul, Hom.toAlgHom_apply, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
        Function.comp_apply, Hom.sub_tmul, LinearMap.map_smul_of_tower, cotangentComplex_mk,
        Hom.subToKer_apply_coe, map_sub, ← algebraMap_eq_smul_one, tmul_sub, smul_sub]

Premises used: map_sub, TensorProduct.tmul_sub, Algebra.Extension.CotangentSpace.map_tmul, LinearMap.coe_restrictScalars, TensorProduct.tmul_smul, Algebra.algebraMap_eq_smul_one, smul_sub, TensorProduct.smul_tmul', LinearMap.coe_comp, Algebra.Extension.Hom.subToKer_apply_coe, Derivation.tensorProductTo_tmul, LinearMap.sub_apply, Function.comp_apply, Algebra.Extension.Hom.sub_tmul, LinearMap.map_smul_of_tower, Algebra.Extension.Hom.toAlgHom_apply, Algebra.Extension.cotangentComplex_mk