awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_3 : FinitePresentation R S
H : ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S),
  Function.Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S) ∧
    Ideal.FG (RingHom.ker f.toRingHom) :=
  ⋯
n : ℕ :=
  H.choose (p := fun (n : ℕ) ↦
    ∃ (f : MvPolynomial (Fin n) R →ₐ[R] S),
      Function.Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S)
          (⇑f : (a : MvPolynomial (Fin n) R) → S) ∧
        Ideal.FG (RingHom.ker f.toRingHom))
f : MvPolynomial (Fin n) R →ₐ[R] S :=
  ⋯.choose (p :=
    fun
      (f :
        MvPolynomial
            (Fin
              (H.choose (p := fun (n : ℕ) ↦
                ∃ (f : MvPolynomial (Fin n) R →ₐ[R] S),
                  Function.Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S)
                      (⇑f : (a : MvPolynomial (Fin n) R) → S) ∧
                    Ideal.FG (RingHom.ker f.toRingHom))))
            R →ₐ[R]
          S) ↦
    Function.Surjective.{u + 1, v + 1} (α :=
        MvPolynomial
          (Fin
            (H.choose (p := fun (n : ℕ) ↦
              ∃ (f : MvPolynomial (Fin n) R →ₐ[R] S),
                Function.Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S)
                    (⇑f : (a : MvPolynomial (Fin n) R) → S) ∧
                  Ideal.FG (RingHom.ker f.toRingHom))))
          R)
        (β := S) (⇑f : (a : MvPolynomial (Fin H.choose) R) → S) ∧
      Ideal.FG (RingHom.ker f.toRingHom))
hf : Function.Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
hf' : Ideal.FG (RingHom.ker f)
H' : ∃ (n_1 : ℕ) (s : Fin n_1 → MvPolynomial (Fin n) R),
  Eq (α := Submodule (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R))
    (Submodule.span (MvPolynomial (Fin n) R) (Set.range s)) (RingHom.ker f) :=
  ⋯
m : ℕ :=
  H'.choose (p := fun (n_1 : ℕ) ↦
    ∃ (s : Fin n_1 → MvPolynomial (Fin n) R),
      Eq (α := Submodule (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R))
        (Submodule.span (MvPolynomial (Fin n) R) (Set.range s)) (RingHom.ker f))
v : Fin m → MvPolynomial (Fin n) R :=
  ⋯.choose (p :=
    fun
      (s :
        Fin
            (H'.choose (p := fun (n_1 : ℕ) ↦
              ∃ (s : Fin n_1 → MvPolynomial (Fin n) R),
                Eq (α := Submodule (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R))
                  (Submodule.span (MvPolynomial (Fin n) R) (Set.range s)) (RingHom.ker f))) →
          MvPolynomial (Fin n) R) ↦
    Eq (α := Submodule (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R))
      (Submodule.span (MvPolynomial (Fin n) R) (Set.range s)) (RingHom.ker f))
hv : Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.span (Set.range v)) (RingHom.ker f)
e_f :
  ∀ (i : Fin n),
    Eq.{v + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) (X i) : S)
      ((aeval fun (x : Fin n) ↦ (f : (a : MvPolynomial (Fin n) R) → S) (X x) : (a : MvPolynomial (Fin n) R) → S) (X i) :
        S)
⊢ f = aeval fun (x : Fin n) ↦ (f : (a : MvPolynomial (Fin n) R) → S) (X x)

Tactic:
ext
-- 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
inst_3 : FinitePresentation R S
H : ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S),
  Function.Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S) ∧
    Ideal.FG (RingHom.ker f.toRingHom) :=
  ⋯
n : ℕ :=
  H.choose (p := fun (n : ℕ) ↦
    ∃ (f : MvPolynomial (Fin n) R →ₐ[R] S),
      Function.Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S)
          (⇑f : (a : MvPolynomial (Fin n) R) → S) ∧
        Ideal.FG (RingHom.ker f.toRingHom))
f : MvPolynomial (Fin n) R →ₐ[R] S :=
  ⋯.choose (p :=
    fun
      (f :
        MvPolynomial
            (Fin
              (H.choose (p := fun (n : ℕ) ↦
                ∃ (f : MvPolynomial (Fin n) R →ₐ[R] S),
                  Function.Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S)
                      (⇑f : (a : MvPolynomial (Fin n) R) → S) ∧
                    Ideal.FG (RingHom.ker f.toRingHom))))
            R →ₐ[R]
          S) ↦
    Function.Surjective.{u + 1, v + 1} (α :=
        MvPolynomial
          (Fin
            (H.choose (p := fun (n : ℕ) ↦
              ∃ (f : MvPolynomial (Fin n) R →ₐ[R] S),
                Function.Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S)
                    (⇑f : (a : MvPolynomial (Fin n) R) → S) ∧
                  Ideal.FG (RingHom.ker f.toRingHom))))
          R)
        (β := S) (⇑f : (a : MvPolynomial (Fin H.choose) R) → S) ∧
      Ideal.FG (RingHom.ker f.toRingHom))
hf : Function.Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
hf' : Ideal.FG (RingHom.ker f)
H' : ∃ (n_1 : ℕ) (s : Fin n_1 → MvPolynomial (Fin n) R),
  Eq (α := Submodule (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R))
    (Submodule.span (MvPolynomial (Fin n) R) (Set.range s)) (RingHom.ker f) :=
  ⋯
m : ℕ :=
  H'.choose (p := fun (n_1 : ℕ) ↦
    ∃ (s : Fin n_1 → MvPolynomial (Fin n) R),
      Eq (α := Submodule (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R))
        (Submodule.span (MvPolynomial (Fin n) R) (Set.range s)) (RingHom.ker f))
v : Fin m → MvPolynomial (Fin n) R :=
  ⋯.choose (p :=
    fun
      (s :
        Fin
            (H'.choose (p := fun (n_1 : ℕ) ↦
              ∃ (s : Fin n_1 → MvPolynomial (Fin n) R),
                Eq (α := Submodule (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R))
                  (Submodule.span (MvPolynomial (Fin n) R) (Set.range s)) (RingHom.ker f))) →
          MvPolynomial (Fin n) R) ↦
    Eq (α := Submodule (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R))
      (Submodule.span (MvPolynomial (Fin n) R) (Set.range s)) (RingHom.ker f))
hv : Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.span (Set.range v)) (RingHom.ker f)
i : Fin n
⊢ Eq.{v + 1} (α := S) ((f : (a : MvPolynomial (Fin n) R) → S) (X i) : S)
    ((aeval fun (x : Fin n) ↦ (f : (a : MvPolynomial (Fin n) R) → S) (X x) : (a : MvPolynomial (Fin n) R) → S) (X i) :
      S)

Tactic:
simp
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 P : Presentation R S ι σ
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
⊢ Ideal.span (Set.range fun (i : σ) ↦ P.relation i) = (P.ofAlgEquiv e).ker

Tactic:
simp [P.span_range_relation_eq_ker]

Premises used: Algebra.Presentation.span_range_relation_eq_ker
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
T : Type u_1
inst_3 : CommRing T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
⊢ (P.ofAlgEquiv e).dimension = P.dimension

Tactic:
rfl

Premises used: Algebra.Presentation.ofAlgEquiv, Algebra.Presentation.dimension, rfl
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
h : Function.Bijective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
simp : ⊥ = (Generators.ofSurjectiveAlgebraMap ⋯).ker
⊢ Ideal.span (Set.range PEmpty.elim) = (Generators.ofSurjectiveAlgebraMap ⋯).ker

Tactic:
simp only [Set.range_eq_empty, Ideal.span_empty]

Premises used: Ideal.span_empty, Set.range_eq_empty
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
h : Function.Bijective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
symm : (Generators.ofSurjectiveAlgebraMap ⋯).ker = ⊥
⊢ ⊥ = (Generators.ofSurjectiveAlgebraMap ⋯).ker

Tactic:
symm
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
h : Function.Bijective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
rw :
  Function.Injective (α := (Generators.ofSurjectiveAlgebraMap ⋯).toExtension.Ring) (β := S)
    (⇑(algebraMap (Generators.ofSurjectiveAlgebraMap ⋯).toExtension.Ring S) :
      (a : (Generators.ofSurjectiveAlgebraMap ⋯).toExtension.Ring) → S)
⊢ (Generators.ofSurjectiveAlgebraMap ⋯).ker = ⊥

Tactic:
rw [← RingHom.injective_iff_ker_eq_bot]

Premises used: RingHom.injective_iff_ker_eq_bot
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
h : Function.Bijective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
change :
  Function.Injective (α := MvPolynomial PEmpty.{w + 1} R) (β := S)
    (⇑(aeval PEmpty.elim) : (a : MvPolynomial PEmpty.{w + 1} R) → S)
⊢ Function.Injective (α := (Generators.ofSurjectiveAlgebraMap ⋯).toExtension.Ring) (β := S)
    (⇑(algebraMap (Generators.ofSurjectiveAlgebraMap ⋯).toExtension.Ring S) :
      (a : (Generators.ofSurjectiveAlgebraMap ⋯).toExtension.Ring) → S)

Tactic:
change Function.Injective (aeval PEmpty.elim)

Premises used: MvPolynomial.aeval, PEmpty.elim, Function.Injective, DFunLike.coe
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
h : Function.Bijective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
rw : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Function.Injective (α := MvPolynomial PEmpty.{w + 1} R) (β := S)
    (⇑(aeval PEmpty.elim) : (a : MvPolynomial PEmpty.{w + 1} R) → S)

Tactic:
rw [aeval_injective_iff_of_isEmpty]

Premises used: MvPolynomial.aeval_injective_iff_of_isEmpty
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
h : Function.Bijective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)

Tactic:
h.injective

Premises used: Function.Bijective.injective
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
h : Function.Bijective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)

Tactic:
exact h.injective

Premises used: Function.Bijective.injective
-- 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
h : Function.Bijective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ (ofBijectiveAlgebraMap h).dimension = 0

Tactic:
simp [dimension]

Premises used: Algebra.Presentation.dimension
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
inst : CommRing R
⊢ dimension.{u_1, u_2, u, u} (id R) = 0

Tactic:
ofBijectiveAlgebraMap_dimension (R := R) Function.bijective_id

Premises used: Function.bijective_id, Algebra.Presentation.id, Algebra.Presentation.ofBijectiveAlgebraMap_dimension
-- 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
hf :
  ∀ (x : Unit),
    Eq.{v + 1} (α := S)
      ((aeval (Generators.val (Generators.localizationAway S r)) : (a : MvPolynomial Unit R) → S) (X x) : S)
      ((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})) :
            (a : MvPolynomial Unit R) → S)
          (X x) :
        S)
⊢ 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})))

Tactic:
ext x
-- 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
x : Unit
hf :
  Eq.{v + 1} (α := S) (invSelf r : S)
    ((mvPolynomialQuotientEquiv 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})
            (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})) :
      S)
⊢ Eq.{v + 1} (α := S)
    ((aeval (Generators.val (Generators.localizationAway S r)) : (a : MvPolynomial Unit R) → S) (X x) : S)
    ((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})) :
          (a : MvPolynomial Unit R) → S)
        (X x) :
      S)

Tactic:
simp only [aeval_X, Generators.localizationAway_val, AlgHom.coe_comp,
      AlgEquiv.coe_algHom, Ideal.Quotient.mkₐ_eq_mk, Function.comp_apply]

Premises used: MvPolynomial.aeval_X, AlgHom.coe_comp, AlgEquiv.coe_algHom, Ideal.Quotient.mkₐ_eq_mk, Algebra.Generators.localizationAway_val, Function.comp_apply
-- 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
x : Unit
hf : Eq.{v + 1} (α := S) (invSelf r : S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) (X x) : S)
hf₁ hf₂ : Eq.{v + 1} (α := S) (invSelf r) (invSelf r)
⊢ Eq.{v + 1} (α := S) (invSelf r : S)
    ((mvPolynomialQuotientEquiv 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})
            (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})) :
      S)

Tactic:
rw [IsLocalization.Away.mvPolynomialQuotientEquiv_apply, aeval_X]

Premises used: MvPolynomial.aeval_X, IsLocalization.Away.mvPolynomialQuotientEquiv_apply
-- 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
⊢ 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})))

Tactic:
have : aeval (S₁ := S) (Generators.localizationAway S r).val =
      (mvPolynomialQuotientEquiv S r).toAlgHom.comp
        (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1})) := by
    ext x
    simp only [aeval_X, Generators.localizationAway_val, AlgHom.coe_comp,
      AlgEquiv.coe_algHom, Ideal.Quotient.mkₐ_eq_mk, Function.comp_apply]
    rw [IsLocalization.Away.mvPolynomialQuotientEquiv_apply, aeval_X]
-- 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})))
rw :
  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} →ₐ[R] S) :
          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})
⊢ Eq (α := Ideal (Generators.Ring (Generators.localizationAway S r))) (Generators.ker (Generators.localizationAway S 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 [Generators.ker_eq_ker_aeval_val, this, ← RingHom.ker_coe_toRingHom, AlgHom.comp_toRingHom,
    ← RingHom.comap_ker]

Premises used: AlgHom.comp_toRingHom, RingHom.comap_ker, RingHom.ker_coe_toRingHom, Algebra.Generators.ker_eq_ker_aeval_val
-- 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})))
⊢ 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})

Tactic:
simp [RingHom.ker_equiv, ← RingHom.ker_eq_comap_bot]

Premises used: RingHom.ker_equiv, RingHom.ker_eq_comap_bot
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
r : R
inst_3 : IsLocalization.Away r S
simp :
  Eq (α := Ideal (Generators.Ring (Generators.localizationAway S r)))
    (Ideal.span
      {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
            ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
          1})
    (Generators.ker (Generators.localizationAway S r))
⊢ Eq (α := Ideal (Generators.Ring (Generators.localizationAway S r)))
    (Ideal.span
      (Set.range fun (x : Unit) ↦
        HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
            ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
          1))
    (Generators.ker (Generators.localizationAway S r))

Tactic:
simp only [Set.range_const]

Premises used: Set.range_const
-- Module: Mathlib.RingTheory.Extension.Presentation.Basic
Goal:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Presentation R S ι σ
r : R
inst_3 : IsLocalization.Away r S
⊢ Eq (α := Ideal (Generators.Ring (Generators.localizationAway S r)))
    (Ideal.span
      {HMul.hMul (α := MvPolynomial Unit R) (β := MvPolynomial Unit R)
            ((C : (a : R) → MvPolynomial Unit R) r : MvPolynomial Unit R) (X ()) -
          1})
    (Generators.ker (Generators.localizationAway S r))

Tactic:
(Generators.ker_localizationAway r).symm

Premises used: Algebra.Generators.ker_localizationAway, Eq.symm