awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
inst : CommRing R
ι : Type u_1
inst_1 : Finite ι
intro :
  ∀ (val : Fintype ι),
    ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial ι R),
      Surjective (α := MvPolynomial (Fin n) R) (β := MvPolynomial ι R)
          (⇑f : (a : MvPolynomial (Fin n) R) → MvPolynomial ι R) ∧
        Ideal.FG (RingHom.ker f.toRingHom)
⊢ ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial ι R),
    Surjective (α := MvPolynomial (Fin n) R) (β := MvPolynomial ι R)
        (⇑f : (a : MvPolynomial (Fin n) R) → MvPolynomial ι R) ∧
      Ideal.FG (RingHom.ker f.toRingHom)

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
inst : CommRing R
ι : Type u_1
inst_1 : Finite ι
val : Fintype ι
eqv : MvPolynomial (Fin (Fintype.card ι)) R ≃ₐ[R] MvPolynomial ι R :=
  AlgEquiv.symm (MvPolynomial.renameEquiv R (Fintype.equivFin ι))
⊢ ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial ι R),
    Surjective (α := MvPolynomial (Fin n) R) (β := MvPolynomial ι R)
        (⇑f : (a : MvPolynomial (Fin n) R) → MvPolynomial ι R) ∧
      Ideal.FG (RingHom.ker f.toRingHom)

Tactic:
⟨Fintype.card ι, eqv, eqv.surjective,
        ((RingHom.injective_iff_ker_eq_bot _).1 eqv.injective).symm ▸ Submodule.fg_bot⟩

Premises used: AlgEquiv.toAlgHom, Eq.rec, Fintype.card, RingHom.injective_iff_ker_eq_bot, And.intro, Exists.intro, Iff.mp, AlgEquiv.injective, Submodule.fg_bot, Eq.symm, AlgEquiv.surjective
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
inst : CommRing R
ι : Type u_1
inst_1 : Finite ι
val : Fintype ι
eqv : MvPolynomial (Fin (Fintype.card ι)) R ≃ₐ[R] MvPolynomial ι R :=
  AlgEquiv.symm (MvPolynomial.renameEquiv R (Fintype.equivFin ι))
⊢ ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial ι R),
    Surjective (α := MvPolynomial (Fin n) R) (β := MvPolynomial ι R)
        (⇑f : (a : MvPolynomial (Fin n) R) → MvPolynomial ι R) ∧
      Ideal.FG (RingHom.ker f.toRingHom)

Tactic:
exact
      ⟨Fintype.card ι, eqv, eqv.surjective,
        ((RingHom.injective_iff_ker_eq_bot _).1 eqv.injective).symm ▸ 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
I : Ideal A
h : I.FG
inst_3 : FinitePresentation R A
obtain :
  ∀ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] A)
    (hf :
      Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
        Ideal.FG (RingHom.ker f.toRingHom)),
    ∃ (n : ℕ) (f : AlgHom.{w₁, w₁, w₂} R (MvPolynomial (Fin n) R) (A ⧸ I)),
      Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A ⧸ I)
          (⇑f : (a : MvPolynomial (Fin n) R) → A ⧸ I) ∧
        Ideal.FG (RingHom.ker f.toRingHom)
⊢ ∃ (n : ℕ) (f : AlgHom.{w₁, w₁, w₂} R (MvPolynomial (Fin n) R) (A ⧸ I)),
    Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A ⧸ I) (⇑f : (a : MvPolynomial (Fin n) R) → A ⧸ I) ∧
      Ideal.FG (RingHom.ker f.toRingHom)

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

Premises used: Algebra.FinitePresentation.out
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
I : Ideal A
h : I.FG
inst_3 : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
⊢ ∃ (n : ℕ) (f : AlgHom.{w₁, w₁, w₂} R (MvPolynomial (Fin n) R) (A ⧸ I)),
    Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A ⧸ I) (⇑f : (a : MvPolynomial (Fin n) R) → A ⧸ I) ∧
      Ideal.FG (RingHom.ker f.toRingHom)

Tactic:
⟨n, (Ideal.Quotient.mkₐ R I).comp f, ?_, ?_⟩

Premises used: And.intro, Exists.intro, AlgHom.comp, Ideal.Quotient.mkₐ
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
I : Ideal A
h : I.FG
inst_3 : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
refine_1 :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A ⧸ I)
    (⇑(AlgHom.comp (Ideal.Quotient.mkₐ R I) f) : (a : MvPolynomial (Fin n) R) → A ⧸ I)
refine_2 :
  Ideal.FG
    (RingHom.ker (F := RingHom.{w₁, w₂} (MvPolynomial (Fin n) R) (A ⧸ I))
      (AlgHom.toRingHom (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)))
⊢ ∃ (n : ℕ) (f : AlgHom.{w₁, w₁, w₂} R (MvPolynomial (Fin n) R) (A ⧸ I)),
    Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A ⧸ I) (⇑f : (a : MvPolynomial (Fin n) R) → A ⧸ I) ∧
      Ideal.FG (RingHom.ker f.toRingHom)

Tactic:
refine ⟨n, (Ideal.Quotient.mkₐ R I).comp f, ?_, ?_⟩
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
I : Ideal A
h : I.FG
inst_3 : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
⊢ Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A ⧸ I)
    (⇑(AlgHom.comp (Ideal.Quotient.mkₐ R I) f) : (a : MvPolynomial (Fin n) R) → A ⧸ I)

Tactic:
(Ideal.Quotient.mkₐ_surjective R I).comp hf.1

Premises used: Submodule.Quotient.mk, And.left, Function.Surjective.comp, Ideal.Quotient.mkₐ_surjective
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
I : Ideal A
h : I.FG
inst_3 : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
⊢ Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A ⧸ I)
    (⇑(AlgHom.comp (Ideal.Quotient.mkₐ R I) f) : (a : MvPolynomial (Fin n) R) → A ⧸ I)

Tactic:
exact (Ideal.Quotient.mkₐ_surjective R I).comp hf.1

Premises used: And.left, Function.Surjective.comp, Ideal.Quotient.mkₐ_surjective
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
I : Ideal A
h : I.FG
inst_3 : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
⊢ Ideal.FG
    (RingHom.ker (F := RingHom.{w₁, w₂} (MvPolynomial (Fin n) R) (A ⧸ I))
      (AlgHom.toRingHom (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)))

Tactic:
Ideal.fg_ker_comp _ _ hf.2 ?_ hf.1

Premises used: Ideal.fg_ker_comp, And.right, And.left
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
I : Ideal A
h : I.FG
inst_3 : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
refine_2 : Ideal.FG (RingHom.ker (F := A →+* A ⧸ I) (AlgHom.toRingHom (Ideal.Quotient.mkₐ R I)))
⊢ Ideal.FG
    (RingHom.ker (F := RingHom.{w₁, w₂} (MvPolynomial (Fin n) R) (A ⧸ I))
      (AlgHom.toRingHom (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)))

Tactic:
refine Ideal.fg_ker_comp _ _ hf.2 ?_ hf.1

Premises used: Ideal.fg_ker_comp, And.right, And.left
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
I : Ideal A
h : I.FG
inst_3 : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
⊢ Ideal.FG (RingHom.ker (F := A →+* A ⧸ I) (AlgHom.toRingHom (Ideal.Quotient.mkₐ R I)))

Tactic:
simp [h]
-- 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
f : A →ₐ[R] B
hf : Surjective.{w₂ + 1, w₃ + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hker : Ideal.FG (RingHom.ker f.toRingHom)
inst_5 : FinitePresentation R A
⊢ FinitePresentation R B

Tactic:
letI : FinitePresentation R (A ⧸ RingHom.ker f) := FinitePresentation.quotient hker
  equiv (Ideal.quotientKerAlgEquivOfSurjective hf)

Premises used: Algebra.FinitePresentation.equiv, Ideal.quotientKerAlgEquivOfSurjective
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
mp :
  FinitePresentation R A →
    ∃ (n : ℕ) (I : Ideal (MvPolynomial (Fin n) R)) (x : (MvPolynomial (Fin n) R ⧸ I) ≃ₐ[R] A), I.FG
mpr :
  (∃ (n : ℕ) (I : Ideal (MvPolynomial (Fin n) R)) (x : (MvPolynomial (Fin n) R ⧸ I) ≃ₐ[R] A), I.FG) →
    FinitePresentation R A
⊢ FinitePresentation R A ↔
    ∃ (n : ℕ) (I : Ideal (MvPolynomial (Fin n) R)) (x : (MvPolynomial (Fin n) R ⧸ I) ≃ₐ[R] A), I.FG

Tactic:
constructor
-- Module: Mathlib.RingTheory.FinitePresentation
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
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
⊢ ∃ (n : ℕ) (I : Ideal (MvPolynomial (Fin n) R)) (x : (MvPolynomial (Fin n) R ⧸ I) ≃ₐ[R] A), I.FG

Tactic:
⟨n, RingHom.ker f.toRingHom, Ideal.quotientKerAlgEquivOfSurjective hf.1, hf.2⟩

Premises used: And.right, And.left, AlgHom.toRingHom, Exists.intro, RingHom.ker, Ideal.quotientKerAlgEquivOfSurjective
-- Module: Mathlib.RingTheory.FinitePresentation
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
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
⊢ ∃ (n : ℕ) (I : Ideal (MvPolynomial (Fin n) R)) (x : (MvPolynomial (Fin n) R ⧸ I) ≃ₐ[R] A), I.FG

Tactic:
exact ⟨n, RingHom.ker f.toRingHom, Ideal.quotientKerAlgEquivOfSurjective hf.1, hf.2⟩
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
n : ℕ
I : Ideal (MvPolynomial (Fin n) R)
e : (MvPolynomial (Fin n) R ⧸ I) ≃ₐ[R] A
hfg : I.FG
this : FinitePresentation R (MvPolynomial (Fin n) R ⧸ I) := ⋯
⊢ FinitePresentation R A

Tactic:
equiv e

Premises used: Algebra.FinitePresentation.equiv
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
n : ℕ
I : Ideal (MvPolynomial (Fin n) R)
e : (MvPolynomial (Fin n) R ⧸ I) ≃ₐ[R] A
hfg : I.FG
this : FinitePresentation R (MvPolynomial (Fin n) R ⧸ I) := ⋯
⊢ FinitePresentation R A

Tactic:
exact equiv e

Premises used: Algebra.FinitePresentation.equiv
-- Module: Mathlib.RingTheory.FinitePresentation
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)
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
⊢ 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)

Tactic:
constructor
-- Module: Mathlib.RingTheory.FinitePresentation
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)

Tactic:
⟨ULift (Fin n), inferInstance, f.comp ulift_var.toAlgHom, hfs.comp ulift_var.surjective,
        Ideal.fg_ker_comp _ _ ?_ hfk ulift_var.surjective⟩

Premises used: AlgEquiv.toAlgHom, ULift, inferInstance, Ideal.fg_ker_comp, And.intro, Exists.intro, Function.Surjective.comp, AlgHom.comp, Fin, AlgEquiv.surjective
-- Module: Mathlib.RingTheory.FinitePresentation
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
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))
⊢ ∃ (ι : 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)

Tactic:
refine
      ⟨ULift (Fin n), inferInstance, f.comp ulift_var.toAlgHom, hfs.comp ulift_var.surjective,
        Ideal.fg_ker_comp _ _ ?_ hfk ulift_var.surjective⟩
-- Module: Mathlib.RingTheory.FinitePresentation
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
⊢ 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:
simpa using 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
ι : 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)
mpr : ∀ (equiv : MvPolynomial ι R ≃ₐ[R] MvPolynomial (Fin (Fintype.card ι)) R), FinitePresentation R A
⊢ FinitePresentation R A

Tactic:
have equiv := MvPolynomial.renameEquiv R (Fintype.equivFin ι)
-- Module: Mathlib.RingTheory.FinitePresentation
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
right :
  Ideal.FG (RingHom.ker (f.comp (↑equiv.symm : MvPolynomial (Fin (Fintype.card ι)) R →ₐ[R] MvPolynomial ι R)).toRingHom)
⊢ FinitePresentation R A

Tactic:
use Fintype.card ι, f.comp equiv.symm, hf.1.comp (AlgEquiv.symm equiv).surjective

Premises used: AlgEquiv.symm, Fintype.card, And.left, Function.Surjective.comp, AlgHom.comp, AlgEquiv.surjective
-- Module: Mathlib.RingTheory.FinitePresentation
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)

Tactic:
Ideal.fg_ker_comp (S := MvPolynomial ι R) (A := A) _ f ?_ hf.2 equiv.symm.surjective

Premises used: AlgEquiv.symm, Ideal.fg_ker_comp, And.right, RingHomClass.toRingHom, AlgEquiv.surjective
-- Module: Mathlib.RingTheory.FinitePresentation
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
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))
⊢ Ideal.FG (RingHom.ker (f.comp (↑equiv.symm : MvPolynomial (Fin (Fintype.card ι)) R →ₐ[R] MvPolynomial ι R)).toRingHom)

Tactic:
refine Ideal.fg_ker_comp (S := MvPolynomial ι R) (A := A) _ f ?_ hf.2 equiv.symm.surjective

Premises used: Ideal.fg_ker_comp, And.right, RingHomClass.toRingHom
-- Module: Mathlib.RingTheory.FinitePresentation
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 := 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:
simpa using 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 ι
⊢ FinitePresentation R A

Tactic:
have hfp : FinitePresentation R A := inferInstance
-- 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 ι
hfp : FinitePresentation R A
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)
⊢ FinitePresentation R (MvPolynomial ι A)

Tactic:
rw [iff_quotient_mvPolynomial'] at hfp ⊢

Premises used: Algebra.FinitePresentation.iff_quotient_mvPolynomial'
-- 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 ι
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)
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)
⊢ ∃ (ι_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
-- 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))
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)
⊢ ∃ (ι_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 (ι ⊕ ι')

Premises used: Sum, nonempty_fintype
-- 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 (ι ⊕ ι')
⊢ Fintype (ι ⊕ ι')

Tactic:
infer_instance
-- 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
    (RingHom.ker (F := MvPolynomial.{v, w₁} (ι ⊕ ι') R →+* MvPolynomial ι (MvPolynomial ι' R))
      (↑(↑(MvPolynomial.sumAlgEquiv R ι ι') : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι (MvPolynomial ι' R)) :
        MvPolynomial (ι ⊕ ι') R →+* MvPolynomial ι (MvPolynomial ι' R)))
intro₁ :
  Ideal.FG
    (RingHom.ker (F := MvPolynomial ι (MvPolynomial ι' R) →+* MvPolynomial ι A)
      (AlgHom.toRingHom (MvPolynomial.mapAlgHom f)))
⊢ ∃ (ι_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:
refine
    ⟨ι ⊕ ι', by infer_instance, g,
      (MvPolynomial.map_surjective f.toRingHom hf_surj).comp (AlgEquiv.surjective _),
      Ideal.fg_ker_comp _ _ ?_ ?_ (AlgEquiv.surjective _)⟩