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
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)
inst_3 : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin m) R) (β := A) (⇑f' : (a : MvPolynomial (Fin m) R) → A)
s : Finset (MvPolynomial (Fin m) R)
hs :
  Eq (α := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R))) (RingHom.ker f'.toRingHom)
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : (i : Fin n) → MvPolynomial (Fin m) R
hg :
  ∀ (i : Fin n),
    Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) (g i) : A)
      ((f : (a : MvPolynomial (Fin n) R) → A) (MvPolynomial.X i) : A)
h : (i : Fin m) → MvPolynomial (Fin n) R
hh :
  ∀ (i : Fin m),
    Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) (h i) : A)
      ((f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) : A)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn :=
  fun (i : Fin n) ↦
    HSub.hSub (α := MvPolynomial (Fin n) R) (β := RXn) (MvPolynomial.X i) ((aeval_h : (a : RXm) → RXn) (g i) : RXn)
hh' :
  ∀ (x : RXm),
    Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) ((aeval_h : (a : RXm) → RXn) x : RXn) : A)
      ((f' : (a : MvPolynomial (Fin m) R) → A) x : A)
s' : Set RXn := Set.range g' ∪ (⇑aeval_h : (a : RXm) → RXn) '' (↑s : Set RXm)
leI : LE.le (α := Ideal RXn) (Ideal.span s') (RingHom.ker f.toRingHom)
x_1 : RXm
y : RXn
hy : Membership.mem (γ := AddSubmonoid RXn) (Submodule.toAddSubmonoid (Ideal.span s')) y
this :
  HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x_1 : RXn) y ∈
    aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
hx_1 : Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) x_1 : A) (0 : A)
x : RXm
hx : x ∈ (↑s : Set RXm)
⊢ Membership.mem (α := RXn) (γ := Set RXn) ((⇑aeval_h : (a : RXm) → RXn) '' (↑s : Set RXm))
    ((aeval_h : (a : RXm) → RXn) x : RXn)

Tactic:
exact Set.mem_image_of_mem _ hx

Premises used: Set.mem_image_of_mem
-- 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)
inst_5 : FinitePresentation R A
inst_6 : FinitePresentation R B
obtain :
  ∀ (n : ℕ) (g : MvPolynomial (Fin n) R →ₐ[R] A)
    (hg : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑g : (a : MvPolynomial (Fin n) R) → A)),
    Ideal.FG (RingHom.ker g.toRingHom) → Ideal.FG (RingHom.ker f.toRingHom)
⊢ Ideal.FG (RingHom.ker f.toRingHom)

Tactic:
obtain ⟨n, g, hg, _⟩ := FinitePresentation.out (R := R) (A := A)

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
f : A →ₐ[R] B
hf : Surjective.{w₂ + 1, w₃ + 1} (α := A) (β := B) (⇑f : (a : A) → B)
inst_5 : FinitePresentation R A
inst_6 : FinitePresentation R B
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] A
hg : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑g : (a : MvPolynomial (Fin n) R) → A)
right : Ideal.FG (RingHom.ker g.toRingHom)
⊢ Ideal.FG.{w₂} (R := A) (Ideal.map g.toRingHom (RingHom.ker (f.comp g).toRingHom))

Tactic:
(ker_fg_of_mvPolynomial (f.comp g) (hf.comp hg)).map g.toRingHom

Premises used: Ideal.FG.map, Algebra.FinitePresentation.ker_fg_of_mvPolynomial, AlgHom.toRingHom, Function.Surjective.comp, AlgHom.comp
-- 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)
inst_5 : FinitePresentation R A
inst_6 : FinitePresentation R B
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] A
hg : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑g : (a : MvPolynomial (Fin n) R) → A)
right : Ideal.FG (RingHom.ker g.toRingHom)
h : Eq (α := Ideal A) (RingHom.ker f.toRingHom) (Ideal.map g.toRingHom (RingHom.ker (f.comp g).toRingHom))
⊢ Ideal.FG (RingHom.ker f.toRingHom)

Tactic:
convert! (ker_fg_of_mvPolynomial (f.comp g) (hf.comp hg)).map g.toRingHom

Premises used: Ideal.FG.map, Algebra.FinitePresentation.ker_fg_of_mvPolynomial, AlgHom.toRingHom, Function.Surjective.comp, AlgHom.comp
-- 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)
inst_5 : FinitePresentation R A
inst_6 : FinitePresentation R B
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] A
hg : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑g : (a : MvPolynomial (Fin n) R) → A)
right : Ideal.FG (RingHom.ker g.toRingHom)
h :
  Eq (α := Ideal A) (Ideal.comap (F := A →+* B) (↑f : A →+* B) ⊥)
    (Ideal.map (F := RingHom.{w₁, w₂} (MvPolynomial (Fin n) R) A) (↑g : MvPolynomial (Fin n) R →+* A)
      (Ideal.comap (F := RingHom.{w₁, w₃} (MvPolynomial (Fin n) R) B)
        (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : A →+* B) (↑g : MvPolynomial (Fin n) R →+* A)) ⊥))
⊢ Eq (α := Ideal A) (RingHom.ker f.toRingHom) (Ideal.map g.toRingHom (RingHom.ker (f.comp g).toRingHom))

Tactic:
simp_rw [RingHom.ker_eq_comap_bot, AlgHom.toRingHom_eq_coe, AlgHom.comp_toRingHom]

Premises used: AlgHom.comp_toRingHom, RingHom.ker_eq_comap_bot, AlgHom.toRingHom_eq_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
f : A →ₐ[R] B
hf : Surjective.{w₂ + 1, w₃ + 1} (α := A) (β := B) (⇑f : (a : A) → B)
inst_5 : FinitePresentation R A
inst_6 : FinitePresentation R B
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] A
hg : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑g : (a : MvPolynomial (Fin n) R) → A)
right : Ideal.FG (RingHom.ker g.toRingHom)
h :
  Eq (α := Ideal A) (Ideal.comap (F := A →+* B) (↑f : A →+* B) ⊥)
    (Ideal.map (F := RingHom.{w₁, w₂} (MvPolynomial (Fin n) R) A) (↑g : MvPolynomial (Fin n) R →+* A)
      (Ideal.comap (F := RingHom.{w₁, w₂} (MvPolynomial (Fin n) R) A) (↑g : MvPolynomial (Fin n) R →+* A)
        (Ideal.comap (F := A →+* B) (↑f : A →+* B) ⊥)))
h₁ h₂ : Eq (α := Ideal A) (Ideal.comap (F := A →+* B) (↑f : A →+* B) ⊥) (Ideal.comap (F := A →+* B) (↑f : A →+* B) ⊥)
⊢ Eq (α := Ideal A) (Ideal.comap (F := A →+* B) (↑f : A →+* B) ⊥)
    (Ideal.map (F := RingHom.{w₁, w₂} (MvPolynomial (Fin n) R) A) (↑g : MvPolynomial (Fin n) R →+* A)
      (Ideal.comap (F := RingHom.{w₁, w₃} (MvPolynomial (Fin n) R) B)
        (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : A →+* B) (↑g : MvPolynomial (Fin n) R →+* A)) ⊥))

Tactic:
rw [← Ideal.comap_comap, Ideal.map_comap_of_surjective (g : MvPolynomial (Fin n) R →+* A) hg]

Premises used: RingHomClass.toRingHom, Ideal.map_comap_of_surjective, Ideal.comap_comap
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
rw : Algebra.FinitePresentation A B ↔ Algebra.FinitePresentation A B
rw₁ rw₂ : Algebra.FinitePresentation A B ↔ Algebra.FinitePresentation A B
⊢ FinitePresentation (algebraMap A B) ↔ Algebra.FinitePresentation A B

Tactic:
rw [RingHom.FinitePresentation, toAlgebra_algebraMap]

Premises used: RingHom.FinitePresentation, toAlgebra_algebraMap
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.FinitePresentation
⊢ f.FiniteType

Tactic:
@Algebra.FiniteType.of_finitePresentation A B _ _ f.toAlgebra hf

Premises used: RingHom.FiniteType, Algebra.FiniteType.of_finitePresentation
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
A : Type u_1
inst : CommRing A
⊢ FinitePresentation (RingHom.id A)

Tactic:
Algebra.FinitePresentation.self A

Premises used: RingHom.FinitePresentation, Algebra.FinitePresentation.self
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
f : A →+* B
g : B →+* C
hf : f.FinitePresentation
hg : Surjective.{u_2 + 1, u_3 + 1} (α := B) (β := C) (⇑g : (a : B) → C)
hker : Ideal.FG (ker g)
⊢ Algebra.FinitePresentation A B

Tactic:
algebraize [f, g.comp f]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
f : A →+* B
g : B →+* C
hf : f.FinitePresentation
hg : Surjective.{u_2 + 1, u_3 + 1} (α := B) (β := C) (⇑g : (a : B) → C)
hker : Ideal.FG (ker g)
algInst : Algebra A B := f.toAlgebra
algInst_1 : Algebra A C := (g.comp f).toAlgebra
algebraizeInst : Algebra.FinitePresentation A B
⊢ (g.comp f).FinitePresentation

Tactic:
Algebra.FinitePresentation.of_surjective
    (f :=
      { g with
        toFun := g
        commutes' := fun _ => rfl })
    hg hker

Premises used: RingHom.FinitePresentation, Algebra.FinitePresentation.of_surjective
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
f : A →+* B
g : B →+* C
hf : f.FinitePresentation
hg : Surjective.{u_2 + 1, u_3 + 1} (α := B) (β := C) (⇑g : (a : B) → C)
hker : Ideal.FG (ker g)
algInst : Algebra A B := f.toAlgebra
algInst_1 : Algebra A C := (g.comp f).toAlgebra
algebraizeInst : Algebra.FinitePresentation A B
⊢ (g.comp f).FinitePresentation

Tactic:
exact Algebra.FinitePresentation.of_surjective
    (f :=
      { g with
        toFun := g
        commutes' := fun _ => rfl })
    hg hker

Premises used: Algebra.FinitePresentation.of_surjective
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hker : Ideal.FG (ker f)
rw : (f.comp (RingHom.id A)).FinitePresentation
⊢ f.FinitePresentation

Tactic:
rw [← f.comp_id]

Premises used: RingHom.comp_id
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hker : Ideal.FG (ker f)
⊢ (f.comp (RingHom.id A)).FinitePresentation

Tactic:
(id A).comp_surjective hf hker

Premises used: RingHom.FinitePresentation.comp_surjective, RingHom.FinitePresentation.id
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hker : Ideal.FG (ker f)
⊢ (f.comp (RingHom.id A)).FinitePresentation

Tactic:
exact (id A).comp_surjective hf hker

Premises used: RingHom.FinitePresentation.comp_surjective, RingHom.FinitePresentation.id
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
rw : Function.Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ Eq (α := Ideal A) (ker f) ⊥

Tactic:
rw [← RingHom.injective_iff_ker_eq_bot]

Premises used: RingHom.injective_iff_ker_eq_bot
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)

Tactic:
hf.1

Premises used: And.left
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)

Tactic:
exact hf.1

Premises used: And.left
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ Eq (α := Ideal A) (ker f) ⊥

Tactic:
have : ker f = ⊥ := by rw [← RingHom.injective_iff_ker_eq_bot]; exact hf.1
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
this : Eq (α := Ideal A) (ker f) ⊥
rw : Ideal.FG.{u_1} (R := A) ⊥
⊢ Ideal.FG (ker f)

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
this : Eq (α := Ideal A) (ker f) ⊥
⊢ Ideal.FG.{u_1} (R := A) ⊥

Tactic:
Submodule.fg_bot

Premises used: Submodule.FG, Ideal.FG, Submodule.fg_bot
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
this : Eq (α := Ideal A) (ker f) ⊥
⊢ Ideal.FG.{u_1} (R := A) ⊥

Tactic:
exact Submodule.fg_bot

Premises used: Submodule.fg_bot
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : IsNoetherianRing A
f : A →+* B
⊢ f.FiniteType ↔ f.FinitePresentation

Tactic:
@Algebra.FinitePresentation.of_finiteType A B _ _ f.toAlgebra _

Premises used: RingHom.FinitePresentation, RingHom.FiniteType, Algebra.FinitePresentation.of_finiteType
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
g : B →+* C
f : A →+* B
hg : g.FinitePresentation
hf : f.FinitePresentation
⊢ Algebra.FinitePresentation B C

Tactic:
algebraize [f, g, g.comp f]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
g : B →+* C
f : A →+* B
hg : g.FinitePresentation
hf : f.FinitePresentation
algebraizeInst : Algebra.FinitePresentation B C
⊢ Algebra.FinitePresentation A B

Tactic:
algebraize [f, g, g.comp f]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
g : B →+* C
f : A →+* B
hg : g.FinitePresentation
hf : f.FinitePresentation
algInst : Algebra A B := f.toAlgebra
algInst_1 : Algebra B C := g.toAlgebra
algInst_2 : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower A B C := ⋯
algebraizeInst : Algebra.FinitePresentation B C
algebraizeInst_1 : Algebra.FinitePresentation A B
⊢ (g.comp f).FinitePresentation

Tactic:
Algebra.FinitePresentation.trans A B C

Premises used: RingHom.FinitePresentation, Algebra.FinitePresentation.trans
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
g : B →+* C
f : A →+* B
hg : g.FinitePresentation
hf : f.FinitePresentation
algInst : Algebra A B := f.toAlgebra
algInst_1 : Algebra B C := g.toAlgebra
algInst_2 : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower A B C := ⋯
algebraizeInst : Algebra.FinitePresentation B C
algebraizeInst_1 : Algebra.FinitePresentation A B
⊢ (g.comp f).FinitePresentation

Tactic:
exact Algebra.FinitePresentation.trans A B C

Premises used: Algebra.FinitePresentation.trans
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
f : A →+* B
g : B →+* C
hg : (g.comp f).FinitePresentation
hf : f.FiniteType
⊢ Algebra.FinitePresentation A C

Tactic:
algebraize [f, g, g.comp f]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
f : A →+* B
g : B →+* C
hg : (g.comp f).FinitePresentation
hf : f.FiniteType
algebraizeInst : Algebra.FinitePresentation A C
⊢ Algebra.FiniteType A B

Tactic:
algebraize [f, g, g.comp f]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
f : A →+* B
g : B →+* C
hg : (g.comp f).FinitePresentation
hf : f.FiniteType
algInst : Algebra A B := f.toAlgebra
algInst_1 : Algebra B C := g.toAlgebra
algInst_2 : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower A B C := ⋯
algebraizeInst : Algebra.FinitePresentation A C
algebraizeInst_1 : Algebra.FiniteType A B
⊢ g.FinitePresentation

Tactic:
Algebra.FinitePresentation.of_restrict_scalars_finitePresentation A B C

Premises used: RingHom.FinitePresentation, Algebra.FinitePresentation.of_restrict_scalars_finitePresentation
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
f : A →+* B
g : B →+* C
hg : (g.comp f).FinitePresentation
hf : f.FiniteType
algInst : Algebra A B := f.toAlgebra
algInst_1 : Algebra B C := g.toAlgebra
algInst_2 : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower A B C := ⋯
algebraizeInst : Algebra.FinitePresentation A C
algebraizeInst_1 : Algebra.FiniteType A B
⊢ g.FinitePresentation

Tactic:
exact Algebra.FinitePresentation.of_restrict_scalars_finitePresentation A B C

Premises used: Algebra.FinitePresentation.of_restrict_scalars_finitePresentation
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_2 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_2 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_2 : CommRing S] (f : R →+* S),
    Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S) → Ideal.FG (ker f) → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_2 : CommRing S] (T : Type v) [inst_3 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.FinitePresentation
letI : Q R S f
⊢ Q R S f

Tactic:
letI := f.toAlgebra
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_2 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_2 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_2 : CommRing S] (f : R →+* S),
    Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S) → Ideal.FG (ker f) → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_2 : CommRing S] (T : Type v) [inst_3 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.FinitePresentation
this : Algebra R S := f.toAlgebra
obtain :
  ∀ (n : ℕ) (g : MvPolynomial (Fin n) R →ₐ[R] S)
    (hg : Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑g : (a : MvPolynomial (Fin n) R) → S))
    (hg' : Ideal.FG (ker g.toRingHom)), Q R S f
⊢ Q R S f

Tactic:
obtain ⟨n, g, hg, hg'⟩ := hf
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_2 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_2 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_2 : CommRing S] (f : R →+* S),
    Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S) → Ideal.FG (ker f) → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_2 : CommRing S] (T : Type v) [inst_3 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
this : Algebra R S := f.toAlgebra
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] S
hg : Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑g : (a : MvPolynomial (Fin n) R) → S)
hg' : Ideal.FG (ker g.toRingHom)
g' : RingHom.{u, v} (MvPolynomial (Fin n) R) S := g.toRingHom
⊢ Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑g' : (a : MvPolynomial (Fin n) R) → S)

Tactic:
change Surjective g' at hg

Premises used: DFunLike.coe, Function.Surjective
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_2 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_2 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_2 : CommRing S] (f : R →+* S),
    Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S) → Ideal.FG (ker f) → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_2 : CommRing S] (T : Type v) [inst_3 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
this : Algebra R S := f.toAlgebra
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] S
hg' : Ideal.FG (ker g.toRingHom)
g' : RingHom.{u, v} (MvPolynomial (Fin n) R) S := g.toRingHom
hg : Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑g' : (a : MvPolynomial (Fin n) R) → S)
⊢ Ideal.FG (ker g')

Tactic:
change (ker g').FG at hg'

Premises used: Ideal.FG, RingHom.ker
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_2 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_2 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_2 : CommRing S] (f : R →+* S),
    Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S) → Ideal.FG (ker f) → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_2 : CommRing S] (T : Type v) [inst_3 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
this : Algebra R S := f.toAlgebra
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] S
g' : RingHom.{u, v} (MvPolynomial (Fin n) R) S := g.toRingHom
hg : Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑g' : (a : MvPolynomial (Fin n) R) → S)
hg' : Ideal.FG (ker g')
⊢ g'.comp MvPolynomial.C = f

Tactic:
have : g'.comp MvPolynomial.C = f := g.comp_algebraMap