mathlib-initiative/mathlib-tactics huggingface dataset:
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:
simpa using

Goal state after:
𝕜 : 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 < r
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
h : ∀ (x : Matrix n m R), (x * A).trace = (x * B).trace
i : m
j : n
⊢ A i j = B i j

Tactic:
simpa using

Goal state after:
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
h : ∀ (x : Matrix n m R), (x * A).trace = (x * B).trace
i : m
j : n
⊢ A i j = B i j
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
h : ∀ (x : Matrix n m R), (A * x).trace = (B * x).trace
i : m
j : n
⊢ A i j = B i j

Tactic:
simpa using

Goal state after:
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
h : ∀ (x : Matrix n m R), (A * x).trace = (B * x).trace
i : m
j : n
⊢ A i j = B i j
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
m : Type u_10
n : Type u_11
inst✝¹¹ : Semiring S
inst✝¹⁰ : Semiring R
inst✝⁹ : Fintype m
inst✝⁸ : Fintype n
inst✝⁷ : AddCommMonoid α
inst✝⁶ : AddCommMonoid β
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : Module R α
inst✝³ : Module R γ
inst✝² : Module S β
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
A : Matrix m m α
B : Matrix n n β
⊢ ∑ i, (((kroneckerMapBilinear f) A) B).diag i = (f (∑ i, A.diag i)) (∑ i, B.diag i)

Tactic:
Matrix.diag,

Goal state after:
R : Type u_1
S : Type u_2
α : Type u_3
β : Type u_5
γ : Type u_7
m : Type u_10
n : Type u_11
inst✝¹¹ : Semiring S
inst✝¹⁰ : Semiring R
inst✝⁹ : Fintype m
inst✝⁸ : Fintype n
inst✝⁷ : AddCommMonoid α
inst✝⁶ : AddCommMonoid β
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : Module R α
inst✝³ : Module R γ
inst✝² : Module S β
inst✝¹ : Module S γ
inst✝ : SMulCommClass S R γ
f : α →ₗ[R] β →ₗ[S] γ
A : Matrix m m α
B : Matrix n n β
⊢ ∑ i, ((kroneckerMapBilinear f) A) B i i = (f (∑ i, A i i)) (∑ i, B i i)
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i : n
this✝ : Nonempty n
n' : ℕ
hn' : Fintype.card n = n'.succ
x✝ : Trunc (n ≃ Fin n'.succ)
e : n ≃ Fin n'.succ
A' : Matrix (Fin n'.succ) (Fin n'.succ) α := (reindex e e) A
this : A.det = ∑ x, A (e.symm (e i)) (e.symm x) * A.adjugate (e.symm x) (e.symm (e i))
⊢ A.det = ∑ j, A i j * A.adjugate j i

Tactic:
← e.sum_comp,

Goal state after:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i : n
this✝ : Nonempty n
n' : ℕ
hn' : Fintype.card n = n'.succ
x✝ : Trunc (n ≃ Fin n'.succ)
e : n ≃ Fin n'.succ
A' : Matrix (Fin n'.succ) (Fin n'.succ) α := (reindex e e) A
this : A.det = ∑ i_1, A (e.symm (e i)) (e.symm (e i_1)) * A.adjugate (e.symm (e i_1)) (e.symm (e i))
⊢ A.det = ∑ j, A i j * A.adjugate j i
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case neg.inr.hnc
𝕜 : 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
hni : n ≠ ↑i
hi : ↑i < n + 1
⊢ ¬n ≤ ↑i

Tactic:
simpa using

Goal state after:
case neg.inr.hnc
𝕜 : 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
hni : n ≠ ↑i
hi : ↑i < n + 1
⊢ ↑i < n
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case neg.inr.hnc
𝕜 : 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
hni : n ≠ ↑i
hi : ↑i < n + 1
⊢ ¬n + 1 ≤ ↑i

Tactic:
simpa using

Goal state after:
case neg.inr.hnc
𝕜 : 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
hni : n ≠ ↑i
hi : ↑i < n + 1
⊢ ↑i < n + 1
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case self.hnc
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
⊢ ¬r ≤ ↑i

Tactic:
simpa using

Goal state after:
case self.hnc
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k : ℕ
⊢ ↑i < r
Module: Mathlib.LinearAlgebra.Matrix.Transvection

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

Tactic:
| self =>

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

Goal state before:
pp: case succ
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k : ℕ
IH : k ≤ r → (M * (List.take k (listTransvecRow M)).prod) i (inr ()) = M i (inr ())
hk : k + 1 ≤ r
⊢ (M * (List.take (k + 1) (listTransvecRow M)).prod) i (inr ()) = M i (inr ())

Tactic:
have hkr : k < r := hk

Goal state after:
case succ
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
k : ℕ
IH : k ≤ r → (M * (List.take k (listTransvecRow M)).prod) i (inr ()) = M i (inr ())
hk : k + 1 ≤ r
hkr : k < r
⊢ (M * (List.take (k + 1) (listTransvecRow M)).prod) i (inr ()) = M i (inr ())
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
A : (listTransvecRow M).length = r
⊢ (M * (List.take r (listTransvecRow M)).prod) i (inr ()) = M i (inr ())

Tactic:
simpa using

Goal state after:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
A : (listTransvecRow M).length = r
⊢ (M * (List.take r (listTransvecRow M)).prod) i (inr ()) = M i (inr ())
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : Invertible A
x✝¹ x✝ : Matrix n m α
h : (fun x ↦ A * x) x✝¹ = (fun x ↦ A * x) x✝
⊢ x✝¹ = x✝

Tactic:
simpa using

Goal state after:
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : Invertible A
x✝¹ x✝ : Matrix n m α
h : (fun x ↦ A * x) x✝¹ = (fun x ↦ A * x) x✝
⊢ x✝¹ = x✝
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : Invertible A
a x : Matrix m n α
hax : (fun x ↦ x * A) a = (fun x ↦ x * A) x
⊢ a = x

Tactic:
simpa using

Goal state after:
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : Invertible A
a x : Matrix m n α
hax : (fun x ↦ x * A) a = (fun x ↦ x * A) x
⊢ a = x
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : CommRing α
A : Matrix m n α
B : Matrix n m α
h : A * B = 1
x✝¹ x✝ : Matrix l m α
g : (fun x ↦ x * A) x✝¹ = (fun x ↦ x * A) x✝
⊢ x✝¹ = x✝

Tactic:
simpa using

Goal state after:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : CommRing α
A : Matrix m n α
B : Matrix n m α
h : A * B = 1
x✝¹ x✝ : Matrix l m α
g : (fun x ↦ x * A) x✝¹ = (fun x ↦ x * A) x✝
⊢ x✝¹ = x✝
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : CommRing α
A : Matrix m n α
B : Matrix n m α
h : A * B = 1
x✝¹ x✝ : Matrix m l α
g : (fun x ↦ B * x) x✝¹ = (fun x ↦ B * x) x✝
⊢ x✝¹ = x✝

Tactic:
simpa using

Goal state after:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : CommRing α
A : Matrix m n α
B : Matrix n m α
h : A * B = 1
x✝¹ x✝ : Matrix m l α
g : (fun x ↦ B * x) x✝¹ = (fun x ↦ B * x) x✝
⊢ x✝¹ = x✝
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
M N : Matrix m m R
b : m → α
inst✝¹ : LT α
inst✝ : AddGroup R
hM : M.BlockTriangular b
x✝ : (M + N).BlockTriangular b
⊢ N.BlockTriangular b

Tactic:
simpa using

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
M N : Matrix m m R
b : m → α
inst✝¹ : LT α
inst✝ : AddGroup R
hM : M.BlockTriangular b
x✝ : (M + N).BlockTriangular b
⊢ N.BlockTriangular b
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
M N : Matrix m m R
b : m → α
inst✝¹ : LT α
inst✝ : AddGroup R
hN : N.BlockTriangular b
x✝ : (M + N).BlockTriangular b
⊢ M.BlockTriangular b

Tactic:
simpa using

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
M N : Matrix m m R
b : m → α
inst✝¹ : LT α
inst✝ : AddGroup R
hN : N.BlockTriangular b
x✝ : (M + N).BlockTriangular b
⊢ M.BlockTriangular b
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
M N : Matrix m m R
b : m → α
inst✝¹ : LT α
inst✝ : AddGroup R
hM : M.BlockTriangular b
x✝ : (M - N).BlockTriangular b
⊢ N.BlockTriangular b

Tactic:
simpa using

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
M N : Matrix m m R
b : m → α
inst✝¹ : LT α
inst✝ : AddGroup R
hM : M.BlockTriangular b
x✝ : (M - N).BlockTriangular b
⊢ N.BlockTriangular b
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
M N : Matrix m m R
b : m → α
inst✝¹ : LT α
inst✝ : AddGroup R
hN : N.BlockTriangular b
x✝ : (M - N).BlockTriangular b
⊢ M.BlockTriangular b

Tactic:
simpa using

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
M N : Matrix m m R
b : m → α
inst✝¹ : LT α
inst✝ : AddGroup R
hN : N.BlockTriangular b
x✝ : (M - N).BlockTriangular b
⊢ M.BlockTriangular b
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0
⊢ ∀ (i : m), ¬¬p i → ∀ (j : m), ¬p j → M i j = 0

Tactic:
simpa using

Goal state after:
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0
⊢ ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0
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
this : listTransvecRow M = listTransvecRow ((listTransvecCol M).prod * M)
⊢ ((listTransvecCol M).prod * M) (inr ()) (inr ()) ≠ 0

Tactic:
simpa using

Goal state after:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
this : listTransvecRow M = listTransvecRow ((listTransvecCol M).prod * M)
⊢ ¬M (inr ()) (inr ()) = 0
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
this : listTransvecCol M = listTransvecCol (M * (listTransvecRow M).prod)
⊢ (M * (listTransvecRow M).prod) (inr ()) (inr ()) ≠ 0

Tactic:
simpa using

Goal state after:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
this : listTransvecCol M = listTransvecCol (M * (listTransvecRow M).prod)
⊢ ¬M (inr ()) (inr ()) = 0
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit A ↔ IsUnit B
⊢ A⁻¹ + B⁻¹ = A⁻¹ * (A + B) * B⁻¹

Tactic:
simpa using

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit A ↔ IsUnit B
⊢ A⁻¹ʳ + B⁻¹ʳ = A⁻¹ʳ * (A + B) * B⁻¹ʳ
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit A ↔ IsUnit B
⊢ A⁻¹ - B⁻¹ = A⁻¹ * (B - A) * B⁻¹

Tactic:
simpa using

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : IsUnit A ↔ IsUnit B
⊢ A⁻¹ʳ - B⁻¹ʳ = A⁻¹ʳ * (B - A) * B⁻¹ʳ
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: 𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : M.IsTwoBlockDiagonal
⊢ ((List.map toMatrix []).prod * M * (List.map toMatrix []).prod).IsTwoBlockDiagonal

Tactic:
simpa using

Goal state after:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
H : M.IsTwoBlockDiagonal
⊢ M.IsTwoBlockDiagonal
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case pos.inl
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), of (fun i j ↦ M (inl i) (inr j)) i j = 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), of (fun i j ↦ M (inr i) (inl j)) i j = 0 i j
i : Fin r
h : M (inl i) (inr ()) ≠ 0
⊢ ∃ L L', ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal

Tactic:
let M' := transvection (inr Unit.unit) (inl i) 1 * M

Goal state after:
case pos.inl
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), of (fun i j ↦ M (inl i) (inr j)) i j = 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), of (fun i j ↦ M (inr i) (inl j)) i j = 0 i j
i : Fin r
h : M (inl i) (inr ()) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := transvection (inr ()) (inl i) 1 * M
⊢ ∃ L L', ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case pos.inr
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), of (fun i j ↦ M (inl i) (inr j)) i j = 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), of (fun i j ↦ M (inr i) (inl j)) i j = 0 i j
i : Fin r
h : M (inr ()) (inl i) ≠ 0
⊢ ∃ L L', ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal

Tactic:
let M' := M * transvection (inl i) (inr unit) 1

Goal state after:
case pos.inr
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) = 0
H :
  (¬∀ (i : Fin r) (j : Unit), of (fun i j ↦ M (inl i) (inr j)) i j = 0 i j) ∨
    ¬∀ (i : Unit) (j : Fin r), of (fun i j ↦ M (inr i) (inl j)) i j = 0 i j
i : Fin r
h : M (inr ()) (inl i) ≠ 0
M' : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜 := M * transvection (inl i) (inr ()) 1
⊢ ∃ L L', ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i ↦ b i < k
h_sum : M⁻¹.toBlock p p * M.toBlock p p + (M⁻¹.toBlock p fun i ↦ ¬p i) * M.toBlock (fun i ↦ ¬p i) p = 1
i : { a // ¬p a }
j : { a // p a }
⊢ M.toBlock (fun i ↦ ¬p i) p i j = 0 i j

Tactic:
simpa using

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i ↦ b i < k
h_sum : M⁻¹.toBlock p p * M.toBlock p p + (M⁻¹.toBlock p fun i ↦ ¬p i) * M.toBlock (fun i ↦ ¬p i) p = 1
i : { a // ¬p a }
j : { a // p a }
⊢ M ↑i ↑j = 0
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i ↦ b i < k
h_sum : M⁻¹.toBlock p p * M.toBlock p p + (M⁻¹.toBlock p fun i ↦ ¬p i) * M.toBlock (fun i ↦ ¬p i) p = 1
h_zero : M.toBlock (fun i ↦ ¬p i) p = 0
⊢ ((M⁻¹.toBlock (fun i ↦ b i < k) fun i ↦ b i < k) * M.toBlock (fun i ↦ b i < k) fun i ↦ b i < k) = 1

Tactic:
simpa using

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i ↦ b i < k
h_sum : M⁻¹.toBlock p p * M.toBlock p p + (M⁻¹.toBlock p fun i ↦ ¬p i) * M.toBlock (fun i ↦ ¬p i) p = 1
h_zero : M.toBlock (fun i ↦ ¬p i) p = 0
⊢ ((M⁻¹.toBlock (fun i ↦ b i < k) fun i ↦ b i < k) * M.toBlock (fun i ↦ b i < k) fun i ↦ b i < k) = 1
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
R : Type v
A : Type u_8
M N : Matrix m m R
b : m → α
inst✝⁶ : CommRing R
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
⊢ (((⅟M).toBlock (fun i ↦ b i < k) fun i ↦ b i < k) * M.toBlock (fun i ↦ b i < k) fun i ↦ b i < k) = 1

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
R : Type v
A : Type u_8
M N : Matrix m m R
b : m → α
inst✝⁶ : CommRing R
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
⊢ ((M⁻¹.toBlock (fun i ↦ b i < k) fun i ↦ b i < k) * M.toBlock (fun i ↦ b i < k) fun i ↦ b i < k) = 1
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i ↦ b i < k
q : m → Prop := fun i ↦ ¬b i < k
h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0
i : { a // q a }
j : { a // p a }
⊢ M.toBlock q p i j = 0 i j

Tactic:
simpa using

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i ↦ b i < k
q : m → Prop := fun i ↦ ¬b i < k
h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0
i : { a // q a }
j : { a // p a }
⊢ M ↑i ↑j = 0
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i ↦ b i < k
q : m → Prop := fun i ↦ ¬b i < k
h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0
h_zero : M.toBlock q p = 0
⊢ M⁻¹.toBlock q p * M.toBlock p p = 0

Tactic:
simpa using

Goal state after:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i ↦ b i < k
q : m → Prop := fun i ↦ ¬b i < k
h_sum : M⁻¹.toBlock q p * M.toBlock p p + M⁻¹.toBlock q q * M.toBlock q p = 0
h_zero : M.toBlock q p = 0
⊢ M⁻¹.toBlock q p * M.toBlock p p = 0
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R[X]
r : R
⊢ eval ((scalar n) r) (matPolyEquiv M) = M.map (eval r)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R[X]
r : R
⊢ eval ((scalar n) r) (matPolyEquiv M) = M.map (eval r)
Module: Mathlib.RingTheory.MatrixPolynomialAlgebra

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R[X]
r : R
i j : n
⊢ eval ((scalar n) r) (matPolyEquiv M) i j = eval r (M i j)

Tactic:
matPolyEquiv_eval_eq_map,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R[X]
r : R
i j : n
⊢ M.map (eval r) i j = eval r (M i j)
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
m : Type u_3
inst✝¹ : DecidableEq m
inst✝ : Fintype m
M : Matrix m m R
t : R
i j : m
⊢ (evalRingHom t).mapMatrix ((scalar m) X - C.mapMatrix M) i j = ((scalar m) t - M) i j

Tactic:
obtain rfl | hij := eq_or_ne i j <;> simp [*]

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix l m α
B : Matrix l n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
⊢ (reindex (Equiv.sumComm l n) (Equiv.sumComm m n)) (fromBlocks A B C D) =
    (reindex (Equiv.sumComm l n) (Equiv.sumComm m n))
      (fromBlocks 1 (B * ⅟D) 0 1 * fromBlocks (A - B * ⅟D * C) 0 0 D * fromBlocks 1 0 (⅟D * C) 1)

Tactic:
simpa using

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁷ : Fintype l
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix l m α
B : Matrix l n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
⊢ fromBlocks D C B A = fromBlocks 1 0 (B * D⁻¹) 1 * fromBlocks D 0 0 (A - B * D⁻¹ * C) * fromBlocks 1 (D⁻¹ * C) 0 1