awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
ι : Type w
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Fintype ι
b : Basis ι A B
z : B
i : ι
⊢ (traceMatrix.{u, v, w} A (B := B) (⇑b : (a : ι) → B) *ᵥ (b.equivFun : (a : B) → ι → A) z) i =
    (trace A B : (a : B) → A) (HMul.hMul (β := B) z ((b : (a : ι) → B) i : B))
have h : Eq.{u + 1} (α := A)
  (∑ j : ι,
      HMul.hMul (α := A) (β := A)
        ((of : (a : ι → ι → A) → Matrix ι ι A)
            (fun (i j : ι) ↦
              (((traceForm A B : (a : B) → B →ₗ[A] A) ((b : (a : ι) → B) i) : B →ₗ[A] A) : (a : B) → A)
                ((b : (a : ι) → B) j : B))
            i j :
          A)
        (replicateCol (Fin 1) ((b.equivFun : (a : B) → ι → A) z) j 0 : A) :
    A)
  ((trace A B : (a : B) → A) (HMul.hMul (β := B) z ((b : (a : ι) → B) i : B)) : A)
Tactic: rw [← replicateCol_apply (ι := Fin 1) (traceMatrix A b *ᵥ b.equivFun z) i 0, replicateCol_mulVec,
    Matrix.mul_apply, traceMatrix]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
ι : Type w
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Fintype ι
b : Basis ι A B
z : B
i : ι
⊢ Eq.{u + 1} (α := A)
    (∑ j : ι,
        HMul.hMul (α := A) (β := A)
          ((of : (a : ι → ι → A) → Matrix ι ι A)
              (fun (i j : ι) ↦
                (((traceForm A B : (a : B) → B →ₗ[A] A) ((b : (a : ι) → B) i) : B →ₗ[A] A) : (a : B) → A)
                  ((b : (a : ι) → B) j : B))
              i j :
            A)
          (replicateCol (Fin 1) ((b.equivFun : (a : B) → ι → A) z) j 0 : A) :
      A)
    ((trace A B : (a : B) → A) (HMul.hMul (β := B) z ((b : (a : ι) → B) i : B)) : A)
have h : Eq.{u + 1} (α := A)
  (∑ x : ι,
      HMul.hMul (α := A) (β := A)
        ((of : (a : ι → ι → A) → Matrix ι ι A)
            (fun (i j : ι) ↦
              (trace A B : (a : B) → A)
                (HMul.hMul (α := B) (β := B) ((b : (a : ι) → B) i : B) ((b : (a : ι) → B) j : B)))
            i x :
          A)
        ((b.equivFun : (a : B) → ι → A) z x : A) :
    A)
  ((trace A B : (a : B) → A) (HMul.hMul (β := B) z ((b : (a : ι) → B) i : B)) : A)
Tactic: simp only [replicateCol_apply, traceForm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
ι : Type w
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Fintype ι
b : Basis ι A B
z : B
i : ι
| ∑ x : ι,
    HMul.hMul (α := A) (β := A)
      ((of : (a : ι → ι → A) → Matrix ι ι A)
          (fun (i j : ι) ↦
            (trace A B : (a : B) → A) (HMul.hMul (α := B) (β := B) ((b : (a : ι) → B) i : B) ((b : (a : ι) → B) j : B)))
          i x :
        A)
      ((b.equivFun : (a : B) → ι → A) z x : A)
have s : univ
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
ι : Type w
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Fintype ι
b : Basis ι A B
z : B
i : ι
s : univ
| ∑ x : ι,
    HMul.hMul (α := A) (β := A)
      ((of : (a : ι → ι → A) → Matrix ι ι A)
          (fun (i j : ι) ↦
            (trace A B : (a : B) → A) (HMul.hMul (α := B) (β := B) ((b : (a : ι) → B) i : B) ((b : (a : ι) → B) j : B)))
          i x :
        A)
      ((b.equivFun : (a : B) → ι → A) z x : A)
have f : fun (x : ι) ↦
  HMul.hMul (α := A) (β := A)
    ((of : (a : ι → ι → A) → Matrix ι ι A)
        (fun (i j : ι) ↦
          (trace A B : (a : B) → A) (HMul.hMul (α := B) (β := B) ((b : (a : ι) → B) i : B) ((b : (a : ι) → B) j : B)))
        i x :
      A)
    ((b.equivFun : (a : B) → ι → A) z x : A)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
ι : Type w
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Fintype ι
b : Basis ι A B
z : B
i : ι
| fun (x : ι) ↦
    HMul.hMul (α := A) (β := A)
      ((of : (a : ι → ι → A) → Matrix ι ι A)
          (fun (i j : ι) ↦
            (trace A B : (a : B) → A) (HMul.hMul (α := B) (β := B) ((b : (a : ι) → B) i : B) ((b : (a : ι) → B) j : B)))
          i x :
        A)
      ((b.equivFun : (a : B) → ι → A) z x : A)
have f : ∀ (x : ι),
  HMul.hMul (α := A) (β := A)
    ((of : (a : ι → ι → A) → Matrix ι ι A)
        (fun (i j : ι) ↦
          (trace A B : (a : B) → A) (HMul.hMul (α := B) (β := B) ((b : (a : ι) → B) i : B) ((b : (a : ι) → B) j : B)))
        i x :
      A)
    ((b.equivFun : (a : B) → ι → A) z x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
ι : Type w
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Fintype ι
b : Basis ι A B
z : B
i x : ι
| HMul.hMul (α := A) (β := A)
    ((of : (a : ι → ι → A) → Matrix ι ι A)
        (fun (i j : ι) ↦
          (trace A B : (a : B) → A) (HMul.hMul (α := B) (β := B) ((b : (a : ι) → B) i : B) ((b : (a : ι) → B) j : B)))
        i x :
      A)
    ((b.equivFun : (a : B) → ι → A) z x : A)
have f : ((trace A B : (a : B) → A)
    (HSMul.hSMul.{u, v, v} (α := A) ((b.equivFun : (a : B) → ι → A) z x : A)
      (HMul.hMul (α := B) (β := B) ((b : (a : ι) → B) i : B) ((b : (a : ι) → B) x : B))) :
  A)
Tactic: rw [mul_comm _ (b.equivFun z _), ← smul_eq_mul, of_apply, ← map_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
ι : Type w
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Fintype ι
b : Basis ι A B
z : B
i : ι
| ∑ x : ι,
    HMul.hMul (α := A) (β := A)
      ((of : (a : ι → ι → A) → Matrix ι ι A)
          (fun (i j : ι) ↦
            (trace A B : (a : B) → A) (HMul.hMul (α := B) (β := B) ((b : (a : ι) → B) i : B) ((b : (a : ι) → B) j : B)))
          i x :
        A)
      ((b.equivFun : (a : B) → ι → A) z x : A)
have f : ∀ (x : ι),
  ((trace A B : (a : B) → A)
      (HSMul.hSMul.{u, v, v} (α := A) ((b.equivFun : (a : B) → ι → A) z x : A)
        (HMul.hMul (α := B) (β := B) ((b : (a : ι) → B) i : B) ((b : (a : ι) → B) x : B))) :
    A)
Tactic: congr
    rfl
    ext
    rw [mul_comm _ (b.equivFun z _), ← smul_eq_mul, of_apply, ← map_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
ι : Type w
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Fintype ι
b : Basis ι A B
z : B
i : ι
⊢ Eq.{u + 1} (α := A)
    (∑ x : ι,
        HMul.hMul (α := A) (β := A)
          ((of : (a : ι → ι → A) → Matrix ι ι A)
              (fun (i j : ι) ↦
                (trace A B : (a : B) → A)
                  (HMul.hMul (α := B) (β := B) ((b : (a : ι) → B) i : B) ((b : (a : ι) → B) j : B)))
              i x :
            A)
          ((b.equivFun : (a : B) → ι → A) z x : A) :
      A)
    ((trace A B : (a : B) → A) (HMul.hMul (β := B) z ((b : (a : ι) → B) i : B)) : A)
have h : Eq.{u + 1} (α := A)
  (∑ x : ι,
      (trace A B : (a : B) → A)
        (HSMul.hSMul.{u, v, v} (α := A) ((b.equivFun : (a : B) → ι → A) z x : A)
          (HMul.hMul (α := B) (β := B) ((b : (a : ι) → B) i : B) ((b : (a : ι) → B) x : B))) :
    A)
  ((trace A B : (a : B) → A) (HMul.hMul (β := B) z ((b : (a : ι) → B) i : B)) : A)
Tactic: conv_lhs =>
    congr
    rfl
    ext
    rw [mul_comm _ (b.equivFun z _), ← smul_eq_mul, of_apply, ← map_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
ι : Type w
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Fintype ι
b : Basis ι A B
z : B
i : ι
⊢ Eq.{u + 1} (α := A)
    (∑ x : ι,
        (trace A B : (a : B) → A)
          (HSMul.hSMul.{u, v, v} (α := A) ((b.equivFun : (a : B) → ι → A) z x : A)
            (HMul.hMul (α := B) (β := B) ((b : (a : ι) → B) i : B) ((b : (a : ι) → B) x : B))) :
      A)
    ((trace A B : (a : B) → A) (HMul.hMul (β := B) z ((b : (a : ι) → B) i : B)) : A)
have h : Eq.{u + 1} (α := A)
  ((trace A B : (a : B) → A)
      (∑ x : ι,
        HSMul.hSMul.{u, v, v} (α := A) ((b.equivFun : (a : B) → ι → A) z x : A)
          (HMul.hMul (α := B) (β := B) ((b : (a : ι) → B) i : B) ((b : (a : ι) → B) x : B))) :
    A)
  ((trace A B : (a : B) → A) (HMul.hMul (β := B) z ((b : (a : ι) → B) i : B)) : A)
Tactic: rw [← _root_.map_sum]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
ι : Type w
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Fintype ι
b : Basis ι A B
z : B
i : ι
⊢ Eq.{u + 1} (α := A)
    ((trace A B : (a : B) → A)
        (∑ x : ι,
          HSMul.hSMul.{u, v, v} (α := A) ((b.equivFun : (a : B) → ι → A) z x : A)
            (HMul.hMul (α := B) (β := B) ((b : (a : ι) → B) i : B) ((b : (a : ι) → B) x : B))) :
      A)
    ((trace A B : (a : B) → A) (HMul.hMul (β := B) z ((b : (a : ι) → B) i : B)) : A)
have h : ∑ x : ι,
    HSMul.hSMul.{u, v, v} (α := A) ((b.equivFun : (a : B) → ι → A) z x : A)
      (HMul.hMul (α := B) (β := B) ((b : (a : ι) → B) i : B) ((b : (a : ι) → B) x : B)) =
  HMul.hMul (β := B) z ((b : (a : ι) → B) i : B)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
ι : Type w
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Fintype ι
b : Basis ι A B
z : B
i : ι
| ∑ x : ι,
    HSMul.hSMul.{u, v, v} (α := A) ((b.equivFun : (a : B) → ι → A) z x : A)
      (HMul.hMul (α := B) (β := B) ((b : (a : ι) → B) i : B) ((b : (a : ι) → B) x : B))
have s : univ
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
ι : Type w
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Fintype ι
b : Basis ι A B
z : B
i : ι
s : univ
| ∑ x : ι,
    HSMul.hSMul.{u, v, v} (α := A) ((b.equivFun : (a : B) → ι → A) z x : A)
      (HMul.hMul (α := B) (β := B) ((b : (a : ι) → B) i : B) ((b : (a : ι) → B) x : B))
have f : fun (x : ι) ↦
  HSMul.hSMul.{u, v, v} (α := A) ((b.equivFun : (a : B) → ι → A) z x : A)
    (HMul.hMul (α := B) (β := B) ((b : (a : ι) → B) i : B) ((b : (a : ι) → B) x : B))
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
ι : Type w
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Fintype ι
b : Basis ι A B
z : B
i : ι
| fun (x : ι) ↦
    HSMul.hSMul.{u, v, v} (α := A) ((b.equivFun : (a : B) → ι → A) z x : A)
      (HMul.hMul (α := B) (β := B) ((b : (a : ι) → B) i : B) ((b : (a : ι) → B) x : B))
have f : ∀ (x : ι),
  HSMul.hSMul.{u, v, v} (α := A) ((b.equivFun : (a : B) → ι → A) z x : A)
    (HMul.hMul (α := B) (β := B) ((b : (a : ι) → B) i : B) ((b : (a : ι) → B) x : B))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
ι : Type w
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Fintype ι
b : Basis ι A B
z : B
i x : ι
| HSMul.hSMul.{u, v, v} (α := A) ((b.equivFun : (a : B) → ι → A) z x : A)
    (HMul.hMul (α := B) (β := B) ((b : (a : ι) → B) i : B) ((b : (a : ι) → B) x : B))
have f : HMul.hMul (α := B) ((b : (a : ι) → B) i : B)
  (HSMul.hSMul.{u, v, v} (α := A) (β := B) ((b.equivFun : (a : B) → ι → A) z x : A) ((b : (a : ι) → B) x : B))
Tactic: rw [← mul_smul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
ι : Type w
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Fintype ι
b : Basis ι A B
z : B
i : ι
| ∑ x : ι,
    HSMul.hSMul.{u, v, v} (α := A) ((b.equivFun : (a : B) → ι → A) z x : A)
      (HMul.hMul (α := B) (β := B) ((b : (a : ι) → B) i : B) ((b : (a : ι) → B) x : B))
have f : ∀ (x : ι),
  HMul.hMul (α := B) ((b : (a : ι) → B) i : B)
    (HSMul.hSMul.{u, v, v} (α := A) (β := B) ((b.equivFun : (a : B) → ι → A) z x : A) ((b : (a : ι) → B) x : B))
Tactic: congr
    rfl
    ext
    rw [← mul_smul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
ι : Type w
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Fintype ι
b : Basis ι A B
z : B
i : ι
⊢ ∑ x : ι,
      HSMul.hSMul.{u, v, v} (α := A) ((b.equivFun : (a : B) → ι → A) z x : A)
        (HMul.hMul (α := B) (β := B) ((b : (a : ι) → B) i : B) ((b : (a : ι) → B) x : B)) =
    HMul.hMul (β := B) z ((b : (a : ι) → B) i : B)
have h : ∑ x : ι,
    HMul.hMul (α := B) ((b : (a : ι) → B) i : B)
      (HSMul.hSMul.{u, v, v} (α := A) (β := B) ((b.equivFun : (a : B) → ι → A) z x : A) ((b : (a : ι) → B) x : B)) =
  HMul.hMul (β := B) z ((b : (a : ι) → B) i : B)
Tactic: conv_lhs =>
    congr
    rfl
    ext
    rw [← mul_smul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
ι : Type w
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Fintype ι
b : Basis ι A B
z : B
i : ι
⊢ ∑ x : ι,
      HMul.hMul (α := B) ((b : (a : ι) → B) i : B)
        (HSMul.hSMul.{u, v, v} (α := A) (β := B) ((b.equivFun : (a : B) → ι → A) z x : A) ((b : (a : ι) → B) x : B)) =
    HMul.hMul (β := B) z ((b : (a : ι) → B) i : B)
have h : HMul.hMul (α := B) (β := B) ((b : (a : ι) → B) i : B)
    (∑ i : ι,
        HSMul.hSMul.{u, v, v} (α := A) (β := B) ((b.equivFun : (a : B) → ι → A) z i : A) ((b : (a : ι) → B) i : B) :
      B) =
  HMul.hMul (α := B) ((b : (a : ι) → B) i : B) z
Tactic: rw [← Finset.mul_sum, mul_comm z]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
ι : Type w
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Fintype ι
b : Basis ι A B
z : B
i : ι
⊢ HMul.hMul (α := B) (β := B) ((b : (a : ι) → B) i : B)
      (∑ i : ι,
          HSMul.hSMul.{u, v, v} (α := A) (β := B) ((b.equivFun : (a : B) → ι → A) z i : A) ((b : (a : ι) → B) i : B) :
        B) =
    HMul.hMul (α := B) ((b : (a : ι) → B) i : B) z
have h : ∑ i : ι, HSMul.hSMul.{u, v, v} (α := A) (β := B) ((b.equivFun : (a : B) → ι → A) z i : A) ((b : (a : ι) → B) i : B) = z
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
ι : Type w
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Fintype ι
b : Basis ι A B
z : B
i : ι
⊢ ∑ i : ι, HSMul.hSMul.{u, v, v} (α := A) (β := B) ((b.equivFun : (a : B) → ι → A) z i : A) ((b : (a : ι) → B) i : B) =
    z
have h : z = z
Tactic: rw [b.sum_equivFun]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
A : Type u
B : Type v
C : Type z
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : CommRing C
inst_4 : Algebra A C
pb : PowerBasis A B
e : Fin pb.dim ≃ (B →ₐ[A] C)
⊢ embeddingsMatrixReindex A C (⇑pb.basis : (a : Fin pb.dim) → B) e =
    (vandermonde fun (i : Fin pb.dim) ↦ (((e : (a : Fin pb.dim) → B →ₐ[A] C) i : B →ₐ[A] C) : (a : B) → C) pb.gen)ᵀ
have a : ∀ (i j : Fin pb.dim),
  embeddingsMatrixReindex A C (⇑pb.basis : (a : Fin pb.dim) → B) e i j =
    (vandermonde fun (i : Fin pb.dim) ↦ (((e : (a : Fin pb.dim) → B →ₐ[A] C) i : B →ₐ[A] C) : (a : B) → C) pb.gen)ᵀ i j
Tactic: ext i j
-- 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
⊢ (traceMatrix K b).map (⇑(algebraMap K E) : (a : K) → E) =
    HMul.hMul (α := Matrix κ (L →ₐ[K] E) E) (β := Matrix (L →ₐ[K] E) κ E) (embeddingsMatrix K E b)
      (embeddingsMatrix K E b)ᵀ
have a : ∀ (i j : κ),
  (traceMatrix K b).map (⇑(algebraMap K E) : (a : K) → E) i j =
    HMul.hMul (α := Matrix κ (L →ₐ[K] E) E) (β := Matrix (L →ₐ[K] E) κ E) (embeddingsMatrix K E b)
      (embeddingsMatrix K E b)ᵀ i j
Tactic: ext (i j)
-- 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)
⊢ (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 κ (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)ᵀ
Tactic: rw [traceMatrix_eq_embeddingsMatrix_mul_trans, embeddingsMatrixReindex, reindex_apply,
    transpose_submatrix, ← submatrix_mul_transpose_submatrix, ← Equiv.coe_refl, Equiv.refl_symm]
-- 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)ᵀ
⊢ (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 κ (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))ᵀ
Tactic: rw [traceMatrix_eq_embeddingsMatrix_mul_trans, embeddingsMatrixReindex, reindex_apply,
    transpose_submatrix, ← submatrix_mul_transpose_submatrix, ← Equiv.coe_refl, Equiv.refl_symm]
-- 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))ᵀ
⊢ (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 κ (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))ᵀ
Tactic: rw [traceMatrix_eq_embeddingsMatrix_mul_trans, embeddingsMatrixReindex, reindex_apply,
    transpose_submatrix, ← submatrix_mul_transpose_submatrix, ← Equiv.coe_refl, Equiv.refl_symm]
-- 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))ᵀ
⊢ (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 κ (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 : κ) → κ))
Tactic: rw [traceMatrix_eq_embeddingsMatrix_mul_trans, embeddingsMatrixReindex, reindex_apply,
    transpose_submatrix, ← submatrix_mul_transpose_submatrix, ← Equiv.coe_refl, Equiv.refl_symm]