-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : IsLocalization.Away r S
this :
  Eq (α := MvPolynomial Unit R →ₐ[R] S) (aeval (Generators.val (Generators.localizationAway S r)))
    (AlgHom.comp
      (↑(mvPolynomialQuotientEquiv S r) :
        MvPolynomial Unit R ⧸ Ideal.span {(C : (a : R) → MvPolynomial Unit R) r * X () - 1} →ₐ[R] S)
      (Ideal.Quotient.mkₐ R
        (Ideal.span
          {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
                ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
              1})))
⊢ Eq (α := Ideal (Generators.Ring (Generators.localizationAway S r)))
    (Ideal.comap (F :=
      MvPolynomial Unit R →+*
        HasQuotient.Quotient (MvPolynomial Unit R) (B := Ideal (MvPolynomial Unit R))
          (Ideal.span
            {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
                  ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
                1}))
      (↑(Ideal.Quotient.mkₐ R
            (Ideal.span
              {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
                    ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
                  1})) :
        MvPolynomial Unit R →+* MvPolynomial Unit R ⧸ Ideal.span {(C : (a : R) → MvPolynomial Unit R) r * X () - 1})
      (RingHom.ker (F :=
        RingHom.{u, v}
          (HasQuotient.Quotient (MvPolynomial Unit R) (B := Ideal (MvPolynomial Unit R))
            (Ideal.span
              {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
                    ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
                  1}))
          S)
        (↑(mvPolynomialQuotientEquiv S r) :
          MvPolynomial Unit R ⧸ Ideal.span {(C : (a : R) → MvPolynomial Unit R) r * X () - 1} →+* S)))
    (Ideal.span
      {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
            ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
          1})
have change : Eq (α := Ideal (MvPolynomial Unit R))
  (Ideal.comap (F :=
    MvPolynomial Unit R →+*
      HasQuotient.Quotient (MvPolynomial Unit R) (B := Ideal (MvPolynomial Unit R))
        (Ideal.span
          {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
                ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
              1}))
    (↑(Ideal.Quotient.mkₐ R
          (Ideal.span
            {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
                  ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
                1})) :
      MvPolynomial Unit R →+* MvPolynomial Unit R ⧸ Ideal.span {(C : (a : R) → MvPolynomial Unit R) r * X () - 1})
    (RingHom.ker (F :=
      HasQuotient.Quotient (MvPolynomial Unit R) (B := Ideal (MvPolynomial Unit R))
          (Ideal.span
            {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
                  ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
                1}) ≃ₐ[R]
        S)
      (mvPolynomialQuotientEquiv S r)))
  (Ideal.span
    {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
          ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
        1})
Tactic: change Ideal.comap _ (RingHom.ker (mvPolynomialQuotientEquiv S r)) = Ideal.span {C r * X () - 1}