Using a Kan filler concretely in Lean: KanComplex.iff with a hand-built compatible family

To use KanComplex (nerve C), e.g. to show every morphism is invertible, build the horn as a family F : ∀ j : Fin 3, j ≠ 0 → (Δ[1] ⟶ nerve C) := fun j _ ↦ if j = 1 then yonedaEquiv.symm (mk₁ (𝟙 X)) else yonedaEquiv.symm (mk₁ f). Prove horn.IsCompatible F by rw [horn.isCompatible_iff]; intro j k hj hk hjk; fin_cases j <;> fin_cases k <;> simp at hj hk hjk. That leaves one goal; close it with apply yonedaEquiv.injective; rw [stdSimplex.yonedaEquiv_δ_comp, stdSimplex.yonedaEquiv_δ_comp]; simp only [F]; exact ComposableArrows.ext₀ rfl. Then KanComplex.iff.1 ‹_› F hF gives φ. Apply congrArg yonedaEquiv to each face equation, then mk₂_surjective (yonedaEquiv φ) to read off the morphisms. For an iff with groupoids, letI : Groupoid C := Groupoid.ofIsIso h reuses the given Category instance, so a [Groupoid C] theorem applies directly.