Commit 2025-01-21 04:10 6fdfd805

View on Github →

feat(Data/Fin/Tuple/Basic): snoc & insertNth are injective (#20771) This PR adds injectivity lemmas for Fin.snoc and Fin.insertNth, similar to those for Fin.cons. This is part of #19315 that is split off.

Estimated changes

deleted theorem Fin.cons_eq_cons
added theorem Fin.cons_inj
added theorem Fin.insertNth_inj
added theorem Fin.snoc_inj
added theorem Fin.snoc_injective2