awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Trace.Basic
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 : κ → B
P : Matrix κ κ A
α β x y : κ
a :
  HMul.hMul (β := A) (P y α)
      ((trace A B : (a : B) → A) (b y * HMul.hMul (β := B) (b x) ((algebraMap A B : (a : A) → B) (P x β) : B)) : A) =
    P y α * traceMatrix A b y x * P x β
⊢ (trace A B : (a : B) → A) (P y α • b y * (b x * P.map (⇑(algebraMap A B) : (a : A) → B) x β)) =
    Pᵀ α y * traceMatrix A b y x * P x β

Tactic:
simp only [smul_eq_mul, RingHom.id_apply, map_apply, transpose_apply, map_smulₛₗ,
    Algebra.smul_mul_assoc]

Premises used: RingHom.id_apply, Matrix.map_apply, MulActionSemiHomClass.map_smulₛₗ, Algebra.smul_mul_assoc, smul_eq_mul, Matrix.transpose_apply
-- Module: Mathlib.RingTheory.Trace.Basic
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 : κ → B
P : Matrix κ κ A
α β x y : κ
a : HMul.hMul (β := A) (P y α) ((trace A B : (a : B) → A) (b y * P x β • b x) : A) = P y α * traceMatrix A b y x * P x β
⊢ HMul.hMul (β := A) (P y α)
      ((trace A B : (a : B) → A) (b y * HMul.hMul (β := B) (b x) ((algebraMap A B : (a : A) → B) (P x β) : B)) : A) =
    P y α * traceMatrix A b y x * P x β

Tactic:
rw [mul_comm (b x), ← smul_def]

Premises used: mul_comm, Algebra.smul_def
-- Module: Mathlib.RingTheory.Trace.Basic
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 : κ → B
P : Matrix κ κ A
α β x y : κ
a : HMul.hMul (β := A) (P y α) ((trace A B : (a : B) → A) (b y * P x β • b x) : A) = P y α * P x β * traceMatrix A b y x
⊢ HMul.hMul (β := A) (P y α) ((trace A B : (a : B) → A) (b y * P x β • b x) : A) = P y α * traceMatrix A b y x * P x β

Tactic:
ring_nf
-- Module: Mathlib.RingTheory.Trace.Basic
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 : κ → B
P : Matrix κ κ A
α β x y : κ
a :
  HMul.hMul (β := A) (P y α) ((trace A B : (a : B) → A) (b y * P x β • b x) : A) = P y α * (P x β * traceMatrix A b y x)
⊢ HMul.hMul (β := A) (P y α) ((trace A B : (a : B) → A) (b y * P x β • b x) : A) = P y α * P x β * traceMatrix A b y x

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.Trace.Basic
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 : κ → B
P : Matrix κ κ A
α β x y : κ
⊢ HMul.hMul (β := A) (P y α) ((trace A B : (a : B) → A) (b y * P x β • b x) : A) = P y α * (P x β * traceMatrix A b y x)

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Trace.Basic
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 : κ → B
P : Matrix κ κ A
⊢ traceMatrix A (P.map (⇑(algebraMap A B) : (a : A) → B) *ᵥ b) = P * traceMatrix A b * Pᵀ

Tactic:
AddEquiv.injective (transposeAddEquiv κ κ A) ?_

Premises used: AddEquiv.injective, Matrix.transposeAddEquiv
-- Module: Mathlib.RingTheory.Trace.Basic
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 : κ → B
P : Matrix κ κ A
refine :
  Eq (α := Matrix κ κ A)
    ((transposeAddEquiv κ κ A : (a : Matrix κ κ A) → Matrix κ κ A)
        (traceMatrix A (P.map (⇑(algebraMap A B) : (a : A) → B) *ᵥ b)) :
      Matrix κ κ A)
    ((transposeAddEquiv κ κ A : (a : Matrix κ κ A) → Matrix κ κ A) (P * traceMatrix A b * Pᵀ) : Matrix κ κ A)
⊢ traceMatrix A (P.map (⇑(algebraMap A B) : (a : A) → B) *ᵥ b) = P * traceMatrix A b * Pᵀ

Tactic:
refine AddEquiv.injective (transposeAddEquiv κ κ A) ?_

Premises used: AddEquiv.injective, Matrix.transposeAddEquiv
-- Module: Mathlib.RingTheory.Trace.Basic
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 : κ → B
P : Matrix κ κ A
rw :
  (traceMatrix A (P.map (⇑(algebraMap A B) : (a : A) → B) *ᵥ b))ᵀ =
    (transposeAddEquiv κ κ A : (a : Matrix κ κ A) → Matrix κ κ A) (P * traceMatrix A b * Pᵀ)
rw₁ : (traceMatrix A (P.map (⇑(algebraMap A B) : (a : A) → B) *ᵥ b))ᵀ = (P * traceMatrix A b * Pᵀ)ᵀ
rw₂ : (traceMatrix A (b ᵥ* (P.map (⇑(algebraMap A B) : (a : A) → B))ᵀ))ᵀ = (P * traceMatrix A b * Pᵀ)ᵀ
rw₃ : (traceMatrix A (b ᵥ* Pᵀ.map (⇑(algebraMap A B) : (a : A) → B)))ᵀ = (P * traceMatrix A b * Pᵀ)ᵀ
rw₄ : (Pᵀᵀ * traceMatrix A b * Pᵀ)ᵀ = (P * traceMatrix A b * Pᵀ)ᵀ
rw₅ rw₆ : (P * traceMatrix A b * Pᵀ)ᵀ = (P * traceMatrix A b * Pᵀ)ᵀ
⊢ Eq (α := Matrix κ κ A)
    ((transposeAddEquiv κ κ A : (a : Matrix κ κ A) → Matrix κ κ A)
        (traceMatrix A (P.map (⇑(algebraMap A B) : (a : A) → B) *ᵥ b)) :
      Matrix κ κ A)
    ((transposeAddEquiv κ κ A : (a : Matrix κ κ A) → Matrix κ κ A) (P * traceMatrix A b * Pᵀ) : Matrix κ κ A)

Tactic:
rw [transposeAddEquiv_apply, transposeAddEquiv_apply, ← vecMul_transpose, ← transpose_map,
    traceMatrix_of_matrix_vecMul, transpose_transpose]

Premises used: Matrix.transpose_transpose, Algebra.traceMatrix_of_matrix_vecMul, Matrix.transpose_map, Matrix.transposeAddEquiv_apply, Matrix.vecMul_transpose
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
κ : Type w
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Fintype κ
inst_4 : DecidableEq κ
b : Basis κ A B
a :
  ∀ (i j : κ),
    traceMatrix.{u, v, w} A (B := B) (⇑b : (a : κ) → B) i j =
      (LinearMap.BilinForm.toMatrix b : (a : BilinForm A B) → Matrix κ κ A) (traceForm A B) i j
⊢ Eq (α := Matrix κ κ A) (traceMatrix.{u, v, w} A (B := B) (⇑b : (a : κ) → B))
    ((LinearMap.BilinForm.toMatrix b : (a : BilinForm A B) → Matrix κ κ A) (traceForm A B))

Tactic:
ext (i j)
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
κ : Type w
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Fintype κ
inst_4 : DecidableEq κ
b : Basis κ A B
i j : κ
a :
  Eq.{u + 1} (α := A)
    ((((traceForm A B : (a : B) → B →ₗ[A] A) ((b : (a : κ) → B) i) : B →ₗ[A] A) : (a : B) → A)
        ((b : (a : κ) → B) j : B) :
      A)
    ((LinearMap.BilinForm.toMatrix b : (a : BilinForm A B) → Matrix κ κ A) (traceForm A B) i j : A)
a₁ :
  Eq.{u + 1} (α := A)
    ((trace A B : (a : B) → A) (HMul.hMul (α := B) (β := B) ((b : (a : κ) → B) i : B) ((b : (a : κ) → B) j : B)) : A)
    ((LinearMap.BilinForm.toMatrix b : (a : BilinForm A B) → Matrix κ κ A) (traceForm A B) i j : A)
a₂ a₃ :
  Eq.{u + 1} (α := A)
    ((trace A B : (a : B) → A) (HMul.hMul (α := B) (β := B) ((b : (a : κ) → B) i : B) ((b : (a : κ) → B) j : B)) : A)
    ((trace A B : (a : B) → A) (HMul.hMul (α := B) (β := B) ((b : (a : κ) → B) i : B) ((b : (a : κ) → B) j : B)) : A)
⊢ traceMatrix.{u, v, w} A (B := B) (⇑b : (a : κ) → B) i j =
    (LinearMap.BilinForm.toMatrix b : (a : BilinForm A B) → Matrix κ κ A) (traceForm A B) i j

Tactic:
rw [traceMatrix_apply, traceForm_apply, traceForm_toMatrix]

Premises used: Algebra.traceMatrix_apply, Algebra.traceForm_apply, Algebra.traceForm_toMatrix
-- Module: Mathlib.RingTheory.Trace.Basic
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
h :
  ∀ (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))
⊢ Eq (α := ι → A) (traceMatrix.{u, v, w} A (B := B) (⇑b : (a : ι) → B) *ᵥ (b.equivFun : (a : B) → ι → A) z)
    fun (i : ι) ↦ (trace A B : (a : B) → A) (HMul.hMul (β := B) z ((b : (a : ι) → B) i : B))

Tactic:
ext i
-- Module: Mathlib.RingTheory.Trace.Basic
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 : ι
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)
⊢ (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))

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

Premises used: Matrix.mul_apply, Matrix.replicateCol_mulVec, OfNat.ofNat, Matrix.replicateCol_apply, Algebra.traceMatrix, Matrix.mulVec, DFunLike.coe, Module.Basis.equivFun
-- Module: Mathlib.RingTheory.Trace.Basic
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 : ι
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)
⊢ 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:
simp only [replicateCol_apply, traceForm_apply]

Premises used: Algebra.traceForm_apply, Matrix.replicateCol_apply
-- Module: Mathlib.RingTheory.Trace.Basic
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
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)
| ∑ 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
-- Module: Mathlib.RingTheory.Trace.Basic
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 : ι
| univ

Tactic:
rfl
-- Module: Mathlib.RingTheory.Trace.Basic
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 : ι
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)
| 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:
ext
-- Module: Mathlib.RingTheory.Trace.Basic
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 : ι
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)
| 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:
rw [mul_comm _ (b.equivFun z _), ← smul_eq_mul, of_apply, ← map_smul]

Premises used: Matrix.of_apply, mul_comm, smul_eq_mul, DFunLike.coe, Module.Basis.equivFun, map_smul
-- Module: Mathlib.RingTheory.Trace.Basic
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 : ι
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)
| ∑ 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
    rfl
    ext
    rw [mul_comm _ (b.equivFun z _), ← smul_eq_mul, of_apply, ← map_smul]

Premises used: Matrix.of_apply, mul_comm, smul_eq_mul, DFunLike.coe, Module.Basis.equivFun, map_smul
-- Module: Mathlib.RingTheory.Trace.Basic
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 : ι
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)
⊢ 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:
conv_lhs =>
    congr
    rfl
    ext
    rw [mul_comm _ (b.equivFun z _), ← smul_eq_mul, of_apply, ← map_smul]

Premises used: Matrix.of_apply, mul_comm, smul_eq_mul, DFunLike.coe, Module.Basis.equivFun, map_smul
-- Module: Mathlib.RingTheory.Trace.Basic
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 : ι
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)
⊢ 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:
rw [← _root_.map_sum]

Premises used: map_sum
-- Module: Mathlib.RingTheory.Trace.Basic
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 : ι
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)
⊢ 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:
congr
-- Module: Mathlib.RingTheory.Trace.Basic
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
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))
| ∑ 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
-- Module: Mathlib.RingTheory.Trace.Basic
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 : ι
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))
| 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:
ext
-- Module: Mathlib.RingTheory.Trace.Basic
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 : ι
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))
| 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:
rw [← mul_smul_comm]

Premises used: mul_smul_comm
-- Module: Mathlib.RingTheory.Trace.Basic
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 : ι
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))
| ∑ 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
    rfl
    ext
    rw [← mul_smul_comm]

Premises used: mul_smul_comm
-- Module: Mathlib.RingTheory.Trace.Basic
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 : ι
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)
⊢ ∑ 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:
conv_lhs =>
    congr
    rfl
    ext
    rw [← mul_smul_comm]

Premises used: mul_smul_comm
-- Module: Mathlib.RingTheory.Trace.Basic
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 : ι
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
⊢ ∑ 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:
rw [← Finset.mul_sum, mul_comm z]

Premises used: Finset.mul_sum, mul_comm
-- Module: Mathlib.RingTheory.Trace.Basic
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 : ι
h :
  ∑ i : ι, HSMul.hSMul.{u, v, v} (α := A) (β := B) ((b.equivFun : (a : B) → ι → A) z i : A) ((b : (a : ι) → B) i : B) =
    z
⊢ 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:
congr
-- Module: Mathlib.RingTheory.Trace.Basic
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 : ι
h h₁ : z = z
⊢ ∑ i : ι, HSMul.hSMul.{u, v, v} (α := A) (β := B) ((b.equivFun : (a : B) → ι → A) z i : A) ((b : (a : ι) → B) i : B) =
    z

Tactic:
rw [b.sum_equivFun]

Premises used: Module.Basis.sum_equivFun
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
κ : Type w
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
b : κ → B
i : κ
σ : B →ₐ[A] C
⊢ embeddingsMatrix A C b i σ = (σ : (a : B) → C) (b i)

Tactic:
rfl

Premises used: Algebra.embeddingsMatrix, rfl
-- Module: Mathlib.RingTheory.Trace.Basic
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)
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
⊢ 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)ᵀ

Tactic:
ext i j
-- Module: Mathlib.RingTheory.Trace.Basic
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)
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:
simp [embeddingsMatrixReindex, embeddingsMatrix]

Premises used: Algebra.embeddingsMatrixReindex, Algebra.embeddingsMatrix
-- Module: Mathlib.RingTheory.Trace.Basic
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
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
⊢ (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)ᵀ

Tactic:
ext (i j)