case mp
R : Type u_1
A : Type u
B : Type ?u.48702
M : Type ?u.48705
N : Type ?u.48708
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ FiniteType R A → ∃ ι x f, Surjective ↑f

case mpr
R : Type u_1
A : Type u
B : Type ?u.48702
M : Type ?u.48705
N : Type ?u.48708
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ (∃ ι x f, Surjective ↑f) → FiniteType R A
R : Type u_1
A : Type u
B : Type ?u.48702
M : Type ?u.48705
N : Type ?u.48708
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ FiniteType R A ↔ ∃ ι x f, Surjective ↑f
constructor
case mp
R : Type u_1
A : Type u
B : Type ?u.48702
M : Type ?u.48705
N : Type ?u.48708
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ (∃ s f, Surjective ↑f) → ∃ ι x f, Surjective ↑f
case mp
R : Type u_1
A : Type u
B : Type ?u.48702
M : Type ?u.48705
N : Type ?u.48708
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ FiniteType R A → ∃ ι x f, Surjective ↑f
rw [iff_quotient_mvPolynomial]
case mp.intro.intro
R : Type u_1
A : Type u
B : Type ?u.48702
M : Type ?u.48705
N : Type ?u.48708
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
s : Finset A
f : MvPolynomial { x // x ∈ s } R →ₐ[R] A
hsur : Surjective ↑f
⊢ ∃ ι x f, Surjective ↑f
case mp
R : Type u_1
A : Type u
B : Type ?u.48702
M : Type ?u.48705
N : Type ?u.48708
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ (∃ s f, Surjective ↑f) → ∃ ι x f, Surjective ↑f
rintro ⟨s, ⟨f, hsur⟩⟩
case mp.intro.intro
R : Type u_1
A : Type u
B : Type ?u.48702
M : Type ?u.48705
N : Type ?u.48708
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
s : Finset A
f : MvPolynomial { x // x ∈ s } R →ₐ[R] A
hsur : Surjective ↑f
⊢ Surjective ↑f
case mp.intro.intro
R : Type u_1
A : Type u
B : Type ?u.48702
M : Type ?u.48705
N : Type ?u.48708
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
s : Finset A
f : MvPolynomial { x // x ∈ s } R →ₐ[R] A
hsur : Surjective ↑f
⊢ ∃ ι x f, Surjective ↑f
use { x : A // x ∈ s }, inferInstance, f
no goals
case mp.intro.intro
R : Type u_1
A : Type u
B : Type ?u.48702
M : Type ?u.48705
N : Type ?u.48708
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
s : Finset A
f : MvPolynomial { x // x ∈ s } R →ₐ[R] A
hsur : Surjective ↑f
⊢ Surjective ↑f
exact hsur
case mpr.intro.intro.intro
R : Type u_1
A : Type u
B : Type ?u.48702
M : Type ?u.48705
N : Type ?u.48708
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
ι : Type u
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] A
hsur : Surjective ↑f
⊢ FiniteType R A
case mpr
R : Type u_1
A : Type u
B : Type ?u.48702
M : Type ?u.48705
N : Type ?u.48708
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ (∃ ι x f, Surjective ↑f) → FiniteType R A
rintro ⟨ι, ⟨hfintype, ⟨f, hsur⟩⟩⟩
case mpr.intro.intro.intro
R : Type u_1
A : Type u
B : Type ?u.48702
M : Type ?u.48705
N : Type ?u.48708
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
ι : Type u
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] A
hsur : Surjective ↑f
this : Fintype ι := hfintype
⊢ FiniteType R A
case mpr.intro.intro.intro
R : Type u_1
A : Type u
B : Type ?u.48702
M : Type ?u.48705
N : Type ?u.48708
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
ι : Type u
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] A
hsur : Surjective ↑f
⊢ FiniteType R A
letI : Fintype ι := hfintype
no goals
case mpr.intro.intro.intro
R : Type u_1
A : Type u
B : Type ?u.48702
M : Type ?u.48705
N : Type ?u.48708
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
ι : Type u
hfintype : Fintype ι
f : MvPolynomial ι R →ₐ[R] A
hsur : Surjective ↑f
this : Fintype ι := hfintype
⊢ FiniteType R A
exact FiniteType.of_surjective (FiniteType.mvPolynomial R ι) f hsur