-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
κ : Type w
E : Type z
inst_3 : Field E
inst_4 : Algebra K E
inst_5 : Module.Finite K L
inst_6 : Algebra.IsSeparable K L
inst_7 : IsAlgClosed E
b : κ → L
inst_8 : Fintype κ
e : κ ≃ (L →ₐ[K] E)
rw :
  HMul.hMul (α := Matrix κ (L →ₐ[K] E) E) (β := Matrix (L →ₐ[K] E) κ E) (embeddingsMatrix K E b)
      (embeddingsMatrix K E b)ᵀ =
    embeddingsMatrixReindex K E b e * (embeddingsMatrixReindex K E b e)ᵀ
rw₁ :
  HMul.hMul (α := Matrix κ (L →ₐ[K] E) E) (β := Matrix (L →ₐ[K] E) κ E) (embeddingsMatrix K E b)
      (embeddingsMatrix K E b)ᵀ =
    HMul.hMul (α := Matrix κ κ E) (β := Matrix κ κ E)
      ((reindex (Equiv.refl κ) e.symm : (a : Matrix κ (L →ₐ[K] E) E) → Matrix κ κ E) (embeddingsMatrix K E b) :
        Matrix κ κ E)
      ((reindex (Equiv.refl κ) e.symm : (a : Matrix κ (L →ₐ[K] E) E) → Matrix κ κ E) (embeddingsMatrix K E b))ᵀ
rw₂ :
  HMul.hMul (α := Matrix κ (L →ₐ[K] E) E) (β := Matrix (L →ₐ[K] E) κ E) (embeddingsMatrix K E b)
      (embeddingsMatrix K E b)ᵀ =
    HMul.hMul (α := Matrix κ κ E)
      (submatrix (n := L →ₐ[K] E) (embeddingsMatrix K E b) (⇑(Equiv.refl κ).symm : (a : κ) → κ)
        (⇑e.symm.symm : (a : κ) → L →ₐ[K] E))
      (submatrix (n := L →ₐ[K] E) (embeddingsMatrix K E b) (⇑(Equiv.refl κ).symm : (a : κ) → κ)
          (⇑e.symm.symm : (a : κ) → L →ₐ[K] E))ᵀ
rw₃ :
  HMul.hMul (α := Matrix κ (L →ₐ[K] E) E) (β := Matrix (L →ₐ[K] E) κ E) (embeddingsMatrix K E b)
      (embeddingsMatrix K E b)ᵀ =
    HMul.hMul (α := Matrix κ κ E)
      (submatrix (n := L →ₐ[K] E) (embeddingsMatrix K E b) (⇑(Equiv.refl κ).symm : (a : κ) → κ)
        (⇑e.symm.symm : (a : κ) → L →ₐ[K] E))
      (submatrix (m := L →ₐ[K] E) (embeddingsMatrix K E b)ᵀ (⇑e.symm.symm : (a : κ) → L →ₐ[K] E)
        (⇑(Equiv.refl κ).symm : (a : κ) → κ))
rw₄ :
  submatrix (n := L →ₐ[K] E) (embeddingsMatrix K E b) _root_.id (⇑e.symm.symm : (a : κ) → L →ₐ[K] E) *
      submatrix (m := L →ₐ[K] E) (embeddingsMatrix K E b)ᵀ (⇑e.symm.symm : (a : κ) → L →ₐ[K] E) _root_.id =
    HMul.hMul (α := Matrix κ κ E)
      (submatrix (n := L →ₐ[K] E) (embeddingsMatrix K E b) (⇑(Equiv.refl κ).symm : (a : κ) → κ)
        (⇑e.symm.symm : (a : κ) → L →ₐ[K] E))
      (submatrix (m := L →ₐ[K] E) (embeddingsMatrix K E b)ᵀ (⇑e.symm.symm : (a : κ) → L →ₐ[K] E)
        (⇑(Equiv.refl κ).symm : (a : κ) → κ))
e₁ : κ ≃ (L →ₐ[K] E)
rw₅ :
  HMul.hMul (α := Matrix κ κ E)
      (submatrix (n := L →ₐ[K] E) (embeddingsMatrix K E b) (⇑(Equiv.refl κ) : (a : κ) → κ)
        (⇑e.symm.symm : (a : κ) → L →ₐ[K] E))
      (submatrix (m := L →ₐ[K] E) (embeddingsMatrix K E b)ᵀ (⇑e.symm.symm : (a : κ) → L →ₐ[K] E)
        (⇑(Equiv.refl κ) : (a : κ) → κ)) =
    HMul.hMul (α := Matrix κ κ E)
      (submatrix (n := L →ₐ[K] E) (embeddingsMatrix K E b) (⇑(Equiv.refl κ).symm : (a : κ) → κ)
        (⇑e.symm.symm : (a : κ) → L →ₐ[K] E))
      (submatrix (m := L →ₐ[K] E) (embeddingsMatrix K E b)ᵀ (⇑e.symm.symm : (a : κ) → L →ₐ[K] E)
        (⇑(Equiv.refl κ).symm : (a : κ) → κ))
e₂ : κ ≃ (L →ₐ[K] E)
⊢ (traceMatrix K b).map (⇑(algebraMap K E) : (a : K) → E) =
    embeddingsMatrixReindex K E b e * (embeddingsMatrixReindex K E b e)ᵀ
have rw₆ : HMul.hMul (α := Matrix κ κ E)
    (submatrix (n := L →ₐ[K] E) (embeddingsMatrix K E b) (⇑(Equiv.refl κ) : (a : κ) → κ)
      (⇑e.symm.symm : (a : κ) → L →ₐ[K] E))
    (submatrix (m := L →ₐ[K] E) (embeddingsMatrix K E b)ᵀ (⇑e.symm.symm : (a : κ) → L →ₐ[K] E)
      (⇑(Equiv.refl κ) : (a : κ) → κ)) =
  HMul.hMul (α := Matrix κ κ E)
    (submatrix (n := L →ₐ[K] E) (embeddingsMatrix K E b) (⇑(Equiv.refl κ) : (a : κ) → κ)
      (⇑e.symm.symm : (a : κ) → L →ₐ[K] E))
    (submatrix (m := L →ₐ[K] E) (embeddingsMatrix K E b)ᵀ (⇑e.symm.symm : (a : κ) → L →ₐ[K] E)
      (⇑(Equiv.refl κ) : (a : κ) → κ))
Tactic: rw [traceMatrix_eq_embeddingsMatrix_mul_trans, embeddingsMatrixReindex, reindex_apply,
    transpose_submatrix, ← submatrix_mul_transpose_submatrix, ← Equiv.coe_refl, Equiv.refl_symm]