awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (hypothesis)
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)) ⊤
⊢ 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))))
have this : ∀ (i : ↥t),
  ∃ (a : MvPolynomial (Fin n) R),
    Eq.{w₃ + 1} (α := B) ((f : (a : MvPolynomial (Fin n) R) → B) a : B) ((algebraMap A B : (a : A) → B) (↑i : A) : B)
Tactic: have := fun i : t => hf (algebraMap A B i)
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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)) ⊤
this :
  ∀ (i : ↥t),
    ∃ (a : MvPolynomial (Fin n) R),
      Eq.{w₃ + 1} (α := B) ((f : (a : MvPolynomial (Fin n) R) → B) a : B) ((algebraMap A B : (a : A) → B) (↑i : A) : B)
⊢ 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))))
have refine_2 : ∀ (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)),
  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: choose t' ht' using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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))
    ⊤
have rw : 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: rw [adjoin_union_eq_adjoin_adjoin, ← Subalgebra.restrictScalars_top R (A := AX)
        (S := { x // x ∈ adjoin R ((algebraMap A AX) '' t) })]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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.{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)))) ⊤)
have 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)) ⊤
Tactic: refine congrArg (Subalgebra.restrictScalars R) ?_
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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.{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)) ⊤
have 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)) ⊤
Tactic: rw [adjoin_algebraMap, ht]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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.{w₂ + 1} (α := Subalgebra (↥(Subalgebra.map (IsScalarTower.toAlgHom R A AX) ⊤)) AX)
    (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom R A AX) ⊤)) (Set.range MvPolynomial.X)) ⊤
have 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) ⊤)) ⊤)
Tactic: apply Subalgebra.restrictScalars_injective R
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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.{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) ⊤)) ⊤)
have 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) ⊤)) ⊤)
Tactic: rw [← adjoin_restrictScalars, adjoin_range_X, Subalgebra.restrictScalars_top,
        Subalgebra.restrictScalars_top]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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) ⊤)) ⊤)
⊢ 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) ⊤)) ⊤)
have a₁ : Eq.{w₂ + 1} (α := Subalgebra R AX) (Subalgebra.restrictScalars R (S := A) ⊤)
  (Subalgebra.restrictScalars R (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom R A AX) ⊤)) ⊤)
Tactic: rw [← adjoin_restrictScalars, adjoin_range_X, Subalgebra.restrictScalars_top,
        Subalgebra.restrictScalars_top]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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) ⊤)) ⊤)
⊢ 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) ⊤)) ⊤)
have a₂ : Eq.{w₂ + 1} (α := Subalgebra R AX) ⊤
  (Subalgebra.restrictScalars R (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom R A AX) ⊤)) ⊤)
Tactic: rw [← adjoin_restrictScalars, adjoin_range_X, Subalgebra.restrictScalars_top,
        Subalgebra.restrictScalars_top]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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) ⊤)) ⊤)
⊢ 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) ⊤)) ⊤)
have a₃ : Eq.{w₂ + 1} (α := Subalgebra R AX) ⊤ ⊤
Tactic: rw [← adjoin_restrictScalars, adjoin_range_X, Subalgebra.restrictScalars_top,
        Subalgebra.restrictScalars_top]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (hypothesis)
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)
⊢ 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))))
have ht'' : 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]
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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))))
have 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))))
Tactic: refine ⟨s.image (map (algebraMap R A)) ∪ t.attach.image g, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.FinitePresentation (goal)
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)
⊢ 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))))
have 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))))
Tactic: rw [Finset.coe_union, Finset.coe_image, Finset.coe_image, Finset.attach_eq_univ,
      Finset.coe_univ, Set.image_univ]