-- Module: Mathlib.RingTheory.Adjoin.Tower
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst : CommSemiring C
inst_1 : CommSemiring D
inst_2 : CommSemiring E
inst_3 : CommSemiring F
inst_4 : Algebra C D
inst_5 : Algebra C E
inst_6 : Algebra C F
inst_7 : Algebra D F
inst_8 : Algebra E F
inst_9 : IsScalarTower C D F
inst_10 : IsScalarTower C E F
S : Set D
T : Set E
hS : Eq (α := Subalgebra C D) (adjoin C S) ⊤
hT : Eq (α := Subalgebra C E) (adjoin C T) ⊤
rw :
  Eq.{u_4 + 1} (α := Subalgebra C F)
    (Subalgebra.restrictScalars C (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) ⊤))
      (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) ⊤)) ((⇑(algebraMap D F) : (a : D) → F) '' S)))
    (Subalgebra.restrictScalars C (adjoin D ((⇑(algebraMap E F) : (a : E) → F) '' T)))
rw₁ :
  Eq.{u_4 + 1} (α := Subalgebra C F)
    (Subalgebra.restrictScalars C (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) ⊤))
      (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) ⊤)) ((⇑(algebraMap D F) : (a : D) → F) '' S)))
    (Subalgebra.restrictScalars C (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom C D F) ⊤))
      (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C D F) ⊤)) ((⇑(algebraMap E F) : (a : E) → F) '' T)))
rw₂ :
  Eq.{u_4 + 1} (α := Subalgebra C F)
    (Subalgebra.restrictScalars C (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) ⊤))
      (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) ⊤)) ((⇑(algebraMap D F) : (a : D) → F) '' S)))
    (Subalgebra.restrictScalars C (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom C D F) (adjoin C S)))
      (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C D F) (adjoin C S))) ((⇑(algebraMap E F) : (a : E) → F) '' T)))
rw₃ :
  Eq.{u_4 + 1} (α := Subalgebra C F)
    (Subalgebra.restrictScalars C (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) (adjoin C T)))
      (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C E F) (adjoin C T))) ((⇑(algebraMap D F) : (a : D) → F) '' S)))
    (Subalgebra.restrictScalars C (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom C D F) (adjoin C S)))
      (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C D F) (adjoin C S))) ((⇑(algebraMap E F) : (a : E) → F) '' T)))
rw₄ :
  Eq.{u_4 + 1} (α := Subalgebra C F)
    (Subalgebra.restrictScalars C (S := ↥(adjoin C ((⇑(IsScalarTower.toAlgHom C E F) : (a : E) → F) '' T)))
      (adjoin (↥(adjoin C ((⇑(IsScalarTower.toAlgHom C E F) : (a : E) → F) '' T)))
        ((⇑(algebraMap D F) : (a : D) → F) '' S)))
    (Subalgebra.restrictScalars C (S := ↥(Subalgebra.map (IsScalarTower.toAlgHom C D F) (adjoin C S)))
      (adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C D F) (adjoin C S))) ((⇑(algebraMap E F) : (a : E) → F) '' T)))
rw₅ :
  Eq.{u_4 + 1} (α := Subalgebra C F)
    (Subalgebra.restrictScalars C (S := ↥(adjoin C ((⇑(IsScalarTower.toAlgHom C E F) : (a : E) → F) '' T)))
      (adjoin (↥(adjoin C ((⇑(IsScalarTower.toAlgHom C E F) : (a : E) → F) '' T)))
        ((⇑(algebraMap D F) : (a : D) → F) '' S)))
    (Subalgebra.restrictScalars C (S := ↥(adjoin C ((⇑(IsScalarTower.toAlgHom C D F) : (a : D) → F) '' S)))
      (adjoin (↥(adjoin C ((⇑(IsScalarTower.toAlgHom C D F) : (a : D) → F) '' S)))
        ((⇑(algebraMap E F) : (a : E) → F) '' T)))
rw₆ :
  Eq.{u_4 + 1} (α := Subalgebra C F)
    (Subalgebra.restrictScalars C (S := ↥(adjoin C ((⇑(↑(IsScalarTower.toAlgHom C E F) : E →+* F) : (a : E) → F) '' T)))
      (adjoin (↥(adjoin C ((⇑(↑(IsScalarTower.toAlgHom C E F) : E →+* F) : (a : E) → F) '' T)))
        ((⇑(algebraMap D F) : (a : D) → F) '' S)))
    (Subalgebra.restrictScalars C (S := ↥(adjoin C ((⇑(IsScalarTower.toAlgHom C D F) : (a : D) → F) '' S)))
      (adjoin (↥(adjoin C ((⇑(IsScalarTower.toAlgHom C D F) : (a : D) → F) '' S)))
        ((⇑(algebraMap E F) : (a : E) → F) '' T)))
rw₇ :
  Eq.{u_4 + 1} (α := Subalgebra C F)
    (Subalgebra.restrictScalars C (S := ↥(adjoin C ((⇑(↑(IsScalarTower.toAlgHom C E F) : E →+* F) : (a : E) → F) '' T)))
      (adjoin (↥(adjoin C ((⇑(↑(IsScalarTower.toAlgHom C E F) : E →+* F) : (a : E) → F) '' T)))
        ((⇑(algebraMap D F) : (a : D) → F) '' S)))
    (Subalgebra.restrictScalars C (S := ↥(adjoin C ((⇑(↑(IsScalarTower.toAlgHom C D F) : D →+* F) : (a : D) → F) '' S)))
      (adjoin (↥(adjoin C ((⇑(↑(IsScalarTower.toAlgHom C D F) : D →+* F) : (a : D) → F) '' S)))
        ((⇑(algebraMap E F) : (a : E) → F) '' T)))
rw₈ :
  Eq.{u_4 + 1} (α := Subalgebra C F)
    (Subalgebra.restrictScalars C (S := ↥(adjoin C ((⇑(algebraMap E F) : (a : E) → F) '' T)))
      (adjoin (↥(adjoin C ((⇑(algebraMap E F) : (a : E) → F) '' T))) ((⇑(algebraMap D F) : (a : D) → F) '' S)))
    (Subalgebra.restrictScalars C (S := ↥(adjoin C ((⇑(↑(IsScalarTower.toAlgHom C D F) : D →+* F) : (a : D) → F) '' S)))
      (adjoin (↥(adjoin C ((⇑(↑(IsScalarTower.toAlgHom C D F) : D →+* F) : (a : D) → F) '' S)))
        ((⇑(algebraMap E F) : (a : E) → F) '' T)))
rw₉ :
  Eq.{u_4 + 1} (α := Subalgebra C F)
    (Subalgebra.restrictScalars C (S := ↥(adjoin C ((⇑(algebraMap E F) : (a : E) → F) '' T)))
      (adjoin (↥(adjoin C ((⇑(algebraMap E F) : (a : E) → F) '' T))) ((⇑(algebraMap D F) : (a : D) → F) '' S)))
    (Subalgebra.restrictScalars C (S := ↥(adjoin C ((⇑(algebraMap D F) : (a : D) → F) '' S)))
      (adjoin (↥(adjoin C ((⇑(algebraMap D F) : (a : D) → F) '' S))) ((⇑(algebraMap E F) : (a : E) → F) '' T)))
rw₁₀ :
  Eq.{u_4 + 1} (α := Subalgebra C F)
    (adjoin C ((⇑(algebraMap E F) : (a : E) → F) '' T ∪ (⇑(algebraMap D F) : (a : D) → F) '' S))
    (Subalgebra.restrictScalars C (S := ↥(adjoin C ((⇑(algebraMap D F) : (a : D) → F) '' S)))
      (adjoin (↥(adjoin C ((⇑(algebraMap D F) : (a : D) → F) '' S))) ((⇑(algebraMap E F) : (a : E) → F) '' T)))
rw₁₁ :
  Eq.{u_4 + 1} (α := Subalgebra C F)
    (adjoin C ((⇑(algebraMap E F) : (a : E) → F) '' T ∪ (⇑(algebraMap D F) : (a : D) → F) '' S))
    (adjoin C ((⇑(algebraMap D F) : (a : D) → F) '' S ∪ (⇑(algebraMap E F) : (a : E) → F) '' T))
rw₁₂ rw₁₃ :
  Eq.{u_4 + 1} (α := Subalgebra C F)
    (adjoin C ((⇑(algebraMap D F) : (a : D) → F) '' S ∪ (⇑(algebraMap E F) : (a : E) → F) '' T))
    (adjoin C ((⇑(algebraMap D F) : (a : D) → F) '' S ∪ (⇑(algebraMap E F) : (a : E) → F) '' T))
⊢ Eq.{u_4 + 1} (α := Subalgebra C F) (Subalgebra.restrictScalars C (adjoin E ((⇑(algebraMap D F) : (a : D) → F) '' S)))
    (Subalgebra.restrictScalars C (adjoin D ((⇑(algebraMap E F) : (a : E) → F) '' T)))

Tactic:
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]

Premises used: AlgHom.coe_toRingHom, IsScalarTower.coe_toAlgHom, Set.union_comm, Algebra.adjoin_image, Algebra.adjoin_restrictScalars, Algebra.adjoin_union_eq_adjoin_adjoin