-- Module: Mathlib.RingTheory.LinearDisjoint
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))
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))
simp_rw₅ :
  Eq.{v + 1} (α := ↥A)
    (∑ x_1 : Free.ChooseBasisIndex R ↥B,
      Matrix.diag
        (Matrix.map.{u, v, v, v} (α := R)
          ((Algebra.leftMulMatrix (Free.chooseBasis R ↥B) :
              (a : ↥B) → Matrix (Free.ChooseBasisIndex R ↥B) (Free.ChooseBasisIndex R ↥B) R)
            x)
          (⇑(algebraMap R ↥A) : (a : R) → ↥A))
        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))
simp_rw₆ :
  Eq.{v + 1} (α := ↥A)
    (∑ x_1 : Free.ChooseBasisIndex R ↥B,
      Matrix.map.{u, v, v, v} (α := R)
        ((Algebra.leftMulMatrix (Free.chooseBasis R ↥B) :
            (a : ↥B) → Matrix (Free.ChooseBasisIndex R ↥B) (Free.ChooseBasisIndex R ↥B) R)
          x)
        (⇑(algebraMap R ↥A) : (a : R) → ↥A) x_1 x_1)
    (∑ x_1 : Free.ChooseBasisIndex R ↥B,
      (algebraMap R ↥A : (a : R) → ↥A)
        ((Algebra.leftMulMatrix (Free.chooseBasis R ↥B) :
            (a : ↥B) → Matrix (Free.ChooseBasisIndex R ↥B) (Free.ChooseBasisIndex R ↥B) R)
          x x_1 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)

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]

Premises used: RingHom.mapMatrix_apply, Matrix.map_apply, Membership.mem, Matrix.trace, Subtype, map_sum, Matrix.diag_apply, Algebra.trace_eq_matrix_trace, Subalgebra.LinearDisjoint.basisOfBasisRight, Subalgebra.LinearDisjoint.leftMulMatrix_basisOfBasisRight_algebraMap, Module.Free.chooseBasis