∀ (A : Type w) (B : Type u₁) (C : Type u_1) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : CommRing C]
  [inst_3 : Algebra A B] [inst_4 : Algebra B C] [inst_5 : Algebra A C] [IsScalarTower A B C] [IsNoetherianRing A],
  ⊤.FG → ⊤.FG → Function.Injective ⇑(algebraMap B C) → ⊤.FG