awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (α :=
    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}))

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
x : Unit
hX :
  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 x) -
      1)
⊢ 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 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}))

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

Premises used: neg_sub, Ideal.Quotient.mk, map_mul, map_one, Ideal.Quotient.mk_eq_mk_iff_sub_mem, Ideal.neg_mem_iff
-- 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 : Unit
⊢ 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 x) -
      1)

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

Premises used: HMul.hMul, Set.Mem, setOf, 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
x : Unit
⊢ 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 x) -
      1)

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

Premises used: HMul.hMul, 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
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})
⊢ ((auxInv S r :
          RingHom.{u_3, u_2} S
            (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}))) :
        (a : S) → MvPolynomial Unit R ⧸ Ideal.span {(C : (a : R) → MvPolynomial Unit R) r * X () - 1})
      ((auxHom S r : (a : MvPolynomial Unit R ⧸ Ideal.span {(C : (a : R) → MvPolynomial Unit R) r * X () - 1}) → S) x) =
    x

Tactic:
simpa using congrFun (congrArg DFunLike.coe <| auxInv_auxHom S r) x

Premises used: congrArg, congrFun, _private.0.IsLocalization.Away.auxInv_auxHom, DFunLike.coe
-- 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
s : S
⊢ (auxHom S r : (a : MvPolynomial Unit R ⧸ Ideal.span {(C : (a : R) → MvPolynomial Unit R) r * X () - 1}) → S)
      (((auxInv S r :
              RingHom.{u_3, u_2} S
                (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}))) :
            (a : S) → MvPolynomial Unit R ⧸ Ideal.span {(C : (a : R) → MvPolynomial Unit R) r * X () - 1})
          s :
        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

Tactic:
simpa using congrFun (congrArg DFunLike.coe <| auxHom_auxInv S r) s

Premises used: congrArg, _private.0.IsLocalization.Away.auxHom_auxInv, congrFun, DFunLike.coe
-- 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
⊢ ∀
    (x y :
      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})),
    (auxHom S r : (a : MvPolynomial Unit R ⧸ Ideal.span {(C : (a : R) → MvPolynomial Unit R) r * X () - 1}) → S)
        (x * y) =
      HMul.hMul (α := S) (β := S)
        ((auxHom S r : (a : MvPolynomial Unit R ⧸ Ideal.span {(C : (a : R) → MvPolynomial Unit R) r * X () - 1}) → S)
            x :
          S)
        ((auxHom S r : (a : MvPolynomial Unit R ⧸ Ideal.span {(C : (a : R) → MvPolynomial Unit R) r * X () - 1}) → S)
            y :
          S)

Tactic:
simp