-- Mathlib/RingTheory/FiniteType.lean
theorem iff_quotient_mvPolynomial'' :
    FiniteType R S ↔ ∃ (n : ℕ) (f : MvPolynomial (Fin n) R →ₐ[R] S), Surjective f

Proof state:
case mp.intro.intro.intro
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
ι : Type uS
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hsur : Surjective ⇑f
equiv : MvPolynomial ι R ≃ₐ[R] MvPolynomial (Fin (Fintype.card ι)) R
⊢ ∃ n f, Surjective ⇑f

Tactic:
exact ⟨Fintype.card ι, AlgHom.comp f equiv.symm.toAlgHom, by simpa using hsur⟩

Result:
no goals

Proof state:
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ FiniteType R S ↔ ∃ n 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 → ∃ n f, Surjective ⇑f

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

Proof state:
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
ι : Type uS
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hsur : Surjective ⇑f
equiv : MvPolynomial ι R ≃ₐ[R] MvPolynomial (Fin (Fintype.card ι)) R
⊢ Surjective ⇑(f.comp ↑equiv.symm)

Tactic:
simpa using hsur

Result:
no goals

Proof state:
case mp.intro.intro.intro
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
ι : Type uS
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hsur : Surjective ⇑f
⊢ ∃ n f, Surjective ⇑f

Tactic:
have equiv := MvPolynomial.renameEquiv R (Fintype.equivFin ι)

Result:
case mp.intro.intro.intro
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
ι : Type uS
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hsur : Surjective ⇑f
equiv : MvPolynomial ι R ≃ₐ[R] MvPolynomial (Fin (Fintype.card ι)) R
⊢ ∃ n f, Surjective ⇑f

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

Tactic:
rw [iff_quotient_mvPolynomial']

Result:
case mp
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ (∃ ι x f, Surjective ⇑f) → ∃ n 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
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hsur : Surjective ⇑f
⊢ FiniteType R S

Tactic:
exact FiniteType.of_surjective (FiniteType.mvPolynomial R (Fin n)) f hsur

Result:
no goals

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

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

Result:
case mpr.intro.intro
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
n : ℕ
f : MvPolynomial (Fin n) 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
⊢ (∃ ι x f, Surjective ⇑f) → ∃ n f, Surjective ⇑f

Tactic:
rintro ⟨ι, hfintype, ⟨f, hsur⟩⟩

Result:
case mp.intro.intro.intro
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
ι : Type uS
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] S
hsur : Surjective ⇑f
⊢ ∃ n f, Surjective ⇑f