awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
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.succ) :
          (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.succ) :
          (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 : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
pos :
  ∀ (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.succ) :
            (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋1⦌.len + 1))
          k :
        Fin (⦋1⦌.len + 1))
neg :
  ∀ (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.succ) :
            (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.succ) :
          (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋1⦌.len + 1))
        k :
      Fin (⦋1⦌.len + 1))

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

Tactic:
grind [Fin.predAbove_of_castSucc_lt, toMk₁_of_le_castSucc]

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

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

Tactic:
rw [toMk₁_of_castSucc_lt i.succ k (by simpa), toMk₁_of_castSucc_lt]

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

Tactic:
by_cases hk' : j.castSucc < k

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

Tactic:
rwa [Fin.predAbove_of_castSucc_lt _ _ hk', Fin.castSucc_pred_lt_iff]

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

Tactic:
simp only [not_lt] at hk'

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

Tactic:
rw [Fin.predAbove_of_le_castSucc _ _ hk']

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

Tactic:
simpa
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hk : k ≤ i
hk' : k ≤ j.castSucc
⊢ (k.castPred ⋯).castSucc < i

Tactic:
exact lt_of_le_of_lt (by simpa) h

Premises used: lt_of_le_of_lt
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i j : Fin (n + 2)
h : toMk₁ i = toMk₁ j
inr : ∀ (this : ∀ ⦃i j : Fin (n + 2)⦄ (h : toMk₁ i = toMk₁ j) (hij : i < j), i = j) (hij : ¬i < j), i = j
wlog : ∀ ⦃i j : Fin (n + 2)⦄ (h : toMk₁ i = toMk₁ j) (hij : i < j), i = j
⊢ i = j

Tactic:
wlog hij : i < j generalizing i j
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i j : Fin (n + 2)
h : toMk₁ i = toMk₁ j
this : ∀ ⦃i j : Fin (n + 2)⦄ (h : toMk₁ i = toMk₁ j) (hij : i < j), i = j
hij : ¬i < j
⊢ i = j

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i j : Fin (n + 2)
h : toMk₁ i = toMk₁ j
hij : i < j
dsimp : (↑j : ℕ) ≤ n + 1
⊢ (↑j : ℕ) ≤ ⦋n⦌.len + 1

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i j : Fin (n + 2)
h : toMk₁ i = toMk₁ j
hij : i < j
⊢ (↑j : ℕ) ≤ n + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i j : Fin (n + 2)
h : toMk₁ i = toMk₁ j
hij : i < j
⊢ 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)) (toMk₁ i) :
          (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)) (toMk₁ j) :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋1⦌.len + 1))
        ⟨(↑i : ℕ), ⋯⟩ :
      Fin (⦋1⦌.len + 1))

Tactic:
have := ConcreteCategory.congr_hom h ⟨i.1, lt_of_lt_of_le hij (by dsimp; lia)⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
Goal:
n : ℕ
i j : Fin (n + 2)
h : toMk₁ i = toMk₁ j
hij : i < j
this :
  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)) (toMk₁ i) :
          (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)) (toMk₁ j) :
          (a : Fin (⦋n⦌.len + 1)) → Fin (⦋1⦌.len + 1))
        ⟨(↑i : ℕ), ⋯⟩ :
      Fin (⦋1⦌.len + 1))
⊢ i = j

Tactic:
simp [toMk₁_apply, if_pos hij] at this

Premises used: if_pos, 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⦌)}
pos : ∀ (hS : S.Nonempty), ∃ (a : Fin (n + 2)), toMk₁ a = f
neg : ∀ (hS : ¬S.Nonempty), ∃ (a : Fin (n + 2)), toMk₁ a = f
⊢ ∃ (a : Fin (n + 2)), toMk₁ a = f

Tactic:
by_cases hS : S.Nonempty

Premises used: Finset.Nonempty
-- 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:
⟨(S.min' hS).castSucc, ConcreteCategory.hom_ext _ _ (fun i ↦ ?_)⟩

Premises used: Finset.min', Exists.intro, CategoryTheory.ConcreteCategory.hom_ext, Fin.castSucc
-- 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
pos :
  ∀ (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)) (toMk₁ (S.min' hS).castSucc) :
            (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 ⟨(S.min' hS).castSucc, 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)
pos :
  Eq (α := Fin 2) (if i.castSucc < (S.min' hS).castSucc 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)) (toMk₁ (S.min' hS).castSucc) :
          (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)
pos :
  ∀ (h : i.castSucc < (S.min' hS).castSucc),
    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 :
  ∀ (h : ¬i.castSucc < (S.min' hS).castSucc),
    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)
⊢ Eq (α := Fin 2) (if i.castSucc < (S.min' hS).castSucc 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:
split_ifs with h
-- 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)
h : i.castSucc < (S.min' hS).castSucc
hi : i ∈ S
⊢ S.min' ⋯ ≤ i

Tactic:
have := S.min'_le _ hi
-- 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)
h : i.castSucc < (S.min' hS).castSucc
hi : i ∈ S
this : S.min' ⋯ ≤ i
⊢ False

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
i : Fin (⦋n⦌.len + 1)
h : i.castSucc < (S.min' hS).castSucc
⊢ i ∉ S

Tactic:
have hi : i ∉ S := fun hi ↦ by have := S.min'_le _ hi; 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
i : Fin (⦋n⦌.len + 1)
h : i.castSucc < (S.min' hS).castSucc
hi : i ∉ S
⊢ ¬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)) f :
            (a : Fin (n + 1)) → Fin 2)
          i :
        Fin 2)
      (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋1⦌)

Tactic:
simp [S] at hi
-- 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)
h : i.castSucc < (S.min' hS).castSucc
hi :
  ¬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)) f :
            (a : Fin (n + 1)) → Fin 2)
          i :
        Fin 2)
      (1 : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) ⦋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:
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
i : Fin (⦋n⦌.len + 1)
h : ¬i.castSucc < (S.min' hS).castSucc
⊢ ∃ (x : Fin (n + 1)) (_ : x ∈ S), x ≤ i

Tactic:
simp only [Fin.castSucc_lt_castSucc_iff, Finset.lt_min'_iff, not_forall,
        not_lt] at h

Premises used: Fin.castSucc_lt_castSucc_iff, not_lt, Finset.lt_min'_iff, Classical.not_forall
-- 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)
h : ∃ (x : Fin (n + 1)) (_ : x ∈ S), x ≤ i
neg :
  ∀ (j : Fin (n + 1)) (hj : j ∈ S) (hij : j ≤ i),
    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)
⊢ 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:
obtain ⟨j, hj, hij⟩ := h