awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
P' : Type u_2 := P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2
h₁ : Surjective.{u_2 + 1, u_3 + 1} (α := P') (β := S) (⇑(algebraMap P' S) : (a : P') → S)
⊢ HPow.hPow (α := Ideal P') (β := ℕ) (RingHom.ker (F := P' →+* S) (algebraMap P' S)) 2 = ⊥

Tactic:
have h₂ : RingHom.ker (algebraMap P' S) ^ 2 = ⊥ := by
    rw [RingHom.algebraMap_toAlgebra, AlgHom.ker_kerSquareLift, Ideal.cotangentIdeal_square]
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
P' : Type u_2 := P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2
h₁ : Surjective.{u_2 + 1, u_3 + 1} (α := P') (β := S) (⇑(algebraMap P' S) : (a : P') → S)
h₂ : HPow.hPow (α := Ideal P') (β := ℕ) (RingHom.ker (F := P' →+* S) (algebraMap P' S)) 2 = ⊥
e₁ : Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)) ≃ₗ[P]
  ↥(RingHom.ker (F := P' →+* S) (algebraMap P' S)) :=
  Ideal.cotangentEquivIdeal (RingHom.ker (F := P →+* S) (algebraMap P S)) ≪≫ₗ
    LinearEquiv.restrictScalars P
      (LinearEquiv.ofEq
        (Ideal.cotangentIdeal (RingHom.ker (F := P →+* S) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P S))))
        (RingHom.ker (F :=
          RingHom.{u_2, u_3}
            (P ⧸
              HPow.hPow (α := Ideal P) (β := ℕ)
                (RingHom.ker (F := P →+* S) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P S))) 2)
            S)
          (AlgHom.toRingHom (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P S))))
        ⋯)
e₂ : S ⊗[P'] Ω[P'⁄R] ≃ₗ[P] S ⊗[P] Ω[P⁄R] := LinearEquiv.restrictScalars P (tensorKaehlerQuotKerSqEquiv R P S)
x : ↥(RingHom.ker (F := P →+* S) (algebraMap P S))
⊢ Eq (α := S ⊗[P] Ω[P⁄R])
    ((kerCotangentToTensor R P S : (a : (RingHom.ker (algebraMap P S)).Cotangent) → S ⊗[P] Ω[P⁄R])
        ((Ideal.toCotangent (RingHom.ker (F := P →+* S) (algebraMap P S)) :
            (a : ↥(RingHom.ker (algebraMap P S))) → (RingHom.ker (algebraMap P S)).Cotangent)
          x) :
      S ⊗[P] Ω[P⁄R])
    (((↑e₂ : S ⊗[P'] Ω[P'⁄R] →ₗ[P] S ⊗[P] Ω[P⁄R]) ∘ₗ
            (↑P :
                  {S M : Type u_2} →
                    {M₂ : Type (max u_2 u_3)} →
                      [inst : Semiring P] →
                        [inst_7 : Semiring S] →
                          [inst_8 : AddCommMonoid M] →
                            [inst_9 : AddCommMonoid M₂] →
                              [inst_10 : Module P M] →
                                [inst_11 : Module P M₂] →
                                  [inst_12 : Module S M] →
                                    [inst_13 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ P S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[P] M₂)
                (kerToTensor R P' S) ∘ₗ
              (↑e₁ : (RingHom.ker (algebraMap P S)).Cotangent →ₗ[P] ↥(RingHom.ker (algebraMap P' S))) :
          (a : (RingHom.ker (algebraMap P S)).Cotangent) → S ⊗[P] Ω[P⁄R])
        ((Ideal.toCotangent (RingHom.ker (F := P →+* S) (algebraMap P S)) :
            (a : ↥(RingHom.ker (algebraMap P S))) → (RingHom.ker (algebraMap P S)).Cotangent)
          x) :
      S ⊗[P] Ω[P⁄R])

Tactic:
exact (tensorKaehlerQuotKerSqEquiv_tmul_D 1 x.1).symm

Premises used: tensorKaehlerQuotKerSqEquiv_tmul_D, OfNat.ofNat, Eq.symm, Subtype.val
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
P' : Type u_2 := P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2
h₁ : Surjective.{u_2 + 1, u_3 + 1} (α := P') (β := S) (⇑(algebraMap P' S) : (a : P') → S)
h₂ : HPow.hPow (α := Ideal P') (β := ℕ) (RingHom.ker (F := P' →+* S) (algebraMap P' S)) 2 = ⊥
e₁ : Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)) ≃ₗ[P]
  ↥(RingHom.ker (F := P' →+* S) (algebraMap P' S)) :=
  Ideal.cotangentEquivIdeal (RingHom.ker (F := P →+* S) (algebraMap P S)) ≪≫ₗ
    LinearEquiv.restrictScalars P
      (LinearEquiv.ofEq
        (Ideal.cotangentIdeal (RingHom.ker (F := P →+* S) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P S))))
        (RingHom.ker (F :=
          RingHom.{u_2, u_3}
            (P ⧸
              HPow.hPow (α := Ideal P) (β := ℕ)
                (RingHom.ker (F := P →+* S) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P S))) 2)
            S)
          (AlgHom.toRingHom (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P S))))
        ⋯)
e₂ : S ⊗[P'] Ω[P'⁄R] ≃ₗ[P] S ⊗[P] Ω[P⁄R] := LinearEquiv.restrictScalars P (tensorKaehlerQuotKerSqEquiv R P S)
⊢ kerCotangentToTensor R P S =
    (↑e₂ : S ⊗[P'] Ω[P'⁄R] →ₗ[P] S ⊗[P] Ω[P⁄R]) ∘ₗ
      (↑P :
            {S M : Type u_2} →
              {M₂ : Type (max u_2 u_3)} →
                [inst : Semiring P] →
                  [inst_7 : Semiring S] →
                    [inst_8 : AddCommMonoid M] →
                      [inst_9 : AddCommMonoid M₂] →
                        [inst_10 : Module P M] →
                          [inst_11 : Module P M₂] →
                            [inst_12 : Module S M] →
                              [inst_13 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ P S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[P] M₂)
          (kerToTensor R P' S) ∘ₗ
        (↑e₁ : (RingHom.ker (algebraMap P S)).Cotangent →ₗ[P] ↥(RingHom.ker (algebraMap P' S)))

Tactic:
have H : kerCotangentToTensor R P S =
      e₂.toLinearMap ∘ₗ (kerToTensor R P' S).restrictScalars P ∘ₗ e₁.toLinearMap := by
    ext x
    obtain ⟨x, rfl⟩ := Ideal.toCotangent_surjective _ x
    exact (tensorKaehlerQuotKerSqEquiv_tmul_D 1 x.1).symm
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
P : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing P
inst_2 : CommRing S
inst_3 : Algebra R P
inst_4 : Algebra P S
inst_5 : Algebra R S
inst_6 : IsScalarTower R P S
hf' : HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2 = ⊥
hf : Surjective.{u_2 + 1, u_3 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
P' : Type u_2 := P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker (F := P →+* S) (algebraMap P S)) 2
h₁ : Surjective.{u_2 + 1, u_3 + 1} (α := P') (β := S) (⇑(algebraMap P' S) : (a : P') → S)
h₂ : HPow.hPow (α := Ideal P') (β := ℕ) (RingHom.ker (F := P' →+* S) (algebraMap P' S)) 2 = ⊥
e₁ : Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)) ≃ₗ[P]
  ↥(RingHom.ker (F := P' →+* S) (algebraMap P' S)) :=
  Ideal.cotangentEquivIdeal (RingHom.ker (F := P →+* S) (algebraMap P S)) ≪≫ₗ
    LinearEquiv.restrictScalars P
      (LinearEquiv.ofEq
        (Ideal.cotangentIdeal (RingHom.ker (F := P →+* S) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P S))))
        (RingHom.ker (F :=
          RingHom.{u_2, u_3}
            (P ⧸
              HPow.hPow (α := Ideal P) (β := ℕ)
                (RingHom.ker (F := P →+* S) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P S))) 2)
            S)
          (AlgHom.toRingHom (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P S))))
        ⋯)
e₂ : S ⊗[P'] Ω[P'⁄R] ≃ₗ[P] S ⊗[P] Ω[P⁄R] := LinearEquiv.restrictScalars P (tensorKaehlerQuotKerSqEquiv R P S)
H :
  kerCotangentToTensor R P S =
    (↑e₂ : S ⊗[P'] Ω[P'⁄R] →ₗ[P] S ⊗[P] Ω[P⁄R]) ∘ₗ
      (↑P :
            {S M : Type u_2} →
              {M₂ : Type (max u_2 u_3)} →
                [inst : Semiring P] →
                  [inst_7 : Semiring S] →
                    [inst_8 : AddCommMonoid M] →
                      [inst_9 : AddCommMonoid M₂] →
                        [inst_10 : Module P M] →
                          [inst_11 : Module P M₂] →
                            [inst_12 : Module S M] →
                              [inst_13 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ P S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[P] M₂)
          (kerToTensor R P' S) ∘ₗ
        (↑e₁ : (RingHom.ker (algebraMap P S)).Cotangent →ₗ[P] ↥(RingHom.ker (algebraMap P' S)))
refine :
  { l : S ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)) //
      l ∘ₗ kerCotangentToTensor R P S = LinearMap.id } ≃
    { l : S ⊗[P'] Ω[P'⁄R] →ₗ[P'] ↥(RingHom.ker (F := P' →+* S) (algebraMap P' S)) //
      l ∘ₗ kerToTensor R P' S = LinearMap.id }
⊢ { l : S ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* S) (algebraMap P S)) //
      l ∘ₗ kerCotangentToTensor R P S = LinearMap.id } ≃
    { g :
      AlgHom.{u_1, u_3, u_2} R S
        (P ⧸
          HPow.hPow (α := Ideal P) (β := ℕ)
            (RingHom.ker (F := P →+* S) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P S))) 2) //
      AlgHom.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P S)) g = AlgHom.id R S }

Tactic:
refine Equiv.trans ?_ (retractionKerToTensorEquivSection (R := R) h₂ h₁)

Premises used: Equiv.trans, retractionKerToTensorEquivSection
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
this :
  CotangentSpace.map P.toInfinitesimal =
    (↑(LinearEquiv.symm (tensorKaehlerQuotKerSqEquiv R P.Ring S)) :
      S ⊗[P.Ring] Ω[P.Ring⁄R] →ₗ[S]
        S ⊗[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2] Ω[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2⁄R])
rw :
  Function.Bijective (α := P.CotangentSpace) (β := P.infinitesimal.CotangentSpace)
    (⇑(↑(LinearEquiv.symm (tensorKaehlerQuotKerSqEquiv R P.Ring S)) :
          S ⊗[P.Ring] Ω[P.Ring⁄R] →ₗ[S]
            S ⊗[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2] Ω[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2⁄R]) :
      (a : P.CotangentSpace) → P.infinitesimal.CotangentSpace)
⊢ Function.Bijective (α := P.CotangentSpace) (β := P.infinitesimal.CotangentSpace)
    (⇑(CotangentSpace.map P.toInfinitesimal) : (a : P.CotangentSpace) → P.infinitesimal.CotangentSpace)

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
this :
  CotangentSpace.map P.toInfinitesimal =
    (↑(LinearEquiv.symm (tensorKaehlerQuotKerSqEquiv R P.Ring S)) :
      S ⊗[P.Ring] Ω[P.Ring⁄R] →ₗ[S]
        S ⊗[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2] Ω[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2⁄R])
⊢ Function.Bijective (α := P.CotangentSpace) (β := P.infinitesimal.CotangentSpace)
    (⇑(↑(LinearEquiv.symm (tensorKaehlerQuotKerSqEquiv R P.Ring S)) :
          S ⊗[P.Ring] Ω[P.Ring⁄R] →ₗ[S]
            S ⊗[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2] Ω[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2⁄R]) :
      (a : P.CotangentSpace) → P.infinitesimal.CotangentSpace)

Tactic:
(tensorKaehlerQuotKerSqEquiv _ _ _).symm.bijective

Premises used: LinearEquiv.symm, LinearEquiv.bijective, Ideal.Quotient.mk, Submodule.Quotient.mk, Quotient, tensorKaehlerQuotKerSqEquiv
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
this :
  CotangentSpace.map P.toInfinitesimal =
    (↑(LinearEquiv.symm (tensorKaehlerQuotKerSqEquiv R P.Ring S)) :
      S ⊗[P.Ring] Ω[P.Ring⁄R] →ₗ[S]
        S ⊗[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2] Ω[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2⁄R])
⊢ Function.Bijective (α := P.CotangentSpace) (β := P.infinitesimal.CotangentSpace)
    (⇑(↑(LinearEquiv.symm (tensorKaehlerQuotKerSqEquiv R P.Ring S)) :
          S ⊗[P.Ring] Ω[P.Ring⁄R] →ₗ[S]
            S ⊗[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2] Ω[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2⁄R]) :
      (a : P.CotangentSpace) → P.infinitesimal.CotangentSpace)

Tactic:
exact (tensorKaehlerQuotKerSqEquiv _ _ _).symm.bijective

Premises used: LinearEquiv.symm, LinearEquiv.bijective, tensorKaehlerQuotKerSqEquiv
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
suffices :
  CotangentSpace.map P.toInfinitesimal =
    (↑(LinearEquiv.symm (tensorKaehlerQuotKerSqEquiv R P.Ring S)) :
      S ⊗[P.Ring] Ω[P.Ring⁄R] →ₗ[S]
        S ⊗[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2] Ω[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2⁄R])
⊢ Function.Bijective (α := P.CotangentSpace) (β := P.infinitesimal.CotangentSpace)
    (⇑(CotangentSpace.map P.toInfinitesimal) : (a : P.CotangentSpace) → P.infinitesimal.CotangentSpace)

Tactic:
suffices CotangentSpace.map P.toInfinitesimal =
      (tensorKaehlerQuotKerSqEquiv _ _ _).symm.toLinearMap by
    rw [this]; exact (tensorKaehlerQuotKerSqEquiv _ _ _).symm.bijective
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
this : Algebra P.Ring P.infinitesimal.Ring :=
  { smul := map_toInfinitesimal_bijective._aux_1 P, algebraMap := map_toInfinitesimal_bijective._aux_2 P,
    commutes' := ⋯, smul_def' := ⋯ }
⊢ IsScalarTower.{u, u, u_3} P.Ring P.infinitesimal.Ring S

Tactic:
have : IsScalarTower P.Ring P.infinitesimal.Ring S := .of_algebraMap_eq' rfl
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
this_1 : Algebra P.Ring P.infinitesimal.Ring :=
  { smul := map_toInfinitesimal_bijective._aux_1 P, algebraMap := map_toInfinitesimal_bijective._aux_2 P,
    commutes' := ⋯, smul_def' := ⋯ }
this : IsScalarTower.{u, u, u_3} P.Ring P.infinitesimal.Ring S
a :
  Eq (α := LinearMap (R := P.Ring) (RingHom.id P.Ring) P.CotangentSpace P.infinitesimal.CotangentSpace)
    ((↑P.Ring :
        {S_1 : Type u_3} →
          {M M₂ : Type (max u u_3)} →
            [inst_3 : Semiring P.Ring] →
              [inst_4 : Semiring S_1] →
                [inst_5 : AddCommMonoid M] →
                  [inst_6 : AddCommMonoid M₂] →
                    [inst_7 : Module P.Ring M] →
                      [inst_8 : Module P.Ring M₂] →
                        [inst_9 : Module S_1 M] →
                          [inst_10 : Module S_1 M₂] →
                            [LinearMap.CompatibleSMul M M₂ P.Ring S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[P.Ring] M₂)
      (CotangentSpace.map P.toInfinitesimal))
    ((↑P.Ring :
        {S_1 : Type u_3} →
          {M M₂ : Type (max u u_3)} →
            [inst_3 : Semiring P.Ring] →
              [inst_4 : Semiring S_1] →
                [inst_5 : AddCommMonoid M] →
                  [inst_6 : AddCommMonoid M₂] →
                    [inst_7 : Module P.Ring M] →
                      [inst_8 : Module P.Ring M₂] →
                        [inst_9 : Module S_1 M] →
                          [inst_10 : Module S_1 M₂] →
                            [LinearMap.CompatibleSMul M M₂ P.Ring S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[P.Ring] M₂)
      (↑(LinearEquiv.symm (tensorKaehlerQuotKerSqEquiv R P.Ring S)) :
        S ⊗[P.Ring] Ω[P.Ring⁄R] →ₗ[S]
          S ⊗[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2] Ω[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2⁄R]))
⊢ CotangentSpace.map P.toInfinitesimal =
    (↑(LinearEquiv.symm (tensorKaehlerQuotKerSqEquiv R P.Ring S)) :
      S ⊗[P.Ring] Ω[P.Ring⁄R] →ₗ[S]
        S ⊗[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2] Ω[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2⁄R])

Tactic:
apply LinearMap.restrictScalars_injective P.Ring

Premises used: Algebra.Extension.Ring, LinearMap.restrictScalars_injective
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
this_1 : Algebra P.Ring P.infinitesimal.Ring :=
  { smul := map_toInfinitesimal_bijective._aux_1 P, algebraMap := map_toInfinitesimal_bijective._aux_2 P,
    commutes' := ⋯, smul_def' := ⋯ }
this : IsScalarTower.{u, u, u_3} P.Ring P.infinitesimal.Ring S
x : S
a : P.Ring
a₁ :
  Eq (α := P.infinitesimal.CotangentSpace)
    (x ⊗ₜ[P.infinitesimal.Ring]
        (D R P.infinitesimal.Ring : (a : P.infinitesimal.Ring) → Ω[P.infinitesimal.Ring⁄R])
          ((P.toInfinitesimal.toRingHom : (a : P.Ring) → P.infinitesimal.Ring) a) :
      TensorProduct.{u, u_3, u} P.infinitesimal.Ring S Ω[P.infinitesimal.Ring⁄R])
    (((↑(LinearEquiv.symm (tensorKaehlerQuotKerSqEquiv R P.Ring S)) :
            S ⊗[P.Ring] Ω[P.Ring⁄R] →ₗ[S]
              S ⊗[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2] Ω[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2⁄R]) :
          (a : S ⊗[P.Ring] Ω[P.Ring⁄R]) → P.infinitesimal.CotangentSpace)
        (x ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) a) :
      P.infinitesimal.CotangentSpace)
⊢ Eq (α := P.infinitesimal.CotangentSpace)
    ((CotangentSpace.map P.toInfinitesimal : (a : S ⊗[P.Ring] Ω[P.Ring⁄R]) → P.infinitesimal.CotangentSpace)
        (x ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) a) :
      P.infinitesimal.CotangentSpace)
    (((↑(LinearEquiv.symm (tensorKaehlerQuotKerSqEquiv R P.Ring S)) :
            S ⊗[P.Ring] Ω[P.Ring⁄R] →ₗ[S]
              S ⊗[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2] Ω[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2⁄R]) :
          (a : S ⊗[P.Ring] Ω[P.Ring⁄R]) → P.infinitesimal.CotangentSpace)
        (x ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) a) :
      P.infinitesimal.CotangentSpace)

Tactic:
simp only [map_tmul, algebraMap_self, RingHom.id_apply, Hom.toAlgHom_apply]

Premises used: RingHom.id_apply, Algebra.algebraMap_self, Algebra.Extension.CotangentSpace.map_tmul, Algebra.Extension.Hom.toAlgHom_apply
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
this_1 : Algebra P.Ring P.infinitesimal.Ring :=
  { smul := map_toInfinitesimal_bijective._aux_1 P, algebraMap := map_toInfinitesimal_bijective._aux_2 P,
    commutes' := ⋯, smul_def' := ⋯ }
this : IsScalarTower.{u, u, u_3} P.Ring P.infinitesimal.Ring S
x : S
a : P.Ring
⊢ Eq (α := P.infinitesimal.CotangentSpace)
    (x ⊗ₜ[P.infinitesimal.Ring]
        (D R P.infinitesimal.Ring : (a : P.infinitesimal.Ring) → Ω[P.infinitesimal.Ring⁄R])
          ((P.toInfinitesimal.toRingHom : (a : P.Ring) → P.infinitesimal.Ring) a) :
      TensorProduct.{u, u_3, u} P.infinitesimal.Ring S Ω[P.infinitesimal.Ring⁄R])
    (((↑(LinearEquiv.symm (tensorKaehlerQuotKerSqEquiv R P.Ring S)) :
            S ⊗[P.Ring] Ω[P.Ring⁄R] →ₗ[S]
              S ⊗[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2] Ω[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2⁄R]) :
          (a : S ⊗[P.Ring] Ω[P.Ring⁄R]) → P.infinitesimal.CotangentSpace)
        (x ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) a) :
      P.infinitesimal.CotangentSpace)

Tactic:
exact (tensorKaehlerQuotKerSqEquiv_symm_tmul_D _ _).symm

Premises used: tensorKaehlerQuotKerSqEquiv_symm_tmul_D, Eq.symm
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
left :
  Function.Injective (α := P.Cotangent) (β := P.infinitesimal.Cotangent)
    (⇑(map P.toInfinitesimal) : (a : P.Cotangent) → P.infinitesimal.Cotangent)
right :
  Surjective (α := P.Cotangent) (β := P.infinitesimal.Cotangent)
    (⇑(map P.toInfinitesimal) : (a : P.Cotangent) → P.infinitesimal.Cotangent)
⊢ Function.Bijective (α := P.Cotangent) (β := P.infinitesimal.Cotangent)
    (⇑(map P.toInfinitesimal) : (a : P.Cotangent) → P.infinitesimal.Cotangent)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
left :
  ∀ (a : P.Cotangent),
    Eq (α := P.infinitesimal.Cotangent)
        ((map P.toInfinitesimal : (a : P.Cotangent) → P.infinitesimal.Cotangent) a : P.infinitesimal.Cotangent)
        (0 : P.infinitesimal.Cotangent) →
      a = 0
⊢ Function.Injective (α := P.Cotangent) (β := P.infinitesimal.Cotangent)
    (⇑(map P.toInfinitesimal) : (a : P.Cotangent) → P.infinitesimal.Cotangent)

Tactic:
rw [injective_iff_map_eq_zero]

Premises used: injective_iff_map_eq_zero
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
x : P.Cotangent
hx :
  Eq (α := P.infinitesimal.Cotangent)
    ((map P.toInfinitesimal : (a : P.Cotangent) → P.infinitesimal.Cotangent) x : P.infinitesimal.Cotangent)
    (0 : P.infinitesimal.Cotangent)
left :
  ∀ (x : ↥P.ker)
    (hx :
      Eq (α := P.infinitesimal.Cotangent)
        ((map P.toInfinitesimal : (a : P.Cotangent) → P.infinitesimal.Cotangent) ((mk : (a : ↥P.ker) → P.Cotangent) x) :
          P.infinitesimal.Cotangent)
        (0 : P.infinitesimal.Cotangent)),
    Eq (α := P.Cotangent) ((mk : (a : ↥P.ker) → P.Cotangent) x : P.Cotangent) (0 : P.Cotangent)
⊢ x = 0

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

Premises used: Algebra.Extension.Cotangent.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
x : ↥P.ker
hx :
  Eq (α := P.infinitesimal.Cotangent)
    ((map P.toInfinitesimal : (a : P.Cotangent) → P.infinitesimal.Cotangent) ((mk : (a : ↥P.ker) → P.Cotangent) x) :
      P.infinitesimal.Cotangent)
    (0 : P.infinitesimal.Cotangent)
⊢ Eq.{u + 1} (α := P.infinitesimal.ker.Cotangent)
    (val
      ((map P.toInfinitesimal : (a : P.Cotangent) → P.infinitesimal.Cotangent) ((mk : (a : ↥P.ker) → P.Cotangent) x)))
    (val 0)

Tactic:
apply_fun Cotangent.val at hx

Premises used: Algebra.Extension.Cotangent.val
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
x : ↥P.ker
hx :
  Eq.{u + 1} (α := P.infinitesimal.ker.Cotangent)
    (val
      ((map P.toInfinitesimal : (a : P.Cotangent) → P.infinitesimal.Cotangent) ((mk : (a : ↥P.ker) → P.Cotangent) x)))
    (val 0)
⊢ Membership.mem (α := P.infinitesimal.Ring) (HPow.hPow (β := ℕ) P.ker.cotangentIdeal 2)
    ((P.toInfinitesimal.toRingHom : (a : P.Ring) → P.infinitesimal.Ring) (↑x : P.Ring) : P.infinitesimal.Ring)

Tactic:
simp only [map_mk, Hom.toAlgHom_apply, val_mk, val_zero, Ideal.toCotangent_eq_zero,
        Extension.ker_infinitesimal] at hx

Premises used: Algebra.Extension.Cotangent.val_mk, Algebra.Extension.ker_infinitesimal, Ideal.toCotangent_eq_zero, Algebra.Extension.Cotangent.val_zero, Algebra.Extension.Cotangent.map_mk, Algebra.Extension.Hom.toAlgHom_apply
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
x : ↥P.ker
hx :
  Membership.mem (α := P.infinitesimal.Ring) (HPow.hPow (β := ℕ) P.ker.cotangentIdeal 2)
    ((P.toInfinitesimal.toRingHom : (a : P.Ring) → P.infinitesimal.Ring) (↑x : P.Ring) : P.infinitesimal.Ring)
⊢ Membership.mem (α := P.infinitesimal.Ring) (γ := Ideal P.infinitesimal.Ring) ⊥
    ((P.toInfinitesimal.toRingHom : (a : P.Ring) → P.infinitesimal.Ring) (↑x : P.Ring) : P.infinitesimal.Ring)

Tactic:
rw [Ideal.cotangentIdeal_square] at hx

Premises used: Ideal.cotangentIdeal_square