awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Smooth.Local
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsLocalRing S
inst_3 : Algebra R S
P : Extension.{u, u_1, u_2} R S
inst_4 : FormallySmooth.{u_1, u} R P.Ring
inst_5 : Module.Free.{u, u} P.Ring Ω[P.Ring⁄R]
inst_6 : Module.Finite.{u, u} P.Ring Ω[P.Ring⁄R]
h' : P.ker.FG
this_1 : Module.Finite.{u, u} P.Ring P.Cotangent
this : Module.Finite.{u_2, u} S P.Cotangent
rw : FormallySmooth R S ↔ ∃ (l' : P.CotangentSpace →ₗ[S] P.Cotangent), l' ∘ₗ P.cotangentComplex = LinearMap.id
rw₁ rw₂ :
  (∃ (l : P.CotangentSpace →ₗ[S] P.Cotangent), l ∘ₗ P.cotangentComplex = LinearMap.id) ↔
    ∃ (l' : P.CotangentSpace →ₗ[S] P.Cotangent), l' ∘ₗ P.cotangentComplex = LinearMap.id
⊢ FormallySmooth R S ↔
    Function.Injective (α := TensorProduct.{u_2, u_2, u} S (ResidueField S) P.Cotangent) (β :=
      ResidueField S ⊗[S] P.CotangentSpace)
      (⇑(LinearMap.lTensor (ResidueField S) P.cotangentComplex) :
        (a : ResidueField S ⊗[S] P.Cotangent) → ResidueField S ⊗[S] P.CotangentSpace)

Tactic:
rw [← IsLocalRing.split_injective_iff_lTensor_residueField_injective,
    P.formallySmooth_iff_split_injection]

Premises used: Algebra.Extension.formallySmooth_iff_split_injection, IsLocalRing.split_injective_iff_lTensor_residueField_injective
-- Module: Mathlib.RingTheory.Smooth.Local
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsLocalRing S
inst_3 : Algebra R S
P : Type u_3
inst_4 : CommRing P
inst_5 : Algebra R P
inst_6 : Algebra P S
inst_7 : IsScalarTower R P S
inst_8 : FormallySmooth R P
inst_9 : Module.Free P Ω[P⁄R]
inst_10 : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective.{u_3 + 1, u_2 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
h₂ : Ideal.FG (RingHom.ker (F := P →+* S) (algebraMap P S))
P' : Extension.{u_3, u_1, u_2} R S :=
  { Ring := P, commRing := inst_4, algebra₁ := inst_5, algebra₂ := inst_6, isScalarTower := inst_7,
    σ := Function.surjInv h₁, algebraMap_σ := ⋯ }
rw :
  Function.Injective (α := TensorProduct.{u_2, u_2, u_3} S (ResidueField S) P'.Cotangent) (β :=
      ResidueField S ⊗[S] P'.CotangentSpace)
      (⇑(LinearMap.lTensor (ResidueField S) P'.cotangentComplex) :
        (a : ResidueField S ⊗[S] P'.Cotangent) → ResidueField S ⊗[S] P'.CotangentSpace) ↔
    Function.Injective (α :=
      TensorProduct.{u_3, u_2, u_3} P (ResidueField S) ↥(RingHom.ker (F := P →+* S) (algebraMap P S))) (β :=
      TensorProduct.{u_3, u_2, u_3} P (ResidueField S) Ω[P⁄R])
      (⇑(cotangentComplexBaseChange R S P (ResidueField S)) :
        (a : ResidueField S ⊗[P] ↥(RingHom.ker (algebraMap P S))) → ResidueField S ⊗[P] Ω[P⁄R])
⊢ FormallySmooth R S ↔
    Function.Injective (α :=
      TensorProduct.{u_3, u_2, u_3} P (ResidueField S) ↥(RingHom.ker (F := P →+* S) (algebraMap P S))) (β :=
      TensorProduct.{u_3, u_2, u_3} P (ResidueField S) Ω[P⁄R])
      (⇑(cotangentComplexBaseChange R S P (ResidueField S)) :
        (a : ResidueField S ⊗[P] ↥(RingHom.ker (algebraMap P S))) → ResidueField S ⊗[P] Ω[P⁄R])

Tactic:
rw [Algebra.FormallySmooth.iff_injective_lTensor_residueField P' h₂]

Premises used: Algebra.FormallySmooth.iff_injective_lTensor_residueField
-- Module: Mathlib.RingTheory.Smooth.Local
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsLocalRing S
inst_3 : Algebra R S
P : Type u_3
inst_4 : CommRing P
inst_5 : Algebra R P
inst_6 : Algebra P S
inst_7 : IsScalarTower R P S
inst_8 : FormallySmooth R P
inst_9 : Module.Free P Ω[P⁄R]
inst_10 : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective.{u_3 + 1, u_2 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
h₂ : Ideal.FG (RingHom.ker (F := P →+* S) (algebraMap P S))
P' : Extension.{u_3, u_1, u_2} R S :=
  { Ring := P, commRing := inst_4, algebra₁ := inst_5, algebra₂ := inst_6, isScalarTower := inst_7,
    σ := Function.surjInv h₁, algebraMap_σ := ⋯ }
⊢ Function.Injective (α := TensorProduct.{u_2, u_2, u_3} S (ResidueField S) P'.Cotangent) (β :=
      ResidueField S ⊗[S] P'.CotangentSpace)
      (⇑(LinearMap.lTensor (ResidueField S) P'.cotangentComplex) :
        (a : ResidueField S ⊗[S] P'.Cotangent) → ResidueField S ⊗[S] P'.CotangentSpace) ↔
    Function.Injective (α :=
      TensorProduct.{u_3, u_2, u_3} P (ResidueField S) ↥(RingHom.ker (F := P →+* S) (algebraMap P S))) (β :=
      TensorProduct.{u_3, u_2, u_3} P (ResidueField S) Ω[P⁄R])
      (⇑((↑(AlgebraTensorModule.cancelBaseChange P'.Ring S (ResidueField S) (ResidueField S) Ω[P'.Ring⁄R]) :
                ResidueField S ⊗[S] (S ⊗[P'.Ring] Ω[P'.Ring⁄R]) →ₗ[ResidueField S]
                  ResidueField S ⊗[P'.Ring] Ω[P'.Ring⁄R]) ∘ₗ
              LinearMap.baseChange (ResidueField S) P'.cotangentComplex ∘ₗ
                (↑(LinearEquiv.symm
                        (AlgebraTensorModule.cancelBaseChange P'.Ring S (ResidueField S) (ResidueField S) ↥P'.ker) ≪≫ₗ
                      LinearEquiv.baseChange S (ResidueField S) (TensorProduct.{u_3, u_2, u_3} P'.Ring S ↥P'.ker)
                        P'.Cotangent P'.cotangentEquiv) :
                  ResidueField S ⊗[P'.Ring] ↥P'.ker →ₗ[ResidueField S] ResidueField S ⊗[S] P'.Cotangent) :
            LinearMap (R := ResidueField S) (RingHom.id (ResidueField S))
              (TensorProduct.{u_3, u_2, u_3} P'.Ring (ResidueField S)
                ↥(RingHom.ker (F := RingHom.{u_3, u_2} P'.Ring S) (algebraMap P'.Ring S)))
              (TensorProduct.{u_3, u_2, u_3} P'.Ring (ResidueField S) Ω[P'.Ring⁄R])) :
        (a : ResidueField S ⊗[P] ↥(RingHom.ker (algebraMap P S))) → ResidueField S ⊗[P] Ω[P⁄R])

Tactic:
.trans ?_ ((AlgebraTensorModule.cancelBaseChange P'.Ring S _ _
    Ω[P'.Ring⁄R]).comp_injective _).symm

Premises used: TensorProduct.AlgebraTensorModule.cancelBaseChange, LinearEquiv.toAddEquiv, Algebra.Extension.Ring, Iff.trans, KaehlerDifferential, Equiv.comp_injective, AddEquiv.toEquiv, Iff.symm
-- Module: Mathlib.RingTheory.Smooth.Local
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsLocalRing S
inst_3 : Algebra R S
P : Type u_3
inst_4 : CommRing P
inst_5 : Algebra R P
inst_6 : Algebra P S
inst_7 : IsScalarTower R P S
inst_8 : FormallySmooth R P
inst_9 : Module.Free P Ω[P⁄R]
inst_10 : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective.{u_3 + 1, u_2 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
h₂ : Ideal.FG (RingHom.ker (F := P →+* S) (algebraMap P S))
P' : Extension.{u_3, u_1, u_2} R S :=
  { Ring := P, commRing := inst_4, algebra₁ := inst_5, algebra₂ := inst_6, isScalarTower := inst_7,
    σ := Function.surjInv h₁, algebraMap_σ := ⋯ }
⊢ Function.Injective (α := TensorProduct.{u_2, u_2, u_3} S (ResidueField S) P'.Cotangent) (β :=
      ResidueField S ⊗[S] P'.CotangentSpace)
      (⇑(LinearMap.lTensor (ResidueField S) P'.cotangentComplex) :
        (a : ResidueField S ⊗[S] P'.Cotangent) → ResidueField S ⊗[S] P'.CotangentSpace) ↔
    Function.Injective (α :=
      TensorProduct.{u_3, u_2, u_3} P (ResidueField S) ↥(RingHom.ker (F := P →+* S) (algebraMap P S))) (β :=
      ResidueField S ⊗[S] TensorProduct.{u_3, u_2, u_3} P'.Ring S Ω[P'.Ring⁄R])
      (⇑(LinearMap.baseChange (ResidueField S) P'.cotangentComplex ∘ₗ
              (↑(LinearEquiv.symm
                      (AlgebraTensorModule.cancelBaseChange P'.Ring S (ResidueField S) (ResidueField S) ↥P'.ker) ≪≫ₗ
                    LinearEquiv.baseChange S (ResidueField S) (TensorProduct.{u_3, u_2, u_3} P'.Ring S ↥P'.ker)
                      P'.Cotangent P'.cotangentEquiv) :
                ResidueField S ⊗[P'.Ring] ↥P'.ker →ₗ[ResidueField S] ResidueField S ⊗[S] P'.Cotangent) :
            LinearMap (R := ResidueField S) (RingHom.id (ResidueField S))
              (TensorProduct.{u_3, u_2, u_3} P'.Ring (ResidueField S)
                ↥(RingHom.ker (F := RingHom.{u_3, u_2} P'.Ring S) (algebraMap P'.Ring S)))
              (ResidueField S ⊗[S] P'.CotangentSpace)) :
        (a : ResidueField S ⊗[P'.Ring] ↥(RingHom.ker (algebraMap P'.Ring S))) → ResidueField S ⊗[S] P'.CotangentSpace)

Tactic:
(((AlgebraTensorModule.cancelBaseChange P'.Ring S _ _ P'.ker).symm ≪≫ₗ
    P'.cotangentEquiv.baseChange (A := _)).injective_comp _).symm

Premises used: TensorProduct.AlgebraTensorModule.cancelBaseChange, LinearEquiv.symm, Algebra.Extension.ker, Quotient.liftOn', Set.Mem, AddCon.liftOn, Membership.mem, Subtype, LinearEquiv.toAddEquiv, Equiv.injective_comp, Algebra.Extension.Ring, LinearEquiv.baseChange, Algebra.Extension.cotangentEquiv, TensorProduct.tmul, AddEquiv.toEquiv, LinearEquiv.trans, AddCon.toQuotient, Iff.symm
-- Module: Mathlib.RingTheory.Smooth.Local
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsLocalRing S
inst_3 : Algebra R S
P : Type u_3
inst_4 : CommRing P
inst_5 : Algebra R P
inst_6 : Algebra P S
inst_7 : IsScalarTower R P S
inst_8 : FormallySmooth R P
inst_9 : Module.Free P Ω[P⁄R]
inst_10 : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective.{u_3 + 1, u_2 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
h₂ : Ideal.FG (RingHom.ker (F := P →+* S) (algebraMap P S))
P' : Extension.{u_3, u_1, u_2} R S :=
  { Ring := P, commRing := inst_4, algebra₁ := inst_5, algebra₂ := inst_6, isScalarTower := inst_7,
    σ := Function.surjInv h₁, algebraMap_σ := ⋯ }
⊢ Function.Injective (α := TensorProduct.{u_2, u_2, u_3} S (ResidueField S) P'.Cotangent) (β :=
      ResidueField S ⊗[S] P'.CotangentSpace)
      (⇑(LinearMap.lTensor (ResidueField S) P'.cotangentComplex) :
        (a : ResidueField S ⊗[S] P'.Cotangent) → ResidueField S ⊗[S] P'.CotangentSpace) ↔
    Function.Injective (α :=
      TensorProduct.{u_3, u_2, u_3} P (ResidueField S) ↥(RingHom.ker (F := P →+* S) (algebraMap P S))) (β :=
      ResidueField S ⊗[S] TensorProduct.{u_3, u_2, u_3} P'.Ring S Ω[P'.Ring⁄R])
      (⇑(LinearMap.baseChange (ResidueField S) P'.cotangentComplex ∘ₗ
              (↑(LinearEquiv.symm
                      (AlgebraTensorModule.cancelBaseChange P'.Ring S (ResidueField S) (ResidueField S) ↥P'.ker) ≪≫ₗ
                    LinearEquiv.baseChange S (ResidueField S) (TensorProduct.{u_3, u_2, u_3} P'.Ring S ↥P'.ker)
                      P'.Cotangent P'.cotangentEquiv) :
                ResidueField S ⊗[P'.Ring] ↥P'.ker →ₗ[ResidueField S] ResidueField S ⊗[S] P'.Cotangent) :
            LinearMap (R := ResidueField S) (RingHom.id (ResidueField S))
              (TensorProduct.{u_3, u_2, u_3} P'.Ring (ResidueField S)
                ↥(RingHom.ker (F := RingHom.{u_3, u_2} P'.Ring S) (algebraMap P'.Ring S)))
              (ResidueField S ⊗[S] P'.CotangentSpace)) :
        (a : ResidueField S ⊗[P'.Ring] ↥(RingHom.ker (algebraMap P'.Ring S))) → ResidueField S ⊗[S] P'.CotangentSpace)

Tactic:
exact (((AlgebraTensorModule.cancelBaseChange P'.Ring S _ _ P'.ker).symm ≪≫ₗ
    P'.cotangentEquiv.baseChange (A := _)).injective_comp _).symm

Premises used: TensorProduct.AlgebraTensorModule.cancelBaseChange, LinearEquiv.symm, Algebra.Extension.ker, Membership.mem, Subtype, LinearEquiv.toAddEquiv, Equiv.injective_comp, Algebra.Extension.Ring, LinearEquiv.baseChange, Algebra.Extension.cotangentEquiv, AddEquiv.toEquiv, LinearEquiv.trans, Iff.symm
-- Module: Mathlib.RingTheory.Smooth.Local
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsLocalRing S
inst_3 : Algebra R S
P : Type u_3
K : Type u_4
inst_4 : Field K
inst_5 : CommRing P
inst_6 : Algebra R P
inst_7 : Algebra P S
inst_8 : IsScalarTower R P S
inst_9 : Algebra S K
inst_10 : Algebra P K
inst_11 : IsScalarTower P S K
inst_12 : FormallySmooth R P
inst_13 : Module.Free P Ω[P⁄R]
inst_14 : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective.{u_3 + 1, u_2 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
h₂ : Ideal.FG (RingHom.ker (F := P →+* S) (algebraMap P S))
h₃ : LE.le (α := Ideal S) (maximalIdeal S) (RingHom.ker (F := S →+* K) (algebraMap S K))
f : ResidueField S →ₐ[S] K := Ideal.Quotient.liftₐ (maximalIdeal S) (ofId S K) h₃
this : Algebra.{u_2, u_4} (ResidueField S) K := f.toAlgebra
⊢ IsScalarTower S (ResidueField S) K

Tactic:
have := IsScalarTower.of_algebraMap_eq' f.comp_algebraMap.symm
-- Module: Mathlib.RingTheory.Smooth.Local
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsLocalRing S
inst_3 : Algebra R S
P : Type u_3
K : Type u_4
inst_4 : Field K
inst_5 : CommRing P
inst_6 : Algebra R P
inst_7 : Algebra P S
inst_8 : IsScalarTower R P S
inst_9 : Algebra S K
inst_10 : Algebra P K
inst_11 : IsScalarTower P S K
inst_12 : FormallySmooth R P
inst_13 : Module.Free P Ω[P⁄R]
inst_14 : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective.{u_3 + 1, u_2 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
h₂ : Ideal.FG (RingHom.ker (F := P →+* S) (algebraMap P S))
h₃ : LE.le (α := Ideal S) (maximalIdeal S) (RingHom.ker (F := S →+* K) (algebraMap S K))
f : ResidueField S →ₐ[S] K := Ideal.Quotient.liftₐ (maximalIdeal S) (ofId S K) h₃
this_1 : Algebra.{u_2, u_4} (ResidueField S) K := f.toAlgebra
this : IsScalarTower S (ResidueField S) K
⊢ IsScalarTower.{u_3, u_2, u_4} P (ResidueField S) K

Tactic:
have : IsScalarTower P (ResidueField S) K := .to₁₃₄ _ S _ _
-- Module: Mathlib.RingTheory.Smooth.Local
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsLocalRing S
inst_3 : Algebra R S
P : Type u_3
K : Type u_4
inst_4 : Field K
inst_5 : CommRing P
inst_6 : Algebra R P
inst_7 : Algebra P S
inst_8 : IsScalarTower R P S
inst_9 : Algebra S K
inst_10 : Algebra P K
inst_11 : IsScalarTower P S K
inst_12 : FormallySmooth R P
inst_13 : Module.Free P Ω[P⁄R]
inst_14 : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective.{u_3 + 1, u_2 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
h₂ : Ideal.FG (RingHom.ker (F := P →+* S) (algebraMap P S))
h₃ : LE.le (α := Ideal S) (maximalIdeal S) (RingHom.ker (F := S →+* K) (algebraMap S K))
f : ResidueField S →ₐ[S] K := Ideal.Quotient.liftₐ (maximalIdeal S) (ofId S K) h₃
this_1 : Algebra.{u_2, u_4} (ResidueField S) K := f.toAlgebra
this_2 : IsScalarTower S (ResidueField S) K
this : IsScalarTower.{u_3, u_2, u_4} P (ResidueField S) K
rw :
  Function.Injective (α :=
      K ⊗[ResidueField S]
        TensorProduct.{u_3, u_2, u_3} P (ResidueField S) ↥(RingHom.ker (F := P →+* S) (algebraMap P S)))
      (β := K ⊗[ResidueField S] TensorProduct.{u_3, u_2, u_3} P (ResidueField S) Ω[P⁄R])
      (⇑(LinearMap.lTensor K (cotangentComplexBaseChange R S P (ResidueField S))) :
        (a : K ⊗[ResidueField S] (ResidueField S ⊗[P] ↥(RingHom.ker (algebraMap P S)))) →
          K ⊗[ResidueField S] (ResidueField S ⊗[P] Ω[P⁄R])) ↔
    Function.Injective (α := K ⊗[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S))) (β := K ⊗[P] Ω[P⁄R])
      (⇑(cotangentComplexBaseChange R S P K) : (a : K ⊗[P] ↥(RingHom.ker (algebraMap P S))) → K ⊗[P] Ω[P⁄R])
⊢ FormallySmooth R S ↔
    Function.Injective (α := K ⊗[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S))) (β := K ⊗[P] Ω[P⁄R])
      (⇑(cotangentComplexBaseChange R S P K) : (a : K ⊗[P] ↥(RingHom.ker (algebraMap P S))) → K ⊗[P] Ω[P⁄R])

Tactic:
rw [FormallySmooth.iff_injective_cotangentComplexBaseChange_residueField P h₁ h₂,
    ← Module.FaithfullyFlat.lTensor_injective_iff_injective _ K]

Premises used: Module.FaithfullyFlat.lTensor_injective_iff_injective, Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange_residueField
-- Module: Mathlib.RingTheory.Smooth.Local
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsLocalRing S
inst_3 : Algebra R S
P : Type u_3
K : Type u_4
inst_4 : Field K
inst_5 : CommRing P
inst_6 : Algebra R P
inst_7 : Algebra P S
inst_8 : IsScalarTower R P S
inst_9 : Algebra S K
inst_10 : Algebra P K
inst_11 : IsScalarTower P S K
inst_12 : FormallySmooth R P
inst_13 : Module.Free P Ω[P⁄R]
inst_14 : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective.{u_3 + 1, u_2 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
h₂ : Ideal.FG (RingHom.ker (F := P →+* S) (algebraMap P S))
h₃ : LE.le (α := Ideal S) (maximalIdeal S) (RingHom.ker (F := S →+* K) (algebraMap S K))
f : ResidueField S →ₐ[S] K := Ideal.Quotient.liftₐ (maximalIdeal S) (ofId S K) h₃
this_1 : Algebra.{u_2, u_4} (ResidueField S) K := f.toAlgebra
this_2 : IsScalarTower S (ResidueField S) K
this : IsScalarTower.{u_3, u_2, u_4} P (ResidueField S) K
x : ↥(RingHom.ker (F := P →+* S) (algebraMap P S))
⊢ Eq (α := K ⊗[P] Ω[P⁄R])
    ((((AlgebraTensorModule.curry
                  ((↑(AlgebraTensorModule.cancelBaseChange P (ResidueField S) K K Ω[P⁄R]) :
                      K ⊗[ResidueField S] (ResidueField S ⊗[P] Ω[P⁄R]) →ₗ[K] K ⊗[P] Ω[P⁄R]) ∘ₗ
                    LinearMap.baseChange K (cotangentComplexBaseChange R S P (ResidueField S)) ∘ₗ
                      (↑(LinearEquiv.symm
                            (AlgebraTensorModule.cancelBaseChange P (ResidueField S) K K
                              ↥(RingHom.ker (F := P →+* S) (algebraMap P S)))) :
                        K ⊗[P] ↥(RingHom.ker (algebraMap P S)) →ₗ[K]
                          K ⊗[ResidueField S] (ResidueField S ⊗[P] ↥(RingHom.ker (algebraMap P S))))) :
                K →ₗ[K] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) →ₗ[P] K ⊗[P] Ω[P⁄R]) :
              (a : K) → ↥(RingHom.ker (algebraMap P S)) →ₗ[P] K ⊗[P] Ω[P⁄R])
            1 :
          (a : ↥(RingHom.ker (algebraMap P S))) → K ⊗[P] Ω[P⁄R])
        x :
      K ⊗[P] Ω[P⁄R])
    ((((AlgebraTensorModule.curry (cotangentComplexBaseChange R S P K) :
                K →ₗ[K] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) →ₗ[P] K ⊗[P] Ω[P⁄R]) :
              (a : K) → ↥(RingHom.ker (algebraMap P S)) →ₗ[P] K ⊗[P] Ω[P⁄R])
            1 :
          (a : ↥(RingHom.ker (algebraMap P S))) → K ⊗[P] Ω[P⁄R])
        x :
      K ⊗[P] Ω[P⁄R])

Tactic:
simp [cotangentComplexBaseChange_tmul]

Premises used: KaehlerDifferential.cotangentComplexBaseChange_tmul
-- Module: Mathlib.RingTheory.Smooth.Local
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsLocalRing S
inst_3 : Algebra R S
P : Type u_3
K : Type u_4
inst_4 : Field K
inst_5 : CommRing P
inst_6 : Algebra R P
inst_7 : Algebra P S
inst_8 : IsScalarTower R P S
inst_9 : Algebra S K
inst_10 : Algebra P K
inst_11 : IsScalarTower P S K
inst_12 : FormallySmooth R P
inst_13 : Module.Free P Ω[P⁄R]
inst_14 : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective.{u_3 + 1, u_2 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
h₂ : Ideal.FG (RingHom.ker (F := P →+* S) (algebraMap P S))
h₃ : LE.le (α := Ideal S) (maximalIdeal S) (RingHom.ker (F := S →+* K) (algebraMap S K))
f : ResidueField S →ₐ[S] K := Ideal.Quotient.liftₐ (maximalIdeal S) (ofId S K) h₃
this_1 : Algebra.{u_2, u_4} (ResidueField S) K := f.toAlgebra
this_2 : IsScalarTower S (ResidueField S) K
this : IsScalarTower.{u_3, u_2, u_4} P (ResidueField S) K
⊢ Eq (α := K ⊗[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) →ₗ[K] K ⊗[P] Ω[P⁄R])
    ((↑(AlgebraTensorModule.cancelBaseChange P (ResidueField S) K K Ω[P⁄R]) :
          K ⊗[ResidueField S] (ResidueField S ⊗[P] Ω[P⁄R]) →ₗ[K] K ⊗[P] Ω[P⁄R]) ∘ₗ
        LinearMap.baseChange K (cotangentComplexBaseChange R S P (ResidueField S)) ∘ₗ
          (↑(LinearEquiv.symm
                (AlgebraTensorModule.cancelBaseChange P (ResidueField S) K K
                  ↥(RingHom.ker (F := P →+* S) (algebraMap P S)))) :
            K ⊗[P] ↥(RingHom.ker (algebraMap P S)) →ₗ[K]
              K ⊗[ResidueField S] (ResidueField S ⊗[P] ↥(RingHom.ker (algebraMap P S)))) :
      K ⊗[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) →ₗ[K] K ⊗[P] Ω[P⁄R])
    (cotangentComplexBaseChange R S P K : K ⊗[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) →ₗ[K] K ⊗[P] Ω[P⁄R])

Tactic:
have : (AlgebraTensorModule.cancelBaseChange _ _ _ _ _).toLinearMap ∘ₗ
      (cotangentComplexBaseChange R S P (ResidueField S)).baseChange K ∘ₗ
      (AlgebraTensorModule.cancelBaseChange _ _ _ _ _).symm.toLinearMap =
      (cotangentComplexBaseChange R S P K) := by
    ext; simp [cotangentComplexBaseChange_tmul]
-- Module: Mathlib.RingTheory.Smooth.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : EssFiniteType R A
h :
  ∀ (p : PrimeSpectrum A),
    Membership.mem (γ := Set (PrimeSpectrum A)) (smoothLocus R A) p ↔
      Membership.mem (γ := Set (PrimeSpectrum A)) ((Module.support A (H1Cotangent R A))ᶜ ∩ Module.freeLocus A Ω[A⁄R]) p
⊢ Eq (α := Set (PrimeSpectrum A)) (smoothLocus R A) ((Module.support A (H1Cotangent R A))ᶜ ∩ Module.freeLocus A Ω[A⁄R])

Tactic:
ext p
-- Module: Mathlib.RingTheory.Smooth.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : EssFiniteType R A
p : PrimeSpectrum A
h :
  Membership.mem (γ := Set (PrimeSpectrum A)) (smoothLocus R A) p ↔
    Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A)) ∧
      Module.Free.{u_2, u_2} (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])
⊢ Membership.mem (γ := Set (PrimeSpectrum A)) (smoothLocus R A) p ↔
    Membership.mem (γ := Set (PrimeSpectrum A)) ((Module.support A (H1Cotangent R A))ᶜ ∩ Module.freeLocus A Ω[A⁄R]) p

Tactic:
simp only [Set.mem_inter_iff, Set.mem_compl_iff, Module.notMem_support_iff,
    Module.mem_freeLocus]

Premises used: Set.mem_inter_iff, Module.notMem_support_iff, Module.mem_freeLocus, Set.mem_compl_iff
-- Module: Mathlib.RingTheory.Smooth.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : EssFiniteType R A
p : PrimeSpectrum A
⊢ Membership.mem (γ := Set (PrimeSpectrum A)) (smoothLocus R A) p ↔
    Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A)) ∧
      Module.Free.{u_2, u_2} (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])

Tactic:
(Algebra.formallySmooth_iff _ _).trans (and_comm.trans ?_)

Premises used: Set.Mem, setOf, and_comm, Algebra.smoothLocus, Iff.trans, Algebra.formallySmooth_iff
-- Module: Mathlib.RingTheory.Smooth.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : EssFiniteType R A
p : PrimeSpectrum A
h :
  Subsingleton (H1Cotangent.{u_1, u_2} R (Localization.AtPrime p.asIdeal)) ∧
      Module.Projective.{u_2, u_2} (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R] ↔
    Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A)) ∧
      Module.Free.{u_2, u_2} (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])
⊢ Membership.mem (γ := Set (PrimeSpectrum A)) (smoothLocus R A) p ↔
    Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A)) ∧
      Module.Free.{u_2, u_2} (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])

Tactic:
refine (Algebra.formallySmooth_iff _ _).trans (and_comm.trans ?_)

Premises used: and_comm, Iff.trans, Algebra.formallySmooth_iff
-- Module: Mathlib.RingTheory.Smooth.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : EssFiniteType R A
p : PrimeSpectrum A
h :
  Subsingleton (H1Cotangent.{u_1, u_2} R (Localization.AtPrime p.asIdeal)) ↔
    Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A))
h₁ :
  Module.Projective.{u_2, u_2} (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R] ↔
    Module.Free.{u_2, u_2} (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])
⊢ Subsingleton (H1Cotangent.{u_1, u_2} R (Localization.AtPrime p.asIdeal)) ∧
      Module.Projective.{u_2, u_2} (Localization.AtPrime p.asIdeal) Ω[Localization.AtPrime p.asIdeal⁄R] ↔
    Subsingleton (LocalizedModule p.asIdeal.primeCompl (H1Cotangent R A)) ∧
      Module.Free.{u_2, u_2} (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])

Tactic:
congr! 1