A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
hf : FiniteType f
hg : Surjective ↑g
x✝ : Algebra A B := toAlgebra f
⊢ FiniteType (comp g f)
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
hf : FiniteType f
hg : Surjective ↑g
⊢ FiniteType (comp g f)
let _ : Algebra A B := f.toAlgebra
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
hf : FiniteType f
hg : Surjective ↑g
x✝¹ : Algebra A B := toAlgebra f
x✝ : Algebra A C := toAlgebra (comp g f)
⊢ FiniteType (comp g f)
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
hf : FiniteType f
hg : Surjective ↑g
x✝ : Algebra A B := toAlgebra f
⊢ FiniteType (comp g f)
let _ : Algebra A C := (g.comp f).toAlgebra
no goals
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
hf : FiniteType f
hg : Surjective ↑g
x✝¹ : Algebra A B := toAlgebra f
x✝ : Algebra A C := toAlgebra (comp g f)
⊢ FiniteType (comp g f)
exact Algebra.FiniteType.of_surjective hf
  { g with
    toFun := g
    commutes' := fun a => rfl }
  hg