-- 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 : A
obtain :
  ∀
    (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)),
    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)
⊢ 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:
obtain ⟨x, rfl⟩ := (Ideal.quotientKerAlgEquivOfSurjective surj).surjective x

Premises used: AlgEquiv.surjective, rfl, Ideal.quotientKerAlgEquivOfSurjective