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)
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
    (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:
have he : (ker (g'.comp <| RingHomClass.toRingHom e.symm)).FG := by
      rw [← RingHom.comap_ker]
      convert! hg'.map e.toAlgHom.toRingHom using 1
      exact Ideal.comap_symm e.toRingEquiv
-- 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))
he :
  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)))
⊢ Q R[X] S
    (RingHom.comp (g'.comp (↑e.symm : MvPolynomial (Fin n) R[X] →+* MvPolynomial (Fin (n + 1)) R)) MvPolynomial.C)

Tactic:
have := IH (R := R[X]) (S := S) (g'.comp e.symm) (hg.comp e.symm.surjective) he
-- 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_1 : 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))
he :
  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)))
this :
  Q R[X] S
    (RingHom.comp (g'.comp (↑e.symm : MvPolynomial (Fin n) R[X] →+* MvPolynomial (Fin (n + 1)) R)) MvPolynomial.C)
⊢ Q R S
    ((RingHom.comp (g'.comp (↑e.symm : MvPolynomial (Fin n) R[X] →+* MvPolynomial (Fin (n + 1)) R)) MvPolynomial.C).comp
      C)

Tactic:
comp _ _ _ _ _ (polynomial _) 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)
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_1 : 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))
he :
  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)))
this :
  Q R[X] S
    (RingHom.comp (g'.comp (↑e.symm : MvPolynomial (Fin n) R[X] →+* MvPolynomial (Fin (n + 1)) R)) MvPolynomial.C)
h :
  g'.comp MvPolynomial.C =
    (RingHom.comp (g'.comp (↑e.symm : MvPolynomial (Fin n) R[X] →+* MvPolynomial (Fin (n + 1)) R)) MvPolynomial.C).comp
      C
⊢ Q R S (g'.comp MvPolynomial.C)

Tactic:
convert! comp _ _ _ _ _ (polynomial _) this using 1
-- 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_1 : 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))
he :
  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)))
this :
  Q R[X] S
    (RingHom.comp (g'.comp (↑e.symm : MvPolynomial (Fin n) R[X] →+* MvPolynomial (Fin (n + 1)) R)) MvPolynomial.C)
h :
  g'.comp MvPolynomial.C =
    g'.comp
      (RingHom.comp (↑e.symm : MvPolynomial (Fin n) R[X] →+* MvPolynomial (Fin (n + 1)) R)
        (RingHom.comp MvPolynomial.C C))
⊢ g'.comp MvPolynomial.C =
    (RingHom.comp (g'.comp (↑e.symm : MvPolynomial (Fin n) R[X] →+* MvPolynomial (Fin (n + 1)) R)) MvPolynomial.C).comp
      C

Tactic:
rw [comp_assoc, comp_assoc]

Premises used: RingHom.comp_assoc
-- 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_1 : 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))
he :
  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)))
this :
  Q R[X] S
    (RingHom.comp (g'.comp (↑e.symm : MvPolynomial (Fin n) R[X] →+* MvPolynomial (Fin (n + 1)) R)) MvPolynomial.C)
h :
  ∀ (r : R) (m : Fin (n + 1) →₀ ℕ),
    Eq.{u + 1} (α := R) (MvPolynomial.coeff m ((MvPolynomial.C : (a : R) → MvPolynomial (Fin (n + 1)) R) r))
      (MvPolynomial.coeff m
        ((RingHom.comp (↑e.symm : MvPolynomial (Fin n) R[X] →+* MvPolynomial (Fin (n + 1)) R)
              (RingHom.comp MvPolynomial.C C) :
            (a : R) → MvPolynomial (Fin (n + 1)) R)
          r))
⊢ g'.comp MvPolynomial.C =
    g'.comp
      (RingHom.comp (↑e.symm : MvPolynomial (Fin n) R[X] →+* MvPolynomial (Fin (n + 1)) R)
        (RingHom.comp MvPolynomial.C C))

Tactic:
congr 1 with r
-- 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_1 : 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))
he :
  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)))
this :
  Q R[X] S
    (RingHom.comp (g'.comp (↑e.symm : MvPolynomial (Fin n) R[X] →+* MvPolynomial (Fin (n + 1)) R)) MvPolynomial.C)
r : R
m : Fin (n + 1) →₀ ℕ
⊢ Eq.{u + 1} (α := R) (MvPolynomial.coeff m ((MvPolynomial.C : (a : R) → MvPolynomial (Fin (n + 1)) R) r))
    (MvPolynomial.coeff m
      ((RingHom.comp (↑e.symm : MvPolynomial (Fin n) R[X] →+* MvPolynomial (Fin (n + 1)) R)
            (RingHom.comp MvPolynomial.C C) :
          (a : R) → MvPolynomial (Fin (n + 1)) R)
        r))

Tactic:
simp [e]
-- 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
n : ℕ
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 : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
zero :
  ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_2 : 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')), Q R S (g'.comp MvPolynomial.C)
succ :
  ∀ (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_2 : 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')), Q R S (g'.comp MvPolynomial.C)
⊢ Q R S (g'.comp MvPolynomial.C)

Tactic:
induction n generalizing R S with
  | zero =>
    refine fg_ker _ _ _ (hg.comp (MvPolynomial.C_surjective (Fin 0))) ?_
    rw [← comap_ker]
    convert! hg'.map (MvPolynomial.isEmptyRingEquiv R (Fin 0)).toRingHom using 1
    simp only [RingEquiv.toRingHom_eq_coe]
    exact Ideal.comap_symm (MvPolynomial.isEmptyRingEquiv R (Fin 0))
  | succ n IH =>
    let e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] MvPolynomial (Fin n) R[X] :=
      (MvPolynomial.renameEquiv R (finSuccEquiv n)).trans (MvPolynomial.optionEquivRight R (Fin n))
    have he : (ker (g'.comp <| RingHomClass.toRingHom e.symm)).FG := by
      rw [← RingHom.comap_ker]
      convert! hg'.map e.toAlgHom.toRingHom using 1
      exact Ideal.comap_symm e.toRingEquiv
    have := IH (R := R[X]) (S := S) (g'.comp e.symm) (hg.comp e.symm.surjective) he
    convert! comp _ _ _ _ _ (polynomial _) this using 1
    rw [comp_assoc, comp_assoc]
    congr 1 with r
    simp [e]

Premises used: Ideal.comap_symm, RingHom.comap_ker, RingHom.comp_assoc, Function.Surjective.comp, RingEquiv.toRingHom_eq_coe, OfNat.ofNat, Fin, MvPolynomial.isEmptyRingEquiv
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
hf : f.FinitePresentation
⊢ f.FiniteType

Tactic:
RingHom.FiniteType.of_finitePresentation hf

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

Tactic:
RingHom.FinitePresentation.id A

Premises used: AlgHom.FinitePresentation, RingHom.FinitePresentation.id
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : CommRing C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
g : B →ₐ[R] C
f : A →ₐ[R] B
hg : g.FinitePresentation
hf : f.FinitePresentation
⊢ (g.comp f).FinitePresentation

Tactic:
RingHom.FinitePresentation.comp hg hf

Premises used: AlgHom.FinitePresentation, RingHom.FinitePresentation.comp
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : CommRing C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
f : A →ₐ[R] B
g : B →ₐ[R] C
hf : f.FinitePresentation
hg : Surjective.{u_3 + 1, u_4 + 1} (α := B) (β := C) (⇑g : (a : B) → C)
hker : Ideal.FG (RingHom.ker g.toRingHom)
⊢ (g.comp f).FinitePresentation

Tactic:
RingHom.FinitePresentation.comp_surjective hf hg hker

Premises used: AlgHom.FinitePresentation, RingHom.FinitePresentation.comp_surjective
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
hf : Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hker : Ideal.FG (RingHom.ker f.toRingHom)
⊢ f.FinitePresentation

Tactic:
RingHom.FinitePresentation.of_surjective f hf hker

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, RingHom.FinitePresentation.of_surjective
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
hf : Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hker : Ideal.FG (RingHom.ker f.toRingHom)
⊢ f.FinitePresentation

Tactic:
convert! RingHom.FinitePresentation.of_surjective f hf hker

Premises used: RingHom.FinitePresentation.of_surjective
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : IsNoetherianRing A
f : A →ₐ[R] B
⊢ f.FiniteType ↔ f.FinitePresentation

Tactic:
RingHom.FinitePresentation.of_finiteType

Premises used: AlgHom.FinitePresentation, AlgHom.FiniteType, RingHom.FinitePresentation.of_finiteType
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : CommRing C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
f : A →ₐ[R] B
g : B →ₐ[R] C
h : (g.comp f).FinitePresentation
h' : f.FiniteType
⊢ g.FinitePresentation

Tactic:
h.of_comp_finiteType _ h'

Premises used: AlgHom.FinitePresentation, RingHom.FinitePresentation.of_comp_finiteType
-- Module: Mathlib.RingTheory.FiniteStability
Goal:
R : Type w₁
inst : CommRing R
A : Type w₂
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w₃
inst_3 : CommRing B
inst_4 : Algebra R B
σ : Type u_1
f : MvPolynomial σ R →ₐ[R] A
hf : Function.Surjective (α := MvPolynomial σ R) (β := A) (⇑f : (a : MvPolynomial σ R) → A)
change :
  Function.Surjective (α := B ⊗[R] MvPolynomial σ R) (β := B ⊗[R] A)
    (⇑(TensorProduct.map (AlgHom.id R B) f : B ⊗[R] MvPolynomial σ R →ₐ[R] B ⊗[R] A) :
      (a : B ⊗[R] MvPolynomial σ R) → B ⊗[R] A)
⊢ Function.Surjective (α := B ⊗[R] MvPolynomial σ R) (β := B ⊗[R] A)
    (⇑(TensorProduct.map (AlgHom.id B B) f : B ⊗[R] MvPolynomial σ R →ₐ[B] B ⊗[R] A) :
      (a : B ⊗[R] MvPolynomial σ R) → B ⊗[R] A)

Tactic:
change Function.Surjective (TensorProduct.map (AlgHom.id R B) f)

Premises used: Algebra.TensorProduct.map, AlgHom.id, DFunLike.coe, Function.Surjective
-- Module: Mathlib.RingTheory.FiniteStability
Goal:
R : Type w₁
inst : CommRing R
A : Type w₂
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w₃
inst_3 : CommRing B
inst_4 : Algebra R B
σ : Type u_1
f : MvPolynomial σ R →ₐ[R] A
hf : Function.Surjective (α := MvPolynomial σ R) (β := A) (⇑f : (a : MvPolynomial σ R) → A)
hf₁ : Function.Surjective (α := B) (β := B) (⇑(AlgHom.id R B) : (a : B) → B)
hg : Function.Surjective (α := MvPolynomial σ R) (β := A) (⇑f : (a : MvPolynomial σ R) → A)
⊢ Function.Surjective (α := B ⊗[R] MvPolynomial σ R) (β := B ⊗[R] A)
    (⇑(TensorProduct.map (AlgHom.id R B) f : B ⊗[R] MvPolynomial σ R →ₐ[R] B ⊗[R] A) :
      (a : B ⊗[R] MvPolynomial σ R) → B ⊗[R] A)

Tactic:
apply TensorProduct.map_surjective

Premises used: Algebra.TensorProduct.map_surjective
-- Module: Mathlib.RingTheory.FiniteStability
Goal:
R : Type w₁
inst : CommRing R
A : Type w₂
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w₃
inst_3 : CommRing B
inst_4 : Algebra R B
σ : Type u_1
f : MvPolynomial σ R →ₐ[R] A
hf : Function.Surjective (α := MvPolynomial σ R) (β := A) (⇑f : (a : MvPolynomial σ R) → A)
⊢ Function.Surjective (α := B) (β := B) (⇑(AlgHom.id R B) : (a : B) → B)

Tactic:
Function.RightInverse.surjective (congrFun rfl)

Premises used: congrFun, Function.RightInverse.surjective, rfl
-- Module: Mathlib.RingTheory.FiniteStability
Goal:
R : Type w₁
inst : CommRing R
A : Type w₂
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w₃
inst_3 : CommRing B
inst_4 : Algebra R B
σ : Type u_1
f : MvPolynomial σ R →ₐ[R] A
hf : Function.Surjective (α := MvPolynomial σ R) (β := A) (⇑f : (a : MvPolynomial σ R) → A)
⊢ Function.Surjective (α := B) (β := B) (⇑(AlgHom.id R B) : (a : B) → B)

Tactic:
exact Function.RightInverse.surjective (congrFun rfl)

Premises used: congrFun, Function.RightInverse.surjective, rfl