may I open a PR? see: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathlib4.20tactics.20list.3F/near/433066915
