Commit 2025-07-24 15:35 2cb771d3
View on Github →chore(LinearAlgebra/RootSystem): golf exists_apply_eq_or and remove note "we should have a tactic to crush this" (#27372)
Remove:
/- The below proof (due to Mario Carneiro, Johan Commelin, Bhavik Mehta, Jingting Wang) should
not really be necessary: we should have a tactic to crush this. -/
We now have such a tactic! 🎉