awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (goal)
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.IsStandardEtale R S
x : S ⊗[R] B
hx : Membership.mem (γ := Subalgebra S (S ⊗[R] B)) (integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)) x
⊢ Membership.mem (γ := Subalgebra S (S ⊗[R] B))
    (AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B))
        (Algebra.TensorProduct.map (AlgHom.id S S) (Subalgebra.val (integralClosure R B)) :
          TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B) →ₐ[S] S ⊗[R] B) :
      Subalgebra S (S ⊗[R] B))
    x
have refine : (↑(Subalgebra.map Algebra.TensorProduct.includeRight (integralClosure R B)) : Set (S ⊗[R] B)) ⊆
  (↑(AlgHom.range (A := TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B))
          (Algebra.TensorProduct.map (AlgHom.id S S) (Subalgebra.val (integralClosure R B)) :
            TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B) →ₐ[S] S ⊗[R] B) :
        Subalgebra S (S ⊗[R] B)) :
    Set (S ⊗[R] B))
Tactic: refine Algebra.adjoin_le ?_ (mem_adjoin_map_integralClosure_of_isStandardEtale x hx)
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (goal)
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.Smooth R S
m : PrimeSpectrum S
⊢ ∃ f ∉ m.asIdeal,
    Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R (Localization.Away f) ↥(integralClosure R B)) (β :=
      ↥(integralClosure (Localization.Away f) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away f) B) :
          Subalgebra (Localization.Away f) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away f) B)))
      (⇑(toIntegralClosure R (Localization.Away f) B) :
        (a : Localization.Away f ⊗[R] ↥(integralClosure R B)) →
          ↥(integralClosure (Localization.Away f) (Localization.Away f ⊗[R] B)))
have obtain : ∀ (f : S) (hfm : f ∉ m.asIdeal) (n : ℕ) (w : Algebra.{u_1, u_2} (MvPolynomial (Fin n) R) (Localization.Away f)),
  IsScalarTower.{u_1, u_1, u_2} R (MvPolynomial (Fin n) R) (Localization.Away f) →
    Algebra.IsStandardEtale.{u_1, u_2} (MvPolynomial (Fin n) R) (Localization.Away f) →
      ∃ f ∉ m.asIdeal,
        Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R (Localization.Away f) ↥(integralClosure R B)) (β :=
          ↥(integralClosure (Localization.Away f) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away f) B) :
              Subalgebra (Localization.Away f) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away f) B)))
          (⇑(toIntegralClosure R (Localization.Away f) B) :
            (a : Localization.Away f ⊗[R] ↥(integralClosure R B)) →
              ↥(integralClosure (Localization.Away f) (Localization.Away f ⊗[R] B)))
Tactic: obtain ⟨f, hfm, n, _, _, _⟩ :=
      Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial (R := R) (p := m.asIdeal)
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (hypothesis)
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.Smooth R S
⊢ Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B)) (β :=
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))
    (⇑(toIntegralClosure R S B) : (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))
have this : ∀ (m : PrimeSpectrum S),
  ∃ f ∉ m.asIdeal,
    Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R (Localization.Away f) ↥(integralClosure R B)) (β :=
      ↥(integralClosure (Localization.Away f) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away f) B) :
          Subalgebra (Localization.Away f) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away f) B)))
      (⇑(toIntegralClosure R (Localization.Away f) B) :
        (a : Localization.Away f ⊗[R] ↥(integralClosure R B)) →
          ↥(integralClosure (Localization.Away f) (Localization.Away f ⊗[R] B)))
Tactic: have (m : PrimeSpectrum S) : ∃ f ∉ m.asIdeal,
      Function.Bijective (toIntegralClosure R (Localization.Away f) B) := by
    obtain ⟨f, hfm, n, _, _, _⟩ :=
      Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial (R := R) (p := m.asIdeal)
    exact ⟨f, hfm, toIntegralClosure_bijective_of_tower (S := MvPolynomial (Fin n) R)
      toIntegralClosure_mvPolynomial_bijective toIntegralClosure_bijective_of_isStandardEtale⟩
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (goal)
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.Smooth R S
this :
  ∀ (m : PrimeSpectrum S),
    ∃ f ∉ m.asIdeal,
      Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R (Localization.Away f) ↥(integralClosure R B)) (β :=
        ↥(integralClosure (Localization.Away f) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away f) B) :
            Subalgebra (Localization.Away f) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away f) B)))
        (⇑(toIntegralClosure R (Localization.Away f) B) :
          (a : Localization.Away f ⊗[R] ↥(integralClosure R B)) →
            ↥(integralClosure (Localization.Away f) (Localization.Away f ⊗[R] B)))
⊢ Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B)) (β :=
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))
    (⇑(toIntegralClosure R S B) : (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))
have choose : ∀ (f : (m : PrimeSpectrum S) → S) (hfm : ∀ (m : PrimeSpectrum S), f m ∉ m.asIdeal)
  (hf :
    ∀ (m : PrimeSpectrum S),
      Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) ↥(integralClosure R B)) (β :=
        ↥(integralClosure (Localization.Away (f m)) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) B) :
            Subalgebra (Localization.Away (f m)) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) B)))
        (⇑(toIntegralClosure R (Localization.Away (f m)) B) :
          (a : Localization.Away (f m) ⊗[R] ↥(integralClosure R B)) →
            ↥(integralClosure (Localization.Away (f m)) (Localization.Away (f m) ⊗[R] B)))),
  Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B)) (β :=
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))
    (⇑(toIntegralClosure R S B) : (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))
Tactic: choose f hfm hf using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (goal)
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.Smooth R S
f : (m : PrimeSpectrum S) → S
hfm : ∀ (m : PrimeSpectrum S), f m ∉ m.asIdeal
hf :
  ∀ (m : PrimeSpectrum S),
    Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) ↥(integralClosure R B)) (β :=
      ↥(integralClosure (Localization.Away (f m)) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) B) :
          Subalgebra (Localization.Away (f m)) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) B)))
      (⇑(toIntegralClosure R (Localization.Away (f m)) B) :
        (a : Localization.Away (f m) ⊗[R] ↥(integralClosure R B)) →
          ↥(integralClosure (Localization.Away (f m)) (Localization.Away (f m) ⊗[R] B)))
⊢ Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R S ↥(integralClosure R B)) (β :=
    ↥(integralClosure S (S ⊗[R] B) : Subalgebra S (S ⊗[R] B)))
    (⇑(toIntegralClosure R S B) : (a : S ⊗[R] ↥(integralClosure R B)) → ↥(integralClosure S (S ⊗[R] B)))
have refine : Eq (α := Ideal S) (Ideal.span (Set.range f)) ⊤
Tactic: refine TensorProduct.toIntegralClosure_bijective_of_isLocalizationAway (R := R)
    (s := Set.range f) (B := B) ?_ (Localization.Away ·.1) (Set.forall_subtype_range_iff.mpr hf)
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (goal)
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.Smooth R S
f : (m : PrimeSpectrum S) → S
hfm : ∀ (m : PrimeSpectrum S), f m ∉ m.asIdeal
hf :
  ∀ (m : PrimeSpectrum S),
    Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) ↥(integralClosure R B)) (β :=
      ↥(integralClosure (Localization.Away (f m)) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) B) :
          Subalgebra (Localization.Away (f m)) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) B)))
      (⇑(toIntegralClosure R (Localization.Away (f m)) B) :
        (a : Localization.Away (f m) ⊗[R] ↥(integralClosure R B)) →
          ↥(integralClosure (Localization.Away (f m)) (Localization.Away (f m) ⊗[R] B)))
⊢ Eq (α := Ideal S) (Ideal.span (Set.range f)) ⊤
have by_contra : ∀ (H : ¬Eq (α := Ideal S) (Ideal.span (Set.range f)) ⊤), False
Tactic: by_contra H
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.IntegralClosure (goal)
Goal:
R : Type u_1
S : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra.Smooth R S
f : (m : PrimeSpectrum S) → S
hfm : ∀ (m : PrimeSpectrum S), f m ∉ m.asIdeal
hf :
  ∀ (m : PrimeSpectrum S),
    Function.Bijective (α := TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) ↥(integralClosure R B)) (β :=
      ↥(integralClosure (Localization.Away (f m)) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) B) :
          Subalgebra (Localization.Away (f m)) (TensorProduct.{u_1, u_2, u_3} R (Localization.Away (f m)) B)))
      (⇑(toIntegralClosure R (Localization.Away (f m)) B) :
        (a : Localization.Away (f m) ⊗[R] ↥(integralClosure R B)) →
          ↥(integralClosure (Localization.Away (f m)) (Localization.Away (f m) ⊗[R] B)))
H : ¬Eq (α := Ideal S) (Ideal.span (Set.range f)) ⊤
⊢ False
have obtain : ∀ (m : Ideal S) (hm : m.IsMaximal) (e : Ideal.span (Set.range f) ≤ m), False
Tactic: obtain ⟨m, hm, e⟩ := Ideal.exists_le_maximal _ H
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Local (hypothesis)
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
⊢ 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)
have this : Module.Finite.{u, u} P.Ring P.Cotangent
Tactic: have : Module.Finite P.Ring P.Cotangent :=
    have : Module.Finite P.Ring P.ker := .of_fg h'
    .of_surjective _ Extension.Cotangent.mk_surjective
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Local (hypothesis)
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 : Module.Finite.{u, u} P.Ring P.Cotangent
⊢ 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)
have this₁ : Module.Finite.{u_2, u} S P.Cotangent
Tactic: have : Module.Finite S P.Cotangent := Module.Finite.of_restrictScalars_finite P.Ring _ _
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Local (goal)
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
⊢ 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)
have rw : FormallySmooth R S ↔ ∃ (l' : P.CotangentSpace →ₗ[S] P.Cotangent), l' ∘ₗ P.cotangentComplex = LinearMap.id
Tactic: rw [← IsLocalRing.split_injective_iff_lTensor_residueField_injective,
    P.formallySmooth_iff_split_injection]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Local (goal)
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
⊢ 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)
have rw₁ : (∃ (l : P.CotangentSpace →ₗ[S] P.Cotangent), l ∘ₗ P.cotangentComplex = LinearMap.id) ↔
  ∃ (l' : P.CotangentSpace →ₗ[S] P.Cotangent), l' ∘ₗ P.cotangentComplex = LinearMap.id
Tactic: rw [← IsLocalRing.split_injective_iff_lTensor_residueField_injective,
    P.formallySmooth_iff_split_injection]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Local (goal)
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_σ := ⋯ }
⊢ 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])
have 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])
Tactic: rw [Algebra.FormallySmooth.iff_injective_lTensor_residueField P' h₂]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Local (goal)
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])
      (⇑(cotangentComplexBaseChange R S P (ResidueField S)) :
        (a : ResidueField S ⊗[P] ↥(RingHom.ker (algebraMap P S))) → ResidueField S ⊗[P] Ω[P⁄R])
have 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])
    (⇑((↑(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: rw [P'.cotangentComplexBaseChange_eq_lTensor_cotangentComplex (ResidueField S)]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Local (hypothesis)
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
⊢ 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])
have this₁ : IsScalarTower S (ResidueField S) K
Tactic: have := IsScalarTower.of_algebraMap_eq' f.comp_algebraMap.symm
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Local (hypothesis)
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
⊢ 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])
have this₁ : IsScalarTower.{u_3, u_2, u_4} P (ResidueField S) K
Tactic: have : IsScalarTower P (ResidueField S) K := .to₁₃₄ _ S _ _
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Local (goal)
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
⊢ 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])
have 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])
Tactic: rw [FormallySmooth.iff_injective_cotangentComplexBaseChange_residueField P h₁ h₂,
    ← Module.FaithfullyFlat.lTensor_injective_iff_injective _ K]