awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Rev (goal)
Goal:
n : ℕ
i : Fin (n + 1)
⊢ rev.map (σ i) = σ i.rev
have a : ∀ (j : Fin ((rev.obj { len := n + 1 : SimplexCategory }).len + 1)),
  Eq (α := Fin ((rev.obj { len := n : SimplexCategory }).len + 1))
    ((Hom.toOrderHom (rev.map (σ i)) :
          (a : Fin ((rev.obj { len := n + 1 }).len + 1)) → Fin ((rev.obj { len := n }).len + 1))
        j :
      Fin ((rev.obj { len := n : SimplexCategory }).len + 1))
    ((Hom.toOrderHom (σ i.rev) : (a : Fin ((rev.obj { len := n + 1 }).len + 1)) → Fin ((rev.obj { len := n }).len + 1))
        j :
      Fin ((rev.obj { len := n : SimplexCategory }).len + 1))
Tactic: ext j : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Rev (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin ((rev.obj { len := n + 1 : SimplexCategory }).len + 1)
⊢ Eq (α := Fin ((rev.obj { len := n : SimplexCategory }).len + 1))
    ((Hom.toOrderHom (rev.map (σ i)) :
          (a : Fin ((rev.obj { len := n + 1 }).len + 1)) → Fin ((rev.obj { len := n }).len + 1))
        j :
      Fin ((rev.obj { len := n : SimplexCategory }).len + 1))
    ((Hom.toOrderHom (σ i.rev) : (a : Fin ((rev.obj { len := n + 1 }).len + 1)) → Fin ((rev.obj { len := n }).len + 1))
        j :
      Fin ((rev.obj { len := n : SimplexCategory }).len + 1))
have a : Eq (α := Fin ((rev.obj { len := n : SimplexCategory }).len + 1))
  (Fin.rev
    ((Hom.toOrderHom (σ i) : (a : Fin ((rev.obj { len := n + 1 }).len + 1)) → Fin ((rev.obj { len := n }).len + 1))
      j.rev))
  ((Hom.toOrderHom (σ i.rev) : (a : Fin ((rev.obj { len := n + 1 }).len + 1)) → Fin ((rev.obj { len := n }).len + 1)) j)
Tactic: rw [rev_map_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Rev (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin ((rev.obj { len := n + 1 : SimplexCategory }).len + 1)
⊢ Eq (α := Fin ((rev.obj { len := n : SimplexCategory }).len + 1))
    (Fin.rev
      ((Hom.toOrderHom (σ i) : (a : Fin ((rev.obj { len := n + 1 }).len + 1)) → Fin ((rev.obj { len := n }).len + 1))
        j.rev))
    ((Hom.toOrderHom (σ i.rev) : (a : Fin ((rev.obj { len := n + 1 }).len + 1)) → Fin ((rev.obj { len := n }).len + 1))
      j)
have a : (i.predAbove j.rev).rev = i.rev.predAbove j
Tactic: dsimp [σ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Rev (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin ((rev.obj { len := n + 1 : SimplexCategory }).len + 1)
⊢ (i.predAbove j.rev).rev = i.rev.predAbove j
have a : (i.rev.predAbove j).rev.rev = i.rev.predAbove j
Tactic: rw [Fin.predAbove_rev_right, Fin.rev_rev]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Rev (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin ((rev.obj { len := n + 1 : SimplexCategory }).len + 1)
a : (i.rev.predAbove j).rev.rev = i.rev.predAbove j
⊢ (i.predAbove j.rev).rev = i.rev.predAbove j
have a₁ : i.rev.predAbove j = i.rev.predAbove j
Tactic: rw [Fin.predAbove_rev_right, Fin.rev_rev]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory (goal)
Goal:
X Y : SemiSimplexCategory
a₁ a₂ : X ⟶ Y
h : toSimplexCategory.map a₁ = toSimplexCategory.map a₂
⊢ a₁ = a₂
have h₁ : ∀ (x : Fin (X.len + 1)),
  Eq (α := Fin (Y.len + 1))
    ((((homEquiv : (a : X ⟶ Y) → Fin (X.len + 1) ↪o Fin (Y.len + 1)) a₁ : Fin (X.len + 1) ↪o Fin (Y.len + 1)) :
          (a : Fin (X.len + 1)) → Fin (Y.len + 1))
        x :
      Fin (Y.len + 1))
    ((((homEquiv : (a : X ⟶ Y) → Fin (X.len + 1) ↪o Fin (Y.len + 1)) a₂ : Fin (X.len + 1) ↪o Fin (Y.len + 1)) :
          (a : Fin (X.len + 1)) → Fin (Y.len + 1))
        x :
      Fin (Y.len + 1))
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory (goal)
Goal:
n m : SemiSimplexCategory
f : n ⟶ m
⊢ Mono (toSimplexCategory.map f)
have rw : Function.Injective (α := Fin ((toSimplexCategory.obj n).len + 1)) (β := Fin ((toSimplexCategory.obj m).len + 1))
  (⇑(SimplexCategory.Hom.toOrderHom (toSimplexCategory.map f)) :
    (a : Fin ((toSimplexCategory.obj n).len + 1)) → Fin ((toSimplexCategory.obj m).len + 1))
Tactic: rw [SimplexCategory.mono_iff_injective]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory (goal)
Goal:
n m : SemiSimplexCategory
f : n ⟶ m
Z : SemiSimplexCategory
g₁ g₂ : Z ⟶ n
h : g₁ ≫ f = g₂ ≫ f
⊢ g₁ = g₂
have a : toSimplexCategory.map g₁ = toSimplexCategory.map g₂
Tactic: apply toSimplexCategory.map_injective
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin (⦋n⦌.len + 1)
h : j₁ ≤ j₂
⊢ LE.le (α := Fin 2) (if j₁.castSucc < i then 0 else 1) (if j₂.castSucc < i then 0 else 1)
have pos : j₁.castSucc < i → j₂.castSucc < i → LE.le (α := Fin 2) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
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
⊢ LE.le (α := Fin 2) (if j₁.castSucc < i then 0 else 1) (if j₂.castSucc < i then 0 else 1)
have neg : j₁.castSucc < i → ¬j₂.castSucc < i → LE.le (α := Fin 2) 0 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
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
⊢ LE.le (α := Fin 2) (if j₁.castSucc < i then 0 else 1) (if j₂.castSucc < i then 0 else 1)
have pos₁ : ¬j₁.castSucc < i → j₂.castSucc < i → LE.le (α := Fin 2) 1 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
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
⊢ LE.le (α := Fin 2) (if j₁.castSucc < i then 0 else 1) (if j₂.castSucc < i then 0 else 1)
have neg₁ : ¬j₁.castSucc < i → ¬j₂.castSucc < i → LE.le (α := Fin 2) 1 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
Goal:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
h : i ≤ j.castSucc
⊢ δ j ≫ toMk₁ i = toMk₁ (i.castPred ⋯)
have obtain : ∀ (i : Fin (n + 2)) (h : i.castSucc ≤ j.castSucc), δ j ≫ toMk₁ i.castSucc = toMk₁ (i.castSucc.castPred sorry)
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))
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (hypothesis)
Goal:
n : ℕ
j i : Fin (n + 2)
h : i.castSucc ≤ j.castSucc
⊢ δ j ≫ toMk₁ i.castSucc = toMk₁ (i.castSucc.castPred ⋯)
have h₁ : i ≤ j
Tactic: simp only [Fin.castSucc_le_castSucc_iff] at h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
Goal:
n : ℕ
j i : Fin (n + 2)
h_1 : i.castSucc ≤ j.castSucc
h : i ≤ j
⊢ δ j ≫ toMk₁ i.castSucc = toMk₁ (i.castSucc.castPred ⋯)
have rw : δ j ≫ toMk₁ i.castSucc = toMk₁ i
Tactic: rw [Fin.castPred_castSucc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
Goal:
n : ℕ
j i : Fin (n + 2)
h_1 : i.castSucc ≤ j.castSucc
h : i ≤ j
⊢ δ j ≫ toMk₁ i.castSucc = toMk₁ i
have 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))
Tactic: refine ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
Goal:
n : ℕ
j i : Fin (n + 2)
h_1 : i.castSucc ≤ j.castSucc
h : i ≤ j
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))
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.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))
Tactic: change toMk₁ i.castSucc (j.succAbove k) = _
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
Goal:
n : ℕ
j i : Fin (n + 2)
h_1 : i.castSucc ≤ j.castSucc
h : i ≤ j
k : Fin (⦋n⦌.len + 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.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)
have rw : (j.succAbove k).castSucc < i.castSucc ↔ k.castSucc < i
Tactic: rw [Fin.eq_iff_eq_zero_iff, toMk₁_apply_eq_zero_iff, toMk₁_apply_eq_zero_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
Goal:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
h : j.castSucc < i
⊢ δ j ≫ toMk₁ i = toMk₁ (i.pred ⋯)
have obtain : ∀ (i : Fin (n + 2)) (h : j.castSucc < i.succ), δ j ≫ toMk₁ i.succ = toMk₁ (i.succ.pred sorry)
Tactic: obtain ⟨i, rfl⟩ := Fin.eq_succ_of_ne_zero (Fin.ne_zero_of_lt h)
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
Goal:
n : ℕ
j i : Fin (n + 2)
h : j.castSucc < i.succ
⊢ δ j ≫ toMk₁ i.succ = toMk₁ (i.succ.pred ⋯)
have rw : δ j ≫ toMk₁ i.succ = toMk₁ i
Tactic: rw [Fin.pred_succ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
Goal:
n : ℕ
j i : Fin (n + 2)
h : j.castSucc < i.succ
⊢ δ j ≫ toMk₁ i.succ = toMk₁ i
have 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))
Tactic: refine ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
Goal:
n : ℕ
j i : Fin (n + 2)
h : j.castSucc < i.succ
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))
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.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))
Tactic: change toMk₁ i.succ (j.succAbove k) = _
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
Goal:
n : ℕ
j i : Fin (n + 2)
h : j.castSucc < i.succ
k : Fin (⦋n⦌.len + 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.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)
have rw : (j.succAbove k).castSucc < i.succ ↔ k.castSucc < i
Tactic: rw [Fin.eq_iff_eq_zero_iff, toMk₁_apply_eq_zero_iff, toMk₁_apply_eq_zero_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
⊢ σ j ≫ toMk₁ i = toMk₁ i.castSucc
have 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))
Tactic: refine ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
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))
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.castSucc) :
        (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 : i ≤ j.castSucc
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.castSucc) :
          (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋1⦌.len + 1))
        k :
      Fin (⦋1⦌.len + 1))
have 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))
Tactic: by_cases! hk : k < i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
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))
⊢ 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))
have 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))
Tactic: by_cases! hk : k < i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
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.castSucc) :
          (a : Fin (n + 1 + 1)) → Fin 2)
        k :
      Fin 2)
have neg : i ≤ (j.predAbove k).castSucc
Tactic: rw [toMk₁_of_le_castSucc, toMk₁_of_le_castSucc _ _ (by simpa)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hk : i ≤ k
⊢ i ≤ (j.predAbove k).castSucc
have pos : ∀ (hk' : k ≤ j.castSucc), i ≤ (j.predAbove k).castSucc
Tactic: by_cases hk' : k ≤ j.castSucc
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
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
⊢ i ≤ (j.predAbove k).castSucc
have neg : ∀ (hk' : ¬k ≤ j.castSucc), i ≤ (j.predAbove k).castSucc
Tactic: by_cases hk' : k ≤ j.castSucc
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
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
have pos : i ≤ (k.castPred sorry).castSucc
Tactic: rwa [Fin.predAbove_of_le_castSucc _ _ hk', Fin.castSucc_castPred]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
⊢ σ j ≫ toMk₁ i = toMk₁ i.succ
have 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))
Tactic: refine ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)