awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Smooth.Basic
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))) ⋯
i : A
change :
  Eq (α := B ⧸ I) ((f : (a : A) → B ⧸ I) ((algebraMap P.Ring A : (a : P.Ring) → A) (X i)) : B ⧸ I)
    ((algebraMap B (B ⧸ I) : (a : B) → B ⧸ I)
        ((aeval (σ ∘ (⇑f : (a : A) → B ⧸ I)) : (a : MvPolynomial A R) → B) (X i)) :
      B ⧸ I)
⊢ Eq.{u_1 + 1} (α := B ⧸ I)
    ((AlgHom.comp (f.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P.Ring A)))
            (Ideal.Quotient.mkₐ R
              (HPow.hPow (α := Ideal P.Ring) (β := ℕ)
                (RingHom.ker (F := P.Ring →+* A) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P.Ring A))) 2)) :
          (a : MvPolynomial A R) → B ⧸ I)
        (X i) :
      B ⧸ I)
    ((AlgHom.comp (AlgHom.comp (Ideal.Quotient.mkₐ R I) l)
            (Ideal.Quotient.mkₐ R
              (HPow.hPow (α := Ideal P.Ring) (β := ℕ)
                (RingHom.ker (F := P.Ring →+* A) (AlgHom.toRingHom (IsScalarTower.toAlgHom R P.Ring A))) 2)) :
          (a : MvPolynomial A R) → B ⧸ I)
        (X i) :
      B ⧸ I)

Tactic:
change f (algebraMap P.Ring A (.X i)) = algebraMap _ _ (MvPolynomial.aeval (σ ∘ f) (.X i))

Premises used: Algebra.Generators.Ring, MvPolynomial.aeval, Algebra.algebraMap, MvPolynomial.X, Function.comp, DFunLike.coe
-- Module: Mathlib.RingTheory.Smooth.Basic
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))) ⋯
i : A
⊢ Eq (α := B ⧸ I) ((f : (a : A) → B ⧸ I) ((algebraMap P.Ring A : (a : P.Ring) → A) (X i)) : B ⧸ I)
    ((algebraMap B (B ⧸ I) : (a : B) → B ⧸ I)
        ((aeval (σ ∘ (⇑f : (a : A) → B ⧸ I)) : (a : MvPolynomial A R) → B) (X i)) :
      B ⧸ I)

Tactic:
simpa using (Function.surjInv_eq _ _).symm

Premises used: Function.surjInv_eq, Eq.symm
-- Module: Mathlib.RingTheory.Smooth.Basic
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))) ⋯
⊢ f.comp (AlgHom.kerSquareLift (IsScalarTower.toAlgHom R P.Ring A)) = AlgHom.comp (Ideal.Quotient.mkₐ R I) l

Tactic:
have : f.comp (IsScalarTower.toAlgHom R P.Ring A).kerSquareLift =
      (Ideal.Quotient.mkₐ R _).comp l := by
    refine Ideal.Quotient.algHom_ext _ (MvPolynomial.algHom_ext fun i ↦ ?_)
    change f (algebraMap P.Ring A (.X i)) = algebraMap _ _ (MvPolynomial.aeval (σ ∘ f) (.X i))
    simpa using (Function.surjInv_eq _ _).symm
-- Module: Mathlib.RingTheory.Smooth.Basic
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
rw₄ rw₅ : f = f
⊢ AlgHom.comp (Ideal.Quotient.mkₐ R I) (l.comp g) = f

Tactic:
rw [← AlgHom.comp_assoc, ← this, AlgHom.comp_assoc, hg, AlgHom.comp_id]

Premises used: AlgHom.comp_assoc, AlgHom.comp_id
-- Module: Mathlib.RingTheory.Smooth.Basic
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
⊢ ∃ (a : A →ₐ[R] B), AlgHom.comp (Ideal.Quotient.mkₐ R I) a = f

Tactic:
exact ⟨l.comp g, by rw [← AlgHom.comp_assoc, ← this, AlgHom.comp_assoc, hg, AlgHom.comp_id]⟩
-- Module: Mathlib.RingTheory.Smooth.Basic
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 σ
⊢ Subsingleton ↥P.toExtension.ker

Tactic:
have : Subsingleton ↥P.toExtension.ker :=
    Submodule.subsingleton_iff_eq_bot.mpr Generators.ker_mvPolynomial
-- Module: Mathlib.RingTheory.Smooth.Basic
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
⊢ Subsingleton P.toExtension.Cotangent

Tactic:
have : Subsingleton P.toExtension.Cotangent := Cotangent.mk_surjective.subsingleton
-- Module: Mathlib.RingTheory.Smooth.Basic
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
⊢ Subsingleton P.toExtension.H1Cotangent

Tactic:
have := P.toExtension.h1Cotangentι_injective.subsingleton
-- Module: Mathlib.RingTheory.Smooth.Basic
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_2 : Subsingleton P.toExtension.Cotangent
this : Subsingleton P.toExtension.H1Cotangent
⊢ FormallySmooth R (MvPolynomial σ R)

Tactic:
⟨inferInstance, P.equivH1Cotangent.symm.subsingleton⟩

Premises used: LinearEquiv.symm, Algebra.FormallySmooth.mk, inferInstance, LinearEquiv.toAddEquiv, Algebra.Generators.equivH1Cotangent, AddEquiv.toEquiv, Equiv.subsingleton
-- Module: Mathlib.RingTheory.Smooth.Basic
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_2 : Subsingleton P.toExtension.Cotangent
this : Subsingleton P.toExtension.H1Cotangent
⊢ FormallySmooth R (MvPolynomial σ R)

Tactic:
exact ⟨inferInstance, P.equivH1Cotangent.symm.subsingleton⟩
-- Module: Mathlib.RingTheory.Smooth.Basic
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)
revert : ∀ (g : AlgHom.{u, v, u_1} R A (B ⧸ I)), ∃ (f : A →ₐ[R] B), AlgHom.comp (Ideal.Quotient.mkₐ R I) f = g
⊢ ∃ (f : A →ₐ[R] B), AlgHom.comp (Ideal.Quotient.mkₐ R I) f = g

Tactic:
revert g
-- Module: Mathlib.RingTheory.Smooth.Basic
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
change :
  Function.Surjective (α := A →ₐ[R] B) (β := AlgHom.{u, v, u_1} R A (B ⧸ I)) (AlgHom.comp (Ideal.Quotient.mkₐ R I))
⊢ ∀ (g : AlgHom.{u, v, u_1} R A (B ⧸ I)), ∃ (f : A →ₐ[R] B), AlgHom.comp (Ideal.Quotient.mkₐ R I) f = g

Tactic:
change Function.Surjective (Ideal.Quotient.mkₐ R I).comp

Premises used: AlgHom.comp, Ideal.Quotient.mkₐ, Function.Surjective
-- Module: Mathlib.RingTheory.Smooth.Basic
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
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))
⊢ 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›

Premises used: Algebra
-- Module: Mathlib.RingTheory.Smooth.Basic
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))
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))
⊢ ∀ [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))

Tactic:
apply Ideal.IsNilpotent.induction_on (S := B) I hI

Premises used: Ideal.IsNilpotent.induction_on
-- Module: Mathlib.RingTheory.Smooth.Basic
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 : Ideal B_1
hI : IsNilpotent I
B : Type u_1
h₁ :
  ∀ [inst_5 : CommRing B] (I : Ideal B),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      ∀ [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))
⊢ ∀ [inst_5 : CommRing B] (I : Ideal B),
    HPow.hPow (β := ℕ) I 2 = ⊥ →
      ∀ [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:
_
-- Module: Mathlib.RingTheory.Smooth.Basic
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_1 : IsNilpotent I_1
B : Type u_1
inst_5 : CommRing B
I : Ideal B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
h₁ :
  ∀ [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))
⊢ ∀ [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:
_
-- Module: Mathlib.RingTheory.Smooth.Basic
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_1 : IsNilpotent I_1
B : Type u_1
inst_5 : CommRing B
I : Ideal B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
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:
FormallySmooth.comp_surjective R A I hI

Premises used: Algebra.FormallySmooth.comp_surjective
-- Module: Mathlib.RingTheory.Smooth.Basic
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_1 : IsNilpotent I_1
B : Type u_1
inst_5 : CommRing B
I : Ideal B
hI : HPow.hPow (β := ℕ) I 2 = ⊥
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:
exact FormallySmooth.comp_surjective R A I hI

Premises used: Algebra.FormallySmooth.comp_surjective
-- Module: Mathlib.RingTheory.Smooth.Basic
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 : Ideal B_1
hI : IsNilpotent I
B : Type u_1
h₂ :
  ∀ [inst_5 : CommRing B] (I J : Ideal B),
    I ≤ J →
      (∀ [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))) →
        (∀ [inst_6 : 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],
            Function.Surjective (α := A →ₐ[R] B) (β := AlgHom.{u, v, u_1} R A (B ⧸ J))
              (AlgHom.comp (Ideal.Quotient.mkₐ R J))
⊢ ∀ [inst_5 : CommRing B] (I J : Ideal B),
    I ≤ J →
      (∀ [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))) →
        (∀ [inst_6 : 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],
            Function.Surjective (α := A →ₐ[R] B) (β := AlgHom.{u, v, u_1} R A (B ⧸ J))
              (AlgHom.comp (Ideal.Quotient.mkₐ R J))

Tactic:
_
-- Module: Mathlib.RingTheory.Smooth.Basic
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_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))
h₂ :
  ∀ [inst_6 : 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)))
h₃ :
  ∀ [inst_6 : Algebra R B],
    Function.Surjective (α := A →ₐ[R] B) (β := AlgHom.{u, v, u_1} R A (B ⧸ J)) (AlgHom.comp (Ideal.Quotient.mkₐ R J))
⊢ ∀ [inst_6 : Algebra R B],
    Function.Surjective (α := A →ₐ[R] B) (β := AlgHom.{u, v, u_1} R A (B ⧸ J)) (AlgHom.comp (Ideal.Quotient.mkₐ R J))

Tactic:
_
-- Module: Mathlib.RingTheory.Smooth.Basic
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' := ⋯ }
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
⊢ ∃ (a : A →ₐ[R] B), AlgHom.comp (Ideal.Quotient.mkₐ R J) a = g

Tactic:
obtain ⟨g', e⟩ := h₂ (this.symm.toAlgHom.comp g)

Premises used: AlgEquiv.toAlgHom, AlgEquiv.symm, AlgHom.comp