no goals
R : Type u
S✝ : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝¹⁰ : CommSemiring C
inst✝⁹ : CommSemiring D
inst✝⁸ : CommSemiring E
inst✝⁷ : CommSemiring F
inst✝⁶ : Algebra C D
inst✝⁵ : Algebra C E
inst✝⁴ : Algebra C F
inst✝³ : Algebra D F
inst✝² : Algebra E F
inst✝¹ : IsScalarTower C D F
inst✝ : IsScalarTower C E F
S : Set D
T : Set E
hS : adjoin C S = ⊤
hT : adjoin C T = ⊤
⊢ Subalgebra.restrictScalars C (adjoin E (↑(algebraMap D F) '' S)) =
    Subalgebra.restrictScalars C (adjoin D (↑(algebraMap E F) '' T))
rw [adjoin_restrictScalars C E, adjoin_restrictScalars C D, ← hS, ← hT, ← Algebra.adjoin_image,
  ← Algebra.adjoin_image, ← AlgHom.coe_toRingHom, ← AlgHom.coe_toRingHom,
  IsScalarTower.coe_toAlgHom, IsScalarTower.coe_toAlgHom, ← adjoin_union_eq_adjoin_adjoin, ←
  adjoin_union_eq_adjoin_adjoin, Set.union_comm]