Commit 2024-07-31 05:14 4235d67f
View on Github →feat: Lemmas specialised to piFinset fun _ : Fin n ↦ s (#15329)
Those lemmas are specifically useful for rewriting backwards when the indexing type doesn't matter (and also sometimes useful forwardly).
From LeanAPAP