-- Lean 4 proof step from Mathlib.RingTheory.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
inst_3 : Free.{u, v} R ↥B
inst_4 : Module.Finite.{u, v} R ↥B
x : ↥B
simp_rw :
  Eq (α := ↥A) ((Algebra.trace (↥A) S : (a : S) → ↥A) ((algebraMap (↥B) S : (a : ↥B) → S) x) : ↥A)
    ((algebraMap R ↥A : (a : R) → ↥A)
        (Matrix.trace.{v, u} (n := Free.ChooseBasisIndex R ↥B)
          ((Algebra.leftMulMatrix (Free.chooseBasis R ↥B) :
              (a : ↥B) → Matrix (Free.ChooseBasisIndex R ↥B) (Free.ChooseBasisIndex R ↥B) R)
            x)) :
      ↥A)
simp_rw₁ :
  Eq.{v + 1} (α := ↥A)
    (Matrix.trace (n := Free.ChooseBasisIndex R ↥B)
      ((Algebra.leftMulMatrix (H.basisOfBasisRight H' (Free.chooseBasis R ↥B)) :
          (a : S) → Matrix (Free.ChooseBasisIndex R ↥B) (Free.ChooseBasisIndex R ↥B) ↥A)
        ((algebraMap (↥B) S : (a : ↥B) → S) x : S)))
    ((algebraMap R ↥A : (a : R) → ↥A)
      (Matrix.trace.{v, u} (n := Free.ChooseBasisIndex R ↥B)
        ((Algebra.leftMulMatrix (Free.chooseBasis R ↥B) :
            (a : ↥B) → Matrix (Free.ChooseBasisIndex R ↥B) (Free.ChooseBasisIndex R ↥B) R)
          x)))
simp_rw₂ :
  Eq.{v + 1} (α := ↥A)
    (∑ i : Free.ChooseBasisIndex R ↥B,
      Matrix.diag
        ((Algebra.leftMulMatrix (H.basisOfBasisRight H' (Free.chooseBasis R ↥B)) :
            (a : S) → Matrix (Free.ChooseBasisIndex R ↥B) (Free.ChooseBasisIndex R ↥B) ↥A)
          ((algebraMap (↥B) S : (a : ↥B) → S) x : S))
        i)
    ((algebraMap R ↥A : (a : R) → ↥A)
      (∑ i : Free.ChooseBasisIndex R ↥B,
        Matrix.diag
          ((Algebra.leftMulMatrix (Free.chooseBasis R ↥B) :
              (a : ↥B) → Matrix (Free.ChooseBasisIndex R ↥B) (Free.ChooseBasisIndex R ↥B) R)
            x)
          i))
simp_rw₃ :
  Eq.{v + 1} (α := ↥A)
    (∑ i : Free.ChooseBasisIndex R ↥B,
      Matrix.diag
        ((Algebra.leftMulMatrix (H.basisOfBasisRight H' (Free.chooseBasis R ↥B)) :
            (a : S) → Matrix (Free.ChooseBasisIndex R ↥B) (Free.ChooseBasisIndex R ↥B) ↥A)
          ((algebraMap (↥B) S : (a : ↥B) → S) x : S))
        i)
    (∑ x_1 : Free.ChooseBasisIndex R ↥B,
      (algebraMap R ↥A : (a : R) → ↥A)
        (Matrix.diag
          ((Algebra.leftMulMatrix (Free.chooseBasis R ↥B) :
              (a : ↥B) → Matrix (Free.ChooseBasisIndex R ↥B) (Free.ChooseBasisIndex R ↥B) R)
            x)
          x_1))
⊢ Eq (α := ↥A) ((Algebra.trace (↥A) S : (a : S) → ↥A) ((algebraMap (↥B) S : (a : ↥B) → S) x) : ↥A)
    ((algebraMap R ↥A : (a : R) → ↥A) ((Algebra.trace R ↥B : (a : ↥B) → R) x) : ↥A)
have simp_rw₄ : Eq.{v + 1} (α := ↥A)
  (∑ x_1 : Free.ChooseBasisIndex R ↥B,
    Matrix.diag
      ((RingHom.mapMatrix (algebraMap R ↥A) :
          (a : Matrix (Free.ChooseBasisIndex R ↥B) (Free.ChooseBasisIndex R ↥B) R) →
            Matrix (Free.ChooseBasisIndex R ↥B) (Free.ChooseBasisIndex R ↥B) ↥A)
        ((Algebra.leftMulMatrix (Free.chooseBasis R ↥B) :
            (a : ↥B) → Matrix (Free.ChooseBasisIndex R ↥B) (Free.ChooseBasisIndex R ↥B) R)
          x))
      x_1)
  (∑ x_1 : Free.ChooseBasisIndex R ↥B,
    (algebraMap R ↥A : (a : R) → ↥A)
      (Matrix.diag
        ((Algebra.leftMulMatrix (Free.chooseBasis R ↥B) :
            (a : ↥B) → Matrix (Free.ChooseBasisIndex R ↥B) (Free.ChooseBasisIndex R ↥B) R)
          x)
        x_1))
Tactic: simp_rw [Algebra.trace_eq_matrix_trace (Module.Free.chooseBasis R B),
    Algebra.trace_eq_matrix_trace (H.basisOfBasisRight H' (Module.Free.chooseBasis R B)),
    Matrix.trace, map_sum, leftMulMatrix_basisOfBasisRight_algebraMap, RingHom.mapMatrix_apply,
    Matrix.diag_apply, Matrix.map_apply]