-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.LocalizationAway (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
P : Generators R S ι
Q : Generators S T Unit := localizationAway T g
algInst : Algebra P.Ring (Generators.Ring (comp (localizationAway T g) P)) :=
  RingHom.toAlgebra (AlgHom.toRingHom (Hom.toAlgHom (toComp (localizationAway T g) P)))
f : P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2 :=
  (Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g)
π : Generators.Ring (comp (localizationAway T g) P) →ₐ[R]
  Localization.Away (M := P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2)
    ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g) :
      P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2) :=
  compLocalizationAwayAlgHom T g P
x : ↥P.toExtension.ker
hx :
  Eq (α := Extension.Cotangent (toExtension (Q.comp P)))
    ((lift
            ((↑S :
                {S_1 M : Type u_3} →
                  {M₂ : Type (max u_1 u_4)} →
                    [inst : Semiring S] →
                      [inst_8 : Semiring S_1] →
                        [inst_9 : AddCommMonoid M] →
                          [inst_10 : AddCommMonoid M₂] →
                            [inst_11 : Module S M] →
                              [inst_12 : Module S M₂] →
                                [inst_13 : Module S_1 M] →
                                  [inst_14 : Module S_1 M₂] →
                                    [LinearMap.CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
              (S := T)
              (((↑(LinearEquiv.symm
                        (LinearMap.ringLmapEquivSelf T T
                          (P.toExtension.Cotangent →ₗ[S] Extension.Cotangent (toExtension (Q.comp P))))) :
                    (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent) →ₗ[T]
                      T →ₗ[T] P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent) :
                  (a : P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent) →
                    T →ₗ[T] P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)
                (Extension.Cotangent.map (Hom.toExtensionHom (Q.toComp P))))) :
          (a : T ⊗[S] P.toExtension.Cotangent) → (Q.comp P).toExtension.Cotangent)
        (((TensorProduct.mk S T P.toExtension.Cotangent :
                (a : T) → P.toExtension.Cotangent →ₗ[S] T ⊗[S] P.toExtension.Cotangent)
              1 :
            (a : P.toExtension.Cotangent) → T ⊗[S] P.toExtension.Cotangent)
          ((Extension.Cotangent.mk : (a : ↥P.toExtension.ker) → P.toExtension.Cotangent) x)) :
      Extension.Cotangent (toExtension (Q.comp P)))
    (0 : Extension.Cotangent (toExtension (Q.comp P)))
⊢ Eq (α := Localization.Away f)
    ((compLocalizationAwayAlgHom T g P :
          (a : ((localizationAway T g).comp P).Ring) →
            Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g)))
        ((Hom.toAlgHom (toComp (localizationAway T g) P) : (a : P.Ring) → ((localizationAway T g).comp P).Ring)
          (↑x : P.toExtension.Ring)) :
      Localization.Away (M := P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2)
        ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) (P.σ g) :
          P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2))
    (0 : Localization.Away f)
have a : Membership.mem (α := Generators.Ring (comp (localizationAway T g) P))
  (HPow.hPow (α := Ideal (Generators.Ring (comp (localizationAway T g) P))) (β := ℕ)
    (ker (comp (localizationAway T g) P)) 2)
  ((Hom.toAlgHom (toComp (localizationAway T g) P) : (a : P.Ring) → ((localizationAway T g).comp P).Ring)
      (↑x : P.toExtension.Ring) :
    Generators.Ring (comp (localizationAway T g) P))
Tactic: apply sq_ker_comp_le_ker_compLocalizationAwayAlgHom