awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
j : Fin (n + 2)
k : Fin (⦋n⦌.len + 1)
i : ℕ
isLt : i < n + 2
H : (⟨i, isLt⟩ : Fin (n + 2)) ≤ j
⊢ (↑(if (if k.castSucc < (⟨i, isLt⟩ : Fin (n + 2)) then k.castSucc else k.succ).castSucc < j.succ then
          (if k.castSucc < (⟨i, isLt⟩ : Fin (n + 2)) then k.castSucc else k.succ).castSucc
        else (if k.castSucc < (⟨i, isLt⟩ : Fin (n + 2)) then k.castSucc else k.succ).succ) :
      ℕ) =
    (↑(if (if k.castSucc < j then k.castSucc else k.succ).castSucc < (⟨i, isLt⟩ : Fin (n + 2)).castSucc then
          (if k.castSucc < j then k.castSucc else k.succ).castSucc
        else (if k.castSucc < j then k.castSucc else k.succ).succ) :
      ℕ)
have a : ∀ (j : ℕ) (isLt_1 : j < n + 2) (H : (⟨i, isLt⟩ : Fin (n + 2)) ≤ ⟨j, isLt_1⟩),
  (↑(if
            (if k.castSucc < (⟨i, isLt⟩ : Fin (n + 2)) then k.castSucc else k.succ).castSucc <
              (⟨j, isLt_1⟩ : Fin (n + 2)).succ then
          (if k.castSucc < (⟨i, isLt⟩ : Fin (n + 2)) then k.castSucc else k.succ).castSucc
        else (if k.castSucc < (⟨i, isLt⟩ : Fin (n + 2)) then k.castSucc else k.succ).succ) :
      ℕ) =
    (↑(if
            (if k.castSucc < (⟨j, isLt_1⟩ : Fin (n + 2)) then k.castSucc else k.succ).castSucc <
              (⟨i, isLt⟩ : Fin (n + 2)).castSucc then
          (if k.castSucc < (⟨j, isLt_1⟩ : Fin (n + 2)) then k.castSucc else k.succ).castSucc
        else (if k.castSucc < (⟨j, isLt_1⟩ : Fin (n + 2)) then k.castSucc else k.succ).succ) :
      ℕ)
Tactic: rcases j with ⟨j, _⟩
Cleared hypotheses: j, H
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
k : Fin (⦋n⦌.len + 1)
i : ℕ
isLt : i < n + 2
j : ℕ
isLt_1 : j < n + 2
H : (⟨i, isLt⟩ : Fin (n + 2)) ≤ ⟨j, isLt_1⟩
⊢ (↑(if
            (if k.castSucc < (⟨i, isLt⟩ : Fin (n + 2)) then k.castSucc else k.succ).castSucc <
              (⟨j, isLt_1⟩ : Fin (n + 2)).succ then
          (if k.castSucc < (⟨i, isLt⟩ : Fin (n + 2)) then k.castSucc else k.succ).castSucc
        else (if k.castSucc < (⟨i, isLt⟩ : Fin (n + 2)) then k.castSucc else k.succ).succ) :
      ℕ) =
    (↑(if
            (if k.castSucc < (⟨j, isLt_1⟩ : Fin (n + 2)) then k.castSucc else k.succ).castSucc <
              (⟨i, isLt⟩ : Fin (n + 2)).castSucc then
          (if k.castSucc < (⟨j, isLt_1⟩ : Fin (n + 2)) then k.castSucc else k.succ).castSucc
        else (if k.castSucc < (⟨j, isLt_1⟩ : Fin (n + 2)) then k.castSucc else k.succ).succ) :
      ℕ)
have a : ∀ (k : ℕ) (isLt_2 : k < ⦋n⦌.len + 1),
  (↑(if
            (if (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < (⟨i, isLt⟩ : Fin (n + 2)) then
                  (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc
                else (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ).castSucc <
              (⟨j, isLt_1⟩ : Fin (n + 2)).succ then
          (if (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < (⟨i, isLt⟩ : Fin (n + 2)) then
              (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc
            else (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ).castSucc
        else
          (if (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < (⟨i, isLt⟩ : Fin (n + 2)) then
              (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc
            else (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ).succ) :
      ℕ) =
    (↑(if
            (if (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < (⟨j, isLt_1⟩ : Fin (n + 2)) then
                  (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc
                else (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ).castSucc <
              (⟨i, isLt⟩ : Fin (n + 2)).castSucc then
          (if (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < (⟨j, isLt_1⟩ : Fin (n + 2)) then
              (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc
            else (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ).castSucc
        else
          (if (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < (⟨j, isLt_1⟩ : Fin (n + 2)) then
              (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc
            else (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ).succ) :
      ℕ)
Tactic: rcases k with ⟨k, _⟩
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n i : ℕ
isLt : i < n + 2
j : ℕ
isLt_1 : j < n + 2
H : (⟨i, isLt⟩ : Fin (n + 2)) ≤ ⟨j, isLt_1⟩
k : ℕ
isLt_2 : k < ⦋n⦌.len + 1
⊢ (↑(if
            (if (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < (⟨i, isLt⟩ : Fin (n + 2)) then
                  (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc
                else (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ).castSucc <
              (⟨j, isLt_1⟩ : Fin (n + 2)).succ then
          (if (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < (⟨i, isLt⟩ : Fin (n + 2)) then
              (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc
            else (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ).castSucc
        else
          (if (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < (⟨i, isLt⟩ : Fin (n + 2)) then
              (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc
            else (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ).succ) :
      ℕ) =
    (↑(if
            (if (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < (⟨j, isLt_1⟩ : Fin (n + 2)) then
                  (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc
                else (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ).castSucc <
              (⟨i, isLt⟩ : Fin (n + 2)).castSucc then
          (if (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < (⟨j, isLt_1⟩ : Fin (n + 2)) then
              (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc
            else (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ).castSucc
        else
          (if (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < (⟨j, isLt_1⟩ : Fin (n + 2)) then
              (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc
            else (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ).succ) :
      ℕ)
have pos : (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨i, isLt⟩ →
  (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨j, isLt_1⟩.succ →
    (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨j, isLt_1⟩ →
      (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨i, isLt⟩.castSucc →
        (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc : ℕ) =
          (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc : ℕ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n i : ℕ
isLt : i < n + 2
j : ℕ
isLt_1 : j < n + 2
H : (⟨i, isLt⟩ : Fin (n + 2)) ≤ ⟨j, isLt_1⟩
k : ℕ
isLt_2 : k < ⦋n⦌.len + 1
pos :
  (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨i, isLt⟩ →
    (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨j, isLt_1⟩.succ →
      (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨j, isLt_1⟩ →
        (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨i, isLt⟩.castSucc →
          (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc : ℕ) =
            (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc : ℕ)
⊢ (↑(if
            (if (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < (⟨i, isLt⟩ : Fin (n + 2)) then
                  (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc
                else (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ).castSucc <
              (⟨j, isLt_1⟩ : Fin (n + 2)).succ then
          (if (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < (⟨i, isLt⟩ : Fin (n + 2)) then
              (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc
            else (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ).castSucc
        else
          (if (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < (⟨i, isLt⟩ : Fin (n + 2)) then
              (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc
            else (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ).succ) :
      ℕ) =
    (↑(if
            (if (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < (⟨j, isLt_1⟩ : Fin (n + 2)) then
                  (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc
                else (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ).castSucc <
              (⟨i, isLt⟩ : Fin (n + 2)).castSucc then
          (if (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < (⟨j, isLt_1⟩ : Fin (n + 2)) then
              (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc
            else (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ).castSucc
        else
          (if (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < (⟨j, isLt_1⟩ : Fin (n + 2)) then
              (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc
            else (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ).succ) :
      ℕ)
have neg : (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨i, isLt⟩ →
  (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨j, isLt_1⟩.succ →
    (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨j, isLt_1⟩ →
      ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨i, isLt⟩.castSucc →
        (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc : ℕ) =
          (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.succ : ℕ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n i : ℕ
isLt : i < n + 2
j : ℕ
isLt_1 : j < n + 2
H : (⟨i, isLt⟩ : Fin (n + 2)) ≤ ⟨j, isLt_1⟩
k : ℕ
isLt_2 : k < ⦋n⦌.len + 1
pos :
  (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨i, isLt⟩ →
    (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨j, isLt_1⟩.succ →
      (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨j, isLt_1⟩ →
        (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨i, isLt⟩.castSucc →
          (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc : ℕ) =
            (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc : ℕ)
neg :
  (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨i, isLt⟩ →
    (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨j, isLt_1⟩.succ →
      (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨j, isLt_1⟩ →
        ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨i, isLt⟩.castSucc →
          (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc : ℕ) =
            (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.succ : ℕ)
⊢ (↑(if
            (if (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < (⟨i, isLt⟩ : Fin (n + 2)) then
                  (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc
                else (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ).castSucc <
              (⟨j, isLt_1⟩ : Fin (n + 2)).succ then
          (if (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < (⟨i, isLt⟩ : Fin (n + 2)) then
              (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc
            else (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ).castSucc
        else
          (if (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < (⟨i, isLt⟩ : Fin (n + 2)) then
              (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc
            else (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ).succ) :
      ℕ) =
    (↑(if
            (if (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < (⟨j, isLt_1⟩ : Fin (n + 2)) then
                  (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc
                else (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ).castSucc <
              (⟨i, isLt⟩ : Fin (n + 2)).castSucc then
          (if (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < (⟨j, isLt_1⟩ : Fin (n + 2)) then
              (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc
            else (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ).castSucc
        else
          (if (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < (⟨j, isLt_1⟩ : Fin (n + 2)) then
              (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc
            else (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ).succ) :
      ℕ)
have pos₁ : (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨i, isLt⟩ →
  (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨j, isLt_1⟩.succ →
    ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨j, isLt_1⟩ →
      (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.castSucc < ⟨i, isLt⟩.castSucc →
        (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc : ℕ) =
          (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.castSucc : ℕ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n i : ℕ
isLt : i < n + 2
j : ℕ
isLt_1 : j < n + 2
H : (⟨i, isLt⟩ : Fin (n + 2)) ≤ ⟨j, isLt_1⟩
k : ℕ
isLt_2 : k < ⦋n⦌.len + 1
h : (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨i, isLt⟩
h_1 : (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨j, isLt_1⟩.succ
h_2 : (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨j, isLt_1⟩
h_3 : ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨i, isLt⟩.castSucc
⊢ (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc : ℕ) = (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.succ : ℕ)
have neg : ∀ (H : i ≤ j), k < i → k < j + 1 → k < j → i ≤ k → False
Tactic: simp at *
Cleared hypotheses: H, h, h_1, h_2, h_3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n i : ℕ
isLt : i < n + 2
j : ℕ
isLt_1 : j < n + 2
H : (⟨i, isLt⟩ : Fin (n + 2)) ≤ ⟨j, isLt_1⟩
k : ℕ
isLt_2 : k < ⦋n⦌.len + 1
h : (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨i, isLt⟩
h_1 : (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨j, isLt_1⟩.succ
h_2 : ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨j, isLt_1⟩
h_3 : (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.castSucc < ⟨i, isLt⟩.castSucc
⊢ (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc : ℕ) = (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.castSucc : ℕ)
have pos : ∀ (H : i ≤ j), k < i → k < j + 1 → j ≤ k → k + 1 < i → False
Tactic: simp at *
Cleared hypotheses: H, h, h_1, h_2, h_3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n i : ℕ
isLt : i < n + 2
j : ℕ
isLt_1 : j < n + 2
H : (⟨i, isLt⟩ : Fin (n + 2)) ≤ ⟨j, isLt_1⟩
k : ℕ
isLt_2 : k < ⦋n⦌.len + 1
h : (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨i, isLt⟩
h_1 : (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨j, isLt_1⟩.succ
h_2 : ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨j, isLt_1⟩
h_3 : ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.castSucc < ⟨i, isLt⟩.castSucc
⊢ (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc : ℕ) = (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.succ : ℕ)
have neg : ∀ (H : i ≤ j), k < i → k < j + 1 → j ≤ k → i ≤ k + 1 → k = k + 1 + 1
Tactic: simp at *
Cleared hypotheses: H, h, h_1, h_2, h_3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n i : ℕ
isLt : i < n + 2
j : ℕ
isLt_1 : j < n + 2
H : (⟨i, isLt⟩ : Fin (n + 2)) ≤ ⟨j, isLt_1⟩
k : ℕ
isLt_2 : k < ⦋n⦌.len + 1
h : (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨i, isLt⟩
h_1 : ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨j, isLt_1⟩.succ
h_2 : (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨j, isLt_1⟩
h_3 : (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨i, isLt⟩.castSucc
⊢ (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.succ : ℕ) = (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc : ℕ)
have pos : ∀ (H : i ≤ j), k < i → j + 1 ≤ k → k < j → k < i → False
Tactic: simp at *
Cleared hypotheses: H, h, h_1, h_2, h_3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n i : ℕ
isLt : i < n + 2
j : ℕ
isLt_1 : j < n + 2
H : (⟨i, isLt⟩ : Fin (n + 2)) ≤ ⟨j, isLt_1⟩
k : ℕ
isLt_2 : k < ⦋n⦌.len + 1
h : (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨i, isLt⟩
h_1 : ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨j, isLt_1⟩.succ
h_2 : ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨j, isLt_1⟩
h_3 : ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.castSucc < ⟨i, isLt⟩.castSucc
⊢ (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.succ : ℕ) = (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.succ : ℕ)
have neg : ∀ (H : i ≤ j), k < i → j + 1 ≤ k → j ≤ k → i ≤ k + 1 → False
Tactic: simp at *
Cleared hypotheses: H, h, h_1, h_2, h_3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n i : ℕ
isLt : i < n + 2
j : ℕ
isLt_1 : j < n + 2
H : (⟨i, isLt⟩ : Fin (n + 2)) ≤ ⟨j, isLt_1⟩
k : ℕ
isLt_2 : k < ⦋n⦌.len + 1
h : ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨i, isLt⟩
h_1 : (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.castSucc < ⟨j, isLt_1⟩.succ
h_2 : (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨j, isLt_1⟩
h_3 : (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨i, isLt⟩.castSucc
⊢ (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.castSucc : ℕ) = (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc : ℕ)
have pos : ∀ (H : i ≤ j), i ≤ k → k < j → k < j → k < i → False
Tactic: simp at *
Cleared hypotheses: H, h, h_1, h_2, h_3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n i : ℕ
isLt : i < n + 2
j : ℕ
isLt_1 : j < n + 2
H : (⟨i, isLt⟩ : Fin (n + 2)) ≤ ⟨j, isLt_1⟩
k : ℕ
isLt_2 : k < ⦋n⦌.len + 1
h : ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨i, isLt⟩
h_1 : (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.castSucc < ⟨j, isLt_1⟩.succ
h_2 : ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨j, isLt_1⟩
h_3 : ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.castSucc < ⟨i, isLt⟩.castSucc
⊢ (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.castSucc : ℕ) = (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.succ : ℕ)
have neg : ∀ (H : i ≤ j), i ≤ k → k < j → j ≤ k → i ≤ k + 1 → False
Tactic: simp at *
Cleared hypotheses: H, h, h_1, h_2, h_3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n i : ℕ
isLt : i < n + 2
j : ℕ
isLt_1 : j < n + 2
H : (⟨i, isLt⟩ : Fin (n + 2)) ≤ ⟨j, isLt_1⟩
k : ℕ
isLt_2 : k < ⦋n⦌.len + 1
h : ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨i, isLt⟩
h_1 : ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.castSucc < ⟨j, isLt_1⟩.succ
h_2 : (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨j, isLt_1⟩
h_3 : (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨i, isLt⟩.castSucc
⊢ (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.succ : ℕ) = (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc : ℕ)
have pos : ∀ (H : i ≤ j), i ≤ k → j ≤ k → k < j → k < i → k + 1 + 1 = k
Tactic: simp at *
Cleared hypotheses: H, h, h_1, h_2, h_3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n i : ℕ
isLt : i < n + 2
j : ℕ
isLt_1 : j < n + 2
H : (⟨i, isLt⟩ : Fin (n + 2)) ≤ ⟨j, isLt_1⟩
k : ℕ
isLt_2 : k < ⦋n⦌.len + 1
h : ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨i, isLt⟩
h_1 : ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.castSucc < ⟨j, isLt_1⟩.succ
h_2 : (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨j, isLt_1⟩
h_3 : ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc < ⟨i, isLt⟩.castSucc
⊢ (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.succ : ℕ) = (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.succ : ℕ)
have neg : ∀ (H : i ≤ j), i ≤ k → j ≤ k → k < j → i ≤ k → False
Tactic: simp at *
Cleared hypotheses: H, h, h_1, h_2, h_3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n i : ℕ
isLt : i < n + 2
j : ℕ
isLt_1 : j < n + 2
H : (⟨i, isLt⟩ : Fin (n + 2)) ≤ ⟨j, isLt_1⟩
k : ℕ
isLt_2 : k < ⦋n⦌.len + 1
h : ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨i, isLt⟩
h_1 : ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.castSucc < ⟨j, isLt_1⟩.succ
h_2 : ¬(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc < ⟨j, isLt_1⟩
h_3 : (⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.castSucc < ⟨i, isLt⟩.castSucc
⊢ (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.succ : ℕ) = (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.castSucc : ℕ)
have pos : ∀ (H : i ≤ j), i ≤ k → j ≤ k → j ≤ k → k + 1 < i → False
Tactic: simp at *
Cleared hypotheses: H, h, h_1, h_2, h_3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
⊢ δ i ≫ δ j = δ (j.pred ⋯) ≫ δ i.castSucc
have rw : δ i ≫ δ j = δ i ≫ δ (j.pred sorry).succ
Tactic: rw [← δ_comp_δ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
rw : δ i ≫ δ j = δ i ≫ δ (j.pred ⋯).succ
⊢ δ i ≫ δ j = δ (j.pred ⋯) ≫ δ i.castSucc
have rw₁ : i ≤ j.pred sorry
Tactic: rw [← δ_comp_δ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
⊢ δ i ≫ δ j = δ i ≫ δ (j.pred ⋯).succ
have rw : δ i ≫ δ j = δ i ≫ δ j
Tactic: rw [Fin.succ_pred]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
⊢ δ (i.castLT ⋯) ≫ δ j.succ = δ j ≫ δ i
have rw : δ j ≫ δ (i.castLT sorry).castSucc = δ j ≫ δ i
Tactic: rw [δ_comp_δ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
rw : δ j ≫ δ (i.castLT ⋯).castSucc = δ j ≫ δ i
⊢ δ (i.castLT ⋯) ≫ δ j.succ = δ j ≫ δ i
have rw₁ : i.castLT sorry ≤ j
Tactic: rw [δ_comp_δ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : j = i.castSucc
⊢ δ i ≫ δ j = δ i ≫ δ i.succ
have subst : δ i ≫ δ i.castSucc = δ i ≫ δ i.succ
Tactic: subst H
Cleared hypotheses: j, H
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
⊢ δ i ≫ δ i.castSucc = δ i ≫ δ i.succ
have rw : δ i ≫ δ i.succ = δ i ≫ δ i.succ
Tactic: rw [δ_comp_δ_self]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
⊢ δ i.castSucc ≫ σ j.succ = σ j ≫ δ i
have a : ∀ (k : Fin (⦋n + 1⦌.len + 1)),
  Eq (α := Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom (δ i.castSucc ≫ σ j.succ) : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k :
      Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom (σ j ≫ δ i) : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k : Fin (⦋n + 1⦌.len + 1))
Tactic: ext k : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
⊢ Eq (α := Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom (δ i.castSucc ≫ σ j.succ) : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k :
      Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom (σ j ≫ δ i) : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k : Fin (⦋n + 1⦌.len + 1))
have a : j.succ.predAbove (i.castSucc.succAbove k) = i.succAbove (j.predAbove k)
Tactic: dsimp [σ, δ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
⊢ j.succ.predAbove (i.castSucc.succAbove k) = i.succAbove (j.predAbove k)
have a : ∀ (hik : i ≤ k), j.succ.predAbove (i.castSucc.succAbove k) = i.succAbove (j.predAbove k)
Tactic: rcases le_or_gt i k with (hik | hik)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
a : ∀ (hik : i ≤ k), j.succ.predAbove (i.castSucc.succAbove k) = i.succAbove (j.predAbove k)
⊢ j.succ.predAbove (i.castSucc.succAbove k) = i.succAbove (j.predAbove k)
have a₁ : ∀ (hik : k < i), j.succ.predAbove (i.castSucc.succAbove k) = i.succAbove (j.predAbove k)
Tactic: rcases le_or_gt i k with (hik | hik)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
⊢ j.succ.predAbove (i.castSucc.succAbove k) = i.succAbove (j.predAbove k)
have a : i ≤ (j.predAbove k).castSucc
Tactic: rw [Fin.succAbove_of_le_castSucc _ _ (Fin.castSucc_le_castSucc_iff.mpr hik),
    Fin.succ_predAbove_succ, Fin.succAbove_of_le_castSucc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
⊢ i ≤ (j.predAbove k).castSucc
have a : ∀ (hjk : k ≤ j.castSucc), i ≤ (j.predAbove k).castSucc
Tactic: rcases le_or_gt k (j.castSucc) with (hjk | hjk)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
a : ∀ (hjk : k ≤ j.castSucc), i ≤ (j.predAbove k).castSucc
⊢ i ≤ (j.predAbove k).castSucc
have a₁ : ∀ (hjk : j.castSucc < k), i ≤ (j.predAbove k).castSucc
Tactic: rcases le_or_gt k (j.castSucc) with (hjk | hjk)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
hjk : k ≤ j.castSucc
⊢ i ≤ (j.predAbove k).castSucc
have a : i ≤ (k.castPred sorry).castSucc
Tactic: rwa [Fin.predAbove_of_le_castSucc _ _ hjk, Fin.castSucc_castPred]