-- Lean 4 proof step from Mathlib.FieldTheory.LinearDisjoint (goal)
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
⊢ (↑(((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)
have a₁ : (↑(((RingEquiv.subsemiringCongr heq).toAddEquiv :
          (a : ↥(extendScalars sorry)) → ↥(Algebra.adjoin ↥A.toSubalgebra (↑L' : Set E)))
        (HMul.hMul (α := ↥(extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) sorry))
          ((algebraMap ↥A ↥(extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) sorry) :
                (a : ↥A) → ↥(extendScalars sorry))
              (Subtype.mk (p := fun (x : E) ↦ x ∈ A) a ha) :
            ↥(extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) sorry))
          (Subtype.mk (p := fun (x : E) ↦
            Membership.mem (γ := IntermediateField (↥A) E)
              (extendScalars (E := restrictScalars F (adjoin L (↑A : Set E))) sorry) 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 sorry)) → ↥(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))) sorry) x)
              x hx) :
          ↥(Algebra.adjoin ↥A.toSubalgebra (↑L' : Set E)))) :
    E)
Tactic: simp_rw [Algebra.smul_def]