-- Mathlib/RingTheory/FiniteType.lean
theorem iff_quotient_mvPolynomial :
    FiniteType R S ↔
      ∃ (s : Finset S) (f : MvPolynomial { x // x ∈ s } R →ₐ[R] S), Surjective f

Proof state:
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ FiniteType R S ↔ ∃ s f, Surjective ⇑f

Tactic:
constructor

Result:
case mp
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ FiniteType R S → ∃ s f, Surjective ⇑f

case mpr
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ (∃ s f, Surjective ⇑f) → FiniteType R S

Proof state:
case h
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
hs : adjoin R ↑s = ⊤
x : S
hrw : ↑s = fun x => x ∈ s.val
⊢ x ∈ ↑(adjoin R (Membership.mem s.val))

Tactic:
simp_rw [← hrw, hs]

Result:
case h
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
hs : adjoin R ↑s = ⊤
x : S
hrw : ↑s = fun x => x ∈ s.val
⊢ x ∈ ↑⊤

Proof state:
case mp.mk.intro
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ ∃ s f, Surjective ⇑f

Tactic:
use s, MvPolynomial.aeval (↑)

Result:
case h
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ Surjective ⇑(MvPolynomial.aeval Subtype.val)

Proof state:
case mpr
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ (∃ s f, Surjective ⇑f) → FiniteType R S

Tactic:
rintro ⟨s, ⟨f, hsur⟩⟩

Result:
case mpr.intro.intro
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
f : MvPolynomial { x // x ∈ s } R →ₐ[R] S
hsur : Surjective ⇑f
⊢ FiniteType R S

Proof state:
case mp
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ FiniteType R S → ∃ s f, Surjective ⇑f

Tactic:
rintro ⟨s, hs⟩

Result:
case mp.mk.intro
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ ∃ s f, Surjective ⇑f

Proof state:
case mpr.intro.intro
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
f : MvPolynomial { x // x ∈ s } R →ₐ[R] S
hsur : Surjective ⇑f
⊢ FiniteType R S

Tactic:
exact FiniteType.of_surjective (FiniteType.mvPolynomial R { x // x ∈ s }) f hsur

Result:
no goals

Proof state:
case h
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ Surjective ⇑(MvPolynomial.aeval Subtype.val)

Tactic:
intro x

Result:
case h
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
hs : adjoin R ↑s = ⊤
x : S
⊢ ∃ a, (MvPolynomial.aeval Subtype.val) a = x

Proof state:
case h
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
hs : adjoin R ↑s = ⊤
x : S
⊢ ∃ a, (MvPolynomial.aeval Subtype.val) a = x

Tactic:
have hrw : (↑s : Set S) = fun x : S => x ∈ s.val := rfl

Result:
case h
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
hs : adjoin R ↑s = ⊤
x : S
hrw : ↑s = fun x => x ∈ s.val
⊢ ∃ a, (MvPolynomial.aeval Subtype.val) a = x

Proof state:
case h
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
hs : adjoin R ↑s = ⊤
x : S
hrw : ↑s = fun x => x ∈ s.val
⊢ x ∈ ↑⊤

Tactic:
exact Set.mem_univ x

Result:
no goals

Proof state:
case h
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
hs : adjoin R ↑s = ⊤
x : S
hrw : ↑s = fun x => x ∈ s.val
⊢ ∃ a, (MvPolynomial.aeval Subtype.val) a = x

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

Result:
case h
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
hs : adjoin R ↑s = ⊤
x : S
hrw : ↑s = fun x => x ∈ s.val
⊢ x ∈ ↑(adjoin R (Membership.mem s.val))