awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : M →ₗ[R] M
H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) R M)
neg :
  Eq.{u + 1} (α := R)
    ((if H : ∃ (s : Finset M), Nonempty (Basis (↥s) R M) then traceAux R ⋯.some else 0 : (a : M →ₗ[R] M) → R) (f * g) :
      R)
    ((if H : ∃ (s : Finset M), Nonempty (Basis (↥s) R M) then traceAux R ⋯.some else 0 : (a : M →ₗ[R] M) → R) (g * f) :
      R)
neg₁ : Eq.{u + 1} (α := R) ((0 : (a : M →ₗ[R] M) → R) (f * g) : R) ((0 : (a : M →ₗ[R] M) → R) (g * f) : R)
⊢ Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * g) : R) ((trace R M : (a : M →ₗ[R] M) → R) (g * f) : R)
have neg₂ : Eq.{u + 1} (α := R) (0 : R) ((0 : (a : M →ₗ[R] M) → R) (g * f) : R)
Tactic: rw [trace, dif_neg H, LinearMap.zero_apply, LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : M →ₗ[R] M
H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) R M)
neg :
  Eq.{u + 1} (α := R)
    ((if H : ∃ (s : Finset M), Nonempty (Basis (↥s) R M) then traceAux R ⋯.some else 0 : (a : M →ₗ[R] M) → R) (f * g) :
      R)
    ((if H : ∃ (s : Finset M), Nonempty (Basis (↥s) R M) then traceAux R ⋯.some else 0 : (a : M →ₗ[R] M) → R) (g * f) :
      R)
neg₁ : Eq.{u + 1} (α := R) ((0 : (a : M →ₗ[R] M) → R) (f * g) : R) ((0 : (a : M →ₗ[R] M) → R) (g * f) : R)
neg₂ : Eq.{u + 1} (α := R) (0 : R) ((0 : (a : M →ₗ[R] M) → R) (g * f) : R)
⊢ Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * g) : R) ((trace R M : (a : M →ₗ[R] M) → R) (g * f) : R)
have neg₃ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [trace, dif_neg H, LinearMap.zero_apply, LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : M →ₗ[R] M
⊢ Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * g) : R) ((trace R M : (a : M →ₗ[R] M) → R) (g * f) : R)
have pos : ∀ (H : ∃ (s : Finset M), Nonempty (Basis (↥s) R M)),
  Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * g) : R) ((trace R M : (a : M →ₗ[R] M) → R) (g * f) : R)
Tactic: classical
  by_cases H : ∃ s : Finset M, Nonempty (Basis s R M)
  · let ⟨s, ⟨b⟩⟩ := H
    simp_rw [trace_eq_matrix_trace R b, LinearMap.toMatrix_mul]
    apply Matrix.trace_mul_comm
  · rw [trace, dif_neg H, LinearMap.zero_apply, LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : M →ₗ[R] M
pos :
  ∀ (H : ∃ (s : Finset M), Nonempty (Basis (↥s) R M)),
    Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * g) : R) ((trace R M : (a : M →ₗ[R] M) → R) (g * f) : R)
⊢ Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * g) : R) ((trace R M : (a : M →ₗ[R] M) → R) (g * f) : R)
have neg : ∀ (H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) R M)),
  Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * g) : R) ((trace R M : (a : M →ₗ[R] M) → R) (g * f) : R)
Tactic: classical
  by_cases H : ∃ s : Finset M, Nonempty (Basis s R M)
  · let ⟨s, ⟨b⟩⟩ := H
    simp_rw [trace_eq_matrix_trace R b, LinearMap.toMatrix_mul]
    apply Matrix.trace_mul_comm
  · rw [trace, dif_neg H, LinearMap.zero_apply, LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g h : M →ₗ[R] M
⊢ Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * g * h) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) (h * f * g) : R)
have rw : Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (h * (f * g)) : R)
  ((trace R M : (a : M →ₗ[R] M) → R) (h * f * g) : R)
Tactic: rw [LinearMap.trace_mul_comm, ← mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g h : M →ₗ[R] M
rw :
  Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (h * (f * g)) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) (h * f * g) : R)
⊢ Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * g * h) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) (h * f * g) : R)
have rw₁ : Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (h * f * g) : R)
  ((trace R M : (a : M →ₗ[R] M) → R) (h * f * g) : R)
Tactic: rw [LinearMap.trace_mul_comm, ← mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g h : M →ₗ[R] M
⊢ Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * (g * h)) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) (h * (f * g)) : R)
have rw : Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * g * h) : R)
  ((trace R M : (a : M →ₗ[R] M) → R) (h * (f * g)) : R)
Tactic: rw [← mul_assoc, LinearMap.trace_mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g h : M →ₗ[R] M
rw :
  Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * g * h) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) (h * (f * g)) : R)
⊢ Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * (g * h)) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) (h * (f * g)) : R)
have rw₁ : Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (h * (f * g)) : R)
  ((trace R M : (a : M →ₗ[R] M) → R) (h * (f * g)) : R)
Tactic: rw [← mul_assoc, LinearMap.trace_mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g h : M →ₗ[R] M
⊢ Eq.{u_2 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (⁅f, g⁆ * h) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) (f * ⁅g, h⁆) : R)
have simp : HSub.hSub (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * (g * h)) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) (g * (f * h)) : R) =
  HSub.hSub (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * (g * h)) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) (f * (h * g)) : R)
Tactic: simp only [Ring.lie_def, sub_mul, mul_sub, map_sub, mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g h : M →ₗ[R] M
⊢ HSub.hSub (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * (g * h)) : R)
      ((trace R M : (a : M →ₗ[R] M) → R) (g * (f * h)) : R) =
    HSub.hSub (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * (g * h)) : R)
      ((trace R M : (a : M →ₗ[R] M) → R) (f * (h * g)) : R)
have rw : HSub.hSub (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * (g * h)) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) (f * h * g) : R) =
  HSub.hSub (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * (g * h)) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) (f * (h * g)) : R)
Tactic: rw [trace_mul_comm R g (f * h), mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g h : M →ₗ[R] M
rw :
  HSub.hSub (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * (g * h)) : R)
      ((trace R M : (a : M →ₗ[R] M) → R) (f * h * g) : R) =
    HSub.hSub (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * (g * h)) : R)
      ((trace R M : (a : M →ₗ[R] M) → R) (f * (h * g)) : R)
⊢ HSub.hSub (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * (g * h)) : R)
      ((trace R M : (a : M →ₗ[R] M) → R) (g * (f * h)) : R) =
    HSub.hSub (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * (g * h)) : R)
      ((trace R M : (a : M →ₗ[R] M) → R) (f * (h * g)) : R)
have rw₁ : HSub.hSub (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * (g * h)) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) (f * (h * g)) : R) =
  HSub.hSub (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * (g * h)) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) (f * (h * g)) : R)
Tactic: rw [trace_mul_comm R g (f * h), mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
g : M →ₗ[R] M
f : (M →ₗ[R] M)ˣ
⊢ Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) ((↑f : M →ₗ[R] M) * g * (↑f⁻¹ : M →ₗ[R] M)) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) g : R)
have rw : Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) ((↑f⁻¹ : M →ₗ[R] M) * ((↑f : M →ₗ[R] M) * g)) : R)
  ((trace R M : (a : M →ₗ[R] M) → R) g : R)
Tactic: rw [trace_mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g : End R M
⊢ Eq.{u_2 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) ⁅f, g⁆ : R) (0 : R)
have rw : HSub.hSub (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) (g * f) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) (g * f) : R) =
  0
Tactic: rw [Ring.lie_def, map_sub, trace_mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
inst_3 : Finite ι
b : Basis ι R M
⊢ Eq (α := Dual R M ⊗[R] M →ₗ[R] R) (trace R M ∘ₗ dualTensorHom R M M) (contractLeft R M)
have intro : ∀ (val : Fintype ι), Eq (α := Dual R M ⊗[R] M →ₗ[R] R) (trace R M ∘ₗ dualTensorHom R M M) (contractLeft R M)
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
inst_3 : Finite ι
b : Basis ι R M
val : Fintype ι
⊢ Eq (α := Dual R M ⊗[R] M →ₗ[R] R) (trace R M ∘ₗ dualTensorHom R M M) (contractLeft R M)
have intro : ∀ (i : ι × ι),
  Eq.{u_1 + 1} (α := R)
    ((trace R M ∘ₗ dualTensorHom R M M : (a : Dual R M ⊗[R] M) → R)
        (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) i :
          Dual R M ⊗[R] M) :
      R)
    ((contractLeft R M : (a : Dual R M ⊗[R] M) → R)
        (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) i :
          Dual R M ⊗[R] M) :
      R)
Tactic: apply Basis.ext (Basis.tensorProduct (Basis.dualBasis b) b)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
inst_3 : Finite ι
b : Basis ι R M
val : Fintype ι
i j : ι
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R M ∘ₗ dualTensorHom R M M : (a : Dual R M ⊗[R] M) → R)
        (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) (i, j) :
          Dual R M ⊗[R] M) :
      R)
    ((contractLeft R M : (a : Dual R M ⊗[R] M) → R)
        (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) (i, j) :
          Dual R M ⊗[R] M) :
      R)
have intro : Eq.{u_1 + 1} (α := R)
  ((trace R M : (a : M →ₗ[R] M) → R)
      ((dualTensorHom R M M : (a : Dual R M ⊗[R] M) → M →ₗ[R] M) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j) : M →ₗ[R] M) :
    R)
  ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)
Tactic: simp only [Function.comp_apply, Basis.tensorProduct_apply, Basis.coe_dualBasis, coe_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
inst_3 : Finite ι
b : Basis ι R M
val : Fintype ι
i j : ι
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        ((dualTensorHom R M M : (a : Dual R M ⊗[R] M) → M →ₗ[R] M) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j) : M →ₗ[R] M) :
      R)
    ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)
have intro : Eq.{u_1 + 1} (α := R) (Matrix.trace (Matrix.single j i 1) : R)
  ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)
Tactic: rw [trace_eq_matrix_trace R b, toMatrix_dualTensorHom]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
inst_3 : Finite ι
b : Basis ι R M
val : Fintype ι
i j : ι
⊢ Eq.{u_1 + 1} (α := R) (Matrix.trace (Matrix.single j i 1) : R)
    ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)
have intro : Eq.{u_1 + 1} (α := R) (Matrix.trace (Matrix.single i i 1) : R)
  ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) i : Dual R M ⊗[R] M) : R)
Tactic: obtain rfl | hij := eq_or_ne i j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
inst_3 : Finite ι
b : Basis ι R M
val : Fintype ι
i j : ι
intro :
  Eq.{u_1 + 1} (α := R) (Matrix.trace (Matrix.single i i 1) : R)
    ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) i : Dual R M ⊗[R] M) : R)
⊢ Eq.{u_1 + 1} (α := R) (Matrix.trace (Matrix.single j i 1) : R)
    ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)
have intro₁ : ∀ (hij : i ≠ j),
  Eq.{u_1 + 1} (α := R) (Matrix.trace (Matrix.single j i 1) : R)
    ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)
Tactic: obtain rfl | hij := eq_or_ne i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
inst_3 : Finite ι
b : Basis ι R M
val : Fintype ι
i j : ι
hij : i ≠ j
⊢ Eq.{u_1 + 1} (α := R) (Matrix.trace (Matrix.single j i 1) : R)
    ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)
have intro : Eq.{u_1 + 1} (α := R) (0 : R)
  ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)
Tactic: rw [Matrix.trace_single_eq_of_ne j i (1 : R) hij.symm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
inst_3 : Finite ι
b : Basis ι R M
⊢ Eq (α := Dual R M ⊗[R] M →ₗ[R] R) (trace R M ∘ₗ dualTensorHom R M M) (contractLeft R M)
have intro : ∀ (val : Fintype ι), Eq (α := Dual R M ⊗[R] M →ₗ[R] R) (trace R M ∘ₗ dualTensorHom R M M) (contractLeft R M)
Tactic: classical
    cases nonempty_fintype ι
    apply Basis.ext (Basis.tensorProduct (Basis.dualBasis b) b)
    rintro ⟨i, j⟩
    simp only [Function.comp_apply, Basis.tensorProduct_apply, Basis.coe_dualBasis, coe_comp]
    rw [trace_eq_matrix_trace R b, toMatrix_dualTensorHom]
    obtain rfl | hij := eq_or_ne i j
    · simp
    rw [Matrix.trace_single_eq_of_ne j i (1 : R) hij.symm]
    simp [hij]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
inst_3 : Finite ι
b : Basis ι R M
intro : ∀ (val : Fintype ι), Eq (α := Dual R M ⊗[R] M →ₗ[R] R) (trace R M ∘ₗ dualTensorHom R M M) (contractLeft R M)
⊢ Eq (α := Dual R M ⊗[R] M →ₗ[R] R) (trace R M ∘ₗ dualTensorHom R M M) (contractLeft R M)
have intro₁ : ∀ (val : Fintype ι) (i : ι × ι),
  Eq.{u_1 + 1} (α := R)
    ((trace R M ∘ₗ dualTensorHom R M M : (a : Dual R M ⊗[R] M) → R)
        (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) i :
          Dual R M ⊗[R] M) :
      R)
    ((contractLeft R M : (a : Dual R M ⊗[R] M) → R)
        (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) i :
          Dual R M ⊗[R] M) :
      R)
Tactic: classical
    cases nonempty_fintype ι
    apply Basis.ext (Basis.tensorProduct (Basis.dualBasis b) b)
    rintro ⟨i, j⟩
    simp only [Function.comp_apply, Basis.tensorProduct_apply, Basis.coe_dualBasis, coe_comp]
    rw [trace_eq_matrix_trace R b, toMatrix_dualTensorHom]
    obtain rfl | hij := eq_or_ne i j
    · simp
    rw [Matrix.trace_single_eq_of_ne j i (1 : R) hij.symm]
    simp [hij]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
inst_3 : Finite ι
b : Basis ι R M
intro : ∀ (val : Fintype ι), Eq (α := Dual R M ⊗[R] M →ₗ[R] R) (trace R M ∘ₗ dualTensorHom R M M) (contractLeft R M)
intro₁ :
  ∀ (val : Fintype ι) (i : ι × ι),
    Eq.{u_1 + 1} (α := R)
      ((trace R M ∘ₗ dualTensorHom R M M : (a : Dual R M ⊗[R] M) → R)
          (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) i :
            Dual R M ⊗[R] M) :
        R)
      ((contractLeft R M : (a : Dual R M ⊗[R] M) → R)
          (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) i :
            Dual R M ⊗[R] M) :
        R)
⊢ Eq (α := Dual R M ⊗[R] M →ₗ[R] R) (trace R M ∘ₗ dualTensorHom R M M) (contractLeft R M)
have intro₂ : ∀ (val : Fintype ι) (i j : ι),
  Eq.{u_1 + 1} (α := R)
    ((trace R M ∘ₗ dualTensorHom R M M : (a : Dual R M ⊗[R] M) → R)
        (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) (i, j) :
          Dual R M ⊗[R] M) :
      R)
    ((contractLeft R M : (a : Dual R M ⊗[R] M) → R)
        (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) (i, j) :
          Dual R M ⊗[R] M) :
      R)
Tactic: classical
    cases nonempty_fintype ι
    apply Basis.ext (Basis.tensorProduct (Basis.dualBasis b) b)
    rintro ⟨i, j⟩
    simp only [Function.comp_apply, Basis.tensorProduct_apply, Basis.coe_dualBasis, coe_comp]
    rw [trace_eq_matrix_trace R b, toMatrix_dualTensorHom]
    obtain rfl | hij := eq_or_ne i j
    · simp
    rw [Matrix.trace_single_eq_of_ne j i (1 : R) hij.symm]
    simp [hij]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
inst_3 : Finite ι
b : Basis ι R M
intro : ∀ (val : Fintype ι), Eq (α := Dual R M ⊗[R] M →ₗ[R] R) (trace R M ∘ₗ dualTensorHom R M M) (contractLeft R M)
intro₁ :
  ∀ (val : Fintype ι) (i : ι × ι),
    Eq.{u_1 + 1} (α := R)
      ((trace R M ∘ₗ dualTensorHom R M M : (a : Dual R M ⊗[R] M) → R)
          (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) i :
            Dual R M ⊗[R] M) :
        R)
      ((contractLeft R M : (a : Dual R M ⊗[R] M) → R)
          (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) i :
            Dual R M ⊗[R] M) :
        R)
intro₂ :
  ∀ (val : Fintype ι) (i j : ι),
    Eq.{u_1 + 1} (α := R)
      ((trace R M ∘ₗ dualTensorHom R M M : (a : Dual R M ⊗[R] M) → R)
          (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) (i, j) :
            Dual R M ⊗[R] M) :
        R)
      ((contractLeft R M : (a : Dual R M ⊗[R] M) → R)
          (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) (i, j) :
            Dual R M ⊗[R] M) :
        R)
⊢ Eq (α := Dual R M ⊗[R] M →ₗ[R] R) (trace R M ∘ₗ dualTensorHom R M M) (contractLeft R M)
have intro₃ : ∀ (val : Fintype ι) (i j : ι),
  Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        ((dualTensorHom R M M : (a : Dual R M ⊗[R] M) → M →ₗ[R] M) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j) : M →ₗ[R] M) :
      R)
    ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)
Tactic: classical
    cases nonempty_fintype ι
    apply Basis.ext (Basis.tensorProduct (Basis.dualBasis b) b)
    rintro ⟨i, j⟩
    simp only [Function.comp_apply, Basis.tensorProduct_apply, Basis.coe_dualBasis, coe_comp]
    rw [trace_eq_matrix_trace R b, toMatrix_dualTensorHom]
    obtain rfl | hij := eq_or_ne i j
    · simp
    rw [Matrix.trace_single_eq_of_ne j i (1 : R) hij.symm]
    simp [hij]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_5
inst_3 : Finite ι
b : Basis ι R M
intro : ∀ (val : Fintype ι), Eq (α := Dual R M ⊗[R] M →ₗ[R] R) (trace R M ∘ₗ dualTensorHom R M M) (contractLeft R M)
intro₁ :
  ∀ (val : Fintype ι) (i : ι × ι),
    Eq.{u_1 + 1} (α := R)
      ((trace R M ∘ₗ dualTensorHom R M M : (a : Dual R M ⊗[R] M) → R)
          (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) i :
            Dual R M ⊗[R] M) :
        R)
      ((contractLeft R M : (a : Dual R M ⊗[R] M) → R)
          (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) i :
            Dual R M ⊗[R] M) :
        R)
intro₂ :
  ∀ (val : Fintype ι) (i j : ι),
    Eq.{u_1 + 1} (α := R)
      ((trace R M ∘ₗ dualTensorHom R M M : (a : Dual R M ⊗[R] M) → R)
          (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) (i, j) :
            Dual R M ⊗[R] M) :
        R)
      ((contractLeft R M : (a : Dual R M ⊗[R] M) → R)
          (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) (i, j) :
            Dual R M ⊗[R] M) :
        R)
intro₃ :
  ∀ (val : Fintype ι) (i j : ι),
    Eq.{u_1 + 1} (α := R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          ((dualTensorHom R M M : (a : Dual R M ⊗[R] M) → M →ₗ[R] M) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j) :
            M →ₗ[R] M) :
        R)
      ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)
⊢ Eq (α := Dual R M ⊗[R] M →ₗ[R] R) (trace R M ∘ₗ dualTensorHom R M M) (contractLeft R M)
have intro₄ : ∀ (val : Fintype ι) (i j : ι),
  Eq.{u_1 + 1} (α := R) (Matrix.trace (Matrix.single j i 1) : R)
    ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)
Tactic: classical
    cases nonempty_fintype ι
    apply Basis.ext (Basis.tensorProduct (Basis.dualBasis b) b)
    rintro ⟨i, j⟩
    simp only [Function.comp_apply, Basis.tensorProduct_apply, Basis.coe_dualBasis, coe_comp]
    rw [trace_eq_matrix_trace R b, toMatrix_dualTensorHom]
    obtain rfl | hij := eq_or_ne i j
    · simp
    rw [Matrix.trace_single_eq_of_ne j i (1 : R) hij.symm]
    simp [hij]