-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
/-- If `i + 1 > j`, `mkOfSucc i ≫ δ j` is the morphism `⦋1⦌ ⟶ ⦋n⦌` that
sends `0` and `1` to `i + 1` and `i + 2`, respectively. -/
lemma mkOfSucc_δ_gt {n : ℕ} {i : Fin n} {j : Fin (n + 2)}
    (h : j < i.succ.castSucc) :
    mkOfSucc i ≫ δ j = mkOfSucc i.succ

Proof state:
case a.h.h.h.«_@».Mathlib.AlgebraicTopology.SimplexCategory.Defs._hyg.913.«1».h
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ j ≤ ((Hom.toOrderHom (mkOfSucc i)) ((fun i => i) ⟨1, ⋯⟩)).castSucc

Tactic:
exact Nat.le_of_lt h

Result:
no goals

Proof state:
case a.h.h.h
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
x : Fin (⦋1⦌.len + 1)
⊢ ↑(j.succAbove ((Hom.toOrderHom (mkOfSucc i)) x)) = ↑((Hom.toOrderHom (mkOfSucc i.succ)) x)

Tactic:
fin_cases x <;> rw [Fin.succAbove_of_le_castSucc]

Result:
case a.h.h.h.«_@».Mathlib.AlgebraicTopology.SimplexCategory.Defs._hyg.913.«0»
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ ↑((Hom.toOrderHom (mkOfSucc i)) ((fun i => i) ⟨0, ⋯⟩)).succ =
    ↑((Hom.toOrderHom (mkOfSucc i.succ)) ((fun i => i) ⟨0, ⋯⟩))

case a.h.h.h.«_@».Mathlib.AlgebraicTopology.SimplexCategory.Defs._hyg.913.«0».h
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ j ≤ ((Hom.toOrderHom (mkOfSucc i)) ((fun i => i) ⟨0, ⋯⟩)).castSucc

case a.h.h.h.«_@».Mathlib.AlgebraicTopology.SimplexCategory.Defs._hyg.913.«1»
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ ↑((Hom.toOrderHom (mkOfSucc i)) ((fun i => i) ⟨1, ⋯⟩)).succ =
    ↑((Hom.toOrderHom (mkOfSucc i.succ)) ((fun i => i) ⟨1, ⋯⟩))

case a.h.h.h.«_@».Mathlib.AlgebraicTopology.SimplexCategory.Defs._hyg.913.«1».h
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ j ≤ ((Hom.toOrderHom (mkOfSucc i)) ((fun i => i) ⟨1, ⋯⟩)).castSucc

Proof state:
case a.h.h.h.«_@».Mathlib.AlgebraicTopology.SimplexCategory.Defs._hyg.913.«0»
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ ↑((Hom.toOrderHom (mkOfSucc i)) ((fun i => i) ⟨0, ⋯⟩)).succ =
    ↑((Hom.toOrderHom (mkOfSucc i.succ)) ((fun i => i) ⟨0, ⋯⟩))

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ mkOfSucc i ≫ δ j = mkOfSucc i.succ

Tactic:
ext x

Result:
case a.h.h.h
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
x : Fin (⦋1⦌.len + 1)
⊢ ↑((Hom.toOrderHom (mkOfSucc i ≫ δ j)) x) = ↑((Hom.toOrderHom (mkOfSucc i.succ)) x)

Proof state:
case a.h.h.h.«_@».Mathlib.AlgebraicTopology.SimplexCategory.Defs._hyg.913.«0».h
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ j ≤ ((Hom.toOrderHom (mkOfSucc i)) ((fun i => i) ⟨0, ⋯⟩)).castSucc

Tactic:
exact Nat.le_of_lt_succ h

Result:
no goals

Proof state:
case a.h.h.h
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
x : Fin (⦋1⦌.len + 1)
⊢ ↑((Hom.toOrderHom (mkOfSucc i ≫ δ j)) x) = ↑((Hom.toOrderHom (mkOfSucc i.succ)) x)

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

Result:
case a.h.h.h
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
x : Fin (⦋1⦌.len + 1)
⊢ ↑(j.succAbove ((Hom.toOrderHom (mkOfSucc i)) x)) = ↑((Hom.toOrderHom (mkOfSucc i.succ)) x)

Proof state:
case a.h.h.h.«_@».Mathlib.AlgebraicTopology.SimplexCategory.Defs._hyg.913.«1»
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ ↑((Hom.toOrderHom (mkOfSucc i)) ((fun i => i) ⟨1, ⋯⟩)).succ =
    ↑((Hom.toOrderHom (mkOfSucc i.succ)) ((fun i => i) ⟨1, ⋯⟩))

Tactic:
rfl

Result:
no goals