awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
B_1 : Type u_1
inst_3 : CommRing B_1
inst_4 : FormallySmooth R A
I_1 : Ideal B_1
hI : IsNilpotent I_1
B : Type u_1
inst_5 : CommRing B
I J : Ideal B
hIJ : I ≤ J
h₁ :
  ∀ [inst_7 : Algebra R B],
    Function.Surjective (α := A →ₐ[R] B) (β := AlgHom.{u, v, u_1} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
h₂ :
  ∀ [inst_7 : Algebra.{u, u_1} R (B ⧸ I)],
    Function.Surjective (α := AlgHom.{u, v, u_1} R A (B ⧸ I)) (β :=
      AlgHom.{u, v, u_1} R A
        (HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
      (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)))
inst_6 : Algebra R B
g : AlgHom.{u, v, u_1} R A (B ⧸ J)
this : HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J) ≃ₐ[R]
  B ⧸ J :=
  let __src :
    HasQuotient.Quotient (B ⧸ I) (B := Ideal (B ⧸ I)) (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J) ≃+*
      B ⧸ J :=
    (DoubleQuot.quotQuotEquivQuotSup I J).trans (Ideal.quotEquivOfEq ⋯);
  { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
g' : A →ₐ[R] B
e :
  (↑this : (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J →ₐ[R] B ⧸ J).comp
      (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
        (AlgHom.comp (Ideal.Quotient.mkₐ R I) g')) =
    (↑this : (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J →ₐ[R] B ⧸ J).comp
      ((↑this.symm : B ⧸ J →ₐ[R] (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J).comp g)
⊢ ∃ (a : A →ₐ[R] B), AlgHom.comp (Ideal.Quotient.mkₐ R J) a = g
have e₁ : (↑this : (B ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J →ₐ[R] B ⧸ J).comp
    (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J))
      (AlgHom.comp (Ideal.Quotient.mkₐ R I) g')) =
  g
Tactic: conv_rhs at e =>
      rw [← AlgHom.comp_assoc, AlgEquiv.comp_symm, AlgHom.id_comp]
Cleared hypotheses: e
-- 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
B : Type u_1
inst_3 : CommRing B
inst_4 : Algebra R B
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra R C
inst_7 : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective.{u_1 + 1, u_4 + 1} (α := B) (β := C) (⇑g : (a : B) → C)
hg' : IsNilpotent (R := Ideal B) (RingHom.ker g)
x : A
⊢ Eq.{u_4 + 1} (α := C) ((g : (a : B) → C) ((liftOfSurjective f g hg hg' : (a : A) → B) x : B) : C)
    ((f : (a : A) → C) x : C)
have a : Eq.{u_1 + 1} (α := HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g))
  (((Ideal.quotientKerAlgEquivOfSurjective hg).symm : (a : C) → B ⧸ RingHom.ker g)
      ((g : (a : B) → C) ((liftOfSurjective f g hg hg' : (a : A) → B) x : B)) :
    HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g))
  (((Ideal.quotientKerAlgEquivOfSurjective hg).symm : (a : C) → B ⧸ RingHom.ker g) ((f : (a : A) → C) x) :
    HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g))
Tactic: apply (Ideal.quotientKerAlgEquivOfSurjective hg).symm.injective
-- 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
B : Type u_1
inst_3 : CommRing B
inst_4 : Algebra R B
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra R C
inst_7 : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective.{u_1 + 1, u_4 + 1} (α := B) (β := C) (⇑g : (a : B) → C)
hg' : IsNilpotent (R := Ideal B) (RingHom.ker g)
x : A
| (((Ideal.quotientKerAlgEquivOfSurjective hg).symm : (a : C) → B ⧸ RingHom.ker g) ((f : (a : A) → C) x) :
    HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g))
have rw : ((Ideal.Quotient.mk (RingHom.ker g) : (a : B) → B ⧸ RingHom.ker g)
    ((lift (RingHom.ker g) hg' ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm : C →ₐ[R] B ⧸ RingHom.ker g).comp f) :
        (a : A) → B)
      x) :
  HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g))
Tactic: rw [← AlgEquiv.coe_algHom, ← AlgHom.comp_apply,
    ← FormallySmooth.mk_lift (A := A) _ hg']
-- 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
B : Type u_1
inst_3 : CommRing B
inst_4 : Algebra R B
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra R C
inst_7 : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective.{u_1 + 1, u_4 + 1} (α := B) (β := C) (⇑g : (a : B) → C)
hg' : IsNilpotent (R := Ideal B) (RingHom.ker g)
x : A
⊢ Eq.{u_1 + 1} (α := HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g))
    (((Ideal.quotientKerAlgEquivOfSurjective hg).symm : (a : C) → B ⧸ RingHom.ker g)
        ((g : (a : B) → C) ((liftOfSurjective f g hg hg' : (a : A) → B) x : B)) :
      HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g))
    (((Ideal.quotientKerAlgEquivOfSurjective hg).symm : (a : C) → B ⧸ RingHom.ker g) ((f : (a : A) → C) x) :
      HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g))
have a : Eq.{u_1 + 1} (α := HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g))
  (((Ideal.quotientKerAlgEquivOfSurjective hg).symm : (a : C) → B ⧸ RingHom.ker g)
      ((g : (a : B) → C) ((liftOfSurjective f g hg hg' : (a : A) → B) x : B)) :
    HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g))
  ((Ideal.Quotient.mk (RingHom.ker g) : (a : B) → B ⧸ RingHom.ker g)
      ((lift (RingHom.ker g) hg'
            ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm : C →ₐ[R] B ⧸ RingHom.ker g).comp f) :
          (a : A) → B)
        x) :
    HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g))
Tactic: conv_rhs => rw [← AlgEquiv.coe_algHom, ← AlgHom.comp_apply,
    ← FormallySmooth.mk_lift (A := A) _ hg']
-- 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
B : Type u_1
inst_3 : CommRing B
inst_4 : Algebra R B
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra R C
inst_7 : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective.{u_1 + 1, u_4 + 1} (α := B) (β := C) (⇑g : (a : B) → C)
hg' : IsNilpotent (R := Ideal B) (RingHom.ker g)
x : A
⊢ Eq.{u_1 + 1} (α := HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g))
    (((Ideal.quotientKerAlgEquivOfSurjective hg).symm : (a : C) → B ⧸ RingHom.ker g)
        ((g : (a : B) → C) ((liftOfSurjective f g hg hg' : (a : A) → B) x : B)) :
      HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g))
    ((Ideal.Quotient.mk (RingHom.ker g) : (a : B) → B ⧸ RingHom.ker g)
        ((lift (RingHom.ker g) hg'
              ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm : C →ₐ[R] B ⧸ RingHom.ker g).comp f) :
            (a : A) → B)
          x) :
      HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g))
have a : Eq.{u_4 + 1} (α := C)
  ((Ideal.quotientKerAlgEquivOfSurjective hg : (a : B ⧸ RingHom.ker g) → C)
      (((Ideal.quotientKerAlgEquivOfSurjective hg).symm : (a : C) → B ⧸ RingHom.ker g)
          ((g : (a : B) → C) ((liftOfSurjective f g hg hg' : (a : A) → B) x : B)) :
        HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g)) :
    C)
  ((Ideal.quotientKerAlgEquivOfSurjective hg : (a : B ⧸ RingHom.ker g) → C)
      ((Ideal.Quotient.mk (RingHom.ker g) : (a : B) → B ⧸ RingHom.ker g)
          ((lift (RingHom.ker g) hg'
                ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm : C →ₐ[R] B ⧸ RingHom.ker g).comp f) :
              (a : A) → B)
            x) :
        HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g)) :
    C)
Tactic: apply (Ideal.quotientKerAlgEquivOfSurjective hg).injective
-- 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
B : Type u_1
inst_3 : CommRing B
inst_4 : Algebra R B
C : Type u_4
inst_5 : CommRing C
inst_6 : Algebra R C
inst_7 : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective.{u_1 + 1, u_4 + 1} (α := B) (β := C) (⇑g : (a : B) → C)
hg' : IsNilpotent (R := Ideal B) (RingHom.ker g)
x : A
⊢ Eq.{u_4 + 1} (α := C)
    ((Ideal.quotientKerAlgEquivOfSurjective hg : (a : B ⧸ RingHom.ker g) → C)
        (((Ideal.quotientKerAlgEquivOfSurjective hg).symm : (a : C) → B ⧸ RingHom.ker g)
            ((g : (a : B) → C) ((liftOfSurjective f g hg hg' : (a : A) → B) x : B)) :
          HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g)) :
      C)
    ((Ideal.quotientKerAlgEquivOfSurjective hg : (a : B ⧸ RingHom.ker g) → C)
        ((Ideal.Quotient.mk (RingHom.ker g) : (a : B) → B ⧸ RingHom.ker g)
            ((lift (RingHom.ker g) hg'
                  ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm : C →ₐ[R] B ⧸ RingHom.ker g).comp f) :
                (a : A) → B)
              x) :
          HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g)) :
      C)
have a : Eq.{u_4 + 1} (α := C) ((g : (a : B) → C) ((liftOfSurjective f g hg hg' : (a : A) → B) x : B) : C)
  ((RingHom.kerLift (↑g : B →+* C) : (a : B ⧸ RingHom.ker (↑g : B →+* C)) → C)
      ((Ideal.Quotient.mk (RingHom.ker g) : (a : B) → B ⧸ RingHom.ker g)
          ((lift (RingHom.ker g) hg'
                ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm : C →ₐ[R] B ⧸ RingHom.ker g).comp f) :
              (a : A) → B)
            x) :
        HasQuotient.Quotient B (B := Ideal B) (RingHom.ker g)) :
    C)
Tactic: rw [AlgEquiv.apply_symm_apply, Ideal.quotientKerAlgEquivOfSurjective_apply]
-- 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
B : Type u_1
P : Type u_2
C : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : CommRing C
inst_6 : Algebra R C
inst_7 : CommRing P
inst_8 : Algebra R P
P₁ : Extension.{u_4, u, v} R A
P₂ : Extension.{u_5, u, v} R A
inst_9 : FormallySmooth.{u, u_4} R P₁.Ring
⊢ HPow.hPow (β := ℕ) P₂.infinitesimal.ker 2 = ⊥
have rw : HPow.hPow (β := ℕ) P₂.ker.cotangentIdeal 2 = ⊥
Tactic: rw [ker_infinitesimal]
-- 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
B : Type u_1
P : Type u_2
C : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : CommRing C
inst_6 : Algebra R C
inst_7 : CommRing P
inst_8 : Algebra R P
P₁ : Extension.{u_4, u, v} R A
P₂ : Extension.{u_5, u, v} R A
inst_9 : FormallySmooth.{u, u_4} R P₁.Ring
lift : AlgHom.{u, u_4, u_5} R P₁.Ring P₂.infinitesimal.Ring :=
  FormallySmooth.liftOfSurjective (IsScalarTower.toAlgHom R P₁.Ring A)
    (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) ⋯ ⋯
⊢ ∀ a ∈ HPow.hPow (β := ℕ) P₁.ker 2,
    Eq.{u_5 + 1} (α := P₂.infinitesimal.Ring) ((lift : (a : P₁.Ring) → P₂.infinitesimal.Ring) a : P₂.infinitesimal.Ring)
      (0 : P₂.infinitesimal.Ring)
have change : HPow.hPow (β := ℕ) P₁.ker 2 ≤ RingHom.ker lift
Tactic: change P₁.ker ^ 2 ≤ RingHom.ker lift
-- 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
B : Type u_1
P : Type u_2
C : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : CommRing C
inst_6 : Algebra R C
inst_7 : CommRing P
inst_8 : Algebra R P
P₁ : Extension.{u_4, u, v} R A
P₂ : Extension.{u_5, u, v} R A
inst_9 : FormallySmooth.{u, u_4} R P₁.Ring
lift : AlgHom.{u, u_4, u_5} R P₁.Ring P₂.infinitesimal.Ring :=
  FormallySmooth.liftOfSurjective (IsScalarTower.toAlgHom R P₁.Ring A)
    (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) ⋯ ⋯
⊢ HPow.hPow (β := ℕ) P₁.ker 2 ≤ RingHom.ker lift
have rw : ∀ r ∈ P₁.ker, ∀ s ∈ P₁.ker, Membership.mem (γ := Ideal P₁.Ring) (RingHom.ker lift) (r * s)
Tactic: rw [pow_two, Ideal.mul_le]
-- 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
B : Type u_1
P : Type u_2
C : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : CommRing C
inst_6 : Algebra R C
inst_7 : CommRing P
inst_8 : Algebra R P
P₁ : Extension.{u_4, u, v} R A
P₂ : Extension.{u_5, u, v} R A
inst_9 : FormallySmooth.{u, u_4} R P₁.Ring
lift : AlgHom.{u, u_4, u_5} R P₁.Ring P₂.infinitesimal.Ring :=
  FormallySmooth.liftOfSurjective (IsScalarTower.toAlgHom R P₁.Ring A)
    (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) ⋯ ⋯
⊢ ∀ r ∈ P₁.ker, ∀ s ∈ P₁.ker, Membership.mem (γ := Ideal P₁.Ring) (RingHom.ker lift) (r * s)
have this : ∀ r ∈ P₁.ker,
  Membership.mem (α := P₂.infinitesimal.Ring) P₂.infinitesimal.ker
    ((lift : (a : P₁.Ring) → P₂.infinitesimal.Ring) r : P₂.infinitesimal.Ring)
Tactic: have : ∀ r ∈ P₁.ker, lift r ∈ P₂.infinitesimal.ker :=
          fun r hr ↦ (FormallySmooth.liftOfSurjective_apply _
            (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) _ _ r).trans hr
-- 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
B : Type u_1
P : Type u_2
C : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : CommRing C
inst_6 : Algebra R C
inst_7 : CommRing P
inst_8 : Algebra R P
P₁ : Extension.{u_4, u, v} R A
P₂ : Extension.{u_5, u, v} R A
inst_9 : FormallySmooth.{u, u_4} R P₁.Ring
lift : AlgHom.{u, u_4, u_5} R P₁.Ring P₂.infinitesimal.Ring :=
  FormallySmooth.liftOfSurjective (IsScalarTower.toAlgHom R P₁.Ring A)
    (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) ⋯ ⋯
this :
  ∀ r ∈ P₁.ker,
    Membership.mem (α := P₂.infinitesimal.Ring) P₂.infinitesimal.ker
      ((lift : (a : P₁.Ring) → P₂.infinitesimal.Ring) r : P₂.infinitesimal.Ring)
r : P₁.Ring
hr : r ∈ P₁.ker
s : P₁.Ring
hs : s ∈ P₁.ker
⊢ Membership.mem (γ := Ideal P₁.Ring) (RingHom.ker lift) (r * s)
have rw : HMul.hMul (α := P₂.infinitesimal.Ring) (β := P₂.infinitesimal.Ring)
    ((lift : (a : P₁.Ring) → P₂.infinitesimal.Ring) r : P₂.infinitesimal.Ring)
    ((lift : (a : P₁.Ring) → P₂.infinitesimal.Ring) s : P₂.infinitesimal.Ring) ∈
  P₂.infinitesimal.ker * P₂.infinitesimal.ker
Tactic: rw [RingHom.mem_ker, map_mul, ← Ideal.mem_bot, ← P₂.ker.cotangentIdeal_square,
          ← ker_infinitesimal, pow_two]
-- 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
B : Type u_1
P : Type u_2
C : Type u_3
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : CommRing C
inst_6 : Algebra R C
inst_7 : CommRing P
inst_8 : Algebra R P
P₁ : Extension.{u_4, u, v} R A
P₂ : Extension.{u_5, u, v} R A
inst_9 : FormallySmooth.{u, u_4} R P₁.Ring
lift : AlgHom.{u, u_4, u_5} R P₁.Ring P₂.infinitesimal.Ring :=
  FormallySmooth.liftOfSurjective (IsScalarTower.toAlgHom R P₁.Ring A)
    (IsScalarTower.toAlgHom R P₂.infinitesimal.Ring A) ⋯ ⋯
x : P₁.infinitesimal.Ring
⊢ Eq (α := A)
    ((algebraMap P₂.infinitesimal.Ring A : (a : P₂.infinitesimal.Ring) → A)
        (((AlgHom.toRingHom (Ideal.Quotient.liftₐ (HPow.hPow (β := ℕ) P₁.ker 2) lift ⋯) :
                RingHom.{u_4, u_5} (P₁.Ring ⧸ HPow.hPow (β := ℕ) P₁.ker 2) P₂.infinitesimal.Ring) :
              (a : P₁.infinitesimal.Ring) → P₂.infinitesimal.Ring)
            x :
          P₂.infinitesimal.Ring) :
      A)
    ((algebraMap A A : (a : A) → A) ((algebraMap P₁.infinitesimal.Ring A : (a : P₁.infinitesimal.Ring) → A) x : A) : A)
have obtain : ∀ (x : P₁.Ring),
  Eq (α := A)
    ((algebraMap P₂.infinitesimal.Ring A : (a : P₂.infinitesimal.Ring) → A)
        (((AlgHom.toRingHom (Ideal.Quotient.liftₐ (HPow.hPow (β := ℕ) P₁.ker 2) lift sorry) :
                RingHom.{u_4, u_5} (P₁.Ring ⧸ HPow.hPow (β := ℕ) P₁.ker 2) P₂.infinitesimal.Ring) :
              (a : P₁.infinitesimal.Ring) → P₂.infinitesimal.Ring)
            ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P₁.ker 2) : (a : P₁.Ring) → P₁.Ring ⧸ P₁.ker ^ 2) x) :
          P₂.infinitesimal.Ring) :
      A)
    ((algebraMap A A : (a : A) → A)
        ((algebraMap P₁.infinitesimal.Ring A : (a : P₁.infinitesimal.Ring) → A)
            ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P₁.ker 2) : (a : P₁.Ring) → P₁.Ring ⧸ P₁.ker ^ 2) x :
              P₁.Ring ⧸ HPow.hPow (β := ℕ) P₁.ker 2) :
          A) :
      A)
Tactic: obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
Cleared hypotheses: x
-- 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.{u_4, u, v} R A
P₂ : Extension.{u_5, u, v} R A
f : P₁.Hom P₂
inst_3 : FormallySmooth.{u, u_4} R P₁.Ring
inst_4 : FormallySmooth.{u, u_5} R P₂.Ring
⊢ (↑(equivOfFormallySmooth P₁ P₂) : P₁.H1Cotangent →ₗ[A] P₂.H1Cotangent) = map f
have h : ∀ (x : P₁.H1Cotangent),
  Eq.{u_5 + 1} (α := P₂.H1Cotangent)
    (((↑(equivOfFormallySmooth P₁ P₂) : P₁.H1Cotangent →ₗ[A] P₂.H1Cotangent) : (a : P₁.H1Cotangent) → P₂.H1Cotangent)
        x :
      P₂.H1Cotangent)
    ((map f : (a : P₁.H1Cotangent) → P₂.H1Cotangent) x : P₂.H1Cotangent)
Tactic: ext1 x
-- 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.{u_4, u, v} R A
P₂ : Extension.{u_5, u, v} R A
f : P₁.Hom P₂
inst_3 : FormallySmooth.{u, u_4} R P₁.Ring
inst_4 : FormallySmooth.{u, u_5} R P₂.Ring
x : P₁.H1Cotangent
⊢ Eq.{u_5 + 1} (α := P₂.H1Cotangent)
    (((↑(equivOfFormallySmooth P₁ P₂) : P₁.H1Cotangent →ₗ[A] P₂.H1Cotangent) : (a : P₁.H1Cotangent) → P₂.H1Cotangent)
        x :
      P₂.H1Cotangent)
    ((map f : (a : P₁.H1Cotangent) → P₂.H1Cotangent) x : P₂.H1Cotangent)
have h : Eq.{u_5 + 1} (α := P₂.infinitesimal.H1Cotangent)
  (((↑(LinearEquiv.trans (re₁₂ := sorry) (re₂₁ := sorry) (LinearEquiv.ofBijective (map P₁.toInfinitesimal) sorry)
              (equiv (P₁.homInfinitesimal P₂) (P₂.homInfinitesimal P₁))) :
          P₁.H1Cotangent →ₗ[A] P₂.infinitesimal.H1Cotangent) :
        (a : P₁.H1Cotangent) → P₂.infinitesimal.H1Cotangent)
      x :
    P₂.infinitesimal.H1Cotangent)
  ((LinearEquiv.ofBijective (map P₂.toInfinitesimal) sorry : (a : P₂.H1Cotangent) → P₂.infinitesimal.H1Cotangent)
      ((map f : (a : P₁.H1Cotangent) → P₂.H1Cotangent) x) :
    P₂.infinitesimal.H1Cotangent)
Tactic: refine (LinearEquiv.symm_apply_eq _).mpr ?_
-- 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.{u_4, u, v} R A
P₂ : Extension.{u_5, u, v} R A
f : P₁.Hom P₂
inst_3 : FormallySmooth.{u, u_4} R P₁.Ring
inst_4 : FormallySmooth.{u, u_5} R P₂.Ring
x : P₁.H1Cotangent
⊢ Eq.{u_5 + 1} (α := P₂.H1Cotangent)
    ((equivOfFormallySmooth P₁ P₂ : (a : P₁.H1Cotangent) → P₂.H1Cotangent) x : P₂.H1Cotangent)
    ((map f : (a : P₁.H1Cotangent) → P₂.H1Cotangent) x : P₂.H1Cotangent)
have rw : Eq.{u_5 + 1} (α := P₂.H1Cotangent)
  ((equivOfFormallySmooth P₁ P₂ : (a : P₁.H1Cotangent) → P₂.H1Cotangent) x : P₂.H1Cotangent)
  (((↑(equivOfFormallySmooth P₁ P₂) : P₁.H1Cotangent →ₗ[A] P₂.H1Cotangent) : (a : P₁.H1Cotangent) → P₂.H1Cotangent) x :
    P₂.H1Cotangent)
Tactic: rw [← equivOfFormallySmooth_toLinearMap, LinearEquiv.coe_coe]
-- 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.{u_4, u, v} R A
P₂ : Extension.{u_5, u, v} R A
f : P₁.Hom P₂
inst_3 : FormallySmooth.{u, u_4} R P₁.Ring
inst_4 : FormallySmooth.{u, u_5} R P₂.Ring
x : P₁.H1Cotangent
rw :
  Eq.{u_5 + 1} (α := P₂.H1Cotangent)
    ((equivOfFormallySmooth P₁ P₂ : (a : P₁.H1Cotangent) → P₂.H1Cotangent) x : P₂.H1Cotangent)
    (((↑(equivOfFormallySmooth P₁ P₂) : P₁.H1Cotangent →ₗ[A] P₂.H1Cotangent) : (a : P₁.H1Cotangent) → P₂.H1Cotangent)
        x :
      P₂.H1Cotangent)
⊢ Eq.{u_5 + 1} (α := P₂.H1Cotangent)
    ((equivOfFormallySmooth P₁ P₂ : (a : P₁.H1Cotangent) → P₂.H1Cotangent) x : P₂.H1Cotangent)
    ((map f : (a : P₁.H1Cotangent) → P₂.H1Cotangent) x : P₂.H1Cotangent)
have rw₁ : Eq.{u_5 + 1} (α := P₂.H1Cotangent)
  ((equivOfFormallySmooth P₁ P₂ : (a : P₁.H1Cotangent) → P₂.H1Cotangent) x : P₂.H1Cotangent)
  ((equivOfFormallySmooth P₁ P₂ : (a : P₁.H1Cotangent) → P₂.H1Cotangent) x : P₂.H1Cotangent)
Tactic: rw [← equivOfFormallySmooth_toLinearMap, LinearEquiv.coe_coe]
-- 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.{u_4, u, v} R A
inst_3 : FormallySmooth.{u, u_4} R P.Ring
⊢ Function.Injective (α := P.Cotangent) (β := P.CotangentSpace)
      (⇑P.cotangentComplex : (a : P.Cotangent) → P.CotangentSpace) ↔
    Subsingleton (H1Cotangent R A)
have rw : Subsingleton.{u_4 + 1} P.H1Cotangent ↔ Subsingleton (H1Cotangent R A)
Tactic: rw [← Algebra.Extension.subsingleton_h1Cotangent,
    P.equivH1CotangentOfFormallySmooth.subsingleton_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 : Extension.{u_4, u, v} R A
inst_3 : FormallySmooth.{u, u_4} R P.Ring
rw : Subsingleton.{u_4 + 1} P.H1Cotangent ↔ Subsingleton (H1Cotangent R A)
⊢ Function.Injective (α := P.Cotangent) (β := P.CotangentSpace)
      (⇑P.cotangentComplex : (a : P.Cotangent) → P.CotangentSpace) ↔
    Subsingleton (H1Cotangent R A)
have rw₁ : Subsingleton (H1Cotangent R A) ↔ Subsingleton (H1Cotangent R A)
Tactic: rw [← Algebra.Extension.subsingleton_h1Cotangent,
    P.equivH1CotangentOfFormallySmooth.subsingleton_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
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)
⊢ FormallySmooth R A ↔
    ∃ (l : A ⊗[P] Ω[P⁄R] →ₗ[P] Ideal.Cotangent (RingHom.ker (F := P →+* A) (algebraMap P A))),
      l ∘ₗ kerCotangentToTensor R P A = LinearMap.id
have rw : (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
Tactic: rw [formallySmooth_iff, and_comm,
    Module.Projective.iff_split_of_projective (KaehlerDifferential.mapBaseChange R P A)
      (mapBaseChange_surjective R P A hf), ← kerCotangentToTensor_injective_iff hf]