∀ (C : Type u_1) (D : Type u_2) (E : Type u_3) [inst : CommSemiring C] [inst_1 : CommSemiring D]
  [inst_2 : CommSemiring E] [inst_3 : Algebra C D] [inst_4 : Algebra C E] [inst_5 : Algebra D E]
  [inst_6 : IsScalarTower C D E] (S : Set E),
  Subalgebra.restrictScalars C (Algebra.adjoin D S) =
    Subalgebra.restrictScalars C (Algebra.adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) S)