State of Lean 3's mathlib tactics

Stream: lean4

[Ryan Lahfa]

As suggested by @Kevin Buzzard

I am wondering if there are people working on mathlib's tactics in Lean 4, e.g. linarith and what has been their experience so far with tactic porting from Lean 3.