awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
p_1 : MvPolynomial Unit R
hp :
  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})
    p_1
p q : MvPolynomial Unit R
refine_3 :
  Membership.mem (γ := Submodule (MvPolynomial Unit R) (MvPolynomial Unit R))
      (MvPolynomial Unit R ∙
        (HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
            ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
          1))
      p →
    ∀
      (hy :
        Membership.mem (γ := Submodule (MvPolynomial Unit R) (MvPolynomial Unit R))
          (MvPolynomial Unit R ∙
            (HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
                ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
              1))
          q),
      Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) p : S) (0 : S) →
        Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) q : S) (0 : S) →
          Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) (p + q) : S) (0 : S)
⊢ ∀
    (hx :
      Membership.mem (γ := Submodule (MvPolynomial Unit R) (MvPolynomial Unit R))
        (MvPolynomial Unit R ∙
          (HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
              ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
            1))
        p)
    (hy :
      Membership.mem (γ := Submodule (MvPolynomial Unit R) (MvPolynomial Unit R))
        (MvPolynomial Unit R ∙
          (HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
              ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
            1))
        q),
    Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) p : S) (0 : S) →
      Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) q : S) (0 : S) →
        Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) (p + q) : S) (0 : S)

Tactic:
_
-- 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
p_1 : MvPolynomial Unit R
hp :
  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})
    p_1
p q : MvPolynomial Unit R
hx :
  Membership.mem (γ := Submodule (MvPolynomial Unit R) (MvPolynomial Unit R))
    (MvPolynomial Unit R ∙
      (HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
          ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
        1))
    p
refine_3 :
  Membership.mem (γ := Submodule (MvPolynomial Unit R) (MvPolynomial Unit R))
      (MvPolynomial Unit R ∙
        (HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
            ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
          1))
      q →
    Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) p : S) (0 : S) →
      Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) q : S) (0 : S) →
        Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) (p + q) : S) (0 : S)
⊢ ∀
    (hy :
      Membership.mem (γ := Submodule (MvPolynomial Unit R) (MvPolynomial Unit R))
        (MvPolynomial Unit R ∙
          (HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
              ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
            1))
        q),
    Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) p : S) (0 : S) →
      Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) q : S) (0 : S) →
        Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) (p + q) : S) (0 : S)

Tactic:
_
-- 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
p_1 : MvPolynomial Unit R
hp_1 :
  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})
    p_1
p q : MvPolynomial Unit R
hx :
  Membership.mem (γ := Submodule (MvPolynomial Unit R) (MvPolynomial Unit R))
    (MvPolynomial Unit R ∙
      (HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
          ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
        1))
    p
hy :
  Membership.mem (γ := Submodule (MvPolynomial Unit R) (MvPolynomial Unit R))
    (MvPolynomial Unit R ∙
      (HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
          ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
        1))
    q
hp : Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) p : S) (0 : S)
hq : Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) q : S) (0 : S)
⊢ Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) (p + q) : S) (0 : S)

Tactic:
simp [hp, hq]
-- 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
p : MvPolynomial Unit R
hp :
  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})
    p
a x : MvPolynomial Unit R
refine_4 :
  Membership.mem (γ := Submodule (MvPolynomial Unit R) (MvPolynomial Unit R))
      (MvPolynomial Unit R ∙
        (HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
            ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
          1))
      x →
    Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) x : S) (0 : S) →
      Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) (a • x) : S) (0 : S)
⊢ ∀
    (hx :
      Membership.mem (γ := Submodule (MvPolynomial Unit R) (MvPolynomial Unit R))
        (MvPolynomial Unit R ∙
          (HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
              ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
            1))
        x),
    Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) x : S) (0 : S) →
      Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) (a • x) : S) (0 : S)

Tactic:
_
-- 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
p : MvPolynomial Unit R
hp :
  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})
    p
a x : MvPolynomial Unit R
hx_1 :
  Membership.mem (γ := Submodule (MvPolynomial Unit R) (MvPolynomial Unit R))
    (MvPolynomial Unit R ∙
      (HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
          ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
        1))
    x
hx : Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) x : S) (0 : S)
⊢ Eq.{u_3 + 1} (α := S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) (a • x) : S) (0 : S)

Tactic:
simp [hx]
-- 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
p : MvPolynomial Unit R
⊢ Eq.{u_3 + 1} (α := S)
    ((auxHom S r : (a : MvPolynomial Unit R ⧸ Ideal.span {(C : (a : R) → MvPolynomial Unit R) r * X () - 1}) → S)
        ((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})
            p :
          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)
    ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) p : S)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Quotient.liftOn', AddCon.liftOn, Finsupp.sum, MvPolynomial.eval₂, Finset.sum, rfl
-- 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
simp :
  IsUnit (M :=
    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}))
⊢ IsUnit (M :=
    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}))
    ((g : (a : R) → MvPolynomial Unit R ⧸ Ideal.span {(C : (a : R) → MvPolynomial Unit R) r * X () - 1}) 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}))

Tactic:
simp only [RingHom.coe_comp, Function.comp_apply, g]

Premises used: RingHom.coe_comp, Function.comp_apply
-- 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
rw :
  ∃ (b :
    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})),
    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}))
        ((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}))
        b =
      1
⊢ IsUnit (M :=
    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}))

Tactic:
rw [isUnit_iff_exists_inv]

Premises used: isUnit_iff_exists_inv
-- 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
⊢ 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)

Tactic:
Ideal.mem_span_singleton_self (C r * X () - 1)

Premises used: Unit.unit, HMul.hMul, Set.Mem, HSub.hSub, MvPolynomial.X, OfNat.ofNat, MvPolynomial.C, DFunLike.coe, Ideal.mem_span_singleton_self
-- 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
⊢ 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)

Tactic:
exact Ideal.mem_span_singleton_self (C r * X () - 1)

Premises used: Unit.unit, HMul.hMul, HSub.hSub, MvPolynomial.X, OfNat.ofNat, MvPolynomial.C, DFunLike.coe, Ideal.mem_span_singleton_self
-- 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
h :
  Eq (α := R →+* S)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (RingHom.comp (β :=
        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}))
        (AlgHom.toRingHom (auxHom S r)) (auxInv S r))
      (algebraMap R S))
    (RingHom.comp (RingHom.id S) (algebraMap R S))
⊢ Eq (α := S →+* S)
    (RingHom.comp (β :=
      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}))
      (AlgHom.toRingHom (auxHom S r)) (auxInv S r))
    (RingHom.id S)

Tactic:
apply IsLocalization.ringHom_ext (Submonoid.powers r)

Premises used: Submonoid.powers, IsLocalization.ringHom_ext
-- 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
h :
  ∀ (x : R),
    Eq.{u_3 + 1} (α := S)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (RingHom.comp (β :=
                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}))
                (AlgHom.toRingHom (auxHom S r)) (auxInv S r))
              (algebraMap R S) :
            (a : R) → S)
          x :
        S)
      ((RingHom.comp (RingHom.id S) (algebraMap R S) : (a : R) → S) x : S)
⊢ Eq (α := R →+* S)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (RingHom.comp (β :=
        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}))
        (AlgHom.toRingHom (auxHom S r)) (auxInv S r))
      (algebraMap R S))
    (RingHom.comp (RingHom.id S) (algebraMap R S))

Tactic:
ext x
-- 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
x : R
⊢ Eq.{u_3 + 1} (α := S)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (RingHom.comp (β :=
              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}))
              (AlgHom.toRingHom (auxHom S r)) (auxInv S r))
            (algebraMap R S) :
          (a : R) → S)
        x :
      S)
    ((RingHom.comp (RingHom.id S) (algebraMap R S) : (a : R) → S) x : S)

Tactic:
simp [auxInv]

Premises used: _private.0.IsLocalization.Away.auxInv
-- 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
rw :
  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})))
⊢ 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}) →+*
      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 _ _ _ _ Semiring.toNonAssocSemiring _ (auxInv S r) (AlgHom.toRingHom (auxHom S r)))
    (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})))

Tactic:
rw [← RingHom.cancel_right (Ideal.Quotient.mk_surjective)]

Premises used: Ideal.Quotient.mk_surjective, RingHom.cancel_right