mathlib

mathlib copied to clipboard

This PR introduces variations on the statements of simplicial relations which makes it easier to use. This is demonstrated in algebraic_topology.dold_kan.faces. The attribute reassoc is also added to the simplicial relations.

---

For example, we introduce the lemma δ_comp_δ_self' {n} {i : fin (n+2)} {j : fin (n+3)} (H : j = i.cast_succ) : δ i ≫ δ j = δ i ≫ δ i.succ which is more practical than δ_comp_δ_self {n} {i : fin (n+2)} : δ i ≫ δ i.cast_succ = δ i ≫ δ i.succ. The idea is that doing rw δ_comp_δ_self' will create the goal j = i.cast_succ which is usually easy to prove.