-- Module: Mathlib.FieldTheory.LinearDisjoint
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
inst_5 : Algebra L E
inst_6 : IsScalarTower F L E
H : A.LinearDisjoint L
halg : Algebra.IsAlgebraic.{u, v} F ↥A ∨ Algebra.IsAlgebraic F L
L' : Subalgebra F E := AlgHom.range (IsScalarTower.toAlgHom F L E)
heq :
  Eq (α := Subsemiring E) (Subalgebra.toSubsemiring (toSubalgebra (adjoin L (↑A : Set E))))
    (Subalgebra.toSubsemiring (R := ↥A) (Algebra.adjoin ↥A (↑L' : Set E)))
x_1 : ↥A
x_2 : ↥(extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) ⋯)
a : E
ha : a ∈ A
x : E
hx : Membership.mem (γ := IntermediateField (↥A) E) (extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) ⋯) x
a₁ :
  (↑(((RingEquiv.subsemiringCongr heq).toAddEquiv :
            (a : ↥(extendScalars ⋯)) → ↥(Algebra.adjoin ↥A.toSubalgebra (↑L' : Set E)))
          (HMul.hMul (α := ↥(extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) ⋯))
            ((algebraMap ↥A ↥(extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) ⋯) :
                  (a : ↥A) → ↥(extendScalars ⋯))
                (Subtype.mk (p := fun (x : E) ↦ x ∈ A) a ha) :
              ↥(extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) ⋯))
            (Subtype.mk (p := fun (x : E) ↦
              Membership.mem (γ := IntermediateField (↥A) E)
                (extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) ⋯) x)
              x hx))) :
      E) =
    (↑(HMul.hMul (α := ↥(Algebra.adjoin ↥A.toSubalgebra (↑L' : Set E))) (β :=
          ↥(Algebra.adjoin ↥A.toSubalgebra (↑L' : Set E)))
          ((algebraMap ↥A.toSubalgebra ↥(Algebra.adjoin ↥A.toSubalgebra (↑L' : Set E)) :
                (a : ↥A.toSubalgebra) → ↥(Algebra.adjoin ↥A.toSubalgebra (↑L' : Set E)))
              ((RingHom.id ↥A : (a : ↥A) → ↥A) (Subtype.mk (p := fun (x : E) ↦ x ∈ A) a ha)) :
            ↥(Algebra.adjoin ↥A.toSubalgebra (↑L' : Set E)))
          (((RingEquiv.subsemiringCongr heq).toAddEquiv :
                (a : ↥(extendScalars ⋯)) → ↥(Algebra.adjoin ↥A.toSubalgebra (↑L' : Set E)))
              (Subtype.mk (p := fun (x : E) ↦
                Membership.mem (γ := IntermediateField (↥A) E)
                  (extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) ⋯) x)
                x hx) :
            ↥(Algebra.adjoin ↥A.toSubalgebra (↑L' : Set E)))) :
      E)
⊢ (↑(((RingEquiv.subsemiringCongr heq).toAddEquiv :
            (a : ↥(extendScalars ⋯)) → ↥(Algebra.adjoin ↥A.toSubalgebra (↑L' : Set E)))
          (Subtype.mk (p := fun (x : E) ↦ x ∈ A) a ha •
            Subtype.mk (p := fun (x : E) ↦
              Membership.mem (γ := IntermediateField (↥A) E)
                (extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) ⋯) x)
              x hx)) :
      E) =
    (↑(HSMul.hSMul (α := ↥A.toSubalgebra) (β := ↥(Algebra.adjoin ↥A.toSubalgebra (↑L' : Set E)))
          ((RingHom.id ↥A : (a : ↥A) → ↥A) (Subtype.mk (p := fun (x : E) ↦ x ∈ A) a ha) : ↥A)
          (((RingEquiv.subsemiringCongr heq).toAddEquiv :
                (a : ↥(extendScalars ⋯)) → ↥(Algebra.adjoin ↥A.toSubalgebra (↑L' : Set E)))
              (Subtype.mk (p := fun (x : E) ↦
                Membership.mem (γ := IntermediateField (↥A) E)
                  (extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) ⋯) x)
                x hx) :
            ↥(Algebra.adjoin ↥A.toSubalgebra (↑L' : Set E)))) :
      E)

Tactic:
simp_rw [Algebra.smul_def]

Premises used: Algebra.smul_def