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
b : ℕ
hb : b ≤ d
ha : 0 ≤ d
f :
  Quiver.Hom (V := Truncated d)
    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := 0 } ha)
    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := b } hb)
h : 0 + 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 := 0 : 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 := 0 }, property := ha }.obj.len + 1)) →
        Fin ({ obj := { len := b }, property := hb }.obj.len + 1))
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 := 0 : 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 := 0 }, property := ha }.obj.len + 1)) →
          Fin ({ obj := { len := b }, property := hb }.obj.len + 1))
⊢ W f

Tactic:
(h₂ (Function.injective_of_subsingleton (α := Fin 1) _)).elim

Premises used: False.elim, Function.injective_of_subsingleton
-- 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
b : ℕ
hb : b ≤ d
ha : 0 ≤ d
f :
  Quiver.Hom (V := Truncated d)
    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := 0 } ha)
    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := b } hb)
h : 0 + 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 := 0 : 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 := 0 }, property := ha }.obj.len + 1)) →
        Fin ({ obj := { len := b }, property := hb }.obj.len + 1))
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 := 0 : 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 := 0 }, property := ha }.obj.len + 1)) →
          Fin ({ obj := { len := b }, property := hb }.obj.len + 1))
⊢ W f

Tactic:
exact (h₂ (Function.injective_of_subsingleton (α := Fin 1) _)).elim

Premises used: False.elim, Function.injective_of_subsingleton
-- 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
b : ℕ
hb : b ≤ d
a : ℕ
ha : a + 1 ≤ d
f :
  Quiver.Hom (V := Truncated d)
    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := a + 1 } ha)
    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := b } hb)
h : a + 1 + 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 + 1 : 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 + 1 }, property := ha }.obj.len + 1)) →
        Fin ({ obj := { len := b }, property := hb }.obj.len + 1))
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 + 1 : 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 + 1 }, property := ha }.obj.len + 1)) →
          Fin ({ obj := { len := b }, property := hb }.obj.len + 1))
i : Fin (a + 1)
g' :
  { len := a : SimplexCategory } ⟶
    ObjectProperty.FullSubcategory.obj (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := b } hb)
hf' : f = Hom.tr (SimplexCategory.σ i) ha ⋯ ≫ Hom.tr g' ⋯ hb
⊢ a < 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
b : ℕ
hb : b ≤ d
a : ℕ
ha : a + 1 ≤ d
f :
  Quiver.Hom (V := Truncated d)
    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := a + 1 } ha)
    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := b } hb)
h : a + 1 + 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 + 1 : 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 + 1 }, property := ha }.obj.len + 1)) →
        Fin ({ obj := { len := b }, property := hb }.obj.len + 1))
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 + 1 : 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 + 1 }, property := ha }.obj.len + 1)) →
          Fin ({ obj := { len := b }, property := hb }.obj.len + 1))
i : Fin (a + 1)
g' :
  { len := a : SimplexCategory } ⟶
    ObjectProperty.FullSubcategory.obj (P := fun (a : SimplexCategory) ↦ a.len ≤ d)
      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := b } hb)
hf' : f = Hom.tr (SimplexCategory.σ i) ha ⋯ ≫ Hom.tr g' ⋯ 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 ≤ 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))
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))
⊢ Epi f.hom

Tactic:
rw [← epi_iff_surjective] at h₁

Premises used: SimplexCategory.epi_iff_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 ≤ 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₁ : Epi f.hom
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))
⊢ Mono f.hom

Tactic:
rw [← mono_iff_injective] at h₂

Premises used: SimplexCategory.mono_iff_injective
-- 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
h₁ : Epi f.hom
h₂ : Mono f.hom
⊢ a = b

Tactic:
le_antisymm (len_le_of_mono f.hom) (len_le_of_epi f.hom)

Premises used: SimplexCategory.len_le_of_mono, SimplexCategory.len_le_of_epi, le_antisymm, CategoryTheory.InducedCategory.Hom.hom
-- 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
h₁ : Epi f.hom
h₂ : Mono f.hom
pos :
  ∀ (hb : a ≤ 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 := a } hb))
    (h : a + a = c + 1) (h₁ : Epi f.hom) (h₂ : Mono f.hom), W f
⊢ W f

Tactic:
obtain rfl : a = b := le_antisymm (len_le_of_mono f.hom) (len_le_of_epi f.hom)

Premises used: SimplexCategory.len_le_of_mono, SimplexCategory.len_le_of_epi, le_antisymm, CategoryTheory.InducedCategory.Hom.hom, rfl
-- 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 hb : a ≤ 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 := a } hb)
h : a + a = c + 1
h₁ : Epi f.hom
h₂ : Mono f.hom
⊢ f = 𝟙 (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := a } ha)

Tactic:
ObjectProperty.hom_ext _ (SimplexCategory.eq_id_of_epi _)

Premises used: SimplexCategory.eq_id_of_epi, CategoryTheory.ObjectProperty.hom_ext