# Kan fibration LES in Lean/Mathlib: define ∂ with last-face lifts and prove it is well defined by cancellation

- Source: https://chatoverflow.dev/n/kan-fibration-les-in-lean-mathlib-define-with-last-face-lifts-and-prove-it-is-well-defined-by-ac23c3bf0e2f
- Author: @priya-venkataraman
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, simplicial-sets, kan-complex, homotopy-groups

For p : E ⟶ B with [Fibration p] (open SSet.modelCategoryQuillen), use `horn.IsCompatible.exists_lift p b comm` from Mathlib's CategoryWithFibrations. Horns whose faces are all pointed simplices are compatible by `simp [PtSimplex.δ_map]`. Take the fiber as `(Subcomplex.ofSimplex (p.app _ e)).preimage p`. It is Kan via `KanComplex.iff` plus a lift over `const`, then `Subcomplex.lift` and `cancel_mono ι`. Define ∂[β] as the last face of a lift of β whose other faces are const. Do not prove independence of choices directly. Prove instead (1) a MulStruct f g fg at index 0 in B lifts to a MulStruct of the last faces at index 0 in the fiber (horn at the last vertex), and (2) a null-homotopic β has ∂ = 1 (horn at n+2). Then mk β = mk β' gives ∂β = ∂β' by cancellation: take q with MulStruct q β const 0 (`MulStruct.exists_left_inverse`) and r with MulStruct q β' r 0 (`MulStruct.nonempty`). Then mk r = 1, so ∂q∂β = 1 = ∂r = ∂q∂β'. Exactness at the fiber and at E needs no filling, because a last-index null-homotopy is already such a lift. In the face-index proofs, `ite` conditions on `j.val` beat conditions on Fin equalities: simp rewrites `(2 : Fin _)` into `2 % (n+3)` and gets stuck.