awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) :=
  {i : Fin (n + 1) |
    Eq (α := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
          i :
        (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)}
hS : S.Nonempty
i : Fin (⦋n⦌.len + 1)
j : Fin (n + 1)
hj : j ∈ S
hij : j ≤ i
⊢ LE.le (α := Fin (⦋1⦌.len + 1))
    ((Hom.toOrderHom f : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋1⦌.len + 1)) j : Fin (⦋1⦌.len + 1))
    ((Hom.toOrderHom f : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋1⦌.len + 1)) i : Fin (⦋1⦌.len + 1))

Tactic:
have := f.toOrderHom.monotone hij
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) :=
  {i : Fin (n + 1) |
    Eq (α := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
          i :
        (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)}
hS : S.Nonempty
i : Fin (⦋n⦌.len + 1)
j : Fin (n + 1)
hj : j ∈ S
hij : j ≤ i
this :
  LE.le (α := Fin (⦋1⦌.len + 1))
    ((Hom.toOrderHom f : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋1⦌.len + 1)) j : Fin (⦋1⦌.len + 1))
    ((Hom.toOrderHom f : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋1⦌.len + 1)) i : Fin (⦋1⦌.len + 1))
neg :
  ∀
    (hS :
      Finset.Nonempty (α := Fin (n + 1))
        {x : Fin (n + 1) |
          Eq (α := Fin 2) ((Hom.toOrderHom f : (a : Fin (n + 1)) → Fin 2) x : Fin 2)
            (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)})
    (hj :
      Eq (α := Fin 2) ((Hom.toOrderHom f : (a : Fin (n + 1)) → Fin 2) j : Fin 2)
        (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌))
    (hij : j ≤ i)
    (this :
      LE.le (α := Fin 2) (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
        ((Hom.toOrderHom f : (a : Fin (n + 1)) → Fin 2) i : Fin 2)),
    Eq (α := Fin 2) (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((Hom.toOrderHom f : (a : Fin (n + 1)) → Fin 2) i : Fin 2)
⊢ Eq (α := Fin 2) (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : Fin (n + 1)) → Fin 2)
        i :
      Fin 2)

Tactic:
simp_all [ConcreteCategory.hom, S]

Premises used: CategoryTheory.ConcreteCategory.hom
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) :=
  {i : Fin (n + 1) |
    Eq (α := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
          i :
        (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)}
i : Fin (⦋n⦌.len + 1)
j : Fin (n + 1)
hS :
  Finset.Nonempty (α := Fin (n + 1))
    {x : Fin (n + 1) |
      Eq (α := Fin 2) ((Hom.toOrderHom f : (a : Fin (n + 1)) → Fin 2) x : Fin 2)
        (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)}
hj :
  Eq (α := Fin 2) ((Hom.toOrderHom f : (a : Fin (n + 1)) → Fin 2) j : Fin 2)
    (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
hij : j ≤ i
this :
  LE.le (α := Fin 2) (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
    ((Hom.toOrderHom f : (a : Fin (n + 1)) → Fin 2) i : Fin 2)
⊢ Eq (α := Fin 2) (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
    ((Hom.toOrderHom f : (a : Fin (n + 1)) → Fin 2) i : Fin 2)

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) :=
  {i : Fin (n + 1) |
    Eq (α := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
          i :
        (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)}
hS : ¬S.Nonempty
⊢ ∃ (a : Fin (n + 2)), toMk₁ a = f

Tactic:
⟨Fin.last _, ConcreteCategory.hom_ext _ _ (fun i ↦ ?_)⟩

Premises used: Fin.last, Exists.intro, CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) :=
  {i : Fin (n + 1) |
    Eq (α := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
          i :
        (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)}
hS : ¬S.Nonempty
neg :
  ∀ (i : Fin (⦋n⦌.len + 1)),
    Eq (α := Fin (⦋1⦌.len + 1))
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (X := ⦋n⦌) (toMk₁ (Fin.last (n + 1))) :
            (a : Fin (⦋n⦌.len + 1)) → Fin (⦋1⦌.len + 1))
          i :
        Fin (⦋1⦌.len + 1))
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : Fin (⦋n⦌.len + 1)) → Fin (⦋1⦌.len + 1))
          i :
        Fin (⦋1⦌.len + 1))
⊢ ∃ (a : Fin (n + 2)), toMk₁ a = f

Tactic:
refine ⟨Fin.last _, ConcreteCategory.hom_ext _ _ (fun i ↦ ?_)⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) :=
  {i : Fin (n + 1) |
    Eq (α := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
          i :
        (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
neg :
  Eq (α := Fin 2) (if i.castSucc < Fin.last (n + 1) then 0 else 1 : Fin 2)
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : Fin (n + 1)) → Fin 2)
        i :
      Fin 2)
⊢ Eq (α := Fin (⦋1⦌.len + 1))
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (X := ⦋n⦌) (toMk₁ (Fin.last (n + 1))) :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋1⦌.len + 1))
        i :
      Fin (⦋1⦌.len + 1))
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋1⦌.len + 1))
        i :
      Fin (⦋1⦌.len + 1))

Tactic:
dsimp [toMk₁_apply]

Premises used: SimplexCategory.toMk₁_apply
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) :=
  {i : Fin (n + 1) |
    Eq (α := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
          i :
        (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
⊢ i.castSucc < Fin.last (n + 1)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) :=
  {i : Fin (n + 1) |
    Eq (α := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
          i :
        (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
neg :
  Eq (α := Fin 2) (0 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : Fin (n + 1)) → Fin 2)
        i :
      Fin 2)
⊢ Eq (α := Fin 2) (if i.castSucc < Fin.last (n + 1) then 0 else 1 : Fin 2)
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : Fin (n + 1)) → Fin 2)
        i :
      Fin 2)

Tactic:
rw [if_pos (by simp)]

Premises used: if_pos
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) :=
  {i : Fin (n + 1) |
    Eq (α := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
          i :
        (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
⊢ ∃ (j : Fin 2),
    (ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
        i =
      j

Tactic:
⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) :=
  {i : Fin (n + 1) |
    Eq (α := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
          i :
        (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
neg :
  ∀ (j : Fin 2)
    (hj :
      (ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
          i =
        j),
    Eq (α := Fin 2) (0 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : Fin (n + 1)) → Fin 2)
          i :
        Fin 2)
⊢ Eq (α := Fin 2) (0 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : Fin (n + 1)) → Fin 2)
        i :
      Fin 2)

Tactic:
obtain ⟨j, hj⟩ : ∃ (j : Fin 2), f i = j := ⟨_, rfl⟩

Premises used: CategoryTheory.ConcreteCategory.hom, OfNat.ofNat, Fin, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) :=
  {i : Fin (n + 1) |
    Eq (α := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
          i :
        (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
j : Fin 2
hj :
  (ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
          fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
        (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      i =
    j
neg :
  ∀
    (hj :
      Eq (α := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
        ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
              (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) →
                (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
            i :
          (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
        ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1))),
    Eq (α := Fin 2) (0 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : Fin (n + 1)) → Fin 2)
          i :
        Fin 2)
neg₁ :
  ∀
    (hj :
      Eq (α := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
        ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
              (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) →
                (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
            i :
          (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
        ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1))),
    Eq (α := Fin 2) (0 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : Fin (n + 1)) → Fin 2)
          i :
        Fin 2)
⊢ Eq (α := Fin 2) (0 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : Fin (n + 1)) → Fin 2)
        i :
      Fin 2)

Tactic:
fin_cases j
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) :=
  {i : Fin (n + 1) |
    Eq (α := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
          i :
        (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
hj :
  Eq (α := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
        i :
      (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
    ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1))
⊢ Eq (α := Fin 2) (0 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : Fin (n + 1)) → Fin 2)
        i :
      Fin 2)

Tactic:
simp_all
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) :=
  {i : Fin (n + 1) |
    Eq (α := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
          i :
        (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
hj :
  Eq (α := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
        i :
      (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
    ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1))
⊢ i ∈ S

Tactic:
simpa [S]
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) :=
  {i : Fin (n + 1) |
    Eq (α := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
          i :
        (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
      (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
hj :
  Eq (α := (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
        i :
      (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
    ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1))
⊢ Eq (α := Fin 2) (0 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
          (a : Fin (n + 1)) → Fin 2)
        i :
      Fin 2)

Tactic:
exact (hS ⟨i, by simpa [S]⟩).elim

Premises used: False.elim, Exists.intro
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
⊢ Function.Bijective (α := Fin (n + 2)) toMk₁

Tactic:
⟨toMk₁_injective, toMk₁_surjective⟩

Premises used: And.intro, Function.Bijective, SimplexCategory.toMk₁_surjective, SimplexCategory.toMk₁_injective
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated
Goal:
n : ℕ
inst : NeZero n
⊢ 0 < n

Tactic:
have := Nat.pos_of_neZero n
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated
Goal:
n : ℕ
inst : NeZero n
this : 0 < n
out : ∀ (d : SimplexCategory), IsConnected (CostructuredArrow (inclusion n) d)
⊢ (inclusion n).Initial

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated
Goal:
n : ℕ
inst : NeZero n
this : 0 < n
Δ : SimplexCategory
⊢ Nonempty (CostructuredArrow (inclusion n) Δ)

Tactic:
have : Nonempty (CostructuredArrow (inclusion n) Δ) := ⟨⟨⦋0⦌ₙ, ⟨⟨⟩⟩, ⦋0⦌.const _ 0 ⟩⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated
Goal:
n : ℕ
inst : NeZero n
this_1 : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
out : ∀ (j₁ j₂ : CostructuredArrow (inclusion n) Δ), Zigzag j₁ j₂
⊢ IsConnected (CostructuredArrow (inclusion n) Δ)

Tactic:
apply zigzag_isConnected

Premises used: CategoryTheory.zigzag_isConnected
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated
Goal:
n : ℕ
inst : NeZero n
this_1 : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f :
  (inclusion n).obj (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) Δ₁ hΔ₁) ⟶
    Functor.obj (Functor.fromPUnit Δ) { as := PUnit.unit : Discrete PUnit.{1} }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' :
  (inclusion n).obj (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) Δ₂ hΔ₂) ⟶
    Functor.obj (Functor.fromPUnit Δ) { as := PUnit.unit : Discrete PUnit.{1} }
out :
  Zigzag
    { left := ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) ⦋0⦌ ⋯,
      right := { as := PUnit.unit },
      hom :=
        ⦋0⦌.const (Functor.obj (Functor.fromPUnit Δ) { as := PUnit.unit : Discrete PUnit.{1} })
          ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f :
              (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ((inclusion n).obj { obj := Δ₁, property := hΔ₁ })) →
                (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ((Functor.fromPUnit Δ).obj { as := PUnit.unit }))
            0) }
    { left := ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) Δ₂ hΔ₂,
      right := { as := PUnit.unit : Discrete PUnit.{1} }, hom := f' : Comma (inclusion n) (Functor.fromPUnit Δ) }
⊢ Zigzag
    { left := ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) Δ₁ hΔ₁,
      right := { as := PUnit.unit : Discrete PUnit.{1} }, hom := f : Comma (inclusion n) (Functor.fromPUnit Δ) }
    { left := ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ n) Δ₂ hΔ₂,
      right := { as := PUnit.unit }, hom := f' }

Tactic:
apply Zigzag.trans (j₂ := ⟨⦋0⦌ₙ, ⟨⟨⟩⟩, ⦋0⦌.const _ (f 0)⟩)
    (.of_inv <| CostructuredArrow.homMk <| Hom.tr <| ⦋0⦌.const _ 0)

Premises used: CategoryTheory.CostructuredArrow.homMk, CategoryTheory.Zigzag.trans, CategoryTheory.Zigzag.of_inv