awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin (⦋n⦌.len + 1)
h : j₁ ≤ j₂
pos : j₁.castSucc < i → j₂.castSucc < i → LE.le (α := Fin 2) 0 0
neg : j₁.castSucc < i → ¬j₂.castSucc < i → LE.le (α := Fin 2) 0 1
pos₁ : ¬j₁.castSucc < i → j₂.castSucc < i → LE.le (α := Fin 2) 1 0
neg₁ : ¬j₁.castSucc < i → ¬j₂.castSucc < i → LE.le (α := Fin 2) 1 1
⊢ LE.le (α := Fin 2) (if j₁.castSucc < i then 0 else 1) (if j₂.castSucc < i then 0 else 1)

Tactic:
split_ifs
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin (⦋n⦌.len + 1)
h : j₁ ≤ j₂
h_1 : j₁.castSucc < i
h_2 : j₂.castSucc < i
⊢ LE.le (α := Fin 2) 0 0

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin (⦋n⦌.len + 1)
h : j₁ ≤ j₂
h_1 : j₁.castSucc < i
h_2 : ¬j₂.castSucc < i
⊢ LE.le (α := Fin 2) 0 1

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin (⦋n⦌.len + 1)
h : j₁ ≤ j₂
h_1 : ¬j₁.castSucc < i
h_2 : j₂.castSucc < i
⊢ LE.le (α := Fin 2) 1 0

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin (⦋n⦌.len + 1)
h : j₁ ≤ j₂
h_1 : ¬j₁.castSucc < i
h_2 : ¬j₂.castSucc < i
⊢ LE.le (α := Fin 2) 1 1

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
⊢ Eq (α := 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)) (toMk₁ i) :
          (a : Fin (n + 1)) → Fin 2)
        j :
      Fin 2)
    (if j.castSucc < i then 0 else 1 : Fin 2)

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
⊢ Eq (α := 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)) (toMk₁ i) :
            (a : Fin (n + 1)) → Fin 2)
          j :
        Fin 2)
      (0 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌) ↔
    j.castSucc < i

Tactic:
simp [toMk₁_apply]

Premises used: SimplexCategory.toMk₁_apply
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
⊢ Eq (α := 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)) (toMk₁ i) :
          (a : Fin (n + 1)) → Fin 2)
        j :
      Fin 2)
    (0 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)

Tactic:
simpa [toMk₁_apply]

Premises used: SimplexCategory.toMk₁_apply
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
⊢ Eq (α := 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)) (toMk₁ i) :
            (a : Fin (n + 1)) → Fin 2)
          j :
        Fin 2)
      (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌) ↔
    i ≤ j.castSucc

Tactic:
simp [toMk₁_apply]

Premises used: SimplexCategory.toMk₁_apply
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
⊢ Eq (α := 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)) (toMk₁ i) :
          (a : Fin (n + 1)) → Fin 2)
        j :
      Fin 2)
    (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)

Tactic:
simpa [toMk₁_apply]

Premises used: SimplexCategory.toMk₁_apply
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
h : i ≤ j.castSucc
obtain : ∀ (i : Fin (n + 2)) (h : i.castSucc ≤ j.castSucc), δ j ≫ toMk₁ i.castSucc = toMk₁ (i.castSucc.castPred ⋯)
⊢ δ j ≫ toMk₁ i = toMk₁ (i.castPred ⋯)

Tactic:
obtain ⟨i, rfl⟩ := Fin.eq_castSucc_of_ne_last
    (Fin.ne_last_of_lt (lt_of_le_of_lt h j.castSucc_lt_succ))

Premises used: lt_of_le_of_lt, Fin.eq_castSucc_of_ne_last, Fin.castSucc_lt_succ, Fin.ne_last_of_lt, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
j i : Fin (n + 2)
h : i.castSucc ≤ j.castSucc
⊢ i ≤ j

Tactic:
simp only [Fin.castSucc_le_castSucc_iff] at h

Premises used: Fin.castSucc_le_castSucc_iff
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
j i : Fin (n + 2)
h_1 : i.castSucc ≤ j.castSucc
h : i ≤ j
rw : δ j ≫ toMk₁ i.castSucc = toMk₁ i
⊢ δ j ≫ toMk₁ i.castSucc = toMk₁ (i.castSucc.castPred ⋯)

Tactic:
rw [Fin.castPred_castSucc]

Premises used: Iff.mpr, Fin.ext_iff, Fin.castPred_castSucc, Iff.not, Fin.castSucc_lt_last, LT.lt.ne
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
j i : Fin (n + 2)
h_1 : i.castSucc ≤ j.castSucc
h : i ≤ j
⊢ δ j ≫ toMk₁ i.castSucc = toMk₁ i

Tactic:
ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
j i : Fin (n + 2)
h_1 : i.castSucc ≤ j.castSucc
h : i ≤ j
refine :
  ∀ (k : 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)) (δ j ≫ toMk₁ i.castSucc) :
            (a : Fin (⦋n⦌.len + 1)) → Fin (⦋1⦌.len + 1))
          k :
        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)) (toMk₁ i) :
            (a : Fin (⦋n⦌.len + 1)) → Fin (⦋1⦌.len + 1))
          k :
        Fin (⦋1⦌.len + 1))
⊢ δ j ≫ toMk₁ i.castSucc = toMk₁ i

Tactic:
refine ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
j i : Fin (n + 2)
h_1 : i.castSucc ≤ j.castSucc
h : i ≤ j
k : Fin (⦋n⦌.len + 1)
change :
  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)) (toMk₁ i.castSucc) :
          (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n + 1⦌) →
            (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
        (j.succAbove k) :
      (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)) (toMk₁ i) :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋1⦌.len + 1))
        k :
      Fin (⦋1⦌.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)) (δ j ≫ toMk₁ i.castSucc) :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋1⦌.len + 1))
        k :
      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)) (toMk₁ i) :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋1⦌.len + 1))
        k :
      Fin (⦋1⦌.len + 1))

Tactic:
change toMk₁ i.castSucc (j.succAbove k) = _

Premises used: Fin.succAbove, SimplexCategory.toMk₁, CategoryTheory.ConcreteCategory.hom, Fin.castSucc, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
j i : Fin (n + 2)
h_1 : i.castSucc ≤ j.castSucc
h : i ≤ j
k : Fin (⦋n⦌.len + 1)
rw : (j.succAbove k).castSucc < i.castSucc ↔ k.castSucc < i
⊢ Eq (α := 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)) (toMk₁ i.castSucc) :
          (a : Fin (n + 1 + 1)) → Fin 2)
        (j.succAbove k) :
      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)) (toMk₁ i) :
          (a : Fin (n + 1)) → Fin 2)
        k :
      Fin 2)

Tactic:
rw [Fin.eq_iff_eq_zero_iff, toMk₁_apply_eq_zero_iff, toMk₁_apply_eq_zero_iff]

Premises used: SimplexCategory.toMk₁_apply_eq_zero_iff, Fin.eq_iff_eq_zero_iff
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
j i : Fin (n + 2)
h_1 : i.castSucc ≤ j.castSucc
h : i ≤ j
k : Fin (⦋n⦌.len + 1)
⊢ (j.succAbove k).castSucc < i.castSucc ↔ k.castSucc < i

Tactic:
grind [Fin.succAbove]

Premises used: Fin.succAbove
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
h : j.castSucc < i
obtain : ∀ (i : Fin (n + 2)) (h : j.castSucc < i.succ), δ j ≫ toMk₁ i.succ = toMk₁ (i.succ.pred ⋯)
⊢ δ j ≫ toMk₁ i = toMk₁ (i.pred ⋯)

Tactic:
obtain ⟨i, rfl⟩ := Fin.eq_succ_of_ne_zero (Fin.ne_zero_of_lt h)

Premises used: Fin.eq_succ_of_ne_zero, Fin.ne_zero_of_lt, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
j i : Fin (n + 2)
h : j.castSucc < i.succ
rw : δ j ≫ toMk₁ i.succ = toMk₁ i
⊢ δ j ≫ toMk₁ i.succ = toMk₁ (i.succ.pred ⋯)

Tactic:
rw [Fin.pred_succ]

Premises used: Fin.pred_succ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
j i : Fin (n + 2)
h : j.castSucc < i.succ
⊢ δ j ≫ toMk₁ i.succ = toMk₁ i

Tactic:
ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
j i : Fin (n + 2)
h : j.castSucc < i.succ
refine :
  ∀ (k : 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)) (δ j ≫ toMk₁ i.succ) :
            (a : Fin (⦋n⦌.len + 1)) → Fin (⦋1⦌.len + 1))
          k :
        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)) (toMk₁ i) :
            (a : Fin (⦋n⦌.len + 1)) → Fin (⦋1⦌.len + 1))
          k :
        Fin (⦋1⦌.len + 1))
⊢ δ j ≫ toMk₁ i.succ = toMk₁ i

Tactic:
refine ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
j i : Fin (n + 2)
h : j.castSucc < i.succ
k : Fin (⦋n⦌.len + 1)
change :
  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)) (toMk₁ i.succ) :
          (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n + 1⦌) →
            (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
        (j.succAbove k) :
      (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)) (toMk₁ i) :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋1⦌.len + 1))
        k :
      Fin (⦋1⦌.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)) (δ j ≫ toMk₁ i.succ) :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋1⦌.len + 1))
        k :
      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)) (toMk₁ i) :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋1⦌.len + 1))
        k :
      Fin (⦋1⦌.len + 1))

Tactic:
change toMk₁ i.succ (j.succAbove k) = _

Premises used: Fin.succAbove, Fin.succ, SimplexCategory.toMk₁, CategoryTheory.ConcreteCategory.hom, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
j i : Fin (n + 2)
h : j.castSucc < i.succ
k : Fin (⦋n⦌.len + 1)
rw : (j.succAbove k).castSucc < i.succ ↔ k.castSucc < i
⊢ Eq (α := 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)) (toMk₁ i.succ) :
          (a : Fin (n + 1 + 1)) → Fin 2)
        (j.succAbove k) :
      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)) (toMk₁ i) :
          (a : Fin (n + 1)) → Fin 2)
        k :
      Fin 2)

Tactic:
rw [Fin.eq_iff_eq_zero_iff, toMk₁_apply_eq_zero_iff, toMk₁_apply_eq_zero_iff]

Premises used: SimplexCategory.toMk₁_apply_eq_zero_iff, Fin.eq_iff_eq_zero_iff
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
j i : Fin (n + 2)
h : j.castSucc < i.succ
k : Fin (⦋n⦌.len + 1)
⊢ (j.succAbove k).castSucc < i.succ ↔ k.castSucc < i

Tactic:
grind [Fin.succAbove]

Premises used: Fin.succAbove
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
⊢ σ j ≫ toMk₁ i = toMk₁ i.castSucc

Tactic:
ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
refine :
  ∀ (k : Fin (⦋n + 1⦌.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)) (σ j ≫ toMk₁ i) :
            (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋1⦌.len + 1))
          k :
        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)) (toMk₁ i.castSucc) :
            (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋1⦌.len + 1))
          k :
        Fin (⦋1⦌.len + 1))
⊢ σ j ≫ toMk₁ i = toMk₁ i.castSucc

Tactic:
refine ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
change :
  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)) (toMk₁ i) :
          (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
        (j.predAbove k) :
      (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)) (toMk₁ i.castSucc) :
          (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋1⦌.len + 1))
        k :
      Fin (⦋1⦌.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)) (σ j ≫ toMk₁ i) :
          (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋1⦌.len + 1))
        k :
      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)) (toMk₁ i.castSucc) :
          (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋1⦌.len + 1))
        k :
      Fin (⦋1⦌.len + 1))

Tactic:
change toMk₁ i (j.predAbove k) = _

Premises used: SimplexCategory.toMk₁, CategoryTheory.ConcreteCategory.hom, Fin.predAbove, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
pos :
  ∀ (hk : k < i),
    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)) (toMk₁ i) :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
          (j.predAbove k) :
        (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)) (toMk₁ i.castSucc) :
            (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋1⦌.len + 1))
          k :
        Fin (⦋1⦌.len + 1))
neg :
  ∀ (hk : i ≤ k),
    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)) (toMk₁ i) :
            (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
          (j.predAbove k) :
        (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)) (toMk₁ i.castSucc) :
            (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋1⦌.len + 1))
          k :
        Fin (⦋1⦌.len + 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)) (toMk₁ i) :
          (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋n⦌) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)
        (j.predAbove k) :
      (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)) (toMk₁ i.castSucc) :
          (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋1⦌.len + 1))
        k :
      Fin (⦋1⦌.len + 1))

Tactic:
by_cases! hk : k < i
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hk : k < i
⊢ Eq (α := 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)) (toMk₁ i) :
          (a : Fin (n + 1)) → Fin 2)
        (j.predAbove k) :
      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)) (toMk₁ i.castSucc) :
          (a : Fin (n + 1 + 1)) → Fin 2)
        k :
      Fin 2)

Tactic:
grind [Fin.castPred, Fin.predAbove_of_le_castSucc, toMk₁_of_castSucc_lt]

Premises used: Fin.castPred, Fin.predAbove_of_le_castSucc, SimplexCategory.toMk₁_of_castSucc_lt
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hk : i ≤ k
⊢ i.castSucc ≤ k.castSucc

Tactic:
simpa
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hk : i ≤ k
neg : i ≤ (j.predAbove k).castSucc
⊢ Eq (α := 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)) (toMk₁ i) :
          (a : Fin (n + 1)) → Fin 2)
        (j.predAbove k) :
      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)) (toMk₁ i.castSucc) :
          (a : Fin (n + 1 + 1)) → Fin 2)
        k :
      Fin 2)

Tactic:
rw [toMk₁_of_le_castSucc, toMk₁_of_le_castSucc _ _ (by simpa)]

Premises used: SimplexCategory.toMk₁_of_le_castSucc
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hk : i ≤ k
pos : ∀ (hk' : k ≤ j.castSucc), i ≤ (j.predAbove k).castSucc
neg : ∀ (hk' : ¬k ≤ j.castSucc), i ≤ (j.predAbove k).castSucc
⊢ i ≤ (j.predAbove k).castSucc

Tactic:
by_cases hk' : k ≤ j.castSucc

Premises used: Fin.castSucc
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hk : i ≤ k
hk' : k ≤ j.castSucc
pos : i ≤ (k.castPred ⋯).castSucc
pos₁ pos₂ pos₃ pos₄ : i ≤ k
⊢ i ≤ (j.predAbove k).castSucc

Tactic:
rwa [Fin.predAbove_of_le_castSucc _ _ hk', Fin.castSucc_castPred]

Premises used: Fin.castSucc_castPred, Fin.predAbove_of_le_castSucc
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hk : i ≤ k
hk' : ¬k ≤ j.castSucc
⊢ i ≤ (j.predAbove k).castSucc

Tactic:
grind [Fin.predAbove]

Premises used: Fin.predAbove
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
⊢ σ j ≫ toMk₁ i = toMk₁ i.succ

Tactic:
ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
refine :
  ∀ (k : Fin (⦋n + 1⦌.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)) (σ j ≫ toMk₁ i) :
            (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋1⦌.len + 1))
          k :
        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)) (toMk₁ i.succ) :
            (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋1⦌.len + 1))
          k :
        Fin (⦋1⦌.len + 1))
⊢ σ j ≫ toMk₁ i = toMk₁ i.succ

Tactic:
refine ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)

Premises used: CategoryTheory.ConcreteCategory.hom_ext