awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
⊢ FinitePresentation R B
have obtain : ∀ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] A)
  (hf :
    Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
      Ideal.FG (RingHom.ker f.toRingHom)),
  FinitePresentation R B
Tactic: obtain ⟨n, f, hf⟩ := FinitePresentation.out (R := R) (A := A)
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
⊢ FinitePresentation R B
have h : Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B)
    (⇑((↑e : A →ₐ[R] B).comp f) : (a : MvPolynomial (Fin n) R) → B) ∧
  Ideal.FG (RingHom.ker ((↑e : A →ₐ[R] B).comp f).toRingHom)
Tactic: use n, AlgHom.comp (↑e) f
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
⊢ Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B)
      (⇑((↑e : A →ₐ[R] B).comp f) : (a : MvPolynomial (Fin n) R) → B) ∧
    Ideal.FG (RingHom.ker ((↑e : A →ₐ[R] B).comp f).toRingHom)
have h : Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B)
  (⇑((↑e : A →ₐ[R] B).comp f) : (a : MvPolynomial (Fin n) R) → B)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
h :
  Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B)
    (⇑((↑e : A →ₐ[R] B).comp f) : (a : MvPolynomial (Fin n) R) → B)
⊢ Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B)
      (⇑((↑e : A →ₐ[R] B).comp f) : (a : MvPolynomial (Fin n) R) → B) ∧
    Ideal.FG (RingHom.ker ((↑e : A →ₐ[R] B).comp f).toRingHom)
have h₁ : Ideal.FG (RingHom.ker ((↑e : A →ₐ[R] B).comp f).toRingHom)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
⊢ Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B)
    (⇑((↑e : A →ₐ[R] B).comp f) : (a : MvPolynomial (Fin n) R) → B)
have h : Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B)
  (Function.comp.{w₁ + 1, w₂ + 1, w₃ + 1} (β := A) (⇑(↑e : A →ₐ[R] B) : (a : A) → B)
    (⇑f : (a : MvPolynomial (Fin n) R) → A))
Tactic: rw [AlgHom.coe_comp]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
this :
  Eq (α := Ideal (MvPolynomial (Fin n) R)) (RingHom.ker ((↑e : A →ₐ[R] B).comp f).toRingHom) (RingHom.ker f.toRingHom)
⊢ Ideal.FG (RingHom.ker ((↑e : A →ₐ[R] B).comp f).toRingHom)
have rw : Ideal.FG (RingHom.ker f.toRingHom)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
⊢ Ideal.FG (RingHom.ker ((↑e : A →ₐ[R] B).comp f).toRingHom)
have h : Eq (α := Ideal (MvPolynomial (Fin n) R)) (RingHom.ker ((↑e : A →ₐ[R] B).comp f).toRingHom) (RingHom.ker f.toRingHom)
Tactic: suffices (RingHom.ker (AlgHom.comp (e : A →ₐ[R] B) f).toRingHom) = RingHom.ker f.toRingHom by
    rw [this]
    exact hf.2
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (hypothesis)
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
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
⊢ ((↑e : A →ₐ[R] B).comp f).toRingHom = RingHom.comp (↑e.toRingEquiv : A →+* B) f.toRingHom
have h : ((↑e : A →ₐ[R] B).comp f).toRingHom = (↑e : A →ₐ[R] B).comp f.toRingHom
Tactic: have h : (AlgHom.comp (e : A →ₐ[R] B) f).toRingHom =
      e.toAlgHom.toRingHom.comp f.toRingHom := rfl
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (hypothesis)
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
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
h : ((↑e : A →ₐ[R] B).comp f).toRingHom = (↑e : A →ₐ[R] B).comp f.toRingHom
⊢ ((↑e : A →ₐ[R] B).comp f).toRingHom = RingHom.comp (↑e.toRingEquiv : A →+* B) f.toRingHom
have h1 : (↑e.toRingEquiv : A →+* B) = (↑e : A →ₐ[R] B).toRingHom
Tactic: have h1 : ↑e.toRingEquiv = e.toAlgHom.toRingHom := rfl
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
h : ((↑e : A →ₐ[R] B).comp f).toRingHom = (↑e : A →ₐ[R] B).comp f.toRingHom
h1 : (↑e.toRingEquiv : A →+* B) = (↑e : A →ₐ[R] B).toRingHom
⊢ ((↑e : A →ₐ[R] B).comp f).toRingHom = RingHom.comp (↑e.toRingEquiv : A →+* B) f.toRingHom
have rw : (↑e : A →ₐ[R] B).comp f.toRingHom = RingHom.comp (↑e.toRingEquiv : A →+* B) f.toRingHom
Tactic: rw [h, h1]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
h : ((↑e : A →ₐ[R] B).comp f).toRingHom = (↑e : A →ₐ[R] B).comp f.toRingHom
h1 : (↑e.toRingEquiv : A →+* B) = (↑e : A →ₐ[R] B).toRingHom
rw : (↑e : A →ₐ[R] B).comp f.toRingHom = RingHom.comp (↑e.toRingEquiv : A →+* B) f.toRingHom
⊢ ((↑e : A →ₐ[R] B).comp f).toRingHom = RingHom.comp (↑e.toRingEquiv : A →+* B) f.toRingHom
have rw₁ : (↑e : A →ₐ[R] B).comp f.toRingHom = (↑e : A →ₐ[R] B).comp f.toRingHom
Tactic: rw [h, h1]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (hypothesis)
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
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
⊢ Eq (α := Ideal (MvPolynomial (Fin n) R)) (RingHom.ker ((↑e : A →ₐ[R] B).comp f).toRingHom) (RingHom.ker f.toRingHom)
have hco : ((↑e : A →ₐ[R] B).comp f).toRingHom = RingHom.comp (↑e.toRingEquiv : A →+* B) f.toRingHom
Tactic: have hco : (AlgHom.comp (e : A →ₐ[R] B) f).toRingHom = RingHom.comp (e.toRingEquiv : A ≃+* B)
    f.toRingHom := by
    have h : (AlgHom.comp (e : A →ₐ[R] B) f).toRingHom =
      e.toAlgHom.toRingHom.comp f.toRingHom := rfl
    have h1 : ↑e.toRingEquiv = e.toAlgHom.toRingHom := rfl
    rw [h, h1]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
hco : ((↑e : A →ₐ[R] B).comp f).toRingHom = RingHom.comp (↑e.toRingEquiv : A →+* B) f.toRingHom
⊢ Eq (α := Ideal (MvPolynomial (Fin n) R)) (RingHom.ker ((↑e : A →ₐ[R] B).comp f).toRingHom) (RingHom.ker f.toRingHom)
have h : Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.comap ((↑e : A →ₐ[R] B).comp f).toRingHom ⊥) (RingHom.ker f.toRingHom)
Tactic: rw [RingHom.ker_eq_comap_bot, hco, ← Ideal.comap_comap, ← RingHom.ker_eq_comap_bot,
    RingHom.ker_coe_equiv (AlgEquiv.toRingEquiv e), RingHom.ker_eq_comap_bot]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
hco : ((↑e : A →ₐ[R] B).comp f).toRingHom = RingHom.comp (↑e.toRingEquiv : A →+* B) f.toRingHom
h :
  Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.comap ((↑e : A →ₐ[R] B).comp f).toRingHom ⊥) (RingHom.ker f.toRingHom)
⊢ Eq (α := Ideal (MvPolynomial (Fin n) R)) (RingHom.ker ((↑e : A →ₐ[R] B).comp f).toRingHom) (RingHom.ker f.toRingHom)
have h₁ : Eq (α := Ideal (MvPolynomial (Fin n) R))
  (Ideal.comap (F := RingHom.{w₁, w₃} (MvPolynomial (Fin n) R) B) (RingHom.comp (↑e.toRingEquiv : A →+* B) f.toRingHom)
    ⊥)
  (RingHom.ker f.toRingHom)
Tactic: rw [RingHom.ker_eq_comap_bot, hco, ← Ideal.comap_comap, ← RingHom.ker_eq_comap_bot,
    RingHom.ker_coe_equiv (AlgEquiv.toRingEquiv e), RingHom.ker_eq_comap_bot]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
hco : ((↑e : A →ₐ[R] B).comp f).toRingHom = RingHom.comp (↑e.toRingEquiv : A →+* B) f.toRingHom
h :
  Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.comap ((↑e : A →ₐ[R] B).comp f).toRingHom ⊥) (RingHom.ker f.toRingHom)
h₁ :
  Eq (α := Ideal (MvPolynomial (Fin n) R))
    (Ideal.comap (F := RingHom.{w₁, w₃} (MvPolynomial (Fin n) R) B)
      (RingHom.comp (↑e.toRingEquiv : A →+* B) f.toRingHom) ⊥)
    (RingHom.ker f.toRingHom)
⊢ Eq (α := Ideal (MvPolynomial (Fin n) R)) (RingHom.ker ((↑e : A →ₐ[R] B).comp f).toRingHom) (RingHom.ker f.toRingHom)
have h₂ : Eq (α := Ideal (MvPolynomial (Fin n) R))
  (Ideal.comap f.toRingHom (Ideal.comap (F := A →+* B) (↑e.toRingEquiv : A →+* B) ⊥)) (RingHom.ker f.toRingHom)
Tactic: rw [RingHom.ker_eq_comap_bot, hco, ← Ideal.comap_comap, ← RingHom.ker_eq_comap_bot,
    RingHom.ker_coe_equiv (AlgEquiv.toRingEquiv e), RingHom.ker_eq_comap_bot]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
hco : ((↑e : A →ₐ[R] B).comp f).toRingHom = RingHom.comp (↑e.toRingEquiv : A →+* B) f.toRingHom
h :
  Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.comap ((↑e : A →ₐ[R] B).comp f).toRingHom ⊥) (RingHom.ker f.toRingHom)
h₁ :
  Eq (α := Ideal (MvPolynomial (Fin n) R))
    (Ideal.comap (F := RingHom.{w₁, w₃} (MvPolynomial (Fin n) R) B)
      (RingHom.comp (↑e.toRingEquiv : A →+* B) f.toRingHom) ⊥)
    (RingHom.ker f.toRingHom)
h₂ :
  Eq (α := Ideal (MvPolynomial (Fin n) R))
    (Ideal.comap f.toRingHom (Ideal.comap (F := A →+* B) (↑e.toRingEquiv : A →+* B) ⊥)) (RingHom.ker f.toRingHom)
⊢ Eq (α := Ideal (MvPolynomial (Fin n) R)) (RingHom.ker ((↑e : A →ₐ[R] B).comp f).toRingHom) (RingHom.ker f.toRingHom)
have h₃ : Eq (α := Ideal (MvPolynomial (Fin n) R))
  (Ideal.comap f.toRingHom (RingHom.ker (F := A →+* B) (↑e.toRingEquiv : A →+* B))) (RingHom.ker f.toRingHom)
Tactic: rw [RingHom.ker_eq_comap_bot, hco, ← Ideal.comap_comap, ← RingHom.ker_eq_comap_bot,
    RingHom.ker_coe_equiv (AlgEquiv.toRingEquiv e), RingHom.ker_eq_comap_bot]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
hco : ((↑e : A →ₐ[R] B).comp f).toRingHom = RingHom.comp (↑e.toRingEquiv : A →+* B) f.toRingHom
h :
  Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.comap ((↑e : A →ₐ[R] B).comp f).toRingHom ⊥) (RingHom.ker f.toRingHom)
h₁ :
  Eq (α := Ideal (MvPolynomial (Fin n) R))
    (Ideal.comap (F := RingHom.{w₁, w₃} (MvPolynomial (Fin n) R) B)
      (RingHom.comp (↑e.toRingEquiv : A →+* B) f.toRingHom) ⊥)
    (RingHom.ker f.toRingHom)
h₂ :
  Eq (α := Ideal (MvPolynomial (Fin n) R))
    (Ideal.comap f.toRingHom (Ideal.comap (F := A →+* B) (↑e.toRingEquiv : A →+* B) ⊥)) (RingHom.ker f.toRingHom)
h₃ :
  Eq (α := Ideal (MvPolynomial (Fin n) R))
    (Ideal.comap f.toRingHom (RingHom.ker (F := A →+* B) (↑e.toRingEquiv : A →+* B))) (RingHom.ker f.toRingHom)
⊢ Eq (α := Ideal (MvPolynomial (Fin n) R)) (RingHom.ker ((↑e : A →ₐ[R] B).comp f).toRingHom) (RingHom.ker f.toRingHom)
have h₄ : Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.comap f.toRingHom ⊥) (RingHom.ker f.toRingHom)
Tactic: rw [RingHom.ker_eq_comap_bot, hco, ← Ideal.comap_comap, ← RingHom.ker_eq_comap_bot,
    RingHom.ker_coe_equiv (AlgEquiv.toRingEquiv e), RingHom.ker_eq_comap_bot]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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
inst_5 : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
hco : ((↑e : A →ₐ[R] B).comp f).toRingHom = RingHom.comp (↑e.toRingEquiv : A →+* B) f.toRingHom
h :
  Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.comap ((↑e : A →ₐ[R] B).comp f).toRingHom ⊥) (RingHom.ker f.toRingHom)
h₁ :
  Eq (α := Ideal (MvPolynomial (Fin n) R))
    (Ideal.comap (F := RingHom.{w₁, w₃} (MvPolynomial (Fin n) R) B)
      (RingHom.comp (↑e.toRingEquiv : A →+* B) f.toRingHom) ⊥)
    (RingHom.ker f.toRingHom)
h₂ :
  Eq (α := Ideal (MvPolynomial (Fin n) R))
    (Ideal.comap f.toRingHom (Ideal.comap (F := A →+* B) (↑e.toRingEquiv : A →+* B) ⊥)) (RingHom.ker f.toRingHom)
h₃ :
  Eq (α := Ideal (MvPolynomial (Fin n) R))
    (Ideal.comap f.toRingHom (RingHom.ker (F := A →+* B) (↑e.toRingEquiv : A →+* B))) (RingHom.ker f.toRingHom)
h₄ : Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.comap f.toRingHom ⊥) (RingHom.ker f.toRingHom)
⊢ Eq (α := Ideal (MvPolynomial (Fin n) R)) (RingHom.ker ((↑e : A →ₐ[R] B).comp f).toRingHom) (RingHom.ker f.toRingHom)
have h₅ : Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.comap f.toRingHom ⊥) (Ideal.comap f.toRingHom ⊥)
Tactic: rw [RingHom.ker_eq_comap_bot, hco, ← Ideal.comap_comap, ← RingHom.ker_eq_comap_bot,
    RingHom.ker_coe_equiv (AlgEquiv.toRingEquiv e), RingHom.ker_eq_comap_bot]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
R : Type w₁
inst : CommRing R
ι : Type u_1
inst_1 : Finite ι
⊢ ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial ι R),
    Surjective (α := MvPolynomial (Fin n) R) (β := MvPolynomial ι R)
        (⇑f : (a : MvPolynomial (Fin n) R) → MvPolynomial ι R) ∧
      Ideal.FG (RingHom.ker f.toRingHom)
have intro : ∀ (val : Fintype ι),
  ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] MvPolynomial ι R),
    Surjective (α := MvPolynomial (Fin n) R) (β := MvPolynomial ι R)
        (⇑f : (a : MvPolynomial (Fin n) R) → MvPolynomial ι R) ∧
      Ideal.FG (RingHom.ker f.toRingHom)
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
I : Ideal A
h : I.FG
inst_3 : FinitePresentation R A
⊢ ∃ (n : ℕ) (f : AlgHom.{w₁, w₁, w₂} R (MvPolynomial (Fin n) R) (A ⧸ I)),
    Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A ⧸ I) (⇑f : (a : MvPolynomial (Fin n) R) → A ⧸ I) ∧
      Ideal.FG (RingHom.ker f.toRingHom)
have obtain : ∀ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] A)
  (hf :
    Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
      Ideal.FG (RingHom.ker f.toRingHom)),
  ∃ (n : ℕ) (f : AlgHom.{w₁, w₁, w₂} R (MvPolynomial (Fin n) R) (A ⧸ I)),
    Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A ⧸ I) (⇑f : (a : MvPolynomial (Fin n) R) → A ⧸ I) ∧
      Ideal.FG (RingHom.ker f.toRingHom)
Tactic: obtain ⟨n, f, hf⟩ := FinitePresentation.out (R := R) (A := A)
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
I : Ideal A
h : I.FG
inst_3 : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
⊢ ∃ (n : ℕ) (f : AlgHom.{w₁, w₁, w₂} R (MvPolynomial (Fin n) R) (A ⧸ I)),
    Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A ⧸ I) (⇑f : (a : MvPolynomial (Fin n) R) → A ⧸ I) ∧
      Ideal.FG (RingHom.ker f.toRingHom)
have refine_1 : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A ⧸ I)
  (⇑(AlgHom.comp (Ideal.Quotient.mkₐ R I) f) : (a : MvPolynomial (Fin n) R) → A ⧸ I)
Tactic: refine ⟨n, (Ideal.Quotient.mkₐ R I).comp f, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
I : Ideal A
h : I.FG
inst_3 : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
refine_1 :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A ⧸ I)
    (⇑(AlgHom.comp (Ideal.Quotient.mkₐ R I) f) : (a : MvPolynomial (Fin n) R) → A ⧸ I)
⊢ ∃ (n : ℕ) (f : AlgHom.{w₁, w₁, w₂} R (MvPolynomial (Fin n) R) (A ⧸ I)),
    Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A ⧸ I) (⇑f : (a : MvPolynomial (Fin n) R) → A ⧸ I) ∧
      Ideal.FG (RingHom.ker f.toRingHom)
have refine_2 : Ideal.FG
  (RingHom.ker (F := RingHom.{w₁, w₂} (MvPolynomial (Fin n) R) (A ⧸ I))
    (AlgHom.toRingHom (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)))
Tactic: refine ⟨n, (Ideal.Quotient.mkₐ R I).comp f, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
I : Ideal A
h : I.FG
inst_3 : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf :
  Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A) ∧
    Ideal.FG (RingHom.ker f.toRingHom)
⊢ Ideal.FG
    (RingHom.ker (F := RingHom.{w₁, w₂} (MvPolynomial (Fin n) R) (A ⧸ I))
      (AlgHom.toRingHom (AlgHom.comp (Ideal.Quotient.mkₐ R I) f)))
have refine_2 : Ideal.FG (RingHom.ker (F := A →+* A ⧸ I) (AlgHom.toRingHom (Ideal.Quotient.mkₐ R I)))
Tactic: refine Ideal.fg_ker_comp _ _ hf.2 ?_ hf.1
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
⊢ FinitePresentation R A ↔
    ∃ (n : ℕ) (I : Ideal (MvPolynomial (Fin n) R)) (x : (MvPolynomial (Fin n) R ⧸ I) ≃ₐ[R] A), I.FG
have mp : FinitePresentation R A → ∃ (n : ℕ) (I : Ideal (MvPolynomial (Fin n) R)) (x : (MvPolynomial (Fin n) R ⧸ I) ≃ₐ[R] A), I.FG
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
mp :
  FinitePresentation R A →
    ∃ (n : ℕ) (I : Ideal (MvPolynomial (Fin n) R)) (x : (MvPolynomial (Fin n) R ⧸ I) ≃ₐ[R] A), I.FG
⊢ FinitePresentation R A ↔
    ∃ (n : ℕ) (I : Ideal (MvPolynomial (Fin n) R)) (x : (MvPolynomial (Fin n) R ⧸ I) ≃ₐ[R] A), I.FG
have mpr : (∃ (n : ℕ) (I : Ideal (MvPolynomial (Fin n) R)) (x : (MvPolynomial (Fin n) R ⧸ I) ≃ₐ[R] A), I.FG) →
  FinitePresentation R A
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
R : Type w₁
A : Type w₂
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
⊢ FinitePresentation R A ↔
    ∃ (ι : Type u_1) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] A),
      Surjective (α := MvPolynomial ι R) (β := A) (⇑f : (a : MvPolynomial ι R) → A) ∧ Ideal.FG (RingHom.ker f.toRingHom)
have mp : FinitePresentation R A →
  ∃ (ι : Type u_1) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] A),
    Surjective (α := MvPolynomial ι R) (β := A) (⇑f : (a : MvPolynomial ι R) → A) ∧ Ideal.FG (RingHom.ker f.toRingHom)
Tactic: constructor