-- 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 : P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker f.toRingHom) 2
simp :
  Eq.{v + 1} (α := A)
    ((RingHom.kerLift (↑f.kerSquareLift : P.Ring ⧸ RingHom.ker (↑f : P.Ring →+* A) ^ 2 →+* A) :
          (a :
              (P.Ring ⧸ RingHom.ker (↑f : P.Ring →+* A) ^ 2) ⧸
                RingHom.ker (↑f.kerSquareLift : P.Ring ⧸ RingHom.ker (↑f : P.Ring →+* A) ^ 2 →+* A)) →
            A)
        ((Ideal.Quotient.mk (RingHom.ker f.kerSquareLift) :
              (a : P.Ring ⧸ RingHom.ker (↑f : P.Ring →+* A) ^ 2) →
                (P.Ring ⧸ RingHom.ker (↑f : P.Ring →+* A) ^ 2) ⧸ RingHom.ker f.kerSquareLift)
            x :
          HasQuotient.Quotient
            (P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker (F := P.Ring →+* A) (↑f : P.Ring →+* A)) 2)
            (B :=
            Ideal
              (P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker (F := P.Ring →+* A) (↑f : P.Ring →+* A)) 2))
            (RingHom.ker f.kerSquareLift)) :
      A)
    ((Ideal.quotientKerAlgEquivOfSurjective surj :
          (a : (P.Ring ⧸ RingHom.ker (↑f : P.Ring →+* A) ^ 2) ⧸ RingHom.ker f.kerSquareLift) → A)
        ((Ideal.Quotient.mk (RingHom.ker f.kerSquareLift) :
              (a : P.Ring ⧸ RingHom.ker (↑f : P.Ring →+* A) ^ 2) →
                (P.Ring ⧸ RingHom.ker (↑f : P.Ring →+* A) ^ 2) ⧸ RingHom.ker f.kerSquareLift)
            x :
          HasQuotient.Quotient
            (P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker (F := P.Ring →+* A) (↑f : P.Ring →+* A)) 2)
            (B :=
            Ideal
              (P.Ring ⧸ HPow.hPow (α := Ideal P.Ring) (β := ℕ) (RingHom.ker (F := P.Ring →+* A) (↑f : P.Ring →+* A)) 2))
            (RingHom.ker f.kerSquareLift)) :
      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)
              ((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)

Tactic:
simp only [AlgHom.toRingHom_eq_coe, AlgEquiv.coe_algHom, AlgEquiv.symm_apply_apply,
    AlgHom.coe_id, id_eq]

Premises used: AlgHom.coe_id, AlgEquiv.symm_apply_apply, AlgEquiv.coe_algHom, AlgHom.toRingHom_eq_coe, id_eq