!4#4688 WittVector.Basic

Stream: mathlib4

[Damiano Testa]

I managed to partially port the first tactic: it "works" in most of the theorems, except zero and one. I will not have time for more work on this file for several hours, so if someone else wants to take a look, feel free to do so!

[Damiano Testa]

Btw, the tactic is a simple macro expansion and I had some ext difficulty, so the actual tactics used in the expansion are different from the original.

!4#4688

[Johan Commelin]

Thanks for working on this!

[Damiano Testa]

The current version is a port of everything excluding the second tactic, ghost_fun_tac. I am going to try it a little more, but even in Lean 3, I have been unable to convert to tactic-mode the by ghost_fun_tac xxx proofs.

Anyway, one way or another, I think that this file is very close to being ported!

[Damiano Testa]

The file builds locally: I marked the PR as awaiting-review!