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_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
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)))
⊢ LE.le (α := Submodule P P) (RingHom.ker (F := P →+* S) (algebraMap P S)) (RingHom.ker (F := P →+* A) (algebraMap P A))

Tactic:
rw [IsScalarTower.algebraMap_eq P S A]

Premises used: IsScalarTower.algebraMap_eq
-- 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_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
x : P
⊢ Membership.mem (γ := Submodule P P) (RingHom.ker (F := P →+* S) (algebraMap P S)) x →
    Membership.mem (γ := Submodule P P)
      (RingHom.ker (F := P →+* A)
        (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S A) (algebraMap P S)))
      x

Tactic:
aesop
-- 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_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))
rw :
  Membership.mem (γ := Ideal P)
    (RingHom.ker (F := P →+* A) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S A) (algebraMap P S)))
    (↑b : P)
⊢ Membership.mem (γ := Ideal P) (RingHom.ker (F := P →+* A) (algebraMap P A)) (↑b : P)

Tactic:
rw [IsScalarTower.algebraMap_eq P S A]

Premises used: IsScalarTower.algebraMap_eq
-- 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_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) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S A) (algebraMap P S)))
    (↑b : P)

Tactic:
aesop
-- Module: Mathlib.RingTheory.Extension.Cotangent.Basic
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
P : Type u_2
A : Type u_3
inst_2 : CommRing P
inst_3 : CommRing A
inst_4 : Algebra P S
inst_5 : Algebra P A
inst_6 : Algebra R P
inst_7 : Algebra S A
inst_8 : IsScalarTower P S A
a : A
b : ↥(RingHom.ker (F := P →+* S) (algebraMap P S))
⊢ (cotangentComplexBaseChange R S P A : (a : A ⊗[P] ↥(RingHom.ker (algebraMap P S))) → A ⊗[P] Ω[P⁄R]) (a ⊗ₜ[P] b) =
    HSMul.hSMul (β := A ⊗[P] Ω[P⁄R]) a
      ((kerToTensor R P A : (a : ↥(RingHom.ker (algebraMap P A))) → A ⊗[P] Ω[P⁄R])
          (Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Ideal P) (RingHom.ker (F := P →+* A) (algebraMap P A)) x)
            (↑b : P) ⋯) :
        A ⊗[P] Ω[P⁄R])

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, 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
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
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])
⊢ 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))

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
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
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:
simp [LinearEquiv.baseChange, cotangentComplexBaseChange_tmul]

Premises used: KaehlerDifferential.cotangentComplexBaseChange_tmul, LinearEquiv.baseChange
-- 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
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
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)
⊢ 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]))

Tactic:
apply LinearMap.coe_injective

Premises used: LinearMap.coe_injective
-- 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
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
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])
⊢ 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)))

Tactic:
rw [LinearEquiv.eq_symm_comp, ← LinearEquiv.comp_symm_eq]

Premises used: LinearEquiv.comp_symm_eq, LinearEquiv.eq_symm_comp
-- 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
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)) →
      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:
congr(($(cotangentComplexBaseChange_eq_lTensor_cotangentComplex P A) : _ → _)).symm

Premises used: Quotient.liftOn', congrArg, AddCon.liftOn, id, Algebra.Extension.cotangentComplexBaseChange_eq_lTensor_cotangentComplex, Eq.symm, DFunLike.coe
-- 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
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)) →
      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:
exact congr(($(cotangentComplexBaseChange_eq_lTensor_cotangentComplex P A) : _ → _)).symm

Premises used: congrArg, id, Algebra.Extension.cotangentComplexBaseChange_eq_lTensor_cotangentComplex, Eq.symm, DFunLike.coe
-- 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''
f : P.Hom P'
this : Algebra.{w, v'} P.Ring S' :=
  RingHom.toAlgebra (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S S') (algebraMap P.Ring S))
⊢ IsScalarTower.{w, v, v'} P.Ring S S'

Tactic:
haveI : IsScalarTower P.Ring S S' := IsScalarTower.of_algebraMap_eq' 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'
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
⊢ 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)
-- 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''
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'
l : LinearMap (R := P.Ring) (RingHom.id P.Ring) Ω[P.Ring⁄R] P'.CotangentSpace
⊢ P.CotangentSpace →ₗ[S] P'.CotangentSpace

Tactic:
apply LinearMap.liftBaseChange

Premises used: 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''
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'
⊢ LinearMap (R := P.Ring) (RingHom.id P.Ring) Ω[P.Ring⁄R] P'.CotangentSpace

Tactic:
refine (TensorProduct.mk _ _ _ 1).restrictScalars _ ∘ₗ KaehlerDifferential.map R R' P.Ring P'.Ring

Premises used: LinearMap.restrictScalars, Algebra.Extension.Ring, OfNat.ofNat, DFunLike.coe, TensorProduct.mk, KaehlerDifferential.map