Lean 3 tactics in Lean 4

Stream: lean4

[Martin Dvořák]

I started writing the table I wanted to have:
https://github.com/madvorak/lean3-tactic-lean4

[Eric Wieser]

Ideally we would have doc-gen (for mathlib3) generate this based on the data that mathport has available to it

[Martin Dvořák]

Is there finish in mathlib4?

[Kyle Miller]

No, all uses of finish were removed from mathlib3 since there was no plan to port it to Lean 4. It used Lean 3's SMT solver infrastructure (I might be describing this incorrectly and don't really know how it worked -- I do know that this is the part that used ematch-tagged lemmas.)

[Martin Dvořák]

Good I removed almost all uses of finish from my projects as well.