-- Module: Mathlib.RingTheory.MvPolynomial.Localization
Goal:
R : Type u_2
inst : CommRing R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : Away r S
hC :
  ∀ (x : R),
    Eq (α :=
      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}))
      ((RingHom.comp
              (RingHom.comp
                (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (auxInv S r) (AlgHom.toRingHom (auxHom S r)))
                (Ideal.Quotient.mk
                  (Ideal.span
                    {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
                          ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
                        1})))
              C :
            (a : R) → MvPolynomial Unit R ⧸ Ideal.span {(C : (a : R) → MvPolynomial Unit R) r * X () - 1})
          x :
        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}))
      ((RingHom.comp
              (RingHom.comp
                (RingHom.id
                  (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
                  (Ideal.span
                    {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
                          ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
                        1})))
              C :
            (a : R) → MvPolynomial Unit R ⧸ Ideal.span {(C : (a : R) → MvPolynomial Unit R) r * X () - 1})
          x :
        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}))
hX :
  ∀ (x : Unit),
    Eq (α :=
      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}))
      ((RingHom.comp (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (auxInv S r) (AlgHom.toRingHom (auxHom S r)))
              (Ideal.Quotient.mk
                (Ideal.span
                  {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
                        ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
                      1})) :
            (a : MvPolynomial Unit R) →
              MvPolynomial Unit R ⧸ Ideal.span {(C : (a : R) → MvPolynomial Unit R) r * X () - 1})
          (X x) :
        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}))
      ((RingHom.comp
              (RingHom.id
                (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
                (Ideal.span
                  {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
                        ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
                      1})) :
            (a : MvPolynomial Unit R) →
              MvPolynomial Unit R ⧸ Ideal.span {(C : (a : R) → MvPolynomial Unit R) r * X () - 1})
          (X x) :
        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}))
⊢ Eq (α :=
    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}))
    (RingHom.comp (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (auxInv S r) (AlgHom.toRingHom (auxHom S r)))
      (Ideal.Quotient.mk
        (Ideal.span
          {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
                ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
              1})))
    (RingHom.comp
      (RingHom.id
        (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
        (Ideal.span
          {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
                ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
              1})))

Tactic:
ext x