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

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.