case mk
n i : ℕ
hi : i < n + 1
⊢ δ (↑Fin.castSucc { val := i, isLt := hi }) ≫ σ { val := i, isLt := hi } = 𝟙 [n]
n : ℕ
i : Fin (n + 1)
⊢ δ (↑Fin.castSucc i) ≫ σ i = 𝟙 [n]
rcases i with ⟨i, hi⟩
case mk.a.h.h.mk.h
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < len [n] + 1
⊢ ↑(↑(Hom.toOrderHom (δ (↑Fin.castSucc { val := i, isLt := hi }) ≫ σ { val := i, isLt := hi }))
        { val := j, isLt := hj }) =
    ↑(↑(Hom.toOrderHom (𝟙 [n])) { val := j, isLt := hj })
case mk
n i : ℕ
hi : i < n + 1
⊢ δ (↑Fin.castSucc { val := i, isLt := hi }) ≫ σ { val := i, isLt := hi } = 𝟙 [n]
ext ⟨j, hj⟩
case mk.a.h.h.mk.h
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
⊢ ↑(↑(Hom.toOrderHom (δ (↑Fin.castSucc { val := i, isLt := hi }) ≫ σ { val := i, isLt := hi }))
        { val := j, isLt := hj }) =
    ↑(↑(Hom.toOrderHom (𝟙 [n])) { val := j, isLt := hj })
case mk.a.h.h.mk.h
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < len [n] + 1
⊢ ↑(↑(Hom.toOrderHom (δ (↑Fin.castSucc { val := i, isLt := hi }) ≫ σ { val := i, isLt := hi }))
        { val := j, isLt := hj }) =
    ↑(↑(Hom.toOrderHom (𝟙 [n])) { val := j, isLt := hj })
simp at hj
case mk.a.h.h.mk.h
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
⊢ ↑(if h :
          { val := i, isLt := (_ : i < Nat.succ (n + 1)) } <
            if { val := j, isLt := (_ : j < Nat.succ (n + 1)) } < { val := i, isLt := (_ : i < Nat.succ (n + 1)) } then
              { val := j, isLt := (_ : j < Nat.succ (n + 1)) }
            else { val := j + 1, isLt := (_ : Nat.succ j < Nat.succ (n + 1)) } then
        Fin.pred
          (if { val := j, isLt := (_ : j < Nat.succ (n + 1)) } < { val := i, isLt := (_ : i < Nat.succ (n + 1)) } then
            { val := j, isLt := (_ : j < Nat.succ (n + 1)) }
          else { val := j + 1, isLt := (_ : Nat.succ j < Nat.succ (n + 1)) })
          (_ :
            (if { val := j, isLt := (_ : j < Nat.succ (n + 1)) } < { val := i, isLt := (_ : i < Nat.succ (n + 1)) } then
                { val := j, isLt := (_ : j < Nat.succ (n + 1)) }
              else { val := j + 1, isLt := (_ : Nat.succ j < Nat.succ (n + 1)) }) ≠
              0)
      else
        Fin.castLT
          (if { val := j, isLt := (_ : j < Nat.succ (n + 1)) } < { val := i, isLt := (_ : i < Nat.succ (n + 1)) } then
            { val := j, isLt := (_ : j < Nat.succ (n + 1)) }
          else { val := j + 1, isLt := (_ : Nat.succ j < Nat.succ (n + 1)) })
          (_ :
            ↑(if
                    { val := j, isLt := (_ : j < Nat.succ (n + 1)) } <
                      { val := i, isLt := (_ : i < Nat.succ (n + 1)) } then
                  { val := j, isLt := (_ : j < Nat.succ (n + 1)) }
                else { val := j + 1, isLt := (_ : Nat.succ j < Nat.succ (n + 1)) }) <
              n + 1)) =
    j
case mk.a.h.h.mk.h
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
⊢ ↑(↑(Hom.toOrderHom (δ (↑Fin.castSucc { val := i, isLt := hi }) ≫ σ { val := i, isLt := hi }))
        { val := j, isLt := hj }) =
    ↑(↑(Hom.toOrderHom (𝟙 [n])) { val := j, isLt := hj })
dsimp [σ, δ, Fin.predAbove, Fin.succAbove]
case mk.a.h.h.mk.h
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
⊢ (if 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 else j + 1) = j
case mk.a.h.h.mk.h
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
⊢ ↑(if h :
          { val := i, isLt := (_ : i < Nat.succ (n + 1)) } <
            if { val := j, isLt := (_ : j < Nat.succ (n + 1)) } < { val := i, isLt := (_ : i < Nat.succ (n + 1)) } then
              { val := j, isLt := (_ : j < Nat.succ (n + 1)) }
            else { val := j + 1, isLt := (_ : Nat.succ j < Nat.succ (n + 1)) } then
        Fin.pred
          (if { val := j, isLt := (_ : j < Nat.succ (n + 1)) } < { val := i, isLt := (_ : i < Nat.succ (n + 1)) } then
            { val := j, isLt := (_ : j < Nat.succ (n + 1)) }
          else { val := j + 1, isLt := (_ : Nat.succ j < Nat.succ (n + 1)) })
          (_ :
            (if { val := j, isLt := (_ : j < Nat.succ (n + 1)) } < { val := i, isLt := (_ : i < Nat.succ (n + 1)) } then
                { val := j, isLt := (_ : j < Nat.succ (n + 1)) }
              else { val := j + 1, isLt := (_ : Nat.succ j < Nat.succ (n + 1)) }) ≠
              0)
      else
        Fin.castLT
          (if { val := j, isLt := (_ : j < Nat.succ (n + 1)) } < { val := i, isLt := (_ : i < Nat.succ (n + 1)) } then
            { val := j, isLt := (_ : j < Nat.succ (n + 1)) }
          else { val := j + 1, isLt := (_ : Nat.succ j < Nat.succ (n + 1)) })
          (_ :
            ↑(if
                    { val := j, isLt := (_ : j < Nat.succ (n + 1)) } <
                      { val := i, isLt := (_ : i < Nat.succ (n + 1)) } then
                  { val := j, isLt := (_ : j < Nat.succ (n + 1)) }
                else { val := j + 1, isLt := (_ : Nat.succ j < Nat.succ (n + 1)) }) <
              n + 1)) =
    j
simp [Fin.lt_iff_val_lt_val, Fin.ite_val, Fin.dite_val]
case mk.a.h.h.mk.h.inl.inl
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : j < i
h✝ : i < j
⊢ j - 1 = j

case mk.a.h.h.mk.h.inl.inr
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : j < i
h✝ : ¬i < j
⊢ j = j

case mk.a.h.h.mk.h.inr.inl
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : ¬j < i
h✝ : i < j + 1
⊢ j + 1 - 1 = j

case mk.a.h.h.mk.h.inr.inr
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : ¬j < i
h✝ : ¬i < j + 1
⊢ j + 1 = j
case mk.a.h.h.mk.h
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
⊢ (if 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 else j + 1) = j
split_ifs
no goals
case mk.a.h.h.mk.h.inl.inl
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : j < i
h✝ : i < j
⊢ j - 1 = j

case mk.a.h.h.mk.h.inl.inr
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : j < i
h✝ : ¬i < j
⊢ j = j

case mk.a.h.h.mk.h.inr.inl
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : ¬j < i
h✝ : i < j + 1
⊢ j + 1 - 1 = j

case mk.a.h.h.mk.h.inr.inr
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : ¬j < i
h✝ : ¬i < j + 1
⊢ j + 1 = j
all_goals try simp <;> linarith
no goals
case mk.a.h.h.mk.h.inr.inr
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : ¬j < i
h✝ : ¬i < j + 1
⊢ j + 1 = j
try simp <;> linarith
no goals
case mk.a.h.h.mk.h.inr.inr
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : ¬j < i
h✝ : ¬i < j + 1
⊢ j + 1 = j
simp <;> linarith