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