-- 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 ι
f : P.Ring
h : (algebraMap P.Ring S : (a : P.Ring) → S) f = g
rw :
  Eq (α := Ideal (Generators.Ring (localizationAway T g))) (ker (localizationAway T g))
    (Ideal.span
      (Set.image (α := Generators.Ring (comp (localizationAway T g) P))
        (⇑(Hom.toAlgHom (ofComp (localizationAway T g) P)) :
          (a : ((localizationAway T g).comp P).Ring) → (localizationAway T g).Ring)
        {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 (localizationAway T g))) (ker (localizationAway T g))
    (Ideal.span
      (singleton (α := Generators.Ring (localizationAway T g))
        ((Hom.toAlgHom (ofComp (localizationAway T g) P) :
              (a : ((localizationAway T g).comp P).Ring) → (localizationAway T g).Ring)
            (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) :
          Generators.Ring (localizationAway T g))))
rw₂ :
  Eq (α := Ideal (Generators.Ring (localizationAway T g))) (ker (localizationAway T g))
    (Ideal.span
      {HSub.hSub (α := Generators.Ring (localizationAway T g)) (β := Generators.Ring (localizationAway T g))
          ((Hom.toAlgHom (ofComp (localizationAway T g) P) :
                (a : ((localizationAway T g).comp P).Ring) → (localizationAway T g).Ring)
              (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 ()))) :
            Generators.Ring (localizationAway T g))
          ((Hom.toAlgHom (ofComp (localizationAway T g) P) :
                (a : ((localizationAway T g).comp P).Ring) → (localizationAway T g).Ring)
              1 :
            Generators.Ring (localizationAway T g))})
rw₃ :
  Eq (α := Ideal (Generators.Ring (localizationAway T g))) (ker (localizationAway T g))
    (Ideal.span
      {HMul.hMul (α := Generators.Ring (localizationAway T g)) (β := Generators.Ring (localizationAway T g))
            ((Hom.toAlgHom (ofComp (localizationAway T g) P) :
                  (a : ((localizationAway T g).comp P).Ring) → (localizationAway T g).Ring)
                ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) f) :
              Generators.Ring (localizationAway T g))
            ((Hom.toAlgHom (ofComp (localizationAway T g) P) :
                  (a : ((localizationAway T g).comp P).Ring) → (localizationAway T g).Ring)
                (X (Sum.inl ())) :
              Generators.Ring (localizationAway T g)) -
          (Hom.toAlgHom (ofComp (localizationAway T g) P) :
              (a : ((localizationAway T g).comp P).Ring) → (localizationAway T g).Ring)
            1})
rw₄ :
  Eq (α := Ideal (Generators.Ring (localizationAway T g))) (ker (localizationAway T g))
    (Ideal.span
      {HMul.hMul (α := Generators.Ring (localizationAway T g)) (β := Generators.Ring (localizationAway T g))
            ((Hom.toAlgHom (ofComp (localizationAway T g) P) :
                  (a : ((localizationAway T g).comp P).Ring) → (localizationAway T g).Ring)
                ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) f) :
              Generators.Ring (localizationAway T g))
            ((Hom.toAlgHom (ofComp (localizationAway T g) P) :
                  (a : ((localizationAway T g).comp P).Ring) → (localizationAway T g).Ring)
                (X (Sum.inl ())) :
              Generators.Ring (localizationAway T g)) -
          1})
⊢ 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}))
have rw₅ : Eq (α := Ideal (Generators.Ring (localizationAway T g)))
  (Ideal.span
    {HMul.hMul (α := MvPolynomial Unit S) (β := MvPolynomial Unit S)
          ((C : (a : S) → MvPolynomial Unit S) g : MvPolynomial Unit S) (X ()) -
        1})
  (Ideal.span
    {HMul.hMul (α := Generators.Ring (localizationAway T g)) (β := Generators.Ring (localizationAway T g))
          ((Hom.toAlgHom (ofComp (localizationAway T g) P) :
                (a : ((localizationAway T g).comp P).Ring) → (localizationAway T g).Ring)
              ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) f) :
            Generators.Ring (localizationAway T g))
          ((Hom.toAlgHom (ofComp (localizationAway T g) P) :
                (a : ((localizationAway T g).comp P).Ring) → (localizationAway T g).Ring)
              (X (Sum.inl ())) :
            Generators.Ring (localizationAway T g)) -
        1})
Tactic: rw [Ideal.map_span, Set.image_singleton, map_sub, map_mul, map_one, ker_localizationAway,
      Hom.toAlgHom_X, toAlgHom_ofComp_rename, h, ofComp_val, Sum.elim_inl]