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)
x : RXm
hx : x ∈ (↑s : Set RXm)
⊢ Membership.mem (γ := Ideal (MvPolynomial (Fin m) R)) (RingHom.ker f'.toRingHom) x
have inr : Membership.mem (γ := Ideal (MvPolynomial (Fin m) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin m) R))) x
Tactic: rw [← hs]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (hypothesis)
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)
⊢ Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.span (Set.range g' ∪ (⇑aeval_h : (a : RXm) → RXn) '' (↑s : Set RXm)))
    (RingHom.ker f.toRingHom)
have leI : LE.le (α := Ideal RXn) (Ideal.span s') (RingHom.ker f.toRingHom)
Tactic: have leI : Ideal.span s' ≤ RingHom.ker f.toRingHom := by
      rw [Ideal.span_le]
      rintro _ (⟨i, rfl⟩ | ⟨x, hx, rfl⟩)
      · change f (g' i) = 0
        rw [map_sub, ← hg, hh', sub_self]
      · change f (aeval_h x) = 0
        rw [hh']
        change x ∈ RingHom.ker f'.toRingHom
        rw [← hs]
        exact Ideal.subset_span hx
-- 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)
⊢ Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.span (Set.range g' ∪ (⇑aeval_h : (a : RXm) → RXn) '' (↑s : Set RXm)))
    (RingHom.ker f.toRingHom)
have apply : LE.le (α := Ideal RXn) (RingHom.ker f.toRingHom) (Ideal.span s')
Tactic: apply leI.antisymm
-- 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 : RXn
hx : Membership.mem (γ := Submodule RXn RXn) (RingHom.ker f.toRingHom) x
⊢ Membership.mem (γ := Subalgebra R RXn) (adjoin R (Set.range MvPolynomial.X)) x
have rw : Membership.mem (γ := Subalgebra R RXn) ⊤ x
Tactic: rw [adjoin_range_X]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (hypothesis)
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 : RXn
hx : Membership.mem (γ := Submodule RXn RXn) (RingHom.ker f.toRingHom) x
⊢ x ∈ aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
have this : Membership.mem (γ := Subalgebra R RXn) (adjoin R (Set.range MvPolynomial.X)) x
Tactic: have : x ∈ adjoin R (Set.range X : Set RXn) := by
        rw [adjoin_range_X]
        trivial
-- 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 : RXn
hx : Membership.mem (γ := Submodule RXn RXn) (RingHom.ker f.toRingHom) x
this : Membership.mem (γ := Subalgebra R RXn) (adjoin R (Set.range MvPolynomial.X)) x
⊢ x ∈ aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
have refine_1 : ∀ (x : RXn) (hx : Membership.mem (γ := Set RXn) (Set.range MvPolynomial.X) x),
  x ∈ aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
Tactic: refine adjoin_induction ?_ ?_ ?_ ?_ 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 : RXn
hx : Membership.mem (γ := Submodule RXn RXn) (RingHom.ker f.toRingHom) x
this : Membership.mem (γ := Subalgebra R RXn) (adjoin R (Set.range MvPolynomial.X)) x
refine_1 :
  ∀ (x : RXn) (hx : Membership.mem (γ := Set RXn) (Set.range MvPolynomial.X) x),
    x ∈ aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
⊢ x ∈ aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
have refine_2 : ∀ (r : R),
  Membership.mem (α := RXn) (aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s'))
    ((algebraMap R RXn : (a : R) → RXn) r : RXn)
Tactic: refine adjoin_induction ?_ ?_ ?_ ?_ 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 : RXn
hx : Membership.mem (γ := Submodule RXn RXn) (RingHom.ker f.toRingHom) x
this : Membership.mem (γ := Subalgebra R RXn) (adjoin R (Set.range MvPolynomial.X)) x
refine_1 :
  ∀ (x : RXn) (hx : Membership.mem (γ := Set RXn) (Set.range MvPolynomial.X) x),
    x ∈ aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
refine_2 :
  ∀ (r : R),
    Membership.mem (α := RXn) (aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s'))
      ((algebraMap R RXn : (a : R) → RXn) r : RXn)
⊢ x ∈ aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
have refine_3 : ∀ (x y : RXn) (hx : Membership.mem (γ := Subalgebra R RXn) (adjoin R (Set.range MvPolynomial.X)) x)
  (hy : Membership.mem (γ := Subalgebra R RXn) (adjoin R (Set.range MvPolynomial.X)) y),
  x ∈ aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s') →
    y ∈ aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s') →
      x + y ∈ aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
Tactic: refine adjoin_induction ?_ ?_ ?_ ?_ 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 : RXn
hx : Membership.mem (γ := Submodule RXn RXn) (RingHom.ker f.toRingHom) x
this : Membership.mem (γ := Subalgebra R RXn) (adjoin R (Set.range MvPolynomial.X)) x
i : Fin n
⊢ MvPolynomial.X i ∈ aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
have refine_1 : HAdd.hAdd (α := MvPolynomial (Fin n) R)
    ((MvPolynomial.aeval h : (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin n) R) (g i) : MvPolynomial (Fin n) R)
    (HSub.hSub (α := MvPolynomial (Fin n) R) (β := MvPolynomial (Fin n) R) (MvPolynomial.X i)
      ((MvPolynomial.aeval h : (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin n) R) (g i) : MvPolynomial (Fin n) R)) ∈
  aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
Tactic: rw [← sub_add_cancel (X i) (aeval h (g i)), add_comm]
-- 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 : RXn
hx : Membership.mem (γ := Submodule RXn RXn) (RingHom.ker f.toRingHom) x
this : Membership.mem (γ := Subalgebra R RXn) (adjoin R (Set.range MvPolynomial.X)) x
i : Fin n
⊢ HAdd.hAdd (α := MvPolynomial (Fin n) R)
      ((MvPolynomial.aeval h : (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin n) R) (g i) : MvPolynomial (Fin n) R)
      (HSub.hSub (α := MvPolynomial (Fin n) R) (β := MvPolynomial (Fin n) R) (MvPolynomial.X i)
        ((MvPolynomial.aeval h : (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin n) R) (g i) :
          MvPolynomial (Fin n) R)) ∈
    aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
have refine_1 : Membership.mem (α := RXn) aeval_h.range.toAddSubmonoid
  ((MvPolynomial.aeval h : (a : MvPolynomial (Fin m) R) → MvPolynomial (Fin n) R) (g i) : MvPolynomial (Fin n) R)
Tactic: apply AddSubmonoid.add_mem_sup