Commit 2023-06-12 12:56 2da2fd33
View on Github →chore: forward port leanprover-community/mathlib#19118 (#4831)
This also removes a stray import Mathlib.Tactic, which causes a downstream file to break.
chore: forward port leanprover-community/mathlib#19118 (#4831)
This also removes a stray import Mathlib.Tactic, which causes a downstream file to break.