awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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
⊢ Q R S f
have 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
Tactic: obtain ⟨n, g, hg, hg'⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (hypothesis)
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
⊢ Q R S f
have hg₁ : Surjective.{u + 1, v + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑g' : (a : MvPolynomial (Fin n) R) → S)
Tactic: change Surjective g' at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (hypothesis)
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')
⊢ Q R S f
have this₁ : g'.comp MvPolynomial.C = f
Tactic: have : g'.comp MvPolynomial.C = f := g.comp_algebraMap
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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
⊢ Q R S f
have 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
Tactic: clear_value g'
Cleared hypotheses: g', hg, hg', this
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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
⊢ Q R S f
have subst : ∀ (g : MvPolynomial (Fin n) R →ₐ[R] S), Q R S (g'.comp MvPolynomial.C)
Tactic: subst this
Cleared hypotheses: f, this_1, g, this
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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)
have zero : Ideal.FG (ker (g'.comp MvPolynomial.C))
Tactic: refine fg_ker _ _ _ (hg.comp (MvPolynomial.C_surjective (Fin 0))) ?_
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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 (ker (g'.comp MvPolynomial.C))
have zero : Ideal.FG (Ideal.comap (F := R →+* MvPolynomial (Fin 0) R) MvPolynomial.C (ker g'))
Tactic: rw [← comap_ker]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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 (Ideal.comap (F := R →+* MvPolynomial (Fin 0) R) MvPolynomial.C (ker g'))
have 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'))
Tactic: convert! hg'.map (MvPolynomial.isEmptyRingEquiv R (Fin 0)).toRingHom using 1
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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) (RingEquiv.toRingHom (MvPolynomial.isEmptyRingEquiv R (Fin 0)))
      (ker g'))
have 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'))
Tactic: simp only [RingEquiv.toRingHom_eq_coe]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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)))
have 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'))
Tactic: rw [← RingHom.comap_ker]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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
    (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'))
have 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'))
Tactic: convert! hg'.map e.toAlgHom.toRingHom using 1
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (hypothesis)
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))
⊢ Q R S (g'.comp MvPolynomial.C)
have 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)))
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
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (hypothesis)
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 S (g'.comp MvPolynomial.C)
have this₁ : 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
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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 (g'.comp MvPolynomial.C)
have 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
Tactic: convert! comp _ _ _ _ _ (polynomial _) this using 1
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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)
⊢ g'.comp MvPolynomial.C =
    (RingHom.comp (g'.comp (↑e.symm : MvPolynomial (Fin n) R[X] →+* MvPolynomial (Fin (n + 1)) R)) MvPolynomial.C).comp
      C
have 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))
Tactic: rw [comp_assoc, comp_assoc]