awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ⋯ ⋯)
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
pos :
  ∀
    (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))),
    W f
neg :
  ∀
    (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))),
    W f
⊢ W f

Tactic:
by_cases h₁ : Function.Surjective f.hom.toOrderHom

Premises used: SimplexCategory.Hom.toOrderHom, CategoryTheory.InducedCategory.Hom.hom, DFunLike.coe, Function.Surjective
-- 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 ⋯ ⋯)
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
hb : 0 ≤ 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 := 0 } hb)
h : a + 0 = 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 := 0 : SimplexCategory } hb)).len +
          1))
      (⇑(Hom.toOrderHom f.hom) :
        (a : Fin ({ obj := { len := a }, property := ha }.obj.len + 1)) →
          Fin ({ obj := { len := 0 }, property := hb }.obj.len + 1))
⊢ W f

Tactic:
(h₁ (fun _ ↦ ⟨0, Subsingleton.elim (α := Fin 1) _ _⟩)).elim

Premises used: False.elim, Exists.intro, SimplexCategory.Hom.toOrderHom, CategoryTheory.InducedCategory.Hom.hom, Subsingleton.elim, OfNat.ofNat, DFunLike.coe
-- 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 ⋯ ⋯)
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
hb : 0 ≤ 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 := 0 } hb)
h : a + 0 = 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 := 0 : SimplexCategory } hb)).len +
          1))
      (⇑(Hom.toOrderHom f.hom) :
        (a : Fin ({ obj := { len := a }, property := ha }.obj.len + 1)) →
          Fin ({ obj := { len := 0 }, property := hb }.obj.len + 1))
⊢ W f

Tactic:
exact (h₁ (fun _ ↦ ⟨0, Subsingleton.elim (α := Fin 1) _ _⟩)).elim

Premises used: False.elim, Exists.intro, SimplexCategory.Hom.toOrderHom, CategoryTheory.InducedCategory.Hom.hom, Subsingleton.elim, OfNat.ofNat, DFunLike.coe
-- 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 ⋯ ⋯)
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 + 1 ≤ 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 + 1 } hb)
h : a + (b + 1) = 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 + 1 : SimplexCategory } hb)).len +
          1))
      (⇑(Hom.toOrderHom f.hom) :
        (a : Fin ({ obj := { len := a }, property := ha }.obj.len + 1)) →
          Fin ({ obj := { len := b + 1 }, property := hb }.obj.len + 1))
neg :
  ∀ (i : Fin (b + 2))
    (g' :
      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 := b })
    (hf' : f.hom = g' ≫ SimplexCategory.δ i), W f
⊢ W f

Tactic:
obtain ⟨i, g', hf'⟩ := eq_comp_δ_of_not_surjective _ h₁

Premises used: SimplexCategory.eq_comp_δ_of_not_surjective
-- 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 ⋯ ⋯)
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 + 1 ≤ 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 + 1 } hb)
h : a + (b + 1) = 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 + 1 : SimplexCategory } hb)).len +
          1))
      (⇑(Hom.toOrderHom f.hom) :
        (a : Fin ({ obj := { len := a }, property := ha }.obj.len + 1)) →
          Fin ({ obj := { len := b + 1 }, property := hb }.obj.len + 1))
i : Fin (b + 2)
g' :
  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 := b }
hf' : f.hom = g' ≫ SimplexCategory.δ i
neg : ∀ (hf' : f = Hom.tr g' ha ⋯ ≫ Hom.tr (SimplexCategory.δ i) ⋯ hb), W f
⊢ W f

Tactic:
replace hf' : f = Hom.tr g' ≫ Hom.tr (SimplexCategory.δ i) :=
          InducedCategory.hom_ext hf'
-- 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 ⋯ ⋯)
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 + 1 ≤ 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 + 1 } hb)
h : a + (b + 1) = 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 + 1 : SimplexCategory } hb)).len +
          1))
      (⇑(Hom.toOrderHom f.hom) :
        (a : Fin ({ obj := { len := a }, property := ha }.obj.len + 1)) →
          Fin ({ obj := { len := b + 1 }, property := hb }.obj.len + 1))
i : Fin (b + 2)
g' :
  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 := b }
hf' : f = Hom.tr g' ha ⋯ ≫ Hom.tr (SimplexCategory.δ i) ⋯ hb
neg : W (Hom.tr g' ha ⋯ ≫ Hom.tr (SimplexCategory.δ i) ⋯ hb)
⊢ W f

Tactic:
rw [hf']
-- 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 ⋯ ⋯)
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 + 1 ≤ 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 + 1 } hb)
h : a + (b + 1) = 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 + 1 : SimplexCategory } hb)).len +
          1))
      (⇑(Hom.toOrderHom f.hom) :
        (a : Fin ({ obj := { len := a }, property := ha }.obj.len + 1)) →
          Fin ({ obj := { len := b + 1 }, property := hb }.obj.len + 1))
i : Fin (b + 2)
g' :
  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 := b }
hf' : f = Hom.tr g' ha ⋯ ≫ Hom.tr (SimplexCategory.δ i) ⋯ hb
⊢ a + b = c

Tactic:
lia
-- 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 ⋯ ⋯)
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 + 1 ≤ 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 + 1 } hb)
h : a + (b + 1) = 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 + 1 : SimplexCategory } hb)).len +
          1))
      (⇑(Hom.toOrderHom f.hom) :
        (a : Fin ({ obj := { len := a }, property := ha }.obj.len + 1)) →
          Fin ({ obj := { len := b + 1 }, property := hb }.obj.len + 1))
i : Fin (b + 2)
g' :
  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 := b }
hf' : f = Hom.tr g' ha ⋯ ≫ Hom.tr (SimplexCategory.δ i) ⋯ hb
⊢ b < d

Tactic:
lia
-- 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 ⋯ ⋯)
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 + 1 ≤ 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 + 1 } hb)
h : a + (b + 1) = 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 + 1 : SimplexCategory } hb)).len +
          1))
      (⇑(Hom.toOrderHom f.hom) :
        (a : Fin ({ obj := { len := a }, property := ha }.obj.len + 1)) →
          Fin ({ obj := { len := b + 1 }, property := hb }.obj.len + 1))
i : Fin (b + 2)
g' :
  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 := b }
hf' : f = Hom.tr g' ha ⋯ ≫ Hom.tr (SimplexCategory.δ i) ⋯ hb
⊢ W (Hom.tr g' ha ⋯ ≫ Hom.tr (SimplexCategory.δ i) ⋯ hb)

Tactic:
exact W.comp_mem _ _ (hc _ _ _ _ _ (by lia))
          (δ_mem _ (by lia) _)

Premises used: CategoryTheory.MorphismProperty.comp_mem