case a.h.h.h
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
k : Fin (len [n] + 1)
⊢ ↑(↑(Hom.toOrderHom (δ i ≫ δ (Fin.succ j))) k) = ↑(↑(Hom.toOrderHom (δ j ≫ δ (↑Fin.castSucc i))) k)
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ δ i ≫ δ (Fin.succ j) = δ j ≫ δ (↑Fin.castSucc i)
ext k
case a.h.h.h
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
k : Fin (len [n] + 1)
⊢ ↑(if ↑Fin.castSucc (if ↑Fin.castSucc k < i then ↑Fin.castSucc k else Fin.succ k) < Fin.succ j then
        ↑Fin.castSucc (if ↑Fin.castSucc k < i then ↑Fin.castSucc k else Fin.succ k)
      else Fin.succ (if ↑Fin.castSucc k < i then ↑Fin.castSucc k else Fin.succ k)) =
    ↑(if ↑Fin.castSucc (if ↑Fin.castSucc k < j then ↑Fin.castSucc k else Fin.succ k) < ↑Fin.castSucc i then
        ↑Fin.castSucc (if ↑Fin.castSucc k < j then ↑Fin.castSucc k else Fin.succ k)
      else Fin.succ (if ↑Fin.castSucc k < j then ↑Fin.castSucc k else Fin.succ k))
case a.h.h.h
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
k : Fin (len [n] + 1)
⊢ ↑(↑(Hom.toOrderHom (δ i ≫ δ (Fin.succ j))) k) = ↑(↑(Hom.toOrderHom (δ j ≫ δ (↑Fin.castSucc i))) k)
dsimp [δ, Fin.succAbove]
case a.h.h.h
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
k : Fin (len [n] + 1)
⊢ ↑(if ↑Fin.castSucc (if ↑Fin.castSucc k < i then ↑Fin.castSucc k else Fin.succ k) < Fin.succ j then
        ↑Fin.castSucc (if ↑Fin.castSucc k < i then ↑Fin.castSucc k else Fin.succ k)
      else Fin.succ (if ↑Fin.castSucc k < i then ↑Fin.castSucc k else Fin.succ k)) =
    ↑(if ↑Fin.castSucc (if ↑Fin.castSucc k < j then ↑Fin.castSucc k else Fin.succ k) < ↑Fin.castSucc i then
        ↑Fin.castSucc (if ↑Fin.castSucc k < j then ↑Fin.castSucc k else Fin.succ k)
      else Fin.succ (if ↑Fin.castSucc k < j then ↑Fin.castSucc k else Fin.succ k))
case a.h.h.h
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
k : Fin (len [n] + 1)
⊢ ↑(if ↑Fin.castSucc (if ↑Fin.castSucc k < i then ↑Fin.castSucc k else Fin.succ k) < Fin.succ j then
        ↑Fin.castSucc (if ↑Fin.castSucc k < i then ↑Fin.castSucc k else Fin.succ k)
      else Fin.succ (if ↑Fin.castSucc k < i then ↑Fin.castSucc k else Fin.succ k)) =
    ↑(if ↑Fin.castSucc (if ↑Fin.castSucc k < j then ↑Fin.castSucc k else Fin.succ k) < ↑Fin.castSucc i then
        ↑Fin.castSucc (if ↑Fin.castSucc k < j then ↑Fin.castSucc k else Fin.succ k)
      else Fin.succ (if ↑Fin.castSucc k < j then ↑Fin.castSucc k else Fin.succ k))
simp only [OrderEmbedding.toOrderHom_coe, OrderEmbedding.coe_ofStrictMono, Function.comp_apply,
  SimplexCategory.Hom.toOrderHom_mk, OrderHom.comp_coe]
case a.h.h.h.mk
n : ℕ
j : Fin (n + 2)
k : Fin (len [n] + 1)
i : ℕ
isLt✝ : i < n + 2
H : { val := i, isLt := isLt✝ } ≤ j
⊢ ↑(if
          ↑Fin.castSucc (if ↑Fin.castSucc k < { val := i, isLt := isLt✝ } then ↑Fin.castSucc k else Fin.succ k) <
            Fin.succ j then
        ↑Fin.castSucc (if ↑Fin.castSucc k < { val := i, isLt := isLt✝ } then ↑Fin.castSucc k else Fin.succ k)
      else Fin.succ (if ↑Fin.castSucc k < { val := i, isLt := isLt✝ } then ↑Fin.castSucc k else Fin.succ k)) =
    ↑(if
          ↑Fin.castSucc (if ↑Fin.castSucc k < j then ↑Fin.castSucc k else Fin.succ k) <
            ↑Fin.castSucc { val := i, isLt := isLt✝ } then
        ↑Fin.castSucc (if ↑Fin.castSucc k < j then ↑Fin.castSucc k else Fin.succ k)
      else Fin.succ (if ↑Fin.castSucc k < j then ↑Fin.castSucc k else Fin.succ k))
case a.h.h.h
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
k : Fin (len [n] + 1)
⊢ ↑(if ↑Fin.castSucc (if ↑Fin.castSucc k < i then ↑Fin.castSucc k else Fin.succ k) < Fin.succ j then
        ↑Fin.castSucc (if ↑Fin.castSucc k < i then ↑Fin.castSucc k else Fin.succ k)
      else Fin.succ (if ↑Fin.castSucc k < i then ↑Fin.castSucc k else Fin.succ k)) =
    ↑(if ↑Fin.castSucc (if ↑Fin.castSucc k < j then ↑Fin.castSucc k else Fin.succ k) < ↑Fin.castSucc i then
        ↑Fin.castSucc (if ↑Fin.castSucc k < j then ↑Fin.castSucc k else Fin.succ k)
      else Fin.succ (if ↑Fin.castSucc k < j then ↑Fin.castSucc k else Fin.succ k))
rcases i with ⟨i, _⟩
case a.h.h.h.mk.mk
n : ℕ
k : Fin (len [n] + 1)
i : ℕ
isLt✝¹ : i < n + 2
j : ℕ
isLt✝ : j < n + 2
H : { val := i, isLt := isLt✝¹ } ≤ { val := j, isLt := isLt✝ }
⊢ ↑(if
          ↑Fin.castSucc (if ↑Fin.castSucc k < { val := i, isLt := isLt✝¹ } then ↑Fin.castSucc k else Fin.succ k) <
            Fin.succ { val := j, isLt := isLt✝ } then
        ↑Fin.castSucc (if ↑Fin.castSucc k < { val := i, isLt := isLt✝¹ } then ↑Fin.castSucc k else Fin.succ k)
      else Fin.succ (if ↑Fin.castSucc k < { val := i, isLt := isLt✝¹ } then ↑Fin.castSucc k else Fin.succ k)) =
    ↑(if
          ↑Fin.castSucc (if ↑Fin.castSucc k < { val := j, isLt := isLt✝ } then ↑Fin.castSucc k else Fin.succ k) <
            ↑Fin.castSucc { val := i, isLt := isLt✝¹ } then
        ↑Fin.castSucc (if ↑Fin.castSucc k < { val := j, isLt := isLt✝ } then ↑Fin.castSucc k else Fin.succ k)
      else Fin.succ (if ↑Fin.castSucc k < { val := j, isLt := isLt✝ } then ↑Fin.castSucc k else Fin.succ k))
case a.h.h.h.mk
n : ℕ
j : Fin (n + 2)
k : Fin (len [n] + 1)
i : ℕ
isLt✝ : i < n + 2
H : { val := i, isLt := isLt✝ } ≤ j
⊢ ↑(if
          ↑Fin.castSucc (if ↑Fin.castSucc k < { val := i, isLt := isLt✝ } then ↑Fin.castSucc k else Fin.succ k) <
            Fin.succ j then
        ↑Fin.castSucc (if ↑Fin.castSucc k < { val := i, isLt := isLt✝ } then ↑Fin.castSucc k else Fin.succ k)
      else Fin.succ (if ↑Fin.castSucc k < { val := i, isLt := isLt✝ } then ↑Fin.castSucc k else Fin.succ k)) =
    ↑(if
          ↑Fin.castSucc (if ↑Fin.castSucc k < j then ↑Fin.castSucc k else Fin.succ k) <
            ↑Fin.castSucc { val := i, isLt := isLt✝ } then
        ↑Fin.castSucc (if ↑Fin.castSucc k < j then ↑Fin.castSucc k else Fin.succ k)
      else Fin.succ (if ↑Fin.castSucc k < j then ↑Fin.castSucc k else Fin.succ k))
rcases j with ⟨j, _⟩
case a.h.h.h.mk.mk.mk
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : { val := i, isLt := isLt✝² } ≤ { val := j, isLt := isLt✝¹ }
k : ℕ
isLt✝ : k < len [n] + 1
⊢ ↑(if
          ↑Fin.castSucc
              (if ↑Fin.castSucc { val := k, isLt := isLt✝ } < { val := i, isLt := isLt✝² } then
                ↑Fin.castSucc { val := k, isLt := isLt✝ }
              else Fin.succ { val := k, isLt := isLt✝ }) <
            Fin.succ { val := j, isLt := isLt✝¹ } then
        ↑Fin.castSucc
          (if ↑Fin.castSucc { val := k, isLt := isLt✝ } < { val := i, isLt := isLt✝² } then
            ↑Fin.castSucc { val := k, isLt := isLt✝ }
          else Fin.succ { val := k, isLt := isLt✝ })
      else
        Fin.succ
          (if ↑Fin.castSucc { val := k, isLt := isLt✝ } < { val := i, isLt := isLt✝² } then
            ↑Fin.castSucc { val := k, isLt := isLt✝ }
          else Fin.succ { val := k, isLt := isLt✝ })) =
    ↑(if
          ↑Fin.castSucc
              (if ↑Fin.castSucc { val := k, isLt := isLt✝ } < { val := j, isLt := isLt✝¹ } then
                ↑Fin.castSucc { val := k, isLt := isLt✝ }
              else Fin.succ { val := k, isLt := isLt✝ }) <
            ↑Fin.castSucc { val := i, isLt := isLt✝² } then
        ↑Fin.castSucc
          (if ↑Fin.castSucc { val := k, isLt := isLt✝ } < { val := j, isLt := isLt✝¹ } then
            ↑Fin.castSucc { val := k, isLt := isLt✝ }
          else Fin.succ { val := k, isLt := isLt✝ })
      else
        Fin.succ
          (if ↑Fin.castSucc { val := k, isLt := isLt✝ } < { val := j, isLt := isLt✝¹ } then
            ↑Fin.castSucc { val := k, isLt := isLt✝ }
          else Fin.succ { val := k, isLt := isLt✝ }))
case a.h.h.h.mk.mk
n : ℕ
k : Fin (len [n] + 1)
i : ℕ
isLt✝¹ : i < n + 2
j : ℕ
isLt✝ : j < n + 2
H : { val := i, isLt := isLt✝¹ } ≤ { val := j, isLt := isLt✝ }
⊢ ↑(if
          ↑Fin.castSucc (if ↑Fin.castSucc k < { val := i, isLt := isLt✝¹ } then ↑Fin.castSucc k else Fin.succ k) <
            Fin.succ { val := j, isLt := isLt✝ } then
        ↑Fin.castSucc (if ↑Fin.castSucc k < { val := i, isLt := isLt✝¹ } then ↑Fin.castSucc k else Fin.succ k)
      else Fin.succ (if ↑Fin.castSucc k < { val := i, isLt := isLt✝¹ } then ↑Fin.castSucc k else Fin.succ k)) =
    ↑(if
          ↑Fin.castSucc (if ↑Fin.castSucc k < { val := j, isLt := isLt✝ } then ↑Fin.castSucc k else Fin.succ k) <
            ↑Fin.castSucc { val := i, isLt := isLt✝¹ } then
        ↑Fin.castSucc (if ↑Fin.castSucc k < { val := j, isLt := isLt✝ } then ↑Fin.castSucc k else Fin.succ k)
      else Fin.succ (if ↑Fin.castSucc k < { val := j, isLt := isLt✝ } then ↑Fin.castSucc k else Fin.succ k))
rcases k with ⟨k, _⟩
no goals
case a.h.h.h.mk.mk.mk.inr.inr.inr.inr
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : { val := i, isLt := isLt✝² } ≤ { val := j, isLt := isLt✝¹ }
k : ℕ
isLt✝ : k < len [n] + 1
h✝³ : ¬↑Fin.castSucc { val := k, isLt := isLt✝ } < { val := i, isLt := isLt✝² }
h✝² : ¬↑Fin.castSucc (Fin.succ { val := k, isLt := isLt✝ }) < Fin.succ { val := j, isLt := isLt✝¹ }
h✝¹ : ¬↑Fin.castSucc { val := k, isLt := isLt✝ } < { val := j, isLt := isLt✝¹ }
h✝ : ¬↑Fin.castSucc (Fin.succ { val := k, isLt := isLt✝ }) < ↑Fin.castSucc { val := i, isLt := isLt✝² }
⊢ ↑(Fin.succ (Fin.succ { val := k, isLt := isLt✝ })) = ↑(Fin.succ (Fin.succ { val := k, isLt := isLt✝ }))
simp at * <;> linarith