-- Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway
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 ι
hsple :
  ∀ {x : Generators.Ring (comp (localizationAway T g) P)}
    (hx :
      Membership.mem (γ := Ideal (Generators.Ring (comp (localizationAway T g) P)))
        (Ideal.span
          {HMul.hMul (α := MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R) (β := MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
                ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ g) :
                  MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
                (X (Sum.inl ())) -
              1})
        x),
    Eq (α :=
      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 :
            (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)))
          x :
        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 (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))
rw :
  HMul.hMul (α := Ideal (Generators.Ring (comp (localizationAway T g) P)))
          (Ideal.map (F := P.Ring →ₐ[R] Generators.Ring (comp (localizationAway T g) P))
            (Hom.toAlgHom (toComp (localizationAway T g) P)) P.ker)
          (Ideal.map (F := P.Ring →ₐ[R] Generators.Ring (comp (localizationAway T g) P))
            (Hom.toAlgHom (toComp (localizationAway T g) P)) P.ker) ⊔
        HMul.hMul (α := Ideal (Generators.Ring (comp (localizationAway T g) P)))
          (Ideal.map (F := P.Ring →ₐ[R] Generators.Ring (comp (localizationAway T g) P))
            (Hom.toAlgHom (toComp (localizationAway T g) P)) P.ker)
          (Ideal.span
            {HMul.hMul (α := MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R) (β := MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
                  ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ g) :
                    MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
                  (X (Sum.inl ())) -
                1}) ⊔
      (HMul.hMul (α := Ideal (Generators.Ring (comp (localizationAway T g) P)))
          (Ideal.span
            {HMul.hMul (α := MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R) (β := MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
                  ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ g) :
                    MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
                  (X (Sum.inl ())) -
                1})
          (Ideal.map (F := P.Ring →ₐ[R] Generators.Ring (comp (localizationAway T g) P))
            (Hom.toAlgHom (toComp (localizationAway T g) P)) P.ker) ⊔
        HMul.hMul (α := Ideal (Generators.Ring (comp (localizationAway T g) P)))
          (Ideal.span
            {HMul.hMul (α := MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R) (β := MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
                  ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ g) :
                    MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
                  (X (Sum.inl ())) -
                1})
          (Ideal.span
            {HMul.hMul (α := MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R) (β := MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
                  ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ g) :
                    MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
                  (X (Sum.inl ())) -
                1})) ≤
    RingHom.ker (F :=
      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)
⊢ HPow.hPow (α := Ideal (Generators.Ring (comp (localizationAway T g) P))) (β := ℕ)
      (ker (comp (localizationAway T g) P)) 2 ≤
    RingHom.ker (F :=
      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)

Tactic:
rw [comp_localizationAway_ker _ _ (P.σ g) (by simp), sq, Ideal.sup_mul, Ideal.mul_sup,
    Ideal.mul_sup]

Premises used: Ideal.mul_sup, sq, Algebra.Generators.comp_localizationAway_ker, Ideal.sup_mul, Algebra.Generators.σ