awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
j : Fin (n + 2)
k : Fin (⦋n⦌.len + 1)
i : ℕ
isLt : i < n + 2
H : (⟨i, isLt⟩ : Fin (n + 2)) ≤ j
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) :
        ℕ)
⊢ (↑(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) :
      ℕ)

Tactic:
rcases j with ⟨j, _⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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⟩
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) :
        ℕ)
⊢ (↑(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 k with ⟨k, _⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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.castSucc : ℕ)

Tactic:
simp at *
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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
neg : ∀ (H : i ≤ j), k < i → k < j + 1 → k < j → i ≤ k → False
⊢ (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc : ℕ) = (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.succ : ℕ)

Tactic:
simp at *
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n i : ℕ
isLt : i < n + 2
j : ℕ
isLt_1 : j < n + 2
k : ℕ
isLt_2 : k < ⦋n⦌.len + 1
H : i ≤ j
h : k < i
h_1 : k < j + 1
h_2 : k < j
h_3 : i ≤ k
⊢ False

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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
pos : ∀ (H : i ≤ j), k < i → k < j + 1 → j ≤ k → k + 1 < i → False
⊢ (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc : ℕ) = (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.castSucc : ℕ)

Tactic:
simp at *
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n i : ℕ
isLt : i < n + 2
j : ℕ
isLt_1 : j < n + 2
k : ℕ
isLt_2 : k < ⦋n⦌.len + 1
H : i ≤ j
h : k < i
h_1 : k < j + 1
h_2 : j ≤ k
h_3 : k + 1 < i
⊢ False

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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
neg : ∀ (H : i ≤ j), k < i → k < j + 1 → j ≤ k → i ≤ k + 1 → k = k + 1 + 1
⊢ (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc : ℕ) = (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.succ : ℕ)

Tactic:
simp at *
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n i : ℕ
isLt : i < n + 2
j : ℕ
isLt_1 : j < n + 2
k : ℕ
isLt_2 : k < ⦋n⦌.len + 1
H : i ≤ j
h : k < i
h_1 : k < j + 1
h_2 : j ≤ k
h_3 : i ≤ k + 1
⊢ k = k + 1 + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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
pos : ∀ (H : i ≤ j), k < i → j + 1 ≤ k → k < j → k < i → False
⊢ (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.succ : ℕ) = (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc : ℕ)

Tactic:
simp at *
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n i : ℕ
isLt : i < n + 2
j : ℕ
isLt_1 : j < n + 2
k : ℕ
isLt_2 : k < ⦋n⦌.len + 1
H : i ≤ j
h : k < i
h_1 : j + 1 ≤ k
h_2 : k < j
h_3 : k < i
⊢ False

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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.succ : ℕ)

Tactic:
simp at *
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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.castSucc : ℕ)

Tactic:
simp at *
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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
neg : ∀ (H : i ≤ j), k < i → j + 1 ≤ k → j ≤ k → i ≤ k + 1 → False
⊢ (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.succ : ℕ) = (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.succ : ℕ)

Tactic:
simp at *
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n i : ℕ
isLt : i < n + 2
j : ℕ
isLt_1 : j < n + 2
k : ℕ
isLt_2 : k < ⦋n⦌.len + 1
H : i ≤ j
h : k < i
h_1 : j + 1 ≤ k
h_2 : j ≤ k
h_3 : i ≤ k + 1
⊢ False

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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
pos : ∀ (H : i ≤ j), i ≤ k → k < j → k < j → k < i → False
⊢ (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.castSucc : ℕ) = (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc : ℕ)

Tactic:
simp at *
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n i : ℕ
isLt : i < n + 2
j : ℕ
isLt_1 : j < n + 2
k : ℕ
isLt_2 : k < ⦋n⦌.len + 1
H : i ≤ j
h : i ≤ k
h_1 h_2 : k < j
h_3 : k < i
⊢ False

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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.succ : ℕ)

Tactic:
simp at *
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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.castSucc : ℕ)

Tactic:
simp at *
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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
neg : ∀ (H : i ≤ j), i ≤ k → k < j → j ≤ k → i ≤ k + 1 → False
⊢ (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.castSucc : ℕ) = (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.succ : ℕ)

Tactic:
simp at *
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n i : ℕ
isLt : i < n + 2
j : ℕ
isLt_1 : j < n + 2
k : ℕ
isLt_2 : k < ⦋n⦌.len + 1
H : i ≤ j
h : i ≤ k
h_1 : k < j
h_2 : j ≤ k
h_3 : i ≤ k + 1
⊢ False

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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
pos : ∀ (H : i ≤ j), i ≤ k → j ≤ k → k < j → k < i → k + 1 + 1 = k
⊢ (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.succ : ℕ) = (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.castSucc : ℕ)

Tactic:
simp at *
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n i : ℕ
isLt : i < n + 2
j : ℕ
isLt_1 : j < n + 2
k : ℕ
isLt_2 : k < ⦋n⦌.len + 1
H : i ≤ j
h : i ≤ k
h_1 : j ≤ k
h_2 : k < j
h_3 : k < i
⊢ k + 1 + 1 = k

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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
neg : ∀ (H : i ≤ j), i ≤ k → j ≤ k → k < j → i ≤ k → False
⊢ (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.succ : ℕ) = (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).castSucc.succ : ℕ)

Tactic:
simp at *
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n i : ℕ
isLt : i < n + 2
j : ℕ
isLt_1 : j < n + 2
k : ℕ
isLt_2 : k < ⦋n⦌.len + 1
H : i ≤ j
h : i ≤ k
h_1 : j ≤ k
h_2 : k < j
h_3 : i ≤ k
⊢ False

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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
pos : ∀ (H : i ≤ j), i ≤ k → j ≤ k → j ≤ k → k + 1 < i → False
⊢ (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.succ : ℕ) = (↑(⟨k, isLt_2⟩ : Fin (⦋n⦌.len + 1)).succ.castSucc : ℕ)

Tactic:
simp at *
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n i : ℕ
isLt : i < n + 2
j : ℕ
isLt_1 : j < n + 2
k : ℕ
isLt_2 : k < ⦋n⦌.len + 1
H : i ≤ j
h : i ≤ k
h_1 h_2 : j ≤ k
h_3 : k + 1 < i
⊢ False

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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.succ : ℕ)

Tactic:
simp at *
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
rw : δ i ≫ δ j = δ i ≫ δ (j.pred ⋯).succ
rw₁ : i ≤ j.pred ⋯
⊢ δ i ≫ δ j = δ (j.pred ⋯) ≫ δ i.castSucc

Tactic:
rw [← δ_comp_δ]

Premises used: SimplexCategory.δ_comp_δ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
rw rw₁ : δ i ≫ δ j = δ i ≫ δ j
⊢ δ i ≫ δ j = δ i ≫ δ (j.pred ⋯).succ

Tactic:
rw [Fin.succ_pred]

Premises used: Fin.succ_pred
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
⊢ i ≤ j.pred ⋯

Tactic:
simpa only [Fin.le_iff_val_le_val, ← Nat.lt_succ_iff, Nat.succ_eq_add_one, ← Fin.val_succ,
      j.succ_pred, Fin.lt_def] using H

Premises used: Nat.succ_eq_add_one, Fin.val_succ, Fin.lt_def, Nat.lt_succ_iff, Fin.succ_pred, Fin.le_iff_val_le_val
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
rw : δ j ≫ δ (i.castLT ⋯).castSucc = δ j ≫ δ i
rw₁ : i.castLT ⋯ ≤ j
⊢ δ (i.castLT ⋯) ≫ δ j.succ = δ j ≫ δ i

Tactic:
rw [δ_comp_δ]

Premises used: SimplexCategory.δ_comp_δ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
⊢ δ j ≫ δ (i.castLT ⋯).castSucc = δ j ≫ δ i

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
⊢ i.castLT ⋯ ≤ j

Tactic:
H
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
⊢ i.castLT ⋯ ≤ j

Tactic:
exact H
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 2)
⊢ δ i ≫ δ i.castSucc = δ i ≫ δ i.succ

Tactic:
(δ_comp_δ (le_refl i)).symm

Premises used: le_refl, SimplexCategory.δ_comp_δ, Eq.symm
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : j = i.castSucc
subst : δ i ≫ δ i.castSucc = δ i ≫ δ i.succ
⊢ δ i ≫ δ j = δ i ≫ δ i.succ

Tactic:
subst H
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 2)
rw rw₁ : δ i ≫ δ i.succ = δ i ≫ δ i.succ
⊢ δ i ≫ δ i.castSucc = δ i ≫ δ i.succ

Tactic:
rw [δ_comp_δ_self]

Premises used: SimplexCategory.δ_comp_δ_self
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
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))
⊢ δ i.castSucc ≫ σ j.succ = σ j ≫ δ i

Tactic:
ext k : 3
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
a : j.succ.predAbove (i.castSucc.succAbove k) = i.succAbove (j.predAbove k)
⊢ 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:
dsimp [σ, δ]

Premises used: SimplexCategory.δ, SimplexCategory.σ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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)
a₁ : ∀ (hik : k < i), j.succ.predAbove (i.castSucc.succAbove k) = i.succAbove (j.predAbove k)
⊢ j.succ.predAbove (i.castSucc.succAbove k) = i.succAbove (j.predAbove k)

Tactic:
rcases le_or_gt i k with (hik | hik)

Premises used: le_or_gt
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
a : i ≤ (j.predAbove k).castSucc
⊢ j.succ.predAbove (i.castSucc.succAbove k) = i.succAbove (j.predAbove k)

Tactic:
rw [Fin.succAbove_of_le_castSucc _ _ (Fin.castSucc_le_castSucc_iff.mpr hik),
    Fin.succ_predAbove_succ, Fin.succAbove_of_le_castSucc]

Premises used: Iff.mpr, Fin.succAbove_of_le_castSucc, Fin.succ_predAbove_succ, Fin.castSucc_le_castSucc_iff
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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
a₁ : ∀ (hjk : j.castSucc < k), i ≤ (j.predAbove k).castSucc
⊢ i ≤ (j.predAbove k).castSucc

Tactic:
rcases le_or_gt k (j.castSucc) with (hjk | hjk)

Premises used: le_or_gt, Fin.castSucc
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
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
a : i ≤ (k.castPred ⋯).castSucc
a₁ a₂ a₃ a₄ : i ≤ k
⊢ i ≤ (j.predAbove k).castSucc

Tactic:
rwa [Fin.predAbove_of_le_castSucc _ _ hjk, Fin.castSucc_castPred]

Premises used: Fin.castSucc_castPred, Fin.predAbove_of_le_castSucc
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
hjk : j.castSucc < k
a : i < k
⊢ i ≤ (j.predAbove k).castSucc

Tactic:
rw [Fin.le_castSucc_iff, Fin.predAbove_of_castSucc_lt _ _ hjk, Fin.succ_pred]

Premises used: Fin.predAbove_of_castSucc_lt, Fin.le_castSucc_iff, Fin.succ_pred
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
hjk : j.castSucc < k
⊢ i < k

Tactic:
H.trans_lt hjk

Premises used: LE.le.trans_lt
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
hjk : j.castSucc < k
⊢ i < k

Tactic:
exact H.trans_lt hjk

Premises used: LE.le.trans_lt
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : k < i
a : j.succ.predAbove k.castSucc = i.succAbove (j.predAbove k)
⊢ j.succ.predAbove (i.castSucc.succAbove k) = i.succAbove (j.predAbove k)

Tactic:
rw [Fin.succAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_castSucc_iff.mpr hik)]

Premises used: Iff.mpr, Fin.castSucc_lt_castSucc_iff, Fin.succAbove_of_castSucc_lt
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : k < i
⊢ k < j.castSucc

Tactic:
have hjk := H.trans_lt' hik
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : k < i
hjk : k < j.castSucc
a : (k.castPred ⋯).castSucc < i
⊢ j.succ.predAbove k.castSucc = i.succAbove (j.predAbove k)

Tactic:
rw [Fin.predAbove_of_le_castSucc _ _ (Fin.castSucc_le_castSucc_iff.mpr
      (hjk.trans Fin.castSucc_lt_succ).le),
      Fin.predAbove_of_le_castSucc _ _ hjk.le, Fin.castPred_castSucc, Fin.succAbove_of_castSucc_lt,
      Fin.castSucc_castPred]

Premises used: Iff.mpr, Fin.ext_iff, Fin.castPred_castSucc, Fin.castSucc_lt_succ, Iff.not, LT.lt.le, Fin.castSucc_lt_last, Fin.castSucc_castPred, Fin.predAbove_of_le_castSucc, Fin.castSucc_le_castSucc_iff, LT.lt.trans, Fin.succAbove_of_castSucc_lt, LT.lt.ne