-- Mathlib/RingTheory/Trace/Basic.lean
theorem traceMatrix_of_basis_mulVec (b : Basis ι A B) (z : B) :
    traceMatrix A b *ᵥ b.equivFun z = fun i => trace A B (z * b i)

Proof state:
case h.h.e_6.h
ι : Type w
inst✝³ : Fintype ι
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
b : Basis ι A B
z : B
i : ι
⊢ ∑ x : ι, b.equivFun z x • (b i * b x) = z * b i

Tactic:
conv_lhs =>
  congr
  rfl
  ext
  rw [← mul_smul_comm]

Result:
case h.h.e_6.h
ι : Type w
inst✝³ : Fintype ι
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
b : Basis ι A B
z : B
i : ι
⊢ ∑ x : ι, b i * b.equivFun z x • b x = z * b i

Proof state:
case h
ι : Type w
inst✝³ : Fintype ι
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
b : Basis ι A B
z : B
i : ι
⊢ ∑ x : ι, of (fun i j => (trace A B) (b i * b j)) i x * b.equivFun z x = (trace A B) (z * b i)

Tactic:
conv_lhs =>
  congr
  rfl
  ext
  rw [mul_comm _ (b.equivFun z _), ← smul_eq_mul, of_apply, ← LinearMap.map_smul]

Result:
case h
ι : Type w
inst✝³ : Fintype ι
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
b : Basis ι A B
z : B
i : ι
⊢ ∑ x : ι, (trace A B) (b.equivFun z x • (b i * b x)) = (trace A B) (z * b i)

Proof state:
case h.h.e_6.h
ι : Type w
inst✝³ : Fintype ι
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
b : Basis ι A B
z : B
i : ι
⊢ ∑ x : ι, b i * b.equivFun z x • b x = z * b i

Tactic:
rw [← Finset.mul_sum, mul_comm z]

Result:
case h.h.e_6.h
ι : Type w
inst✝³ : Fintype ι
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
b : Basis ι A B
z : B
i : ι
⊢ b i * ∑ i : ι, b.equivFun z i • b i = b i * z

Proof state:
case h
ι : Type w
inst✝³ : Fintype ι
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
b : Basis ι A B
z : B
i : ι
⊢ (traceMatrix A ⇑b *ᵥ b.equivFun z) i = (trace A B) (z * b i)

Tactic:
rw [← col_apply (ι := Fin 1) (traceMatrix A b *ᵥ b.equivFun z) i 0, col_mulVec,
  Matrix.mul_apply, traceMatrix]

Result:
case h
ι : Type w
inst✝³ : Fintype ι
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
b : Basis ι A B
z : B
i : ι
⊢ ∑ j : ι, of (fun i j => ((traceForm A B) (b i)) (b j)) i j * col (Fin 1) (b.equivFun z) j 0 = (trace A B) (z * b i)

Proof state:
case h.h.e_6.h
ι : Type w
inst✝³ : Fintype ι
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
b : Basis ι A B
z : B
i : ι
⊢ b i * ∑ i : ι, b.equivFun z i • b i = b i * z

Tactic:
congr

Result:
case h.h.e_6.h.e_a
ι : Type w
inst✝³ : Fintype ι
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
b : Basis ι A B
z : B
i : ι
⊢ ∑ i : ι, b.equivFun z i • b i = z

Proof state:
ι : Type w
inst✝³ : Fintype ι
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
b : Basis ι A B
z : B
⊢ traceMatrix A ⇑b *ᵥ b.equivFun z = fun i => (trace A B) (z * b i)

Tactic:
ext i

Result:
case h
ι : Type w
inst✝³ : Fintype ι
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
b : Basis ι A B
z : B
i : ι
⊢ (traceMatrix A ⇑b *ᵥ b.equivFun z) i = (trace A B) (z * b i)

Proof state:
case h
ι : Type w
inst✝³ : Fintype ι
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
b : Basis ι A B
z : B
i : ι
⊢ (trace A B) (∑ x : ι, b.equivFun z x • (b i * b x)) = (trace A B) (z * b i)

Tactic:
congr

Result:
case h.h.e_6.h
ι : Type w
inst✝³ : Fintype ι
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
b : Basis ι A B
z : B
i : ι
⊢ ∑ x : ι, b.equivFun z x • (b i * b x) = z * b i

Proof state:
case h
ι : Type w
inst✝³ : Fintype ι
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
b : Basis ι A B
z : B
i : ι
⊢ ∑ x : ι, (trace A B) (b.equivFun z x • (b i * b x)) = (trace A B) (z * b i)

Tactic:
rw [← _root_.map_sum]

Result:
case h
ι : Type w
inst✝³ : Fintype ι
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
b : Basis ι A B
z : B
i : ι
⊢ (trace A B) (∑ x : ι, b.equivFun z x • (b i * b x)) = (trace A B) (z * b i)

Proof state:
case h
ι : Type w
inst✝³ : Fintype ι
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
b : Basis ι A B
z : B
i : ι
⊢ ∑ j : ι, of (fun i j => ((traceForm A B) (b i)) (b j)) i j * col (Fin 1) (b.equivFun z) j 0 = (trace A B) (z * b i)

Tactic:
simp only [col_apply, traceForm_apply]

Result:
case h
ι : Type w
inst✝³ : Fintype ι
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
b : Basis ι A B
z : B
i : ι
⊢ ∑ x : ι, of (fun i j => (trace A B) (b i * b j)) i x * b.equivFun z x = (trace A B) (z * b i)

Proof state:
case h.h.e_6.h.e_a
ι : Type w
inst✝³ : Fintype ι
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
b : Basis ι A B
z : B
i : ι
⊢ ∑ i : ι, b.equivFun z i • b i = z

Tactic:
rw [b.sum_equivFun]

Result:
no goals