awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 a₁ a₂ a₃ : k < i
⊢ (k.castPred ⋯).castSucc < i

Tactic:
rwa [Fin.castSucc_castPred]

Premises used: Fin.castSucc_castPred
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 1)
rcases : ∀ (i : ℕ) (hi : i < n + 1), δ (⟨i, hi⟩ : Fin (n + 1)).castSucc ≫ σ (⟨i, hi⟩ : Fin (n + 1)) = 𝟙 ⦋n⦌
⊢ δ i.castSucc ≫ σ i = 𝟙 ⦋n⦌

Tactic:
rcases i with ⟨i, hi⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n i : ℕ
hi : i < n + 1
a :
  ∀ (j : ℕ) (hj : j < ⦋n⦌.len + 1),
    (↑((Hom.toOrderHom (δ (⟨i, hi⟩ : Fin (n + 1)).castSucc ≫ σ (⟨i, hi⟩ : Fin (n + 1))) :
              (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1))
            (⟨j, hj⟩ : Fin (⦋n⦌.len + 1))) :
        ℕ) =
      (↑((Hom.toOrderHom (𝟙 ⦋n⦌) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1)) ⟨j, hj⟩) : ℕ)
⊢ δ (⟨i, hi⟩ : Fin (n + 1)).castSucc ≫ σ (⟨i, hi⟩ : Fin (n + 1)) = 𝟙 ⦋n⦌

Tactic:
ext ⟨j, hj⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
a :
  (↑(if h :
            (⟨i, ⋯⟩ : Fin (n + 1 + 1)) <
              if (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < (⟨i, ⋯⟩ : Fin (n + 1 + 1)) then (⟨j, ⋯⟩ : Fin (n + 1 + 1))
              else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1)) then
          (if (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < (⟨i, ⋯⟩ : Fin (n + 1 + 1)) then (⟨j, ⋯⟩ : Fin (n + 1 + 1))
              else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1))).pred
            ⋯
        else
          (if (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < (⟨i, ⋯⟩ : Fin (n + 1 + 1)) then (⟨j, ⋯⟩ : Fin (n + 1 + 1))
              else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1))).castPred
            ⋯) :
      ℕ) =
    j
⊢ (↑((Hom.toOrderHom (δ (⟨i, hi⟩ : Fin (n + 1)).castSucc ≫ σ (⟨i, hi⟩ : Fin (n + 1))) :
            (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          (⟨j, hj⟩ : Fin (⦋n⦌.len + 1))) :
      ℕ) =
    (↑((Hom.toOrderHom (𝟙 ⦋n⦌) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1)) ⟨j, hj⟩) : ℕ)

Tactic:
dsimp [σ, δ, Fin.predAbove, Fin.succAbove]

Premises used: Fin.succAbove, SimplexCategory.δ, SimplexCategory.σ, Fin.predAbove
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
a :
  (if h : i < if j < i then j else j + 1 then (if j < i then j else j + 1) - 1
    else (↑((if j < i then (⟨j, ⋯⟩ : Fin (n + 1 + 1)) else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1))).castPred ⋯) : ℕ)) =
    j
⊢ (↑(if h :
            (⟨i, ⋯⟩ : Fin (n + 1 + 1)) <
              if (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < (⟨i, ⋯⟩ : Fin (n + 1 + 1)) then (⟨j, ⋯⟩ : Fin (n + 1 + 1))
              else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1)) then
          (if (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < (⟨i, ⋯⟩ : Fin (n + 1 + 1)) then (⟨j, ⋯⟩ : Fin (n + 1 + 1))
              else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1))).pred
            ⋯
        else
          (if (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < (⟨i, ⋯⟩ : Fin (n + 1 + 1)) then (⟨j, ⋯⟩ : Fin (n + 1 + 1))
              else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1))).castPred
            ⋯) :
      ℕ) =
    j

Tactic:
simp only [Fin.lt_def, Fin.dite_val, Fin.ite_val, Fin.val_pred]

Premises used: Fin.dite_val, Fin.val_pred, Fin.lt_def, Fin.ite_val
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
pos : j < i → i < j → j - 1 = j
neg : ∀ (h : j < i) (h_1 : ¬i < j), (↑((⟨j, ⋯⟩ : Fin (n + 1 + 1)).castPred ⋯) : ℕ) = j
pos₁ : ¬j < i → i < j + 1 → j + 1 - 1 = j
neg₁ : ∀ (h : ¬j < i) (h_1 : ¬i < j + 1), (↑((⟨j + 1, ⋯⟩ : Fin (n + 1 + 1)).castPred ⋯) : ℕ) = j
⊢ (if h : i < if j < i then j else j + 1 then (if j < i then j else j + 1) - 1
    else (↑((if j < i then (⟨j, ⋯⟩ : Fin (n + 1 + 1)) else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1))).castPred ⋯) : ℕ)) =
    j

Tactic:
split_ifs
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
h : j < i
h_1 : ¬i < j
⊢ (↑((⟨j, ⋯⟩ : Fin (n + 1 + 1)).castPred ⋯) : ℕ) = j

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
h : ¬j < i
h_1 : i < j + 1
⊢ j + 1 - 1 = j

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
h : ¬j < i
h_1 : ¬i < j + 1
neg : False
⊢ (↑((⟨j + 1, ⋯⟩ : Fin (n + 1 + 1)).castPred ⋯) : ℕ) = j

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
h : j < i
h_1 : i < j
⊢ j - 1 = j

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
h : ¬j < i
h_1 : ¬i < j + 1
⊢ False

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = i.castSucc
subst : δ i.castSucc ≫ σ i = 𝟙 ⦋n⦌
⊢ δ j ≫ σ i = 𝟙 ⦋n⦌

Tactic:
subst H
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 1)
rw rw₁ : 𝟙 ⦋n⦌ = 𝟙 ⦋n⦌
⊢ δ i.castSucc ≫ σ i = 𝟙 ⦋n⦌

Tactic:
rw [δ_comp_σ_self]

Premises used: SimplexCategory.δ_comp_σ_self
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 1)
a :
  ∀ (j : Fin (⦋n⦌.len + 1)),
    (↑((Hom.toOrderHom (δ i.succ ≫ σ i) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1)) j) : ℕ) =
      (↑((Hom.toOrderHom (𝟙 ⦋n⦌) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1)) j) : ℕ)
⊢ δ i.succ ≫ σ i = 𝟙 ⦋n⦌

Tactic:
ext j
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin (⦋n⦌.len + 1)
a :
  ∀ (i : ℕ) (isLt : i < n + 1),
    (↑((Hom.toOrderHom (δ (⟨i, isLt⟩ : Fin (n + 1)).succ ≫ σ (⟨i, isLt⟩ : Fin (n + 1))) :
              (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1))
            j) :
        ℕ) =
      (↑((Hom.toOrderHom (𝟙 ⦋n⦌) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1)) j) : ℕ)
⊢ (↑((Hom.toOrderHom (δ i.succ ≫ σ i) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1)) j) : ℕ) =
    (↑((Hom.toOrderHom (𝟙 ⦋n⦌) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1)) j) : ℕ)

Tactic:
rcases i with ⟨i, _⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
j : Fin (⦋n⦌.len + 1)
i : ℕ
isLt : i < n + 1
a :
  ∀ (j : ℕ) (isLt_1 : j < ⦋n⦌.len + 1),
    (↑((Hom.toOrderHom (δ (⟨i, isLt⟩ : Fin (n + 1)).succ ≫ σ (⟨i, isLt⟩ : Fin (n + 1))) :
              (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1))
            (⟨j, isLt_1⟩ : Fin (⦋n⦌.len + 1))) :
        ℕ) =
      (↑((Hom.toOrderHom (𝟙 ⦋n⦌) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1)) ⟨j, isLt_1⟩) : ℕ)
⊢ (↑((Hom.toOrderHom (δ (⟨i, isLt⟩ : Fin (n + 1)).succ ≫ σ (⟨i, isLt⟩ : Fin (n + 1))) :
            (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          j) :
      ℕ) =
    (↑((Hom.toOrderHom (𝟙 ⦋n⦌) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1)) j) : ℕ)

Tactic:
rcases j with ⟨j, _⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n i : ℕ
isLt : i < n + 1
j : ℕ
isLt_1 : j < ⦋n⦌.len + 1
a :
  (↑(if h :
            (⟨i, ⋯⟩ : Fin (n + 1 + 1)) <
              if (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) then (⟨j, ⋯⟩ : Fin (n + 1 + 1))
              else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1)) then
          (if (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) then (⟨j, ⋯⟩ : Fin (n + 1 + 1))
              else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1))).pred
            ⋯
        else
          (if (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) then (⟨j, ⋯⟩ : Fin (n + 1 + 1))
              else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1))).castPred
            ⋯) :
      ℕ) =
    j
⊢ (↑((Hom.toOrderHom (δ (⟨i, isLt⟩ : Fin (n + 1)).succ ≫ σ (⟨i, isLt⟩ : Fin (n + 1))) :
            (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          (⟨j, isLt_1⟩ : Fin (⦋n⦌.len + 1))) :
      ℕ) =
    (↑((Hom.toOrderHom (𝟙 ⦋n⦌) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1)) ⟨j, isLt_1⟩) : ℕ)

Tactic:
dsimp [δ, σ, Fin.succAbove, Fin.predAbove]

Premises used: Fin.succAbove, SimplexCategory.δ, SimplexCategory.σ, Fin.predAbove
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n i : ℕ
isLt : i < n + 1
j : ℕ
isLt_1 : j < ⦋n⦌.len + 1
pos :
  ∀ (h : (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < ⟨i + 1, ⋯⟩) (h_1 : (⟨i, ⋯⟩ : Fin (n + 1 + 1)) < ⟨j, ⋯⟩),
    (↑((⟨j, ⋯⟩ : Fin (n + 1 + 1)).pred ⋯) : ℕ) = j
neg :
  ∀ (h : (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < ⟨i + 1, ⋯⟩) (h_1 : ¬(⟨i, ⋯⟩ : Fin (n + 1 + 1)) < ⟨j, ⋯⟩),
    (↑((⟨j, ⋯⟩ : Fin (n + 1 + 1)).castPred ⋯) : ℕ) = j
pos₁ :
  ∀ (h : ¬(⟨j, ⋯⟩ : Fin (n + 1 + 1)) < ⟨i + 1, ⋯⟩) (h_1 : (⟨i, ⋯⟩ : Fin (n + 1 + 1)) < ⟨j + 1, ⋯⟩),
    (↑((⟨j + 1, ⋯⟩ : Fin (n + 1 + 1)).pred ⋯) : ℕ) = j
neg₁ :
  ∀ (h : ¬(⟨j, ⋯⟩ : Fin (n + 1 + 1)) < ⟨i + 1, ⋯⟩) (h_1 : ¬(⟨i, ⋯⟩ : Fin (n + 1 + 1)) < ⟨j + 1, ⋯⟩),
    (↑((⟨j + 1, ⋯⟩ : Fin (n + 1 + 1)).castPred ⋯) : ℕ) = j
⊢ (↑(if h :
            (⟨i, ⋯⟩ : Fin (n + 1 + 1)) <
              if (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) then (⟨j, ⋯⟩ : Fin (n + 1 + 1))
              else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1)) then
          (if (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) then (⟨j, ⋯⟩ : Fin (n + 1 + 1))
              else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1))).pred
            ⋯
        else
          (if (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) then (⟨j, ⋯⟩ : Fin (n + 1 + 1))
              else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1))).castPred
            ⋯) :
      ℕ) =
    j

Tactic:
split_ifs
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n i : ℕ
isLt : i < n + 1
j : ℕ
isLt_1 : j < ⦋n⦌.len + 1
h : (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < ⟨i + 1, ⋯⟩
h_1 : (⟨i, ⋯⟩ : Fin (n + 1 + 1)) < ⟨j, ⋯⟩
pos : j - 1 = j
⊢ (↑((⟨j, ⋯⟩ : Fin (n + 1 + 1)).pred ⋯) : ℕ) = j

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n i : ℕ
isLt : i < n + 1
j : ℕ
isLt_1 : j < ⦋n⦌.len + 1
h : (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < ⟨i + 1, ⋯⟩
h_1 : ¬(⟨i, ⋯⟩ : Fin (n + 1 + 1)) < ⟨j, ⋯⟩
⊢ (↑((⟨j, ⋯⟩ : Fin (n + 1 + 1)).castPred ⋯) : ℕ) = j

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n i : ℕ
isLt : i < n + 1
j : ℕ
isLt_1 : j < ⦋n⦌.len + 1
h : ¬(⟨j, ⋯⟩ : Fin (n + 1 + 1)) < ⟨i + 1, ⋯⟩
h_1 : (⟨i, ⋯⟩ : Fin (n + 1 + 1)) < ⟨j + 1, ⋯⟩
⊢ (↑((⟨j + 1, ⋯⟩ : Fin (n + 1 + 1)).pred ⋯) : ℕ) = j

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n i : ℕ
isLt : i < n + 1
j : ℕ
isLt_1 : j < ⦋n⦌.len + 1
h : ¬(⟨j, ⋯⟩ : Fin (n + 1 + 1)) < ⟨i + 1, ⋯⟩
h_1 : ¬(⟨i, ⋯⟩ : Fin (n + 1 + 1)) < ⟨j + 1, ⋯⟩
neg : False
⊢ (↑((⟨j + 1, ⋯⟩ : Fin (n + 1 + 1)).castPred ⋯) : ℕ) = j

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n i : ℕ
isLt : i < n + 1
j : ℕ
isLt_1 : j < ⦋n⦌.len + 1
h : (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < ⟨i + 1, ⋯⟩
h_1 : (⟨i, ⋯⟩ : Fin (n + 1 + 1)) < ⟨j, ⋯⟩
⊢ j < i + 1

Tactic:
simp at *
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n i : ℕ
isLt : i < n + 1
j : ℕ
isLt_1 : j < ⦋n⦌.len + 1
h_1 : (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < ⟨i + 1, ⋯⟩
h_2 : (⟨i, ⋯⟩ : Fin (n + 1 + 1)) < ⟨j, ⋯⟩
h : j < i + 1
⊢ i < j

Tactic:
simp at *
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n i : ℕ
isLt : i < n + 1
j : ℕ
isLt_1 : j < ⦋n⦌.len + 1
h : ¬(⟨j, ⋯⟩ : Fin (n + 1 + 1)) < ⟨i + 1, ⋯⟩
h_1 : ¬(⟨i, ⋯⟩ : Fin (n + 1 + 1)) < ⟨j + 1, ⋯⟩
⊢ i + 1 ≤ j

Tactic:
simp at *
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n i : ℕ
isLt : i < n + 1
j : ℕ
isLt_1 : j < ⦋n⦌.len + 1
h_1 : ¬(⟨j, ⋯⟩ : Fin (n + 1 + 1)) < ⟨i + 1, ⋯⟩
h_2 : ¬(⟨i, ⋯⟩ : Fin (n + 1 + 1)) < ⟨j + 1, ⋯⟩
h : i + 1 ≤ j
⊢ j + 1 ≤ i

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

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n i : ℕ
isLt : i < n + 1
j : ℕ
isLt_1 : j < ⦋n⦌.len + 1
h : i + 1 ≤ j
h_1 : j + 1 ≤ i
⊢ False

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = i.succ
subst : δ i.succ ≫ σ i = 𝟙 ⦋n⦌
⊢ δ j ≫ σ i = 𝟙 ⦋n⦌

Tactic:
subst H
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 1)
rw rw₁ : 𝟙 ⦋n⦌ = 𝟙 ⦋n⦌
⊢ δ i.succ ≫ σ i = 𝟙 ⦋n⦌

Tactic:
rw [δ_comp_σ_succ]

Premises used: SimplexCategory.δ_comp_σ_succ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
a :
  ∀ (k : Fin (⦋n + 1⦌.len + 1)),
    Eq (α := Fin (⦋n + 1⦌.len + 1))
      ((Hom.toOrderHom (δ i.succ ≫ σ j.castSucc) : (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.succ ≫ σ j.castSucc = σ j ≫ δ i

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

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

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

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

Premises used: Iff.mpr, Fin.succAbove_of_castSucc_lt, Fin.castSucc_lt_succ_iff
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
a : ∀ (hjk : k ≤ j.castSucc), j.castSucc.predAbove k.castSucc = i.succAbove (j.predAbove k)
a₁ : ∀ (hjk : j.castSucc < k), j.castSucc.predAbove k.castSucc = i.succAbove (j.predAbove k)
⊢ j.castSucc.predAbove k.castSucc = i.succAbove (j.predAbove k)

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 : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
hjk : k ≤ j.castSucc
a : (k.castPred ⋯).castSucc < i
⊢ j.castSucc.predAbove k.castSucc = i.succAbove (j.predAbove k)

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

Premises used: Iff.mpr, Fin.ext_iff, Fin.castPred_castSucc, Iff.not, Fin.castSucc_lt_last, Fin.castSucc_castPred, Fin.predAbove_of_le_castSucc, Fin.castSucc_le_castSucc_iff, Fin.succAbove_of_castSucc_lt, LT.lt.ne
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
hjk : k ≤ j.castSucc
a : k < i
⊢ (k.castPred ⋯).castSucc < i

Tactic:
rw [Fin.castSucc_castPred]

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

Tactic:
hjk.trans_lt H

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

Tactic:
exact hjk.trans_lt H

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

Tactic:
rw [Fin.predAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_castSucc_iff.mpr hjk),
      Fin.predAbove_of_castSucc_lt _ _ hjk, Fin.succAbove_of_castSucc_lt,
      Fin.castSucc_pred_eq_pred_castSucc]

Premises used: Iff.mpr, Fin.predAbove_of_castSucc_lt, Fin.castSucc_lt_castSucc_iff, Fin.castSucc_pred_eq_pred_castSucc, Fin.succAbove_of_castSucc_lt
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
hjk : j.castSucc < k
a : (k.pred ⋯).succ ≤ i
a₁ a₂ a₃ a₄ : k ≤ i
⊢ (k.pred ⋯).castSucc < i

Tactic:
rwa [Fin.castSucc_lt_iff_succ_le, Fin.succ_pred]

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

Tactic:
rw [Fin.succAbove_of_le_castSucc _ _ (Fin.succ_le_castSucc_iff.mpr hik)]

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

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

Tactic:
rw [Fin.predAbove_of_castSucc_lt _ _ hjk, Fin.predAbove_of_castSucc_lt _ _
      (Fin.castSucc_lt_succ_iff.mpr hjk.le),
    Fin.pred_succ, Fin.succAbove_of_le_castSucc, Fin.succ_pred]

Premises used: Iff.mpr, Fin.succAbove_of_le_castSucc, Fin.predAbove_of_castSucc_lt, LT.lt.le, Fin.pred_succ, Fin.succ_pred, Fin.castSucc_lt_succ_iff
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : i < k
hjk : j.castSucc < k
a a₁ a₂ a₃ : i < k
⊢ i ≤ (k.pred ⋯).castSucc

Tactic:
rwa [Fin.le_castSucc_pred_iff]

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

Tactic:
rw [← δ_comp_σ_of_gt]

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

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

Tactic:
rw [Fin.castSucc_castLT, ← Fin.succ_lt_succ_iff, Fin.succ_pred]

Premises used: Fin.succ_lt_succ_iff, Fin.castSucc_castLT, Fin.succ_pred
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ j.succ < i

Tactic:
H
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ j.succ < i

Tactic:
exact H
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
a :
  ∀ (k : Fin (⦋n + 1 + 1⦌.len + 1)),
    Eq (α := Fin (⦋n⦌.len + 1))
      ((Hom.toOrderHom (σ i.castSucc ≫ σ j) : (a : Fin (⦋n + 1 + 1⦌.len + 1)) → Fin (⦋n⦌.len + 1)) k :
        Fin (⦋n⦌.len + 1))
      ((Hom.toOrderHom (σ j.succ ≫ σ i) : (a : Fin (⦋n + 1 + 1⦌.len + 1)) → Fin (⦋n⦌.len + 1)) k : Fin (⦋n⦌.len + 1))
⊢ σ i.castSucc ≫ σ j = σ j.succ ≫ σ i

Tactic:
ext k : 3
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (⦋n + 1 + 1⦌.len + 1)
a : j.predAbove (i.castSucc.predAbove k) = i.predAbove (j.succ.predAbove k)
⊢ Eq (α := Fin (⦋n⦌.len + 1))
    ((Hom.toOrderHom (σ i.castSucc ≫ σ j) : (a : Fin (⦋n + 1 + 1⦌.len + 1)) → Fin (⦋n⦌.len + 1)) k : Fin (⦋n⦌.len + 1))
    ((Hom.toOrderHom (σ j.succ ≫ σ i) : (a : Fin (⦋n + 1 + 1⦌.len + 1)) → Fin (⦋n⦌.len + 1)) k : Fin (⦋n⦌.len + 1))

Tactic:
dsimp [σ]

Premises used: SimplexCategory.σ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ j.predAbove (i.castSucc.predAbove (Fin.last ⦋n + 1 + 1⦌.len)) =
    i.predAbove (j.succ.predAbove (Fin.last ⦋n + 1 + 1⦌.len))

Tactic:
simp only [len_mk, Fin.predAbove_right_last]

Premises used: SimplexCategory.len_mk, Fin.predAbove_right_last
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ j.predAbove (i.castSucc.predAbove (Fin.castSucc 0)) = i.predAbove (j.succ.predAbove (Fin.castSucc 0))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
a : ∀ (h : i ≤ k), j.predAbove (i.castSucc.predAbove k.succ.castSucc) = i.predAbove (j.succ.predAbove k.succ.castSucc)
a₁ : ∀ (h : k < i), j.predAbove (i.castSucc.predAbove k.succ.castSucc) = i.predAbove (j.succ.predAbove k.succ.castSucc)
⊢ j.predAbove (i.castSucc.predAbove k.succ.castSucc) = i.predAbove (j.succ.predAbove k.succ.castSucc)

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

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

Tactic:
simp_rw [Fin.predAbove_of_castSucc_lt i.castSucc _ (Fin.castSucc_lt_castSucc_iff.mpr
        (Fin.castSucc_lt_succ_iff.mpr h)), ← Fin.succ_castSucc, Fin.pred_succ,
        Fin.succ_predAbove_succ]

Premises used: Iff.mpr, Fin.predAbove_of_castSucc_lt, Fin.succ_predAbove_succ, Fin.castSucc_lt_castSucc_iff, Fin.pred_succ, Fin.succ_castSucc, Fin.castSucc, Fin.castSucc_lt_succ_iff
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
rw : i ≤ j.predAbove k.castSucc
⊢ j.predAbove k.castSucc = i.predAbove (j.predAbove k.castSucc).succ

Tactic:
rw [Fin.predAbove_of_castSucc_lt i _ (Fin.castSucc_lt_succ_iff.mpr _), Fin.pred_succ]

Premises used: Iff.mpr, Fin.predAbove_of_castSucc_lt, Fin.pred_succ, Fin.castSucc_lt_succ_iff
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
inl : ∀ (hkj : k ≤ j), i ≤ j.predAbove k.castSucc
inr : ∀ (hkj : j < k), i ≤ j.predAbove k.castSucc
⊢ i ≤ j.predAbove k.castSucc

Tactic:
rcases le_or_gt k j with (hkj | hkj)

Premises used: le_or_gt
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
hkj : k ≤ j
inl : i ≤ k.castSucc.castPred ⋯
inl₁ inl₂ inl₃ inl₄ : i ≤ k
⊢ i ≤ j.predAbove k.castSucc

Tactic:
rwa [Fin.predAbove_of_le_castSucc _ _ (Fin.castSucc_le_castSucc_iff.mpr hkj),
          Fin.castPred_castSucc]

Premises used: Iff.mpr, Fin.ext_iff, Fin.castPred_castSucc, Iff.not, Fin.castSucc_lt_last, Fin.predAbove_of_le_castSucc, Fin.castSucc_le_castSucc_iff, LT.lt.ne