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)
refine :
  Eq.{w₂ + 1} (α := Subalgebra (↥(adjoin R ((⇑(algebraMap A AX) : (a : A) → AX) '' (↑t : Set A)))) AX)
    (adjoin (↥(adjoin R ((⇑(algebraMap A AX) : (a : A) → AX) '' (↑t : Set A)))) (Set.range MvPolynomial.X)) ⊤
⊢ Eq.{w₂ + 1} (α := Subalgebra R AX)
    (Subalgebra.restrictScalars R (S := ↥(adjoin R ((⇑(algebraMap A AX) : (a : A) → AX) '' (↑t : Set A))))
      (adjoin (↥(adjoin R ((⇑(algebraMap A AX) : (a : A) → AX) '' (↑t : Set A)))) (Set.range MvPolynomial.X)))
    (Subalgebra.restrictScalars R (S := ↥(adjoin R ((⇑(algebraMap A AX) : (a : A) → AX) '' (↑t : Set A)))) ⊤)

Tactic:
refine congrArg (Subalgebra.restrictScalars R) ?_

Premises used: congrArg, Subalgebra.restrictScalars
-- 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)
rw :
  Eq.{w₂ + 1} (α := Subalgebra (↥(Subalgebra.map (IsScalarTower.toAlgHom R A AX) ⊤)) AX)
    (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom R A AX) ⊤)) (Set.range MvPolynomial.X)) ⊤
⊢ Eq.{w₂ + 1} (α := Subalgebra (↥(adjoin R ((⇑(algebraMap A AX) : (a : A) → AX) '' (↑t : Set A)))) AX)
    (adjoin (↥(adjoin R ((⇑(algebraMap A AX) : (a : A) → AX) '' (↑t : Set A)))) (Set.range MvPolynomial.X)) ⊤

Tactic:
rw [adjoin_algebraMap, ht]

Premises used: Algebra.adjoin_algebraMap
-- 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)
a :
  Eq.{w₂ + 1} (α := Subalgebra R AX)
    (Subalgebra.restrictScalars R (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom R A AX) ⊤))
      (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom R A AX) ⊤)) (Set.range MvPolynomial.X)))
    (Subalgebra.restrictScalars R (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom R A AX) ⊤)) ⊤)
⊢ Eq.{w₂ + 1} (α := Subalgebra (↥(Subalgebra.map (IsScalarTower.toAlgHom R A AX) ⊤)) AX)
    (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom R A AX) ⊤)) (Set.range MvPolynomial.X)) ⊤

Tactic:
apply Subalgebra.restrictScalars_injective R

Premises used: Subalgebra.restrictScalars_injective
-- 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)
a :
  Eq (α := Subalgebra R AX) (Subalgebra.restrictScalars R (adjoin A (Set.range MvPolynomial.X)))
    (Subalgebra.restrictScalars R (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom R A AX) ⊤)) ⊤)
a₁ :
  Eq.{w₂ + 1} (α := Subalgebra R AX) (Subalgebra.restrictScalars R (S := A) ⊤)
    (Subalgebra.restrictScalars R (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom R A AX) ⊤)) ⊤)
a₂ :
  Eq.{w₂ + 1} (α := Subalgebra R AX) ⊤
    (Subalgebra.restrictScalars R (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom R A AX) ⊤)) ⊤)
a₃ a₄ : Eq.{w₂ + 1} (α := Subalgebra R AX) ⊤ ⊤
⊢ Eq.{w₂ + 1} (α := Subalgebra R AX)
    (Subalgebra.restrictScalars R (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom R A AX) ⊤))
      (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom R A AX) ⊤)) (Set.range MvPolynomial.X)))
    (Subalgebra.restrictScalars R (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom R A AX) ⊤)) ⊤)

Tactic:
rw [← adjoin_restrictScalars, adjoin_range_X, Subalgebra.restrictScalars_top,
        Subalgebra.restrictScalars_top]

Premises used: MvPolynomial.adjoin_range_X, Algebra.adjoin_restrictScalars, Subalgebra.restrictScalars_top
-- 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)
⊢ Eq (α := Subalgebra R AX) (adjoin R ((⇑(algebraMap A AX) : (a : A) → AX) '' (↑t : Set A) ∪ Set.range MvPolynomial.X))
    ⊤

Tactic:
have ht'' : Algebra.adjoin R (algebraMap A AX '' t ∪ Set.range (X : _ → AX)) = ⊤ := by
      rw [adjoin_union_eq_adjoin_adjoin, ← Subalgebra.restrictScalars_top R (A := AX)
        (S := { x // x ∈ adjoin R ((algebraMap A AX) '' t) })]
      refine congrArg (Subalgebra.restrictScalars R) ?_
      rw [adjoin_algebraMap, ht]
      apply Subalgebra.restrictScalars_injective R
      rw [← adjoin_restrictScalars, adjoin_range_X, Subalgebra.restrictScalars_top,
        Subalgebra.restrictScalars_top]
-- 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)
⊢ Ideal.FG
    (RingHom.ker (F := RingHom.{w₂, w₃} (MvPolynomial (Fin n) A) B)
      (AlgHom.toRingHom
        (MvPolynomial.aeval
          (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
            MvPolynomial.X))))

Tactic:
⟨s.image (map (algebraMap R A)) ∪ t.attach.image g, ?_⟩

Premises used: Algebra.algebraMap, Ideal.FG, Finset.attach, Exists.intro, MvPolynomial.map, Union.union, DFunLike.coe, Finset.image
-- 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)
refine_2 :
  Eq (α := Ideal (MvPolynomial (Fin n) A))
    (Ideal.span
      (↑(Finset.image (⇑(MvPolynomial.map (algebraMap R A)) : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) A) s ∪
            Finset.image g t.attach) :
        Set (MvPolynomial (Fin n) A)))
    (RingHom.ker (F := RingHom.{w₂, w₃} (MvPolynomial (Fin n) A) B)
      (AlgHom.toRingHom
        (MvPolynomial.aeval
          (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
            MvPolynomial.X))))
⊢ Ideal.FG
    (RingHom.ker (F := RingHom.{w₂, w₃} (MvPolynomial (Fin n) A) B)
      (AlgHom.toRingHom
        (MvPolynomial.aeval
          (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
            MvPolynomial.X))))

Tactic:
refine ⟨s.image (map (algebraMap R A)) ∪ t.attach.image g, ?_⟩
-- 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)
refine_2 :
  Eq (α := 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 := RingHom.{w₂, w₃} (MvPolynomial (Fin n) A) B)
      (AlgHom.toRingHom
        (MvPolynomial.aeval
          (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
            MvPolynomial.X))))
⊢ Eq (α := Ideal (MvPolynomial (Fin n) A))
    (Ideal.span
      (↑(Finset.image (⇑(MvPolynomial.map (algebraMap R A)) : (a : MvPolynomial (Fin n) R) → MvPolynomial (Fin n) A) s ∪
            Finset.image g t.attach) :
        Set (MvPolynomial (Fin n) A)))
    (RingHom.ker (F := RingHom.{w₂, w₃} (MvPolynomial (Fin n) A) B)
      (AlgHom.toRingHom
        (MvPolynomial.aeval
          (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
            MvPolynomial.X))))

Tactic:
rw [Finset.coe_union, Finset.coe_image, Finset.coe_image, Finset.attach_eq_univ,
      Finset.coe_univ, Set.image_univ]

Premises used: Set.image_univ, Finset.attach_eq_univ, Finset.coe_univ, Finset.coe_image, Finset.coe_union
-- 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))
refine_2 : Ideal.span s₀ = I
⊢ Eq (α := 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 := RingHom.{w₂, w₃} (MvPolynomial (Fin n) A) B)
      (AlgHom.toRingHom
        (MvPolynomial.aeval
          (Function.comp.{1, w₁ + 1, w₃ + 1} (β := MvPolynomial (Fin n) R) (⇑f : (a : MvPolynomial (Fin n) R) → B)
            MvPolynomial.X))))

Tactic:
change Ideal.span s₀ = I

Premises used: Ideal.span
-- 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))
rw :
  (⇑(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))) :
      Set (MvPolynomial (Fin n) A))
⊢ 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:
rw [Ideal.span_le]

Premises used: Ideal.span_le
-- 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)
    ((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)
⊢ Membership.mem (α := 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))) :
      Set (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)
        x :
      MvPolynomial (Fin n) A)

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

Premises used: RingHom.mem_ker, SetLike.mem_coe