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

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 (intervalEdge (↑i) 2 ⋯)) x)

Tactic:
fin_cases x

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 ≫ δ j)) ((fun i => i) ⟨0, ⋯⟩)) =
    ↑((Hom.toOrderHom (intervalEdge (↑i) 2 ⋯)) ((fun i => i) ⟨0, ⋯⟩))

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 ≫ δ j)) ((fun i => i) ⟨1, ⋯⟩)) =
    ↑((Hom.toOrderHom (intervalEdge (↑i) 2 ⋯)) ((fun i => i) ⟨1, ⋯⟩))

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

Tactic:
simp only [δ, len_mk, Nat.reduceAdd, mkHom, comp_toOrderHom, Hom.toOrderHom_mk,
  Fin.zero_eta, OrderHom.comp_coe, OrderEmbedding.toOrderHom_coe, Function.comp_apply,
  mkOfSucc_homToOrderHom_zero, Fin.succAboveOrderEmb_apply,
  Fin.castSucc_succAbove_castSucc, Fin.succAbove_succ_self]

Result:
case a.h.h.h.«_@».Mathlib.AlgebraicTopology.SimplexCategory.Defs._hyg.913.«0»
n : ℕ
i : Fin n
⊢ ↑i.castSucc.castSucc = ↑((Hom.toOrderHom (intervalEdge (↑i) 2 ⋯)) 0)

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

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 (intervalEdge (↑i) 2 ⋯)) x)

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 ≫ δ j)) ((fun i => i) ⟨0, ⋯⟩)) =
    ↑((Hom.toOrderHom (intervalEdge (↑i) 2 ⋯)) ((fun i => i) ⟨0, ⋯⟩))

Tactic:
subst h

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

Proof state:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
⊢ ↑i + 2 ≤ n + 1

Tactic:
omega

Result:
no goals

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 ≫ δ j)) ((fun i => i) ⟨1, ⋯⟩)) =
    ↑((Hom.toOrderHom (intervalEdge (↑i) 2 ⋯)) ((fun i => i) ⟨1, ⋯⟩))

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

Result:
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
⊢ ↑(j.succAbove i.succ) = ↑((Hom.toOrderHom (intervalEdge (↑i) 2 ⋯)) 1)

Proof state:
case a.h.h.h.«_@».Mathlib.AlgebraicTopology.SimplexCategory.Defs._hyg.913.«0»
n : ℕ
i : Fin n
⊢ ↑i.castSucc.castSucc = ↑((Hom.toOrderHom (intervalEdge (↑i) 2 ⋯)) 0)

Tactic:
rfl

Result:
no goals

Proof state:
case a.h.h.h.«_@».Mathlib.AlgebraicTopology.SimplexCategory.Defs._hyg.913.«1»
n : ℕ
i : Fin n
⊢ ↑(i.succ.castSucc.succAbove i.succ) = ↑((Hom.toOrderHom (intervalEdge (↑i) 2 ⋯)) 1)

Tactic:
rw [Fin.succAbove_castSucc_self]

Result:
case a.h.h.h.«_@».Mathlib.AlgebraicTopology.SimplexCategory.Defs._hyg.913.«1»
n : ℕ
i : Fin n
⊢ ↑i.succ.succ = ↑((Hom.toOrderHom (intervalEdge (↑i) 2 ⋯)) 1)

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
⊢ ↑(j.succAbove i.succ) = ↑((Hom.toOrderHom (intervalEdge (↑i) 2 ⋯)) 1)

Tactic:
subst h

Result:
case a.h.h.h.«_@».Mathlib.AlgebraicTopology.SimplexCategory.Defs._hyg.913.«1»
n : ℕ
i : Fin n
⊢ ↑(i.succ.castSucc.succAbove i.succ) = ↑((Hom.toOrderHom (intervalEdge (↑i) 2 ⋯)) 1)

Proof state:
case a.h.h.h.«_@».Mathlib.AlgebraicTopology.SimplexCategory.Defs._hyg.913.«1»
n : ℕ
i : Fin n
⊢ ↑i.succ.succ = ↑((Hom.toOrderHom (intervalEdge (↑i) 2 ⋯)) 1)

Tactic:
rfl

Result:
no goals