awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
P : Type u_2
inst_3 : CommRing P
inst_4 : Algebra R P
inst_5 : FormallySmooth R P
inst_6 : Algebra P A
inst_7 : IsScalarTower R P A
hf : Function.Surjective.{u_2 + 1, v + 1} (α := P) (β := A) (⇑(algebraMap P A) : (a : P) → A)
⊢ (Function.Injective (α := Ideal.Cotangent (RingHom.ker (F := P →+* A) (algebraMap P A))) (β := A ⊗[P] Ω[P⁄R])
        (⇑(kerCotangentToTensor R P A) : (a : (RingHom.ker (algebraMap P A)).Cotangent) → A ⊗[P] Ω[P⁄R]) ∧
      ∃ (i : Ω[A⁄R] →ₗ[A] A ⊗[P] Ω[P⁄R]), mapBaseChange R P A ∘ₗ i = LinearMap.id) ↔
    ∃ (l : A ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* A) (algebraMap P A))),
      l ∘ₗ kerCotangentToTensor R P A = LinearMap.id
have h : (∃ (i : Ω[A⁄R] →ₗ[A] A ⊗[P] Ω[P⁄R]), mapBaseChange R P A ∘ₗ i = LinearMap.id) ↔
  ∃ (l : Ω[A⁄R] →ₗ[P] A ⊗[P] Ω[P⁄R]),
    (↑P :
            {S : Type v} →
              {M : Type (max u_2 v)} →
                {M₂ : Type v} →
                  [inst : Semiring P] →
                    [inst_8 : Semiring S] →
                      [inst_9 : AddCommMonoid M] →
                        [inst_10 : AddCommMonoid M₂] →
                          [inst_11 : Module P M] →
                            [inst_12 : Module P M₂] →
                              [inst_13 : Module S M] →
                                [inst_14 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ P S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[P] M₂)
          (mapBaseChange R P A) ∘ₗ
        l =
      LinearMap.id
Tactic: convert!
    (((exact_kerCotangentToTensor_mapBaseChange R _ _ hf).split_tfae' (g :=
          (KaehlerDifferential.mapBaseChange R P A).restrictScalars P)).out
      0 1) using 2
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
P : Type u_2
inst_3 : CommRing P
inst_4 : Algebra R P
inst_5 : FormallySmooth R P
inst_6 : Algebra P A
inst_7 : IsScalarTower R P A
hf : Function.Surjective.{u_2 + 1, v + 1} (α := P) (β := A) (⇑(algebraMap P A) : (a : P) → A)
h :
  (∃ (i : Ω[A⁄R] →ₗ[A] A ⊗[P] Ω[P⁄R]), mapBaseChange R P A ∘ₗ i = LinearMap.id) ↔
    ∃ (l : Ω[A⁄R] →ₗ[P] A ⊗[P] Ω[P⁄R]),
      (↑P :
              {S : Type v} →
                {M : Type (max u_2 v)} →
                  {M₂ : Type v} →
                    [inst : Semiring P] →
                      [inst_8 : Semiring S] →
                        [inst_9 : AddCommMonoid M] →
                          [inst_10 : AddCommMonoid M₂] →
                            [inst_11 : Module P M] →
                              [inst_12 : Module P M₂] →
                                [inst_13 : Module S M] →
                                  [inst_14 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ P S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[P] M₂)
            (mapBaseChange R P A) ∘ₗ
          l =
        LinearMap.id
⊢ (Function.Injective (α := Ideal.Cotangent (RingHom.ker (F := P →+* A) (algebraMap P A))) (β := A ⊗[P] Ω[P⁄R])
        (⇑(kerCotangentToTensor R P A) : (a : (RingHom.ker (algebraMap P A)).Cotangent) → A ⊗[P] Ω[P⁄R]) ∧
      ∃ (i : Ω[A⁄R] →ₗ[A] A ⊗[P] Ω[P⁄R]), mapBaseChange R P A ∘ₗ i = LinearMap.id) ↔
    ∃ (l : A ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* A) (algebraMap P A))),
      l ∘ₗ kerCotangentToTensor R P A = LinearMap.id
have h₁ : (∃ (l : A ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* A) (algebraMap P A))),
    l ∘ₗ kerCotangentToTensor R P A = LinearMap.id) ↔
  Function.Surjective (α := A ⊗[P] Ω[P⁄R]) (β := Ω[A⁄R])
      (⇑((↑P :
              {S : Type v} →
                {M : Type (max u_2 v)} →
                  {M₂ : Type v} →
                    [inst : Semiring P] →
                      [inst_8 : Semiring S] →
                        [inst_9 : AddCommMonoid M] →
                          [inst_10 : AddCommMonoid M₂] →
                            [inst_11 : Module P M] →
                              [inst_12 : Module P M₂] →
                                [inst_13 : Module S M] →
                                  [inst_14 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ P S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[P] M₂)
            (mapBaseChange R P A)) :
        (a : A ⊗[P] Ω[P⁄R]) → Ω[A⁄R]) ∧
    ∃ (l : A ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* A) (algebraMap P A))),
      l ∘ₗ kerCotangentToTensor R P A = LinearMap.id
Tactic: convert!
    (((exact_kerCotangentToTensor_mapBaseChange R _ _ hf).split_tfae' (g :=
          (KaehlerDifferential.mapBaseChange R P A).restrictScalars P)).out
      0 1) using 2
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
P : Type u_2
inst_3 : CommRing P
inst_4 : Algebra R P
inst_5 : FormallySmooth R P
inst_6 : Algebra P A
inst_7 : IsScalarTower R P A
hf : Function.Surjective.{u_2 + 1, v + 1} (α := P) (β := A) (⇑(algebraMap P A) : (a : P) → A)
⊢ (∃ (i : Ω[A⁄R] →ₗ[A] A ⊗[P] Ω[P⁄R]), mapBaseChange R P A ∘ₗ i = LinearMap.id) ↔
    ∃ (l : Ω[A⁄R] →ₗ[P] A ⊗[P] Ω[P⁄R]),
      (↑P :
              {S : Type v} →
                {M : Type (max u_2 v)} →
                  {M₂ : Type v} →
                    [inst : Semiring P] →
                      [inst_8 : Semiring S] →
                        [inst_9 : AddCommMonoid M] →
                          [inst_10 : AddCommMonoid M₂] →
                            [inst_11 : Module P M] →
                              [inst_12 : Module P M₂] →
                                [inst_13 : Module S M] →
                                  [inst_14 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ P S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[P] M₂)
            (mapBaseChange R P A) ∘ₗ
          l =
        LinearMap.id
have h : (∃ (a : Ω[A⁄R] →ₗ[P] A ⊗[P] Ω[P⁄R]),
    Eq (α := Ω[A⁄R] →ₗ[A] Ω[A⁄R])
      (mapBaseChange R P A ∘ₗ
        (AddEquiv.toEquiv
              (LinearEquiv.toAddEquiv
                (LinearMap.extendScalarsOfSurjectiveEquiv hf :
                  (Ω[A⁄R] →ₗ[P] A ⊗[P] Ω[P⁄R]) ≃ₗ[P] Ω[A⁄R] →ₗ[A] A ⊗[P] Ω[P⁄R])) :
            (a : Ω[A⁄R] →ₗ[P] A ⊗[P] Ω[P⁄R]) → Ω[A⁄R] →ₗ[A] A ⊗[P] Ω[P⁄R])
          a)
      LinearMap.id) ↔
  ∃ (l : Ω[A⁄R] →ₗ[P] A ⊗[P] Ω[P⁄R]),
    (↑P :
            {S : Type v} →
              {M : Type (max u_2 v)} →
                {M₂ : Type v} →
                  [inst : Semiring P] →
                    [inst_8 : Semiring S] →
                      [inst_9 : AddCommMonoid M] →
                        [inst_10 : AddCommMonoid M₂] →
                          [inst_11 : Module P M] →
                            [inst_12 : Module P M₂] →
                              [inst_13 : Module S M] →
                                [inst_14 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ P S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[P] M₂)
          (mapBaseChange R P A) ∘ₗ
        l =
      LinearMap.id
Tactic: rw [← (LinearMap.extendScalarsOfSurjectiveEquiv hf).exists_congr_right]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
P : Type u_2
inst_3 : CommRing P
inst_4 : Algebra R P
inst_5 : FormallySmooth R P
inst_6 : Algebra P A
inst_7 : IsScalarTower R P A
hf : Function.Surjective.{u_2 + 1, v + 1} (α := P) (β := A) (⇑(algebraMap P A) : (a : P) → A)
⊢ (∃ (l : A ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* A) (algebraMap P A))),
      l ∘ₗ kerCotangentToTensor R P A = LinearMap.id) ↔
    Function.Surjective (α := A ⊗[P] Ω[P⁄R]) (β := Ω[A⁄R])
        (⇑((↑P :
                {S : Type v} →
                  {M : Type (max u_2 v)} →
                    {M₂ : Type v} →
                      [inst : Semiring P] →
                        [inst_8 : Semiring S] →
                          [inst_9 : AddCommMonoid M] →
                            [inst_10 : AddCommMonoid M₂] →
                              [inst_11 : Module P M] →
                                [inst_12 : Module P M₂] →
                                  [inst_13 : Module S M] →
                                    [inst_14 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ P S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[P] M₂)
              (mapBaseChange R P A)) :
          (a : A ⊗[P] Ω[P⁄R]) → Ω[A⁄R]) ∧
      ∃ (l : A ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* A) (algebraMap P A))),
        l ∘ₗ kerCotangentToTensor R P A = LinearMap.id
have h : (∃ (l : A ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* A) (algebraMap P A))),
    l ∘ₗ kerCotangentToTensor R P A = LinearMap.id) ↔
  ∃ (l : A ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* A) (algebraMap P A))),
    l ∘ₗ kerCotangentToTensor R P A = LinearMap.id
Tactic: rw [and_iff_right (by exact mapBaseChange_surjective R P A hf)]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
P : Extension.{w, u, v} R A
inst_3 : FormallySmooth.{u, w} R P.Ring
⊢ FormallySmooth R A ↔ ∃ (l : P.CotangentSpace →ₗ[A] P.Cotangent), l ∘ₗ P.cotangentComplex = LinearMap.id
have refine : (∃ (l :
    LinearMap (R := P.Ring) (RingHom.id P.Ring) (TensorProduct.{w, v, w} P.Ring A Ω[P.Ring⁄R])
      (Ideal.Cotangent (RingHom.ker (F := RingHom.{w, v} P.Ring A) (algebraMap P.Ring A)))),
    l ∘ₗ kerCotangentToTensor R P.Ring A = LinearMap.id) ↔
  ∃ (l : P.CotangentSpace →ₗ[A] P.Cotangent), l ∘ₗ P.cotangentComplex = LinearMap.id
Tactic: refine (Algebra.FormallySmooth.iff_split_injection P.algebraMap_surjective).trans ?_
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
P : Extension.{w, u, v} R A
inst_3 : FormallySmooth.{u, w} R P.Ring
r : P.Ring
m : P.ker.Cotangent
⊢ Cotangent.val (Equiv.toFun (AddEquiv.toEquiv (AddEquiv.refl P.ker.Cotangent)) (r • m)) =
    (HSMul.hSMul (α := P.Ring) ((RingHom.id P.Ring : (a : P.Ring) → P.Ring) r : P.Ring)
        (Equiv.toFun (AddEquiv.toEquiv (AddEquiv.refl P.ker.Cotangent)) m)).val
have e : Cotangent.val (r • m) = r • Cotangent.val m
Tactic: simp
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
P : Extension.{w, u, v} R A
inst_3 : FormallySmooth.{u, w} R P.Ring
e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent :=
  let __spread.0 : P.ker.Cotangent ≃+ P.ker.Cotangent := AddEquiv.refl P.ker.Cotangent;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
⊢ (∃ (l :
      LinearMap (R := P.Ring) (RingHom.id P.Ring) (TensorProduct.{w, v, w} P.Ring A Ω[P.Ring⁄R])
        (Ideal.Cotangent (RingHom.ker (F := RingHom.{w, v} P.Ring A) (algebraMap P.Ring A)))),
      l ∘ₗ kerCotangentToTensor R P.Ring A = LinearMap.id) ↔
    ∃ (l : P.CotangentSpace →ₗ[A] P.Cotangent), l ∘ₗ P.cotangentComplex = LinearMap.id
have mp : (∃ (l :
    LinearMap (R := P.Ring) (RingHom.id P.Ring) (TensorProduct.{w, v, w} P.Ring A Ω[P.Ring⁄R])
      (Ideal.Cotangent (RingHom.ker (F := RingHom.{w, v} P.Ring A) (algebraMap P.Ring A)))),
    l ∘ₗ kerCotangentToTensor R P.Ring A = LinearMap.id) →
  ∃ (l : P.CotangentSpace →ₗ[A] P.Cotangent), l ∘ₗ P.cotangentComplex = LinearMap.id
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
P : Extension.{w, u, v} R A
inst_3 : FormallySmooth.{u, w} R P.Ring
e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent :=
  let __spread.0 : P.ker.Cotangent ≃+ P.ker.Cotangent := AddEquiv.refl P.ker.Cotangent;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
mp :
  (∃ (l :
      LinearMap (R := P.Ring) (RingHom.id P.Ring) (TensorProduct.{w, v, w} P.Ring A Ω[P.Ring⁄R])
        (Ideal.Cotangent (RingHom.ker (F := RingHom.{w, v} P.Ring A) (algebraMap P.Ring A)))),
      l ∘ₗ kerCotangentToTensor R P.Ring A = LinearMap.id) →
    ∃ (l : P.CotangentSpace →ₗ[A] P.Cotangent), l ∘ₗ P.cotangentComplex = LinearMap.id
⊢ (∃ (l :
      LinearMap (R := P.Ring) (RingHom.id P.Ring) (TensorProduct.{w, v, w} P.Ring A Ω[P.Ring⁄R])
        (Ideal.Cotangent (RingHom.ker (F := RingHom.{w, v} P.Ring A) (algebraMap P.Ring A)))),
      l ∘ₗ kerCotangentToTensor R P.Ring A = LinearMap.id) ↔
    ∃ (l : P.CotangentSpace →ₗ[A] P.Cotangent), l ∘ₗ P.cotangentComplex = LinearMap.id
have mpr : (∃ (l : P.CotangentSpace →ₗ[A] P.Cotangent), l ∘ₗ P.cotangentComplex = LinearMap.id) →
  ∃ (l :
    LinearMap (R := P.Ring) (RingHom.id P.Ring) (TensorProduct.{w, v, w} P.Ring A Ω[P.Ring⁄R])
      (Ideal.Cotangent (RingHom.ker (F := RingHom.{w, v} P.Ring A) (algebraMap P.Ring A)))),
    l ∘ₗ kerCotangentToTensor R P.Ring A = LinearMap.id
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
P : Type u_2
inst_3 : CommRing P
inst_4 : Algebra R P
inst_5 : FormallySmooth R P
f : P →ₐ[R] A
hf : Function.Surjective.{u_2 + 1, v + 1} (α := P) (β := A) (⇑f : (a : P) → A)
this : Algebra P A := f.toAlgebra
⊢ FormallySmooth R A ↔
    ∃ (g : AlgHom.{u, v, u_2} R A (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker f.toRingHom) 2)),
      f.kerSquareLift.comp g = AlgHom.id R A
have rw : Nonempty
    { g :
      AlgHom.{u, v, u_2} R A
        (P ⧸
          HPow.hPow (α := Ideal P) (β := ℕ)
            (RingHom.ker (F := P →+* A) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P A))) 2) //
      AlgHom.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P A)) g = AlgHom.id R A } ↔
  Nonempty
    { g : AlgHom.{u, v, u_2} R A (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker f.toRingHom) 2) //
      f.kerSquareLift.comp g = AlgHom.id R A }
Tactic: rw [iff_split_injection hf, ← nonempty_subtype, ← nonempty_subtype,
    (retractionKerCotangentToTensorEquivSection hf).nonempty_congr]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
P : Type u_2
inst_3 : CommRing P
inst_4 : Algebra R P
inst_5 : FormallySmooth R P
f : P →ₐ[R] A
g : AlgHom.{u, v, u_2} R A (P ⧸ HPow.hPow (α := Ideal P) (β := ℕ) (RingHom.ker f.toRingHom) 2)
h : f.kerSquareLift.comp g = AlgHom.id R A
⊢ FormallySmooth R A
have refine : ∀ (x : A), ∃ (a : P), (f : (a : P) → A) a = x
Tactic: refine (iff_split_surjection f fun x ↦ ?_).mpr ⟨g, h⟩
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
H :
  ∀ ⦃B : Type (max u v)⦄ [inst_3 : CommRing B] [inst_4 : Algebra R B] (I : Ideal B),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Surjective (α := A →ₐ[R] B) (β := A →ₐ[R] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
P : Generators R A A := Generators.self R A
f : P.Ring →ₐ[R] A := IsScalarTower.toAlgHom R P.Ring A
⊢ FormallySmooth R A
have rw : ∃ (g : A →ₐ[R] P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2),
  f.kerSquareLift.comp g = AlgHom.id R A
Tactic: rw [iff_split_surjection f P.algebraMap_surjective]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
H :
  ∀ ⦃B : Type (max u v)⦄ [inst_3 : CommRing B] [inst_4 : Algebra R B] (I : Ideal B),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Surjective (α := A →ₐ[R] B) (β := A →ₐ[R] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
P : Generators R A A := Generators.self R A
f : P.Ring →ₐ[R] A := IsScalarTower.toAlgHom R P.Ring A
⊢ ∃ (g : A →ₐ[R] P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2),
    f.kerSquareLift.comp g = AlgHom.id R A
have surj : Function.Surjective (α := P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2) (β := A)
  (⇑f.kerSquareLift : (a : P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) → A)
Tactic: have surj : Function.Surjective f.kerSquareLift :=
    Ideal.Quotient.lift_surjective_of_surjective _ _ P.algebraMap_surjective
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
H :
  ∀ ⦃B : Type (max u v)⦄ [inst_3 : CommRing B] [inst_4 : Algebra R B] (I : Ideal B),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Surjective (α := A →ₐ[R] B) (β := A →ₐ[R] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
P : Generators R A A := Generators.self R A
f : P.Ring →ₐ[R] A := IsScalarTower.toAlgHom R P.Ring A
surj :
  Function.Surjective (α := P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2) (β := A)
    (⇑f.kerSquareLift : (a : P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) → A)
⊢ HPow.hPow (α := Ideal (P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2)) (β := ℕ)
      (RingHom.ker f.kerSquareLift.toRingHom) 2 =
    ⊥
have rw : HPow.hPow (α := Ideal (P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2)) (β := ℕ)
    (Ideal.cotangentIdeal (RingHom.ker f.toRingHom)) 2 =
  ⊥
Tactic: rw [AlgHom.ker_kerSquareLift, Ideal.cotangentIdeal_square]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
H :
  ∀ ⦃B : Type (max u v)⦄ [inst_3 : CommRing B] [inst_4 : Algebra R B] (I : Ideal B),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Surjective (α := A →ₐ[R] B) (β := A →ₐ[R] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
P : Generators R A A := Generators.self R A
f : P.Ring →ₐ[R] A := IsScalarTower.toAlgHom R P.Ring A
surj :
  Function.Surjective (α := P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2) (β := A)
    (⇑f.kerSquareLift : (a : P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) → A)
rw :
  HPow.hPow (α := Ideal (P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2)) (β := ℕ)
      (Ideal.cotangentIdeal (RingHom.ker f.toRingHom)) 2 =
    ⊥
⊢ HPow.hPow (α := Ideal (P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2)) (β := ℕ)
      (RingHom.ker f.kerSquareLift.toRingHom) 2 =
    ⊥
have rw₁ : Eq (α := Ideal (P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2)) ⊥ ⊥
Tactic: rw [AlgHom.ker_kerSquareLift, Ideal.cotangentIdeal_square]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (hypothesis)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
H :
  ∀ ⦃B : Type (max u v)⦄ [inst_3 : CommRing B] [inst_4 : Algebra R B] (I : Ideal B),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Surjective (α := A →ₐ[R] B) (β := A →ₐ[R] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
P : Generators R A A := Generators.self R A
f : P.Ring →ₐ[R] A := IsScalarTower.toAlgHom R P.Ring A
surj :
  Function.Surjective (α := P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2) (β := A)
    (⇑f.kerSquareLift : (a : P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) → A)
⊢ ∃ (g : A →ₐ[R] P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2),
    f.kerSquareLift.comp g = AlgHom.id R A
have sqz : HPow.hPow (α := Ideal (P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2)) (β := ℕ)
    (RingHom.ker f.kerSquareLift.toRingHom) 2 =
  ⊥
Tactic: have sqz : RingHom.ker f.kerSquareLift.toRingHom ^ 2 = ⊥ := by
    rw [AlgHom.ker_kerSquareLift, Ideal.cotangentIdeal_square]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
H :
  ∀ ⦃B : Type (max u v)⦄ [inst_3 : CommRing B] [inst_4 : Algebra R B] (I : Ideal B),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Surjective (α := A →ₐ[R] B) (β := A →ₐ[R] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
P : Generators R A A := Generators.self R A
f : P.Ring →ₐ[R] A := IsScalarTower.toAlgHom R P.Ring A
surj :
  Function.Surjective (α := P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2) (β := A)
    (⇑f.kerSquareLift : (a : P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) → A)
sqz :
  HPow.hPow (α := Ideal (P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f) 2)) (β := ℕ)
      (RingHom.ker f.kerSquareLift) 2 =
    ⊥
⊢ ∃ (g : A →ₐ[R] P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2),
    f.kerSquareLift.comp g = AlgHom.id R A
have obtain : ∀ (g : A →ₐ[R] P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f) 2)
  (hg :
    AlgHom.comp (Ideal.Quotient.mkₐ R (RingHom.ker f.kerSquareLift)) g =
      (↑(Ideal.quotientKerAlgEquivOfSurjective surj).symm :
        A →ₐ[R] (P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) ⧸ RingHom.ker f.kerSquareLift)),
  ∃ (g : A →ₐ[R] P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2),
    f.kerSquareLift.comp g = AlgHom.id R A
Tactic: obtain ⟨g, hg⟩ := H _ sqz (Ideal.quotientKerAlgEquivOfSurjective surj).symm.toAlgHom
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u
A : Type v
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
H :
  ∀ ⦃B : Type (max u v)⦄ [inst_3 : CommRing B] [inst_4 : Algebra R B] (I : Ideal B),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      Function.Surjective (α := A →ₐ[R] B) (β := A →ₐ[R] B ⧸ I) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
P : Generators R A A := Generators.self R A
f : P.Ring →ₐ[R] A := IsScalarTower.toAlgHom R P.Ring A
surj :
  Function.Surjective (α := P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2) (β := A)
    (⇑f.kerSquareLift : (a : P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) → A)
sqz :
  HPow.hPow (α := Ideal (P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f) 2)) (β := ℕ)
      (RingHom.ker f.kerSquareLift) 2 =
    ⊥
g : A →ₐ[R] P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f) 2
hg :
  AlgHom.comp (Ideal.Quotient.mkₐ R (RingHom.ker f.kerSquareLift)) g =
    (↑(Ideal.quotientKerAlgEquivOfSurjective surj).symm :
      A →ₐ[R] (P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) ⧸ RingHom.ker f.kerSquareLift)
⊢ ∃ (g : A →ₐ[R] P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2),
    f.kerSquareLift.comp g = AlgHom.id R A
have refine : ∀ (x : A),
  Eq.{v + 1} (α := A)
    ((f.kerSquareLift.kerLift :
          (a : (P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) ⧸ RingHom.ker f.kerSquareLift.toRingHom) → A)
        (((↑(Ideal.quotientKerAlgEquivOfSurjective surj).symm :
                A →ₐ[R] (P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) ⧸ RingHom.ker f.kerSquareLift) :
              (a : A) → (P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) ⧸ RingHom.ker f.kerSquareLift)
            x :
          HasQuotient.Quotient (P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2) (B :=
            Ideal (P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2))
            (RingHom.ker f.kerSquareLift)) :
      A)
    ((AlgHom.id R A : (a : A) → A) x : A)
Tactic: refine ⟨g, AlgHom.ext fun x ↦ congr(f.kerSquareLift.kerLift ($hg x)).trans ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Basic (goal)
Goal:
R : Type u_4
inst : CommRing R
A : Type u_5
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type u_6
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FormallySmooth R A
inst_8 : FormallySmooth A B
⊢ FormallySmooth R B
have refine : ∀ (C : Type (max u_4 u_6)) (x : CommRing C) (x_1 : Algebra R C) (I : Ideal C) (hI : HPow.hPow (β := ℕ) I 2 = ⊥)
  (f : B →ₐ[R] C ⧸ I), ∃ (a : B →ₐ[R] C), AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f
Tactic: refine .of_comp_surjective fun C _ _ I hI f ↦ ?_