awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (hypothesis)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this_1 : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
g : K[X]
hg₁ : g.Separable
n : ℕ
hg₂ : Eq (α := K[X]) ((expand K (p ^ (n + 1)) : (a : K[X]) → K[X]) g : K[X]) (minpoly K x : K[X])
h : p ^ (n + 1) ∣ g.natDegree * p ^ (n + 1) - 1
this : p ^ (n + 1) ∣ g.natDegree * p ^ (n + 1) - (g.natDegree * p ^ (n + 1) - 1)
⊢ g.natDegree * p ^ (n + 1) ≠ 0
have this₁ : g.natDegree ≠ 0
Tactic: have : g.natDegree ≠ 0 := fun e ↦ by
            have := congr(natDegree $hg₂)
            rw [natDegree_expand, e, zero_mul] at this
            exact (minpoly.natDegree_pos (IsIntegral.isIntegral x)).ne this
-- 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
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
g : K[X]
hg₁ : g.Separable
m : ℕ
hg₂ : Eq (α := K[X]) ((expand K (p ^ m) : (a : K[X]) → K[X]) g : K[X]) (minpoly K x : K[X])
⊢ (↑(finrank (↥K⟮x⟯) L) : K) * -nextCoeff (minpoly K x) = (0 : (a : L) → K) x
have neg : ∀ (hg₂ : Eq (α := K[X]) ((expand K (HPow.hPow (β := ℕ) p 0) : (a : K[X]) → K[X]) g : K[X]) (minpoly K x : K[X])),
  (↑(finrank (↥K⟮x⟯) L) : K) * -nextCoeff (minpoly K x) = (0 : (a : L) → K) x
Tactic: cases m with
    | zero =>
      obtain rfl : g = minpoly K x := by simpa using hg₂
      cases hx hg₁
    | succ n =>
      rw [nextCoeff, if_neg, ← hg₂, coeff_expand (by positivity),
        if_neg, neg_zero, mul_zero, LinearMap.zero_apply]
      · rw [natDegree_expand]
        intro h
        have := Nat.dvd_sub (dvd_mul_left (p ^ (n + 1)) g.natDegree) h
        rw [tsub_tsub_cancel_of_le, Nat.dvd_one] at this
        · obtain rfl : g = minpoly K x := by simpa [this] using hg₂
          cases hx hg₁
        · rw [Nat.one_le_iff_ne_zero]
          have : g.natDegree ≠ 0 := fun e ↦ by
            have := congr(natDegree $hg₂)
            rw [natDegree_expand, e, zero_mul] at this
            exact (minpoly.natDegree_pos (IsIntegral.isIntegral x)).ne this
          positivity
      · exact (minpoly.natDegree_pos (IsIntegral.isIntegral x)).ne'
Cleared hypotheses: m, hg₂
-- 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
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
x : L
h₀ : FiniteDimensional K L
hx : ¬IsSeparable K x
g : K[X]
hg₁ : g.Separable
m : ℕ
hg₂ : Eq (α := K[X]) ((expand K (p ^ m) : (a : K[X]) → K[X]) g : K[X]) (minpoly K x : K[X])
neg :
  ∀ (hg₂ : Eq (α := K[X]) ((expand K (HPow.hPow (β := ℕ) p 0) : (a : K[X]) → K[X]) g : K[X]) (minpoly K x : K[X])),
    (↑(finrank (↥K⟮x⟯) L) : K) * -nextCoeff (minpoly K x) = (0 : (a : L) → K) x
⊢ (↑(finrank (↥K⟮x⟯) L) : K) * -nextCoeff (minpoly K x) = (0 : (a : L) → K) x
have neg₁ : ∀ (n : ℕ) (hg₂ : Eq (α := K[X]) ((expand K (p ^ (n + 1)) : (a : K[X]) → K[X]) g : K[X]) (minpoly K x : K[X])),
  (↑(finrank (↥K⟮x⟯) L) : K) * -nextCoeff (minpoly K x) = (0 : (a : L) → K) x
Tactic: cases m with
    | zero =>
      obtain rfl : g = minpoly K x := by simpa using hg₂
      cases hx hg₁
    | succ n =>
      rw [nextCoeff, if_neg, ← hg₂, coeff_expand (by positivity),
        if_neg, neg_zero, mul_zero, LinearMap.zero_apply]
      · rw [natDegree_expand]
        intro h
        have := Nat.dvd_sub (dvd_mul_left (p ^ (n + 1)) g.natDegree) h
        rw [tsub_tsub_cancel_of_le, Nat.dvd_one] at this
        · obtain rfl : g = minpoly K x := by simpa [this] using hg₂
          cases hx hg₁
        · rw [Nat.one_le_iff_ne_zero]
          have : g.natDegree ≠ 0 := fun e ↦ by
            have := congr(natDegree $hg₂)
            rw [natDegree_expand, e, zero_mul] at this
            exact (minpoly.natDegree_pos (IsIntegral.isIntegral x)).ne this
          positivity
      · exact (minpoly.natDegree_pos (IsIntegral.isIntegral x)).ne'
Cleared hypotheses: m, hg₂
-- 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
κ' : Type u_7
b : Basis κ A B
f : κ ≃ κ'
⊢ Eq (α := Matrix κ' κ' A) (traceMatrix.{u, v, u_7} A (B := B) (⇑(b.reindex f) : (a : κ') → B))
    ((reindex f f : (a : Matrix κ κ A) → Matrix κ' κ' A) (traceMatrix.{u, v, w} A (B := B) (⇑b : (a : κ) → B)))
have a : ∀ (x y : κ'),
  traceMatrix.{u, v, u_7} A (B := B) (⇑(b.reindex f) : (a : κ') → B) x y =
    (reindex f f : (a : Matrix κ κ A) → Matrix κ' κ' A) (traceMatrix.{u, v, w} A (B := B) (⇑b : (a : κ) → B)) x y
Tactic: ext (x y)
-- 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 : κ → B
P : Matrix κ κ A
⊢ traceMatrix A (b ᵥ* P.map (⇑(algebraMap A B) : (a : A) → B)) = Pᵀ * traceMatrix A b * P
have a : ∀ (α β : κ), traceMatrix A (b ᵥ* P.map (⇑(algebraMap A B) : (a : A) → B)) α β = (Pᵀ * traceMatrix A b * P) α β
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 : κ → B
P : Matrix κ κ A
α β : κ
⊢ traceMatrix A (b ᵥ* P.map (⇑(algebraMap A B) : (a : A) → B)) α β = (Pᵀ * traceMatrix A b * P) α β
have a : Eq.{u + 1} (α := A)
  (∑ y : κ,
    ∑ x : κ,
      (((traceForm A B : (a : B) → B →ₗ[A] A) (b x * P.map (⇑(algebraMap A B) : (a : A) → B) x α) : B →ₗ[A] A) :
          (a : B) → A)
        (b y * P.map (⇑(algebraMap A B) : (a : A) → B) y β))
  (∑ j : κ, (Pᵀ * traceMatrix A b) α j * P j β)
Tactic: rw [traceMatrix_apply, vecMul, dotProduct, vecMul, dotProduct, Matrix.mul_apply,
    BilinForm.sum_left,
    Fintype.sum_congr _ _ fun i : κ =>
      BilinForm.sum_right _ _ (b i * P.map (algebraMap A B) i α) fun y : κ =>
        b y * P.map (algebraMap A B) y β,
    sum_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 : κ → B
P : Matrix κ κ A
α β : κ
⊢ Eq.{u + 1} (α := A)
    (∑ y : κ,
      ∑ x : κ,
        (((traceForm A B : (a : B) → B →ₗ[A] A) (b x * P.map (⇑(algebraMap A B) : (a : A) → B) x α) : B →ₗ[A] A) :
            (a : B) → A)
          (b y * P.map (⇑(algebraMap A B) : (a : A) → B) y β))
    (∑ j : κ, (Pᵀ * traceMatrix A b) α j * P j β)
have a : Eq (α := κ → A)
  (fun (y : κ) ↦
    ∑ x : κ,
      (((traceForm A B : (a : B) → B →ₗ[A] A) (b x * P.map (⇑(algebraMap A B) : (a : A) → B) x α) : B →ₗ[A] A) :
          (a : B) → A)
        (b y * P.map (⇑(algebraMap A B) : (a : A) → B) y β))
  fun (j : κ) ↦ (Pᵀ * traceMatrix A b) α j * P j β
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 : κ → B
P : Matrix κ κ A
α β : κ
⊢ Eq (α := κ → A)
    (fun (y : κ) ↦
      ∑ x : κ,
        (((traceForm A B : (a : B) → B →ₗ[A] A) (b x * P.map (⇑(algebraMap A B) : (a : A) → B) x α) : B →ₗ[A] A) :
            (a : B) → A)
          (b y * P.map (⇑(algebraMap A B) : (a : A) → B) y β))
    fun (j : κ) ↦ (Pᵀ * traceMatrix A b) α j * P j β
have a : ∀ (x : κ),
  ∑ x_1 : κ,
      (((traceForm A B : (a : B) → B →ₗ[A] A) (b x_1 * P.map (⇑(algebraMap A B) : (a : A) → B) x_1 α) : B →ₗ[A] A) :
          (a : B) → A)
        (b x * P.map (⇑(algebraMap A B) : (a : A) → B) x β) =
    (Pᵀ * traceMatrix A b) α x * P x β
Tactic: ext x
-- 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 : κ → B
P : Matrix κ κ A
α β x : κ
⊢ ∑ x_1 : κ,
      (((traceForm A B : (a : B) → B →ₗ[A] A) (b x_1 * P.map (⇑(algebraMap A B) : (a : A) → B) x_1 α) : B →ₗ[A] A) :
          (a : B) → A)
        (b x * P.map (⇑(algebraMap A B) : (a : A) → B) x β) =
    (Pᵀ * traceMatrix A b) α x * P x β
have a : Eq.{u + 1} (α := A)
  (∑ x_1 : κ,
    (((traceForm A B : (a : B) → B →ₗ[A] A) (b x_1 * P.map (⇑(algebraMap A B) : (a : A) → B) x_1 α) : B →ₗ[A] A) :
        (a : B) → A)
      (b x * P.map (⇑(algebraMap A B) : (a : A) → B) x β))
  (∑ i : κ, Pᵀ α i * traceMatrix A b i x * P x β)
Tactic: rw [Matrix.mul_apply, sum_mul]
-- 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 : κ → B
P : Matrix κ κ A
α β x : κ
⊢ Eq.{u + 1} (α := A)
    (∑ x_1 : κ,
      (((traceForm A B : (a : B) → B →ₗ[A] A) (b x_1 * P.map (⇑(algebraMap A B) : (a : A) → B) x_1 α) : B →ₗ[A] A) :
          (a : B) → A)
        (b x * P.map (⇑(algebraMap A B) : (a : A) → B) x β))
    (∑ i : κ, Pᵀ α i * traceMatrix A b i x * P x β)
have a : Eq (α := κ → A)
  (fun (x_1 : κ) ↦
    (((traceForm A B : (a : B) → B →ₗ[A] A) (b x_1 * P.map (⇑(algebraMap A B) : (a : A) → B) x_1 α) : B →ₗ[A] A) :
        (a : B) → A)
      (b x * P.map (⇑(algebraMap A B) : (a : A) → B) x β))
  fun (i : κ) ↦ Pᵀ α i * traceMatrix A b i x * P x β
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 : κ → B
P : Matrix κ κ A
α β x : κ
⊢ Eq (α := κ → A)
    (fun (x_1 : κ) ↦
      (((traceForm A B : (a : B) → B →ₗ[A] A) (b x_1 * P.map (⇑(algebraMap A B) : (a : A) → B) x_1 α) : B →ₗ[A] A) :
          (a : B) → A)
        (b x * P.map (⇑(algebraMap A B) : (a : A) → B) x β))
    fun (i : κ) ↦ Pᵀ α i * traceMatrix A b i x * P x β
have a : ∀ (y : κ),
  (((traceForm A B : (a : B) → B →ₗ[A] A) (b y * P.map (⇑(algebraMap A B) : (a : A) → B) y α) : B →ₗ[A] A) :
        (a : B) → A)
      (b x * P.map (⇑(algebraMap A B) : (a : A) → B) x β) =
    Pᵀ α y * traceMatrix A b y x * P x β
Tactic: ext y
-- 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 : κ → B
P : Matrix κ κ A
α β x y : κ
⊢ (((traceForm A B : (a : B) → B →ₗ[A] A) (b y * P.map (⇑(algebraMap A B) : (a : A) → B) y α) : B →ₗ[A] A) :
        (a : B) → A)
      (b x * P.map (⇑(algebraMap A B) : (a : A) → B) x β) =
    Pᵀ α y * traceMatrix A b y x * P x β
have a : (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: rw [map_apply, traceForm_apply, mul_comm (b y), ← smul_def]
-- 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 : κ → B
P : Matrix κ κ A
α β x y : κ
⊢ (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 β
have 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 β
Tactic: simp only [smul_eq_mul, RingHom.id_apply, map_apply, transpose_apply, map_smulₛₗ,
    Algebra.smul_mul_assoc]
-- 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 : κ → B
P : Matrix κ κ A
α β x y : κ
⊢ 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 β
have 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 β
Tactic: rw [mul_comm (b x), ← smul_def]
-- 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 : κ → 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 α * traceMatrix A b y x * P x β
have 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
Tactic: ring_nf
-- 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 : κ → 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
have 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)
Tactic: rw [mul_assoc]
-- 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 : κ → B
P : Matrix κ κ A
⊢ traceMatrix A (P.map (⇑(algebraMap A B) : (a : A) → B) *ᵥ b) = P * traceMatrix A b * Pᵀ
have 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)
Tactic: refine AddEquiv.injective (transposeAddEquiv κ κ A) ?_
-- 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 : κ → B
P : Matrix κ κ A
⊢ 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)
have rw : (traceMatrix A (P.map (⇑(algebraMap A B) : (a : A) → B) *ᵥ b))ᵀ =
  (transposeAddEquiv κ κ A : (a : Matrix κ κ A) → Matrix κ κ A) (P * traceMatrix A b * Pᵀ)
Tactic: rw [transposeAddEquiv_apply, transposeAddEquiv_apply, ← vecMul_transpose, ← transpose_map,
    traceMatrix_of_matrix_vecMul, transpose_transpose]
-- 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 : κ → 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ᵀ)
⊢ 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)
have rw₁ : (traceMatrix A (P.map (⇑(algebraMap A B) : (a : A) → B) *ᵥ b))ᵀ = (P * traceMatrix A b * Pᵀ)ᵀ
Tactic: rw [transposeAddEquiv_apply, transposeAddEquiv_apply, ← vecMul_transpose, ← transpose_map,
    traceMatrix_of_matrix_vecMul, transpose_transpose]
-- 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 : κ → 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ᵀ)ᵀ
⊢ 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)
have rw₂ : (traceMatrix A (b ᵥ* (P.map (⇑(algebraMap A B) : (a : A) → B))ᵀ))ᵀ = (P * traceMatrix A b * Pᵀ)ᵀ
Tactic: rw [transposeAddEquiv_apply, transposeAddEquiv_apply, ← vecMul_transpose, ← transpose_map,
    traceMatrix_of_matrix_vecMul, transpose_transpose]
-- 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 : κ → 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ᵀ)ᵀ
⊢ 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)
have rw₃ : (traceMatrix A (b ᵥ* Pᵀ.map (⇑(algebraMap A B) : (a : A) → B)))ᵀ = (P * traceMatrix A b * Pᵀ)ᵀ
Tactic: rw [transposeAddEquiv_apply, transposeAddEquiv_apply, ← vecMul_transpose, ← transpose_map,
    traceMatrix_of_matrix_vecMul, transpose_transpose]
-- 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 : κ → 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ᵀ)ᵀ
⊢ 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)
have rw₄ : (Pᵀᵀ * traceMatrix A b * Pᵀ)ᵀ = (P * traceMatrix A b * Pᵀ)ᵀ
Tactic: rw [transposeAddEquiv_apply, transposeAddEquiv_apply, ← vecMul_transpose, ← transpose_map,
    traceMatrix_of_matrix_vecMul, transpose_transpose]
-- 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 : κ → 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ᵀ)ᵀ
⊢ 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)
have rw₅ : (P * traceMatrix A b * Pᵀ)ᵀ = (P * traceMatrix A b * Pᵀ)ᵀ
Tactic: rw [transposeAddEquiv_apply, transposeAddEquiv_apply, ← vecMul_transpose, ← transpose_map,
    traceMatrix_of_matrix_vecMul, transpose_transpose]
-- 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 κ
inst_4 : DecidableEq κ
b : Basis κ A B
⊢ 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))
have 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
Tactic: ext (i j)
-- 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 κ
inst_4 : DecidableEq κ
b : Basis κ A B
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
have 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)
Tactic: rw [traceMatrix_apply, traceForm_apply, traceForm_toMatrix]
-- 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 κ
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)
⊢ 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
have 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)
Tactic: rw [traceMatrix_apply, traceForm_apply, traceForm_toMatrix]
-- 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 κ
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)
⊢ 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
have 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)
Tactic: rw [traceMatrix_apply, traceForm_apply, traceForm_toMatrix]
-- 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
⊢ 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))
have 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))
Tactic: ext i