awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
j a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ} (hL : IsAdmissible m L) (hj₁ : j < m + L.length) (hj₂ : simplicialEvalσ L j = simplicialEvalσ L (j + 1)),
    j ∈ L
m : ℕ
hL : IsAdmissible m (a :: L)
hj₁ : j < m + (a :: L).length
hj₂ : simplicialEvalσ (a :: L) j = simplicialEvalσ (a :: L) (j + 1)
this : ∀ ⦃b : ℕ⦄, a + 1 ≤ b → simplicialEvalσ L (a + 1) ≤ simplicialEvalσ L b
h : j = a
⊢ j ∈ a :: L

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
j a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ} (hL : IsAdmissible m L) (hj₁ : j < m + L.length) (hj₂ : simplicialEvalσ L j = simplicialEvalσ L (j + 1)),
    j ∈ L
m : ℕ
hL : IsAdmissible m (a :: L)
hj₁ : j < m + (a :: L).length
hj₂ : simplicialEvalσ (a :: L) j = simplicialEvalσ (a :: L) (j + 1)
this : ∀ ⦃b : ℕ⦄, a + 1 ≤ b → simplicialEvalσ L (a + 1) ≤ simplicialEvalσ L b
h : a < j
⊢ j ∈ a :: L

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m : ℕ
L : List ℕ
hL : IsAdmissible m L
j : ℕ
hj₁ : j < m + L.length
hj₂ : simplicialEvalσ L j = simplicialEvalσ L (j + 1)
nil :
  ∀ {m : ℕ} (hL : IsAdmissible m []) (hj₁ : j < m + List.length (α := ℕ) [])
    (hj₂ : simplicialEvalσ [] j = simplicialEvalσ [] (j + 1)), Membership.mem (γ := List ℕ) [] j
cons :
  ∀ (a : ℕ) (L : List ℕ)
    (h_rec :
      ∀ {m : ℕ} (hL : IsAdmissible m L) (hj₁ : j < m + L.length)
        (hj₂ : simplicialEvalσ L j = simplicialEvalσ L (j + 1)), j ∈ L)
    {m : ℕ} (hL : IsAdmissible m (a :: L)) (hj₁ : j < m + (a :: L).length)
    (hj₂ : simplicialEvalσ (a :: L) j = simplicialEvalσ (a :: L) (j + 1)), j ∈ a :: L
⊢ j ∈ L

Tactic:
induction L generalizing m with
  | nil => grind
  | cons a L h_rec =>
    have := simplicialEvalσ_monotone L (a := a + 1)
    rcases lt_trichotomy j a with h | h | h <;> grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m : ℕ
L : List ℕ
hL : IsAdmissible m L
j : ℕ
hj : j ∈ L
⊢ j < m + L.length ∧ simplicialEvalσ L j = simplicialEvalσ L (j + 1)

Tactic:
grind [List.mem_iff_getElem]

Premises used: List.mem_iff_getElem
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m : ℕ
L : List ℕ
hL : IsAdmissible m L
j : ℕ
⊢ j ∈ L ↔ j < m + L.length ∧ simplicialEvalσ L j = simplicialEvalσ L (j + 1)

Tactic:
grind [lt_and_eval_eq_eval_add_one_of_mem_isAdmissible,
    mem_isAdmissible_of_lt_and_eval_eq_eval_add_one]

Premises used: SimplexCategoryGenRel.mem_isAdmissible_of_lt_and_eval_eq_eval_add_one, SimplexCategoryGenRel.lt_and_eval_eq_eval_add_one_of_mem_isAdmissible
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty
Goal:
d : ℕ
W : MorphismProperty (Truncated d)
inst : W.IsMultiplicative
n : ℕ
hn : n < d
i : Fin (n + 2)
dsimp : n ≤ d
⊢ { len := n : SimplexCategory }.len ≤ d

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty
Goal:
d : ℕ
W : MorphismProperty (Truncated d)
inst : W.IsMultiplicative
n : ℕ
hn : n < d
i : Fin (n + 2)
⊢ n ≤ d

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty
Goal:
d : ℕ
W : MorphismProperty (Truncated d)
inst : W.IsMultiplicative
n : ℕ
hn : n < d
i : Fin (n + 2)
⊢ n + 1 ≤ 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 ⋯ ⋯)
n : ℕ
hn : n < d
i : Fin (n + 1)
⊢ n + 1 ≤ 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 ⋯ ⋯)
n : ℕ
hn : n < d
i : Fin (n + 1)
dsimp : n ≤ d
⊢ { len := n : SimplexCategory }.len ≤ d

Tactic:
dsimp
-- 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 ⋯ ⋯)
n : ℕ
hn : n < d
i : Fin (n + 1)
⊢ n ≤ 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 ⋯ ⋯)
h :
  ∀ (a : SimplexCategory) (ha : a.len ≤ d) (b : SimplexCategory) (hb : b.len ≤ d)
    (f :
      Quiver.Hom (V := Truncated d)
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) a ha)
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) b hb)),
    W f ↔ ⊤ f
⊢ W = ⊤

Tactic:
ext ⟨a, ha⟩ ⟨b, hb⟩ f
-- 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 : SimplexCategory
ha : a.len ≤ d
b : SimplexCategory
hb : b.len ≤ d
f :
  Quiver.Hom (V := Truncated d) (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) a ha)
    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) b hb)
h : W f
⊢ W f ↔ ⊤ f

Tactic:
simp only [MorphismProperty.top_apply, iff_true]

Premises used: iff_true, CategoryTheory.MorphismProperty.top_apply
-- 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 : SimplexCategory
ha : a.len ≤ d
b : SimplexCategory
hb : b.len ≤ d
f :
  Quiver.Hom (V := Truncated d) (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) a ha)
    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) b hb)
h :
  ∀ (a : ℕ) (ha : { len := a : SimplexCategory }.len ≤ 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) b hb)),
    W f
⊢ W f

Tactic:
induction a using SimplexCategory.rec with | _ a
-- 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 ⋯ ⋯)
b : SimplexCategory
hb : b.len ≤ d
a : ℕ
ha : { len := a : SimplexCategory }.len ≤ 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) b hb)
h :
  ∀ (b : ℕ) (hb : { len := b : SimplexCategory }.len ≤ 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)),
    W f
⊢ W f

Tactic:
induction b using SimplexCategory.rec with | _ b
-- 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)
h : ∀ (c : ℕ) (h : a + b = c), W f
⊢ W f

Tactic:
generalize h : a + b = c
-- 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)
h : a + b = 0
⊢ a = 0

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 ⋯ ⋯)
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
h₁ :
  ∀ (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 = 0), W f
⊢ W f

Tactic:
obtain rfl : a = 0 := by lia

Premises used: 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 ⋯ ⋯)
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 = 0
⊢ b = 0

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 ⋯ ⋯)
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 = 0
h₁ :
  ∀ (hb : 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 := 0 } hb))
    (h : HAdd.hAdd (α := ℕ) 0 0 = 0), W f
⊢ W f

Tactic:
obtain rfl : b = 0 := by lia

Premises used: 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 ⋯ ⋯)
ha hb : 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 := 0 } hb)
h : HAdd.hAdd (α := ℕ) 0 0 = 0
h₁ :
  ∀
    (i :
      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)),
    Eq (α :=
      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 := 0 }, property := ha }.obj.len + 1)) →
              Fin ({ obj := { len := 0 }, property := hb }.obj.len + 1))
          i :
        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
              (InducedCategory.Hom.hom
                (𝟙 (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := 0 } ha))) :
            (a : Fin ({ obj := { len := 0 }, property := ha }.obj.len + 1)) →
              Fin ({ obj := { len := 0 }, property := hb }.obj.len + 1))
          i :
        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))
⊢ f = 𝟙 (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := 0 } ha)

Tactic:
ext i : 3
-- 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 ⋯ ⋯)
ha hb : 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 := 0 } hb)
h : HAdd.hAdd (α := ℕ) 0 0 = 0
i :
  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)
⊢ Eq (α :=
    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 := 0 }, property := ha }.obj.len + 1)) →
            Fin ({ obj := { len := 0 }, property := hb }.obj.len + 1))
        i :
      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
            (InducedCategory.Hom.hom
              (𝟙 (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := 0 } ha))) :
          (a : Fin ({ obj := { len := 0 }, property := ha }.obj.len + 1)) →
            Fin ({ obj := { len := 0 }, property := hb }.obj.len + 1))
        i :
      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))

Tactic:
apply Subsingleton.elim (α := Fin 1)

Premises used: Subsingleton.elim
-- 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 ⋯ ⋯)
ha hb : 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 := 0 } hb)
h : HAdd.hAdd (α := ℕ) 0 0 = 0
h₁ :
  W (X := ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := 0 } ha)
    (𝟙 (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := 0 } ha))
⊢ W f

Tactic:
obtain rfl : f = 𝟙 _ := by
      ext i : 3
      apply Subsingleton.elim (α := Fin 1)

Premises used: CategoryTheory.CategoryStruct.id, 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 ⋯ ⋯)
ha hb : 0 ≤ d
h : HAdd.hAdd (α := ℕ) 0 0 = 0
⊢ W (X := ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := 0 } ha)
    (𝟙 (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ d) { len := 0 } ha))

Tactic:
apply MorphismProperty.id_mem

Premises used: CategoryTheory.MorphismProperty.id_mem