awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 : 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')
this : g'.comp MvPolynomial.C = f
clear_value :
  ∀ (g' : RingHom.{u, v} (MvPolynomial (Fin n) 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')) (this : g'.comp MvPolynomial.C = f), Q R S f
⊢ Q R S f

Tactic:
clear_value g'
-- 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_1 : Algebra R S := f.toAlgebra
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] S
g' : RingHom.{u, v} (MvPolynomial (Fin n) 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')
this : g'.comp MvPolynomial.C = f
subst : ∀ (g : MvPolynomial (Fin n) R →ₐ[R] S), Q R S (g'.comp MvPolynomial.C)
⊢ Q R S f

Tactic:
subst this
-- 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
g' : RingHom.{u, v} (MvPolynomial (Fin 0) R) S
hg : Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin 0) R) (β := S) (⇑g' : (a : MvPolynomial (Fin 0) R) → S)
hg' : Ideal.FG (ker g')
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
⊢ Q R S (g'.comp MvPolynomial.C)

Tactic:
fg_ker _ _ _ (hg.comp (MvPolynomial.C_surjective (Fin 0))) ?_

Premises used: MvPolynomial.C_surjective, Function.Surjective.comp, OfNat.ofNat, Fin
-- 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
g' : RingHom.{u, v} (MvPolynomial (Fin 0) R) S
hg : Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin 0) R) (β := S) (⇑g' : (a : MvPolynomial (Fin 0) R) → S)
hg' : Ideal.FG (ker g')
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
zero : Ideal.FG (ker (g'.comp MvPolynomial.C))
⊢ Q R S (g'.comp MvPolynomial.C)

Tactic:
refine fg_ker _ _ _ (hg.comp (MvPolynomial.C_surjective (Fin 0))) ?_

Premises used: Function.Surjective.comp
-- 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
g' : RingHom.{u, v} (MvPolynomial (Fin 0) R) S
hg : Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin 0) R) (β := S) (⇑g' : (a : MvPolynomial (Fin 0) R) → S)
hg' : Ideal.FG (ker g')
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
zero : Ideal.FG (Ideal.comap (F := R →+* MvPolynomial (Fin 0) R) MvPolynomial.C (ker g'))
⊢ Ideal.FG (ker (g'.comp MvPolynomial.C))

Tactic:
rw [← comap_ker]

Premises used: RingHom.comap_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
g' : RingHom.{u, v} (MvPolynomial (Fin 0) R) S
hg : Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin 0) R) (β := S) (⇑g' : (a : MvPolynomial (Fin 0) R) → S)
hg' : Ideal.FG (ker g')
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
⊢ Ideal.FG (R := R)
    (Ideal.map (F := MvPolynomial (Fin 0) R →+* R) (RingEquiv.toRingHom (MvPolynomial.isEmptyRingEquiv R (Fin 0)))
      (ker g'))

Tactic:
hg'.map (MvPolynomial.isEmptyRingEquiv R (Fin 0)).toRingHom

Premises used: Ideal.FG.map, RingEquiv.toRingHom, OfNat.ofNat, Fin, MvPolynomial.isEmptyRingEquiv
-- 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
g' : RingHom.{u, v} (MvPolynomial (Fin 0) R) S
hg : Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin 0) R) (β := S) (⇑g' : (a : MvPolynomial (Fin 0) R) → S)
hg' : Ideal.FG (ker g')
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
h :
  Eq (α := Ideal R) (Ideal.comap (F := R →+* MvPolynomial (Fin 0) R) MvPolynomial.C (ker g'))
    (Ideal.map (F := MvPolynomial (Fin 0) R →+* R) (RingEquiv.toRingHom (MvPolynomial.isEmptyRingEquiv R (Fin 0)))
      (ker g'))
⊢ Ideal.FG (Ideal.comap (F := R →+* MvPolynomial (Fin 0) R) MvPolynomial.C (ker g'))

Tactic:
convert! hg'.map (MvPolynomial.isEmptyRingEquiv R (Fin 0)).toRingHom using 1

Premises used: Ideal.FG.map, RingEquiv.toRingHom, OfNat.ofNat, Fin, MvPolynomial.isEmptyRingEquiv
-- 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
g' : RingHom.{u, v} (MvPolynomial (Fin 0) R) S
hg : Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin 0) R) (β := S) (⇑g' : (a : MvPolynomial (Fin 0) R) → S)
hg' : Ideal.FG (ker g')
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
h :
  Eq (α := Ideal R) (Ideal.comap (F := R →+* MvPolynomial (Fin 0) R) MvPolynomial.C (ker g'))
    (Ideal.map (F := MvPolynomial (Fin 0) R →+* R)
      (↑(MvPolynomial.isEmptyRingEquiv R (Fin 0)) : MvPolynomial (Fin 0) R →+* R) (ker g'))
⊢ Eq (α := Ideal R) (Ideal.comap (F := R →+* MvPolynomial (Fin 0) R) MvPolynomial.C (ker g'))
    (Ideal.map (F := MvPolynomial (Fin 0) R →+* R) (RingEquiv.toRingHom (MvPolynomial.isEmptyRingEquiv R (Fin 0)))
      (ker g'))

Tactic:
simp only [RingEquiv.toRingHom_eq_coe]

Premises used: RingEquiv.toRingHom_eq_coe
-- 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
g' : RingHom.{u, v} (MvPolynomial (Fin 0) R) S
hg : Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin 0) R) (β := S) (⇑g' : (a : MvPolynomial (Fin 0) R) → S)
hg' : Ideal.FG (ker g')
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
⊢ Eq (α := Ideal R) (Ideal.comap (F := R →+* MvPolynomial (Fin 0) R) MvPolynomial.C (ker g'))
    (Ideal.map (F := MvPolynomial (Fin 0) R →+* R)
      (↑(MvPolynomial.isEmptyRingEquiv R (Fin 0)) : MvPolynomial (Fin 0) R →+* R) (ker g'))

Tactic:
Ideal.comap_symm (MvPolynomial.isEmptyRingEquiv R (Fin 0))

Premises used: Ideal.comap_symm, Ideal.map, RingHomClass.toRingHom, Ideal.comap, OfNat.ofNat, Fin, MvPolynomial.isEmptyRingEquiv, MvPolynomial.C, RingEquiv.symm, Finsupp.single
-- 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
g' : RingHom.{u, v} (MvPolynomial (Fin 0) R) S
hg : Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin 0) R) (β := S) (⇑g' : (a : MvPolynomial (Fin 0) R) → S)
hg' : Ideal.FG (ker g')
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
⊢ Eq (α := Ideal R) (Ideal.comap (F := R →+* MvPolynomial (Fin 0) R) MvPolynomial.C (ker g'))
    (Ideal.map (F := MvPolynomial (Fin 0) R →+* R)
      (↑(MvPolynomial.isEmptyRingEquiv R (Fin 0)) : MvPolynomial (Fin 0) R →+* R) (ker g'))

Tactic:
exact Ideal.comap_symm (MvPolynomial.isEmptyRingEquiv R (Fin 0))

Premises used: Ideal.comap_symm, OfNat.ofNat, Fin, MvPolynomial.isEmptyRingEquiv
-- 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)
n : ℕ
IH :
  ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_2 : CommRing S] (g' : RingHom.{u, v} (MvPolynomial (Fin n) 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')),
    let this := (g'.comp MvPolynomial.C).toAlgebra;
    Q R S (g'.comp MvPolynomial.C)
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
g' : RingHom.{u, v} (MvPolynomial (Fin (n + 1)) R) S
hg :
  Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin (n + 1)) R) (β := S) (⇑g' : (a : MvPolynomial (Fin (n + 1)) R) → S)
hg' : Ideal.FG (ker g')
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] MvPolynomial (Fin n) R[X] :=
  AlgEquiv.trans (MvPolynomial.renameEquiv R (finSuccEquiv n)) (MvPolynomial.optionEquivRight R (Fin n))
rw :
  Ideal.FG
    (Ideal.comap (F := MvPolynomial (Fin n) R[X] →+* MvPolynomial (Fin (n + 1)) R)
      (↑e.symm : MvPolynomial (Fin n) R[X] →+* MvPolynomial (Fin (n + 1)) R) (ker g'))
⊢ Ideal.FG
    (ker (F := RingHom.{u, v} (MvPolynomial (Fin n) R[X]) S)
      (g'.comp (↑e.symm : MvPolynomial (Fin n) R[X] →+* MvPolynomial (Fin (n + 1)) R)))

Tactic:
rw [← RingHom.comap_ker]

Premises used: RingHom.comap_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)
n : ℕ
IH :
  ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_2 : CommRing S] (g' : RingHom.{u, v} (MvPolynomial (Fin n) 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')),
    let this := (g'.comp MvPolynomial.C).toAlgebra;
    Q R S (g'.comp MvPolynomial.C)
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
g' : RingHom.{u, v} (MvPolynomial (Fin (n + 1)) R) S
hg :
  Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin (n + 1)) R) (β := S) (⇑g' : (a : MvPolynomial (Fin (n + 1)) R) → S)
hg' : Ideal.FG (ker g')
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] MvPolynomial (Fin n) R[X] :=
  AlgEquiv.trans (MvPolynomial.renameEquiv R (finSuccEquiv n)) (MvPolynomial.optionEquivRight R (Fin n))
⊢ Ideal.FG (R := MvPolynomial (Fin n) R[X])
    (Ideal.map (↑e : MvPolynomial (Fin (n + 1)) R →ₐ[R] MvPolynomial (Fin n) R[X]).toRingHom (ker g'))

Tactic:
hg'.map e.toAlgHom.toRingHom

Premises used: AlgEquiv.toAlgHom, Ideal.FG.map, AlgHom.toRingHom
-- 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)
n : ℕ
IH :
  ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_2 : CommRing S] (g' : RingHom.{u, v} (MvPolynomial (Fin n) 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')),
    let this := (g'.comp MvPolynomial.C).toAlgebra;
    Q R S (g'.comp MvPolynomial.C)
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
g' : RingHom.{u, v} (MvPolynomial (Fin (n + 1)) R) S
hg :
  Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin (n + 1)) R) (β := S) (⇑g' : (a : MvPolynomial (Fin (n + 1)) R) → S)
hg' : Ideal.FG (ker g')
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] MvPolynomial (Fin n) R[X] :=
  AlgEquiv.trans (MvPolynomial.renameEquiv R (finSuccEquiv n)) (MvPolynomial.optionEquivRight R (Fin n))
h :
  Eq (α := Ideal (MvPolynomial (Fin n) R[X]))
    (Ideal.comap (F := MvPolynomial (Fin n) R[X] →+* MvPolynomial (Fin (n + 1)) R)
      (↑e.symm : MvPolynomial (Fin n) R[X] →+* MvPolynomial (Fin (n + 1)) R) (ker g'))
    (Ideal.map (↑e : MvPolynomial (Fin (n + 1)) R →ₐ[R] MvPolynomial (Fin n) R[X]).toRingHom (ker g'))
⊢ Ideal.FG
    (Ideal.comap (F := MvPolynomial (Fin n) R[X] →+* MvPolynomial (Fin (n + 1)) R)
      (↑e.symm : MvPolynomial (Fin n) R[X] →+* MvPolynomial (Fin (n + 1)) R) (ker g'))

Tactic:
convert! hg'.map e.toAlgHom.toRingHom using 1

Premises used: AlgEquiv.toAlgHom, Ideal.FG.map, AlgHom.toRingHom
-- 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)
n : ℕ
IH :
  ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_2 : CommRing S] (g' : RingHom.{u, v} (MvPolynomial (Fin n) 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')),
    let this := (g'.comp MvPolynomial.C).toAlgebra;
    Q R S (g'.comp MvPolynomial.C)
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
g' : RingHom.{u, v} (MvPolynomial (Fin (n + 1)) R) S
hg :
  Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin (n + 1)) R) (β := S) (⇑g' : (a : MvPolynomial (Fin (n + 1)) R) → S)
hg' : Ideal.FG (ker g')
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] MvPolynomial (Fin n) R[X] :=
  AlgEquiv.trans (MvPolynomial.renameEquiv R (finSuccEquiv n)) (MvPolynomial.optionEquivRight R (Fin n))
⊢ Eq (α := Ideal (MvPolynomial (Fin n) R[X]))
    (Ideal.comap (F := MvPolynomial (Fin n) R[X] →+* MvPolynomial (Fin (n + 1)) R)
      (↑e.symm : MvPolynomial (Fin n) R[X] →+* MvPolynomial (Fin (n + 1)) R) (ker g'))
    (Ideal.map (↑e : MvPolynomial (Fin (n + 1)) R →ₐ[R] MvPolynomial (Fin n) R[X]).toRingHom (ker g'))

Tactic:
Ideal.comap_symm e.toRingEquiv

Premises used: Ideal.comap_symm, Ideal.map, RingHomClass.toRingHom, AlgEquiv.toRingEquiv, Ideal.comap
-- 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)
n : ℕ
IH :
  ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_2 : CommRing S] (g' : RingHom.{u, v} (MvPolynomial (Fin n) 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')),
    let this := (g'.comp MvPolynomial.C).toAlgebra;
    Q R S (g'.comp MvPolynomial.C)
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
g' : RingHom.{u, v} (MvPolynomial (Fin (n + 1)) R) S
hg :
  Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin (n + 1)) R) (β := S) (⇑g' : (a : MvPolynomial (Fin (n + 1)) R) → S)
hg' : Ideal.FG (ker g')
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] MvPolynomial (Fin n) R[X] :=
  AlgEquiv.trans (MvPolynomial.renameEquiv R (finSuccEquiv n)) (MvPolynomial.optionEquivRight R (Fin n))
⊢ Eq (α := Ideal (MvPolynomial (Fin n) R[X]))
    (Ideal.comap (F := MvPolynomial (Fin n) R[X] →+* MvPolynomial (Fin (n + 1)) R)
      (↑e.symm : MvPolynomial (Fin n) R[X] →+* MvPolynomial (Fin (n + 1)) R) (ker g'))
    (Ideal.map (↑e : MvPolynomial (Fin (n + 1)) R →ₐ[R] MvPolynomial (Fin n) R[X]).toRingHom (ker g'))

Tactic:
exact Ideal.comap_symm e.toRingEquiv

Premises used: Ideal.comap_symm, AlgEquiv.toRingEquiv