awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FinitePresentation R B
inst_8 : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B) (⇑f : (a : MvPolynomial (Fin n) R) → B)
s : Finset (MvPolynomial (Fin n) R)
hs : Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin n) R))) (RingHom.ker f.toRingHom)
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : Eq (α := Subalgebra R A) (adjoin R (↑t : Set A)) ⊤
t' : (i : ↥t) → MvPolynomial (Fin n) R
ht' :
  ∀ (i : ↥t),
    Eq.{w₃ + 1} (α := B) ((f : (a : MvPolynomial (Fin n) R) → B) (t' i) : B)
      ((algebraMap A B : (a : A) → B) (↑i : A) : B)
ht'' :
  Eq (α := Subalgebra R AX) (adjoin R ((⇑(algebraMap A AX) : (a : A) → AX) '' (↑t : Set A) ∪ Set.range MvPolynomial.X))
    ⊤
g : ↥t → AX :=
  fun (x : ↥t) ↦
    HSub.hSub (α := MvPolynomial (Fin n) A) (β := MvPolynomial (Fin n) A)
      ((MvPolynomial.C : (a : A) → MvPolynomial (Fin n) A) (↑x : A) : MvPolynomial (Fin n) A)
      (((MvPolynomial.map (algebraMap R A) : RingHom.{w₁, w₂} (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) A)) :
            (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) A)
          (t' x) :
        MvPolynomial (Fin n) A)
s₀ : Set (MvPolynomial (Fin n) A) :=
  (⇑(MvPolynomial.map (algebraMap R A)) : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) A) ''
      (↑s : Set (MvPolynomial (Fin n) R)) ∪
    Set.range g
I : Ideal (MvPolynomial (Fin n) A) :=
  RingHom.ker (F := MvPolynomial (Fin n) A →ₐ[A] B)
    (MvPolynomial.aeval
      (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
        MvPolynomial.X))
x : A
hx : x ∈ t
inr :
  Eq.{w₃ + 1} (α := B)
    ((MvPolynomial.aeval
            (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
              MvPolynomial.X) :
          (a : MvPolynomial (Fin n) A) → B)
        (g (Subtype.mk (p := fun (x : A) ↦ x ∈ t) x hx)) :
      B)
    (0 : B)
⊢ g (Subtype.mk (p := fun (x : A) ↦ x ∈ t) x hx) ∈
    (↑(RingHom.ker (F := MvPolynomial (Fin n) A →ₐ[A] B)
          (MvPolynomial.aeval
            (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
              MvPolynomial.X))) :
      Set (MvPolynomial (Fin n) A))

Tactic:
rw [SetLike.mem_coe, RingHom.mem_ker]

Premises used: RingHom.mem_ker, SetLike.mem_coe
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FinitePresentation R B
inst_8 : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B) (⇑f : (a : MvPolynomial (Fin n) R) → B)
s : Finset (MvPolynomial (Fin n) R)
hs : Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin n) R))) (RingHom.ker f.toRingHom)
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : Eq (α := Subalgebra R A) (adjoin R (↑t : Set A)) ⊤
t' : (i : ↥t) → MvPolynomial (Fin n) R
ht' :
  ∀ (i : ↥t),
    Eq.{w₃ + 1} (α := B) ((f : (a : MvPolynomial (Fin n) R) → B) (t' i) : B)
      ((algebraMap A B : (a : A) → B) (↑i : A) : B)
ht'' :
  Eq (α := Subalgebra R AX) (adjoin R ((⇑(algebraMap A AX) : (a : A) → AX) '' (↑t : Set A) ∪ Set.range MvPolynomial.X))
    ⊤
g : ↥t → AX :=
  fun (x : ↥t) ↦
    HSub.hSub (α := MvPolynomial (Fin n) A) (β := MvPolynomial (Fin n) A)
      ((MvPolynomial.C : (a : A) → MvPolynomial (Fin n) A) (↑x : A) : MvPolynomial (Fin n) A)
      (((MvPolynomial.map (algebraMap R A) : RingHom.{w₁, w₂} (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) A)) :
            (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) A)
          (t' x) :
        MvPolynomial (Fin n) A)
s₀ : Set (MvPolynomial (Fin n) A) :=
  (⇑(MvPolynomial.map (algebraMap R A)) : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) A) ''
      (↑s : Set (MvPolynomial (Fin n) R)) ∪
    Set.range g
I : Ideal (MvPolynomial (Fin n) A) :=
  RingHom.ker (F := MvPolynomial (Fin n) A →ₐ[A] B)
    (MvPolynomial.aeval
      (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
        MvPolynomial.X))
x : MvPolynomial (Fin n) R
hx : x ∈ (↑s : Set (MvPolynomial (Fin n) R))
inl : Eq.{w₃ + 1} (α := B) ((f : (a : MvPolynomial (Fin n) R) → B) x : B) (0 : B)
⊢ Eq.{w₃ + 1} (α := B)
    ((MvPolynomial.aeval
            (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
              MvPolynomial.X) :
          (a : MvPolynomial (Fin n) A) → B)
        (((MvPolynomial.map (algebraMap R A) : RingHom.{w₁, w₂} (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) A)) :
              (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) A)
            x :
          MvPolynomial (Fin n) A) :
      B)
    (0 : B)

Tactic:
rw [MvPolynomial.aeval_map_algebraMap (R := R) (A := A), ← aeval_unique]

Premises used: MvPolynomial.aeval_map_algebraMap, MvPolynomial.aeval_unique
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FinitePresentation R B
inst_8 : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B) (⇑f : (a : MvPolynomial (Fin n) R) → B)
s : Finset (MvPolynomial (Fin n) R)
hs : Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin n) R))) (RingHom.ker f.toRingHom)
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : Eq (α := Subalgebra R A) (adjoin R (↑t : Set A)) ⊤
t' : (i : ↥t) → MvPolynomial (Fin n) R
ht' :
  ∀ (i : ↥t),
    Eq.{w₃ + 1} (α := B) ((f : (a : MvPolynomial (Fin n) R) → B) (t' i) : B)
      ((algebraMap A B : (a : A) → B) (↑i : A) : B)
ht'' :
  Eq (α := Subalgebra R AX) (adjoin R ((⇑(algebraMap A AX) : (a : A) → AX) '' (↑t : Set A) ∪ Set.range MvPolynomial.X))
    ⊤
g : ↥t → AX :=
  fun (x : ↥t) ↦
    HSub.hSub (α := MvPolynomial (Fin n) A) (β := MvPolynomial (Fin n) A)
      ((MvPolynomial.C : (a : A) → MvPolynomial (Fin n) A) (↑x : A) : MvPolynomial (Fin n) A)
      (((MvPolynomial.map (algebraMap R A) : RingHom.{w₁, w₂} (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) A)) :
            (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) A)
          (t' x) :
        MvPolynomial (Fin n) A)
s₀ : Set (MvPolynomial (Fin n) A) :=
  (⇑(MvPolynomial.map (algebraMap R A)) : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) A) ''
      (↑s : Set (MvPolynomial (Fin n) R)) ∪
    Set.range g
I : Ideal (MvPolynomial (Fin n) A) :=
  RingHom.ker (F := MvPolynomial (Fin n) A →ₐ[A] B)
    (MvPolynomial.aeval
      (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
        MvPolynomial.X))
x : MvPolynomial (Fin n) R
hx : x ∈ (↑s : Set (MvPolynomial (Fin n) R))
⊢ x ∈ (↑(Ideal.span (↑s : Set (MvPolynomial (Fin n) R))) : Set (MvPolynomial (Fin n) R))

Tactic:
have := Ideal.subset_span hx
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FinitePresentation R B
inst_8 : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B) (⇑f : (a : MvPolynomial (Fin n) R) → B)
s : Finset (MvPolynomial (Fin n) R)
hs : Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin n) R))) (RingHom.ker f.toRingHom)
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : Eq (α := Subalgebra R A) (adjoin R (↑t : Set A)) ⊤
t' : (i : ↥t) → MvPolynomial (Fin n) R
ht' :
  ∀ (i : ↥t),
    Eq.{w₃ + 1} (α := B) ((f : (a : MvPolynomial (Fin n) R) → B) (t' i) : B)
      ((algebraMap A B : (a : A) → B) (↑i : A) : B)
ht'' :
  Eq (α := Subalgebra R AX) (adjoin R ((⇑(algebraMap A AX) : (a : A) → AX) '' (↑t : Set A) ∪ Set.range MvPolynomial.X))
    ⊤
g : ↥t → AX :=
  fun (x : ↥t) ↦
    HSub.hSub (α := MvPolynomial (Fin n) A) (β := MvPolynomial (Fin n) A)
      ((MvPolynomial.C : (a : A) → MvPolynomial (Fin n) A) (↑x : A) : MvPolynomial (Fin n) A)
      (((MvPolynomial.map (algebraMap R A) : RingHom.{w₁, w₂} (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) A)) :
            (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) A)
          (t' x) :
        MvPolynomial (Fin n) A)
s₀ : Set (MvPolynomial (Fin n) A) :=
  (⇑(MvPolynomial.map (algebraMap R A)) : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) A) ''
      (↑s : Set (MvPolynomial (Fin n) R)) ∪
    Set.range g
I : Ideal (MvPolynomial (Fin n) A) :=
  RingHom.ker (F := MvPolynomial (Fin n) A →ₐ[A] B)
    (MvPolynomial.aeval
      (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
        MvPolynomial.X))
x : MvPolynomial (Fin n) R
hx : x ∈ (↑s : Set (MvPolynomial (Fin n) R))
this : x ∈ (↑(Ideal.span (↑s : Set (MvPolynomial (Fin n) R))) : Set (MvPolynomial (Fin n) R))
inl inl₁ inl₂ inl₃ :
  ∀ (this : x ∈ (↑(RingHom.ker f.toRingHom) : Set (MvPolynomial (Fin n) R))),
    Eq.{w₃ + 1} (α := B) ((f : (a : MvPolynomial (Fin n) R) → B) x : B) (0 : B)
⊢ Eq.{w₃ + 1} (α := B) ((f : (a : MvPolynomial (Fin n) R) → B) x : B) (0 : B)

Tactic:
rwa [hs] at this
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FinitePresentation R B
inst_8 : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B) (⇑f : (a : MvPolynomial (Fin n) R) → B)
s : Finset (MvPolynomial (Fin n) R)
hs : Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin n) R))) (RingHom.ker f.toRingHom)
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : Eq (α := Subalgebra R A) (adjoin R (↑t : Set A)) ⊤
t' : (i : ↥t) → MvPolynomial (Fin n) R
ht' :
  ∀ (i : ↥t),
    Eq.{w₃ + 1} (α := B) ((f : (a : MvPolynomial (Fin n) R) → B) (t' i) : B)
      ((algebraMap A B : (a : A) → B) (↑i : A) : B)
ht'' :
  Eq (α := Subalgebra R AX) (adjoin R ((⇑(algebraMap A AX) : (a : A) → AX) '' (↑t : Set A) ∪ Set.range MvPolynomial.X))
    ⊤
g : ↥t → AX :=
  fun (x : ↥t) ↦
    HSub.hSub (α := MvPolynomial (Fin n) A) (β := MvPolynomial (Fin n) A)
      ((MvPolynomial.C : (a : A) → MvPolynomial (Fin n) A) (↑x : A) : MvPolynomial (Fin n) A)
      (((MvPolynomial.map (algebraMap R A) : RingHom.{w₁, w₂} (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) A)) :
            (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) A)
          (t' x) :
        MvPolynomial (Fin n) A)
s₀ : Set (MvPolynomial (Fin n) A) :=
  (⇑(MvPolynomial.map (algebraMap R A)) : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) A) ''
      (↑s : Set (MvPolynomial (Fin n) R)) ∪
    Set.range g
I : Ideal (MvPolynomial (Fin n) A) :=
  RingHom.ker (F := MvPolynomial (Fin n) A →ₐ[A] B)
    (MvPolynomial.aeval
      (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
        MvPolynomial.X))
⊢ LE.le (α := Ideal (MvPolynomial (Fin n) A))
    (Ideal.span
      ((⇑(MvPolynomial.map (algebraMap R A)) : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) A) ''
          (↑s : Set (MvPolynomial (Fin n) R)) ∪
        Set.range g))
    (RingHom.ker (F := MvPolynomial (Fin n) A →ₐ[A] B)
      (MvPolynomial.aeval
        (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
          MvPolynomial.X)))

Tactic:
have leI : Ideal.span ((MvPolynomial.map (algebraMap R A)) '' s ∪ Set.range g) ≤
      RingHom.ker (MvPolynomial.aeval (R := A) (f ∘ MvPolynomial.X)) := by
      rw [Ideal.span_le]
      rintro _ (⟨x, hx, rfl⟩ | ⟨⟨x, hx⟩, rfl⟩) <;>
      rw [SetLike.mem_coe, RingHom.mem_ker]
      · rw [MvPolynomial.aeval_map_algebraMap (R := R) (A := A), ← aeval_unique]
        have := Ideal.subset_span hx
        rwa [hs] at this
      · rw [map_sub, MvPolynomial.aeval_map_algebraMap, ← aeval_unique,
          MvPolynomial.aeval_C, ht', Subtype.coe_mk, sub_self]
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FinitePresentation R B
inst_8 : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B) (⇑f : (a : MvPolynomial (Fin n) R) → B)
s : Finset (MvPolynomial (Fin n) R)
hs : Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin n) R))) (RingHom.ker f.toRingHom)
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : Eq (α := Subalgebra R A) (adjoin R (↑t : Set A)) ⊤
t' : (i : ↥t) → MvPolynomial (Fin n) R
ht' :
  ∀ (i : ↥t),
    Eq.{w₃ + 1} (α := B) ((f : (a : MvPolynomial (Fin n) R) → B) (t' i) : B)
      ((algebraMap A B : (a : A) → B) (↑i : A) : B)
ht'' :
  Eq (α := Subalgebra R AX) (adjoin R ((⇑(algebraMap A AX) : (a : A) → AX) '' (↑t : Set A) ∪ Set.range MvPolynomial.X))
    ⊤
g : ↥t → AX :=
  fun (x : ↥t) ↦
    HSub.hSub (α := MvPolynomial (Fin n) A) (β := MvPolynomial (Fin n) A)
      ((MvPolynomial.C : (a : A) → MvPolynomial (Fin n) A) (↑x : A) : MvPolynomial (Fin n) A)
      (((MvPolynomial.map (algebraMap R A) : RingHom.{w₁, w₂} (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) A)) :
            (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) A)
          (t' x) :
        MvPolynomial (Fin n) A)
s₀ : Set (MvPolynomial (Fin n) A) :=
  (⇑(MvPolynomial.map (algebraMap R A)) : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) A) ''
      (↑s : Set (MvPolynomial (Fin n) R)) ∪
    Set.range g
I : Ideal (MvPolynomial (Fin n) A) :=
  RingHom.ker (F := MvPolynomial (Fin n) A →ₐ[A] B)
    (MvPolynomial.aeval
      (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
        MvPolynomial.X))
leI :
  LE.le (α := Ideal (MvPolynomial (Fin n) A))
    (Ideal.span
      ((⇑(MvPolynomial.map (algebraMap R A)) : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) A) ''
          (↑s : Set (MvPolynomial (Fin n) R)) ∪
        Set.range g))
    (RingHom.ker (F := MvPolynomial (Fin n) A →ₐ[A] B)
      (MvPolynomial.aeval
        (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
          MvPolynomial.X)))
refine_2 :
  LE.le (α := Ideal (MvPolynomial (Fin n) A))
    (RingHom.ker (F := MvPolynomial (Fin n) A →ₐ[A] B)
      (MvPolynomial.aeval
        (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
          MvPolynomial.X)))
    (Ideal.span
      ((⇑(MvPolynomial.map (algebraMap R A)) : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) A) ''
          (↑s : Set (MvPolynomial (Fin n) R)) ∪
        Set.range g))
⊢ Ideal.span s₀ = I

Tactic:
apply leI.antisymm

Premises used: LE.le.antisymm
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FinitePresentation R B
inst_8 : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B) (⇑f : (a : MvPolynomial (Fin n) R) → B)
s : Finset (MvPolynomial (Fin n) R)
hs : Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin n) R))) (RingHom.ker f.toRingHom)
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : Eq (α := Subalgebra R A) (adjoin R (↑t : Set A)) ⊤
t' : (i : ↥t) → MvPolynomial (Fin n) R
ht' :
  ∀ (i : ↥t),
    Eq.{w₃ + 1} (α := B) ((f : (a : MvPolynomial (Fin n) R) → B) (t' i) : B)
      ((algebraMap A B : (a : A) → B) (↑i : A) : B)
ht'' :
  Eq (α := Subalgebra R AX) (adjoin R ((⇑(algebraMap A AX) : (a : A) → AX) '' (↑t : Set A) ∪ Set.range MvPolynomial.X))
    ⊤
g : ↥t → AX :=
  fun (x : ↥t) ↦
    HSub.hSub (α := MvPolynomial (Fin n) A) (β := MvPolynomial (Fin n) A)
      ((MvPolynomial.C : (a : A) → MvPolynomial (Fin n) A) (↑x : A) : MvPolynomial (Fin n) A)
      (((MvPolynomial.map (algebraMap R A) : RingHom.{w₁, w₂} (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) A)) :
            (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) A)
          (t' x) :
        MvPolynomial (Fin n) A)
s₀ : Set (MvPolynomial (Fin n) A) :=
  (⇑(MvPolynomial.map (algebraMap R A)) : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) A) ''
      (↑s : Set (MvPolynomial (Fin n) R)) ∪
    Set.range g
I : Ideal (MvPolynomial (Fin n) A) :=
  RingHom.ker (F := MvPolynomial (Fin n) A →ₐ[A] B)
    (MvPolynomial.aeval
      (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
        MvPolynomial.X))
leI :
  LE.le (α := Ideal (MvPolynomial (Fin n) A))
    (Ideal.span
      ((⇑(MvPolynomial.map (algebraMap R A)) : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) A) ''
          (↑s : Set (MvPolynomial (Fin n) R)) ∪
        Set.range g))
    (RingHom.ker (F := MvPolynomial (Fin n) A →ₐ[A] B)
      (MvPolynomial.aeval
        (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
          MvPolynomial.X)))
x : MvPolynomial (Fin n) A
hx :
  Membership.mem (γ := Submodule (MvPolynomial (Fin n) A) (MvPolynomial (Fin n) A))
    (RingHom.ker (F := MvPolynomial (Fin n) A →ₐ[A] B)
      (MvPolynomial.aeval
        (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
          MvPolynomial.X)))
    x
⊢ Eq.{w₃ + 1} (α := B)
    ((MvPolynomial.aeval
            (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
              MvPolynomial.X) :
          (a : MvPolynomial (Fin n) A) → B)
        x :
      B)
    (0 : B)

Tactic:
rw [RingHom.mem_ker] at hx

Premises used: RingHom.mem_ker
-- Module: Mathlib.RingTheory.FinitePresentation
Goal:
R : Type w₁
A : Type w₂
B : Type w₃
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : Algebra A B
inst_6 : IsScalarTower R A B
inst_7 : FinitePresentation R B
inst_8 : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective.{w₁ + 1, w₃ + 1} (α := MvPolynomial (Fin n) R) (β := B) (⇑f : (a : MvPolynomial (Fin n) R) → B)
s : Finset (MvPolynomial (Fin n) R)
hs : Eq (α := Ideal (MvPolynomial (Fin n) R)) (Ideal.span (↑s : Set (MvPolynomial (Fin n) R))) (RingHom.ker f.toRingHom)
RX : Type w₁ := MvPolynomial (Fin n) R
AX : Type w₂ := MvPolynomial (Fin n) A
t : Finset A
ht : Eq (α := Subalgebra R A) (adjoin R (↑t : Set A)) ⊤
t' : (i : ↥t) → MvPolynomial (Fin n) R
ht' :
  ∀ (i : ↥t),
    Eq.{w₃ + 1} (α := B) ((f : (a : MvPolynomial (Fin n) R) → B) (t' i) : B)
      ((algebraMap A B : (a : A) → B) (↑i : A) : B)
ht'' :
  Eq (α := Subalgebra R AX) (adjoin R ((⇑(algebraMap A AX) : (a : A) → AX) '' (↑t : Set A) ∪ Set.range MvPolynomial.X))
    ⊤
g : ↥t → AX :=
  fun (x : ↥t) ↦
    HSub.hSub (α := MvPolynomial (Fin n) A) (β := MvPolynomial (Fin n) A)
      ((MvPolynomial.C : (a : A) → MvPolynomial (Fin n) A) (↑x : A) : MvPolynomial (Fin n) A)
      (((MvPolynomial.map (algebraMap R A) : RingHom.{w₁, w₂} (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) A)) :
            (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) A)
          (t' x) :
        MvPolynomial (Fin n) A)
s₀_1 : Set (MvPolynomial (Fin n) A) :=
  (⇑(MvPolynomial.map (algebraMap R A)) : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) A) ''
      (↑s : Set (MvPolynomial (Fin n) R)) ∪
    Set.range g
I : Ideal (MvPolynomial (Fin n) A) :=
  RingHom.ker (F := MvPolynomial (Fin n) A →ₐ[A] B)
    (MvPolynomial.aeval
      (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
        MvPolynomial.X))
leI :
  LE.le (α := Ideal (MvPolynomial (Fin n) A))
    (Ideal.span
      ((⇑(MvPolynomial.map (algebraMap R A)) : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) A) ''
          (↑s : Set (MvPolynomial (Fin n) R)) ∪
        Set.range g))
    (RingHom.ker (F := MvPolynomial (Fin n) A →ₐ[A] B)
      (MvPolynomial.aeval
        (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
          MvPolynomial.X)))
x : MvPolynomial (Fin n) A
hx :
  Eq.{w₃ + 1} (α := B)
    ((MvPolynomial.aeval
            (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
              MvPolynomial.X) :
          (a : MvPolynomial (Fin n) A) → B)
        x :
      B)
    (0 : B)
s₀ : Set (MvPolynomial (Fin n) A) :=
  (⇑(MvPolynomial.map (algebraMap R A)) : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) A) ''
      (↑s : Set (MvPolynomial (Fin n) R)) ∪
    Set.range g
⊢ Membership.mem (γ := Subalgebra R AX) ⊤ x

Tactic:
have : x ∈ (⊤ : Subalgebra R AX) := trivial