case intro
R✝ : Type ?u.65970
A : Type u
B : Type ?u.65961
M : Type ?u.65964
N : Type ?u.65967
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
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ IsNoetherianRing S
R✝ : Type ?u.65970
A : Type u
B : Type ?u.65961
M : Type ?u.65964
N : Type ?u.65967
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
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
⊢ IsNoetherianRing S
obtain ⟨s, hs⟩ := h.1
case intro.hf
R✝ : Type ?u.65970
A : Type u
B : Type ?u.65961
M : Type ?u.65964
N : Type ?u.65967
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
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ Surjective ↑↑(MvPolynomial.aeval Subtype.val)
case intro
R✝ : Type ?u.65970
A : Type u
B : Type ?u.65961
M : Type ?u.65964
N : Type ?u.65967
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
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ IsNoetherianRing S
apply
  isNoetherianRing_of_surjective (MvPolynomial s R) S
    (MvPolynomial.aeval (↑) : MvPolynomial s R →ₐ[R] S).toRingHom
case intro.hf
R✝ : Type ?u.65970
A : Type u
B : Type ?u.65961
M : Type ?u.65964
N : Type ?u.65967
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
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ ↑⊤ = Set.univ
case intro.hf
R✝ : Type ?u.65970
A : Type u
B : Type ?u.65961
M : Type ?u.65964
N : Type ?u.65967
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
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ Surjective ↑↑(MvPolynomial.aeval Subtype.val)
erw [← Set.range_iff_surjective, ← AlgHom.coe_range, ←
  Algebra.adjoin_range_eq_range_aeval, Subtype.range_coe_subtype, Finset.setOf_mem, hs]
no goals
case intro.hf
R✝ : Type ?u.65970
A : Type u
B : Type ?u.65961
M : Type ?u.65964
N : Type ?u.65967
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
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
h : FiniteType R S
inst✝ : IsNoetherianRing R
s : Finset S
hs : adjoin R ↑s = ⊤
⊢ ↑⊤ = Set.univ
rfl