!4#3466 LinearAlgebra.FiniteDimensional

Stream: mathlib4

[Jeremy Tan]

!4#3466 (LinearAlgebra.FiniteDimensional) has been opened. It's quite a tough cookie, so feel free to commit anything that solves at least one of the remaining 90 errors

[Eric Wieser]

I pushed some partial fixes

[Eric Wieser]

It seems that a lot of PUnits now need to be PUnit.{u+1}

[Scott Morrison]

I pushed some more fixes to LinearAlgebra.FiniteDimensional. There's still a bit more to do!

[Eric Wieser]

I'm now stuck at a goal that is Module.rank F { x // x ∈ ⊥ } = Module.rank F { x // x ∈ ⊥ }. If I use sorry then the tactic state is happy but the kernel times out. If it dare try refl then that times out too

[Eric Wieser]

One possible idea is that switching to flat structures for subalgebra/submodule (like we did in Lean 3) would help here

[Eric Wieser]

I bumped up the timeout and now the proof is ok

[Eric Wieser]

The lemma takes 1.39s in Lean 3, I don't know how to get a total time in Lean 4 21s in Lean 4

[Sebastian Ullrich]

You can use trace.profiler and look at the root node

[Scott Morrison]

Finished!

[Scott Morrison]

Could we just drop all the -- Porting note: gets around lean4#2074? They are just noise at this point, making it harder to review the real porting notes.

[Eric Wieser]

I pushed a possibly controversial commit that removed a hack in favor of bumping a timeout

[Eric Wieser]

The downside is one lemma is now 100x slower (instead of 15x) than it was in Lean 3

[Eric Wieser]

On the other hand, I'm worried that continuing to add ad-hoc instances to speedup TC search in one specific place at at a time is just going to slow down TC search globally and make TC search harder to predict.

[Scott Morrison]

Maybe we could leave in place a comment explaining the instances that would speed it up, just as a breadcrumb.

[Eric Wieser]

That sounds like a good compromise