awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
ι : Type v
inst_4 : Finite ι
ι' : Type v
w : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective (α := MvPolynomial ι' R) (β := A) (⇑f : (a : MvPolynomial ι' R) → A)
hf_ker : Ideal.FG (RingHom.ker f.toRingHom)
g : MvPolynomial.{v, w₁} (ι ⊕ ι') R →ₐ[R] MvPolynomial ι A :=
  AlgHom.comp (MvPolynomial.mapAlgHom f)
    (↑(MvPolynomial.sumAlgEquiv R ι ι') : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι (MvPolynomial ι' R))
val : Fintype (ι ⊕ ι')
intro : Ideal.FG (R := MvPolynomial.{v, w₁} (ι ⊕ ι') R) ⊥
⊢ Ideal.FG
    (RingHom.ker (F := MvPolynomial.{v, w₁} (ι ⊕ ι') R →+* MvPolynomial ι (MvPolynomial ι' R))
      (↑(↑(MvPolynomial.sumAlgEquiv R ι ι') : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι (MvPolynomial ι' R)) :
        MvPolynomial (ι ⊕ ι') R →+* MvPolynomial ι (MvPolynomial ι' R)))

Tactic:
rw [AlgEquiv.toAlgHom_toRingHom, AlgHom.ker_coe_equiv]

Premises used: AlgEquiv.toAlgHom_toRingHom, AlgHom.ker_coe_equiv
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
ι : Type v
inst_4 : Finite ι
ι' : Type v
w : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective (α := MvPolynomial ι' R) (β := A) (⇑f : (a : MvPolynomial ι' R) → A)
hf_ker : Ideal.FG (RingHom.ker f.toRingHom)
g : MvPolynomial.{v, w₁} (ι ⊕ ι') R →ₐ[R] MvPolynomial ι A :=
  AlgHom.comp (MvPolynomial.mapAlgHom f)
    (↑(MvPolynomial.sumAlgEquiv R ι ι') : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι (MvPolynomial ι' R))
val : Fintype (ι ⊕ ι')
⊢ Ideal.FG (R := MvPolynomial.{v, w₁} (ι ⊕ ι') R) ⊥

Tactic:
Submodule.fg_bot

Premises used: Submodule.FG, Ideal.FG, Submodule.fg_bot
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
ι : Type v
inst_4 : Finite ι
ι' : Type v
w : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective (α := MvPolynomial ι' R) (β := A) (⇑f : (a : MvPolynomial ι' R) → A)
hf_ker : Ideal.FG (RingHom.ker f.toRingHom)
g : MvPolynomial.{v, w₁} (ι ⊕ ι') R →ₐ[R] MvPolynomial ι A :=
  AlgHom.comp (MvPolynomial.mapAlgHom f)
    (↑(MvPolynomial.sumAlgEquiv R ι ι') : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι (MvPolynomial ι' R))
val : Fintype (ι ⊕ ι')
⊢ Ideal.FG (R := MvPolynomial.{v, w₁} (ι ⊕ ι') R) ⊥

Tactic:
exact Submodule.fg_bot

Premises used: Submodule.fg_bot
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
ι : Type v
inst_4 : Finite ι
ι' : Type v
w : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective (α := MvPolynomial ι' R) (β := A) (⇑f : (a : MvPolynomial ι' R) → A)
hf_ker : Ideal.FG (RingHom.ker f.toRingHom)
g : MvPolynomial.{v, w₁} (ι ⊕ ι') R →ₐ[R] MvPolynomial ι A :=
  AlgHom.comp (MvPolynomial.mapAlgHom f)
    (↑(MvPolynomial.sumAlgEquiv R ι ι') : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι (MvPolynomial ι' R))
val : Fintype (ι ⊕ ι')
intro :
  Ideal.FG (R := MvPolynomial ι (MvPolynomial ι' R))
    (Ideal.map (F := MvPolynomial ι' R →+* MvPolynomial ι (MvPolynomial ι' R)) MvPolynomial.C
      (RingHom.ker (F := MvPolynomial ι' R →+* A) (↑f : MvPolynomial ι' R →+* A)))
⊢ Ideal.FG
    (RingHom.ker (F := MvPolynomial ι (MvPolynomial ι' R) →+* MvPolynomial ι A)
      (AlgHom.toRingHom (MvPolynomial.mapAlgHom f)))

Tactic:
rw [AlgHom.toRingHom_eq_coe, MvPolynomial.mapAlgHom_coe_ringHom, MvPolynomial.ker_map]

Premises used: MvPolynomial.ker_map, AlgHom.toRingHom_eq_coe, MvPolynomial.mapAlgHom_coe_ringHom
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
ι : Type v
inst_4 : Finite ι
ι' : Type v
w : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective (α := MvPolynomial ι' R) (β := A) (⇑f : (a : MvPolynomial ι' R) → A)
hf_ker : Ideal.FG (RingHom.ker f.toRingHom)
g : MvPolynomial.{v, w₁} (ι ⊕ ι') R →ₐ[R] MvPolynomial ι A :=
  AlgHom.comp (MvPolynomial.mapAlgHom f)
    (↑(MvPolynomial.sumAlgEquiv R ι ι') : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι (MvPolynomial ι' R))
val : Fintype (ι ⊕ ι')
⊢ Ideal.FG (R := MvPolynomial ι (MvPolynomial ι' R))
    (Ideal.map (F := MvPolynomial ι' R →+* MvPolynomial ι (MvPolynomial ι' R)) MvPolynomial.C
      (RingHom.ker (F := MvPolynomial ι' R →+* A) (↑f : MvPolynomial ι' R →+* A)))

Tactic:
hf_ker.map MvPolynomial.C

Premises used: Ideal.FG.map, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, MvPolynomial.C
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : FinitePresentation R A
ι : Type v
inst_4 : Finite ι
ι' : Type v
w : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective (α := MvPolynomial ι' R) (β := A) (⇑f : (a : MvPolynomial ι' R) → A)
hf_ker : Ideal.FG (RingHom.ker f.toRingHom)
g : MvPolynomial.{v, w₁} (ι ⊕ ι') R →ₐ[R] MvPolynomial ι A :=
  AlgHom.comp (MvPolynomial.mapAlgHom f)
    (↑(MvPolynomial.sumAlgEquiv R ι ι') : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι (MvPolynomial ι' R))
val : Fintype (ι ⊕ ι')
⊢ Ideal.FG (R := MvPolynomial ι (MvPolynomial ι' R))
    (Ideal.map (F := MvPolynomial ι' R →+* MvPolynomial ι (MvPolynomial ι' R)) MvPolynomial.C
      (RingHom.ker (F := MvPolynomial ι' R →+* A) (↑f : MvPolynomial ι' R →+* A)))

Tactic:
exact hf_ker.map MvPolynomial.C

Premises used: Ideal.FG.map, MvPolynomial.C
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FinitePresentation R A
inst_8 : FinitePresentation A B
⊢ FinitePresentation A B

Tactic:
have hfpB : FinitePresentation A B := inferInstance
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FinitePresentation R A
inst_8 hfpB : FinitePresentation A B
obtain :
  ∀ (n : ℕ) (I : Ideal (MvPolynomial (Fin n) A)) (e : (MvPolynomial (Fin n) A ⧸ I) ≃ₐ[A] B) (hfg : I.FG),
    FinitePresentation R B
⊢ FinitePresentation R B

Tactic:
obtain ⟨n, I, e, hfg⟩ := iff.1 hfpB

Premises used: Algebra.FinitePresentation.iff, Iff.mp
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FinitePresentation R A
inst_8 hfpB : FinitePresentation A B
n : ℕ
I : Ideal (MvPolynomial (Fin n) A)
e : (MvPolynomial (Fin n) A ⧸ I) ≃ₐ[A] B
hfg : I.FG
this : FinitePresentation.{w₁, w₂} R (MvPolynomial (Fin n) A ⧸ I) := ⋯
⊢ FinitePresentation R B

Tactic:
equiv (e.restrictScalars R)

Premises used: Algebra.FinitePresentation.equiv, AlgEquiv.restrictScalars
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FinitePresentation R A
inst_8 hfpB : FinitePresentation A B
n : ℕ
I : Ideal (MvPolynomial (Fin n) A)
e : (MvPolynomial (Fin n) A ⧸ I) ≃ₐ[A] B
hfg : I.FG
this : FinitePresentation.{w₁, w₂} R (MvPolynomial (Fin n) A ⧸ I) := ⋯
⊢ FinitePresentation R B

Tactic:
exact equiv (e.restrictScalars R)

Premises used: Algebra.FinitePresentation.equiv, AlgEquiv.restrictScalars
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
ι : Type u_1
inst_6 : Finite ι
⊢ FinitePresentation R (MvPolynomial ι A)

Tactic:
have := FinitePresentation.mvPolynomial_aux A ι; .trans _ A _

Premises used: _private.0.Algebra.FinitePresentation.mvPolynomial_aux, MvPolynomial, Algebra.FinitePresentation.trans
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
⊢ FinitePresentation R R

Tactic:
have := FinitePresentation.mvPolynomial_aux R Empty
  equiv (MvPolynomial.isEmptyAlgEquiv R Empty)

Premises used: Algebra.FinitePresentation.equiv, _private.0.Algebra.FinitePresentation.mvPolynomial_aux, MvPolynomial.isEmptyAlgEquiv, Empty
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
⊢ FinitePresentation.{w₁, w₂} R A[X]

Tactic:
letI := FinitePresentation.mvPolynomial R A Unit
  have := equiv (MvPolynomial.uniqueAlgEquiv.{_, 0} A PUnit)
  .trans _ A _

Premises used: Algebra.FinitePresentation.equiv, MvPolynomial.uniqueAlgEquiv, Polynomial, PUnit, Algebra.FinitePresentation.trans
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FinitePresentation R B
inst_8 : FiniteType R A
obtain :
  ∀ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] B)
    (hf : Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B) (⇑f : (a : MvPolynomial (Fin n) R) → B))
    (s : Finset (MvPolynomial (Fin n) R))
    (hs :
      Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin n) R)))
        (RingHom.ker f.toRingHom)),
    FinitePresentation A B
⊢ FinitePresentation A B

Tactic:
obtain ⟨n, f, hf, s, hs⟩ := FinitePresentation.out (R := R) (A := B)

Premises used: Algebra.FinitePresentation.out
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FinitePresentation R B
inst_8 : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B) (⇑f : (a : MvPolynomial (Fin n) R) → B)
s : Finset (MvPolynomial (Fin n) R)
hs : Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin n) R))) (RingHom.ker f.toRingHom)
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
⊢ FinitePresentation A B

Tactic:
⟨n, MvPolynomial.aeval (f ∘ X), ?_, ?_⟩

Premises used: MvPolynomial.aeval, MvPolynomial.X, Function.comp, Algebra.FinitePresentation.mk, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FinitePresentation R B
inst_8 : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B) (⇑f : (a : MvPolynomial (Fin n) R) → B)
s : Finset (MvPolynomial (Fin n) R)
hs : Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin n) R))) (RingHom.ker f.toRingHom)
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
refine_1 :
  Surjective.{w₂ + 1, w₃ + 1} (α := MvPolynomial (Fin n) A) (β := B)
    (⇑(MvPolynomial.aeval
          (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
            MvPolynomial.X)) :
      (a : MvPolynomial (Fin n) A) → B)
refine_2 :
  Ideal.FG
    (RingHom.ker (F := RingHom.{w₂, w₃} (MvPolynomial (Fin n) A) B)
      (AlgHom.toRingHom
        (MvPolynomial.aeval
          (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
            MvPolynomial.X))))
⊢ FinitePresentation A B

Tactic:
refine ⟨n, MvPolynomial.aeval (f ∘ X), ?_, ?_⟩
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FinitePresentation R B
inst_8 : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B) (⇑f : (a : MvPolynomial (Fin n) R) → B)
s : Finset (MvPolynomial (Fin n) R)
hs : Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin n) R))) (RingHom.ker f.toRingHom)
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
refine_1 : ∀ (x : B), Membership.mem (γ := Subalgebra A B) (adjoin A (↑⊤ : Set B)) x
⊢ Surjective.{w₂ + 1, w₃ + 1} (α := MvPolynomial (Fin n) A) (β := B)
    (⇑(MvPolynomial.aeval
          (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
            MvPolynomial.X)) :
      (a : MvPolynomial (Fin n) A) → B)

Tactic:
rw [← AlgHom.range_eq_top, ← Algebra.adjoin_range_eq_range_aeval,
      Set.range_comp f MvPolynomial.X, eq_top_iff, ← @adjoin_adjoin_of_tower R A B,
      adjoin_image, adjoin_range_X, Algebra.map_top, (AlgHom.range_eq_top _).mpr hf]

Premises used: Iff.mpr, Set.range_comp, Algebra.adjoin_adjoin_of_tower, MvPolynomial.adjoin_range_X, MvPolynomial.X, AlgHom.range_eq_top, Algebra.adjoin_range_eq_range_aeval, Algebra.adjoin_image, Algebra.eq_top_iff, Algebra.map_top, DFunLike.coe
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FinitePresentation R B
inst_8 : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B) (⇑f : (a : MvPolynomial (Fin n) R) → B)
s : Finset (MvPolynomial (Fin n) R)
hs : Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin n) R))) (RingHom.ker f.toRingHom)
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
⊢ ∀ (x : B), Membership.mem (γ := Subalgebra A B) (adjoin A (↑⊤ : Set B)) x

Tactic:
fun {x} => subset_adjoin ⟨⟩

Premises used: Algebra.subset_adjoin, True.intro
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FinitePresentation R B
inst_8 : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B) (⇑f : (a : MvPolynomial (Fin n) R) → B)
s : Finset (MvPolynomial (Fin n) R)
hs : Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin n) R))) (RingHom.ker f.toRingHom)
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
⊢ ∀ (x : B), Membership.mem (γ := Subalgebra A B) (adjoin A (↑⊤ : Set B)) x

Tactic:
exact fun {x} => subset_adjoin ⟨⟩
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FinitePresentation R B
inst_8 : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B) (⇑f : (a : MvPolynomial (Fin n) R) → B)
s : Finset (MvPolynomial (Fin n) R)
hs : Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin n) R))) (RingHom.ker f.toRingHom)
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
refine_2 :
  ∀ (t : Finset A) (ht : Eq (α := Subalgebra R A) (adjoin R (↑t : Set A)) ⊤),
    Ideal.FG
      (RingHom.ker (F := RingHom.{w₂, w₃} (MvPolynomial (Fin n) A) B)
        (AlgHom.toRingHom
          (MvPolynomial.aeval
            (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
              MvPolynomial.X))))
⊢ Ideal.FG
    (RingHom.ker (F := RingHom.{w₂, w₃} (MvPolynomial (Fin n) A) B)
      (AlgHom.toRingHom
        (MvPolynomial.aeval
          (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
            MvPolynomial.X))))

Tactic:
obtain ⟨t, ht⟩ := FiniteType.out (R := R) (A := A)

Premises used: Algebra.FiniteType.out
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FinitePresentation R B
inst_8 : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B) (⇑f : (a : MvPolynomial (Fin n) R) → B)
s : Finset (MvPolynomial (Fin n) R)
hs : Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin n) R))) (RingHom.ker f.toRingHom)
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : Eq (α := Subalgebra R A) (adjoin R (↑t : Set A)) ⊤
⊢ ∀ (i : ↥t),
    ∃ (a : MvPolynomial (Fin n) R),
      Eq.{w₃ + 1} (α := B) ((f : (a : MvPolynomial (Fin n) R) → B) a : B) ((algebraMap A B : (a : A) → B) (↑i : A) : B)

Tactic:
have := fun i : t => hf (algebraMap A B i)
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FinitePresentation R B
inst_8 : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B) (⇑f : (a : MvPolynomial (Fin n) R) → B)
s : Finset (MvPolynomial (Fin n) R)
hs : Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin n) R))) (RingHom.ker f.toRingHom)
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : Eq (α := Subalgebra R A) (adjoin R (↑t : Set A)) ⊤
this :
  ∀ (i : ↥t),
    ∃ (a : MvPolynomial (Fin n) R),
      Eq.{w₃ + 1} (α := B) ((f : (a : MvPolynomial (Fin n) R) → B) a : B) ((algebraMap A B : (a : A) → B) (↑i : A) : B)
refine_2 :
  ∀ (t' : (i : ↥t) → MvPolynomial (Fin n) R)
    (ht' :
      ∀ (i : ↥t),
        Eq.{w₃ + 1} (α := B) ((f : (a : MvPolynomial (Fin n) R) → B) (t' i) : B)
          ((algebraMap A B : (a : A) → B) (↑i : A) : B)),
    Ideal.FG
      (RingHom.ker (F := RingHom.{w₂, w₃} (MvPolynomial (Fin n) A) B)
        (AlgHom.toRingHom
          (MvPolynomial.aeval
            (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
              MvPolynomial.X))))
⊢ Ideal.FG
    (RingHom.ker (F := RingHom.{w₂, w₃} (MvPolynomial (Fin n) A) B)
      (AlgHom.toRingHom
        (MvPolynomial.aeval
          (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
            MvPolynomial.X))))

Tactic:
choose t' ht' using this
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FinitePresentation R B
inst_8 : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B) (⇑f : (a : MvPolynomial (Fin n) R) → B)
s : Finset (MvPolynomial (Fin n) R)
hs : Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin n) R))) (RingHom.ker f.toRingHom)
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : Eq (α := Subalgebra R A) (adjoin R (↑t : Set A)) ⊤
t' : (i : ↥t) → MvPolynomial (Fin n) R
ht' :
  ∀ (i : ↥t),
    Eq.{w₃ + 1} (α := B) ((f : (a : MvPolynomial (Fin n) R) → B) (t' i) : B)
      ((algebraMap A B : (a : A) → B) (↑i : A) : B)
rw :
  Eq.{w₂ + 1} (α := Subalgebra R AX)
    (Subalgebra.restrictScalars R (S := ↥(adjoin R ((⇑(algebraMap A AX) : (a : A) → AX) '' (↑t : Set A))))
      (adjoin (↥(adjoin R ((⇑(algebraMap A AX) : (a : A) → AX) '' (↑t : Set A)))) (Set.range MvPolynomial.X)))
    (Subalgebra.restrictScalars R (S := ↥(adjoin R ((⇑(algebraMap A AX) : (a : A) → AX) '' (↑t : Set A)))) ⊤)
⊢ Eq (α := Subalgebra R AX) (adjoin R ((⇑(algebraMap A AX) : (a : A) → AX) '' (↑t : Set A) ∪ Set.range MvPolynomial.X))
    ⊤

Tactic:
rw [adjoin_union_eq_adjoin_adjoin, ← Subalgebra.restrictScalars_top R (A := AX)
        (S := { x // x ∈ adjoin R ((algebraMap A AX) '' t) })]

Premises used: Algebra.adjoin_union_eq_adjoin_adjoin, Subalgebra.restrictScalars_top
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FinitePresentation R B
inst_8 : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B) (⇑f : (a : MvPolynomial (Fin n) R) → B)
s : Finset (MvPolynomial (Fin n) R)
hs : Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin n) R))) (RingHom.ker f.toRingHom)
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : Eq (α := Subalgebra R A) (adjoin R (↑t : Set A)) ⊤
t' : (i : ↥t) → MvPolynomial (Fin n) R
ht' :
  ∀ (i : ↥t),
    Eq.{w₃ + 1} (α := B) ((f : (a : MvPolynomial (Fin n) R) → B) (t' i) : B)
      ((algebraMap A B : (a : A) → B) (↑i : A) : B)
⊢ Eq.{w₂ + 1} (α := Subalgebra R AX)
    (Subalgebra.restrictScalars R (S := ↥(adjoin R ((⇑(algebraMap A AX) : (a : A) → AX) '' (↑t : Set A))))
      (adjoin (↥(adjoin R ((⇑(algebraMap A AX) : (a : A) → AX) '' (↑t : Set A)))) (Set.range MvPolynomial.X)))
    (Subalgebra.restrictScalars R (S := ↥(adjoin R ((⇑(algebraMap A AX) : (a : A) → AX) '' (↑t : Set A)))) ⊤)

Tactic:
congrArg (Subalgebra.restrictScalars R) ?_

Premises used: congrArg, Set.Mem, setOf, Subalgebra.restrictScalars