awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
mp :
  FinitePresentation R A →
    ∃ (ι : Type u_1) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] A),
      Surjective (α := MvPolynomial ι R) (β := A) (⇑f : (a : MvPolynomial ι R) → A) ∧ Ideal.FG (RingHom.ker f.toRingHom)
⊢ FinitePresentation R A ↔
    ∃ (ι : Type u_1) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] A),
      Surjective (α := MvPolynomial ι R) (β := A) (⇑f : (a : MvPolynomial ι R) → A) ∧ Ideal.FG (RingHom.ker f.toRingHom)
have mpr : (∃ (ι : Type u_1) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] A),
    Surjective (α := MvPolynomial ι R) (β := A) (⇑f : (a : MvPolynomial ι R) → A) ∧
      Ideal.FG (RingHom.ker f.toRingHom)) →
  FinitePresentation R A
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hfs : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
hfk : Ideal.FG (RingHom.ker f.toRingHom)
ulift_var : MvPolynomial.{u_1, w₁} (ULift.{u_1, 0} (Fin n)) R ≃ₐ[R] MvPolynomial (Fin n) R :=
  MvPolynomial.renameEquiv R Equiv.ulift
⊢ ∃ (ι : Type u_1) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] A),
    Surjective (α := MvPolynomial ι R) (β := A) (⇑f : (a : MvPolynomial ι R) → A) ∧ Ideal.FG (RingHom.ker f.toRingHom)
have mp : Ideal.FG
  (RingHom.ker (F := MvPolynomial.{u_1, w₁} (ULift.{u_1, 0} (Fin n)) R →+* MvPolynomial (Fin n) R)
    (↑(↑ulift_var : MvPolynomial (ULift.{u_1, 0} (Fin n)) R →ₐ[R] MvPolynomial (Fin n) R) :
      MvPolynomial (ULift.{u_1, 0} (Fin n)) R →+* MvPolynomial (Fin n) R))
Tactic: refine
      ⟨ULift (Fin n), inferInstance, f.comp ulift_var.toAlgHom, hfs.comp ulift_var.surjective,
        Ideal.fg_ker_comp _ _ ?_ hfk ulift_var.surjective⟩
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
ι : Type u_1
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] A
hf : Surjective (α := MvPolynomial ι R) (β := A) (⇑f : (a : MvPolynomial ι R) → A) ∧ Ideal.FG (RingHom.ker f.toRingHom)
⊢ FinitePresentation R A
have mpr : ∀ (equiv : MvPolynomial ι R ≃ₐ[R] MvPolynomial (Fin (Fintype.card ι)) R), FinitePresentation R A
Tactic: have equiv := MvPolynomial.renameEquiv R (Fintype.equivFin ι)
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
ι : Type u_1
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] A
hf : Surjective (α := MvPolynomial ι R) (β := A) (⇑f : (a : MvPolynomial ι R) → A) ∧ Ideal.FG (RingHom.ker f.toRingHom)
equiv : MvPolynomial ι R ≃ₐ[R] MvPolynomial (Fin (Fintype.card ι)) R
⊢ FinitePresentation R A
have right : Ideal.FG (RingHom.ker (f.comp (↑equiv.symm : MvPolynomial (Fin (Fintype.card ι)) R →ₐ[R] MvPolynomial ι R)).toRingHom)
Tactic: use Fintype.card ι, f.comp equiv.symm, hf.1.comp (AlgEquiv.symm equiv).surjective
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
ι : Type u_1
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] A
hf : Surjective (α := MvPolynomial ι R) (β := A) (⇑f : (a : MvPolynomial ι R) → A) ∧ Ideal.FG (RingHom.ker f.toRingHom)
equiv : MvPolynomial ι R ≃ₐ[R] MvPolynomial (Fin (Fintype.card ι)) R
⊢ Ideal.FG (RingHom.ker (f.comp (↑equiv.symm : MvPolynomial (Fin (Fintype.card ι)) R →ₐ[R] MvPolynomial ι R)).toRingHom)
have right : Ideal.FG
  (RingHom.ker (F := MvPolynomial (Fin (Fintype.card ι)) R →+* MvPolynomial ι R)
    (↑(↑equiv.symm : MvPolynomial (Fin (Fintype.card ι)) R →ₐ[R] MvPolynomial ι R) :
      MvPolynomial (Fin (Fintype.card ι)) R →+* MvPolynomial ι R))
Tactic: refine Ideal.fg_ker_comp (S := MvPolynomial ι R) (A := A) _ f ?_ hf.2 equiv.symm.surjective
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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 ι
hfp : FinitePresentation R A
⊢ FinitePresentation R (MvPolynomial ι A)
have rw : ∀
  (hfp :
    ∃ (ι : Type v) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] A),
      Surjective (α := MvPolynomial ι R) (β := A) (⇑f : (a : MvPolynomial ι R) → A) ∧
        Ideal.FG (RingHom.ker f.toRingHom)),
  ∃ (ι_1 : Type v) (x : Fintype ι_1) (f : MvPolynomial ι_1 R →ₐ[R] MvPolynomial ι A),
    Surjective (α := MvPolynomial ι_1 R) (β := MvPolynomial ι A) (⇑f : (a : MvPolynomial ι_1 R) → MvPolynomial ι A) ∧
      Ideal.FG (RingHom.ker f.toRingHom)
Tactic: rw [iff_quotient_mvPolynomial'] at hfp ⊢
Cleared hypotheses: hfp
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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 ι
hfp :
  ∃ (ι : Type v) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] A),
    Surjective (α := MvPolynomial ι R) (β := A) (⇑f : (a : MvPolynomial ι R) → A) ∧ Ideal.FG (RingHom.ker f.toRingHom)
⊢ ∃ (ι_1 : Type v) (x : Fintype ι_1) (f : MvPolynomial ι_1 R →ₐ[R] MvPolynomial ι A),
    Surjective (α := MvPolynomial ι_1 R) (β := MvPolynomial ι A) (⇑f : (a : MvPolynomial ι_1 R) → MvPolynomial ι A) ∧
      Ideal.FG (RingHom.ker f.toRingHom)
have obtain : ∀ (ι' : 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)),
  ∃ (ι_1 : Type v) (x : Fintype ι_1) (f : MvPolynomial ι_1 R →ₐ[R] MvPolynomial ι A),
    Surjective (α := MvPolynomial ι_1 R) (β := MvPolynomial ι A) (⇑f : (a : MvPolynomial ι_1 R) → MvPolynomial ι A) ∧
      Ideal.FG (RingHom.ker f.toRingHom)
Tactic: obtain ⟨(ι' : Type v), _, f, hf_surj, hf_ker⟩ := hfp
Cleared hypotheses: hfp
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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))
⊢ ∃ (ι_1 : Type v) (x : Fintype ι_1) (f : MvPolynomial ι_1 R →ₐ[R] MvPolynomial ι A),
    Surjective (α := MvPolynomial ι_1 R) (β := MvPolynomial ι A) (⇑f : (a : MvPolynomial ι_1 R) → MvPolynomial ι A) ∧
      Ideal.FG (RingHom.ker f.toRingHom)
have intro : ∀ (val : Fintype (ι ⊕ ι')),
  ∃ (ι_1 : Type v) (x : Fintype ι_1) (f : MvPolynomial ι_1 R →ₐ[R] MvPolynomial ι A),
    Surjective (α := MvPolynomial ι_1 R) (β := MvPolynomial ι A) (⇑f : (a : MvPolynomial ι_1 R) → MvPolynomial ι A) ∧
      Ideal.FG (RingHom.ker f.toRingHom)
Tactic: cases nonempty_fintype (ι ⊕ ι')
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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 (ι ⊕ ι')
⊢ ∃ (ι_1 : Type v) (x : Fintype ι_1) (f : MvPolynomial ι_1 R →ₐ[R] MvPolynomial ι A),
    Surjective (α := MvPolynomial ι_1 R) (β := MvPolynomial ι A) (⇑f : (a : MvPolynomial ι_1 R) → MvPolynomial ι A) ∧
      Ideal.FG (RingHom.ker f.toRingHom)
have intro : 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: refine
    ⟨ι ⊕ ι', by infer_instance, g,
      (MvPolynomial.map_surjective f.toRingHom hf_surj).comp (AlgEquiv.surjective _),
      Ideal.fg_ker_comp _ _ ?_ ?_ (AlgEquiv.surjective _)⟩
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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
    (RingHom.ker (F := MvPolynomial.{v, w₁} (ι ⊕ ι') R →+* MvPolynomial ι (MvPolynomial ι' R))
      (↑(↑(MvPolynomial.sumAlgEquiv R ι ι') : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι (MvPolynomial ι' R)) :
        MvPolynomial (ι ⊕ ι') R →+* MvPolynomial ι (MvPolynomial ι' R)))
⊢ ∃ (ι_1 : Type v) (x : Fintype ι_1) (f : MvPolynomial ι_1 R →ₐ[R] MvPolynomial ι A),
    Surjective (α := MvPolynomial ι_1 R) (β := MvPolynomial ι A) (⇑f : (a : MvPolynomial ι_1 R) → MvPolynomial ι A) ∧
      Ideal.FG (RingHom.ker f.toRingHom)
have intro₁ : Ideal.FG
  (RingHom.ker (F := MvPolynomial ι (MvPolynomial ι' R) →+* MvPolynomial ι A)
    (AlgHom.toRingHom (MvPolynomial.mapAlgHom f)))
Tactic: refine
    ⟨ι ⊕ ι', by infer_instance, g,
      (MvPolynomial.map_surjective f.toRingHom hf_surj).comp (AlgEquiv.surjective _),
      Ideal.fg_ker_comp _ _ ?_ ?_ (AlgEquiv.surjective _)⟩
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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
    (RingHom.ker (F := MvPolynomial.{v, w₁} (ι ⊕ ι') R →+* MvPolynomial ι (MvPolynomial ι' R))
      (↑(↑(MvPolynomial.sumAlgEquiv R ι ι') : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι (MvPolynomial ι' R)) :
        MvPolynomial (ι ⊕ ι') R →+* MvPolynomial ι (MvPolynomial ι' R)))
have intro : Ideal.FG (R := MvPolynomial.{v, w₁} (ι ⊕ ι') R) ⊥
Tactic: rw [AlgEquiv.toAlgHom_toRingHom, AlgHom.ker_coe_equiv]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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
    (RingHom.ker (F := MvPolynomial ι (MvPolynomial ι' R) →+* MvPolynomial ι A)
      (AlgHom.toRingHom (MvPolynomial.mapAlgHom f)))
have 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)))
Tactic: rw [AlgHom.toRingHom_eq_coe, MvPolynomial.mapAlgHom_coe_ringHom, MvPolynomial.ker_map]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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 ι
hfp :
  ∃ (ι : Type v) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] A),
    Surjective (α := MvPolynomial ι R) (β := A) (⇑f : (a : MvPolynomial ι R) → A) ∧ Ideal.FG (RingHom.ker f.toRingHom)
⊢ ∃ (ι_1 : Type v) (x : Fintype ι_1) (f : MvPolynomial ι_1 R →ₐ[R] MvPolynomial ι A),
    Surjective (α := MvPolynomial ι_1 R) (β := MvPolynomial ι A) (⇑f : (a : MvPolynomial ι_1 R) → MvPolynomial ι A) ∧
      Ideal.FG (RingHom.ker f.toRingHom)
have Make : ∀ (ι' : 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)),
  ∃ (ι_1 : Type v) (x : Fintype ι_1) (f : MvPolynomial ι_1 R →ₐ[R] MvPolynomial ι A),
    Surjective (α := MvPolynomial ι_1 R) (β := MvPolynomial ι A) (⇑f : (a : MvPolynomial ι_1 R) → MvPolynomial ι A) ∧
      Ideal.FG (RingHom.ker f.toRingHom)
Tactic: classical
  -- Make universe level `v` explicit so it matches that of `ι`
  obtain ⟨(ι' : Type v), _, f, hf_surj, hf_ker⟩ := hfp
  let g := (MvPolynomial.mapAlgHom f).comp (MvPolynomial.sumAlgEquiv R ι ι').toAlgHom
  cases nonempty_fintype (ι ⊕ ι')
  refine
    ⟨ι ⊕ ι', by infer_instance, g,
      (MvPolynomial.map_surjective f.toRingHom hf_surj).comp (AlgEquiv.surjective _),
      Ideal.fg_ker_comp _ _ ?_ ?_ (AlgEquiv.surjective _)⟩
  · rw [AlgEquiv.toAlgHom_toRingHom, AlgHom.ker_coe_equiv]
    exact Submodule.fg_bot
  · rw [AlgHom.toRingHom_eq_coe, MvPolynomial.mapAlgHom_coe_ringHom, MvPolynomial.ker_map]
    exact hf_ker.map MvPolynomial.C
Cleared hypotheses: hfp
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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 ι
hfp :
  ∃ (ι : Type v) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] A),
    Surjective (α := MvPolynomial ι R) (β := A) (⇑f : (a : MvPolynomial ι R) → A) ∧ Ideal.FG (RingHom.ker f.toRingHom)
Make :
  ∀ (ι' : 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)),
    ∃ (ι_1 : Type v) (x : Fintype ι_1) (f : MvPolynomial ι_1 R →ₐ[R] MvPolynomial ι A),
      Surjective (α := MvPolynomial ι_1 R) (β := MvPolynomial ι A) (⇑f : (a : MvPolynomial ι_1 R) → MvPolynomial ι A) ∧
        Ideal.FG (RingHom.ker f.toRingHom)
Make₁ :
  ∀ (ι' : 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)),
    ∃ (ι_1 : Type v) (x : Fintype ι_1) (f : MvPolynomial ι_1 R →ₐ[R] MvPolynomial ι A),
      Surjective (α := MvPolynomial ι_1 R) (β := MvPolynomial ι A) (⇑f : (a : MvPolynomial ι_1 R) → MvPolynomial ι A) ∧
        Ideal.FG (RingHom.ker f.toRingHom)
⊢ ∃ (ι_1 : Type v) (x : Fintype ι_1) (f : MvPolynomial ι_1 R →ₐ[R] MvPolynomial ι A),
    Surjective (α := MvPolynomial ι_1 R) (β := MvPolynomial ι A) (⇑f : (a : MvPolynomial ι_1 R) → MvPolynomial ι A) ∧
      Ideal.FG (RingHom.ker f.toRingHom)
have intro : ∀ (ι' : 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)) (val : Fintype (ι ⊕ ι')),
  ∃ (ι_1 : Type v) (x : Fintype ι_1) (f : MvPolynomial ι_1 R →ₐ[R] MvPolynomial ι A),
    Surjective (α := MvPolynomial ι_1 R) (β := MvPolynomial ι A) (⇑f : (a : MvPolynomial ι_1 R) → MvPolynomial ι A) ∧
      Ideal.FG (RingHom.ker f.toRingHom)
Tactic: classical
  -- Make universe level `v` explicit so it matches that of `ι`
  obtain ⟨(ι' : Type v), _, f, hf_surj, hf_ker⟩ := hfp
  let g := (MvPolynomial.mapAlgHom f).comp (MvPolynomial.sumAlgEquiv R ι ι').toAlgHom
  cases nonempty_fintype (ι ⊕ ι')
  refine
    ⟨ι ⊕ ι', by infer_instance, g,
      (MvPolynomial.map_surjective f.toRingHom hf_surj).comp (AlgEquiv.surjective _),
      Ideal.fg_ker_comp _ _ ?_ ?_ (AlgEquiv.surjective _)⟩
  · rw [AlgEquiv.toAlgHom_toRingHom, AlgHom.ker_coe_equiv]
    exact Submodule.fg_bot
  · rw [AlgHom.toRingHom_eq_coe, MvPolynomial.mapAlgHom_coe_ringHom, MvPolynomial.ker_map]
    exact hf_ker.map MvPolynomial.C
Cleared hypotheses: hfp
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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
⊢ FinitePresentation R B
have obtain : ∀ (n : ℕ) (I : Ideal (MvPolynomial (Fin n) A)) (e : (MvPolynomial (Fin n) A ⧸ I) ≃ₐ[A] B) (hfg : I.FG),
  FinitePresentation R B
Tactic: obtain ⟨n, I, e, hfg⟩ := iff.1 hfpB
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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
⊢ FinitePresentation A B
have 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
Tactic: obtain ⟨n, f, hf, s, hs⟩ := FinitePresentation.out (R := R) (A := B)
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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
have 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)
Tactic: refine ⟨n, MvPolynomial.aeval (f ∘ X), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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)
⊢ FinitePresentation A B
have 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))))
Tactic: refine ⟨n, MvPolynomial.aeval (f ∘ X), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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
⊢ 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)
have refine_1 : ∀ (x : B), Membership.mem (γ := Subalgebra A B) (adjoin A (↑⊤ : Set B)) x
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]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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
⊢ 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))))
have 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))))
Tactic: obtain ⟨t, ht⟩ := FiniteType.out (R := R) (A := A)