-- 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 ι
f : P.Ring
h : (algebraMap P.Ring S : (a : P.Ring) → S) f = g
this :
  Eq (α := Ideal (Generators.Ring (localizationAway T g))) (ker (localizationAway T g))
    (Ideal.map (R := Generators.Ring (comp (localizationAway T g) P)) (F :=
      Generators.Ring (comp (localizationAway T g) P) →ₐ[R] Generators.Ring (localizationAway T g))
      (Hom.toAlgHom (ofComp (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) f :
                MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
              (X (Sum.inl ())) -
            1}))
rw :
  Eq (α := Ideal (Generators.Ring (comp (localizationAway T g) P)))
    (RingHom.ker (F := Generators.Ring (comp (localizationAway T g) P) →ₐ[R] Generators.Ring (localizationAway T g))
          (Hom.toAlgHom (ofComp (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) f :
                  MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
                (X (Sum.inl ())) -
              1} ⊔
      RingHom.ker (F := Generators.Ring (comp (localizationAway T g) P) →ₐ[R] Generators.Ring (localizationAway T g))
        (Hom.toAlgHom (ofComp (localizationAway T g) P)))
    (RingHom.ker (F := Generators.Ring (comp (localizationAway T g) P) →ₐ[R] Generators.Ring (localizationAway T g))
        (Hom.toAlgHom (ofComp (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) f :
                MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
              (X (Sum.inl ())) -
            1})
⊢ Eq (α := Ideal (Generators.Ring (comp (localizationAway T g) P))) (ker (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) f :
                MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
              (X (Sum.inl ())) -
            1})

Tactic:
rw [ker_comp_eq_sup, Algebra.Generators.map_toComp_ker, this,
    Ideal.comap_map_of_surjective _ (toAlgHom_ofComp_surjective _ P), ← RingHom.ker_eq_comap_bot,
    ← sup_assoc]

Premises used: Algebra.Generators.map_toComp_ker, Algebra.Generators.toAlgHom_ofComp_surjective, sup_assoc, Ideal.comap_map_of_surjective, RingHom.ker_eq_comap_bot, Algebra.Generators.ker_comp_eq_sup