Commit 2026-10-18 20:50 5b040b83

fix(Tactic/CategoryTheory/Slice): do not generate redundant goals (#44569) This PR fixes the slice/slice_lhs/slice_rhs tactics to not generate goals other than the intended one. The fix to use the lhs and rhs conv mode tactics instead of congr (which generates multiple goals). This is a step towards supporting the multiGoal linter in conv mode, but is also a nice fix on its own.