awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_3
T : Type u_7
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
x : Generators.Ring (Q.comp P)
hx : Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) (0 : Q.Ring)
rw :
  Eq.{u_7 + 1} (α := T)
    ((aeval Q.val : (a : MvPolynomial ι' S) → T)
        ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) :
      T)
    (0 : T)
⊢ Eq (α := T) ((algebraMap T T : (a : T) → T) ((aeval (val (Q.comp P)) : (a : MvPolynomial (ι' ⊕ ι) R) → T) x : T) : T)
    (0 : T)
have rw₁ : Eq.{u_7 + 1} (α := T) ((aeval Q.val : (a : MvPolynomial ι' S) → T) 0 : T) (0 : T)
Tactic: rw [← Generators.Hom.algebraMap_toAlgHom (Q.ofComp P), hx, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Generators (goal)
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι' : Type u_3
T : Type u_7
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
x : Generators.Ring (Q.comp P)
hx : Eq (α := Q.Ring) ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) (0 : Q.Ring)
rw :
  Eq.{u_7 + 1} (α := T)
    ((aeval Q.val : (a : MvPolynomial ι' S) → T)
        ((Hom.toAlgHom (Q.ofComp P) : (a : (Q.comp P).Ring) → Q.Ring) x : Q.Ring) :
      T)
    (0 : T)
rw₁ : Eq.{u_7 + 1} (α := T) ((aeval Q.val : (a : MvPolynomial ι' S) → T) 0 : T) (0 : T)
⊢ Eq (α := T) ((algebraMap T T : (a : T) → T) ((aeval (val (Q.comp P)) : (a : MvPolynomial (ι' ⊕ ι) R) → T) x : T) : T)
    (0 : T)
have rw₂ : Eq.{u_7 + 1} (α := T) 0 0
Tactic: rw [← Generators.Hom.algebraMap_toAlgHom (Q.ofComp P), hx, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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 ι σ
i : σ
⊢ Eq.{v + 1} (α := S) ((aeval P.val : (a : MvPolynomial ι R) → S) (P.relation i) : S) (0 : S)
have rw : Membership.mem (γ := Ideal (MvPolynomial ι R)) (Ideal.span (Set.range P.relation)) (P.relation i)
Tactic: rw [← RingHom.mem_ker, ← P.ker_eq_ker_aeval_val, ← P.span_range_relation_eq_ker]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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 ι σ
i : σ
⊢ P.relation i ∈ P.ker
have rw : Membership.mem (γ := Ideal P.Ring) (Ideal.span (Set.range P.relation)) (P.relation i)
Tactic: rw [← P.span_range_relation_eq_ker]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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 ι σ
i : σ
⊢ Membership.mem (γ := Ideal P.Ring) (Ideal.span (Set.range P.relation)) (P.relation i)
have a : P.relation i ∈ Set.range P.relation
Tactic: apply Ideal.subset_span
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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 ι σ
i w : σ
⊢ P.relation i ∈ Set.range P.relation
have h : P.relation i = P.relation i
Tactic: use i
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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 ι σ
x : S
⊢ (ofId P.Ring S : (a : P.Ring) → S) (P.σ x) = x
have rw : (algebraMap P.Ring S : (a : P.Ring) → S) (P.σ x) = x
Tactic: rw [Algebra.ofId_apply, P.algebraMap_apply, P.aeval_val_σ]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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 ι σ
x : S
rw : (algebraMap P.Ring S : (a : P.Ring) → S) (P.σ x) = x
⊢ (ofId P.Ring S : (a : P.Ring) → S) (P.σ x) = x
have rw₁ : (aeval P.val : (a : MvPolynomial ι R) → S) (P.σ x) = x
Tactic: rw [Algebra.ofId_apply, P.algebraMap_apply, P.aeval_val_σ]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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 ι σ
x : S
rw : (algebraMap P.Ring S : (a : P.Ring) → S) (P.σ x) = x
rw₁ : (aeval P.val : (a : MvPolynomial ι R) → S) (P.σ x) = x
⊢ (ofId P.Ring S : (a : P.Ring) → S) (P.σ x) = x
have rw₂ : x = x
Tactic: rw [Algebra.ofId_apply, P.algebraMap_apply, P.aeval_val_σ]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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 ι σ
inst_3 : Finite σ
⊢ P.ker.FG
have h : Ideal.span (↑(sorry.toFinset (s := Set.range P.relation)) : Set P.Ring) = P.ker
Tactic: use (Set.finite_range P.relation).toFinset
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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)
⊢ Function.Surjective.{max (u + 1) 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S)
    (⇑(aeval fun (x : Fin n) ↦ (f : (a : MvPolynomial (Fin n) R) → S) (X x)) : (a : MvPolynomial (Fin n) R) → S)
have h : (aeval fun (x : Fin n) ↦ (f : (a : MvPolynomial (Fin n) R) → S) (X x)) = f
Tactic: convert! hf
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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)
⊢ RingHom.ker f =
    Generators.ker (Generators.ofSurjective (fun (x : Fin n) ↦ (f : (a : MvPolynomial (Fin n) R) → S) (X x)) ⋯)
have e_f : f = aeval fun (x : Fin n) ↦ (f : (a : MvPolynomial (Fin n) R) → S) (X x)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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)
⊢ Ideal.span (Set.range PEmpty.elim) = (Generators.ofSurjectiveAlgebraMap ⋯).ker
have simp : ⊥ = (Generators.ofSurjectiveAlgebraMap sorry).ker
Tactic: simp only [Set.range_eq_empty, Ideal.span_empty]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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)
⊢ ⊥ = (Generators.ofSurjectiveAlgebraMap ⋯).ker
have symm : (Generators.ofSurjectiveAlgebraMap sorry).ker = ⊥
Tactic: symm
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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)
⊢ (Generators.ofSurjectiveAlgebraMap ⋯).ker = ⊥
have rw : Function.Injective (α := (Generators.ofSurjectiveAlgebraMap sorry).toExtension.Ring) (β := S)
  (⇑(algebraMap (Generators.ofSurjectiveAlgebraMap sorry).toExtension.Ring S) :
    (a : (Generators.ofSurjectiveAlgebraMap sorry).toExtension.Ring) → S)
Tactic: rw [← RingHom.injective_iff_ker_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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 (α := (Generators.ofSurjectiveAlgebraMap ⋯).toExtension.Ring) (β := S)
    (⇑(algebraMap (Generators.ofSurjectiveAlgebraMap ⋯).toExtension.Ring S) :
      (a : (Generators.ofSurjectiveAlgebraMap ⋯).toExtension.Ring) → S)
have change : Function.Injective (α := MvPolynomial PEmpty.{w + 1} R) (β := S)
  (⇑(aeval PEmpty.elim) : (a : MvPolynomial PEmpty.{w + 1} R) → S)
Tactic: change Function.Injective (aeval PEmpty.elim)
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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 (α := MvPolynomial PEmpty.{w + 1} R) (β := S)
    (⇑(aeval PEmpty.elim) : (a : MvPolynomial PEmpty.{w + 1} R) → S)
have rw : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
Tactic: rw [aeval_injective_iff_of_isEmpty]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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})))
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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
⊢ 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)
have 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)
Tactic: simp only [aeval_X, Generators.localizationAway_val, AlgHom.coe_comp,
      AlgEquiv.coe_algHom, Ideal.Quotient.mkₐ_eq_mk, Function.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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
⊢ 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)
have hf : Eq.{v + 1} (α := S) (invSelf r : S) ((aeval fun (x : Unit) ↦ invSelf r : (a : MvPolynomial Unit R) → S) (X x) : S)
Tactic: rw [IsLocalization.Away.mvPolynomialQuotientEquiv_apply, aeval_X]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (goal)
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)
⊢ 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)
have hf₁ : Eq.{v + 1} (α := S) (invSelf r) (invSelf r)
Tactic: rw [IsLocalization.Away.mvPolynomialQuotientEquiv_apply, aeval_X]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Basic (hypothesis)
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 (α := 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})
have 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})))
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]