case h.e'_6
R : Type u_1
A : Type u
B : Type u_2
M : Type ?u.22919
N : Type ?u.22922
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
hRA : FiniteType R A
f : A →ₐ[R] B
hf : Surjective ↑f
⊢ ⊤ = Subalgebra.map f ⊤
R : Type u_1
A : Type u
B : Type u_2
M : Type ?u.22919
N : Type ?u.22922
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
hRA : FiniteType R A
f : A →ₐ[R] B
hf : Surjective ↑f
⊢ Subalgebra.FG ⊤
convert hRA.1.map f
no goals
case h.e'_6
R : Type u_1
A : Type u
B : Type u_2
M : Type ?u.22919
N : Type ?u.22922
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
hRA : FiniteType R A
f : A →ₐ[R] B
hf : Surjective ↑f
⊢ ⊤ = Subalgebra.map f ⊤
simpa only [map_top f, @eq_comm _ ⊤, eq_top_iff, AlgHom.mem_range] using hf