awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
inst_3 : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin m) R) (β := A) (⇑f' : (a : MvPolynomial (Fin m) R) → A)
s : Finset (MvPolynomial (Fin m) R)
hs :
  Eq (α := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R))) (RingHom.ker f'.toRingHom)
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : (i : Fin n) → MvPolynomial (Fin m) R
hg :
  ∀ (i : Fin n),
    Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) (g i) : A)
      ((f : (a : MvPolynomial (Fin n) R) → A) (MvPolynomial.X i) : A)
h : (i : Fin m) → MvPolynomial (Fin n) R
hh :
  ∀ (i : Fin m),
    Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) (h i) : A)
      ((f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) : A)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn :=
  fun (i : Fin n) ↦
    HSub.hSub (α := MvPolynomial (Fin n) R) (β := RXn) (MvPolynomial.X i) ((aeval_h : (a : RXm) → RXn) (g i) : RXn)
hh' :
  ∀ (x : RXm),
    Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) ((aeval_h : (a : RXm) → RXn) x : RXn) : A)
      ((f' : (a : MvPolynomial (Fin m) R) → A) x : A)
s' : Set RXn := Set.range g' ∪ (⇑aeval_h : (a : RXm) → RXn) '' (↑s : Set RXm)
leI : LE.le (α := Ideal RXn) (Ideal.span s') (RingHom.ker f.toRingHom)
x : RXm
y : RXn
hy : Membership.mem (γ := AddSubmonoid RXn) (Submodule.toAddSubmonoid (Ideal.span s')) y
this_1 :
  HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x : RXn) y ∈
    aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
hx : Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) x : A) (0 : A)
this : LE.le (α := Ideal RXm) (Ideal.span (↑s : Set RXm)) (Ideal.comap aeval_h (Ideal.span s'))
⊢ Membership.mem (α := RXn) (γ := Submodule RXn RXn) (Ideal.span s') ((aeval_h.toRingHom : (a : RXm) → RXn) x : RXn)
have a : Membership.mem (γ := Submodule RXm RXm) (Ideal.span (↑s : Set RXm)) x
Tactic: apply this
-- 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
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
inst_3 : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin m) R) (β := A) (⇑f' : (a : MvPolynomial (Fin m) R) → A)
s : Finset (MvPolynomial (Fin m) R)
hs :
  Eq (α := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R))) (RingHom.ker f'.toRingHom)
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : (i : Fin n) → MvPolynomial (Fin m) R
hg :
  ∀ (i : Fin n),
    Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) (g i) : A)
      ((f : (a : MvPolynomial (Fin n) R) → A) (MvPolynomial.X i) : A)
h : (i : Fin m) → MvPolynomial (Fin n) R
hh :
  ∀ (i : Fin m),
    Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) (h i) : A)
      ((f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) : A)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn :=
  fun (i : Fin n) ↦
    HSub.hSub (α := MvPolynomial (Fin n) R) (β := RXn) (MvPolynomial.X i) ((aeval_h : (a : RXm) → RXn) (g i) : RXn)
hh' :
  ∀ (x : RXm),
    Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) ((aeval_h : (a : RXm) → RXn) x : RXn) : A)
      ((f' : (a : MvPolynomial (Fin m) R) → A) x : A)
s' : Set RXn := Set.range g' ∪ (⇑aeval_h : (a : RXm) → RXn) '' (↑s : Set RXm)
leI : LE.le (α := Ideal RXn) (Ideal.span s') (RingHom.ker f.toRingHom)
x : RXm
y : RXn
hy : Membership.mem (γ := AddSubmonoid RXn) (Submodule.toAddSubmonoid (Ideal.span s')) y
this_1 :
  HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x : RXn) y ∈
    aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
hx : Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) x : A) (0 : A)
this : LE.le (α := Ideal RXm) (Ideal.span (↑s : Set RXm)) (Ideal.comap aeval_h (Ideal.span s'))
⊢ Membership.mem (γ := Submodule RXm RXm) (Ideal.span (↑s : Set RXm)) x
have a : Membership.mem (γ := Submodule RXm RXm) (RingHom.ker f'.toRingHom) x
Tactic: rwa [hs]
-- 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
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
inst_3 : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin m) R) (β := A) (⇑f' : (a : MvPolynomial (Fin m) R) → A)
s : Finset (MvPolynomial (Fin m) R)
hs :
  Eq (α := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R))) (RingHom.ker f'.toRingHom)
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : (i : Fin n) → MvPolynomial (Fin m) R
hg :
  ∀ (i : Fin n),
    Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) (g i) : A)
      ((f : (a : MvPolynomial (Fin n) R) → A) (MvPolynomial.X i) : A)
h : (i : Fin m) → MvPolynomial (Fin n) R
hh :
  ∀ (i : Fin m),
    Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) (h i) : A)
      ((f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) : A)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn :=
  fun (i : Fin n) ↦
    HSub.hSub (α := MvPolynomial (Fin n) R) (β := RXn) (MvPolynomial.X i) ((aeval_h : (a : RXm) → RXn) (g i) : RXn)
hh' :
  ∀ (x : RXm),
    Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) ((aeval_h : (a : RXm) → RXn) x : RXn) : A)
      ((f' : (a : MvPolynomial (Fin m) R) → A) x : A)
s' : Set RXn := Set.range g' ∪ (⇑aeval_h : (a : RXm) → RXn) '' (↑s : Set RXm)
leI : LE.le (α := Ideal RXn) (Ideal.span s') (RingHom.ker f.toRingHom)
x : RXm
y : RXn
hy : Membership.mem (γ := AddSubmonoid RXn) (Submodule.toAddSubmonoid (Ideal.span s')) y
this :
  HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x : RXn) y ∈
    aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
hx : Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) x : A) (0 : A)
⊢ Membership.mem (α := RXn) (γ := Submodule RXn RXn) (Ideal.span s') ((aeval_h.toRingHom : (a : RXm) → RXn) x : RXn)
have suffices : LE.le (α := Ideal RXm) (Ideal.span (↑s : Set RXm)) (Ideal.comap aeval_h (Ideal.span s'))
Tactic: suffices Ideal.span (s : Set RXm) ≤ (Ideal.span s').comap aeval_h by
      apply this
      rwa [hs]
-- 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
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
inst_3 : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin m) R) (β := A) (⇑f' : (a : MvPolynomial (Fin m) R) → A)
s : Finset (MvPolynomial (Fin m) R)
hs :
  Eq (α := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R))) (RingHom.ker f'.toRingHom)
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : (i : Fin n) → MvPolynomial (Fin m) R
hg :
  ∀ (i : Fin n),
    Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) (g i) : A)
      ((f : (a : MvPolynomial (Fin n) R) → A) (MvPolynomial.X i) : A)
h : (i : Fin m) → MvPolynomial (Fin n) R
hh :
  ∀ (i : Fin m),
    Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) (h i) : A)
      ((f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) : A)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn :=
  fun (i : Fin n) ↦
    HSub.hSub (α := MvPolynomial (Fin n) R) (β := RXn) (MvPolynomial.X i) ((aeval_h : (a : RXm) → RXn) (g i) : RXn)
hh' :
  ∀ (x : RXm),
    Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) ((aeval_h : (a : RXm) → RXn) x : RXn) : A)
      ((f' : (a : MvPolynomial (Fin m) R) → A) x : A)
s' : Set RXn := Set.range g' ∪ (⇑aeval_h : (a : RXm) → RXn) '' (↑s : Set RXm)
leI : LE.le (α := Ideal RXn) (Ideal.span s') (RingHom.ker f.toRingHom)
x : RXm
y : RXn
hy : Membership.mem (γ := AddSubmonoid RXn) (Submodule.toAddSubmonoid (Ideal.span s')) y
this :
  HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x : RXn) y ∈
    aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
hx : Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) x : A) (0 : A)
⊢ LE.le (α := Ideal RXm) (Ideal.span (↑s : Set RXm)) (Ideal.comap aeval_h (Ideal.span s'))
have rw : (↑s : Set RXm) ⊆ (↑(Ideal.comap aeval_h (Ideal.span s')) : Set RXm)
Tactic: rw [Ideal.span_le]
-- 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
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
inst_3 : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin m) R) (β := A) (⇑f' : (a : MvPolynomial (Fin m) R) → A)
s : Finset (MvPolynomial (Fin m) R)
hs :
  Eq (α := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R))) (RingHom.ker f'.toRingHom)
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : (i : Fin n) → MvPolynomial (Fin m) R
hg :
  ∀ (i : Fin n),
    Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) (g i) : A)
      ((f : (a : MvPolynomial (Fin n) R) → A) (MvPolynomial.X i) : A)
h : (i : Fin m) → MvPolynomial (Fin n) R
hh :
  ∀ (i : Fin m),
    Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) (h i) : A)
      ((f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) : A)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn :=
  fun (i : Fin n) ↦
    HSub.hSub (α := MvPolynomial (Fin n) R) (β := RXn) (MvPolynomial.X i) ((aeval_h : (a : RXm) → RXn) (g i) : RXn)
hh' :
  ∀ (x : RXm),
    Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) ((aeval_h : (a : RXm) → RXn) x : RXn) : A)
      ((f' : (a : MvPolynomial (Fin m) R) → A) x : A)
s' : Set RXn := Set.range g' ∪ (⇑aeval_h : (a : RXm) → RXn) '' (↑s : Set RXm)
leI : LE.le (α := Ideal RXn) (Ideal.span s') (RingHom.ker f.toRingHom)
x_1 : RXm
y : RXn
hy : Membership.mem (γ := AddSubmonoid RXn) (Submodule.toAddSubmonoid (Ideal.span s')) y
this :
  HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x_1 : RXn) y ∈
    aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
hx_1 : Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) x_1 : A) (0 : A)
x : RXm
hx : x ∈ (↑s : Set RXm)
⊢ x ∈ (↑(Ideal.comap aeval_h (Ideal.span s')) : Set RXm)
have a : Membership.mem (α := RXn) s' ((aeval_h : (a : RXm) → RXn) x : RXn)
Tactic: apply Submodule.subset_span
-- 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
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
inst_3 : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin m) R) (β := A) (⇑f' : (a : MvPolynomial (Fin m) R) → A)
s : Finset (MvPolynomial (Fin m) R)
hs :
  Eq (α := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R))) (RingHom.ker f'.toRingHom)
RXn : Type w₁ := MvPolynomial (Fin n) R
RXm : Type w₁ := MvPolynomial (Fin m) R
g : (i : Fin n) → MvPolynomial (Fin m) R
hg :
  ∀ (i : Fin n),
    Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) (g i) : A)
      ((f : (a : MvPolynomial (Fin n) R) → A) (MvPolynomial.X i) : A)
h : (i : Fin m) → MvPolynomial (Fin n) R
hh :
  ∀ (i : Fin m),
    Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) (h i) : A)
      ((f' : (a : MvPolynomial (Fin m) R) → A) (MvPolynomial.X i) : A)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn :=
  fun (i : Fin n) ↦
    HSub.hSub (α := MvPolynomial (Fin n) R) (β := RXn) (MvPolynomial.X i) ((aeval_h : (a : RXm) → RXn) (g i) : RXn)
hh' :
  ∀ (x : RXm),
    Eq.{w₂ + 1} (α := A) ((f : (a : MvPolynomial (Fin n) R) → A) ((aeval_h : (a : RXm) → RXn) x : RXn) : A)
      ((f' : (a : MvPolynomial (Fin m) R) → A) x : A)
s' : Set RXn := Set.range g' ∪ (⇑aeval_h : (a : RXm) → RXn) '' (↑s : Set RXm)
leI : LE.le (α := Ideal RXn) (Ideal.span s') (RingHom.ker f.toRingHom)
x_1 : RXm
y : RXn
hy : Membership.mem (γ := AddSubmonoid RXn) (Submodule.toAddSubmonoid (Ideal.span s')) y
this :
  HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x_1 : RXn) y ∈
    aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
hx_1 : Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) x_1 : A) (0 : A)
x : RXm
hx : x ∈ (↑s : Set RXm)
⊢ Membership.mem (α := RXn) s' ((aeval_h : (a : RXm) → RXn) x : RXn)
have a : Membership.mem (α := RXn) (γ := Set RXn) ((⇑aeval_h : (a : RXm) → RXn) '' (↑s : Set RXm))
  ((aeval_h : (a : RXm) → RXn) x : RXn)
Tactic: apply Set.mem_union_right
-- 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
f : A →ₐ[R] B
hf : Surjective.{w₂ + 1, w₃ + 1} (α := A) (β := B) (⇑f : (a : A) → B)
inst_5 : FinitePresentation R A
inst_6 : FinitePresentation R B
⊢ Ideal.FG (RingHom.ker f.toRingHom)
have obtain : ∀ (n : ℕ) (g : MvPolynomial (Fin n) R →ₐ[R] A)
  (hg : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑g : (a : MvPolynomial (Fin n) R) → A)),
  Ideal.FG (RingHom.ker g.toRingHom) → Ideal.FG (RingHom.ker f.toRingHom)
Tactic: obtain ⟨n, g, hg, _⟩ := 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
f : A →ₐ[R] B
hf : Surjective.{w₂ + 1, w₃ + 1} (α := A) (β := B) (⇑f : (a : A) → B)
inst_5 : FinitePresentation R A
inst_6 : FinitePresentation R B
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] A
hg : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑g : (a : MvPolynomial (Fin n) R) → A)
right : Ideal.FG (RingHom.ker g.toRingHom)
⊢ Ideal.FG (RingHom.ker f.toRingHom)
have h : Eq (α := Ideal A) (RingHom.ker f.toRingHom) (Ideal.map g.toRingHom (RingHom.ker (f.comp g).toRingHom))
Tactic: convert! (ker_fg_of_mvPolynomial (f.comp g) (hf.comp hg)).map g.toRingHom
-- 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
f : A →ₐ[R] B
hf : Surjective.{w₂ + 1, w₃ + 1} (α := A) (β := B) (⇑f : (a : A) → B)
inst_5 : FinitePresentation R A
inst_6 : FinitePresentation R B
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] A
hg : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑g : (a : MvPolynomial (Fin n) R) → A)
right : Ideal.FG (RingHom.ker g.toRingHom)
⊢ Eq (α := Ideal A) (RingHom.ker f.toRingHom) (Ideal.map g.toRingHom (RingHom.ker (f.comp g).toRingHom))
have h : Eq (α := Ideal A) (Ideal.comap (F := A →+* B) (↑f : A →+* B) ⊥)
  (Ideal.map (F := RingHom.{w₁, w₂} (MvPolynomial (Fin n) R) A) (↑g : MvPolynomial (Fin n) R →+* A)
    (Ideal.comap (F := RingHom.{w₁, w₃} (MvPolynomial (Fin n) R) B)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : A →+* B) (↑g : MvPolynomial (Fin n) R →+* A)) ⊥))
Tactic: simp_rw [RingHom.ker_eq_comap_bot, AlgHom.toRingHom_eq_coe, AlgHom.comp_toRingHom]
-- 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
f : A →ₐ[R] B
hf : Surjective.{w₂ + 1, w₃ + 1} (α := A) (β := B) (⇑f : (a : A) → B)
inst_5 : FinitePresentation R A
inst_6 : FinitePresentation R B
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] A
hg : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑g : (a : MvPolynomial (Fin n) R) → A)
right : Ideal.FG (RingHom.ker g.toRingHom)
⊢ Eq (α := Ideal A) (Ideal.comap (F := A →+* B) (↑f : A →+* B) ⊥)
    (Ideal.map (F := RingHom.{w₁, w₂} (MvPolynomial (Fin n) R) A) (↑g : MvPolynomial (Fin n) R →+* A)
      (Ideal.comap (F := RingHom.{w₁, w₃} (MvPolynomial (Fin n) R) B)
        (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : A →+* B) (↑g : MvPolynomial (Fin n) R →+* A)) ⊥))
have h : Eq (α := Ideal A) (Ideal.comap (F := A →+* B) (↑f : A →+* B) ⊥)
  (Ideal.map (F := RingHom.{w₁, w₂} (MvPolynomial (Fin n) R) A) (↑g : MvPolynomial (Fin n) R →+* A)
    (Ideal.comap (F := RingHom.{w₁, w₂} (MvPolynomial (Fin n) R) A) (↑g : MvPolynomial (Fin n) R →+* A)
      (Ideal.comap (F := A →+* B) (↑f : A →+* B) ⊥)))
Tactic: rw [← Ideal.comap_comap, Ideal.map_comap_of_surjective (g : MvPolynomial (Fin n) R →+* A) hg]
-- 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
f : A →ₐ[R] B
hf : Surjective.{w₂ + 1, w₃ + 1} (α := A) (β := B) (⇑f : (a : A) → B)
inst_5 : FinitePresentation R A
inst_6 : FinitePresentation R B
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] A
hg : Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑g : (a : MvPolynomial (Fin n) R) → A)
right : Ideal.FG (RingHom.ker g.toRingHom)
h :
  Eq (α := Ideal A) (Ideal.comap (F := A →+* B) (↑f : A →+* B) ⊥)
    (Ideal.map (F := RingHom.{w₁, w₂} (MvPolynomial (Fin n) R) A) (↑g : MvPolynomial (Fin n) R →+* A)
      (Ideal.comap (F := RingHom.{w₁, w₂} (MvPolynomial (Fin n) R) A) (↑g : MvPolynomial (Fin n) R →+* A)
        (Ideal.comap (F := A →+* B) (↑f : A →+* B) ⊥)))
⊢ Eq (α := Ideal A) (Ideal.comap (F := A →+* B) (↑f : A →+* B) ⊥)
    (Ideal.map (F := RingHom.{w₁, w₂} (MvPolynomial (Fin n) R) A) (↑g : MvPolynomial (Fin n) R →+* A)
      (Ideal.comap (F := RingHom.{w₁, w₃} (MvPolynomial (Fin n) R) B)
        (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : A →+* B) (↑g : MvPolynomial (Fin n) R →+* A)) ⊥))
have h₁ : Eq (α := Ideal A) (Ideal.comap (F := A →+* B) (↑f : A →+* B) ⊥) (Ideal.comap (F := A →+* B) (↑f : A →+* B) ⊥)
Tactic: rw [← Ideal.comap_comap, Ideal.map_comap_of_surjective (g : MvPolynomial (Fin n) R →+* A) hg]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
⊢ FinitePresentation (algebraMap A B) ↔ Algebra.FinitePresentation A B
have rw : Algebra.FinitePresentation A B ↔ Algebra.FinitePresentation A B
Tactic: rw [RingHom.FinitePresentation, toAlgebra_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
rw : Algebra.FinitePresentation A B ↔ Algebra.FinitePresentation A B
⊢ FinitePresentation (algebraMap A B) ↔ Algebra.FinitePresentation A B
have rw₁ : Algebra.FinitePresentation A B ↔ Algebra.FinitePresentation A B
Tactic: rw [RingHom.FinitePresentation, toAlgebra_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (hypothesis)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
f : A →+* B
g : B →+* C
hf : f.FinitePresentation
hg : Surjective.{u_2 + 1, u_3 + 1} (α := B) (β := C) (⇑g : (a : B) → C)
hker : Ideal.FG (ker g)
⊢ (g.comp f).FinitePresentation
have algebraizeInst : Algebra.FinitePresentation A B
Tactic: algebraize [f, g.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
hker : Ideal.FG (ker f)
⊢ f.FinitePresentation
have rw : (f.comp (RingHom.id A)).FinitePresentation
Tactic: rw [← f.comp_id]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ Eq (α := Ideal A) (ker f) ⊥
have rw : Function.Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
Tactic: rw [← RingHom.injective_iff_ker_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ Ideal.FG (ker f)
have this : Eq (α := Ideal A) (ker f) ⊥
Tactic: have : ker f = ⊥ := by rw [← RingHom.injective_iff_ker_eq_bot]; exact hf.1
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
this : Eq (α := Ideal A) (ker f) ⊥
⊢ Ideal.FG (ker f)
have rw : Ideal.FG.{u_1} (R := A) ⊥
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (hypothesis)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
g : B →+* C
f : A →+* B
hg : g.FinitePresentation
hf : f.FinitePresentation
⊢ (g.comp f).FinitePresentation
have algebraizeInst : Algebra.FinitePresentation B C
Tactic: algebraize [f, g, g.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (hypothesis)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
g : B →+* C
f : A →+* B
hg : g.FinitePresentation
hf : f.FinitePresentation
algebraizeInst : Algebra.FinitePresentation B C
⊢ (g.comp f).FinitePresentation
have algebraizeInst₁ : Algebra.FinitePresentation A B
Tactic: algebraize [f, g, g.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (hypothesis)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
f : A →+* B
g : B →+* C
hg : (g.comp f).FinitePresentation
hf : f.FiniteType
⊢ g.FinitePresentation
have algebraizeInst : Algebra.FinitePresentation A C
Tactic: algebraize [f, g, g.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (hypothesis)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
f : A →+* B
g : B →+* C
hg : (g.comp f).FinitePresentation
hf : f.FiniteType
algebraizeInst : Algebra.FinitePresentation A C
⊢ g.FinitePresentation
have algebraizeInst₁ : Algebra.FiniteType A B
Tactic: algebraize [f, g, g.comp f]