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 : 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)

Tactic:
add_mem ?_ hy

Premises used: AddMemClass.add_mem
-- 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 : 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')
refine :
  Membership.mem (α := RXn) (γ := Submodule RXn RXn) (Ideal.span s') ((aeval_h.toRingHom : (a : RXm) → RXn) x : RXn)
⊢ Membership.mem (γ := Submodule RXn RXn) (Ideal.span s')
    (HAdd.hAdd (α := RXn) ((aeval_h.toRingHom : (a : RXm) → RXn) x : RXn) y)

Tactic:
refine add_mem ?_ hy

Premises used: AddMemClass.add_mem
-- 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 : 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')
⊢ Eq.{w₂ + 1} (α := A) ((f' : (a : MvPolynomial (Fin m) R) → A) x : A) (0 : A)

Tactic:
simp only [RXn, RingHom.mem_ker, AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, map_add,
      show f y = 0 from leI hy, add_zero, hh'] at hx

Premises used: AlgHom.coe_toRingHom, RingHom.mem_ker, map_add, AlgHom.toRingHom_eq_coe, add_zero
-- 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 : 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'))
a : Membership.mem (γ := Submodule RXm RXm) (Ideal.span (↑s : Set RXm)) x
⊢ Membership.mem (α := RXn) (γ := Submodule RXn RXn) (Ideal.span s') ((aeval_h.toRingHom : (a : RXm) → RXn) x : RXn)

Tactic:
apply this
-- 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 : 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'))
a a₁ a₂ a₃ : Membership.mem (γ := Submodule RXm RXm) (RingHom.ker f'.toRingHom) x
⊢ Membership.mem (γ := Submodule RXm RXm) (Ideal.span (↑s : Set RXm)) x

Tactic:
rwa [hs]
-- 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 : 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)
suffices : 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)

Tactic:
suffices Ideal.span (s : Set RXm) ≤ (Ideal.span s').comap aeval_h by
      apply this
      rwa [hs]
-- 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 : 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)
rw : (↑s : Set RXm) ⊆ (↑(Ideal.comap aeval_h (Ideal.span s')) : Set RXm)
⊢ LE.le (α := Ideal RXm) (Ideal.span (↑s : Set RXm)) (Ideal.comap aeval_h (Ideal.span s'))

Tactic:
rw [Ideal.span_le]

Premises used: Ideal.span_le
-- 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_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)
a : Membership.mem (α := RXn) s' ((aeval_h : (a : RXm) → RXn) x : RXn)
⊢ x ∈ (↑(Ideal.comap aeval_h (Ideal.span s')) : Set RXm)

Tactic:
apply Submodule.subset_span

Premises used: Submodule.subset_span
-- 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_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)
a :
  Membership.mem (α := RXn) (γ := Set RXn) ((⇑aeval_h : (a : RXm) → RXn) '' (↑s : Set RXm))
    ((aeval_h : (a : RXm) → RXn) x : RXn)
⊢ Membership.mem (α := RXn) s' ((aeval_h : (a : RXm) → RXn) x : RXn)

Tactic:
apply Set.mem_union_right

Premises used: Set.mem_union_right
-- 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_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) (γ := Set RXn) ((⇑aeval_h : (a : RXm) → RXn) '' (↑s : Set RXm))
    ((aeval_h : (a : RXm) → RXn) x : RXn)

Tactic:
Set.mem_image_of_mem _ hx

Premises used: Set.mem_image_of_mem