We currently have both ite_self and ite_id which are both, up to argument order, identical.
There is more duplication between Init.SimpLemmas and Init.ByCases.
I’d say these lemmas are useful independent of simp and by_cases, and would suggest consolidating them in, say, a module Init.Ite dedicated to lemmas about ite and dite.
We currently have both ite_self and ite_id which are both, up to argument order, identical.
There is more duplication between
Init.SimpLemmasandInit.ByCases.I’d say these lemmas are useful independent of
simpandby_cases, and would suggest consolidating them in, say, a moduleInit.Itededicated to lemmas aboutiteanddite.Versions
7dc1ceb8d4312850b39cef9e751e0a3b651946e3
Impact
Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.