awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.BaseChange (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Module.Flat R T
t : T
x : H1Cotangent R S
⊢ (tensorH1CotangentOfFlat R S T : (a : T ⊗[R] H1Cotangent R S) → H1Cotangent T (T ⊗[R] S)) (t ⊗ₜ[R] x) =
    HSMul.hSMul (β := H1Cotangent T (T ⊗[R] S)) t
      ((H1Cotangent.map R T S (T ⊗[R] S) : (a : H1Cotangent R S) → H1Cotangent T (T ⊗[R] S)) x :
        H1Cotangent T (T ⊗[R] S))
have simp : HSMul.hSMul (β := H1Cotangent T (T ⊗[R] S)) t
    ((sorry : (a : (Generators.baseChange T (Generators.self R S)).toExtension.H1Cotangent) → H1Cotangent T (T ⊗[R] S))
        ((sorry :
            (a : (Generators.self R S).toExtension.baseChange.H1Cotangent) →
              (Generators.baseChange T (Generators.self R S)).toExtension.H1Cotangent)
          ((Extension.H1Cotangent.map (Extension.toBaseChange T) :
              (a : (Generators.self R S).toExtension.H1Cotangent) →
                (Generators.self R S).toExtension.baseChange.H1Cotangent)
            x)) :
      H1Cotangent T (T ⊗[R] S)) =
  HSMul.hSMul (β := H1Cotangent T (T ⊗[R] S)) t
    ((H1Cotangent.map R T S (T ⊗[R] S) : (a : H1Cotangent R S) → H1Cotangent T (T ⊗[R] S)) x : H1Cotangent T (T ⊗[R] S))
Tactic: simp only [tensorH1CotangentOfFlat, LinearEquiv.trans_apply,
    Extension.tensorH1CotangentOfFlat_tmul, map_smul, LinearEquiv.restrictScalars_apply,
    Extension.H1Cotangent.equiv, LinearEquiv.coe_mk, Generators.equivH1Cotangent,
    Generators.H1Cotangent.equiv]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Extension.{w, u, v} R S
A_1 : Type u_1
inst_3 : CommRing A_1
inst_4 : Algebra S A_1
inst_5 : Algebra.{w, u_1} P_1.Ring A_1
inst_6 : IsScalarTower.{w, v, u_1} P_1.Ring S A_1
P : Type u_2
A : Type u_3
inst_7 : CommRing P
inst_8 : CommRing A
inst_9 : Algebra P S
inst_10 : Algebra P A
inst_11 : Algebra R P
inst_12 : Algebra S A
inst_13 : IsScalarTower P S A
⊢ LE.le (α := Submodule P P) (RingHom.ker (F := P →+* S) (algebraMap P S)) (RingHom.ker (F := P →+* A) (algebraMap P A))
have rw : LE.le (α := Submodule P P) (RingHom.ker (F := P →+* S) (algebraMap P S))
  (RingHom.ker (F := P →+* A) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S A) (algebraMap P S)))
Tactic: rw [IsScalarTower.algebraMap_eq P S A]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Extension.{w, u, v} R S
A_1 : Type u_1
inst_3 : CommRing A_1
inst_4 : Algebra S A_1
inst_5 : Algebra.{w, u_1} P_1.Ring A_1
inst_6 : IsScalarTower.{w, v, u_1} P_1.Ring S A_1
P : Type u_2
A : Type u_3
inst_7 : CommRing P
inst_8 : CommRing A
inst_9 : Algebra P S
inst_10 : Algebra P A
inst_11 : Algebra R P
inst_12 : Algebra S A
inst_13 : IsScalarTower P S A
a : A
b : ↥(RingHom.ker (F := P →+* S) (algebraMap P S))
⊢ Membership.mem (γ := Ideal P) (RingHom.ker (F := P →+* A) (algebraMap P A)) (↑b : P)
have rw : Membership.mem (γ := Ideal P)
  (RingHom.ker (F := P →+* A) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S A) (algebraMap P S)))
  (↑b : P)
Tactic: rw [IsScalarTower.algebraMap_eq P S A]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
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
A : Type u_1
inst_3 : CommRing A
inst_4 : Algebra S A
inst_5 : Algebra.{w, u_1} P.Ring A
inst_6 : IsScalarTower.{w, v, u_1} P.Ring S A
⊢ Eq (α :=
    TensorProduct.{w, u_1, w} P.Ring A ↥(RingHom.ker (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S)) →ₗ[A]
      TensorProduct.{w, u_1, w} P.Ring A Ω[P.Ring⁄R])
    (cotangentComplexBaseChange R S P.Ring A)
    ((↑(AlgebraTensorModule.cancelBaseChange P.Ring S A A Ω[P.Ring⁄R]) :
        A ⊗[S] (S ⊗[P.Ring] Ω[P.Ring⁄R]) →ₗ[A] A ⊗[P.Ring] Ω[P.Ring⁄R]) ∘ₗ
      LinearMap.baseChange A P.cotangentComplex ∘ₗ
        (↑(LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange P.Ring S A A ↥P.ker) ≪≫ₗ
              LinearEquiv.baseChange S A (TensorProduct.{w, v, w} P.Ring S ↥P.ker) P.Cotangent P.cotangentEquiv) :
          A ⊗[P.Ring] ↥P.ker →ₗ[A] A ⊗[S] P.Cotangent))
have a : ∀ (x : ↥(RingHom.ker (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S))),
  Eq (α := TensorProduct.{w, u_1, w} P.Ring A Ω[P.Ring⁄R])
    ((((AlgebraTensorModule.curry (cotangentComplexBaseChange R S P.Ring A) :
                A →ₗ[A]
                  LinearMap (R := P.Ring) (RingHom.id P.Ring)
                    (↥(RingHom.ker (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S)))
                    (TensorProduct.{w, u_1, w} P.Ring A Ω[P.Ring⁄R])) :
              (a : A) → ↥(RingHom.ker (algebraMap P.Ring S)) →ₗ[P.Ring] A ⊗[P.Ring] Ω[P.Ring⁄R])
            1 :
          (a : ↥(RingHom.ker (algebraMap P.Ring S))) → A ⊗[P.Ring] Ω[P.Ring⁄R])
        x :
      TensorProduct.{w, u_1, w} P.Ring A Ω[P.Ring⁄R])
    ((((AlgebraTensorModule.curry
                  ((↑(AlgebraTensorModule.cancelBaseChange P.Ring S A A Ω[P.Ring⁄R]) :
                      A ⊗[S] (S ⊗[P.Ring] Ω[P.Ring⁄R]) →ₗ[A] A ⊗[P.Ring] Ω[P.Ring⁄R]) ∘ₗ
                    LinearMap.baseChange A P.cotangentComplex ∘ₗ
                      (↑(LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange P.Ring S A A ↥P.ker) ≪≫ₗ
                            LinearEquiv.baseChange S A (TensorProduct.{w, v, w} P.Ring S ↥P.ker) P.Cotangent
                              P.cotangentEquiv) :
                        A ⊗[P.Ring] ↥P.ker →ₗ[A] A ⊗[S] P.Cotangent)) :
                A →ₗ[A]
                  LinearMap (R := P.Ring) (RingHom.id P.Ring)
                    (↥(RingHom.ker (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S)))
                    (TensorProduct.{w, u_1, w} P.Ring A Ω[P.Ring⁄R])) :
              (a : A) → ↥(RingHom.ker (algebraMap P.Ring S)) →ₗ[P.Ring] A ⊗[P.Ring] Ω[P.Ring⁄R])
            1 :
          (a : ↥(RingHom.ker (algebraMap P.Ring S))) → A ⊗[P.Ring] Ω[P.Ring⁄R])
        x :
      TensorProduct.{w, u_1, w} P.Ring A Ω[P.Ring⁄R])
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
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
A : Type u_1
inst_3 : CommRing A
inst_4 : Algebra S A
inst_5 : Algebra.{w, u_1} P.Ring A
inst_6 : IsScalarTower.{w, v, u_1} P.Ring S A
⊢ Eq (α := TensorProduct.{v, u_1, w} S A P.Cotangent →ₗ[A] A ⊗[S] P.CotangentSpace)
    (LinearMap.baseChange A P.cotangentComplex)
    (((↑(LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange P.Ring S A A Ω[P.Ring⁄R])) :
          TensorProduct.{w, u_1, w} P.Ring A Ω[P.Ring⁄R] →ₗ[A] A ⊗[S] TensorProduct.{w, v, w} P.Ring S Ω[P.Ring⁄R]) :
        TensorProduct.{w, u_1, w} P.Ring A Ω[P.Ring⁄R] →ₗ[A] A ⊗[S] TensorProduct.{w, v, w} P.Ring S Ω[P.Ring⁄R]) ∘ₗ
      (cotangentComplexBaseChange R S P.Ring A ∘ₗ
          (↑(LinearEquiv.symm
                (LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange P.Ring S A A ↥P.ker) ≪≫ₗ
                  LinearEquiv.baseChange S A (TensorProduct.{w, v, w} P.Ring S ↥P.ker) P.Cotangent P.cotangentEquiv)) :
            A ⊗[S] P.Cotangent →ₗ[A] A ⊗[P.Ring] ↥P.ker) :
        TensorProduct.{v, u_1, w} S A P.Cotangent →ₗ[A] TensorProduct.{w, u_1, w} P.Ring A Ω[P.Ring⁄R]))
have a : Eq (α := (a : TensorProduct.{v, u_1, w} S A P.Cotangent) → A ⊗[S] P.CotangentSpace)
  (⇑(LinearMap.baseChange A P.cotangentComplex) : (a : A ⊗[S] P.Cotangent) → A ⊗[S] P.CotangentSpace)
  (⇑(((↑(LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange P.Ring S A A Ω[P.Ring⁄R])) :
            TensorProduct.{w, u_1, w} P.Ring A Ω[P.Ring⁄R] →ₗ[A] A ⊗[S] TensorProduct.{w, v, w} P.Ring S Ω[P.Ring⁄R]) :
          TensorProduct.{w, u_1, w} P.Ring A Ω[P.Ring⁄R] →ₗ[A] A ⊗[S] TensorProduct.{w, v, w} P.Ring S Ω[P.Ring⁄R]) ∘ₗ
        (cotangentComplexBaseChange R S P.Ring A ∘ₗ
            (↑(LinearEquiv.symm
                  (LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange P.Ring S A A ↥P.ker) ≪≫ₗ
                    LinearEquiv.baseChange S A (TensorProduct.{w, v, w} P.Ring S ↥P.ker) P.Cotangent
                      P.cotangentEquiv)) :
              A ⊗[S] P.Cotangent →ₗ[A] A ⊗[P.Ring] ↥P.ker) :
          TensorProduct.{v, u_1, w} S A P.Cotangent →ₗ[A] TensorProduct.{w, u_1, w} P.Ring A Ω[P.Ring⁄R])) :
    (a : A ⊗[S] P.Cotangent) → A ⊗[S] P.CotangentSpace)
Tactic: apply LinearMap.coe_injective
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
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
A : Type u_1
inst_3 : CommRing A
inst_4 : Algebra S A
inst_5 : Algebra.{w, u_1} P.Ring A
inst_6 : IsScalarTower.{w, v, u_1} P.Ring S A
⊢ Eq (α := (a : TensorProduct.{v, u_1, w} S A P.Cotangent) → A ⊗[S] P.CotangentSpace)
    (⇑(LinearMap.baseChange A P.cotangentComplex) : (a : A ⊗[S] P.Cotangent) → A ⊗[S] P.CotangentSpace)
    (Function.comp (β := TensorProduct.{w, u_1, w} P.Ring A Ω[P.Ring⁄R])
      (⇑(LinearEquiv.symm (AlgebraTensorModule.cancelBaseChange P.Ring S A A Ω[P.Ring⁄R]) :
            TensorProduct.{w, u_1, w} P.Ring A Ω[P.Ring⁄R] ≃ₗ[A] A ⊗[S] TensorProduct.{w, v, w} P.Ring S Ω[P.Ring⁄R]) :
        (a : A ⊗[P.Ring] Ω[P.Ring⁄R]) → A ⊗[S] (S ⊗[P.Ring] Ω[P.Ring⁄R]))
      (Function.comp (β :=
        TensorProduct.{w, u_1, w} P.Ring A ↥(RingHom.ker (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S)))
        (⇑(cotangentComplexBaseChange R S P.Ring A) :
          (a : A ⊗[P.Ring] ↥(RingHom.ker (algebraMap P.Ring S))) → A ⊗[P.Ring] Ω[P.Ring⁄R])
        (⇑(LinearEquiv.symm
                  (LinearEquiv.baseChange S A (TensorProduct.{w, v, w} P.Ring S ↥P.ker) P.Cotangent
                    P.cotangentEquiv) ≪≫ₗ
                AlgebraTensorModule.cancelBaseChange P.Ring S A A ↥P.ker :
              TensorProduct.{v, u_1, w} S A P.Cotangent ≃ₗ[A] TensorProduct.{w, u_1, w} P.Ring A ↥P.ker) :
          (a : A ⊗[S] P.Cotangent) → A ⊗[P.Ring] ↥P.ker)))
have a : Eq (α :=
  TensorProduct.{w, u_1, w} P.Ring A ↥(RingHom.ker (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S)) →
    TensorProduct.{w, u_1, w} P.Ring A Ω[P.Ring⁄R])
  (Function.comp (β := TensorProduct.{v, u_1, w} S A P.Cotangent)
    (Function.comp (β := A ⊗[S] P.CotangentSpace)
      (⇑(AlgebraTensorModule.cancelBaseChange P.Ring S A A Ω[P.Ring⁄R] :
            A ⊗[S] TensorProduct.{w, v, w} P.Ring S Ω[P.Ring⁄R] ≃ₗ[A] TensorProduct.{w, u_1, w} P.Ring A Ω[P.Ring⁄R]) :
        (a : A ⊗[S] P.CotangentSpace) → A ⊗[P.Ring] Ω[P.Ring⁄R])
      (⇑(LinearMap.baseChange A P.cotangentComplex) : (a : A ⊗[S] P.Cotangent) → A ⊗[S] P.CotangentSpace))
    (⇑(LinearEquiv.symm
            (LinearEquiv.symm
                (LinearEquiv.baseChange S A (TensorProduct.{w, v, w} P.Ring S ↥P.ker) P.Cotangent P.cotangentEquiv) ≪≫ₗ
              AlgebraTensorModule.cancelBaseChange P.Ring S A A ↥P.ker) :
          TensorProduct.{w, u_1, w} P.Ring A ↥(RingHom.ker (F := RingHom.{w, v} P.Ring S) (algebraMap P.Ring S)) ≃ₗ[A]
            TensorProduct.{v, u_1, w} S A P.Cotangent) :
      (a : A ⊗[P.Ring] ↥(RingHom.ker (algebraMap P.Ring S))) → A ⊗[S] P.Cotangent))
  (⇑(cotangentComplexBaseChange R S P.Ring A) :
    (a : A ⊗[P.Ring] ↥(RingHom.ker (algebraMap P.Ring S))) → A ⊗[P.Ring] Ω[P.Ring⁄R])
Tactic: rw [LinearEquiv.eq_symm_comp, ← LinearEquiv.comp_symm_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (hypothesis)
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''
f : P.Hom P'
this : Algebra.{w, v'} P.Ring S' :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S))
⊢ P.CotangentSpace →ₗ[S] P'.CotangentSpace
have this₁ : IsScalarTower.{w, v, v'} P.Ring S S'
Tactic: haveI : IsScalarTower P.Ring S S' := IsScalarTower.of_algebraMap_eq' rfl
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (hypothesis)
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''
f : 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 : Algebra.{w, w'} P.Ring P'.Ring := (AlgHom.toRingHom f.toAlgHom).toAlgebra
⊢ P.CotangentSpace →ₗ[S] P'.CotangentSpace
have this₁ : IsScalarTower.{w, w', v'} P.Ring P'.Ring S'
Tactic: haveI : IsScalarTower P.Ring P'.Ring S' :=
    IsScalarTower.of_algebraMap_eq (fun x ↦ (f.algebraMap_toRingHom x).symm)
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
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''
f : 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'
⊢ P.CotangentSpace →ₗ[S] P'.CotangentSpace
have l : LinearMap (R := P.Ring) (RingHom.id P.Ring) Ω[P.Ring⁄R] P'.CotangentSpace
Tactic: apply LinearMap.liftBaseChange
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
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'
f : P.Hom P'
x : S
y : P.Ring
⊢ Eq (α := P'.CotangentSpace)
    ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace)
        (x ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) y) :
      P'.CotangentSpace)
    ((algebraMap S S' : (a : S) → S') x ⊗ₜ[P'.Ring]
        (D R' P'.Ring : (a : P'.Ring) → Ω[P'.Ring⁄R'])
          (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y) :
      TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R'])
have simp : HSMul.hSMul (β := P'.CotangentSpace) x
    (1 ⊗ₜ[P'.Ring]
        (D R' P'.Ring : (a : P'.Ring) → Ω[P'.Ring⁄R']) ((algebraMap P.Ring P'.Ring : (a : P.Ring) → P'.Ring) y) :
      TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R']) =
  (algebraMap S S' : (a : S) → S') x ⊗ₜ[P'.Ring]
    (D R' P'.Ring : (a : P'.Ring) → Ω[P'.Ring⁄R'])
      (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y)
Tactic: simp only [CotangentSpace.map, AlgHom.toRingHom_eq_coe, LinearMap.liftBaseChange_tmul,
    LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply, map_D, mk_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
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'
f : P.Hom P'
x : S
y : P.Ring
⊢ HSMul.hSMul (β := P'.CotangentSpace) x
      (1 ⊗ₜ[P'.Ring]
          (D R' P'.Ring : (a : P'.Ring) → Ω[P'.Ring⁄R']) ((algebraMap P.Ring P'.Ring : (a : P.Ring) → P'.Ring) y) :
        TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R']) =
    (algebraMap S S' : (a : S) → S') x ⊗ₜ[P'.Ring]
      (D R' P'.Ring : (a : P'.Ring) → Ω[P'.Ring⁄R'])
        (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y)
have rw : Eq (α := P'.CotangentSpace)
  ((algebraMap S S' : (a : S) → S') x ⊗ₜ[P'.Ring]
      (D R' P'.Ring : (a : P'.Ring) → Ω[P'.Ring⁄R']) ((algebraMap P.Ring P'.Ring : (a : P.Ring) → P'.Ring) y) :
    TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R'])
  ((algebraMap S S' : (a : S) → S') x ⊗ₜ[P'.Ring]
      (D R' P'.Ring : (a : P'.Ring) → Ω[P'.Ring⁄R'])
        (((f.toAlgHom : AlgHom.{u, w, w'} R P.Ring P'.Ring) : (a : P.Ring) → P'.Ring) y) :
    TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R'])
Tactic: rw [smul_tmul', ← Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
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'
f : P.Hom P'
x : S
y : Ω[P.Ring⁄R]
⊢ Eq (α := P'.CotangentSpace)
    ((CotangentSpace.map f : (a : P.CotangentSpace) → P'.CotangentSpace) (x ⊗ₜ[P.Ring] y) : P'.CotangentSpace)
    ((algebraMap S S' : (a : S) → S') x ⊗ₜ[P'.Ring]
        (KaehlerDifferential.map R R' P.Ring P'.Ring : (a : Ω[P.Ring⁄R]) → Ω[P'.Ring⁄R']) y :
      TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R'])
have rw : Eq (α := P'.CotangentSpace)
  ((LinearMap.liftBaseChange S
          ((↑P.Ring :
                {S_1 M : Type w'} →
                  {M₂ : Type (max v' w')} →
                    [inst_10 : Semiring P.Ring] →
                      [inst_11 : Semiring S_1] →
                        [inst_12 : AddCommMonoid M] →
                          [inst_13 : AddCommMonoid M₂] →
                            [inst_14 : Module P.Ring M] →
                              [inst_15 : Module P.Ring M₂] →
                                [inst_16 : Module S_1 M] →
                                  [inst_17 : Module S_1 M₂] →
                                    [LinearMap.CompatibleSMul M M₂ P.Ring S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[P.Ring] M₂)
              (S := P'.Ring)
              ((TensorProduct.mk P'.Ring S' Ω[P'.Ring⁄R'] :
                  (a : S') → Ω[P'.Ring⁄R'] →ₗ[P'.Ring] S' ⊗[P'.Ring] Ω[P'.Ring⁄R'])
                1) ∘ₗ
            KaehlerDifferential.map R R' P.Ring P'.Ring) :
        (a : P.CotangentSpace) → P'.CotangentSpace)
      (x ⊗ₜ[P.Ring] y) :
    P'.CotangentSpace)
  ((algebraMap S S' : (a : S) → S') x ⊗ₜ[P'.Ring]
      (KaehlerDifferential.map R R' P.Ring P'.Ring : (a : Ω[P.Ring⁄R]) → Ω[P'.Ring⁄R']) y :
    TensorProduct.{w', v', w'} P'.Ring S' Ω[P'.Ring⁄R'])
Tactic: rw [CotangentSpace.map, LinearMap.liftBaseChange_tmul, LinearMap.coe_comp, Function.comp_apply,
    LinearMap.restrictScalars_apply, mk_apply, smul_tmul', Algebra.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basic (goal)
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
⊢ CotangentSpace.map (Hom.id P) = LinearMap.id
have a : ∀ (a : P.Ring),
  Eq (α := P.CotangentSpace)
    (((((LinearMap.compDer
                    (((AlgebraTensorModule.curry (CotangentSpace.map (Hom.id P)) :
                          S →ₗ[S] LinearMap (R := P.Ring) (RingHom.id P.Ring) Ω[P.Ring⁄R] P.CotangentSpace) :
                        (a : S) → Ω[P.Ring⁄R] →ₗ[P.Ring] P.CotangentSpace)
                      1) :
                  LinearMap (R := P.Ring) (RingHom.id P.Ring) (Derivation R P.Ring Ω[P.Ring⁄R])
                    (Derivation R P.Ring P.CotangentSpace)) :
                (a : Derivation R P.Ring Ω[P.Ring⁄R]) → Derivation R P.Ring P.CotangentSpace)
              (D R P.Ring) :
            Derivation R P.Ring P.CotangentSpace) :
          (a : P.Ring) → P.CotangentSpace)
        a :
      P.CotangentSpace)
    (((((LinearMap.compDer
                    (((AlgebraTensorModule.curry LinearMap.id :
                          S →ₗ[S] LinearMap (R := P.Ring) (RingHom.id P.Ring) Ω[P.Ring⁄R] P.CotangentSpace) :
                        (a : S) → Ω[P.Ring⁄R] →ₗ[P.Ring] P.CotangentSpace)
                      1) :
                  LinearMap (R := P.Ring) (RingHom.id P.Ring) (Derivation R P.Ring Ω[P.Ring⁄R])
                    (Derivation R P.Ring P.CotangentSpace)) :
                (a : Derivation R P.Ring Ω[P.Ring⁄R]) → Derivation R P.Ring P.CotangentSpace)
              (D R P.Ring) :
            Derivation R P.Ring P.CotangentSpace) :
          (a : P.Ring) → P.CotangentSpace)
        a :
      P.CotangentSpace)
Tactic: ext