Commit 2025-11-20 22:24 22da866f
View on Github →doc(Tactic/MinImports): tidy backticks (#31861) Found and fixed with help from Codex. This is the last remaining true positive finding of the detection script in https://github.com/leanprover-community/mathlib4/pull/31463.