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

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).