awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FiniteType
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
obtain : ∀ (s : Finset A) (hS : Eq (α := Subalgebra R A) (adjoin R (↑s : Set A)) ⊤), FiniteType S A
⊢ FiniteType S A

Tactic:
obtain ⟨s, hS⟩ := hA.out

Premises used: Algebra.FiniteType.out
-- Module: Mathlib.RingTheory.FiniteType
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

Tactic:
⟨⟨s, eq_top_iff.2 fun b => ?_⟩⟩

Premises used: Iff.mpr, Algebra.FiniteType.mk, Exists.intro, Algebra.eq_top_iff
-- Module: Mathlib.RingTheory.FiniteType
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)) ⊤
refine : ∀ (b : A), Membership.mem (γ := Subalgebra S A) (adjoin S (↑s : Set A)) b
⊢ FiniteType S A

Tactic:
refine ⟨⟨s, eq_top_iff.2 fun b => ?_⟩⟩
-- Module: Mathlib.RingTheory.FiniteType
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
apply : (↑s : Set A) ⊆ (↑(Subalgebra.restrictScalars R (adjoin S (↑s : Set A))) : Set A)
⊢ LE.le (α := Subalgebra R A) (adjoin R (↑s : Set A)) (Subalgebra.restrictScalars R (adjoin S (↑s : Set A)))

Tactic:
apply (Algebra.adjoin_le _ : adjoin R (s : Set A) ≤ Subalgebra.restrictScalars R (adjoin S ↑s))

Premises used: Algebra.adjoin_le
-- Module: Mathlib.RingTheory.FiniteType
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
⊢ (↑s : Set A) ⊆ (↑(adjoin S (↑s : Set A)) : Set A)

Tactic:
Algebra.subset_adjoin

Premises used: Algebra.subset_adjoin
-- Module: Mathlib.RingTheory.FiniteType
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
⊢ (↑s : Set A) ⊆ (↑(adjoin S (↑s : Set A)) : Set A)

Tactic:
exact Algebra.subset_adjoin

Premises used: Algebra.subset_adjoin
-- Module: Mathlib.RingTheory.FiniteType
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)))

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
-- Module: Mathlib.RingTheory.FiniteType
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.le (α := Subalgebra R A) (adjoin R (↑s : Set A)) (Subalgebra.restrictScalars R (adjoin S (↑s : Set A)))
⊢ Membership.mem (γ := Subalgebra S A) (adjoin S (↑s : Set A)) b

Tactic:
le (eq_top_iff.1 hS b)

Premises used: Set.Mem, Iff.mp, Algebra.eq_top_iff
-- Module: Mathlib.RingTheory.FiniteType
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.le (α := Subalgebra R A) (adjoin R (↑s : Set A)) (Subalgebra.restrictScalars R (adjoin S (↑s : Set A)))
⊢ Membership.mem (γ := Subalgebra S A) (adjoin S (↑s : Set A)) b

Tactic:
exact le (eq_top_iff.1 hS b)

Premises used: Iff.mp, Algebra.eq_top_iff
-- Module: Mathlib.RingTheory.FiniteType
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.map f ⊤).FG

Tactic:
‹FiniteType R A›.1.map f

Premises used: Subalgebra.FG.map, Algebra.FiniteType.out
-- Module: Mathlib.RingTheory.FiniteType
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)
h : ⊤ = Subalgebra.map f ⊤
⊢ Subalgebra.FG.{uR, uB} (R := R) (A := B) ⊤

Tactic:
convert! ‹FiniteType R A›.1.map f

Premises used: Subalgebra.FG.map, Algebra.FiniteType.out
-- Module: Mathlib.RingTheory.FiniteType
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.map f ⊤

Tactic:
simpa only [map_top f, @eq_comm _ ⊤, eq_top_iff, AlgHom.mem_range] using hf

Premises used: AlgHom.mem_range, eq_comm, Algebra.eq_top_iff, Algebra.map_top
-- Module: Mathlib.RingTheory.FiniteType
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
hRA : FiniteType R A
e : A ≃ₐ[R] B
⊢ FiniteType R B

Tactic:
hRA.of_surjective e e.surjective

Premises used: Algebra.FiniteType.of_surjective, AlgEquiv.toAlgHom, AlgEquiv.surjective
-- Module: Mathlib.RingTheory.FiniteType
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
hRS : FiniteType R S
hSA : FiniteType S A
⊢ FiniteType R A

Tactic:
⟨fg_trans' hRS.1 hSA.1⟩

Premises used: Algebra.fg_trans', Algebra.FiniteType.mk, Algebra.FiniteType.out
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R_1 : Type uR
S_1 : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
inst : CommSemiring R_1
inst_1 : CommSemiring S_1
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R_1 S_1
inst_5 : Algebra R_1 A
inst_6 : Algebra R_1 B
inst_7 : AddCommMonoid M
inst_8 : Module R_1 M
inst_9 : AddCommMonoid N
inst_10 : Module R_1 N
R : Type u_1
S : Type u_2
inst_11 : CommSemiring R
inst_12 : CommRing S
inst_13 : Algebra R S
I : Ideal S
h : FiniteType R S
⊢ FiniteType.{u_1, u_2} R (S ⧸ I)

Tactic:
Algebra.FiniteType.trans h inferInstance

Premises used: inferInstance, Algebra.FiniteType.trans
-- Module: Mathlib.RingTheory.FiniteType
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]

Tactic:
.trans ‹_› ⟨{Polynomial.X}, ?_⟩

Premises used: Algebra.FiniteType.mk, Exists.intro, Algebra.FiniteType.trans, Singleton.singleton, Polynomial.X
-- Module: Mathlib.RingTheory.FiniteType
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
refine : Eq (α := Subalgebra S S[X]) (adjoin S (↑{X} : Set S[X])) ⊤
⊢ FiniteType.{uR, uS} R S[X]

Tactic:
refine .trans ‹_› ⟨{Polynomial.X}, ?_⟩
-- Module: Mathlib.RingTheory.FiniteType
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
rw : Eq (α := Subalgebra S S[X]) S[ X] ⊤
⊢ Eq (α := Subalgebra S S[X]) (adjoin S (↑{X} : Set S[X])) ⊤

Tactic:
rw [Finset.coe_singleton]

Premises used: Finset.coe_singleton
-- Module: Mathlib.RingTheory.FiniteType
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]) S[ X] ⊤

Tactic:
Polynomial.adjoin_X

Premises used: Polynomial.adjoin_X
-- Module: Mathlib.RingTheory.FiniteType
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]) S[ X] ⊤

Tactic:
exact Polynomial.adjoin_X

Premises used: Polynomial.adjoin_X
-- Module: Mathlib.RingTheory.FiniteType
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)

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.RingTheory.FiniteType
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)

Tactic:
.trans ‹_› ⟨Finset.univ.image MvPolynomial.X, ?_⟩

Premises used: Finset.univ, MvPolynomial.X, Algebra.FiniteType.mk, Exists.intro, Algebra.FiniteType.trans, Finset.image
-- Module: Mathlib.RingTheory.FiniteType
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 ι
intro :
  Eq (α := Subalgebra S (MvPolynomial ι S))
    (adjoin S (↑(Finset.image MvPolynomial.X Finset.univ) : Set (MvPolynomial ι S))) ⊤
⊢ FiniteType R (MvPolynomial ι S)

Tactic:
refine .trans ‹_› ⟨Finset.univ.image MvPolynomial.X, ?_⟩
-- Module: Mathlib.RingTheory.FiniteType
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 ι
intro : Eq (α := Subalgebra S (MvPolynomial ι S)) (adjoin S (Set.range MvPolynomial.X)) ⊤
⊢ Eq (α := Subalgebra S (MvPolynomial ι S))
    (adjoin S (↑(Finset.image MvPolynomial.X Finset.univ) : Set (MvPolynomial ι S))) ⊤

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

Premises used: Set.image_univ, Finset.coe_univ, Finset.coe_image
-- Module: Mathlib.RingTheory.FiniteType
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 (Set.range MvPolynomial.X)) ⊤

Tactic:
MvPolynomial.adjoin_range_X

Premises used: MvPolynomial.adjoin_range_X
-- Module: Mathlib.RingTheory.FiniteType
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 (Set.range MvPolynomial.X)) ⊤

Tactic:
exact MvPolynomial.adjoin_range_X

Premises used: MvPolynomial.adjoin_range_X
-- Module: Mathlib.RingTheory.FiniteType
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))) ⊤
intro₂ : ∀ (val : Fintype ι), Eq (α := Subalgebra S (MvPolynomial ι S)) (adjoin S (Set.range MvPolynomial.X)) ⊤
⊢ 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

Premises used: Set.image_univ, Finset.coe_univ, MvPolynomial.adjoin_range_X, Finset.coe_image, nonempty_fintype
-- Module: Mathlib.RingTheory.FiniteType
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 ι)

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.RingTheory.FiniteType
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 ι)

Tactic:
.trans ‹_› ⟨Finset.univ.image (FreeAlgebra.ι _), ?_⟩

Premises used: FreeAlgebra.ι, Finset.univ, Algebra.FiniteType.mk, Exists.intro, Algebra.FiniteType.trans, Finset.image
-- Module: Mathlib.RingTheory.FiniteType
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 ι
intro :
  Eq (α := Subalgebra S (FreeAlgebra S ι))
    (adjoin S (↑(Finset.image (FreeAlgebra.ι S) Finset.univ) : Set (FreeAlgebra S ι))) ⊤
⊢ FiniteType R (FreeAlgebra S ι)

Tactic:
refine .trans ‹_› ⟨Finset.univ.image (FreeAlgebra.ι _), ?_⟩
-- Module: Mathlib.RingTheory.FiniteType
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 ι
intro : Eq (α := Subalgebra S (FreeAlgebra S ι)) (adjoin S (Set.range (FreeAlgebra.ι S))) ⊤
⊢ Eq (α := Subalgebra S (FreeAlgebra S ι))
    (adjoin S (↑(Finset.image (FreeAlgebra.ι S) Finset.univ) : Set (FreeAlgebra S ι))) ⊤

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

Premises used: Set.image_univ, Finset.coe_univ, Finset.coe_image
-- Module: Mathlib.RingTheory.FiniteType
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 (Set.range (FreeAlgebra.ι S))) ⊤

Tactic:
FreeAlgebra.adjoin_range_ι ..

Premises used: FreeAlgebra.adjoin_range_ι
-- Module: Mathlib.RingTheory.FiniteType
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 (Set.range (FreeAlgebra.ι S))) ⊤

Tactic:
exact FreeAlgebra.adjoin_range_ι ..

Premises used: FreeAlgebra.adjoin_range_ι
-- Module: Mathlib.RingTheory.FiniteType
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 ι))) ⊤
intro₂ : ∀ (val : Fintype ι), Eq (α := Subalgebra S (FreeAlgebra S ι)) (adjoin S (Set.range (FreeAlgebra.ι S))) ⊤
⊢ 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_ι ..

Premises used: Set.image_univ, Finset.coe_univ, Finset.coe_image, nonempty_fintype, FreeAlgebra.adjoin_range_ι
-- Module: Mathlib.RingTheory.FiniteType
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)
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
⊢ 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
-- Module: Mathlib.RingTheory.FiniteType
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)

Tactic:
⟨s, FreeAlgebra.lift _ (↑), ?_⟩

Premises used: Exists.intro, FreeAlgebra.lift, Subtype.val, DFunLike.coe
-- Module: Mathlib.RingTheory.FiniteType
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 :
  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)
⊢ ∃ (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:
refine ⟨s, FreeAlgebra.lift _ (↑), ?_⟩
-- Module: Mathlib.RingTheory.FiniteType
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
mp₅ : (↑⊤ : Set A) = Set.univ
mp₆ mp₇ : Eq.{uA + 1} (α := Set A) Set.univ 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)

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]

Premises used: Set.range_eq_univ, AlgHom.coe_range, Algebra.coe_top, Finset.setOf_mem, Algebra.adjoin_range_eq_range_freeAlgebra_lift, Subtype.range_coe_subtype
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Finset A
f : FreeAlgebra.{uR, uA} R ↥s →ₐ[R] A
hsur : Surjective (α := FreeAlgebra.{uR, uA} R ↥s) (β := A) (⇑f : (a : FreeAlgebra R ↥s) → A)
⊢ FiniteType R A

Tactic:
.of_surjective f hsur

Premises used: Algebra.FiniteType.of_surjective
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
s : Finset A
f : FreeAlgebra.{uR, uA} R ↥s →ₐ[R] A
hsur : Surjective (α := FreeAlgebra.{uR, uA} R ↥s) (β := A) (⇑f : (a : FreeAlgebra R ↥s) → A)
⊢ FiniteType R A

Tactic:
exact .of_surjective f hsur