-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
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})))
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})
⊢ 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})

Tactic:
change Ideal.comap _ (RingHom.ker (mvPolynomialQuotientEquiv S r)) = Ideal.span {C r * X () - 1}

Premises used: Unit.unit, HMul.hMul, HSub.hSub, MvPolynomial.X, Ideal.comap, Ideal.span, IsLocalization.Away.mvPolynomialQuotientEquiv, Singleton.singleton, OfNat.ofNat, MvPolynomial.C, DFunLike.coe, RingHom.ker