awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
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))
have 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))
Tactic: change toMk₁ i (j.predAbove k) = _
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 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))
have 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))
Tactic: by_cases! hk : i < k
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
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))
⊢ 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))
have 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))
Tactic: by_cases! hk : i < k
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
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.succ) :
          (a : Fin (n + 1 + 1)) → Fin 2)
        k :
      Fin 2)
have neg : (j.predAbove k).castSucc < i
Tactic: rw [toMk₁_of_castSucc_lt i.succ k (by simpa), toMk₁_of_castSucc_lt]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hk : k ≤ i
⊢ (j.predAbove k).castSucc < i
have pos : ∀ (hk' : j.castSucc < k), (j.predAbove k).castSucc < i
Tactic: by_cases hk' : j.castSucc < k
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
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
⊢ (j.predAbove k).castSucc < i
have neg : ∀ (hk' : ¬j.castSucc < k), (j.predAbove k).castSucc < i
Tactic: by_cases hk' : j.castSucc < k
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
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
⊢ (j.predAbove k).castSucc < i
have pos : (k.pred sorry).castSucc < i
Tactic: rwa [Fin.predAbove_of_castSucc_lt _ _ hk', Fin.castSucc_pred_lt_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (hypothesis)
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
⊢ (j.predAbove k).castSucc < i
have hk'₁ : k ≤ j.castSucc
Tactic: simp only [not_lt] at hk'
Cleared hypotheses: hk'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
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
⊢ (j.predAbove k).castSucc < i
have neg : (k.castPred sorry).castSucc < i
Tactic: rw [Fin.predAbove_of_le_castSucc _ _ hk']
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
Goal:
n : ℕ
i j : Fin (n + 2)
h : toMk₁ i = toMk₁ j
⊢ i = j
have inr : ∀ (this : ∀ ⦃i j : Fin (n + 2)⦄ (h : toMk₁ i = toMk₁ j) (hij : i < j), i = j) (hij : ¬i < j), i = j
Tactic: wlog hij : i < j generalizing i j
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
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
⊢ i = j
have wlog : ∀ ⦃i j : Fin (n + 2)⦄ (h : toMk₁ i = toMk₁ j) (hij : i < j), i = j
Tactic: wlog hij : i < j generalizing i j
Cleared hypotheses: i, j, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
Goal:
n : ℕ
i j : Fin (n + 2)
h : toMk₁ i = toMk₁ j
hij : i < j
⊢ (↑j : ℕ) ≤ ⦋n⦌.len + 1
have dsimp : (↑j : ℕ) ≤ n + 1
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (hypothesis)
Goal:
n : ℕ
i j : Fin (n + 2)
h : toMk₁ i = toMk₁ j
hij : i < j
⊢ i = j
have 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 : ℕ), sorry⟩ :
    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 : ℕ), sorry⟩ :
    Fin (⦋1⦌.len + 1))
Tactic: have := ConcreteCategory.congr_hom h ⟨i.1, lt_of_lt_of_le hij (by dsimp; lia)⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
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⦌)}
⊢ ∃ (a : Fin (n + 2)), toMk₁ a = f
have pos : ∀ (hS : S.Nonempty), ∃ (a : Fin (n + 2)), toMk₁ a = f
Tactic: by_cases hS : S.Nonempty
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
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
⊢ ∃ (a : Fin (n + 2)), toMk₁ a = f
have neg : ∀ (hS : ¬S.Nonempty), ∃ (a : Fin (n + 2)), toMk₁ a = f
Tactic: by_cases hS : S.Nonempty
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
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
have 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))
Tactic: refine ⟨(S.min' hS).castSucc, ConcreteCategory.hom_ext _ _ (fun i ↦ ?_)⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
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)
⊢ 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))
have 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)
Tactic: dsimp [toMk₁_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
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)
⊢ 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)
have 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)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
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)
⊢ 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)
have 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)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (hypothesis)
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
⊢ False
have this : S.min' sorry ≤ i
Tactic: have := S.min'_le _ hi
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (hypothesis)
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
⊢ 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)
have hi : i ∉ S
Tactic: have hi : i ∉ S := fun hi ↦ by have := S.min'_le _ hi; grind
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (hypothesis)
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) (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)
have 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⦌)
Tactic: simp [S] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (hypothesis)
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
⊢ 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)
have h₁ : ∃ (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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
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
⊢ 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)
have 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)
Tactic: obtain ⟨j, hj, hij⟩ := h
Cleared hypotheses: h