-- Lean 4 proof step from Mathlib.RingTheory.Adjoin.Tower (goal)
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)))
⊢ 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)))
have 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)))
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]