LinearAlgebra.Matrix.ToLin !4#3552

Stream: mathlib4

[Scott Morrison]

LinearAlgebra.Matrix.ToLin !4#3552 is now error-free, but I am sad about the porting notes about simp not working in places rw does. If anyone would like to look at this (whether to decide to merge as is, or indicate that we should investigate further), that would be great!

[Ruben Van de Velde]

It would be really great to have someone debug the simp issue - it's bothered me in a bunch of places already. I'd prefer not to let this sit for too long if nobody picks it up, though

[Ruben Van de Velde]

@Scott Morrison but we'll have to wait until you push your fixes anyway :)

[Scott Morrison]

Ugh, I can't find them??

[Ruben Van de Velde]

If you committed them, git reflog should have them

[Johan Commelin]

You will need to know in which clone you committed them (-;

[Eric Wieser]

I'll take a look once the fixes are found

[Scott Morrison]

I am completely mystified. I think at this point I should just try again, and hope I remember how the fixes looked.

[Scott Morrison]

Now the file looks unfamiliar to me, and I have no idea how I came to post this message. I am seriously feeling as if the matrix glitched....?!? Sorry for the noise.

[Reid Barton]

Johan Commelin said:

You will need to know in which clone you committed them (-;

Are we talking about clones of mathlib, or clones of Scott?

[Eric Wieser]

I've pushed some more fixes to this PR

[Eric Wieser]

There's one really weird error where congr didn't try to apply congr_fun

[Eric Wieser]

And a bunch of timeouts near the bottom of the file