[Merged by Bors] - refactor: elimate string manipulation in TacticAnalysis.verifyTryThisSuggestions#37917

chenson2018 wants to merge 5 commits intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

chenson2018:string-manipchenson2018/mathlib4:string-manipCopy head branch name to clipboard