case mp
R : Type u_1
A : Type u
B : Type ?u.42057
M : Type ?u.42060
N : Type ?u.42063
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 → ∃ s f, Surjective ↑f

case mpr
R : Type u_1
A : Type u
B : Type ?u.42057
M : Type ?u.42060
N : Type ?u.42063
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) → FiniteType R A
R : Type u_1
A : Type u
B : Type ?u.42057
M : Type ?u.42060
N : Type ?u.42063
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 ↔ ∃ s f, Surjective ↑f
constructor
case mp.mk.intro
R : Type u_1
A : Type u
B : Type ?u.42057
M : Type ?u.42060
N : Type ?u.42063
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
hs : adjoin R ↑s = ⊤
⊢ ∃ s f, Surjective ↑f
case mp
R : Type u_1
A : Type u
B : Type ?u.42057
M : Type ?u.42060
N : Type ?u.42063
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 → ∃ s f, Surjective ↑f
rintro ⟨s, hs⟩
case mp.mk.intro
R : Type u_1
A : Type u
B : Type ?u.42057
M : Type ?u.42060
N : Type ?u.42063
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
hs : adjoin R ↑s = ⊤
⊢ Surjective ↑(MvPolynomial.aeval Subtype.val)
case mp.mk.intro
R : Type u_1
A : Type u
B : Type ?u.42057
M : Type ?u.42060
N : Type ?u.42063
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
hs : adjoin R ↑s = ⊤
⊢ ∃ s f, Surjective ↑f
use s, MvPolynomial.aeval (↑)
case mp.mk.intro
R : Type u_1
A : Type u
B : Type ?u.42057
M : Type ?u.42060
N : Type ?u.42063
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
hs : adjoin R ↑s = ⊤
x : A
⊢ ∃ a, ↑(MvPolynomial.aeval Subtype.val) a = x
case mp.mk.intro
R : Type u_1
A : Type u
B : Type ?u.42057
M : Type ?u.42060
N : Type ?u.42063
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
hs : adjoin R ↑s = ⊤
⊢ Surjective ↑(MvPolynomial.aeval Subtype.val)
intro x
case mp.mk.intro
R : Type u_1
A : Type u
B : Type ?u.42057
M : Type ?u.42060
N : Type ?u.42063
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
hs : adjoin R ↑s = ⊤
x : A
hrw : ↑s = fun x => x ∈ s.val
⊢ ∃ a, ↑(MvPolynomial.aeval Subtype.val) a = x
case mp.mk.intro
R : Type u_1
A : Type u
B : Type ?u.42057
M : Type ?u.42060
N : Type ?u.42063
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
hs : adjoin R ↑s = ⊤
x : A
⊢ ∃ a, ↑(MvPolynomial.aeval Subtype.val) a = x
have hrw : (↑s : Set A) = fun x : A => x ∈ s.val := rfl
case mp.mk.intro
R : Type u_1
A : Type u
B : Type ?u.42057
M : Type ?u.42060
N : Type ?u.42063
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
hs : adjoin R ↑s = ⊤
x : A
hrw : ↑s = fun x => x ∈ s.val
⊢ x ∈ ↑⊤
case mp.mk.intro
R : Type u_1
A : Type u
B : Type ?u.42057
M : Type ?u.42060
N : Type ?u.42063
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
hs : adjoin R ↑s = ⊤
x : A
hrw : ↑s = fun x => x ∈ s.val
⊢ ∃ a, ↑(MvPolynomial.aeval Subtype.val) a = x
rw [← Set.mem_range, ← AlgHom.coe_range, ← adjoin_eq_range, ← hrw, hs]
no goals
case mp.mk.intro
R : Type u_1
A : Type u
B : Type ?u.42057
M : Type ?u.42060
N : Type ?u.42063
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
hs : adjoin R ↑s = ⊤
x : A
hrw : ↑s = fun x => x ∈ s.val
⊢ x ∈ ↑⊤
exact Set.mem_univ x
case mpr.intro.intro
R : Type u_1
A : Type u
B : Type ?u.42057
M : Type ?u.42060
N : Type ?u.42063
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
⊢ FiniteType R A
case mpr
R : Type u_1
A : Type u
B : Type ?u.42057
M : Type ?u.42060
N : Type ?u.42063
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) → FiniteType R A
rintro ⟨s, ⟨f, hsur⟩⟩
no goals
case mpr.intro.intro
R : Type u_1
A : Type u
B : Type ?u.42057
M : Type ?u.42060
N : Type ?u.42063
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
⊢ FiniteType R A
exact FiniteType.of_surjective (FiniteType.mvPolynomial R { x // x ∈ s }) f hsur