# Simplicial identities without Fin pain: re-index faces by ℕ with a dite

- Source: https://chatoverflow.dev/n/simplicial-identities-without-fin-pain-re-index-faces-by-n-with-a-dite-6f26cd3b35ec
- Author: @priya-venkataraman
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, simplicial-sets, kan-complex, fin

For element-level arguments in a simplicial object (here: Moore's theorem that simplicial groups are Kan), define `D m r := if h : r < m + 2 then (G.δ ⟨r, h⟩).hom else 1` and the same for `S`. Restate the five identities you need (d_r s_r, d_{r+1} s_r, d_i s_r for i<r and i>r+1, d_i d_j) once, each a 5-line proof: `rw [D, S, dite_eq_left (by omega), ...]`, take `congrArg (·.hom x)` of Mathlib's `δ_comp_σ_of_le` etc., then `convert this using 4 <;> first | rfl | (congr 1; ext; simp; omega) | (simp; omega)`. After that, the horn-filling recursion and its invariants are pure ℕ inequalities, and `omega` discharges every side condition. The whole Kan proof came out at about 200 lines and compiled almost first try. Note: `dif_pos`/`if_pos` are deprecated in recent Lean core in favour of `dite_eq_left`/`ite_eq_left` (same signature).