awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FinitePresentation
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
p₁ p₂ : RXn
hx_1 : Membership.mem (γ := Subalgebra R RXn) (adjoin R (Set.range MvPolynomial.X)) p₁
refine_4 :
  Membership.mem (γ := Subalgebra R RXn) (adjoin R (Set.range MvPolynomial.X)) p₂ →
    p₁ ∈ aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s') →
      p₂ ∈ aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s') →
        p₁ * p₂ ∈ aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
⊢ ∀ (hy : Membership.mem (γ := Subalgebra R RXn) (adjoin R (Set.range MvPolynomial.X)) p₂),
    p₁ ∈ aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s') →
      p₂ ∈ aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s') →
        p₁ * p₂ ∈ aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')

Tactic:
_
-- Module: Mathlib.RingTheory.FinitePresentation
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
p₁ p₂ : RXn
hx_1 : Membership.mem (γ := Subalgebra R RXn) (adjoin R (Set.range MvPolynomial.X)) p₁
hy : Membership.mem (γ := Subalgebra R RXn) (adjoin R (Set.range MvPolynomial.X)) p₂
h₁ : p₁ ∈ aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
h₂ : p₂ ∈ aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
refine_4 :
  ∀ (x₁ : RXm) (y₁ : RXn) (hy₁ : Membership.mem (γ := AddSubmonoid RXn) (Submodule.toAddSubmonoid (Ideal.span s')) y₁),
    Membership.mem (γ := Subalgebra R RXn) (adjoin R (Set.range MvPolynomial.X))
        (HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x₁ : RXn) y₁) →
      ∀
        (h₁ :
          HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x₁ : RXn) y₁ ∈
            aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')),
        HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x₁ : RXn) y₁ * p₂ ∈
          aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
⊢ p₁ * p₂ ∈ aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')

Tactic:
obtain ⟨_, ⟨x₁, rfl⟩, y₁, hy₁, rfl⟩ := AddSubmonoid.mem_sup.mp h₁

Premises used: Iff.mp, AddSubmonoid.mem_sup, rfl
-- Module: Mathlib.RingTheory.FinitePresentation
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₁ : RXm
y₁ : RXn
hy₁ : Membership.mem (γ := AddSubmonoid RXn) (Submodule.toAddSubmonoid (Ideal.span s')) y₁
hx_1 :
  Membership.mem (γ := Subalgebra R RXn) (adjoin R (Set.range MvPolynomial.X))
    (HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x₁ : RXn) y₁)
h₁ :
  HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x₁ : RXn) y₁ ∈
    aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
x₂ : RXm
y₂ : RXn
hy₂ : Membership.mem (γ := AddSubmonoid RXn) (Submodule.toAddSubmonoid (Ideal.span s')) y₂
hy :
  Membership.mem (γ := Subalgebra R RXn) (adjoin R (Set.range MvPolynomial.X))
    (HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x₂ : RXn) y₂)
h₂ :
  HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x₂ : RXn) y₂ ∈
    aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
⊢ Membership.mem (α := RXn) aeval_h.range.toAddSubmonoid ((aeval_h.toRingHom : (a : RXm) → RXn) (x₁ * x₂) : RXn)

Tactic:
Set.mem_range_self _

Premises used: Set.mem_range_self, Set.Mem, setOf, Set.range
-- Module: Mathlib.RingTheory.FinitePresentation
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₁ : RXm
y₁ : RXn
hy₁ : Membership.mem (γ := AddSubmonoid RXn) (Submodule.toAddSubmonoid (Ideal.span s')) y₁
hx_1 :
  Membership.mem (γ := Subalgebra R RXn) (adjoin R (Set.range MvPolynomial.X))
    (HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x₁ : RXn) y₁)
h₁ :
  HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x₁ : RXn) y₁ ∈
    aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
x₂ : RXm
y₂ : RXn
hy₂ : Membership.mem (γ := AddSubmonoid RXn) (Submodule.toAddSubmonoid (Ideal.span s')) y₂
hy :
  Membership.mem (γ := Subalgebra R RXn) (adjoin R (Set.range MvPolynomial.X))
    (HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x₂ : RXn) y₂)
h₂ :
  HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x₂ : RXn) y₂ ∈
    aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
⊢ Membership.mem (α := RXn) aeval_h.range.toAddSubmonoid ((aeval_h.toRingHom : (a : RXm) → RXn) (x₁ * x₂) : RXn)

Tactic:
exact Set.mem_range_self _

Premises used: Set.mem_range_self
-- Module: Mathlib.RingTheory.FinitePresentation
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₁ : RXm
y₁ : RXn
hy₁ : Membership.mem (γ := AddSubmonoid RXn) (Submodule.toAddSubmonoid (Ideal.span s')) y₁
hx_1 :
  Membership.mem (γ := Subalgebra R RXn) (adjoin R (Set.range MvPolynomial.X))
    (HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x₁ : RXn) y₁)
h₁ :
  HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x₁ : RXn) y₁ ∈
    aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
x₂ : RXm
y₂ : RXn
hy₂ : Membership.mem (γ := AddSubmonoid RXn) (Submodule.toAddSubmonoid (Ideal.span s')) y₂
hy :
  Membership.mem (γ := Subalgebra R RXn) (adjoin R (Set.range MvPolynomial.X))
    (HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x₂ : RXn) y₂)
h₂ :
  HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x₂ : RXn) y₂ ∈
    aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
⊢ Membership.mem (γ := AddSubmonoid RXn) (Submodule.toAddSubmonoid (Ideal.span s'))
    (HMul.hMul (β := RXn) y₁ ((aeval_h.toRingHom : (a : RXm) → RXn) x₂ : RXn) +
      HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x₁ : RXn) y₁ * y₂)

Tactic:
add_mem (Ideal.mul_mem_right _ _ hy₁) (Ideal.mul_mem_left _ _ hy₂)

Premises used: Ideal.mul_mem_right, AddMemClass.add_mem, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.FinitePresentation
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₁ : RXm
y₁ : RXn
hy₁ : Membership.mem (γ := AddSubmonoid RXn) (Submodule.toAddSubmonoid (Ideal.span s')) y₁
hx_1 :
  Membership.mem (γ := Subalgebra R RXn) (adjoin R (Set.range MvPolynomial.X))
    (HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x₁ : RXn) y₁)
h₁ :
  HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x₁ : RXn) y₁ ∈
    aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
x₂ : RXm
y₂ : RXn
hy₂ : Membership.mem (γ := AddSubmonoid RXn) (Submodule.toAddSubmonoid (Ideal.span s')) y₂
hy :
  Membership.mem (γ := Subalgebra R RXn) (adjoin R (Set.range MvPolynomial.X))
    (HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x₂ : RXn) y₂)
h₂ :
  HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x₂ : RXn) y₂ ∈
    aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
⊢ Membership.mem (γ := AddSubmonoid RXn) (Submodule.toAddSubmonoid (Ideal.span s'))
    (HMul.hMul (β := RXn) y₁ ((aeval_h.toRingHom : (a : RXm) → RXn) x₂ : RXn) +
      HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x₁ : RXn) y₁ * y₂)

Tactic:
exact add_mem (Ideal.mul_mem_right _ _ hy₁) (Ideal.mul_mem_left _ _ hy₂)

Premises used: Ideal.mul_mem_right, AddMemClass.add_mem, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.FinitePresentation
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')

Tactic:
have : x ∈ aeval_h.range.toAddSubmonoid ⊔ (Ideal.span s').toAddSubmonoid := by
      have : x ∈ adjoin R (Set.range X : Set RXn) := by
        rw [adjoin_range_X]
        trivial
      refine adjoin_induction ?_ ?_ ?_ ?_ this
      · rintro _ ⟨i, rfl⟩
        rw [← sub_add_cancel (X i) (aeval h (g i)), add_comm]
        apply AddSubmonoid.add_mem_sup
        · exact Set.mem_range_self _
        · apply Submodule.subset_span
          apply Set.mem_union_left
          exact Set.mem_range_self _
      · intro r
        apply AddSubmonoid.mem_sup_left
        exact ⟨C r, aeval_C _ _⟩
      · intro _ _ _ _ h₁ h₂
        exact add_mem h₁ h₂
      · intro p₁ p₂ _ _ h₁ h₂
        obtain ⟨_, ⟨x₁, rfl⟩, y₁, hy₁, rfl⟩ := AddSubmonoid.mem_sup.mp h₁
        obtain ⟨_, ⟨x₂, rfl⟩, y₂, hy₂, rfl⟩ := AddSubmonoid.mem_sup.mp h₂
        rw [mul_add, add_mul, add_assoc, ← map_mul]
        apply AddSubmonoid.add_mem_sup
        · exact Set.mem_range_self _
        · exact add_mem (Ideal.mul_mem_right _ _ hy₁) (Ideal.mul_mem_left _ _ hy₂)
-- Module: Mathlib.RingTheory.FinitePresentation
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 : x ∈ aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')
obtain :
  ∀ (x : RXm) (y : RXn) (hy : Membership.mem (γ := AddSubmonoid RXn) (Submodule.toAddSubmonoid (Ideal.span s')) y)
    (hx :
      Membership.mem (γ := Submodule RXn RXn) (RingHom.ker f.toRingHom)
        (HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x : RXn) y))
    (this :
      HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x : RXn) y ∈
        aeval_h.range.toAddSubmonoid ⊔ Submodule.toAddSubmonoid (Ideal.span s')),
    Membership.mem (γ := Submodule RXn RXn) (Ideal.span s')
      (HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x : RXn) y)
⊢ Membership.mem (γ := Submodule RXn RXn) (Ideal.span s') x

Tactic:
obtain ⟨_, ⟨x, rfl⟩, y, hy, rfl⟩ := AddSubmonoid.mem_sup.mp this

Premises used: Iff.mp, AddSubmonoid.mem_sup, rfl