awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
mp :
  FiniteType R S →
    ∃ (s : Finset S) (f : MvPolynomial.{uS, uR} (↥s) R →ₐ[R] S),
      Surjective (α := MvPolynomial.{uS, uR} (↥s) R) (β := S) (⇑f : (a : MvPolynomial (↥s) R) → S)
mpr :
  (∃ (s : Finset S) (f : MvPolynomial.{uS, uR} (↥s) R →ₐ[R] S),
      Surjective (α := MvPolynomial.{uS, uR} (↥s) R) (β := S) (⇑f : (a : MvPolynomial (↥s) R) → S)) →
    FiniteType R S
⊢ FiniteType R S ↔
    ∃ (s : Finset S) (f : MvPolynomial.{uS, uR} (↥s) R →ₐ[R] S),
      Surjective (α := MvPolynomial.{uS, uR} (↥s) R) (β := S) (⇑f : (a : MvPolynomial (↥s) R) → S)

Tactic:
constructor
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
h :
  Surjective (α := MvPolynomial.{uS, uR} (↥s) R) (β := S)
    (⇑(MvPolynomial.aeval (Subtype.val (p := fun (x : S) ↦ x ∈ s))) : (a : MvPolynomial (↥s) R) → S)
⊢ ∃ (s : Finset S) (f : MvPolynomial.{uS, uR} (↥s) R →ₐ[R] S),
    Surjective (α := MvPolynomial.{uS, uR} (↥s) R) (β := S) (⇑f : (a : MvPolynomial (↥s) R) → S)

Tactic:
use s, MvPolynomial.aeval (↑)

Premises used: MvPolynomial.aeval
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
x : S
h : Membership.mem (γ := Subalgebra R S) ⊤ x
⊢ ∃ (a : MvPolynomial.{uS, uR} (↥s) R),
    (MvPolynomial.aeval (Subtype.val (p := fun (x : S) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → S) a = x

Tactic:
rw [← Set.mem_range, ← AlgHom.coe_range, ← adjoin_eq_range, SetLike.mem_coe, hs]

Premises used: Set.mem_range, AlgHom.coe_range, Algebra.adjoin_eq_range, SetLike.mem_coe
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
x : S
⊢ Membership.mem (γ := Subalgebra R S) ⊤ x

Tactic:
apply mem_top

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

Tactic:
.of_surjective f hsur

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

Tactic:
exact .of_surjective f hsur
-- 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 →
    ∃ (ι : Type uA) (x : Fintype ι) (f : FreeAlgebra R ι →ₐ[R] A),
      Surjective (α := FreeAlgebra R ι) (β := A) (⇑f : (a : FreeAlgebra R ι) → A)
mpr :
  (∃ (ι : Type uA) (x : Fintype ι) (f : FreeAlgebra R ι →ₐ[R] A),
      Surjective (α := FreeAlgebra R ι) (β := A) (⇑f : (a : FreeAlgebra R ι) → A)) →
    FiniteType R A
⊢ FiniteType R A ↔
    ∃ (ι : Type uA) (x : Fintype ι) (f : FreeAlgebra R ι →ₐ[R] A),
      Surjective (α := FreeAlgebra R ι) (β := A) (⇑f : (a : FreeAlgebra R ι) → 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
mp :
  (∃ (s : Finset A) (f : FreeAlgebra.{uR, uA} R ↥s →ₐ[R] A),
      Surjective (α := FreeAlgebra.{uR, uA} R ↥s) (β := A) (⇑f : (a : FreeAlgebra R ↥s) → A)) →
    ∃ (ι : Type uA) (x : Fintype ι) (f : FreeAlgebra R ι →ₐ[R] A),
      Surjective (α := FreeAlgebra R ι) (β := A) (⇑f : (a : FreeAlgebra R ι) → A)
⊢ FiniteType R A →
    ∃ (ι : Type uA) (x : Fintype ι) (f : FreeAlgebra R ι →ₐ[R] A),
      Surjective (α := FreeAlgebra R ι) (β := A) (⇑f : (a : FreeAlgebra R ι) → A)

Tactic:
rw [iff_quotient_freeAlgebra]

Premises used: Algebra.FiniteType.iff_quotient_freeAlgebra
-- 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)
w : Type uA
w₁ : Fintype ↥s
w₂ : FreeAlgebra.{uR, uA} R ↥s →ₐ[R] A
h : Surjective (α := FreeAlgebra.{uR, uA} R ↥s) (β := A) (⇑f : (a : FreeAlgebra R ↥s) → A)
⊢ ∃ (ι : Type uA) (x : Fintype ι) (f : FreeAlgebra R ι →ₐ[R] A),
    Surjective (α := FreeAlgebra R ι) (β := A) (⇑f : (a : FreeAlgebra R ι) → A)

Tactic:
use { x : A // x ∈ s }, inferInstance, f
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
ι : Type uA
hfintype : Fintype ι
f : FreeAlgebra R ι →ₐ[R] A
hsur : Surjective (α := FreeAlgebra R ι) (β := A) (⇑f : (a : FreeAlgebra R ι) → A)
this : Fintype ι := hfintype
⊢ 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
ι : Type uA
hfintype : Fintype ι
f : FreeAlgebra R ι →ₐ[R] A
hsur : Surjective (α := FreeAlgebra R ι) (β := A) (⇑f : (a : FreeAlgebra R ι) → A)
this : Fintype ι := hfintype
⊢ FiniteType R A

Tactic:
exact .of_surjective f hsur
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
mp :
  FiniteType R S →
    ∃ (ι : Type uS) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] S),
      Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)
mpr :
  (∃ (ι : Type uS) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] S),
      Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)) →
    FiniteType R S
⊢ FiniteType R S ↔
    ∃ (ι : Type uS) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] S),
      Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)

Tactic:
constructor
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
mp :
  (∃ (s : Finset S) (f : MvPolynomial.{uS, uR} (↥s) R →ₐ[R] S),
      Surjective (α := MvPolynomial.{uS, uR} (↥s) R) (β := S) (⇑f : (a : MvPolynomial (↥s) R) → S)) →
    ∃ (ι : Type uS) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] S),
      Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)
⊢ FiniteType R S →
    ∃ (ι : Type uS) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] S),
      Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)

Tactic:
rw [iff_quotient_mvPolynomial]

Premises used: Algebra.FiniteType.iff_quotient_mvPolynomial
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
s : Finset S
f : MvPolynomial.{uS, uR} (↥s) R →ₐ[R] S
hsur : Surjective (α := MvPolynomial.{uS, uR} (↥s) R) (β := S) (⇑f : (a : MvPolynomial (↥s) R) → S)
w : Type uS
w₁ : Fintype ↥s
w₂ : MvPolynomial.{uS, uR} (↥s) R →ₐ[R] S
h : Surjective (α := MvPolynomial.{uS, uR} (↥s) R) (β := S) (⇑f : (a : MvPolynomial (↥s) R) → S)
⊢ ∃ (ι : Type uS) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] S),
    Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)

Tactic:
use { x : S // x ∈ s }, inferInstance, f
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type uS
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hsur : Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)
this : Fintype ι := hfintype
⊢ FiniteType R S

Tactic:
.of_surjective f hsur

Premises used: Algebra.FiniteType.of_surjective
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type uS
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hsur : Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)
this : Fintype ι := hfintype
⊢ FiniteType R S

Tactic:
exact .of_surjective f hsur
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
mp :
  FiniteType R S →
    ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S),
      Surjective.{uR + 1, uS + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
mpr :
  (∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S),
      Surjective.{uR + 1, uS + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)) →
    FiniteType R S
⊢ FiniteType R S ↔
    ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S),
      Surjective.{uR + 1, uS + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)

Tactic:
constructor
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
mp :
  (∃ (ι : Type uS) (x : Fintype ι) (f : MvPolynomial ι R →ₐ[R] S),
      Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)) →
    ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S),
      Surjective.{uR + 1, uS + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
⊢ FiniteType R S →
    ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S),
      Surjective.{uR + 1, uS + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)

Tactic:
rw [iff_quotient_mvPolynomial']

Premises used: Algebra.FiniteType.iff_quotient_mvPolynomial'
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type uS
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hsur : Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)
mp :
  ∀ (equiv : MvPolynomial ι R ≃ₐ[R] MvPolynomial (Fin (Fintype.card ι)) R),
    ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S),
      Surjective.{uR + 1, uS + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
⊢ ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S),
    Surjective.{uR + 1, uS + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)

Tactic:
have equiv := MvPolynomial.renameEquiv R (Fintype.equivFin ι)
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type uS
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hsur : Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)
equiv : MvPolynomial ι R ≃ₐ[R] MvPolynomial (Fin (Fintype.card ι)) R
⊢ Surjective.{uR + 1, uS + 1} (α := MvPolynomial (Fin (Fintype.card ι)) R) (β := S)
    (⇑(f.comp (↑equiv.symm : MvPolynomial (Fin (Fintype.card ι)) R →ₐ[R] MvPolynomial ι R)) :
      (a : MvPolynomial (Fin (Fintype.card ι)) R) → S)

Tactic:
simpa using hsur
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type uS
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hsur : Surjective (α := MvPolynomial ι R) (β := S) (⇑f : (a : MvPolynomial ι R) → S)
equiv : MvPolynomial ι R ≃ₐ[R] MvPolynomial (Fin (Fintype.card ι)) R
⊢ ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S),
    Surjective.{uR + 1, uS + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)

Tactic:
exact ⟨Fintype.card ι, AlgHom.comp f equiv.symm.toAlgHom, by simpa using hsur⟩
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hsur : Surjective.{uR + 1, uS + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
⊢ FiniteType R S

Tactic:
.of_surjective f hsur

Premises used: Algebra.FiniteType.of_surjective
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type uR
S : Type uS
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hsur : Surjective.{uR + 1, uS + 1} (α := MvPolynomial (Fin n) R) (β := S) (⇑f : (a : MvPolynomial (Fin n) R) → S)
⊢ FiniteType R S

Tactic:
exact .of_surjective f hsur
-- 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
hA : FiniteType R A
hB : FiniteType R B
rw : Subalgebra.FG (R := R) (A := A × B) (Subalgebra.prod ⊤ ⊤)
⊢ Subalgebra.FG (R := R) (A := A × B) ⊤

Tactic:
rw [← Subalgebra.prod_top]

Premises used: Subalgebra.prod_top
-- 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
hA : FiniteType R A
hB : FiniteType R B
⊢ Subalgebra.FG (R := R) (A := A × B) (Subalgebra.prod ⊤ ⊤)

Tactic:
hA.1.prod hB.1

Premises used: Subalgebra.FG.prod, Algebra.FiniteType.out
-- 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
hA : FiniteType R A
hB : FiniteType R B
⊢ Subalgebra.FG (R := R) (A := A × B) (Subalgebra.prod ⊤ ⊤)

Tactic:
exact hA.1.prod hB.1

Premises used: Subalgebra.FG.prod, Algebra.FiniteType.out
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : FiniteType R S
inst_3 : IsNoetherianRing R
obtain : ∀ (s : Finset S) (hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤), IsNoetherianRing S
⊢ IsNoetherianRing S

Tactic:
obtain ⟨s, hs⟩ := h.1

Premises used: Algebra.FiniteType.out
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : FiniteType R S
inst_3 : IsNoetherianRing R
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
hf :
  Surjective (α := MvPolynomial.{u_2, u_1} (↥s) R) (β := S)
    (⇑(AlgHom.toRingHom (MvPolynomial.aeval (Subtype.val (p := fun (x : S) ↦ x ∈ s)))) : (a : MvPolynomial (↥s) R) → S)
⊢ IsNoetherianRing S

Tactic:
apply
    isNoetherianRing_of_surjective (MvPolynomial s R) S
      (MvPolynomial.aeval (↑) : MvPolynomial s R →ₐ[R] S).toRingHom

Premises used: MvPolynomial.aeval, isNoetherianRing_of_surjective, Membership.mem, Subtype, AlgHom.toRingHom, MvPolynomial, Subtype.val
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : FiniteType R S
inst_3 : IsNoetherianRing R
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
hf : (↑⊤ : Set S) = Set.univ
⊢ Surjective (α := MvPolynomial.{u_2, u_1} (↥s) R) (β := S)
    (⇑(AlgHom.toRingHom (MvPolynomial.aeval (Subtype.val (p := fun (x : S) ↦ x ∈ s)))) : (a : MvPolynomial (↥s) R) → S)

Tactic:
rw [← Set.range_eq_univ, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, ← AlgHom.coe_range,
    ← Algebra.adjoin_range_eq_range_aeval, Subtype.range_coe_subtype, Finset.setOf_mem, hs]

Premises used: Set.range_eq_univ, AlgHom.coe_range, RingHom.coe_coe, Finset.setOf_mem, Subtype.range_coe_subtype, Algebra.adjoin_range_eq_range_aeval, AlgHom.toRingHom_eq_coe
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : FiniteType R S
inst_3 : IsNoetherianRing R
s : Finset S
hs : Eq (α := Subalgebra R S) (adjoin R (↑s : Set S)) ⊤
⊢ (↑⊤ : Set S) = Set.univ

Tactic:
rfl
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type uR
A : Type uA
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
S : Subalgebra R A
⊢ S.FG ↔ FiniteType.{uR, uA} R ↥S

Tactic:
S.fg_top.symm.trans ⟨fun h => ⟨h⟩, fun h => h.out⟩

Premises used: Subalgebra.fg_top, Iff.intro, Algebra.FiniteType.mk, Iff.trans, Algebra.FiniteType.out, Iff.symm
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type uR
inst : CommSemiring R
A : Type u_1
inst_1 : CommSemiring A
inst_2 : Algebra R A
t : Set A
h : t.Finite
rw : Subalgebra.FG (adjoin R t)
⊢ FiniteType.{uR, u_1} R ↥(adjoin R t)

Tactic:
rw [← Subalgebra.fg_iff_finiteType]

Premises used: Subalgebra.fg_iff_finiteType
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type uR
inst : CommSemiring R
A : Type u_1
inst_1 : CommSemiring A
inst_2 : Algebra R A
t : Set A
h : t.Finite
⊢ Eq (α := Subalgebra R A) (adjoin R (↑(h.toFinset (s := t)) : Set A)) (adjoin R t)

Tactic:
simp
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type uR
inst : CommSemiring R
A : Type u_1
inst_1 : CommSemiring A
inst_2 : Algebra R A
t : Set A
h : t.Finite
⊢ Subalgebra.FG (adjoin R t)

Tactic:
exact ⟨h.toFinset, by simp⟩
-- Module: Mathlib.RingTheory.FiniteType
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
rw : Algebra.FiniteType A B ↔ Algebra.FiniteType A B
rw₁ rw₂ : Algebra.FiniteType A B ↔ Algebra.FiniteType A B
⊢ FiniteType (algebraMap A B) ↔ Algebra.FiniteType A B

Tactic:
rw [FiniteType, toAlgebra_algebraMap]

Premises used: RingHom.FiniteType, toAlgebra_algebraMap
-- Module: Mathlib.RingTheory.FiniteType
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : f.Finite
⊢ f.FiniteType

Tactic:
@Module.Finite.finiteType _ _ _ _ f.toAlgebra hf

Premises used: Module.Finite.finiteType, RingHom.FiniteType
-- Module: Mathlib.RingTheory.FiniteType
Goal:
A : Type u_1
inst : CommRing A
⊢ Algebra.FiniteType A A

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.FiniteType
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
f : A →+* B
g : B →+* C
hf : f.FiniteType
hg : Surjective.{u_2 + 1, u_3 + 1} (α := B) (β := C) (⇑g : (a : B) → C)
algInst : Algebra A B := f.toAlgebra
algInst_1 : Algebra A C := (g.comp f).toAlgebra
⊢ (g.comp f).FiniteType

Tactic:
‹Algebra.FiniteType _ _›.of_surjective
    { g with
      toFun := g
      commutes' := fun a => rfl }
    hg

Premises used: Algebra.FiniteType.of_surjective, RingHom.map_add', RingHom.mk, OneHom.mk, RingHom.FiniteType, MonoidHom.mk, OneHom.map_one', AlgHom.mk, MonoidHom.toOneHom, RingHom.map_zero', MonoidHom.map_mul', RingHom.toMonoidHom, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.FiniteType
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
f : A →+* B
g : B →+* C
hf : f.FiniteType
hg : Surjective.{u_2 + 1, u_3 + 1} (α := B) (β := C) (⇑g : (a : B) → C)
algInst : Algebra A B := f.toAlgebra
algInst_1 : Algebra A C := (g.comp f).toAlgebra
⊢ (g.comp f).FiniteType

Tactic:
exact ‹Algebra.FiniteType _ _›.of_surjective
    { g with
      toFun := g
      commutes' := fun a => rfl }
    hg

Premises used: Algebra.FiniteType.of_surjective, RingHom.map_add', RingHom.mk, OneHom.mk, MonoidHom.mk, OneHom.map_one', AlgHom.mk, MonoidHom.toOneHom, RingHom.map_zero', MonoidHom.map_mul', RingHom.toMonoidHom, DFunLike.coe
-- Module: Mathlib.RingTheory.FiniteType
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
rw : (f.comp (RingHom.id A)).FiniteType
⊢ f.FiniteType

Tactic:
rw [← f.comp_id]

Premises used: RingHom.comp_id
-- Module: Mathlib.RingTheory.FiniteType
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ (f.comp (RingHom.id A)).FiniteType

Tactic:
(id A).comp_surjective hf

Premises used: RingHom.FiniteType.comp_surjective, RingHom.FiniteType.id
-- Module: Mathlib.RingTheory.FiniteType
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ (f.comp (RingHom.id A)).FiniteType

Tactic:
exact (id A).comp_surjective hf

Premises used: RingHom.FiniteType.comp_surjective, RingHom.FiniteType.id
-- Module: Mathlib.RingTheory.FiniteType
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
g : B →+* C
f : A →+* B
hg : g.FiniteType
hf : f.FiniteType
algInst : Algebra A B := f.toAlgebra
algInst_1 : Algebra B C := g.toAlgebra
algInst_2 : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower A B C := ⋯
⊢ (g.comp f).FiniteType

Tactic:
Algebra.FiniteType.trans hf hg

Premises used: RingHom.FiniteType, Algebra.FiniteType.trans
-- Module: Mathlib.RingTheory.FiniteType
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
g : B →+* C
f : A →+* B
hg : g.FiniteType
hf : f.FiniteType
algInst : Algebra A B := f.toAlgebra
algInst_1 : Algebra B C := g.toAlgebra
algInst_2 : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower A B C := ⋯
⊢ (g.comp f).FiniteType

Tactic:
exact Algebra.FiniteType.trans hf hg

Premises used: Algebra.FiniteType.trans
-- Module: Mathlib.RingTheory.FiniteType
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
f : A →+* B
g : B →+* C
h : (g.comp f).FiniteType
⊢ Algebra.FiniteType A C

Tactic:
algebraize [f, g, g.comp f]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.FiniteType
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
f : A →+* B
g : B →+* C
h : (g.comp f).FiniteType
algInst : Algebra A B := f.toAlgebra
algInst_1 : Algebra B C := g.toAlgebra
algInst_2 : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower A B C := ⋯
algebraizeInst : Algebra.FiniteType A C
⊢ g.FiniteType

Tactic:
Algebra.FiniteType.of_restrictScalars_finiteType A B C

Premises used: Algebra.FiniteType.of_restrictScalars_finiteType, RingHom.FiniteType
-- Module: Mathlib.RingTheory.FiniteType
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
f : A →+* B
g : B →+* C
h : (g.comp f).FiniteType
algInst : Algebra A B := f.toAlgebra
algInst_1 : Algebra B C := g.toAlgebra
algInst_2 : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower A B C := ⋯
algebraizeInst : Algebra.FiniteType A C
⊢ g.FiniteType

Tactic:
exact Algebra.FiniteType.of_restrictScalars_finiteType A B C

Premises used: Algebra.FiniteType.of_restrictScalars_finiteType
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
hf : f.Finite
⊢ f.FiniteType

Tactic:
RingHom.Finite.finiteType hf

Premises used: AlgHom.FiniteType, RingHom.Finite.finiteType
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
⊢ FiniteType (AlgHom.id R A)

Tactic:
RingHom.FiniteType.id A

Premises used: AlgHom.FiniteType, RingHom.FiniteType.id
-- Module: Mathlib.RingTheory.FiniteType
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : CommRing C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
g : B →ₐ[R] C
f : A →ₐ[R] B
hg : g.FiniteType
hf : f.FiniteType
⊢ (g.comp f).FiniteType

Tactic:
RingHom.FiniteType.comp hg hf

Premises used: AlgHom.FiniteType, RingHom.FiniteType.comp