awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n_1 : Type u_1
inst : Fintype n_1
n : Type u_1
inst_1 : Fintype n
inst_2 : DecidableEq n
S : Type u_2
inst_3 : CommRing S
inst_4 : LinearOrder S
inst_5 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ A i j < 0
h : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
h_sup : 0 < Finset.sup' Finset.univ ⋯ v
j₀ : n
h_j₀ : Finset.sup' Finset.univ ⋯ v = v j₀
rw : LE.le.{u_2} (α := S) (∑ i : n, v j₀ * A i j₀) (∑ i : n, v i * A i j₀)
⊢ LE.le.{u_2} (α := S) (∑ i : n, v j₀ * A i j₀) 0

Tactic:
rw [show 0 = ∑ i, v i * A i j₀ from (congrFun h_vA j₀).symm]

Premises used: congrFun, Eq.symm
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n_1 : Type u_1
inst : Fintype n_1
n : Type u_1
inst_1 : Fintype n
inst_2 : DecidableEq n
S : Type u_2
inst_3 : CommRing S
inst_4 : LinearOrder S
inst_5 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ A i j < 0
h : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
h_sup : 0 < Finset.sup' Finset.univ ⋯ v
j₀ : n
h_j₀ : Finset.sup' Finset.univ ⋯ v = v j₀
⊢ LE.le.{u_2} (α := S) (∑ i : n, v j₀ * A i j₀) (∑ i : n, v i * A i j₀)

Tactic:
Finset.sum_le_sum (fun i hi => ?_)

Premises used: Finset.sum_le_sum
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n_1 : Type u_1
inst : Fintype n_1
n : Type u_1
inst_1 : Fintype n
inst_2 : DecidableEq n
S : Type u_2
inst_3 : CommRing S
inst_4 : LinearOrder S
inst_5 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ A i j < 0
h : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
h_sup : 0 < Finset.sup' Finset.univ ⋯ v
j₀ : n
h_j₀ : Finset.sup' Finset.univ ⋯ v = v j₀
refine : ∀ (i : n) (hi : Membership.mem (γ := Finset n) Finset.univ i), v j₀ * A i j₀ ≤ v i * A i j₀
⊢ LE.le.{u_2} (α := S) (∑ i : n, v j₀ * A i j₀) (∑ i : n, v i * A i j₀)

Tactic:
refine Finset.sum_le_sum (fun i hi => ?_)

Premises used: Finset.sum_le_sum
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n_1 : Type u_1
inst : Fintype n_1
n : Type u_1
inst_1 : Fintype n
inst_2 : DecidableEq n
S : Type u_2
inst_3 : CommRing S
inst_4 : LinearOrder S
inst_5 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ A i j < 0
h : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
h_sup : 0 < Finset.sup' Finset.univ ⋯ v
j₀ : n
h_j₀ : Finset.sup' Finset.univ ⋯ v = v j₀
i : n
hi : Membership.mem (γ := Finset n) Finset.univ i
pos : ∀ (h : i = j₀), v j₀ * A i j₀ ≤ v i * A i j₀
neg : ∀ (h : ¬i = j₀), v j₀ * A i j₀ ≤ v i * A i j₀
⊢ v j₀ * A i j₀ ≤ v i * A i j₀

Tactic:
by_cases h : i = j₀
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n_1 : Type u_1
inst : Fintype n_1
n : Type u_1
inst_1 : Fintype n
inst_2 : DecidableEq n
S : Type u_2
inst_3 : CommRing S
inst_4 : LinearOrder S
inst_5 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ A i j < 0
h_1 : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
h_sup : 0 < Finset.sup' Finset.univ ⋯ v
j₀ : n
h_j₀ : Finset.sup' Finset.univ ⋯ v = v j₀
i : n
hi : Membership.mem (γ := Finset n) Finset.univ i
h : i = j₀
pos pos₁ : v j₀ * A j₀ j₀ ≤ v j₀ * A j₀ j₀
⊢ v j₀ * A i j₀ ≤ v i * A i j₀

Tactic:
rw [h]
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n_1 : Type u_1
inst : Fintype n_1
n : Type u_1
inst_1 : Fintype n
inst_2 : DecidableEq n
S : Type u_2
inst_3 : CommRing S
inst_4 : LinearOrder S
inst_5 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ A i j < 0
h_1 : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
h_sup : 0 < Finset.sup' Finset.univ ⋯ v
j₀ : n
h_j₀ : Finset.sup' Finset.univ ⋯ v = v j₀
i : n
hi : Membership.mem (γ := Finset n) Finset.univ i
h : ¬i = j₀
⊢ v j₀ * A i j₀ ≤ v i * A i j₀

Tactic:
(mul_le_mul_right_of_neg (h1 h)).mpr (h_j₀ ▸ Finset.le_sup' v hi)

Premises used: Iff.mpr, Eq.rec, mul_le_mul_right_of_neg, Finset.le_sup'
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n_1 : Type u_1
inst : Fintype n_1
n : Type u_1
inst_1 : Fintype n
inst_2 : DecidableEq n
S : Type u_2
inst_3 : CommRing S
inst_4 : LinearOrder S
inst_5 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ A i j < 0
h_1 : Nonempty n
h2 : A.det = 0
v : n → S
h_vnz : v ≠ 0
h_vA : v ᵥ* A = 0
h_sup : 0 < Finset.sup' Finset.univ ⋯ v
j₀ : n
h_j₀ : Finset.sup' Finset.univ ⋯ v = v j₀
i : n
hi : Membership.mem (γ := Finset n) Finset.univ i
h : ¬i = j₀
⊢ v j₀ * A i j₀ ≤ v i * A i j₀

Tactic:
exact (mul_le_mul_right_of_neg (h1 h)).mpr (h_j₀ ▸ Finset.le_sup' v hi)

Premises used: Iff.mpr, mul_le_mul_right_of_neg
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
S : Type u_2
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ A i j < 0
h2 : ∀ (i : n), LT.lt.{u_2} (α := S) 0 (∑ j : n, A i j)
rw : Aᵀ.det ≠ 0
⊢ A.det ≠ 0

Tactic:
rw [← Matrix.det_transpose]

Premises used: Matrix.det_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
S : Type u_2
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ A i j < 0
h2 : ∀ (i : n), LT.lt.{u_2} (α := S) 0 (∑ j : n, A i j)
⊢ Aᵀ.det ≠ 0

Tactic:
det_ne_zero_of_sum_col_pos ?_ ?_

Premises used: Matrix.det_ne_zero_of_sum_col_pos
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
S : Type u_2
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ A i j < 0
h2 : ∀ (i : n), LT.lt.{u_2} (α := S) 0 (∑ j : n, A i j)
refine_1 : Pairwise fun (i j : n) ↦ Aᵀ i j < 0
refine_2 : ∀ (j : n), LT.lt.{u_2} (α := S) 0 (∑ i : n, Aᵀ i j)
⊢ Aᵀ.det ≠ 0

Tactic:
refine det_ne_zero_of_sum_col_pos ?_ ?_

Premises used: Matrix.det_ne_zero_of_sum_col_pos
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
S : Type u_2
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ A i j < 0
h2 : ∀ (i : n), LT.lt.{u_2} (α := S) 0 (∑ j : n, A i j)
refine_1 : Pairwise fun (i j : n) ↦ A j i < 0
⊢ Pairwise fun (i j : n) ↦ Aᵀ i j < 0

Tactic:
simp_rw [Matrix.transpose_apply]

Premises used: Matrix.transpose_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
S : Type u_2
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ A i j < 0
h2 : ∀ (i : n), LT.lt.{u_2} (α := S) 0 (∑ j : n, A i j)
⊢ Pairwise fun (i j : n) ↦ A j i < 0

Tactic:
fun i j h => h1 h.symm

Premises used: Ne.symm, Pairwise
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
S : Type u_2
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ A i j < 0
h2 : ∀ (i : n), LT.lt.{u_2} (α := S) 0 (∑ j : n, A i j)
⊢ Pairwise fun (i j : n) ↦ A j i < 0

Tactic:
exact fun i j h => h1 h.symm
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
S : Type u_2
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ A i j < 0
h2 refine_2 : ∀ (j : n), LT.lt.{u_2} (α := S) 0 (∑ x : n, A j x)
⊢ ∀ (j : n), LT.lt.{u_2} (α := S) 0 (∑ i : n, Aᵀ i j)

Tactic:
simp_rw [Matrix.transpose_apply]

Premises used: Matrix.transpose_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
S : Type u_2
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ A i j < 0
h2 : ∀ (i : n), LT.lt.{u_2} (α := S) 0 (∑ j : n, A i j)
⊢ ∀ (j : n), LT.lt.{u_2} (α := S) 0 (∑ x : n, A j x)

Tactic:
h2
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
S : Type u_2
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ A i j < 0
h2 : ∀ (i : n), LT.lt.{u_2} (α := S) 0 (∑ j : n, A i j)
⊢ ∀ (j : n), LT.lt.{u_2} (α := S) 0 (∑ x : n, A j x)

Tactic:
exact h2
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
R : Type u_6
inst : AddCommMonoid R
o : Type u_8
inst_1 : Fintype o
inst_2 : DecidableEq o
d : o → R
⊢ (diagonal d).trace = ∑ i : o, d i

Tactic:
simp only [trace, diag_apply, diagonal_apply_eq]

Premises used: Matrix.diagonal_apply_eq, Matrix.trace, Matrix.diag_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
n : Type u_3
R : Type u_6
inst : Fintype n
inst_1 : AddCommMonoid R
⊢ Eq.{u_6 + 1} (α := R) (trace.{u_3, u_6} (n := n) 0) 0

Tactic:
(Finset.sum_const (0 : R)).trans <| smul_zero _

Premises used: Matrix.diag, smul_zero, Matrix.trace, OfNat.ofNat, Eq.trans, Finset.sum_const
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
n : Type u_3
R : Type u_6
inst : Fintype n
inst_1 : AddCommMonoid R
inst_2 : IsEmpty n
A : Matrix n n R
⊢ A.trace = 0

Tactic:
simp [trace]

Premises used: Matrix.trace
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
n : Type u_3
R : Type u_6
inst : Fintype n
inst_1 : AddCommMonoid R
A B : Matrix n n R
⊢ (A + B).trace = A.trace + B.trace

Tactic:
Finset.sum_add_distrib

Premises used: Matrix.diag, Finset.sum_add_distrib, Matrix.trace
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
n : Type u_3
α : Type u_5
R : Type u_6
inst : Fintype n
inst_1 : AddCommMonoid R
inst_2 : DistribSMul α R
r : α
A : Matrix n n R
⊢ (r • A).trace = r • A.trace

Tactic:
Finset.smul_sum.symm

Premises used: Matrix.diag, Matrix.trace, Finset.smul_sum, Eq.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
n : Type u_3
R : Type u_6
inst : Fintype n
inst_1 : AddCommMonoid R
A : Matrix n n R
⊢ Aᵀ.trace = A.trace

Tactic:
rfl

Premises used: Matrix.diag, Matrix.trace, Matrix.transpose, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
n : Type u_3
R : Type u_6
inst : Fintype n
inst_1 : AddCommMonoid R
inst_2 : StarAddMonoid R
A : Matrix n n R
⊢ Aᴴ.trace = star A.trace

Tactic:
(star_sum _ _).symm

Premises used: Matrix.diag, Matrix.trace, star_sum, Matrix.transpose, Matrix.map, Eq.symm, Matrix.conjTranspose
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
n : Type u_3
R : Type u_6
inst : Fintype n
inst_1 : AddCommMonoid R
l : List (Matrix n n R)
⊢ l.sum.trace = (List.map trace l).sum

Tactic:
map_list_sum (traceAddMonoidHom n R) l

Premises used: Multiset.sum, Matrix.diag, Multiset.foldr, Matrix.trace, map_list_sum, Finset.sum, Matrix.traceAddMonoidHom
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
n : Type u_3
R : Type u_6
inst : Fintype n
inst_1 : AddCommMonoid R
s : Multiset (Matrix n n R)
⊢ s.sum.trace = (Multiset.map trace s).sum

Tactic:
map_multiset_sum (traceAddMonoidHom n R) s

Premises used: Multiset.sum, map_multiset_sum, Multiset.foldr, Matrix.trace, Finset.sum, Matrix.traceAddMonoidHom
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
ι : Type u_1
n : Type u_3
R : Type u_6
inst : Fintype n
inst_1 : AddCommMonoid R
s : Finset ι
f : ι → Matrix n n R
⊢ Eq.{u_6 + 1} (α := R) (trace.{u_3, u_6} (n := n) (∑ i ∈ s, f i)) (∑ i ∈ s, (f i).trace)

Tactic:
map_sum (traceAddMonoidHom n R) f s

Premises used: Multiset.sum, Matrix.diag, Multiset.foldr, Matrix.trace, map_sum, Finset.sum, Matrix.traceAddMonoidHom
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
n : Type u_3
R : Type u_6
S : Type u_7
inst : Fintype n
inst_1 : AddCommMonoid R
inst_2 : AddCommMonoid S
F : Type u_8
inst_3 : FunLike F R S
inst_4 : AddMonoidHomClass F R S
f : F
A : Matrix n n R
⊢ Eq.{u_7 + 1} (α := S) ((f : (a : R) → S) A.trace : S) (trace (A.map (⇑f : (a : R) → S)) : S)

Tactic:
map_sum f (fun i => diag A i) Finset.univ

Premises used: Matrix.diag, Finset.univ, Matrix.trace, map_sum, Matrix.map
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
n : Type u_3
p : Type u_4
R : Type u_6
inst : Fintype n
inst_1 : Fintype p
inst_2 : AddCommMonoid R
inst_3 : DecidableEq p
M : p → Matrix n n R
⊢ (blockDiagonal M).trace = ∑ i : p, (M i).trace

Tactic:
simp [blockDiagonal, trace, Finset.sum_comm (γ := n), Fintype.sum_prod_type]

Premises used: Matrix.blockDiagonal, Matrix.trace, Finset.sum_comm, Fintype.sum_prod_type
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
p : Type u_4
R : Type u_6
inst : Fintype p
inst_1 : AddCommMonoid R
inst_2 : DecidableEq p
m : p → Type u_8
inst_3 : (i : p) → Fintype (m i)
M : (i : p) → Matrix.{u_8, u_8, u_6} (m i) (m i) R
⊢ (blockDiagonal' (m' := m) (n' := m) M).trace = ∑ i : p, (M i).trace

Tactic:
simp [blockDiagonal', trace, Finset.sum_sigma']

Premises used: Matrix.trace, Finset.sum_sigma', Matrix.blockDiagonal'
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
n : Type u_3
R : Type u_6
inst : Fintype n
inst_1 : AddCommGroup R
A B : Matrix n n R
⊢ (A - B).trace = A.trace - B.trace

Tactic:
Finset.sum_sub_distrib ..

Premises used: Matrix.diag, Matrix.trace, Finset.sum_sub_distrib
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
n : Type u_3
R : Type u_6
inst : Fintype n
inst_1 : AddCommGroup R
A : Matrix n n R
⊢ (-A).trace = -A.trace

Tactic:
Finset.sum_neg_distrib ..

Premises used: Matrix.diag, Matrix.trace, Finset.sum_neg_distrib
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
n : Type u_3
R : Type u_6
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : AddCommMonoidWithOne R
simp_rw : Eq.{u_6 + 1} (α := R) (∑ i : n, diag 1 i) (↑(Fintype.card n) : R)
simp_rw₁ : Eq.{u_6 + 1} (α := R) (∑ x : n, 1 x) (↑(Fintype.card n) : R)
simp_rw₂ : Eq.{u_6 + 1} (α := R) (∑ x : n, 1) (↑(Fintype.card n) : R)
simp_rw₃ : HSMul.hSMul (β := R) (Finset.card.{u_3} (α := n) Finset.univ) 1 = (↑(Fintype.card n) : R)
simp_rw₄ : Eq.{u_6 + 1} (α := R) (↑(Finset.card.{u_3} (α := n) Finset.univ) : R) (↑(Fintype.card n) : R)
⊢ Eq.{u_6 + 1} (α := R) (trace.{u_3, u_6} (n := n) 1) (↑(Fintype.card n) : R)

Tactic:
simp_rw [trace, diag_one, Pi.one_def, Finset.sum_const, nsmul_one, Finset.card_univ]

Premises used: Finset.card_univ, Matrix.trace, Pi.one_def, Matrix.diag_one, nsmul_one, Finset.sum_const
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
m : Type u_2
n : Type u_3
R : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : AddCommMonoid R
inst_3 : Mul R
A : Matrix m n R
B : Matrix n m R
⊢ (Aᵀ * Bᵀ).trace = (A * B).trace

Tactic:
Finset.sum_comm

Premises used: Multiset.sum, Matrix.diag, Multiset.foldr, dotProduct, Matrix.trace, Matrix.transpose, Finset.sum_comm, Finset.sum
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
m : Type u_2
n : Type u_3
R : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : AddCommMonoid R
inst_3 : CommMagma R
A : Matrix m n R
B : Matrix n m R
rw : (A * B)ᵀ.trace = (B * A).trace
rw₁ : (A * B)ᵀ.trace = (Bᵀ * Aᵀ).trace
rw₂ rw₃ : (Bᵀ * Aᵀ).trace = (Bᵀ * Aᵀ).trace
⊢ (A * B).trace = (B * A).trace

Tactic:
rw [← trace_transpose, ← trace_transpose_mul, transpose_mul]

Premises used: Matrix.trace_transpose, Matrix.transpose_mul, Matrix.trace_transpose_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : Fintype p
inst_3 : NonUnitalCommSemiring R
A : Matrix m n R
B : Matrix n p R
C : Matrix p m R
rw : (C * (A * B)).trace = (C * A * B).trace
rw₁ rw₂ : (C * (A * B)).trace = (C * (A * B)).trace
⊢ (A * B * C).trace = (C * A * B).trace

Tactic:
rw [trace_mul_comm, Matrix.mul_assoc]

Premises used: Matrix.trace_mul_comm, Matrix.mul_assoc
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_6
inst : Fintype m
inst_1 : Fintype n
inst_2 : Fintype p
inst_3 : NonUnitalCommSemiring R
A : Matrix m n R
B : Matrix n p R
C : Matrix p m R
rw : (A * B * C).trace = (C * (A * B)).trace
rw₁ rw₂ : (C * (A * B)).trace = (C * (A * B)).trace
⊢ (A * (B * C)).trace = (C * (A * B)).trace

Tactic:
rw [← Matrix.mul_assoc, trace_mul_comm]

Premises used: Matrix.trace_mul_comm, Matrix.mul_assoc
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
n : Type u_3
R : Type u_6
inst : Fintype n
ι : Type u_8
inst_1 : Unique ι
inst_2 : NonUnitalNonAssocSemiring R
a b : n → R
apply :
  ∀ (x : n), Membership.mem (γ := Finset n) Finset.univ x → (replicateCol ι a * replicateRow ι b).diag x = a x * b x
⊢ (replicateCol ι a * replicateRow ι b).trace = a ⬝ᵥ b

Tactic:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
n : Type u_3
R : Type u_6
inst : Fintype n
ι : Type u_8
inst_1 : Unique ι
inst_2 : NonUnitalNonAssocSemiring R
a b : n → R
⊢ ∀ (x : n), Membership.mem (γ := Finset n) Finset.univ x → (replicateCol ι a * replicateRow ι b).diag x = a x * b x

Tactic:
simp [mul_apply]

Premises used: Matrix.mul_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
n : Type u_3
R : Type u_6
inst : Fintype n
inst_1 : NonUnitalNonAssocSemiring R
a b : n → R
rw : (replicateCol Unit a * replicateRow Unit b).trace = a ⬝ᵥ b
rw₁ rw₂ : a ⬝ᵥ b = a ⬝ᵥ b
⊢ (vecMulVec a b).trace = a ⬝ᵥ b

Tactic:
rw [vecMulVec_eq Unit, trace_replicateCol_mul_replicateRow]

Premises used: Matrix.vecMulVec_eq, Matrix.trace_replicateCol_mul_replicateRow, Unit
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
R : Type u_6
n : ℕ
inst : AddCommMonoid R
M : Matrix (Fin n.succ) (Fin n.succ) R
delta : M 0 0 + ∑ i : Fin n, (M.submatrix Fin.succ Fin.succ).diag i = ∑ i : Fin n.succ, M.diag i
⊢ M 0 0 + (M.submatrix Fin.succ Fin.succ).trace = M.trace

Tactic:
delta trace

Premises used: Matrix.trace
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
R : Type u_6
n : ℕ
inst : AddCommMonoid R
M : Matrix (Fin n.succ) (Fin n.succ) R
rw :
  M 0 0 + ∑ i : Fin n, (M.submatrix Fin.succ Fin.succ).diag i =
    ∑ i : Option (Fin n), M.diag (((finSuccEquiv n).symm : (a : Option (Fin n)) → Fin (n + 1)) i)
⊢ M 0 0 + ∑ i : Fin n, (M.submatrix Fin.succ Fin.succ).diag i = ∑ i : Fin n.succ, M.diag i

Tactic:
rw [← (finSuccEquiv n).symm.sum_comp]

Premises used: Equiv.sum_comp, finSuccEquiv, Equiv.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
R : Type u_6
n : ℕ
inst : AddCommMonoid R
M : Matrix (Fin n.succ) (Fin n.succ) R
⊢ M 0 0 + ∑ i : Fin n, (M.submatrix Fin.succ Fin.succ).diag i =
    ∑ i : Option (Fin n), M.diag (((finSuccEquiv n).symm : (a : Option (Fin n)) → Fin (n + 1)) i)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
m : Type u_2
R : Type u_6
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : CommSemiring R
M : (Matrix m m R)ˣ
N : Matrix m m R
rw : ((↑M⁻¹ : Matrix m m R) * (↑M : Matrix m m R) * N).trace = N.trace
rw₁ : (1 * N).trace = N.trace
rw₂ rw₃ : N.trace = N.trace
⊢ ((↑M : Matrix m m R) * N * (↑M⁻¹ : Matrix m m R)).trace = N.trace

Tactic:
rw [trace_mul_cycle, Units.inv_mul, one_mul]

Premises used: Units.inv_mul, Matrix.trace_mul_cycle, one_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
m : Type u_2
R : Type u_6
inst : Fintype m
inst_1 : DecidableEq m
inst_2 : CommSemiring R
M : (Matrix m m R)ˣ
N : Matrix m m R
⊢ ((↑M⁻¹ : Matrix m m R) * N * (↑M : Matrix m m R)).trace = N.trace

Tactic:
trace_units_conj M⁻¹ N

Premises used: Matrix.trace_units_conj, Inv.inv
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
R : Type u_6
inst : AddCommMonoid R
A : Matrix (Fin 0) (Fin 0) R
⊢ A.trace = 0

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Matrix.trace, List.foldr, Finset.sum, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
R : Type u_6
inst : AddCommMonoid R
A : Matrix (Fin 1) (Fin 1) R
⊢ A.trace = A 0 0

Tactic:
add_zero _

Premises used: Multiset.sum, Matrix.diag, Multiset.foldr, Fin.ofNat, Matrix.trace, add_zero, List.foldr, Finset.sum
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
R : Type u_6
inst : AddCommMonoid R
A : Matrix (Fin 2) (Fin 2) R
⊢ A.trace = A 0 0 + A 1 1

Tactic:
congr_arg (_ + ·) (add_zero (A 1 1))

Premises used: Multiset.sum, Matrix.diag, Multiset.foldr, Fin.ofNat, Matrix.trace, congr_arg, HAdd.hAdd, add_zero, OfNat.ofNat, List.foldr, Finset.sum
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
R : Type u_6
inst : AddCommMonoid R
A : Matrix (Fin 3) (Fin 3) R
rw : A.trace = A 0 0 + (A 1 1 + (A 2 2 + 0))
⊢ A.trace = A 0 0 + A 1 1 + A 2 2

Tactic:
rw [← add_zero (A 2 2), add_assoc]

Premises used: add_assoc, add_zero, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
R : Type u_6
inst : AddCommMonoid R
A : Matrix (Fin 3) (Fin 3) R
⊢ A.trace = A 0 0 + (A 1 1 + (A 2 2 + 0))

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
R : Type u_6
inst : AddCommMonoid R
a : R
⊢ trace (n := Fin 1) !![a] = a

Tactic:
trace_fin_one _

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, Fin.induction, Matrix.trace_fin_one, Fin.cases, Matrix.vecCons
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
R : Type u_6
inst : AddCommMonoid R
a b c d : R
⊢ trace (n := Fin 2) !![a, b; c, d] = a + d

Tactic:
trace_fin_two _

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, Matrix.trace_fin_two, Fin.induction, Fin.cases, Matrix.vecCons
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
R : Type u_6
inst : AddCommMonoid R
a b c d e f g h i : R
⊢ trace (n := Fin 3) !![a, b, c; d, e, f; g, h, i] = a + e + i

Tactic:
trace_fin_three _

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, Matrix.trace_fin_three, Fin.induction, Fin.cases, Matrix.vecCons
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
n : Type u_10
α : Type u_12
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : AddCommMonoid α
i j : n
c : α
h : i ≠ j
⊢ (single i j c).trace = 0

Tactic:
simp [trace, h]

Premises used: Matrix.trace
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
n : Type u_10
α : Type u_12
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : AddCommMonoid α
i : n
c : α
⊢ (single i i c).trace = c

Tactic:
simp [trace]

Premises used: Matrix.trace
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
m : Type u_9
n : Type u_10
R : Type u_11
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : Fintype m
i : n
j : m
a : R
x : Matrix m n R
⊢ (single i j a * x).trace = a • x j i

Tactic:
simp [trace, mul_apply, single, ite_and]

Premises used: Matrix.trace, Matrix.mul_apply, ite_and, Matrix.single
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
m : Type u_9
n : Type u_10
R : Type u_11
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Fintype n
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : Fintype m
x : Matrix m n R
i : n
j : m
a : R
⊢ (x * single i j a).trace = MulOpposite.op a • x j i

Tactic:
simp [trace, mul_apply, single, ite_and]

Premises used: Matrix.trace, Matrix.mul_apply, ite_and, Matrix.single
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
n : Type u_3
R : Type u_6
inst : Fintype n
inst_1 : AddCommMonoid R
inst_2 : Nonempty n
r : R
inhabit : ∀ (inhabited_h : Inhabited n), ∃ (a : Matrix n n R), a.trace = r
⊢ ∃ (a : Matrix n n R), a.trace = r

Tactic:
inhabit n
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
n : Type u_3
R : Type u_6
inst : Fintype n
inst_1 : AddCommMonoid R
inst_2 : Nonempty n
r : R
inhabited_h : Inhabited n
⊢ ∃ (a : Matrix n n R), a.trace = r

Tactic:
⟨single default default r, trace_single_eq_same default r⟩

Premises used: Inhabited.default, Matrix.trace_single_eq_same, Exists.intro, Matrix.single
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
n : Type u_3
R : Type u_6
inst : Fintype n
inst_1 : AddCommMonoid R
inst_2 : Nonempty n
r : R
inhabited_h : Inhabited n
⊢ ∃ (a : Matrix n n R), a.trace = r

Tactic:
exact ⟨single default default r, trace_single_eq_same default r⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Trace
Goal:
n : Type u_3
R : Type u_6
inst : Fintype n
inst_1 : AddCommMonoid R
inst_2 : Nonempty n
r : R
inhabit : ∀ (inhabited_h : Inhabited n), ∃ (a : Matrix n n R), a.trace = r
⊢ ∃ (a : Matrix n n R), a.trace = r

Tactic:
classical
  inhabit n
  exact ⟨single default default r, trace_single_eq_same default r⟩