-- Module: Mathlib.RingTheory.MvPolynomial.Localization
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
M : Submonoid R
S : Type u_3
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
inst_3 : Away r S
g : 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
    (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
h :
  Membership.mem (γ := 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})
    (HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
        ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
      1)
⊢ HMul.hMul (α :=
      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}))
      (β :=
      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})
          ((C : (a : R) → MvPolynomial Unit R) 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
              (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 ()) :
        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})) =
    1

Tactic:
rw [← map_mul, ← map_one (Ideal.Quotient.mk _), Ideal.Quotient.mk_eq_mk_iff_sub_mem]

Premises used: Ideal.Quotient.mk, map_mul, map_one, Ideal.Quotient.mk_eq_mk_iff_sub_mem