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
B : Type u_1
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FormallySmooth R A
I : Ideal B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : AlgHom.{u, v, u_1} R A (B ⧸ I)
P : Generators R A A := Generators.self R A
hP :
  Function.Injective (α := P.toExtension.Cotangent) (β := P.toExtension.CotangentSpace)
    (⇑P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.CotangentSpace)
l_1 : P.toExtension.CotangentSpace →ₗ[A] P.toExtension.Cotangent
hl : l_1 ∘ₗ P.toExtension.cotangentComplex = LinearMap.id
g :
  A →ₐ[R]
    P.Ring ⧸
      HPow.hPow (α := Ideal P.Ring) (β := ℕ)
        (RingHom.ker (F := P.Ring →+* A) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P.Ring A))) 2
hg : AlgHom.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P.Ring A)) g = AlgHom.id R A
σ : (b : B ⧸ I) → B := Function.surjInv (f := (⇑(algebraMap B (B ⧸ I)) : (a : B) → B ⧸ I)) ⋯
H :
  ∀ (x : P.Ring),
    Eq (α := B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((aeval (σ ∘ (⇑f : (a : A) → B ⧸ I)) : (a : MvPolynomial A R) → B) x) :
        B ⧸ I)
      ((f : (a : A) → B ⧸ I) ((algebraMap P.Ring A : (a : P.Ring) → A) x) : B ⧸ I)
l : P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker (F := P.Ring →+* A) (algebraMap P.Ring A)) 2 →ₐ[R] B :=
  Ideal.Quotient.liftₐ
    (HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker (F := P.Ring →+* A) (algebraMap P.Ring A)) 2)
    (aeval (σ ∘ (⇑f : (a : A) → B ⧸ I))) ⋯
this : f.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P.Ring A)) = AlgHom.comp (Ideal.Quotient.mkₐ R I) l
⊢ AlgHom.comp (Ideal.Quotient.mkₐ R I) (l.comp g) = f
have rw : AlgHom.comp (AlgHom.comp (Ideal.Quotient.mkₐ R I) l) g = f
Tactic: rw [← AlgHom.comp_assoc, ← this, AlgHom.comp_assoc, hg, AlgHom.comp_id]
-- 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
inst_5 : FormallySmooth R A
I : Ideal B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : AlgHom.{u, v, u_1} R A (B ⧸ I)
P : Generators R A A := Generators.self R A
hP :
  Function.Injective (α := P.toExtension.Cotangent) (β := P.toExtension.CotangentSpace)
    (⇑P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.CotangentSpace)
l_1 : P.toExtension.CotangentSpace →ₗ[A] P.toExtension.Cotangent
hl : l_1 ∘ₗ P.toExtension.cotangentComplex = LinearMap.id
g :
  A →ₐ[R]
    P.Ring ⧸
      HPow.hPow (α := Ideal P.Ring) (β := ℕ)
        (RingHom.ker (F := P.Ring →+* A) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P.Ring A))) 2
hg : AlgHom.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P.Ring A)) g = AlgHom.id R A
σ : (b : B ⧸ I) → B := Function.surjInv (f := (⇑(algebraMap B (B ⧸ I)) : (a : B) → B ⧸ I)) ⋯
H :
  ∀ (x : P.Ring),
    Eq (α := B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((aeval (σ ∘ (⇑f : (a : A) → B ⧸ I)) : (a : MvPolynomial A R) → B) x) :
        B ⧸ I)
      ((f : (a : A) → B ⧸ I) ((algebraMap P.Ring A : (a : P.Ring) → A) x) : B ⧸ I)
l : P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker (F := P.Ring →+* A) (algebraMap P.Ring A)) 2 →ₐ[R] B :=
  Ideal.Quotient.liftₐ
    (HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker (F := P.Ring →+* A) (algebraMap P.Ring A)) 2)
    (aeval (σ ∘ (⇑f : (a : A) → B ⧸ I))) ⋯
this : f.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P.Ring A)) = AlgHom.comp (Ideal.Quotient.mkₐ R I) l
rw : AlgHom.comp (AlgHom.comp (Ideal.Quotient.mkₐ R I) l) g = f
⊢ AlgHom.comp (Ideal.Quotient.mkₐ R I) (l.comp g) = f
have rw₁ : AlgHom.comp (f.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P.Ring A))) g = f
Tactic: rw [← AlgHom.comp_assoc, ← this, AlgHom.comp_assoc, hg, AlgHom.comp_id]
-- 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
inst_5 : FormallySmooth R A
I : Ideal B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : AlgHom.{u, v, u_1} R A (B ⧸ I)
P : Generators R A A := Generators.self R A
hP :
  Function.Injective (α := P.toExtension.Cotangent) (β := P.toExtension.CotangentSpace)
    (⇑P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.CotangentSpace)
l_1 : P.toExtension.CotangentSpace →ₗ[A] P.toExtension.Cotangent
hl : l_1 ∘ₗ P.toExtension.cotangentComplex = LinearMap.id
g :
  A →ₐ[R]
    P.Ring ⧸
      HPow.hPow (α := Ideal P.Ring) (β := ℕ)
        (RingHom.ker (F := P.Ring →+* A) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P.Ring A))) 2
hg : AlgHom.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P.Ring A)) g = AlgHom.id R A
σ : (b : B ⧸ I) → B := Function.surjInv (f := (⇑(algebraMap B (B ⧸ I)) : (a : B) → B ⧸ I)) ⋯
H :
  ∀ (x : P.Ring),
    Eq (α := B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((aeval (σ ∘ (⇑f : (a : A) → B ⧸ I)) : (a : MvPolynomial A R) → B) x) :
        B ⧸ I)
      ((f : (a : A) → B ⧸ I) ((algebraMap P.Ring A : (a : P.Ring) → A) x) : B ⧸ I)
l : P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker (F := P.Ring →+* A) (algebraMap P.Ring A)) 2 →ₐ[R] B :=
  Ideal.Quotient.liftₐ
    (HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker (F := P.Ring →+* A) (algebraMap P.Ring A)) 2)
    (aeval (σ ∘ (⇑f : (a : A) → B ⧸ I))) ⋯
this : f.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P.Ring A)) = AlgHom.comp (Ideal.Quotient.mkₐ R I) l
rw : AlgHom.comp (AlgHom.comp (Ideal.Quotient.mkₐ R I) l) g = f
rw₁ : AlgHom.comp (f.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P.Ring A))) g = f
⊢ AlgHom.comp (Ideal.Quotient.mkₐ R I) (l.comp g) = f
have rw₂ : f.comp (AlgHom.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P.Ring A)) g) = f
Tactic: rw [← AlgHom.comp_assoc, ← this, AlgHom.comp_assoc, hg, AlgHom.comp_id]
-- 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
inst_5 : FormallySmooth R A
I : Ideal B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : AlgHom.{u, v, u_1} R A (B ⧸ I)
P : Generators R A A := Generators.self R A
hP :
  Function.Injective (α := P.toExtension.Cotangent) (β := P.toExtension.CotangentSpace)
    (⇑P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.CotangentSpace)
l_1 : P.toExtension.CotangentSpace →ₗ[A] P.toExtension.Cotangent
hl : l_1 ∘ₗ P.toExtension.cotangentComplex = LinearMap.id
g :
  A →ₐ[R]
    P.Ring ⧸
      HPow.hPow (α := Ideal P.Ring) (β := ℕ)
        (RingHom.ker (F := P.Ring →+* A) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P.Ring A))) 2
hg : AlgHom.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P.Ring A)) g = AlgHom.id R A
σ : (b : B ⧸ I) → B := Function.surjInv (f := (⇑(algebraMap B (B ⧸ I)) : (a : B) → B ⧸ I)) ⋯
H :
  ∀ (x : P.Ring),
    Eq (α := B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((aeval (σ ∘ (⇑f : (a : A) → B ⧸ I)) : (a : MvPolynomial A R) → B) x) :
        B ⧸ I)
      ((f : (a : A) → B ⧸ I) ((algebraMap P.Ring A : (a : P.Ring) → A) x) : B ⧸ I)
l : P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker (F := P.Ring →+* A) (algebraMap P.Ring A)) 2 →ₐ[R] B :=
  Ideal.Quotient.liftₐ
    (HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker (F := P.Ring →+* A) (algebraMap P.Ring A)) 2)
    (aeval (σ ∘ (⇑f : (a : A) → B ⧸ I))) ⋯
this : f.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P.Ring A)) = AlgHom.comp (Ideal.Quotient.mkₐ R I) l
rw : AlgHom.comp (AlgHom.comp (Ideal.Quotient.mkₐ R I) l) g = f
rw₁ : AlgHom.comp (f.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P.Ring A))) g = f
rw₂ : f.comp (AlgHom.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P.Ring A)) g) = f
⊢ AlgHom.comp (Ideal.Quotient.mkₐ R I) (l.comp g) = f
have rw₃ : f.comp (AlgHom.id R A) = f
Tactic: rw [← AlgHom.comp_assoc, ← this, AlgHom.comp_assoc, hg, AlgHom.comp_id]
-- 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
inst_5 : FormallySmooth R A
I : Ideal B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
f : AlgHom.{u, v, u_1} R A (B ⧸ I)
P : Generators R A A := Generators.self R A
hP :
  Function.Injective (α := P.toExtension.Cotangent) (β := P.toExtension.CotangentSpace)
    (⇑P.toExtension.cotangentComplex : (a : P.toExtension.Cotangent) → P.toExtension.CotangentSpace)
l_1 : P.toExtension.CotangentSpace →ₗ[A] P.toExtension.Cotangent
hl : l_1 ∘ₗ P.toExtension.cotangentComplex = LinearMap.id
g :
  A →ₐ[R]
    P.Ring ⧸
      HPow.hPow (α := Ideal P.Ring) (β := ℕ)
        (RingHom.ker (F := P.Ring →+* A) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P.Ring A))) 2
hg : AlgHom.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P.Ring A)) g = AlgHom.id R A
σ : (b : B ⧸ I) → B := Function.surjInv (f := (⇑(algebraMap B (B ⧸ I)) : (a : B) → B ⧸ I)) ⋯
H :
  ∀ (x : P.Ring),
    Eq (α := B ⧸ I)
      ((Ideal.Quotient.mk I : (a : B) → B ⧸ I) ((aeval (σ ∘ (⇑f : (a : A) → B ⧸ I)) : (a : MvPolynomial A R) → B) x) :
        B ⧸ I)
      ((f : (a : A) → B ⧸ I) ((algebraMap P.Ring A : (a : P.Ring) → A) x) : B ⧸ I)
l : P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker (F := P.Ring →+* A) (algebraMap P.Ring A)) 2 →ₐ[R] B :=
  Ideal.Quotient.liftₐ
    (HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker (F := P.Ring →+* A) (algebraMap P.Ring A)) 2)
    (aeval (σ ∘ (⇑f : (a : A) → B ⧸ I))) ⋯
this : f.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P.Ring A)) = AlgHom.comp (Ideal.Quotient.mkₐ R I) l
rw : AlgHom.comp (AlgHom.comp (Ideal.Quotient.mkₐ R I) l) g = f
rw₁ : AlgHom.comp (f.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P.Ring A))) g = f
rw₂ : f.comp (AlgHom.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P.Ring A)) g) = f
rw₃ : f.comp (AlgHom.id R A) = f
⊢ AlgHom.comp (Ideal.Quotient.mkₐ R I) (l.comp g) = f
have rw₄ : f = f
Tactic: rw [← AlgHom.comp_assoc, ← this, AlgHom.comp_assoc, hg, AlgHom.comp_id]
-- 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_1 : 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_1
inst_8 : Algebra R P_1
σ : Type u_4
P : Generators R (MvPolynomial σ R) σ := Generators.mvPolynomial R σ
⊢ FormallySmooth R (MvPolynomial σ R)
have this : Subsingleton ↥P.toExtension.ker
Tactic: have : Subsingleton ↥P.toExtension.ker :=
    Submodule.subsingleton_iff_eq_bot.mpr Generators.ker_mvPolynomial
-- 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_1 : 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_1
inst_8 : Algebra R P_1
σ : Type u_4
P : Generators R (MvPolynomial σ R) σ := Generators.mvPolynomial R σ
this : Subsingleton ↥P.toExtension.ker
⊢ FormallySmooth R (MvPolynomial σ R)
have this₁ : Subsingleton P.toExtension.Cotangent
Tactic: have : Subsingleton P.toExtension.Cotangent := Cotangent.mk_surjective.subsingleton
-- 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_1 : 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_1
inst_8 : Algebra R P_1
σ : Type u_4
P : Generators R (MvPolynomial σ R) σ := Generators.mvPolynomial R σ
this_1 : Subsingleton ↥P.toExtension.ker
this : Subsingleton P.toExtension.Cotangent
⊢ FormallySmooth R (MvPolynomial σ R)
have this₁ : Subsingleton P.toExtension.H1Cotangent
Tactic: have := P.toExtension.h1Cotangentι_injective.subsingleton
-- 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
inst_5 : FormallySmooth R A
I : Ideal B
hI : IsNilpotent I
g : AlgHom.{u, v, u_1} R A (B ⧸ I)
⊢ ∃ (f : A →ₐ[R] B), AlgHom.comp (Ideal.Quotient.mkₐ R I) f = g
have revert : ∀ (g : AlgHom.{u, v, u_1} R A (B ⧸ I)), ∃ (f : A →ₐ[R] B), AlgHom.comp (Ideal.Quotient.mkₐ R I) f = g
Tactic: revert g
Cleared hypotheses: g
-- 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
inst_5 : FormallySmooth R A
I : Ideal B
hI : IsNilpotent I
⊢ ∀ (g : AlgHom.{u, v, u_1} R A (B ⧸ I)), ∃ (f : A →ₐ[R] B), AlgHom.comp (Ideal.Quotient.mkₐ R I) f = g
have change : Function.Surjective (α := A →ₐ[R] B) (β := AlgHom.{u, v, u_1} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
Tactic: change Function.Surjective (Ideal.Quotient.mkₐ R I).comp
-- 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
inst_5 : FormallySmooth R A
I : Ideal B
hI : IsNilpotent I
⊢ Function.Surjective (α := A →ₐ[R] B) (β := AlgHom.{u, v, u_1} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
have revert : ∀ [inst_6 : Algebra R B],
  Function.Surjective (α := A →ₐ[R] B) (β := AlgHom.{u, v, u_1} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
Tactic: revert ‹Algebra R B›
Cleared hypotheses: inst_4
-- 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 : FormallySmooth R A
I : Ideal B
hI : IsNilpotent I
⊢ ∀ [inst_5 : Algebra R B],
    Function.Surjective (α := A →ₐ[R] B) (β := AlgHom.{u, v, u_1} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
have h₁ : ∀ ⦃S : Type u_1⦄ [inst_5 : CommRing S] (I : Ideal S),
  HPow.hPow (β := ℕ) I 2 = ⊥ →
    ∀ [inst_6 : Algebra R S],
      Function.Surjective (α := A →ₐ[R] S) (β := AlgHom.{u, v, u_1} R A (S ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
Tactic: apply Ideal.IsNilpotent.induction_on (S := B) I hI
-- 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 : FormallySmooth R A
I : Ideal B
hI : IsNilpotent I
h₁ :
  ∀ ⦃S : Type u_1⦄ [inst_5 : CommRing S] (I : Ideal S),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      ∀ [inst_6 : Algebra R S],
        Function.Surjective (α := A →ₐ[R] S) (β := AlgHom.{u, v, u_1} R A (S ⧸ I))
          (AlgHom.comp (Ideal.Quotient.mkₐ R I))
⊢ ∀ [inst_5 : Algebra R B],
    Function.Surjective (α := A →ₐ[R] B) (β := AlgHom.{u, v, u_1} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
have h₂ : ∀ ⦃S : Type u_1⦄ [inst_5 : CommRing S] (I J : Ideal S),
  I ≤ J →
    (∀ [inst_6 : Algebra R S],
        Function.Surjective (α := A →ₐ[R] S) (β := AlgHom.{u, v, u_1} R A (S ⧸ I))
          (AlgHom.comp (Ideal.Quotient.mkₐ R I))) →
      (∀ [inst_6 : Algebra.{u, u_1} R (S ⧸ I)],
          Function.Surjective (α := AlgHom.{u, v, u_1} R A (S ⧸ I)) (β :=
            AlgHom.{u, v, u_1} R A
              (HasQuotient.Quotient (S ⧸ I) (B := Ideal (S ⧸ I))
                (Ideal.map (F := S →+* S ⧸ I) (Ideal.Quotient.mk I) J)))
            (AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := S →+* S ⧸ I) (Ideal.Quotient.mk I) J)))) →
        ∀ [inst_6 : Algebra R S],
          Function.Surjective (α := A →ₐ[R] S) (β := AlgHom.{u, v, u_1} R A (S ⧸ J))
            (AlgHom.comp (Ideal.Quotient.mkₐ R J))
Tactic: apply Ideal.IsNilpotent.induction_on (S := B) I hI
-- 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_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' := ⋯ }
⊢ ∃ (a : A →ₐ[R] B), AlgHom.comp (Ideal.Quotient.mkₐ R J) a = g
have h₃ : ∀ (g' : AlgHom.{u, v, u_1} R A (B ⧸ I))
  (e :
    AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)) g' =
      (↑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
Tactic: obtain ⟨g', e⟩ := h₂ (this.symm.toAlgHom.comp g)
-- 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_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' : AlgHom.{u, v, u_1} R A (B ⧸ I)
e :
  AlgHom.comp (Ideal.Quotient.mkₐ R (Ideal.map (F := B →+* B ⧸ I) (Ideal.Quotient.mk I) J)) g' =
    (↑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 h₃ : ∀ (g' : A →ₐ[R] B)
  (e :
    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.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
Tactic: obtain ⟨g', rfl⟩ := h₁ g'
Cleared hypotheses: g', e
-- 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 :
  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.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')) =
  (↑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)
Tactic: replace e := congr_arg this.toAlgHom.comp e
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_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)
| (↑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)
have rw : g
Tactic: rw [← AlgHom.comp_assoc, AlgEquiv.comp_symm, AlgHom.id_comp]