awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Extension.Generators
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 (α := T) ((algebraMap T T : (a : T) → T) ((aeval (val (Q.comp P)) : (a : MvPolynomial (ι' ⊕ ι) R) → T) x : T) : T)
    (0 : T)
⊢ Membership.mem (γ := Submodule (Generators.Ring (Q.comp P)) (Generators.Ring (Q.comp P))) (ker (Q.comp P)) x

Tactic:
rw [Generators.ker_eq_ker_aeval_val, RingHom.mem_ker,
    ← algebraMap_self_apply (MvPolynomial.aeval _ x)]

Premises used: Algebra.algebraMap_self_apply, MvPolynomial.aeval, RingHom.mem_ker, Algebra.Generators.ker_eq_ker_aeval_val, DFunLike.coe
-- Module: Mathlib.RingTheory.Extension.Generators
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)
rw₂ rw₃ : Eq.{u_7 + 1} (α := T) 0 0
⊢ Eq (α := T) ((algebraMap T T : (a : T) → T) ((aeval (val (Q.comp P)) : (a : MvPolynomial (ι' ⊕ ι) R) → T) x : T) : T)
    (0 : T)

Tactic:
rw [← Generators.Hom.algebraMap_toAlgHom (Q.ofComp P), hx, map_zero]

Premises used: map_zero, Algebra.Generators.ofComp, Algebra.Generators.Hom.algebraMap_toAlgHom
-- Module: Mathlib.RingTheory.Extension.Generators
Goal:
R : Type u
S : Type v
ι : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Generators R S ι
T : Type u_7
inst_3 : CommRing T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
g : S
inst_7 : IsLocalization.Away g T
⊢ (Hom.toAlgHom (ofComp (localizationAway T g) P) :
        (a : ((localizationAway T g).comp P).Ring) → (localizationAway T g).Ring)
      (HMul.hMul (α := MvPolynomial.{w, u} (Unit ⊕ ι) R) (β := MvPolynomial.{w, u} (Unit ⊕ ι) R)
          ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R) (P.σ g) :
            MvPolynomial.{w, u} (Unit ⊕ ι) R)
          (X (Sum.inl ())) -
        1) =
    HMul.hMul (α := MvPolynomial Unit S) (β := MvPolynomial Unit S)
        ((C : (a : S) → MvPolynomial Unit S) g : MvPolynomial Unit S) (X ()) -
      1

Tactic:
simp [Generators.Hom.toAlgHom, Generators.ofComp, aeval_rename]

Premises used: Algebra.Generators.Hom.toAlgHom, Algebra.Generators.ofComp, MvPolynomial.aeval_rename
-- 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 ι σ
i : σ
rw : Membership.mem (γ := Ideal (MvPolynomial ι R)) (Ideal.span (Set.range P.relation)) (P.relation i)
⊢ Eq.{v + 1} (α := S) ((aeval P.val : (a : MvPolynomial ι R) → S) (P.relation i) : S) (0 : S)

Tactic:
rw [← RingHom.mem_ker, ← P.ker_eq_ker_aeval_val, ← P.span_range_relation_eq_ker]

Premises used: RingHom.mem_ker, Algebra.Presentation.span_range_relation_eq_ker, Algebra.Generators.ker_eq_ker_aeval_val, Algebra.Presentation.toGenerators
-- 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 ι σ
i : σ
⊢ Membership.mem (γ := Ideal (MvPolynomial ι R)) (Ideal.span (Set.range P.relation)) (P.relation i)

Tactic:
Ideal.subset_span ⟨i, rfl⟩

Premises used: Ideal.subset_span, Set.Mem, setOf, Exists.intro, 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 ι σ
i : σ
⊢ Membership.mem (γ := Ideal (MvPolynomial ι R)) (Ideal.span (Set.range P.relation)) (P.relation i)

Tactic:
exact Ideal.subset_span ⟨i, 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 ι σ
i : σ
rw : Membership.mem (γ := Ideal P.Ring) (Ideal.span (Set.range P.relation)) (P.relation i)
⊢ P.relation i ∈ P.ker

Tactic:
rw [← 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 ι σ
i : σ
a : P.relation i ∈ Set.range P.relation
⊢ Membership.mem (γ := Ideal P.Ring) (Ideal.span (Set.range P.relation)) (P.relation i)

Tactic:
apply Ideal.subset_span

Premises used: Ideal.subset_span
-- 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 ι σ
i w : σ
h : P.relation i = P.relation i
⊢ P.relation i ∈ Set.range P.relation

Tactic:
use i
-- 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 ι σ
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
rw₂ rw₃ : x = x
⊢ (ofId P.Ring S : (a : P.Ring) → S) (P.σ x) = x

Tactic:
rw [Algebra.ofId_apply, P.algebraMap_apply, P.aeval_val_σ]

Premises used: Algebra.Generators.algebraMap_apply, Algebra.Generators.aeval_val_σ, Algebra.ofId_apply, Algebra.Presentation.toGenerators
-- 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 ι σ
p : P.Ring
⊢ Eq.{v + 1} (α := S)
    ((P.quotientEquiv : (a : P.Quotient) → S)
        ((Ideal.Quotient.mk P.ker : (a : P.Ring) → P.Ring ⧸ P.ker) p : P.Ring ⧸ P.ker) :
      S)
    ((algebraMap P.Ring S : (a : P.Ring) → S) p : S)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, 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 ι σ
x : S
⊢ Eq (α := P.Quotient) ((P.quotientEquiv.symm : (a : S) → P.Quotient) x : P.Quotient)
    ((Ideal.Quotient.mk P.ker : (a : P.Ring) → P.Ring ⧸ P.ker) (P.σ x) : P.Ring ⧸ P.ker)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, AddMonoidAlgebra, 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 ι σ
inst_3 : Finite σ
h : Ideal.span (↑(⋯.toFinset (s := Set.range P.relation)) : Set P.Ring) = P.ker
⊢ P.ker.FG

Tactic:
use (Set.finite_range P.relation).toFinset

Premises used: Set.finite_range, Algebra.Presentation.relation, Set.Finite.toFinset
-- 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 ι σ
inst_3 : Finite σ
⊢ Ideal.span (↑(⋯.toFinset (s := Set.range P.relation)) : Set P.Ring) = P.ker

Tactic:
simp [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 ι σ
inst_3 : Finite σ
inst_4 : Finite ι
⊢ FinitePresentation R P.Quotient

Tactic:
FinitePresentation.quotient P.fg_ker

Premises used: Algebra.Presentation.fg_ker, Algebra.FinitePresentation.quotient
-- 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
inst_3 : Finite σ
inst_4 : Finite ι
P : Presentation R S ι σ
⊢ FinitePresentation R S

Tactic:
FinitePresentation.equiv (P.quotientEquiv.restrictScalars R)

Premises used: Algebra.FinitePresentation.equiv, AlgEquiv.restrictScalars, Algebra.Presentation.quotientEquiv
-- 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)
⊢ Function.Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)

Tactic:
hf
-- 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)
h : (aeval fun (x : Fin n) ↦ (f : (a : MvPolynomial (Fin n) R) → S) (X x)) = 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)

Tactic:
convert! hf
-- 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)
h :
  ∀ (i : Fin n),
    Eq.{v + 1} (α := 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 : (a : MvPolynomial (Fin n) R) → S) (X i) : S)
⊢ (aeval fun (x : Fin n) ↦ (f : (a : MvPolynomial (Fin n) R) → S) (X x)) = f

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)
    ((aeval fun (x : Fin n) ↦ (f : (a : MvPolynomial (Fin n) R) → S) (X x) : (a : MvPolynomial (Fin n) R) → S) (X i) :
      S)
    ((f : (a : MvPolynomial (Fin n) R) → S) (X i) : S)

Tactic:
simp
-- 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 : f = aeval fun (x : Fin n) ↦ (f : (a : MvPolynomial (Fin n) R) → S) (X x)
⊢ RingHom.ker f =
    Generators.ker (Generators.ofSurjective (fun (x : Fin n) ↦ (f : (a : MvPolynomial (Fin n) R) → S) (X x)) ⋯)

Tactic:
congr