awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FiniteStability (goal)
Goal:
R : Type w₁
inst : CommRing R
A : Type w₂
inst_1 : CommRing A
inst_2 : Algebra R A
B : Type w₃
inst_3 : CommRing B
inst_4 : Algebra R B
inst_5 : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hsurj :
  Function.Surjective.{w₁ + 1, w₂ + 1} (α := MvPolynomial (Fin n) R) (β := A) (⇑f : (a : MvPolynomial (Fin n) R) → A)
hfg : Ideal.FG (RingHom.ker f.toRingHom)
g : B ⊗[R] MvPolynomial (Fin n) R →ₐ[B] B ⊗[R] A := TensorProduct.map (AlgHom.id B B) f
hgsurj :
  Function.Surjective (α := B ⊗[R] MvPolynomial (Fin n) R) (β := B ⊗[R] A)
    (⇑g : (a : B ⊗[R] MvPolynomial (Fin n) R) → B ⊗[R] A)
hker_eq :
  Eq (α := Ideal (B ⊗[R] MvPolynomial (Fin n) R)) (RingHom.ker g)
    (Ideal.map (F := MvPolynomial (Fin n) R →ₐ[R] B ⊗[R] MvPolynomial (Fin n) R) TensorProduct.includeRight
      (RingHom.ker f))
hfgg : Ideal.FG (RingHom.ker g)
g' : MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] A :=
  g.comp
    (↑(AlgEquiv.symm (MvPolynomial.algebraTensorAlgEquiv R B)) :
      MvPolynomial (Fin n) B →ₐ[B] B ⊗[R] MvPolynomial (Fin n) R)
⊢ Ideal.FG
    (RingHom.ker (F := MvPolynomial (Fin n) B ≃ₐ[B] B ⊗[R] MvPolynomial (Fin n) R)
      (AlgEquiv.symm (MvPolynomial.algebraTensorAlgEquiv R B)))
have refine_2 : Ideal.FG.{w₃} (R := MvPolynomial (Fin n) B) ⊥
Tactic: simp only [RingHom.ker_equiv]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
hA : FiniteType R A
⊢ FiniteType S A
have obtain : ∀ (s : Finset A) (hS : Eq (α := Subalgebra R A) (adjoin R (↑s : Set A)) ⊤), FiniteType S A
Tactic: obtain ⟨s, hS⟩ := hA.out
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
hA : FiniteType R A
s : Finset A
hS : Eq (α := Subalgebra R A) (adjoin R (↑s : Set A)) ⊤
⊢ FiniteType S A
have refine : ∀ (b : A), Membership.mem (γ := Subalgebra S A) (adjoin S (↑s : Set A)) b
Tactic: refine ⟨⟨s, eq_top_iff.2 fun b => ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
hA : FiniteType R A
s : Finset A
hS : Eq (α := Subalgebra R A) (adjoin R (↑s : Set A)) ⊤
b : A
⊢ LE.le (α := Subalgebra R A) (adjoin R (↑s : Set A)) (Subalgebra.restrictScalars R (adjoin S (↑s : Set A)))
have apply : (↑s : Set A) ⊆ (↑(Subalgebra.restrictScalars R (adjoin S (↑s : Set A))) : Set A)
Tactic: apply (Algebra.adjoin_le _ : adjoin R (s : Set A) ≤ Subalgebra.restrictScalars R (adjoin S ↑s))
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (hypothesis)
Goal:
R : Type uR
S : Type uS
A : Type uA
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R S
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
hA : FiniteType R A
s : Finset A
hS : Eq (α := Subalgebra R A) (adjoin R (↑s : Set A)) ⊤
b : A
⊢ Membership.mem (γ := Subalgebra S A) (adjoin S (↑s : Set A)) b
have le : LE.le (α := Subalgebra R A) (adjoin R (↑s : Set A)) (Subalgebra.restrictScalars R (adjoin S (↑s : Set A)))
Tactic: have le : adjoin R (s : Set A) ≤ Subalgebra.restrictScalars R (adjoin S s) := by
    apply (Algebra.adjoin_le _ : adjoin R (s : Set A) ≤ Subalgebra.restrictScalars R (adjoin S ↑s))
    simp only [Subalgebra.coe_restrictScalars]
    exact Algebra.subset_adjoin
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
A : Type uA
B : Type uB
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : FiniteType R A
f : A →ₐ[R] B
hf : Surjective.{uA + 1, uB + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ Subalgebra.FG.{uR, uB} (R := R) (A := B) ⊤
have h : ⊤ = Subalgebra.map f ⊤
Tactic: convert! ‹FiniteType R A›.1.map f
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : AddCommMonoid M
inst_8 : Module R M
inst_9 : AddCommMonoid N
inst_10 : Module R N
inst_11 : FiniteType R S
⊢ FiniteType.{uR, uS} R S[X]
have refine : Eq (α := Subalgebra S S[X]) (adjoin S (↑{X} : Set S[X])) ⊤
Tactic: refine .trans ‹_› ⟨{Polynomial.X}, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : AddCommMonoid M
inst_8 : Module R M
inst_9 : AddCommMonoid N
inst_10 : Module R N
inst_11 : FiniteType R S
⊢ Eq (α := Subalgebra S S[X]) (adjoin S (↑{X} : Set S[X])) ⊤
have rw : Eq (α := Subalgebra S S[X]) S[ X] ⊤
Tactic: rw [Finset.coe_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : AddCommMonoid M
inst_8 : Module R M
inst_9 : AddCommMonoid N
inst_10 : Module R N
ι : Type u_1
inst_11 : Finite ι
inst_12 : FiniteType R S
⊢ FiniteType R (MvPolynomial ι S)
have intro : ∀ (val : Fintype ι), FiniteType R (MvPolynomial ι S)
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : AddCommMonoid M
inst_8 : Module R M
inst_9 : AddCommMonoid N
inst_10 : Module R N
ι : Type u_1
inst_11 : Finite ι
inst_12 : FiniteType R S
val : Fintype ι
⊢ FiniteType R (MvPolynomial ι S)
have intro : Eq (α := Subalgebra S (MvPolynomial ι S))
  (adjoin S (↑(Finset.image MvPolynomial.X Finset.univ) : Set (MvPolynomial ι S))) ⊤
Tactic: refine .trans ‹_› ⟨Finset.univ.image MvPolynomial.X, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : AddCommMonoid M
inst_8 : Module R M
inst_9 : AddCommMonoid N
inst_10 : Module R N
ι : Type u_1
inst_11 : Finite ι
inst_12 : FiniteType R S
val : Fintype ι
⊢ Eq (α := Subalgebra S (MvPolynomial ι S))
    (adjoin S (↑(Finset.image MvPolynomial.X Finset.univ) : Set (MvPolynomial ι S))) ⊤
have intro : Eq (α := Subalgebra S (MvPolynomial ι S)) (adjoin S (Set.range MvPolynomial.X)) ⊤
Tactic: rw [Finset.coe_image, Finset.coe_univ, Set.image_univ]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : AddCommMonoid M
inst_8 : Module R M
inst_9 : AddCommMonoid N
inst_10 : Module R N
ι : Type u_1
inst_11 : Finite ι
inst_12 : FiniteType R S
⊢ FiniteType R (MvPolynomial ι S)
have intro : ∀ (val : Fintype ι), FiniteType R (MvPolynomial ι S)
Tactic: classical
  cases nonempty_fintype ι
  refine .trans ‹_› ⟨Finset.univ.image MvPolynomial.X, ?_⟩
  rw [Finset.coe_image, Finset.coe_univ, Set.image_univ]
  exact MvPolynomial.adjoin_range_X
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : AddCommMonoid M
inst_8 : Module R M
inst_9 : AddCommMonoid N
inst_10 : Module R N
ι : Type u_1
inst_11 : Finite ι
inst_12 : FiniteType R S
intro : ∀ (val : Fintype ι), FiniteType R (MvPolynomial ι S)
⊢ FiniteType R (MvPolynomial ι S)
have intro₁ : ∀ (val : Fintype ι),
  Eq (α := Subalgebra S (MvPolynomial ι S))
    (adjoin S (↑(Finset.image MvPolynomial.X Finset.univ) : Set (MvPolynomial ι S))) ⊤
Tactic: classical
  cases nonempty_fintype ι
  refine .trans ‹_› ⟨Finset.univ.image MvPolynomial.X, ?_⟩
  rw [Finset.coe_image, Finset.coe_univ, Set.image_univ]
  exact MvPolynomial.adjoin_range_X
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : AddCommMonoid M
inst_8 : Module R M
inst_9 : AddCommMonoid N
inst_10 : Module R N
ι : Type u_1
inst_11 : Finite ι
inst_12 : FiniteType R S
intro : ∀ (val : Fintype ι), FiniteType R (MvPolynomial ι S)
intro₁ :
  ∀ (val : Fintype ι),
    Eq (α := Subalgebra S (MvPolynomial ι S))
      (adjoin S (↑(Finset.image MvPolynomial.X Finset.univ) : Set (MvPolynomial ι S))) ⊤
⊢ FiniteType R (MvPolynomial ι S)
have intro₂ : ∀ (val : Fintype ι), Eq (α := Subalgebra S (MvPolynomial ι S)) (adjoin S (Set.range MvPolynomial.X)) ⊤
Tactic: classical
  cases nonempty_fintype ι
  refine .trans ‹_› ⟨Finset.univ.image MvPolynomial.X, ?_⟩
  rw [Finset.coe_image, Finset.coe_univ, Set.image_univ]
  exact MvPolynomial.adjoin_range_X
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : AddCommMonoid M
inst_8 : Module R M
inst_9 : AddCommMonoid N
inst_10 : Module R N
ι : Type u_1
inst_11 : Finite ι
inst_12 : FiniteType R S
⊢ FiniteType R (FreeAlgebra S ι)
have intro : ∀ (val : Fintype ι), FiniteType R (FreeAlgebra S ι)
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : AddCommMonoid M
inst_8 : Module R M
inst_9 : AddCommMonoid N
inst_10 : Module R N
ι : Type u_1
inst_11 : Finite ι
inst_12 : FiniteType R S
val : Fintype ι
⊢ FiniteType R (FreeAlgebra S ι)
have intro : Eq (α := Subalgebra S (FreeAlgebra S ι))
  (adjoin S (↑(Finset.image (FreeAlgebra.ι S) Finset.univ) : Set (FreeAlgebra S ι))) ⊤
Tactic: refine .trans ‹_› ⟨Finset.univ.image (FreeAlgebra.ι _), ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : AddCommMonoid M
inst_8 : Module R M
inst_9 : AddCommMonoid N
inst_10 : Module R N
ι : Type u_1
inst_11 : Finite ι
inst_12 : FiniteType R S
val : Fintype ι
⊢ Eq (α := Subalgebra S (FreeAlgebra S ι))
    (adjoin S (↑(Finset.image (FreeAlgebra.ι S) Finset.univ) : Set (FreeAlgebra S ι))) ⊤
have intro : Eq (α := Subalgebra S (FreeAlgebra S ι)) (adjoin S (Set.range (FreeAlgebra.ι S))) ⊤
Tactic: rw [Finset.coe_image, Finset.coe_univ, Set.image_univ]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : AddCommMonoid M
inst_8 : Module R M
inst_9 : AddCommMonoid N
inst_10 : Module R N
ι : Type u_1
inst_11 : Finite ι
inst_12 : FiniteType R S
⊢ FiniteType R (FreeAlgebra S ι)
have intro : ∀ (val : Fintype ι), FiniteType R (FreeAlgebra S ι)
Tactic: classical
  cases nonempty_fintype ι
  refine .trans ‹_› ⟨Finset.univ.image (FreeAlgebra.ι _), ?_⟩
  rw [Finset.coe_image, Finset.coe_univ, Set.image_univ]
  exact FreeAlgebra.adjoin_range_ι ..
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : AddCommMonoid M
inst_8 : Module R M
inst_9 : AddCommMonoid N
inst_10 : Module R N
ι : Type u_1
inst_11 : Finite ι
inst_12 : FiniteType R S
intro : ∀ (val : Fintype ι), FiniteType R (FreeAlgebra S ι)
⊢ FiniteType R (FreeAlgebra S ι)
have intro₁ : ∀ (val : Fintype ι),
  Eq (α := Subalgebra S (FreeAlgebra S ι))
    (adjoin S (↑(Finset.image (FreeAlgebra.ι S) Finset.univ) : Set (FreeAlgebra S ι))) ⊤
Tactic: classical
  cases nonempty_fintype ι
  refine .trans ‹_› ⟨Finset.univ.image (FreeAlgebra.ι _), ?_⟩
  rw [Finset.coe_image, Finset.coe_univ, Set.image_univ]
  exact FreeAlgebra.adjoin_range_ι ..
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : AddCommMonoid M
inst_8 : Module R M
inst_9 : AddCommMonoid N
inst_10 : Module R N
ι : Type u_1
inst_11 : Finite ι
inst_12 : FiniteType R S
intro : ∀ (val : Fintype ι), FiniteType R (FreeAlgebra S ι)
intro₁ :
  ∀ (val : Fintype ι),
    Eq (α := Subalgebra S (FreeAlgebra S ι))
      (adjoin S (↑(Finset.image (FreeAlgebra.ι S) Finset.univ) : Set (FreeAlgebra S ι))) ⊤
⊢ FiniteType R (FreeAlgebra S ι)
have intro₂ : ∀ (val : Fintype ι), Eq (α := Subalgebra S (FreeAlgebra S ι)) (adjoin S (Set.range (FreeAlgebra.ι S))) ⊤
Tactic: classical
  cases nonempty_fintype ι
  refine .trans ‹_› ⟨Finset.univ.image (FreeAlgebra.ι _), ?_⟩
  rw [Finset.coe_image, Finset.coe_univ, Set.image_univ]
  exact FreeAlgebra.adjoin_range_ι ..
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ FiniteType R A ↔
    ∃ (s : Finset A) (f : FreeAlgebra.{uR, uA} R ↥s →ₐ[R] A),
      Surjective (α := FreeAlgebra.{uR, uA} R ↥s) (β := A) (⇑f : (a : FreeAlgebra R ↥s) → A)
have mp : FiniteType R A →
  ∃ (s : Finset A) (f : FreeAlgebra.{uR, uA} R ↥s →ₐ[R] A),
    Surjective (α := FreeAlgebra.{uR, uA} R ↥s) (β := A) (⇑f : (a : FreeAlgebra R ↥s) → A)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
mp :
  FiniteType R A →
    ∃ (s : Finset A) (f : FreeAlgebra.{uR, uA} R ↥s →ₐ[R] A),
      Surjective (α := FreeAlgebra.{uR, uA} R ↥s) (β := A) (⇑f : (a : FreeAlgebra R ↥s) → A)
⊢ FiniteType R A ↔
    ∃ (s : Finset A) (f : FreeAlgebra.{uR, uA} R ↥s →ₐ[R] A),
      Surjective (α := FreeAlgebra.{uR, uA} R ↥s) (β := A) (⇑f : (a : FreeAlgebra R ↥s) → A)
have mpr : (∃ (s : Finset A) (f : FreeAlgebra.{uR, uA} R ↥s →ₐ[R] A),
    Surjective (α := FreeAlgebra.{uR, uA} R ↥s) (β := A) (⇑f : (a : FreeAlgebra R ↥s) → A)) →
  FiniteType R A
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Finset A
hs : Eq (α := Subalgebra R A) (adjoin R (↑s : Set A)) ⊤
⊢ ∃ (s : Finset A) (f : FreeAlgebra.{uR, uA} R ↥s →ₐ[R] A),
    Surjective (α := FreeAlgebra.{uR, uA} R ↥s) (β := A) (⇑f : (a : FreeAlgebra R ↥s) → A)
have mp : Surjective (α := FreeAlgebra.{uR, uA} R ↥s) (β := A)
  (⇑((FreeAlgebra.lift R : (a : ↥s → A) → FreeAlgebra R ↥s →ₐ[R] A) (Subtype.val (p := fun (x : A) ↦ x ∈ s)) :
        FreeAlgebra.{uR, uA} R ↥s →ₐ[R] A) :
    (a : FreeAlgebra R ↥s) → A)
Tactic: refine ⟨s, FreeAlgebra.lift _ (↑), ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Finset A
hs : Eq (α := Subalgebra R A) (adjoin R (↑s : Set A)) ⊤
⊢ Surjective (α := FreeAlgebra.{uR, uA} R ↥s) (β := A)
    (⇑((FreeAlgebra.lift R : (a : ↥s → A) → FreeAlgebra R ↥s →ₐ[R] A) (Subtype.val (p := fun (x : A) ↦ x ∈ s)) :
          FreeAlgebra.{uR, uA} R ↥s →ₐ[R] A) :
      (a : FreeAlgebra R ↥s) → A)
have mp : Eq.{uA + 1} (α := Set A)
  (Set.range (ι := FreeAlgebra.{uR, uA} R ↥s)
    (⇑((FreeAlgebra.lift R : (a : ↥s → A) → FreeAlgebra R ↥s →ₐ[R] A) (Subtype.val (p := fun (x : A) ↦ x ∈ s)) :
          FreeAlgebra.{uR, uA} R ↥s →ₐ[R] A) :
      (a : FreeAlgebra R ↥s) → A))
  Set.univ
Tactic: rw [← Set.range_eq_univ, ← AlgHom.coe_range, ← adjoin_range_eq_range_freeAlgebra_lift,
      Subtype.range_coe_subtype, Finset.setOf_mem, hs, coe_top]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Finset A
hs : Eq (α := Subalgebra R A) (adjoin R (↑s : Set A)) ⊤
mp :
  Eq.{uA + 1} (α := Set A)
    (Set.range (ι := FreeAlgebra.{uR, uA} R ↥s)
      (⇑((FreeAlgebra.lift R : (a : ↥s → A) → FreeAlgebra R ↥s →ₐ[R] A) (Subtype.val (p := fun (x : A) ↦ x ∈ s)) :
            FreeAlgebra.{uR, uA} R ↥s →ₐ[R] A) :
        (a : FreeAlgebra R ↥s) → A))
    Set.univ
⊢ Surjective (α := FreeAlgebra.{uR, uA} R ↥s) (β := A)
    (⇑((FreeAlgebra.lift R : (a : ↥s → A) → FreeAlgebra R ↥s →ₐ[R] A) (Subtype.val (p := fun (x : A) ↦ x ∈ s)) :
          FreeAlgebra.{uR, uA} R ↥s →ₐ[R] A) :
      (a : FreeAlgebra R ↥s) → A)
have mp₁ : (↑(AlgHom.range (A := FreeAlgebra.{uR, uA} R ↥s)
        ((FreeAlgebra.lift R : (a : ↥s → A) → FreeAlgebra R ↥s →ₐ[R] A) (Subtype.val (p := fun (x : A) ↦ x ∈ s)))) :
    Set A) =
  Set.univ
Tactic: rw [← Set.range_eq_univ, ← AlgHom.coe_range, ← adjoin_range_eq_range_freeAlgebra_lift,
      Subtype.range_coe_subtype, Finset.setOf_mem, hs, coe_top]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Finset A
hs : Eq (α := Subalgebra R A) (adjoin R (↑s : Set A)) ⊤
mp :
  Eq.{uA + 1} (α := Set A)
    (Set.range (ι := FreeAlgebra.{uR, uA} R ↥s)
      (⇑((FreeAlgebra.lift R : (a : ↥s → A) → FreeAlgebra R ↥s →ₐ[R] A) (Subtype.val (p := fun (x : A) ↦ x ∈ s)) :
            FreeAlgebra.{uR, uA} R ↥s →ₐ[R] A) :
        (a : FreeAlgebra R ↥s) → A))
    Set.univ
mp₁ :
  (↑(AlgHom.range (A := FreeAlgebra.{uR, uA} R ↥s)
          ((FreeAlgebra.lift R : (a : ↥s → A) → FreeAlgebra R ↥s →ₐ[R] A) (Subtype.val (p := fun (x : A) ↦ x ∈ s)))) :
      Set A) =
    Set.univ
⊢ Surjective (α := FreeAlgebra.{uR, uA} R ↥s) (β := A)
    (⇑((FreeAlgebra.lift R : (a : ↥s → A) → FreeAlgebra R ↥s →ₐ[R] A) (Subtype.val (p := fun (x : A) ↦ x ∈ s)) :
          FreeAlgebra.{uR, uA} R ↥s →ₐ[R] A) :
      (a : FreeAlgebra R ↥s) → A)
have mp₂ : (↑(adjoin R (Set.range (ι := ↥s) (Subtype.val (p := fun (x : A) ↦ x ∈ s)))) : Set A) = Set.univ
Tactic: rw [← Set.range_eq_univ, ← AlgHom.coe_range, ← adjoin_range_eq_range_freeAlgebra_lift,
      Subtype.range_coe_subtype, Finset.setOf_mem, hs, coe_top]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Finset A
hs : Eq (α := Subalgebra R A) (adjoin R (↑s : Set A)) ⊤
mp :
  Eq.{uA + 1} (α := Set A)
    (Set.range (ι := FreeAlgebra.{uR, uA} R ↥s)
      (⇑((FreeAlgebra.lift R : (a : ↥s → A) → FreeAlgebra R ↥s →ₐ[R] A) (Subtype.val (p := fun (x : A) ↦ x ∈ s)) :
            FreeAlgebra.{uR, uA} R ↥s →ₐ[R] A) :
        (a : FreeAlgebra R ↥s) → A))
    Set.univ
mp₁ :
  (↑(AlgHom.range (A := FreeAlgebra.{uR, uA} R ↥s)
          ((FreeAlgebra.lift R : (a : ↥s → A) → FreeAlgebra R ↥s →ₐ[R] A) (Subtype.val (p := fun (x : A) ↦ x ∈ s)))) :
      Set A) =
    Set.univ
mp₂ : (↑(adjoin R (Set.range (ι := ↥s) (Subtype.val (p := fun (x : A) ↦ x ∈ s)))) : Set A) = Set.univ
⊢ Surjective (α := FreeAlgebra.{uR, uA} R ↥s) (β := A)
    (⇑((FreeAlgebra.lift R : (a : ↥s → A) → FreeAlgebra R ↥s →ₐ[R] A) (Subtype.val (p := fun (x : A) ↦ x ∈ s)) :
          FreeAlgebra.{uR, uA} R ↥s →ₐ[R] A) :
      (a : FreeAlgebra R ↥s) → A)
have mp₃ : (↑(adjoin R {x : A | x ∈ s}) : Set A) = Set.univ
Tactic: rw [← Set.range_eq_univ, ← AlgHom.coe_range, ← adjoin_range_eq_range_freeAlgebra_lift,
      Subtype.range_coe_subtype, Finset.setOf_mem, hs, coe_top]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Finset A
hs : Eq (α := Subalgebra R A) (adjoin R (↑s : Set A)) ⊤
mp :
  Eq.{uA + 1} (α := Set A)
    (Set.range (ι := FreeAlgebra.{uR, uA} R ↥s)
      (⇑((FreeAlgebra.lift R : (a : ↥s → A) → FreeAlgebra R ↥s →ₐ[R] A) (Subtype.val (p := fun (x : A) ↦ x ∈ s)) :
            FreeAlgebra.{uR, uA} R ↥s →ₐ[R] A) :
        (a : FreeAlgebra R ↥s) → A))
    Set.univ
mp₁ :
  (↑(AlgHom.range (A := FreeAlgebra.{uR, uA} R ↥s)
          ((FreeAlgebra.lift R : (a : ↥s → A) → FreeAlgebra R ↥s →ₐ[R] A) (Subtype.val (p := fun (x : A) ↦ x ∈ s)))) :
      Set A) =
    Set.univ
mp₂ : (↑(adjoin R (Set.range (ι := ↥s) (Subtype.val (p := fun (x : A) ↦ x ∈ s)))) : Set A) = Set.univ
mp₃ : (↑(adjoin R {x : A | x ∈ s}) : Set A) = Set.univ
⊢ Surjective (α := FreeAlgebra.{uR, uA} R ↥s) (β := A)
    (⇑((FreeAlgebra.lift R : (a : ↥s → A) → FreeAlgebra R ↥s →ₐ[R] A) (Subtype.val (p := fun (x : A) ↦ x ∈ s)) :
          FreeAlgebra.{uR, uA} R ↥s →ₐ[R] A) :
      (a : FreeAlgebra R ↥s) → A)
have mp₄ : (↑(adjoin R (↑s : Set A)) : Set A) = Set.univ
Tactic: rw [← Set.range_eq_univ, ← AlgHom.coe_range, ← adjoin_range_eq_range_freeAlgebra_lift,
      Subtype.range_coe_subtype, Finset.setOf_mem, hs, coe_top]
-- Lean 4 proof step from Mathlib.RingTheory.FiniteType (goal)
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Finset A
hs : Eq (α := Subalgebra R A) (adjoin R (↑s : Set A)) ⊤
mp :
  Eq.{uA + 1} (α := Set A)
    (Set.range (ι := FreeAlgebra.{uR, uA} R ↥s)
      (⇑((FreeAlgebra.lift R : (a : ↥s → A) → FreeAlgebra R ↥s →ₐ[R] A) (Subtype.val (p := fun (x : A) ↦ x ∈ s)) :
            FreeAlgebra.{uR, uA} R ↥s →ₐ[R] A) :
        (a : FreeAlgebra R ↥s) → A))
    Set.univ
mp₁ :
  (↑(AlgHom.range (A := FreeAlgebra.{uR, uA} R ↥s)
          ((FreeAlgebra.lift R : (a : ↥s → A) → FreeAlgebra R ↥s →ₐ[R] A) (Subtype.val (p := fun (x : A) ↦ x ∈ s)))) :
      Set A) =
    Set.univ
mp₂ : (↑(adjoin R (Set.range (ι := ↥s) (Subtype.val (p := fun (x : A) ↦ x ∈ s)))) : Set A) = Set.univ
mp₃ : (↑(adjoin R {x : A | x ∈ s}) : Set A) = Set.univ
mp₄ : (↑(adjoin R (↑s : Set A)) : Set A) = Set.univ
⊢ Surjective (α := FreeAlgebra.{uR, uA} R ↥s) (β := A)
    (⇑((FreeAlgebra.lift R : (a : ↥s → A) → FreeAlgebra R ↥s →ₐ[R] A) (Subtype.val (p := fun (x : A) ↦ x ∈ s)) :
          FreeAlgebra.{uR, uA} R ↥s →ₐ[R] A) :
      (a : FreeAlgebra R ↥s) → A)
have mp₅ : (↑⊤ : Set A) = Set.univ
Tactic: rw [← Set.range_eq_univ, ← AlgHom.coe_range, ← adjoin_range_eq_range_freeAlgebra_lift,
      Subtype.range_coe_subtype, Finset.setOf_mem, hs, coe_top]