awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
hkj : j < k
inr : i < k
⊢ i ≤ j.predAbove k.castSucc

Tactic:
rw [Fin.predAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_castSucc_iff.mpr hkj),
          Fin.le_pred_iff,
          Fin.succ_le_castSucc_iff]

Premises used: Iff.mpr, Fin.predAbove_of_castSucc_lt, Fin.castSucc_lt_castSucc_iff, Fin.succ_le_castSucc_iff, Fin.le_pred_iff
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
hkj : j < k
⊢ i < k

Tactic:
H.trans_lt hkj

Premises used: LE.le.trans_lt
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
hkj : j < k
⊢ i < k

Tactic:
exact H.trans_lt hkj

Premises used: LE.le.trans_lt
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : k < i
a : j.predAbove k.succ = 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_le_castSucc i.castSucc _ (Fin.castSucc_le_castSucc_iff.mpr
        (Fin.succ_le_castSucc_iff.mpr h)), Fin.castPred_castSucc, ← Fin.succ_castSucc,
        Fin.succ_predAbove_succ]

Premises used: Iff.mpr, Fin.ext_iff, Fin.castPred_castSucc, Fin.succ_predAbove_succ, Iff.not, Fin.succ_le_castSucc_iff, Fin.castSucc_lt_last, Fin.predAbove_of_le_castSucc, Fin.castSucc_le_castSucc_iff, Fin.succ_castSucc, Fin.castSucc, LT.lt.ne
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : k < i
a : j.predAbove k.succ = i.predAbove (k.castSucc.castPred ⋯).succ
a₁ : j.predAbove k.succ = i.predAbove k.succ
a₂ : k.succ.castPred ⋯ = i.predAbove k.succ
a₃ a₄ : k.succ.castPred ⋯ = k.succ.castPred ⋯
⊢ j.predAbove k.succ = i.predAbove (j.predAbove k.castSucc).succ

Tactic:
rw [Fin.predAbove_of_le_castSucc _ k.castSucc
        (Fin.castSucc_le_castSucc_iff.mpr (h.le.trans H)),
        Fin.castPred_castSucc, Fin.predAbove_of_le_castSucc _ k.succ
        (Fin.succ_le_castSucc_iff.mpr (H.trans_lt' h)), Fin.predAbove_of_le_castSucc _ k.succ
        (Fin.succ_le_castSucc_iff.mpr h)]

Premises used: Iff.mpr, Fin.ext_iff, Fin.castPred_castSucc, Fin.succ, Iff.not, LT.lt.le, Fin.succ_le_castSucc_iff, Fin.castSucc_lt_last, LE.le.trans_lt', Fin.predAbove_of_le_castSucc, Fin.castSucc_le_castSucc_iff, LE.le.trans, Fin.castSucc, LT.lt.ne
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin ⦋n + 1 + 1⦌.len
a : j.predAbove (i.castSucc.predAbove (Fin.castSucc 0)) = i.predAbove (j.succ.predAbove (Fin.castSucc 0))
a₁ :
  ∀ (k : Fin (n + 1)),
    j.predAbove (i.castSucc.predAbove k.succ.castSucc) = i.predAbove (j.succ.predAbove k.succ.castSucc)
⊢ j.predAbove (i.castSucc.predAbove k.castSucc) = i.predAbove (j.succ.predAbove k.castSucc)

Tactic:
cases k using Fin.cases with
    | zero =>
      simp
    | succ k =>
      rcases le_or_gt i k with (h | h)
      · 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]
        rw [Fin.predAbove_of_castSucc_lt i _ (Fin.castSucc_lt_succ_iff.mpr _), Fin.pred_succ]
        rcases le_or_gt k j with (hkj | hkj)
        · rwa [Fin.predAbove_of_le_castSucc _ _ (Fin.castSucc_le_castSucc_iff.mpr hkj),
          Fin.castPred_castSucc]
        · rw [Fin.predAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_castSucc_iff.mpr hkj),
          Fin.le_pred_iff,
          Fin.succ_le_castSucc_iff]
          exact H.trans_lt hkj
      · simp_rw [Fin.predAbove_of_le_castSucc i.castSucc _ (Fin.castSucc_le_castSucc_iff.mpr
        (Fin.succ_le_castSucc_iff.mpr h)), Fin.castPred_castSucc, ← Fin.succ_castSucc,
        Fin.succ_predAbove_succ]
        rw [Fin.predAbove_of_le_castSucc _ k.castSucc
        (Fin.castSucc_le_castSucc_iff.mpr (h.le.trans H)),
        Fin.castPred_castSucc, Fin.predAbove_of_le_castSucc _ k.succ
        (Fin.succ_le_castSucc_iff.mpr (H.trans_lt' h)), Fin.predAbove_of_le_castSucc _ k.succ
        (Fin.succ_le_castSucc_iff.mpr h)]

Premises used: Iff.mpr, Fin.ext_iff, Fin.castPred_castSucc, Fin.predAbove_of_castSucc_lt, Fin.succ_predAbove_succ, Iff.not, Fin.succ_le_castSucc_iff, Fin.pred_succ, Fin.castSucc_lt_last, Fin.succ_castSucc, Fin.le_pred_iff, Fin.castSucc_lt_succ_iff, LT.lt.ne
-- 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 (Fin.last ⦋n + 1 + 1⦌.len)) =
    i.predAbove (j.succ.predAbove (Fin.last ⦋n + 1 + 1⦌.len))
a₁ :
  ∀ (k : Fin ⦋n + 1 + 1⦌.len), j.predAbove (i.castSucc.predAbove k.castSucc) = i.predAbove (j.succ.predAbove k.castSucc)
⊢ j.predAbove (i.castSucc.predAbove k) = i.predAbove (j.succ.predAbove k)

Tactic:
cases k using Fin.lastCases with
  | last => simp only [len_mk, Fin.predAbove_right_last]
  | cast k =>
    cases k using Fin.cases with
    | zero =>
      simp
    | succ k =>
      rcases le_or_gt i k with (h | h)
      · 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]
        rw [Fin.predAbove_of_castSucc_lt i _ (Fin.castSucc_lt_succ_iff.mpr _), Fin.pred_succ]
        rcases le_or_gt k j with (hkj | hkj)
        · rwa [Fin.predAbove_of_le_castSucc _ _ (Fin.castSucc_le_castSucc_iff.mpr hkj),
          Fin.castPred_castSucc]
        · rw [Fin.predAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_castSucc_iff.mpr hkj),
          Fin.le_pred_iff,
          Fin.succ_le_castSucc_iff]
          exact H.trans_lt hkj
      · simp_rw [Fin.predAbove_of_le_castSucc i.castSucc _ (Fin.castSucc_le_castSucc_iff.mpr
        (Fin.succ_le_castSucc_iff.mpr h)), Fin.castPred_castSucc, ← Fin.succ_castSucc,
        Fin.succ_predAbove_succ]
        rw [Fin.predAbove_of_le_castSucc _ k.castSucc
        (Fin.castSucc_le_castSucc_iff.mpr (h.le.trans H)),
        Fin.castPred_castSucc, Fin.predAbove_of_le_castSucc _ k.succ
        (Fin.succ_le_castSucc_iff.mpr (H.trans_lt' h)), Fin.predAbove_of_le_castSucc _ k.succ
        (Fin.succ_le_castSucc_iff.mpr h)]

Premises used: Iff.mpr, Fin.ext_iff, SimplexCategory.len_mk, Fin.castPred_castSucc, Fin.predAbove_of_castSucc_lt, Fin.succ_predAbove_succ, Fin.predAbove_right_last, cast, Iff.not, Fin.succ_le_castSucc_iff, Fin.pred_succ, Fin.castSucc_lt_last, Fin.succ_castSucc, Fin.le_pred_iff, Fin.castSucc_lt_succ_iff, LT.lt.ne
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
⊢ Eq (α := ⦋0⦌ ⟶ ⦋HAdd.hAdd (α := ℕ) 0 1⦌) (δ 0) (⦋0⦌.const ⦋HAdd.hAdd (α := ℕ) 0 1⦌ 1)

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
⊢ Eq (α := ⦋0⦌ ⟶ ⦋HAdd.hAdd (α := ℕ) 0 1⦌) (δ 1) (⦋0⦌.const ⦋HAdd.hAdd (α := ℕ) 0 1⦌ 0)

Tactic:
decide
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
j : Fin (n + 2)
hj : ∀ (k : Fin (m + 1)), (Hom.toOrderHom f : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k ≠ j
a :
  ∀ (k : Fin (⦋m⦌.len + 1)),
    Eq (α := Fin (⦋n + 1⦌.len + 1))
      ((Hom.toOrderHom (factor_δ f j ≫ δ j) : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k :
        Fin (⦋n + 1⦌.len + 1))
      ((Hom.toOrderHom f : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k : Fin (⦋n + 1⦌.len + 1))
⊢ factor_δ f j ≫ δ j = f

Tactic:
ext k : 3
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
j : Fin (n + 2)
hj : ∀ (k : Fin (m + 1)), (Hom.toOrderHom f : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k ≠ j
k : Fin (⦋m⦌.len + 1)
a :
  ∀
    (hj :
      ∀ (k : Fin (m + 1)),
        Ne (α := Fin (⦋n + 1⦌.len + 1))
          ((Hom.toOrderHom f : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k : Fin (⦋n + 1⦌.len + 1))
          (0 : Fin (n + 1 + 1))),
    Eq (α := Fin (⦋n + 1⦌.len + 1))
      ((Hom.toOrderHom (factor_δ f 0 ≫ δ 0) : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k :
        Fin (⦋n + 1⦌.len + 1))
      ((Hom.toOrderHom f : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k : Fin (⦋n + 1⦌.len + 1))
a₁ :
  ∀ (i : Fin (n + 1))
    (hj : ∀ (k : Fin (m + 1)), (Hom.toOrderHom f : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k ≠ i.succ),
    Eq (α := Fin (⦋n + 1⦌.len + 1))
      ((Hom.toOrderHom (factor_δ f i.succ ≫ δ i.succ) : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k :
        Fin (⦋n + 1⦌.len + 1))
      ((Hom.toOrderHom f : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k : Fin (⦋n + 1⦌.len + 1))
⊢ Eq (α := Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom (factor_δ f j ≫ δ j) : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k : Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom f : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k : Fin (⦋n + 1⦌.len + 1))

Tactic:
cases j using Fin.cases
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
k : Fin (⦋m⦌.len + 1)
hj :
  ∀ (k : Fin (m + 1)),
    Ne (α := Fin (⦋n + 1⦌.len + 1))
      ((Hom.toOrderHom f : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k : Fin (⦋n + 1⦌.len + 1))
      (0 : Fin (n + 1 + 1))
⊢ Eq (α := Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom (factor_δ f 0 ≫ δ 0) : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k : Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom f : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k : Fin (⦋n + 1⦌.len + 1))

Tactic:
simp_all [factor_δ, δ, σ]

Premises used: SimplexCategory.δ, SimplexCategory.σ, SimplexCategory.factor_δ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
k : Fin (⦋m⦌.len + 1)
i : Fin (n + 1)
hj : ∀ (k : Fin (m + 1)), (Hom.toOrderHom f : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k ≠ i.succ
⊢ Eq (α := Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom (factor_δ f i.succ ≫ δ i.succ) : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k :
      Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom f : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k : Fin (⦋n + 1⦌.len + 1))

Tactic:
simp_all [factor_δ, δ, σ]

Premises used: SimplexCategory.δ, SimplexCategory.σ, SimplexCategory.factor_δ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
a :
  ∀ (x : Fin (⦋0⦌.len + 1)),
    (↑((Hom.toOrderHom (δ 0 ≫ mkOfSucc i) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋n⦌.len + 1)) x) : ℕ) =
      (↑((Hom.toOrderHom (⦋0⦌.const ⦋n⦌ i.succ) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋n⦌.len + 1)) x) : ℕ)
⊢ δ 0 ≫ mkOfSucc i = ⦋0⦌.const ⦋n⦌ i.succ

Tactic:
ext x
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
x : Fin (⦋0⦌.len + 1)
a :
  (↑((Hom.toOrderHom (δ 0 ≫ mkOfSucc i) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋0⦌.len + 1)))) :
      ℕ) =
    (↑((Hom.toOrderHom (⦋0⦌.const ⦋n⦌ i.succ) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)) :
      ℕ)
⊢ (↑((Hom.toOrderHom (δ 0 ≫ mkOfSucc i) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋n⦌.len + 1)) x) : ℕ) =
    (↑((Hom.toOrderHom (⦋0⦌.const ⦋n⦌ i.succ) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋n⦌.len + 1)) x) : ℕ)

Tactic:
fin_cases x
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
⊢ (↑((Hom.toOrderHom (δ 0 ≫ mkOfSucc i) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋0⦌.len + 1)))) :
      ℕ) =
    (↑((Hom.toOrderHom (⦋0⦌.const ⦋n⦌ i.succ) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)) :
      ℕ)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
a :
  ∀ (x : Fin (⦋0⦌.len + 1)),
    (↑((Hom.toOrderHom (δ 1 ≫ mkOfSucc i) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋n⦌.len + 1)) x) : ℕ) =
      (↑((Hom.toOrderHom (⦋0⦌.const ⦋n⦌ i.castSucc) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋n⦌.len + 1)) x) : ℕ)
⊢ δ 1 ≫ mkOfSucc i = ⦋0⦌.const ⦋n⦌ i.castSucc

Tactic:
ext x
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
x : Fin (⦋0⦌.len + 1)
a :
  (↑((Hom.toOrderHom (δ 1 ≫ mkOfSucc i) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋0⦌.len + 1)))) :
      ℕ) =
    (↑((Hom.toOrderHom (⦋0⦌.const ⦋n⦌ i.castSucc) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)) :
      ℕ)
⊢ (↑((Hom.toOrderHom (δ 1 ≫ mkOfSucc i) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋n⦌.len + 1)) x) : ℕ) =
    (↑((Hom.toOrderHom (⦋0⦌.const ⦋n⦌ i.castSucc) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋n⦌.len + 1)) x) : ℕ)

Tactic:
fin_cases x
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
⊢ (↑((Hom.toOrderHom (δ 1 ≫ mkOfSucc i) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋0⦌.len + 1)))) :
      ℕ) =
    (↑((Hom.toOrderHom (⦋0⦌.const ⦋n⦌ i.castSucc) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)) :
      ℕ)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
a :
  ∀ (x : Fin (⦋1⦌.len + 1)),
    (↑((Hom.toOrderHom (mkOfSucc i ≫ δ j) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x) : ℕ) =
      (↑((Hom.toOrderHom (mkOfSucc i.castSucc) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x) : ℕ)
⊢ mkOfSucc i ≫ δ j = mkOfSucc i.castSucc

Tactic:
ext x
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
x : Fin (⦋1⦌.len + 1)
a :
  (↑((Hom.toOrderHom (mkOfSucc i ≫ δ j) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1)))) :
      ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.castSucc) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)) :
      ℕ)
a₁ :
  (↑((Hom.toOrderHom (mkOfSucc i ≫ δ j) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1)))) :
      ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.castSucc) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩)) :
      ℕ)
⊢ (↑((Hom.toOrderHom (mkOfSucc i ≫ δ j) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x) : ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.castSucc) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x) : ℕ)

Tactic:
fin_cases x
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
⊢ (↑((Hom.toOrderHom (mkOfSucc i ≫ δ j) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1)))) :
      ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.castSucc) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)) :
      ℕ)

Tactic:
simp [δ, Fin.succAbove_of_castSucc_lt _ _ (Nat.lt_trans _ h)]

Premises used: SimplexCategory.δ, Fin.succAbove_of_castSucc_lt, Nat.lt_trans
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
⊢ (↑((Hom.toOrderHom (mkOfSucc i ≫ δ j) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1)))) :
      ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.castSucc) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩)) :
      ℕ)

Tactic:
simp [δ, Fin.succAbove_of_castSucc_lt _ _ h]

Premises used: SimplexCategory.δ, Fin.succAbove_of_castSucc_lt
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
a :
  ∀ (x : Fin (⦋1⦌.len + 1)),
    (↑((Hom.toOrderHom (mkOfSucc i ≫ δ j) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x) : ℕ) =
      (↑((Hom.toOrderHom (mkOfSucc i.succ) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x) : ℕ)
⊢ mkOfSucc i ≫ δ j = mkOfSucc i.succ

Tactic:
ext x
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
x : Fin (⦋1⦌.len + 1)
a :
  (↑(j.succAbove ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1)) x)) : ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.succ) : (a : Fin (1 + 1)) → Fin (n + 1 + 1)) x) : ℕ)
⊢ (↑((Hom.toOrderHom (mkOfSucc i ≫ δ j) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x) : ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.succ) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x) : ℕ)

Tactic:
simp only [δ, len_mk, mkHom, comp_toOrderHom, Hom.toOrderHom_mk, OrderHom.comp_coe,
    OrderEmbedding.toOrderHom_coe, Function.comp_apply, Fin.succAboveOrderEmb_apply]

Premises used: SimplexCategory.len_mk, OrderEmbedding.toOrderHom_coe, SimplexCategory.mkHom, SimplexCategory.δ, SimplexCategory.Hom.toOrderHom_mk, OrderHom.comp_coe, Function.comp_apply, SimplexCategory.comp_toOrderHom, Fin.succAboveOrderEmb_apply
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
x : Fin (⦋1⦌.len + 1)
a :
  (↑(j.succAbove
          ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1))
            ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1))))) :
      ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.succ) : (a : Fin (1 + 1)) → Fin (n + 1 + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)) :
      ℕ)
a₁ :
  (↑(j.succAbove
          ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1))
            ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1))))) :
      ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.succ) : (a : Fin (1 + 1)) → Fin (n + 1 + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩)) :
      ℕ)
⊢ (↑(j.succAbove ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1)) x)) : ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.succ) : (a : Fin (1 + 1)) → Fin (n + 1 + 1)) x) : ℕ)

Tactic:
fin_cases x
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
a :
  (↑(Fin.succ
          ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1))
            ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1))))) :
      ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.succ) : (a : Fin (1 + 1)) → Fin (n + 1 + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)) :
      ℕ)
a₁ :
  j ≤
    Fin.castSucc
      ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1)) ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩))
⊢ (↑(j.succAbove
          ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1))
            ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1))))) :
      ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.succ) : (a : Fin (1 + 1)) → Fin (n + 1 + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)) :
      ℕ)

Tactic:
rw [Fin.succAbove_of_le_castSucc]

Premises used: Fin.succAbove_of_le_castSucc
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
a :
  (↑(Fin.succ
          ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1))
            ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1))))) :
      ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.succ) : (a : Fin (1 + 1)) → Fin (n + 1 + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩)) :
      ℕ)
a₁ :
  j ≤
    Fin.castSucc
      ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1)) ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩))
⊢ (↑(j.succAbove
          ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1))
            ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1))))) :
      ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.succ) : (a : Fin (1 + 1)) → Fin (n + 1 + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩)) :
      ℕ)

Tactic:
rw [Fin.succAbove_of_le_castSucc]

Premises used: Fin.succAbove_of_le_castSucc
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ (↑(Fin.succ
          ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1))
            ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1))))) :
      ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.succ) : (a : Fin (1 + 1)) → Fin (n + 1 + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)) :
      ℕ)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ j ≤
    Fin.castSucc
      ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1)) ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩))

Tactic:
Nat.le_of_lt_succ h

Premises used: Nat.le_of_lt_succ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ j ≤
    Fin.castSucc
      ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1)) ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩))

Tactic:
exact Nat.le_of_lt_succ h

Premises used: Nat.le_of_lt_succ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ (↑(Fin.succ
          ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1))
            ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1))))) :
      ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.succ) : (a : Fin (1 + 1)) → Fin (n + 1 + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩)) :
      ℕ)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ j ≤
    Fin.castSucc
      ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1)) ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩))

Tactic:
Nat.le_of_lt h

Premises used: Nat.le_of_lt
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ j ≤
    Fin.castSucc
      ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1)) ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩))

Tactic:
exact Nat.le_of_lt h

Premises used: Nat.le_of_lt
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
⊢ (↑i : ℕ) + 2 ≤ n + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
a :
  ∀ (x : Fin (⦋1⦌.len + 1)),
    (↑((Hom.toOrderHom (mkOfSucc i ≫ δ j) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x) : ℕ) =
      (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 ⋯) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x) : ℕ)
⊢ mkOfSucc i ≫ δ j = intervalEdge (↑i : ℕ) 2 ⋯

Tactic:
ext x
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
x : Fin (⦋1⦌.len + 1)
a :
  (↑((Hom.toOrderHom (mkOfSucc i ≫ δ j) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1)))) :
      ℕ) =
    (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 ⋯) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)) :
      ℕ)
a₁ :
  (↑((Hom.toOrderHom (mkOfSucc i ≫ δ j) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋1⦌.len + 1)))) :
      ℕ) =
    (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 ⋯) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, ⋯⟩)) :
      ℕ)
⊢ (↑((Hom.toOrderHom (mkOfSucc i ≫ δ j) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x) : ℕ) =
    (↑((Hom.toOrderHom (intervalEdge (↑i : ℕ) 2 ⋯) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x) : ℕ)

Tactic:
fin_cases x