Commit 2024-10-15 14:56 1b5eaee6
View on Github →chore(AlgebraicTopology): remove eqns attribute (#17774)
This eqns does slightly change the generated lemmas: objX.eq_2 talks about n.succ while objX_add_one talks about n + 1. Still, it's easy enough to replace the one failing unfold in a rw with a rw [objX_add_one].