-- Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty
Goal:
d : ℕ
W : MorphismProperty (Truncated d)
inst : W.IsMultiplicative
δ_mem :
  ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)),
    W (X := ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := n } ⋯) (Y :=
      ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := n + 1 } ⋯) (δ d i ⋯ ⋯)
σ_mem :
  ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)),
    W (X := ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := n + 1 } ⋯) (Y :=
      ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := n } ⋯) (σ d i ⋯ ⋯)
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f :
  Quiver.Hom (V := Truncated d)
    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := a } ha)
    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := b } hb)
c : ℕ
h : a + b = c
h₁ :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f :
      Quiver.Hom (V := Truncated d)
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := a } ha)
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := b } hb))
    (h : a + b = 0), W f
h₂ :
  ∀ (c : ℕ)
    (hc :
      ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
        (f :
          Quiver.Hom (V := Truncated d)
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := a } ha)
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := b } hb))
        (h : a + b = c), W f)
    (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f :
      Quiver.Hom (V := Truncated d)
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := a } ha)
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := b } hb))
    (h : a + b = c + 1), W f
⊢ W f

Tactic:
induction c generalizing a b with
  | zero =>
    obtain rfl : a = 0 := by lia
    obtain rfl : b = 0 := by lia
    obtain rfl : f = 𝟙 _ := by
      ext i : 3
      apply Subsingleton.elim (α := Fin 1)
    apply MorphismProperty.id_mem
  | succ c hc =>
    by_cases h₁ : Function.Surjective f.hom.toOrderHom; swap
    · obtain _ | b := b
      · exact (h₁ (fun _ ↦ ⟨0, Subsingleton.elim (α := Fin 1) _ _⟩)).elim
      · obtain ⟨i, g', hf'⟩ := eq_comp_δ_of_not_surjective _ h₁
        replace hf' : f = Hom.tr g' ≫ Hom.tr (SimplexCategory.δ i) :=
          InducedCategory.hom_ext hf'
        rw [hf']
        exact W.comp_mem _ _ (hc _ _ _ _ _ (by lia))
          (δ_mem _ (by lia) _)
    by_cases h₂ : Function.Injective f.hom.toOrderHom; swap
    · obtain _ | a := a
      · exact (h₂ (Function.injective_of_subsingleton (α := Fin 1) _)).elim
      · obtain ⟨i, g', hf'⟩ := eq_σ_comp_of_not_injective _ h₂
        replace hf' : f = Hom.tr (SimplexCategory.σ i) ≫ Hom.tr g' :=
          InducedCategory.hom_ext hf'
        rw [hf']
        exact W.comp_mem _ _ (σ_mem _ (by lia) _) (hc _ _ _ _ _ (by lia))
    rw [← epi_iff_surjective] at h₁
    rw [← mono_iff_injective] at h₂
    obtain rfl : a = b := le_antisymm (len_le_of_mono f.hom) (len_le_of_epi f.hom)
    obtain rfl : f = 𝟙 _ := ObjectProperty.hom_ext _ (SimplexCategory.eq_id_of_epi _)
    apply W.id_mem

Premises used: CategoryTheory.CategoryStruct.id, SimplexCategory.eq_id_of_epi, SimplexCategory.mono_iff_injective, CategoryTheory.ObjectProperty.hom_ext, SimplexCategory.Hom.toOrderHom, CategoryTheory.MorphismProperty.id_mem, Function.Injective, CategoryTheory.InducedCategory.Hom.hom, DFunLike.coe, Function.Surjective, SimplexCategory.epi_iff_surjective, rfl