-- Module: Mathlib.RingTheory.Smooth.Basic
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)
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)
obtain :
  ∀ (x : P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2),
    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)
              ((Ideal.quotientKerAlgEquivOfSurjective surj :
                  (a : (P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) ⧸ RingHom.ker f.kerSquareLift) → A)
                ((Ideal.Quotient.mk (RingHom.ker f.kerSquareLift) :
                      (a : P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) →
                        (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))) :
            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)
          ((Ideal.quotientKerAlgEquivOfSurjective surj :
                (a : (P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) ⧸ RingHom.ker f.kerSquareLift) → A)
              ((Ideal.Quotient.mk (RingHom.ker f.kerSquareLift) :
                    (a : P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) →
                      (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) :
        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)
            ((Ideal.quotientKerAlgEquivOfSurjective surj :
                (a : (P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) ⧸ RingHom.ker f.kerSquareLift) → A)
              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)
        ((Ideal.quotientKerAlgEquivOfSurjective surj :
              (a : (P.Ring ⧸ RingHom.ker f.toRingHom ^ 2) ⧸ RingHom.ker f.kerSquareLift) → A)
            x :
          A) :
      A)

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Premises used: Ideal.Quotient.mk_surjective, rfl