-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty (goal)
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 ⋯ ⋯)
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
h₁ :
  Function.Surjective (α :=
    Fin
      ((ObjectProperty.FullSubcategory.obj (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
              { len := a : SimplexCategory } ha)).len +
        1))
    (β :=
    Fin
      ((ObjectProperty.FullSubcategory.obj (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
              { len := b : SimplexCategory } hb)).len +
        1))
    (⇑(Hom.toOrderHom f.hom) :
      (a : Fin ({ obj := { len := a }, property := ha }.obj.len + 1)) →
        Fin ({ obj := { len := b }, property := hb }.obj.len + 1))
pos :
  ∀
    (h₂ :
      Function.Injective (α :=
        Fin
          ((ObjectProperty.FullSubcategory.obj (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
                  { len := a : SimplexCategory } ha)).len +
            1))
        (β :=
        Fin
          ((ObjectProperty.FullSubcategory.obj (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
                  { len := b : SimplexCategory } hb)).len +
            1))
        (⇑(Hom.toOrderHom f.hom) :
          (a : Fin ({ obj := { len := a }, property := ha }.obj.len + 1)) →
            Fin ({ obj := { len := b }, property := hb }.obj.len + 1))),
    W f
⊢ W f
have neg : ∀
  (h₂ :
    ¬Function.Injective (α :=
        Fin
          ((ObjectProperty.FullSubcategory.obj (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
                  { len := a : SimplexCategory } ha)).len +
            1))
        (β :=
        Fin
          ((ObjectProperty.FullSubcategory.obj (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
                  { len := b : SimplexCategory } hb)).len +
            1))
        (⇑(Hom.toOrderHom f.hom) :
          (a : Fin ({ obj := { len := a }, property := ha }.obj.len + 1)) →
            Fin ({ obj := { len := b }, property := hb }.obj.len + 1))),
  W f
Tactic: by_cases h₂ : Function.Injective f.hom.toOrderHom