mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A : Matrix n n α
B : Matrix n m α
inst✝ : Invertible A
⊢ ⅟A * (A * B) = B

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A : Matrix n n α
B : Matrix n m α
inst✝ : Invertible A
⊢ A * (⅟A * B) = B

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A : Matrix m n α
B : Matrix n n α
inst✝ : Invertible B
⊢ A * ⅟B * B = A

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A : Matrix m n α
B : Matrix n n α
inst✝ : Invertible B
⊢ A * B * ⅟B = A

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
T : Type uT
inst✝⁷ : CommRing T
inst✝⁶ : NoZeroDivisors T
inst✝⁵ : Algebra R T
inst✝⁴ : FaithfulSMul R T
P : Type uM
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g : M →ₗ[R] P
bc : IsBaseChange T g
⊢ Module.rank T P = Module.rank R M

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : ℕ
h : i < (listTransvecCol M).length
⊢ (listTransvecCol M)[i] = transvection (inl ⟨i, ⋯⟩) (inr ()) (-M (inl ⟨i, ⋯⟩) (inr ()) / M (inr ()) (inr ()))

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
⊢ (listTransvecRow M).length = r

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : ℕ
h : i < (listTransvecRow M).length
⊢ (listTransvecRow M)[i] = transvection (inr ()) (inl ⟨i, ⋯⟩) (-M (inr ()) (inl ⟨i, ⋯⟩) / M (inr ()) (inr ()))

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A B : Matrix n m α
C : Matrix n n α
inst✝ : Invertible C
⊢ ⅟C * A = B ↔ A = C * B

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i
⊢ n < (listTransvecCol M).length

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
this : LinearIndependent R fun i ↦ r * ↑s ^ ↑i
⊢ ↑n ≤ Module.rank R R

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A B : Matrix n m α
C : Matrix n n α
inst✝ : Invertible C
⊢ C * A = B ↔ A = ⅟C * B

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: α : Type w
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
⊢ A.adjugate = !![A 1 1, -A 0 1; -A 1 0, A 0 0]

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
this : ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
g : Fin n → R
hg : ∑ i, g i • (r * ↑s ^ ↑i) = 0
i : Fin n
⊢ ∑ i ∈ Finset.range n, (if h : i < n then g ⟨i, h⟩ else 0) • (r * ↑s ^ (i + 0)) = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A B : Matrix m n α
C : Matrix n n α
inst✝ : Invertible C
⊢ A * ⅟C = B ↔ A = B * C

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
this : ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
⊢ LinearIndependent R fun i ↦ r * ↑s ^ ↑i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : Semiring α
A B : Matrix m n α
C : Matrix n n α
inst✝ : Invertible C
⊢ A * C = B ↔ A = B * ⅟C

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : StarRing α
A : Matrix n n α
inst✝ : Invertible Aᴴ
⊢ Invertible A

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k : ℕ
hk : k ≤ r
⊢ ((List.drop k (listTransvecCol M)).prod * M) (inr ()) i = M (inr ()) i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring α
A : Matrix n n α
inst✝ : Invertible A
⊢ (⅟A)ᵀ * Aᵀ = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
⊢ ((listTransvecCol M).prod * M) (inr ()) i = M (inr ()) i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring α
A : Matrix n n α
inst✝ : Invertible A
⊢ Aᵀ * (⅟A)ᵀ = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: n : Type u_2
α : Type u_3
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommSemiring α
A : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible Aᵀ
⊢ (⅟A)ᵀ = ⅟Aᵀ

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
H : ∀ k ≤ r, ((List.drop k (listTransvecCol M)).prod * M) (inl i) (inr ()) = if k ≤ ↑i then 0 else M (inl i) (inr ())
⊢ ((listTransvecCol M).prod * M) (inl i) (inr ()) = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring α
A : Matrix n n α
inst✝ : Invertible Aᵀ
⊢ (⅟Aᵀ)ᵀ * A = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommSemiring α
A : Matrix n n α
inst✝ : Invertible Aᵀ
⊢ A * (⅟Aᵀ)ᵀ = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: n : Type u_2
α : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring α
A : Matrix n n α
⊢ IsUnit Aᵀ ↔ IsUnit A

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) = if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
⊢ n < (listTransvecCol M).length

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) = if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < (listTransvecCol M).length
n' : Fin r := ⟨n, hn⟩
⊢ (listTransvecCol M)[n] = transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ (A + U * C * V) * (⅟A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A) =
    A * ⅟A - A * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A + U * C * V * ⅟A -
      U * C * V * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
IH : ∀ (g : ℕ → R) (x : ℕ), ∑ i ∈ Finset.range n, g i • (r * ↑s ^ (i + x)) = 0 → ∀ i < n, g i = 0
g : ℕ → R
x i : ℕ
hin : i < n + 1
hg0 : ¬g 0 = 0
hg : (-∑ i ∈ Finset.range n, g (i + 1) * r * ↑s ^ i) * ↑s * ↑s ^ x = g 0 * r * ↑s ^ x
this : (-∑ i ∈ Finset.range n, g (i + 1) * r * ↑s ^ i) * ↑s = g 0 * r
⊢ g 0 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
hS : IsEmpty (OreLocalization.OreSet R⁰)
⊢ ℵ₀ ≤ Module.rank R R

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : IsDomain R
inst✝ : StrongRankCondition R
⊢ Nonempty (OreLocalization.OreSet R⁰)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ A * ⅟A - A * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A + U * C * V * ⅟A -
      U * C * V * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A =
    1 + U * C * V * ⅟A - (U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A + U * C * V * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) = if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < (listTransvecCol M).length
n' : Fin r := ⟨n, hn⟩
A : (listTransvecCol M)[n] = transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : n' = i
⊢ n = ↑i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: R : Type u_6
inst✝² : AddCommMonoid R
o : Type u_8
inst✝¹ : Fintype o
inst✝ : DecidableEq o
d : o → R
⊢ (diagonal d).trace = ∑ i, d i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: n : Type u_3
R : Type u_6
inst✝² : Fintype n
inst✝¹ : AddCommMonoid R
inst✝ : IsEmpty n
A : Matrix n n R
⊢ A.trace = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: n : Type u_3
p : Type u_4
R : Type u_6
inst✝³ : Fintype n
inst✝² : Fintype p
inst✝¹ : AddCommMonoid R
inst✝ : DecidableEq p
M : p → Matrix n n R
⊢ (blockDiagonal M).trace = ∑ i, (M i).trace

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: p : Type u_4
R : Type u_6
inst✝³ : Fintype p
inst✝² : AddCommMonoid R
inst✝¹ : DecidableEq p
m : p → Type u_8
inst✝ : (i : p) → Fintype (m i)
M : (i : p) → Matrix (m i) (m i) R
⊢ (blockDiagonal' M).trace = ∑ i, (M i).trace

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: n : Type u_3
R : Type u_6
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : AddCommMonoidWithOne R
⊢ trace 1 = ↑(Fintype.card n)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_6
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : AddCommMonoid R
inst✝ : CommMagma R
A : Matrix m n R
B : Matrix n m R
⊢ (A * B).trace = (B * A).trace

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_6
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype p
inst✝ : NonUnitalCommSemiring R
A : Matrix m n R
B : Matrix n p R
C : Matrix p m R
⊢ (A * B * C).trace = (C * A * B).trace

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_6
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype p
inst✝ : NonUnitalCommSemiring R
A : Matrix m n R
B : Matrix n p R
C : Matrix p m R
⊢ (A * (B * C)).trace = (C * (A * B)).trace

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: n : Type u_3
R : Type u_6
inst✝² : Fintype n
ι : Type u_8
inst✝¹ : Unique ι
inst✝ : NonUnitalNonAssocSemiring R
a b : n → R
⊢ (replicateCol ι a * replicateRow ι b).trace = a ⬝ᵥ b

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: n : Type u_3
R : Type u_6
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring R
a b : n → R
⊢ (vecMulVec a b).trace = a ⬝ᵥ b

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: R : Type u_6
n : ℕ
inst✝ : AddCommMonoid R
M : Matrix (Fin n.succ) (Fin n.succ) R
⊢ M 0 0 + (M.submatrix Fin.succ Fin.succ).trace = M.trace

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) = if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < (listTransvecCol M).length
n' : Fin r := ⟨n, hn⟩
A : (listTransvecCol M)[n] = transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
⊢ n ≠ ↑i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ 1 + U * C * V * ⅟A - (U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A + U * C * V * ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A) =
    1 + U * C * V * ⅟A - (U + U * C * V * ⅟A * U) * ⅟(⅟C + V * ⅟A * U) * V * ⅟A

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: m : Type u_2
R : Type u_6
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : CommSemiring R
M : (Matrix m m R)ˣ
N : Matrix m m R
⊢ (↑M * N * ↑M⁻¹).trace = N.trace

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: 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

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: n : Type u_10
α : Type u_12
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : AddCommMonoid α
i j : n
c : α
h : i ≠ j
⊢ (single i j c).trace = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: n : Type u_10
α : Type u_12
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : AddCommMonoid α
i : n
c : α
⊢ (single i i c).trace = c

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: m : Type u_9
n : Type u_10
R : Type u_11
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : Fintype m
i : n
j : m
a : R
x : Matrix m n R
⊢ (single i j a * x).trace = a • x j i

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: m : Type u_9
n : Type u_10
R : Type u_11
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : 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:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: n : Type u_3
R : Type u_6
inst✝² : Fintype n
inst✝¹ : AddCommMonoid R
inst✝ : Nonempty n
r : R
⊢ ∃ a, a.trace = r

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ 1 + U * C * V * ⅟A - (U + U * C * V * ⅟A * U) * ⅟(⅟C + V * ⅟A * U) * V * ⅟A =
    1 + U * C * V * ⅟A - U * C * (⅟C + V * ⅟A * U) * ⅟(⅟C + V * ⅟A * U) * V * ⅟A

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_6
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonAssocSemiring R
A B : Matrix m n R
⊢ A = B ↔ ∀ (x : Matrix n m R), (x * A).trace = (x * B).trace

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_6
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonAssocSemiring R
A B : Matrix m n R
⊢ A = B ↔ ∀ (x : Matrix n m R), (A * x).trace = (B * x).trace

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
i₁ : l
j₁ : m
i₂ : n
j₂ : p
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
a : α
b : β
⊢ kroneckerMap f (single i₁ j₁ a) (single i₂ j₂ b) = single (i₁, i₂) (j₁, j₂) (f a b)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : Zero γ
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
a : m → α
b : n → β
⊢ kroneckerMap f (diagonal a) (diagonal b) = diagonal fun mn ↦ f (a mn.1) (b mn.2)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : DecidableEq n
f : α → β → γ
hf : ∀ (a : α), f a 0 = 0
A : Matrix l m α
b : n → β
⊢ kroneckerMap f A (diagonal b) = blockDiagonal fun i ↦ A.map fun a ↦ f a (b i)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
inst✝² : Zero α
inst✝¹ : Zero γ
inst✝ : DecidableEq l
f : α → β → γ
hf : ∀ (b : β), f 0 b = 0
a : l → α
B : Matrix m n β
⊢ kroneckerMap f (diagonal a) B =
    (reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (blockDiagonal fun i ↦ B.map fun b ↦ f (a i) b)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝⁷ : Zero α
inst✝⁶ : Zero β
inst✝⁵ : Zero γ
inst✝⁴ : One α
inst✝³ : One β
inst✝² : One γ
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
f : α → β → γ
hf₁ : ∀ (b : β), f 0 b = 0
hf₂ : ∀ (a : α), f a 0 = 0
hf₃ : f 1 1 = 1
⊢ (diagonal fun mn ↦ f 1 1) = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
p : Type u_12
l' : Type u_15
m' : Type u_16
n' : Type u_17
p' : Type u_18
f : α → β → γ
el : l ≃ l'
em : m ≃ m'
en : n ≃ n'
ep : p ≃ p'
M : Matrix l m α
N : Matrix n p β
⊢ kroneckerMap f ((reindex el em) M) ((reindex en ep) N) =
    (reindex (el.prodCongr en) (em.prodCongr ep)) (kroneckerMap f M N)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ 1 + U * C * V * ⅟A - U * C * (⅟C + V * ⅟A * U) * ⅟(⅟C + V * ⅟A * U) * V * ⅟A = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ (A + U * C * V) * (⅟A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A) = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Kronecker

Goal state before:
pp: R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
l : Type u_9
m : Type u_10
n : Type u_11
l' : Type u_15
m' : Type u_16
n' : Type u_17
inst✝¹¹ : Semiring S
inst✝¹⁰ : Semiring R
inst✝⁹ : Fintype m
inst✝⁸ : Fintype m'
inst✝⁷ : NonUnitalNonAssocSemiring α
inst✝⁶ : NonUnitalNonAssocSemiring β
inst✝⁵ : NonUnitalNonAssocSemiring γ
inst✝⁴ : Module R α
inst✝³ : Module R γ
inst✝² : Module S β
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b'
A : Matrix l m α
B : Matrix m n α
A' : Matrix l' m' β
B' : Matrix m' n' β
⊢ ((kroneckerMapBilinear f) (A * B)) (A' * B') = ((kroneckerMapBilinear f) A) A' * ((kroneckerMapBilinear f) B) B'

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ (⅟A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A) * (A + U * C * V) =
    ⅟A * A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A * A + ⅟A * U * C * V -
      ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A * U * C * V

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ A.adjugate =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
      -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
      A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]

Tactic:
by

Goal state after: