matrix determinant lemma

Stream: Is there code for X?

[Yufei Liu]

Has the matrix determinant lemma been proved in LEAN yet?

[Eric Wieser]

Note that you can search for this on the #docs

[Eric Wieser]

The answer is no; the closest thing we have is docs#matrix.det_one_add_col_mul_row which is a special case of it

[Yufei Liu]

thank you so much
may i know is the mathlib regularly updated?

[Yufei Liu]

i plan to start a project on proving that in LEAN, but I'm just a beginner

[Eric Wieser]

I think a good proof to follow would be section 7.126 of http://www.cip.ifi.lmu.de/~grinberg/primes2015/sols.pdf

[Mauricio Collares]

Note that Eric linked to mathlib3 but at this point any new contributions should go to mathlib4. The easiest thing would be to wait a bit until port-status#linear_algebra/matrix/schur_complement is ported (or even help with the porting to get it done faster!), but you can also start working in lean3 then translate your additions to lean4.

[Eric Wieser]

I currently have a hold in place on that file due to a bunch of mathlib3 PRs, so please don't start porting it yet

[Mauricio Collares]

Good point, but there are 17 unported dependencies too

[Eric Wieser]

I think it's probably sensible for yufei to work on this in mathlib3/lean3

[Eric Wieser]

I just made #19117, which upstreams some lemmas that @MohanadAhmed and I wrote in another project, that may help with the determinant lemma.

[Eric Wieser]

Mauricio Collares said:

Good point, but there are 17 unported dependencies too

And another 12 in progress

[Mauricio Collares]

Yufei probably has a week then ;)

[Yufei Liu]

thank you two so much

[Notification Bot]

This topic was moved here from #lean4 > matrix determinant lemma by Eric Wieser.

[MohanadAhmed]

Hello isn't docs#matrix.det_one_add_mul_comm the one you mean?

[MohanadAhmed]

Oh OK the first matrix is not the identity.

[Kevin Buzzard]

Oh I think the first matrix is the identity. The issue is that there is no variable t, and over a general commutative ring a polynomial function is not determined by its values.

[MohanadAhmed]

If I understand from Wikipedia this applies only to invertible A matrix thus we can pull it out, By the determinant product rule, followed by repeated application of the docs#matrix.det_one_add_mul_comm we get the desired identity

[Kevin Buzzard]

There are no assumptions of invertibility in the mathlib assertion and hence there are no assumptions of invertibility necessary.

[MohanadAhmed]

Kevin Buzzard said:

There are no assumptions of invertibility in the mathlib assertion and hence there are no assumptions of invertibility necessary.

@Kevin Buzzard . I guess you are referring to proving $det(I - tAB) = det(I -tBA)$? From the other thread about Characteristic Power Series and Characeristic Polynomials?

[Kevin Buzzard]

I was referring to the theorem you linked to

[MohanadAhmed]

@yufei Liu asked above about the Matrix Determinant Lemma. At WIkipedia Matrix Determinant Lemma is stated as:
$\text{det}(A +UV^T) = \text{det}(I_m + V^TA^{-1}U)\text{det}(A)$. What I was suggesting is that Eric stated :

Eric Wieser said:

The answer is no; the closest thing we have is docs#matrix.det_one_add_col_mul_row which is a special case of it

I am suggesting the closest thing we have is docs#matrix.det_one_add_mul_comm. This can go as follows:

$det(A + UV^T) = det(A)det(I + A^{-1}UV^T) = det(A)det(I + V^TA^{-1}U)$. This would save @yufei Liu some steps.

[Eric Wieser]

@MohanadAhmed, the reason that I say that that is not the matrix determinant lemma is because it applies only when U/V are vectors

[Eric Wieser]

Nevermind, the statement isn't what I expected it to be

[MohanadAhmed]

Yes I agree. The other one docs# docs#matrix.det_one_add_mul_comm. applies to matrices

[Eric Wieser]

It seems I'm not totally imagining things; the version I expected is listed in the "generalizations" subheading

[MohanadAhmed]

The statement should look something like this:

lemma matrix_rank_lemma (A: matrix m m ℂ)(B: matrix n n ℂ)
  (U V: matrix m n ℂ):
  (A + U⬝Vᵀ).det = A.det * (1 + Vᵀ⬝(A⁻¹)⬝U).det := begin

end

[Eric Wieser]

I think you need A invertible for that to hold

[Eric Wieser]

i.e. try A = 0, U, V as 1x1 identity matrices, and you get 1 = 0 * 1

[MohanadAhmed]

Yes that is exactly the statement on Wikipedia I. E. A is invertible

[Eric Wieser]

The statement would also be (syntactically) more general if you replaced Vᵀ with V : matrix n m _

[MohanadAhmed]

Hello @yufei Liu
To add my two cents to the comments above, if you are only interested in the Matrix Determinant Lemma I think you can do it in Lean4/Mathlib4. It also makes sense to learn Lean4 since it is the new thing.

I just gave it a try and it took a couple of hours to get the missing lemmas in place. You do not need the whole schur_complement file. You only need the top seven lemmas

[MohanadAhmed]

If you want I can share the code with you if that will not spoil it for you

[Yufei Liu]

Please share the code, thank you so much

[Yufei Liu]

MohanadAhmed said:

yufei Liu asked above about the Matrix Determinant Lemma. At WIkipedia Matrix Determinant Lemma is stated as:
$\text{det}(A +UV^T) = \text{det}(I_m + V^TA^{-1}U)\text{det}(A)$. What I was suggesting is that Eric stated :

Eric Wieser said:

The answer is no; the closest thing we have is docs#matrix.det_one_add_col_mul_row which is a special case of it

I am suggesting the closest thing we have is docs#matrix.det_one_add_mul_comm. This can go as follows:

$det(A + UV^T) = det(A)det(I + A^{-1}UV^T) = det(A)det(I + V^TA^{-1}U)$. This would save yufei Liu some steps.

you are implying i can use docs#matrix.det_one_add_mul_comm to solve this right? $det(A)det(I + A^{-1}UV^T) = det(A)det(I + V^TA^{-1}U)$? but i didnt get how would this $det(A + UV^T) = det(A)det(I + A^{-1}UV^T)$ save me steps.

[Yufei Liu]

Hello @Eric Wieser @MohanadAhmed
I have a few more questions though regarding the things you were discussing:

1. So far ive only found the lean3 installation guide: lean3 guide, is there any detailed guide for me to start learn lean4?

2. is the docs you linked all lean3 library? is there similar thing for lean4?

3. I'm planning to do this as my final year project, probably titled as "formalising math in LEAN", which aims to formalise undergraduate level math (since im a math undergrad) in LEAN, hopefully those that are not in the mathlib yet. Matrix determinant lemma is just a topic where I think I can start with, probably i will try to prove more things that are not in the lean library. I understand the community is switching to LEAN4 and i would like to help, just considering im still a beginner in lean3 so not very confident at this moment. Considering my situation, do you think i should continue study lean3 or start learning lean4? Also, do you know any projects in the community that might suit me? Thank you!

[Yaël Dillies]

If you're interested in combinatorics, I will run informal summer projects revolving around github.com/YaelDillies/LeanCamCombi. I don't mind too much if they are in Lean 3 or Lean 4, but all my infrastructure is in Lean 3 and Lean 4 doesn't make any bit of the formalisation easier.

[MohanadAhmed]

The code in Lean 3 is below
You can place the cursor after every comma and look at the infoview in VSCode to see the steps of the derivation

Matrix Determinant Lemma Lean3 / Mathlib 3

import data.matrix.basic
import data.complex.basic
import linear_algebra.matrix.determinant
import linear_algebra.matrix.schur_complement
import data.polynomial.basic

open matrix
open_locale big_operators matrix

variables {m n q R: Type*}
variables [fintype m][fintype n][decidable_eq m][decidable_eq n]
variables [fintype q][decidable_eq q]
variables [field R]

lemma matrix_determinant_lemma (A: matrix m m R)(B: matrix n n R)
  (U: matrix m n R)(V: matrix  n m R) {hA: is_unit A.det}:
  (A + U⬝V).det = A.det * (1 + V⬝(A⁻¹)⬝U).det := begin
  nth_rewrite 0 ← matrix.mul_one A,
  rwa [← mul_nonsing_inv_cancel_left A (U⬝V), ← matrix.mul_add A,
    det_mul, ← matrix.mul_assoc, det_one_add_mul_comm, ← matrix.mul_assoc],
end

[MohanadAhmed]

yufei Liu said:

Hello Eric Wieser MohanadAhmed
I have a few more questions though regarding the things you were discussing:

1. So far ive only found the lean3 installation guide: lean3 guide, is there any detailed guide for me to start learn lean4?

2. is the docs you linked all lean3 library? is there similar thing for lean4?

3. I'm planning to do this as my final year project, probably titled as "formalising math in LEAN", which aims to formalise undergraduate level math (since im a math undergrad) in LEAN, hopefully those that are not in the mathlib yet. Matrix determinant lemma is just a topic where I think I can start with, probably i will try to prove more things that are not in the lean library. I understand the community is switching to LEAN4 and i would like to help, just considering im still a beginner in lean3 so not very confident at this moment. Considering my situation, do you think i should continue study lean3 or start learning lean4? Also, do you know any projects in the community that might suit me? Thank you!

For Question 1:

You need two things Lean4 and Mathlib4. The lean4 installation is described here (https://github.com/leanprover/lean4/blob/master/doc/quickstart.md)
To use Mathlib4 in a new project. The steps are in the Mathlib4 github landing page under Using mathlib4 as a dependency.

For Question 2:

The documentation is located here (https://leanprover-community.github.io/mathlib4_docs/)
For example the lemma about the determinant of the product of two matrices is the product of their determinants is called Matrix.det_mul and is located at docs4#Matrix.det_mul

[MohanadAhmed]

For Question 3:

Just so that you don't learn things twice, it is probably better to learn lean4. There are still stuff that are in Mathlib3 but missing in Mathlib4 particularly when you come to more "applied" type maths like matrices, for example. Which means if you work in mathlib4 there will be more work to do before you get to the part you "actually" want to do.

[MohanadAhmed]

For example to prove the Matrix Determinant Lemma above in LEAN4/Mathlib4 the code is shown below. You notice the proof for matrix determinant lemma "alone" is short but I had to translate 6 lemmas from mathlib3 to mathlib4. Once these are in place the matrix determinant lemma is just a few lines!
Working in mathlib4 you will be seeing a lot of this!! But that is part of the journey and the fun anyway!

Matrix Determinant Lemma Lean4 / Mathlib 4

import Mathlib
import Mathlib.Tactic.NthRewrite
import Mathlib.Tactic.SimpRw

variable (l m n: Type)
variable [Fintype l][Fintype m][Fintype n][DecidableEq m][DecidableEq n][DecidableEq l]


variable (R: Type)
variable [Field R][DecidableEq R]

namespace Matrix
open Matrix

/-- LDU decomposition of a block matrix with an invertible top-left corner, using the
Schur complement. -/
lemma from_blocks_eq_of_invertible₁₁
  (A : Matrix m m R) (B : Matrix m n R) (C : Matrix l m R) (D : Matrix l n R) [Invertible A] :
  fromBlocks A B C D =
    fromBlocks 1 0 (C⬝⅟A) 1 ⬝ fromBlocks A 0 0 (D - C⬝(⅟A)⬝B) ⬝ fromBlocks 1 (⅟A⬝B) 0 1 := by
  simp only [fromBlocks_multiply, Matrix.mul_zero, Matrix.zero_mul, add_zero, zero_add,
      Matrix.one_mul, Matrix.mul_one, Matrix.invOf_mul_self, Matrix.mul_invOf_self_assoc,
        Matrix.mul_invOf_mul_self_cancel, Matrix.mul_assoc, add_sub_cancel'_right]

/-- LDU decomposition of a block matrix with an invertible bottom-right corner, using the
Schur complement. -/
lemma from_blocks_eq_of_invertible₂₂
  (A : Matrix l m R) (B : Matrix l n R) (C : Matrix n m R) (D : Matrix n n R) [Invertible D] :
  fromBlocks A B C D =
    fromBlocks 1 (B⬝⅟D) 0 1 ⬝ fromBlocks (A - B⬝⅟D⬝C) 0 0 D ⬝ fromBlocks 1 0 (⅟D ⬝ C) 1 := by
  simp only [fromBlocks_multiply, Matrix.mul_zero, Matrix.zero_mul, add_zero, zero_add,
      Matrix.one_mul, Matrix.mul_one, Matrix.mul_invOf_self_assoc,
        Matrix.mul_invOf_mul_self_cancel, Matrix.mul_assoc, sub_add_cancel, Matrix.invOf_mul_self]

section det

lemma det_from_blocks₁₁ (A : Matrix m m R) (B : Matrix m n R) (C : Matrix n m R) (D : Matrix n n R)
  [Invertible A] : (Matrix.fromBlocks A B C D).det = det A * det (D - C ⬝ (⅟A) ⬝ B) := by
  rw [from_blocks_eq_of_invertible₁₁, det_mul, det_mul, det_fromBlocks_zero₂₁,
    det_fromBlocks_zero₂₁, det_fromBlocks_zero₁₂, det_one, det_one, one_mul, one_mul, mul_one]

@[simp] lemma det_from_blocks_one₁₁ (B : Matrix m n R) (C : Matrix n m R) (D : Matrix n n R) :
  (Matrix.fromBlocks 1 B C D).det = det (D - C ⬝ B) := by
  haveI : Invertible (1 : Matrix m m R) := invertibleOne
  rw [det_from_blocks₁₁, invOf_one, Matrix.mul_one, det_one, one_mul]

/-- Determinant of a 2×2 block matrix, expanded around an invertible bottom right element in terms
of the Schur complement. -/
lemma det_from_blocks₂₂ (A : Matrix m m R) (B : Matrix m n R) (C : Matrix n m R) (D : Matrix n n R)
  [Invertible D] : (Matrix.fromBlocks A B C D).det = det D * det (A - B ⬝ (⅟D) ⬝ C) := by
  have : fromBlocks A B C D = (fromBlocks D C B A).submatrix (Equiv.sumComm _ _) (Equiv.sumComm _ _) := by
    ext i j
    cases i;cases j; rfl; rfl
    cases j; rfl; rfl
  rw [this, Matrix.det_submatrix_equiv_self, det_from_blocks₁₁]

@[simp] lemma det_from_blocks_one₂₂ (A : Matrix m m R) (B : Matrix m n R) (C : Matrix n m R):
  (Matrix.fromBlocks A B C 1).det = det (A - B ⬝ C) := by
  haveI : Invertible (1 : Matrix n n R) := invertibleOne
  rw [det_from_blocks₂₂, invOf_one, Matrix.mul_one, det_one, one_mul]

lemma det_one_add_mul_comm(A : Matrix m n R) (B : Matrix n m R) :
  Matrix.det (1 + A ⬝ B) = Matrix.det (1 + B ⬝ A) := by
  calc  det (1 + A ⬝ B)
        = det (fromBlocks 1 (-A) B 1) := by rw [det_from_blocks_one₂₂, Matrix.neg_mul, sub_neg_eq_add]
     _  = det (1 + B ⬝ A)              := by rw [det_from_blocks_one₁₁, Matrix.mul_neg, sub_neg_eq_add]

lemma MatrixDeterminantLemma
  (A: Matrix m m R)(U: Matrix m n R)(V: Matrix n m R)(hA: IsUnit A.det):
  (A + U⬝V).det = A.det*(1 + V⬝(A⁻¹)⬝U).det := by
  nth_rewrite 1 [← Matrix.mul_one A]
  rwa [← Matrix.mul_nonsing_inv_cancel_left A (U⬝V), ←Matrix.mul_add, det_mul,
    ←Matrix.mul_assoc, det_one_add_mul_comm, ←Matrix.mul_assoc]

end det

[Kevin Buzzard]

It would not surprise me if all of mathlib 3 has been translated into lean 4 in around a month or so

[MohanadAhmed]

For Question 3: Project Suggestions

I don't know how much time you have for a final year project in your university. I will assume here it is two semesters (a full academic year) like it was during my undergrad years. Here are some random suggestions (more like a personal wishlist :grinning_face_with_smiling_eyes: ):

1. One area that is very lacking in both mathlib3 and mathlib4 is basic probability theory as taught in an introductory probability and staticsitcs course in engineering. Like definitions of basic distributions including gaussians, uniform, Poisson ... etc. Theorems like sum of a gaussian is a gaussian and so on. For the way the mathlib is structured this probably requires strong Measure Theory background.

2. Widgets. Take a look at this (https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Announcing.20ProofWidgets4). Maybe widgets for geometry proofs.

3. Linear Algebra Stuff: As far as I know the are still missing from mathlib (and mathlib4) (and probably many more):
   a. Singular Value Decomposition of matrices.
   b. Jordan Normal form Decomposition of Matrices
   c. Cholesky Decomposition of Positive Semidefinite matrices
   d. QR Decomposition
   e. Other matrix decomposition ... etc

[MohanadAhmed]

Also you can check with @Eric Wieser for his Matrix Cookbook Project. This is in lean3 however.

[Yufei Liu]

Thank you so much for your suggestions! I will do some background research about all the topics you have mentioned and probably get back to you and ask you more questions :rolling_on_the_floor_laughing: ,thank you for your patience

[Yufei Liu]

and yes, it is two semesters

[MohanadAhmed]

Note you can open the code above in the web playground (by the small arrow at the top of the code). You should see something like this

Animation.gif

[Yufei Liu]

thank you! im aware i can do this in VScode. But just out of curiosity, is this the online LEAN editor you are using? sometimes i feel like it takes a long time to load. And which one do you think is better? the online editor or the local one? Considering im starting a long term project

[Scott Morrison]

@yufei Liu, no they are using the new Lean 4 web editor, at https://lean.math.hhu.de/, while you linked to the old Lean 3 web editor.

[Scott Morrison]

@yufei Liu, no they are using the new Lean 4 web editor, at https://lean.math.hhu.de/, while you linked to the old Lean 3 web editor.

[Yufei Liu]

Noted, thank you

[Yufei Liu]

so lean 4 and lean 3 has not much difference in terms of syntax?

[MohanadAhmed]

Yufei Liu said:

Noted, thank you

They have enough differences to be annoying when moving from one to the other. There is also the naming of lemmas and theorems in mathlib, commas between statements vs white space, tactics tactic conventions .... etc etc etc

[Yufei Liu]

ic

[Yufei Liu]

im trying to display your lean 4 proof of matrix determinant lemma on vscode, and my supervisor suggest we create a shared project for us to both see it. Currently I have cloned a mathlib 4 and i am trying to creating a new lean file in the mathlib4 folder, but it is taking too long to load in the import mathlib stage.

So my question is,

1. is creating a new .lean file inside the mathlib a correct way of testing new lean stuff?

2. how do i create a shared project for me and my supervisor both work on it?

[Eric Wieser]

is creating a new .lean file inside the mathlib a correct way of testing new lean stuff?

This is a totally reasonable way to do things, but creating a separate project folder is also very sensible, especially if you intend to collaborate outside of mathlib

[Eric Wieser]

Currently I have cloned a mathlib 4 and i am trying to creating a new lean file in the mathlib4 folder, but it is taking too long to load in the import mathlib stage.

It sounds like you didn't run lake exe get cache first? If you have vscode open, you would do best to close it completely before running that command.

[Yufei Liu]

ok i will try that

[Yufei Liu]

mathlib4 % lake exe get cache
error: unknown executable get

i get an error message like above

[Damiano Testa]

lake exe cache get, swap get and cache.

[Yufei Liu]

it's working thanks

[Yufei Liu]

Does (hA: IsUnit A.det) mean A is invertible? how does the syntax work? why not (hA: IsUnit A)

[Yakov Pechersky]

It is a lemma that the two are equivalent. docs#Matrix.isUnit_iff_isUnit_det. As a proof obligation, it is easier to come up with a witness for the invertibility of a scalar than of a matrix.

[Eric Wieser]

Strictly speaking IsUnit A is more general as it doesn't need commutativity of the underlying ring

[Yufei Liu]

Yakov Pechersky said:

It is a lemma that the two are equivalent. docs#Matrix.isUnit_iff_isUnit_det. As a proof obligation, it is easier to come up with a witness for the invertibility of a scalar than of a matrix.

thanks for the reply. but how is invertibility of a scalar and invertibility of a matrix the same thing?

[Damiano Testa]

Yufei Liu, the two concepts are not the same, but the truth of one is equivalent to the truth of the other (as long as you assume that you are working over a commutative ring -- thanks Eric!).

The equivalence of the two requires a proof and you can look at lemma docs#Matrix.isUnit_iff_isUnit_det to see a proof.

[Yufei Liu]

thank you guys, i'll look it up

[MohanadAhmed]

Yufei Liu said:

Does (hA: IsUnit A.det) mean A is invertible? how does the syntax work? why not (hA: IsUnit A)

Yes IsUnit A.det means A is invertible. The lemma in mathlib is docs#Matrix.invertibleOfIsUnitDet.

[MohanadAhmed]

The other one with "similar" implication is docs#Matrix.invertibleOfDetInvertible

[MohanadAhmed]

Both these definitions take a matrix and a proof that the determinant is invertible (for the cases I know, it means determinant non-zero) and give you a proof that the matrix is invertible.

[MohanadAhmed]

Yufei Liu said:

Yakov Pechersky said:

It is a lemma that the two are equivalent. docs#Matrix.isUnit_iff_isUnit_det. As a proof obligation, it is easier to come up with a witness for the invertibility of a scalar than of a matrix.

thanks for the reply. but how is invertibility of a scalar and invertibility of a matrix the same thing?

If I understand your question correctly, you are asking why does the invertibility of the determinant imply the invertibility of the Matrix. Well because:

• for a scalar to be invertible it must be nonzero. docs#isUnit_iff_ne_zero
• A nonzero determinant implies invertibility of the matrix. ( I assume you know this from some Linear Algebra/Matrices course).

You can also walk this argument line backwards.

[Yufei Liu]

ah! this clears everything for me, thank you.

[Yufei Liu]

i am trying to formalize a more generalised matrix determinant lemma here:

/- A more generalization of the **Matrix determinant lemma** -/
theorem more_generalised_mdl {A : Matrix m m α} {W : Matrix n n α} (U : Matrix m n α)
    (V : Matrix n m α) (hA : IsUnit A.det) (hW : IsUnit W.det) :
    (A + U * W * V).det = W.det * A.det * (W⁻¹ + V * (A⁻¹) * U).det := by
    nth_rewrite 1 [← Matrix.mul_one A]
    rw [← Matrix.mul_nonsing_inv_cancel_left A (U * W * V), ←Matrix.mul_add, det_mul]
    nth_rewrite 1 [← Matrix.mul_one W⁻¹]
    rw [← Matrix.mul_nonsing_inv_cancel_left W⁻¹ (V * A⁻¹ * U), ←Matrix.mul_add, det_mul]
    rw [inv_inv]

but i met problem at the inv_inv part:

MDL123.lean:51:8
tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  ?a⁻¹⁻¹
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 m m α
W: Matrix n n α
U: Matrix m n α
V: Matrix n m α
hA: IsUnit (det A)
hW: IsUnit (det W)
⊢ det A * det (1 + A⁻¹ * (U * W * V)) = det W * det A * (det W⁻¹ * det (1 + W⁻¹⁻¹ * (V * A⁻¹ * U)))

how can i fix this?

[Scott Morrison]

Try dsimp before the rw, alternatively try erw.

[Scott Morrison]

(But these are suggestions out of ignorance about what the actual problem is --- they are "emergency measures"!)

[Yufei Liu]

Scott Morrison said:

Try dsimp before the rw, alternatively try erw.

sorry that seems do not work

[Ruben Van de Velde]

Then please make a #mwe

[Yufei Liu]

Ruben Van de Velde said:

Then please make a #mwe

My apology, here's the complete code

import Mathlib

variable {l m n α : Type*}

namespace Matrix

open scoped Matrix

section CommRing

variable [Fintype l] [Fintype m] [Fintype n]

variable [DecidableEq l] [DecidableEq m] [DecidableEq n]

variable [CommRing α]

/- A more generalization of the **Matrix determinant lemma** -/
theorem more_generalised_mdl {A : Matrix m m α} {W : Matrix n n α} (U : Matrix m n α)
    (V : Matrix n m α) (hA : IsUnit A.det) (hW : IsUnit W.det) :
    (A + U * W * V).det = W.det * A.det * (W⁻¹ + V * (A⁻¹) * U).det := by
    nth_rewrite 1 [← Matrix.mul_one A]
    rw [← Matrix.mul_nonsing_inv_cancel_left A (U * W * V), ←Matrix.mul_add, det_mul]
    nth_rewrite 1 [← Matrix.mul_one W⁻¹]
    rw [← Matrix.mul_nonsing_inv_cancel_left W⁻¹ (V * A⁻¹ * U), ←Matrix.mul_add, det_mul]
    rw [inv_inv]

my question is the inv_inv here doesnt work, what i want to do is change W⁻¹⁻¹ to W in the latest goal after the end of the second last line

[Eric Wieser]

You need rw [nonsing_inv_nonsing_inv]

[Eric Wieser]

docs#inv_inv is effectively for fields and groups, which matrices are not

[Yaël Dillies]

(that's not quite right, but the technical details are such that indeed inv_inv doesn't apply to matrices)

[Yufei Liu]

Eric Wieser said:

You need rw [nonsing_inv_nonsing_inv]

thank you that worked. btw is there any tricks for finding the lemma i want to use in mathlib? so far the method im using is guess the lemma name and search for it file by file in, for example, the Matrix folder

[Kevin Buzzard]

I've never done this before but @loogle (_⁻¹)⁻¹

[loogle]

:exclamation: <input>:1:33: expected term

[Kevin Buzzard]

@loogle (?a⁻¹)⁻¹

[Kevin Buzzard]

@loogle (?a⁻¹)⁻¹

[loogle]

Failure! Bot is unavailable

[Kevin Buzzard]

I'm pretty sure the answer is "you can use loogle if you know what you're doing" (and I don't, yet)

[Kevin Buzzard]

@loogle |- (?a⁻¹)⁻¹ = ?a

[loogle]

Failure! Bot is unavailable

[Mario Carneiro]

https://loogle.lean-fro.org/?q=%7C-+%28%3Fa%E2%81%BB%C2%B9%29%E2%81%BB%C2%B9+%3D+%3Fa has a more informative error message

[Mario Carneiro]

@Joachim Breitner

[Mario Carneiro]

(it's a timeout in isDefEq)

[Damiano Testa]

Joachim is the official loogler.

[Damiano Testa]

@loogle |- (?a⁻¹ : Matrix _ _ _)⁻¹ = ?a

[loogle]

:search: Matrix.inv_inv_inv, Matrix.inv_inv_of_invertible, and 1 more

[Yufei Liu]

oh wow that's impressive :big_smile:

[Yufei Liu]

thanks

[Kevin Buzzard]

(note that the 1 more is indeed nonsing_inv_nonsing_inv)

[Kevin Buzzard]

@loogle |- (?a⁻¹)⁻¹ = ?a

[loogle]

Failure! Bot is unavailable

[Kevin Buzzard]

So I'm generating too many lemmas here, or what?

[Kevin Buzzard]

I like the trick to restrict to matrices though, because the user knows they only care about matrices here.

[Damiano Testa]

Honestly, this might be the first time that I successfully loogled something!

[Joachim Breitner]

If you can guess parts of the name, you can make queries much faster:

[Joachim Breitner]

@loogle (?a⁻¹)⁻¹ = ?a, "Matrix"

[loogle]

:search: Matrix.inv_inv_inv, Matrix.inv_inv_of_invertible, and 1 more

[Joachim Breitner]

Or mention that you want lemmas involving the Matrix type anywhere:

[Joachim Breitner]

@loogle (?a⁻¹)⁻¹ = ?a, Matrix

[loogle]

Failure! Bot is unavailable

[Joachim Breitner]

Also, because the server is single-threaded, a query can timeout because someone else just runs a long query…
I can probably make it return a more helpful error message then…

[Yufei Liu]

I'm now working on formalising the matrix determinant lemma (the adjugate one without assuming A is invertible).

import Mathlib
import Mathlib.Data.Matrix.Invertible
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
import Mathlib.LinearAlgebra.Matrix.PosDef
import Mathlib.LinearAlgebra.Matrix.SchurComplement

variable {l m n α : Type*}

namespace Matrix

open scoped Matrix

section CommRing

variable [Fintype l] [Fintype m] [Fintype n]

variable [DecidableEq l] [DecidableEq m] [DecidableEq n]

variable [CommRing α]

theorem mdl_without_A_invertible (A : Matrix m m α) (u v : m → α):
    (A + col u * row v).det = A.det + v ⬝ᵥ (adjugate A).mulVec u := by
    sorry

And i currently has a hand written math proof like this:
mdl_math_proof.jpg

What is the likelihood of formalizing this proof in LEAN? Or is there a simpler proof?

[Anne Baanen]

Up to the usual difficulties of formalizing this seems quite doable. The first few steps with matrix and determinant manipulations would be: docs#Matrix.det_fromBlocks₂₂, docs#Matrix.det_updateRow_add, docs#Matrix.det_succ_row_zero. And from there results in Algebra.BigOperators should take you home.

[Anne Baanen]

Whether it's a good idea to follow this route also depends on your goals: do you want to contribute this to Mathlib?

[Eric Wieser]

Nice! I had in mind a proof that follows a similar strategy to how docs#Matrix.det_adjugate is proved, by going through a suitable polynomial

[Eric Wieser]

But I think that might be more work anyway

[Yufei Liu]

Anne Baanen said:

Whether it's a good idea to follow this route also depends on your goals: do you want to contribute this to Mathlib?

thank you for your reply, i already began contribute to mathlib, i will go check the lemmas you gave

[Yufei Liu]

Eric Wieser said:

Nice! I had in mind a proof that follows a similar strategy to how docs#Matrix.det_adjugate is proved, by going through a suitable polynomial

thank you, i'll check that out

[Yufei Liu]

my problem now is i never handled very element wise kind of proof before in LEAN, so my progress is slow

[Eric Wieser]

To be clear, I am not claiming that the polynomial proof is necessarily a good approach, and would be happy with your approach too!

[Yufei Liu]

Eric Wieser said:

To be clear, I am not claiming that the polynomial proof is necessarily a good approach, and would be happy with your approach too!

noted, thanks, this occurs to me only because the first step's lemma is already in LEAN :rolling_on_the_floor_laughing:

[Yufei Liu]

not sure if the rest are easy to be formalised or not, i mean my proof

[Yufei Liu]

i was trying to formalise the first step of my written proof.
Yufei Liu said:

And i currently has a hand written math proof like this:
mdl_math_proof.jpg

The difficulty is: the lemma i want to apply is all in matrix form:

theorem det_fromBlocks_one₁₁ (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) :
    (Matrix.fromBlocks 1 B C D).det = det (D - C * B) := by
  haveI : Invertible (1 : Matrix m m α) := invertibleOne
  rw [det_fromBlocks₁₁, invOf_one, Matrix.mul_one, det_one, one_mul]
#align matrix.det_from_blocks_one₁₁ Matrix.det_fromBlocks_one₁₁

But i want to apply it when B and C are defined as vector: col u and row v.
how do i turn a vector into matrix to apply the matrix lemmas on vectors?

[Yufei Liu]

i tried define then as U: Matrix 0 1 α, but even the variable declaration cannot work, what's wrong about thsi?

[Eric Wieser]

col u is a matrix when u is a vector

[Eric Wieser]

docs#Matrix.col

[Yufei Liu]

oh i see let me try

[Yufei Liu]

regarding the issue of formalising the matrix determinant lemma (the adjugate one without assuming A is invertible)
im currently stuck here:

import Mathlib
import Mathlib.Data.Matrix.Invertible
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
import Mathlib.LinearAlgebra.Matrix.PosDef
import Mathlib.LinearAlgebra.Matrix.SchurComplement

variable {l m n α : Type*}

namespace Matrix

open scoped Matrix

open BigOperators

section CommRing

variable [Fintype l] [Fintype m] [Fintype n]

variable [DecidableEq l] [DecidableEq m] [DecidableEq n]

variable [CommRing α]

theorem expand_block (A : Matrix m m α) (u v : m → α):
    (fromBlocks 1 (row v) (-col u) A).det = A.det + (fromBlocks 0 (row v) (-col u) A).det := by

theorem mdl_without_A_invertible (A : Matrix m m α) (u v : m → α):
    (A + col u * row v).det = A.det + v ⬝ᵥ (adjugate A).mulVec u := by
    have h1 :
      (A + col u * row v).det = (A - (- col u) * row v).det := by
        simp
    rw [h1]
    rw [← det_fromBlocks_one₁₁]
    sorry

so the main goal is to complete theorem mdl_without_A_invertible, and where i stuck is to try prove the subgoal of theorem expand_block. It'll involve element-wise matrix manipulation which im not familiar with. Can some one help me? thank you.

[Yufei Liu]

Yufei Liu said:

regarding the issue of formalising the matrix determinant lemma (the adjugate one without assuming A is invertible)
im currently stuck here:

import Mathlib
import Mathlib.Data.Matrix.Invertible
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
import Mathlib.LinearAlgebra.Matrix.PosDef
import Mathlib.LinearAlgebra.Matrix.SchurComplement

variable {l m n α : Type*}

namespace Matrix

open scoped Matrix

open BigOperators

section CommRing

variable [Fintype l] [Fintype m] [Fintype n]

variable [DecidableEq l] [DecidableEq m] [DecidableEq n]

variable [CommRing α]

theorem expand_block (A : Matrix m m α) (u v : m → α):
    (fromBlocks 1 (row v) (-col u) A).det = A.det + (fromBlocks 0 (row v) (-col u) A).det := by

theorem mdl_without_A_invertible (A : Matrix m m α) (u v : m → α):
    (A + col u * row v).det = A.det + v ⬝ᵥ (adjugate A).mulVec u := by
    have h1 :
      (A + col u * row v).det = (A - (- col u) * row v).det := by
        simp
    rw [h1]
    rw [← det_fromBlocks_one₁₁]
    sorry

so the main goal is to complete theorem mdl_without_A_invertible, and where i stuck is to try prove the subgoal of theorem expand_block. It'll involve element-wise matrix manipulation which im not familiar with. Can some one help me? thank you.

To phrase my question better: I was asking how to do cofactor expansion, especially on block matrix, and once expand this:

(fromBlocks 1 (row v) (-col u) A).det

i only need the first term: A.det be written so i can cancel it with the left hand side, the rest can be left expanded, since im going to expand them further anyway

[Eric Wieser]

I think we have a handful of lemmas with docs#Matrix.det_fromBlocks as a prefix; do any of them help?

[Eric Wieser]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/Matrix/SchurComplement.html#Matrix.det_fromBlocks_one%E2%82%81%E2%82%81 looks like the one

[Yufei Liu]

image.png
well the last step i was at is trying to convert (A - (- col u) * row v).det into block form so that i can isolate A.det out via expansion. I just want to know is there anyway i can do cofactor expansion on block matrix directly?

[Yufei Liu]

i've found the cofactor expansion lemma in mathlib that i want to apply:
docs#Matrix.det_succ_row_zero
, but due to syntax error i cannot rewrite this statement on my current goal properly.

i'm referring to the last line of the below code, where i want to apply cofactor expansion to a fromblock matrix

import Mathlib
import Mathlib.Data.Matrix.Invertible
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
import Mathlib.LinearAlgebra.Matrix.PosDef
import Mathlib.LinearAlgebra.Matrix.SchurComplement

universe z

open Equiv Equiv.Perm Finset Function

namespace Matrix

open Matrix BigOperators

variable {m n : Type*} [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m]

variable {R : Type z} [CommRing R]

/-- theorem i want to apply: -/

-- theorem det_succ_row_zero {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R) :
--     det A = ∑ j : Fin n.succ, (-1) ^ (j : ℕ) * A 0 j * det (A.submatrix Fin.succ j.succAbove)

theorem mdl_without_A_invertible (A : Matrix m m R) (u v : m → R):
    (A + col u * row v).det = A.det + v ⬝ᵥ (adjugate A).mulVec u := by
    have h1 :
      (A + col u * row v).det = (A - (- col u) * row v).det := by
        simp
    rw [h1]
    rw [← det_fromBlocks_one₁₁]
    sorry

theorem mdl_without_A_invertible_Fin? {m : ℕ} (A : Matrix (Fin m) (Fin m) R) (u v : (Fin m) → R):
    (A + col u * row v).det = A.det + v ⬝ᵥ (adjugate A).mulVec u := by
    have h1 :
      (A + col u * row v).det = (A - (- col u) * row v).det := by
        simp
    rw [h1]
    rw [← det_fromBlocks_one₁₁]
    rw [det_succ_row_zero fromBlocks 1 (row v) (-col u) A]

you can see there's two version of mdl_without_A_invertible here, one without specifying {m : ℕ} and one with.
the second one mdl_without_A_invertible_Fin? is my current goal and i modify it from my original mdl_without_A_invertible to match the variable setting of the lemma i want to apply: docs#Matrix.det_succ_row_zero

there are 2 questions i have:

1. why i cannot use (A : Matrix m m R) anymore when i specify {m : ℕ} ? i have to use (A : Matrix (Fin m) (Fin m) R) instead? what's the type theory logic here?

2. i notice that the fromblocks matrix has dimention @fromBlocks Unit (Fin m) Unit (Fin m) R 1 (row v) (-col u) A : Matrix (Unit ⊕ Fin m) (Unit ⊕ Fin m) R, but docs#Matrix.det_succ_row_zero has dimension A : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R
   is (Unit ⊕ Fin m) and Fin(m.succ) the same thing? i guess it's not and probably this type mismatch is why it cause a rewrite error. If so, how can i fix this?

[Ruben Van de Velde]

1. Matrices in mathlib are indexed by a type, like you declared in your first variable line. If you then say "no, m is instead a natural number", then you can no longer use it as an indexing type

[Anne Baanen]

is (Unit ⊕ Fin m) and Fin(m.succ) the same thing? i guess it's not and probably this type mismatch is why it cause a rewrite error. If so, how can i fix this?

They are indeed different types that happen to have the same number of elements. So you can make a bijection and then use docs#Matrix.reindex to change the indexing types. Let me figure out the best way to construct this bijection...

[Anne Baanen]

Let's go for something like this:

noncomputable def unitSumFinEquiv {m : ℕ} : Unit ⊕ Fin m ≃ Fin (m + 1) :=
  (Equiv.sumComm _ _).trans <|
  (Equiv.sumCongr (.refl _) (Fintype.equivFinOfCardEq rfl)).trans
  finSumFinEquiv

[Yufei Liu]

Anne Baanen said:

Let's go for something like this:

noncomputable def unitSumFinEquiv {m : ℕ} : Unit ⊕ Fin m ≃ Fin (m + 1) :=
  (Equiv.sumComm _ _).trans <|
  (Equiv.sumCongr (.refl _) (Fintype.equivFinOfCardEq rfl)).trans
  finSumFinEquiv

1. is this a definition or a proof of Unit ⊕ Fin m ≃ Fin (m + 1)? i see it's a def, but everything after the Unit ⊕ Fin m ≃ Fin (m + 1): is considered a proof of this def? or construction process using definition of Unit and Fin's original definition? that can be considered as a proof?
2. Since ive never seen such syntax before, and i dont understand a single part of this code after the colon. I just wonder is there any tutorial to help me understand this code?
3. still don't know how to apply reindex after i put your code in front of mine. basically i want to change this fromBlocks 1 v (-u) A 's (not even explicitly written in previous variable declaration since it's a byproduct of a rewrite tactic, it's on the left hand side of the most recent goal.) dimention from Unit ⊕ Fin m to Fin (m + 1). I've never altered a variable's setup before, can you teach me how to do that?

[Ruben Van de Velde]

≃ is a type, so you get definitions, not proofs

[Anne Baanen]

is this a definition or a proof of Unit ⊕ Fin m ≃ Fin (m + 1)? i see it's a def, but everything after the Unit ⊕ Fin m ≃ Fin (m + 1): is considered a proof of this def? or construction process using definition of Unit and Fin's original definition? that can be considered as a proof?

There may be less difference than you think! It's definitely a definition, since it gives a name (unitSumFinEquiv) to an object (whatever comes after the := sign). But you can say it is also a proof that Unit ⊕ Fin m and Fin (m + 1) are in bijection. And this proof consists of constructing the map. Ruben is right in the technical aspect, that for Lean's logic we have to use def instead of theorem.

[Anne Baanen]

Since ive never seen such syntax before, and i dont understand a single part of this code after the colon. I just wonder is there any tutorial to help me understand this code?

You are right that I used quite a few complicated Lean features. Here's an attempt at using nothing more than function application:

noncomputable def unitSumFinEquiv {m : ℕ} : Unit ⊕ Fin m ≃ Fin (m + 1) :=
  Equiv.trans (Equiv.sumComm _ _)
    (Equiv.trans (Equiv.sumCongr (Equiv.refl _) (Fintype.equivFinOfCardEq rfl))
      finSumFinEquiv)

[Anne Baanen]

The <| operator is basically a shortcut for parentheses: f x <| g y = ((f x) (g y)). (Equiv.sumComm _ _).trans is an abbreviation for Equiv.trans (Equiv.sumComm _ _), and .refl _ is a shortcut for Equiv.refl _.

[Anne Baanen]

I am sure this is explained much better in Functional Programming in Lean: #fpil

[Yufei Liu]

although i still cannot fully understand this because ive never done functional programming in lean bofore, but still thank you very much for the explanation. I think my current focus is on completing this proof, may i ask how can apply unitSumFinEquiv to my current goal?

import Mathlib
import Mathlib.Data.Matrix.Invertible
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
import Mathlib.LinearAlgebra.Matrix.PosDef
import Mathlib.LinearAlgebra.Matrix.SchurComplement

universe z

open Equiv Equiv.Perm Finset Function

namespace Matrix

open Matrix BigOperators

variable {m n : Type*} [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m]

variable {R : Type z} [CommRing R]

noncomputable def unitSumFinEquiv {m : ℕ} : Unit ⊕ Fin m ≃ Fin (m + 1) :=
  (Equiv.sumComm _ _).trans <|
  (Equiv.sumCongr (.refl _) (Fintype.equivFinOfCardEq rfl)).trans
  finSumFinEquiv

theorem mdl_without_A_invertible_Fin {m : ℕ} (A : Matrix (Fin m) (Fin m) R) (eₘ : Unit ⊕ Fin m ≃ Fin (m + 1))
(u: Matrix (Fin m) (Fin 1) R)(v: Matrix (Fin 1) (Fin m) R):
    (A + u * v).det = A.det + (v * (adjugate A) * u).det := by
    have h1 :
      (A + u * v).det = (A - - u * v).det := by
        simp
    rw [h1]
    rw [← det_fromBlocks_one₁₁]
    rw [det_fin_one]

/- how do i make the next line work? i know i need reindex but dont know how to apply.-/
    rw [det_succ_row_zero (fromBlocks 1 v (-u) A)]
    sorry

[Anne Baanen]

still don't know how to apply reindex after i put your code in front of mine. basically i want to change this fromBlocks 1 v (-u) A 's (not even explicitly written in previous variable declaration since it's a byproduct of a rewrite tactic, it's on the left hand side of the most recent goal.) dimention from Unit ⊕ Fin m to Fin (m + 1). I've never altered a variable's setup before, can you teach me how to do that?

You actually cannot change the type of a term! We will have the type fromBlocks 1 v (-u) A : Matrix (Unit ⊕ Fin m) (Unit ⊕ Fin m) R and never have the type fromBlocks 1 v (-u) A : Matrix (Fin (m+1)) (Fin (m+1)) R. But with reindex we can make a new term: Matrix.reindex (fromBlocks 1 v (-u) A) unitSumFinEquiv unitSumFinEquiv : Matrix (Fin (m+1)) (Fin (m+1)) R.

How do we get that term into your goal? Well, we can use rw, just like you used rw to introduce fromBlocks using det_fromBlocks_one₁₁:

import Mathlib

universe z

open Equiv Equiv.Perm Finset Function

namespace Matrix

open Matrix BigOperators

variable {m n : Type*} [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m]

variable {R : Type z} [CommRing R]

noncomputable def unitSumFinEquiv {m : ℕ} : Unit ⊕ Fin m ≃ Fin (m + 1) :=
  (Equiv.sumComm _ _).trans <|
  (Equiv.sumCongr (.refl _) (Fintype.equivFinOfCardEq rfl)).trans
  finSumFinEquiv

/-- theorem i want to apply: -/

-- theorem det_succ_row_zero {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R) :
--     det A = ∑ j : Fin n.succ, (-1) ^ (j : ℕ) * A 0 j * det (A.submatrix Fin.succ j.succAbove)

theorem mdl_without_A_invertible (A : Matrix m m R) (u v : m → R):
    (A + col u * row v).det = A.det + v ⬝ᵥ (adjugate A).mulVec u := by
    have h1 :
      (A + col u * row v).det = (A - (- col u) * row v).det := by
        simp
    rw [h1]
    rw [← det_fromBlocks_one₁₁]
    sorry

theorem mdl_without_A_invertible_Fin? {m : ℕ} (A : Matrix (Fin m) (Fin m) R) (u v : (Fin m) → R):
    (A + col u * row v).det = A.det + v ⬝ᵥ (adjugate A).mulVec u := by
  have h1 :
    (A + col u * row v).det = (A - (- col u) * row v).det := by
      simp
  have h2 : det (A - (- col u) * row v) =
    ∑ j : Fin (m + 1), (-1) ^ (j : ℕ) *
      reindex unitSumFinEquiv unitSumFinEquiv (fromBlocks 1 (row v) (-col u) A) 0 j *
      det (submatrix (reindex unitSumFinEquiv unitSumFinEquiv (fromBlocks 1 (row v) (-col u) A))
        Fin.succ (Fin.succAbove j)) := by
    rw [← det_fromBlocks_one₁₁, ← Matrix.det_reindex_self unitSumFinEquiv, det_succ_row_zero]
  rw [h1, h2]

[Eric Wieser]

As presumably was intended, you've sniped someone (me) into making a computable version:

def unitSumFinEquiv {m : ℕ} : Unit ⊕ Fin m ≃ Fin (m + 1) :=
  Equiv.sumComm _ _
    |>.trans <| Equiv.sumCongr (.refl _) (Equiv.equivPUnit _).symm
    |>.trans <| finSumFinEquiv

[Yufei Liu]

how do i split sum? that is to say express sum over set A+set B = sum over set A + sum over set B?

my goal is to solve h4, perhaps h3 can help? (or is h3 the right syntax?)

another question is because i use too much reindex unitSumFinEquiv unitSumFinEquiv (fromBlocks 1 (row v) (-col u) A) in my writing, i want to simplify it by giving it a new name, see def sub_mm. But apparently there's a syntax error. how to fix this?

import Mathlib

universe z

open Equiv Equiv.Perm Finset Function

namespace Matrix

open Matrix BigOperators

variable {m n : Type*} [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m]

variable {R : Type z} [CommRing R]

def unitSumFinEquiv {m : ℕ} : Unit ⊕ Fin m ≃ Fin (m + 1) :=
  Equiv.sumComm _ _
    |>.trans <| Equiv.sumCongr (.refl _) (Equiv.equivPUnit _).symm
    |>.trans <| finSumFinEquiv

def sub_mm {m : ℕ}{A : Matrix (Fin m) (Fin m) R}{u v : (Fin m) → R} Matrix (Fin (m + 1)) (Fin (m + 1)) α := reindex unitSumFinEquiv unitSumFinEquiv (fromBlocks 1 (row v) (-col u) A)


theorem mdl_without_A_invertible_Fin_3 {m : ℕ} (A : Matrix (Fin m) (Fin m) R) (u v : (Fin m) → R):
    (A + col u * row v).det = A.det + v ⬝ᵥ (adjugate A).mulVec u := by
  have h1 :
    (A + col u * row v).det = (A - (- col u) * row v).det := by
      simp
  have h2 : det (A - (- col u) * row v) =
    ∑ j : Fin (m + 1), (-1) ^ (j : ℕ) *
      reindex unitSumFinEquiv unitSumFinEquiv (fromBlocks 1 (row v) (-col u) A) 0 j *
      det (submatrix (reindex unitSumFinEquiv unitSumFinEquiv (fromBlocks 1 (row v) (-col u) A)) Fin.succ (Fin.succAbove j)) := by
    rw [← det_fromBlocks_one₁₁, ← Matrix.det_reindex_self unitSumFinEquiv, det_succ_row_zero]
  rw [h1, h2]

  /-Perhaps this h3 can help h4?-/
  have h3 : Fin (m + 1) = (Fin (1) ⊕ Ico 2 m) := by
    sorry

  /-seperate the first term of the summation:
  ∑ j : Fin (m + 1), (-1) ^ (j : ℕ) * blah =
  ∑ j : Fin (1), (-1) ^ (j : ℕ) * blah +   ∑ j : Fin (m), (-1) ^ (j+1 : ℕ) * blah-/
  have h4 : ∑ j : Fin (m + 1), (-1) ^ (j : ℕ) *
    reindex unitSumFinEquiv unitSumFinEquiv (fromBlocks 1 (row v) (-col u) A) 0 j *
      det (submatrix (reindex unitSumFinEquiv unitSumFinEquiv (fromBlocks 1 (row v) (-col u) A)) Fin.succ (Fin.succAbove j)) =
      ∑ j : Fin (1), (-1) ^ (j : ℕ) * reindex unitSumFinEquiv unitSumFinEquiv (fromBlocks 1 (row v) (-col u) A) 0 j *
      det (submatrix (reindex unitSumFinEquiv unitSumFinEquiv (fromBlocks 1 (row v) (-col u) A)) Fin.succ (Fin.succAbove j)) + ∑ j : Fin m, (-1) ^ (j+1 : ℕ) *
      reindex unitSumFinEquiv unitSumFinEquiv (fromBlocks 1 (row v) (-col u) A) 0 j *
      det (submatrix (reindex unitSumFinEquiv unitSumFinEquiv (fromBlocks 1 (row v) (-col u) A)) Fin.succ (Fin.succAbove j)) := by
    sorry

  have h5: ∑ j : Fin (1), (-1) ^ (j : ℕ) * reindex unitSumFinEquiv unitSumFinEquiv (fromBlocks 1 (row v) (-col u) A) 0 j *
      det (submatrix (reindex unitSumFinEquiv unitSumFinEquiv (fromBlocks 1 (row v) (-col u) A)) Fin.succ (Fin.succAbove j)) = reindex unitSumFinEquiv unitSumFinEquiv (fromBlocks 1 (row v) (-col u) A) 0 0 *
      det (submatrix (reindex unitSumFinEquiv unitSumFinEquiv (fromBlocks 1 (row v) (-col u) A)) Fin.succ (Fin.succAbove 0)) := by
      simp

[Ruben Van de Velde]

rw? seems to immediately find

rw [@Fin.sum_univ_add]

[Ruben Van de Velde]

Though

 rw [@Fin.sum_univ_succ]

might be nicer