[GOAL]
x : SimplexCategory
i : Fin (len x + 1)
⊢ Monotone fun x => i
[PROOFSTEP]
tauto
[GOAL]
f : [0] ⟶ [0]
⊢ f = 𝟙 [0]
[PROOFSTEP]
ext : 3
[GOAL]
case a.h.h
f : [0] ⟶ [0]
x✝ : Fin (len [0] + 1)
⊢ ↑(Hom.toOrderHom f) x✝ = ↑(Hom.toOrderHom (𝟙 [0])) x✝
[PROOFSTEP]
apply @Subsingleton.elim (Fin 1)
[GOAL]
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ δ i ≫ δ (Fin.succ j) = δ j ≫ δ (Fin.castSucc i)
[PROOFSTEP]
ext k
[GOAL]
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)
[PROOFSTEP]
dsimp [δ, Fin.succAbove]
[GOAL]
case a.h.h.h
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
k : Fin (len [n] + 1)
⊢ ↑(if ↑(if ↑k < ↑i then Fin.castSucc k else Fin.succ k) < ↑(Fin.succ j) then
        Fin.castSucc (if ↑k < ↑i then Fin.castSucc k else Fin.succ k)
      else Fin.succ (if ↑k < ↑i then Fin.castSucc k else Fin.succ k)) =
    ↑(if ↑(if ↑k < ↑j then Fin.castSucc k else Fin.succ k) < ↑i then
        Fin.castSucc (if ↑k < ↑j then Fin.castSucc k else Fin.succ k)
      else Fin.succ (if ↑k < ↑j then Fin.castSucc k else Fin.succ k))
[PROOFSTEP]
rcases i with ⟨i, _⟩
[GOAL]
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 ↑(if ↑k < ↑{ val := i, isLt := isLt✝ } then Fin.castSucc k else Fin.succ k) < ↑(Fin.succ j) then
        Fin.castSucc (if ↑k < ↑{ val := i, isLt := isLt✝ } then Fin.castSucc k else Fin.succ k)
      else Fin.succ (if ↑k < ↑{ val := i, isLt := isLt✝ } then Fin.castSucc k else Fin.succ k)) =
    ↑(if ↑(if ↑k < ↑j then Fin.castSucc k else Fin.succ k) < ↑{ val := i, isLt := isLt✝ } then
        Fin.castSucc (if ↑k < ↑j then Fin.castSucc k else Fin.succ k)
      else Fin.succ (if ↑k < ↑j then Fin.castSucc k else Fin.succ k))
[PROOFSTEP]
rcases j with ⟨j, _⟩
[GOAL]
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
          ↑(if ↑k < ↑{ val := i, isLt := isLt✝¹ } then Fin.castSucc k else Fin.succ k) <
            ↑(Fin.succ { val := j, isLt := isLt✝ }) then
        Fin.castSucc (if ↑k < ↑{ val := i, isLt := isLt✝¹ } then Fin.castSucc k else Fin.succ k)
      else Fin.succ (if ↑k < ↑{ val := i, isLt := isLt✝¹ } then Fin.castSucc k else Fin.succ k)) =
    ↑(if
          ↑(if ↑k < ↑{ val := j, isLt := isLt✝ } then Fin.castSucc k else Fin.succ k) <
            ↑{ val := i, isLt := isLt✝¹ } then
        Fin.castSucc (if ↑k < ↑{ val := j, isLt := isLt✝ } then Fin.castSucc k else Fin.succ k)
      else Fin.succ (if ↑k < ↑{ val := j, isLt := isLt✝ } then Fin.castSucc k else Fin.succ k))
[PROOFSTEP]
rcases k with ⟨k, _⟩
[GOAL]
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
          ↑(if ↑{ 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 ↑{ 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 ↑{ val := k, isLt := isLt✝ } < ↑{ val := i, isLt := isLt✝² } then Fin.castSucc { val := k, isLt := isLt✝ }
          else Fin.succ { val := k, isLt := isLt✝ })) =
    ↑(if
          ↑(if ↑{ val := k, isLt := isLt✝ } < ↑{ val := j, isLt := isLt✝¹ } then
                Fin.castSucc { val := k, isLt := isLt✝ }
              else Fin.succ { val := k, isLt := isLt✝ }) <
            ↑{ val := i, isLt := isLt✝² } then
        Fin.castSucc
          (if ↑{ 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 ↑{ val := k, isLt := isLt✝ } < ↑{ val := j, isLt := isLt✝¹ } then Fin.castSucc { val := k, isLt := isLt✝ }
          else Fin.succ { val := k, isLt := isLt✝ }))
[PROOFSTEP]
split_ifs
[GOAL]
case pos
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✝³ : ↑{ val := k, isLt := isLt✝ } < ↑{ val := i, isLt := isLt✝² }
h✝² : ↑(Fin.castSucc { val := k, isLt := isLt✝ }) < ↑(Fin.succ { val := j, isLt := isLt✝¹ })
h✝¹ : ↑{ val := k, isLt := isLt✝ } < ↑{ val := j, isLt := isLt✝¹ }
h✝ : ↑(Fin.castSucc { val := k, isLt := isLt✝ }) < ↑{ val := i, isLt := isLt✝² }
⊢ ↑(Fin.castSucc (Fin.castSucc { val := k, isLt := isLt✝ })) =
    ↑(Fin.castSucc (Fin.castSucc { val := k, isLt := isLt✝ }))
[PROOFSTEP]
simp at *
[GOAL]
case neg
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✝³ : ↑{ val := k, isLt := isLt✝ } < ↑{ val := i, isLt := isLt✝² }
h✝² : ↑(Fin.castSucc { val := k, isLt := isLt✝ }) < ↑(Fin.succ { val := j, isLt := isLt✝¹ })
h✝¹ : ↑{ val := k, isLt := isLt✝ } < ↑{ val := j, isLt := isLt✝¹ }
h✝ : ¬↑(Fin.castSucc { val := k, isLt := isLt✝ }) < ↑{ val := i, isLt := isLt✝² }
⊢ ↑(Fin.castSucc (Fin.castSucc { val := k, isLt := isLt✝ })) = ↑(Fin.succ (Fin.castSucc { val := k, isLt := isLt✝ }))
[PROOFSTEP]
simp at *
[GOAL]
case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < len [n] + 1
h✝³ : k < i
h✝² : k < j + 1
h✝¹ : k < j
H : i ≤ j
h✝ : i ≤ k
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case pos
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✝³ : ↑{ val := k, isLt := isLt✝ } < ↑{ val := i, isLt := isLt✝² }
h✝² : ↑(Fin.castSucc { val := k, isLt := isLt✝ }) < ↑(Fin.succ { val := j, isLt := isLt✝¹ })
h✝¹ : ¬↑{ val := k, isLt := isLt✝ } < ↑{ val := j, isLt := isLt✝¹ }
h✝ : ↑(Fin.succ { val := k, isLt := isLt✝ }) < ↑{ val := i, isLt := isLt✝² }
⊢ ↑(Fin.castSucc (Fin.castSucc { val := k, isLt := isLt✝ })) = ↑(Fin.castSucc (Fin.succ { val := k, isLt := isLt✝ }))
[PROOFSTEP]
simp at *
[GOAL]
case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < len [n] + 1
h✝³ : k < i
h✝² : k < j + 1
h✝¹ : k + 1 < i
H : i ≤ j
h✝ : j ≤ k
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case neg
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✝³ : ↑{ val := k, isLt := isLt✝ } < ↑{ val := i, isLt := isLt✝² }
h✝² : ↑(Fin.castSucc { val := k, isLt := isLt✝ }) < ↑(Fin.succ { val := j, isLt := isLt✝¹ })
h✝¹ : ¬↑{ val := k, isLt := isLt✝ } < ↑{ val := j, isLt := isLt✝¹ }
h✝ : ¬↑(Fin.succ { val := k, isLt := isLt✝ }) < ↑{ val := i, isLt := isLt✝² }
⊢ ↑(Fin.castSucc (Fin.castSucc { val := k, isLt := isLt✝ })) = ↑(Fin.succ (Fin.succ { val := k, isLt := isLt✝ }))
[PROOFSTEP]
simp at *
[GOAL]
case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < len [n] + 1
h✝³ : k < i
h✝² : k < j + 1
H : i ≤ j
h✝¹ : j ≤ k
h✝ : i ≤ k + 1
⊢ k = k + 1 + 1
[PROOFSTEP]
linarith
[GOAL]
case pos
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✝³ : ↑{ val := k, isLt := isLt✝ } < ↑{ val := i, isLt := isLt✝² }
h✝² : ¬↑(Fin.castSucc { val := k, isLt := isLt✝ }) < ↑(Fin.succ { val := j, isLt := isLt✝¹ })
h✝¹ : ↑{ val := k, isLt := isLt✝ } < ↑{ val := j, isLt := isLt✝¹ }
h✝ : ↑(Fin.castSucc { val := k, isLt := isLt✝ }) < ↑{ val := i, isLt := isLt✝² }
⊢ ↑(Fin.succ (Fin.castSucc { val := k, isLt := isLt✝ })) = ↑(Fin.castSucc (Fin.castSucc { val := k, isLt := isLt✝ }))
[PROOFSTEP]
simp at *
[GOAL]
case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < len [n] + 1
h✝³ : k < i
h✝² : k < j
h✝¹ : k < i
H : i ≤ j
h✝ : j + 1 ≤ k
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case neg
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✝³ : ↑{ val := k, isLt := isLt✝ } < ↑{ val := i, isLt := isLt✝² }
h✝² : ¬↑(Fin.castSucc { val := k, isLt := isLt✝ }) < ↑(Fin.succ { val := j, isLt := isLt✝¹ })
h✝¹ : ↑{ val := k, isLt := isLt✝ } < ↑{ val := j, isLt := isLt✝¹ }
h✝ : ¬↑(Fin.castSucc { val := k, isLt := isLt✝ }) < ↑{ val := i, isLt := isLt✝² }
⊢ ↑(Fin.succ (Fin.castSucc { val := k, isLt := isLt✝ })) = ↑(Fin.succ (Fin.castSucc { val := k, isLt := isLt✝ }))
[PROOFSTEP]
simp at *
[GOAL]
case pos
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✝³ : ↑{ val := k, isLt := isLt✝ } < ↑{ val := i, isLt := isLt✝² }
h✝² : ¬↑(Fin.castSucc { val := k, isLt := isLt✝ }) < ↑(Fin.succ { val := j, isLt := isLt✝¹ })
h✝¹ : ¬↑{ val := k, isLt := isLt✝ } < ↑{ val := j, isLt := isLt✝¹ }
h✝ : ↑(Fin.succ { val := k, isLt := isLt✝ }) < ↑{ val := i, isLt := isLt✝² }
⊢ ↑(Fin.succ (Fin.castSucc { val := k, isLt := isLt✝ })) = ↑(Fin.castSucc (Fin.succ { val := k, isLt := isLt✝ }))
[PROOFSTEP]
simp at *
[GOAL]
case neg
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✝³ : ↑{ val := k, isLt := isLt✝ } < ↑{ val := i, isLt := isLt✝² }
h✝² : ¬↑(Fin.castSucc { val := k, isLt := isLt✝ }) < ↑(Fin.succ { val := j, isLt := isLt✝¹ })
h✝¹ : ¬↑{ val := k, isLt := isLt✝ } < ↑{ val := j, isLt := isLt✝¹ }
h✝ : ¬↑(Fin.succ { val := k, isLt := isLt✝ }) < ↑{ val := i, isLt := isLt✝² }
⊢ ↑(Fin.succ (Fin.castSucc { val := k, isLt := isLt✝ })) = ↑(Fin.succ (Fin.succ { val := k, isLt := isLt✝ }))
[PROOFSTEP]
simp at *
[GOAL]
case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < len [n] + 1
h✝³ : k < i
H : i ≤ j
h✝² : j + 1 ≤ k
h✝¹ : j ≤ k
h✝ : i ≤ k + 1
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case pos
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✝³ : ¬↑{ val := k, isLt := isLt✝ } < ↑{ val := i, isLt := isLt✝² }
h✝² : ↑(Fin.succ { val := k, isLt := isLt✝ }) < ↑(Fin.succ { val := j, isLt := isLt✝¹ })
h✝¹ : ↑{ val := k, isLt := isLt✝ } < ↑{ val := j, isLt := isLt✝¹ }
h✝ : ↑(Fin.castSucc { val := k, isLt := isLt✝ }) < ↑{ val := i, isLt := isLt✝² }
⊢ ↑(Fin.castSucc (Fin.succ { val := k, isLt := isLt✝ })) = ↑(Fin.castSucc (Fin.castSucc { val := k, isLt := isLt✝ }))
[PROOFSTEP]
simp at *
[GOAL]
case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < len [n] + 1
h✝³ : k < j
h✝² : k < i
H : i ≤ j
h✝¹ : i ≤ k
h✝ : k < j
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case neg
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✝³ : ¬↑{ val := k, isLt := isLt✝ } < ↑{ val := i, isLt := isLt✝² }
h✝² : ↑(Fin.succ { val := k, isLt := isLt✝ }) < ↑(Fin.succ { val := j, isLt := isLt✝¹ })
h✝¹ : ↑{ val := k, isLt := isLt✝ } < ↑{ val := j, isLt := isLt✝¹ }
h✝ : ¬↑(Fin.castSucc { val := k, isLt := isLt✝ }) < ↑{ val := i, isLt := isLt✝² }
⊢ ↑(Fin.castSucc (Fin.succ { val := k, isLt := isLt✝ })) = ↑(Fin.succ (Fin.castSucc { val := k, isLt := isLt✝ }))
[PROOFSTEP]
simp at *
[GOAL]
case pos
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✝³ : ¬↑{ val := k, isLt := isLt✝ } < ↑{ val := i, isLt := isLt✝² }
h✝² : ↑(Fin.succ { val := k, isLt := isLt✝ }) < ↑(Fin.succ { val := j, isLt := isLt✝¹ })
h✝¹ : ¬↑{ val := k, isLt := isLt✝ } < ↑{ val := j, isLt := isLt✝¹ }
h✝ : ↑(Fin.succ { val := k, isLt := isLt✝ }) < ↑{ val := i, isLt := isLt✝² }
⊢ ↑(Fin.castSucc (Fin.succ { val := k, isLt := isLt✝ })) = ↑(Fin.castSucc (Fin.succ { val := k, isLt := isLt✝ }))
[PROOFSTEP]
simp at *
[GOAL]
case neg
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✝³ : ¬↑{ val := k, isLt := isLt✝ } < ↑{ val := i, isLt := isLt✝² }
h✝² : ↑(Fin.succ { val := k, isLt := isLt✝ }) < ↑(Fin.succ { val := j, isLt := isLt✝¹ })
h✝¹ : ¬↑{ val := k, isLt := isLt✝ } < ↑{ val := j, isLt := isLt✝¹ }
h✝ : ¬↑(Fin.succ { val := k, isLt := isLt✝ }) < ↑{ val := i, isLt := isLt✝² }
⊢ ↑(Fin.castSucc (Fin.succ { val := k, isLt := isLt✝ })) = ↑(Fin.succ (Fin.succ { val := k, isLt := isLt✝ }))
[PROOFSTEP]
simp at *
[GOAL]
case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < len [n] + 1
H : i ≤ j
h✝³ : i ≤ k
h✝² : k < j
h✝¹ : j ≤ k
h✝ : i ≤ k + 1
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case pos
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✝³ : ¬↑{ val := k, isLt := isLt✝ } < ↑{ val := i, isLt := isLt✝² }
h✝² : ¬↑(Fin.succ { val := k, isLt := isLt✝ }) < ↑(Fin.succ { val := j, isLt := isLt✝¹ })
h✝¹ : ↑{ val := k, isLt := isLt✝ } < ↑{ val := j, isLt := isLt✝¹ }
h✝ : ↑(Fin.castSucc { val := k, isLt := isLt✝ }) < ↑{ val := i, isLt := isLt✝² }
⊢ ↑(Fin.succ (Fin.succ { val := k, isLt := isLt✝ })) = ↑(Fin.castSucc (Fin.castSucc { val := k, isLt := isLt✝ }))
[PROOFSTEP]
simp at *
[GOAL]
case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < len [n] + 1
h✝³ : k < j
h✝² : k < i
H : i ≤ j
h✝¹ : i ≤ k
h✝ : j ≤ k
⊢ k + 1 + 1 = k
[PROOFSTEP]
linarith
[GOAL]
case neg
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✝³ : ¬↑{ val := k, isLt := isLt✝ } < ↑{ val := i, isLt := isLt✝² }
h✝² : ¬↑(Fin.succ { val := k, isLt := isLt✝ }) < ↑(Fin.succ { val := j, isLt := isLt✝¹ })
h✝¹ : ↑{ val := k, isLt := isLt✝ } < ↑{ val := j, isLt := isLt✝¹ }
h✝ : ¬↑(Fin.castSucc { val := k, isLt := isLt✝ }) < ↑{ val := i, isLt := isLt✝² }
⊢ ↑(Fin.succ (Fin.succ { val := k, isLt := isLt✝ })) = ↑(Fin.succ (Fin.castSucc { val := k, isLt := isLt✝ }))
[PROOFSTEP]
simp at *
[GOAL]
case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < len [n] + 1
h✝³ : k < j
H : i ≤ j
h✝² : i ≤ k
h✝¹ : j ≤ k
h✝ : i ≤ k
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case pos
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✝³ : ¬↑{ val := k, isLt := isLt✝ } < ↑{ val := i, isLt := isLt✝² }
h✝² : ¬↑(Fin.succ { val := k, isLt := isLt✝ }) < ↑(Fin.succ { val := j, isLt := isLt✝¹ })
h✝¹ : ¬↑{ val := k, isLt := isLt✝ } < ↑{ val := j, isLt := isLt✝¹ }
h✝ : ↑(Fin.succ { val := k, isLt := isLt✝ }) < ↑{ val := i, isLt := isLt✝² }
⊢ ↑(Fin.succ (Fin.succ { val := k, isLt := isLt✝ })) = ↑(Fin.castSucc (Fin.succ { val := k, isLt := isLt✝ }))
[PROOFSTEP]
simp at *
[GOAL]
case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < len [n] + 1
h✝³ : k + 1 < i
H : i ≤ j
h✝² : i ≤ k
h✝¹ h✝ : j ≤ k
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case neg
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✝³ : ¬↑{ val := k, isLt := isLt✝ } < ↑{ val := i, isLt := isLt✝² }
h✝² : ¬↑(Fin.succ { val := k, isLt := isLt✝ }) < ↑(Fin.succ { val := j, isLt := isLt✝¹ })
h✝¹ : ¬↑{ val := k, isLt := isLt✝ } < ↑{ val := j, isLt := isLt✝¹ }
h✝ : ¬↑(Fin.succ { val := k, isLt := isLt✝ }) < ↑{ val := i, isLt := isLt✝² }
⊢ ↑(Fin.succ (Fin.succ { val := k, isLt := isLt✝ })) = ↑(Fin.succ (Fin.succ { val := k, isLt := isLt✝ }))
[PROOFSTEP]
simp at *
[GOAL]
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : Fin.castSucc i < j
hj : j = 0
⊢ False
[PROOFSTEP]
simp [hj, Fin.not_lt_zero] at H
[GOAL]
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : Fin.castSucc i < j
⊢ δ i ≫ δ j = δ (Fin.pred j (_ : j = 0 → False)) ≫ δ (Fin.castSucc i)
[PROOFSTEP]
rw [← δ_comp_δ]
[GOAL]
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : Fin.castSucc i < j
⊢ δ i ≫ δ j = δ i ≫ δ (Fin.succ (Fin.pred j (_ : j = 0 → False)))
[PROOFSTEP]
rw [Fin.succ_pred]
[GOAL]
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : Fin.castSucc i < j
⊢ i ≤ Fin.pred j (_ : j = 0 → False)
[PROOFSTEP]
simpa only [Fin.le_iff_val_le_val, ← Nat.lt_succ_iff, Nat.succ_eq_add_one, ← Fin.val_succ, j.succ_pred,
  Fin.lt_iff_val_lt_val] using H
[GOAL]
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ Fin.castSucc j
⊢ δ (Fin.castLT i (_ : ↑i < n + 2)) ≫ δ (Fin.succ j) = δ j ≫ δ i
[PROOFSTEP]
rw [δ_comp_δ]
[GOAL]
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ Fin.castSucc j
⊢ δ j ≫ δ (Fin.castSucc (Fin.castLT i (_ : ↑i < n + 2))) = δ j ≫ δ i
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ Fin.castSucc j
⊢ Fin.castLT i (_ : ↑i < n + 2) ≤ j
[PROOFSTEP]
exact H
[GOAL]
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : j = Fin.castSucc i
⊢ δ i ≫ δ j = δ i ≫ δ (Fin.succ i)
[PROOFSTEP]
subst H
[GOAL]
n : ℕ
i : Fin (n + 2)
⊢ δ i ≫ δ (Fin.castSucc i) = δ i ≫ δ (Fin.succ i)
[PROOFSTEP]
rw [δ_comp_δ_self]
[GOAL]
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ Fin.castSucc j
⊢ δ (Fin.castSucc i) ≫ σ (Fin.succ j) = σ j ≫ δ i
[PROOFSTEP]
rcases i with ⟨i, hi⟩
[GOAL]
case mk
n : ℕ
j : Fin (n + 1)
i : ℕ
hi : i < n + 2
H : { val := i, isLt := hi } ≤ Fin.castSucc j
⊢ δ (Fin.castSucc { val := i, isLt := hi }) ≫ σ (Fin.succ j) = σ j ≫ δ { val := i, isLt := hi }
[PROOFSTEP]
rcases j with ⟨j, hj⟩
[GOAL]
case mk.mk
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : { val := i, isLt := hi } ≤ Fin.castSucc { val := j, isLt := hj }
⊢ δ (Fin.castSucc { val := i, isLt := hi }) ≫ σ (Fin.succ { val := j, isLt := hj }) =
    σ { val := j, isLt := hj } ≫ δ { val := i, isLt := hi }
[PROOFSTEP]
ext ⟨k, hk⟩
[GOAL]
case mk.mk.a.h.h.mk.h
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : { val := i, isLt := hi } ≤ Fin.castSucc { val := j, isLt := hj }
k : ℕ
hk : k < len [n + 1] + 1
⊢ ↑(↑(Hom.toOrderHom (δ (Fin.castSucc { val := i, isLt := hi }) ≫ σ (Fin.succ { val := j, isLt := hj })))
        { val := k, isLt := hk }) =
    ↑(↑(Hom.toOrderHom (σ { val := j, isLt := hj } ≫ δ { val := i, isLt := hi })) { val := k, isLt := hk })
[PROOFSTEP]
simp at H hk
[GOAL]
case mk.mk.a.h.h.mk.h
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
⊢ ↑(↑(Hom.toOrderHom (δ (Fin.castSucc { val := i, isLt := hi }) ≫ σ (Fin.succ { val := j, isLt := hj })))
        { val := k, isLt := hk }) =
    ↑(↑(Hom.toOrderHom (σ { val := j, isLt := hj } ≫ δ { val := i, isLt := hi })) { val := k, isLt := hk })
[PROOFSTEP]
dsimp [σ, δ, Fin.predAbove, Fin.succAbove]
[GOAL]
case mk.mk.a.h.h.mk.h
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
⊢ ↑(if h :
          { val := j + 1, isLt := (_ : j + 1 < Nat.succ (n + 1 + 1)) } <
            if k < i then { val := k, isLt := (_ : k < Nat.succ (n + 1 + 1)) }
            else { val := k + 1, isLt := (_ : Nat.succ k < Nat.succ (n + 1 + 1)) } then
        Fin.pred
          (if k < i then { val := k, isLt := (_ : k < Nat.succ (n + 1 + 1)) }
          else { val := k + 1, isLt := (_ : Nat.succ k < Nat.succ (n + 1 + 1)) })
          (_ :
            (if k < i then { val := k, isLt := (_ : k < Nat.succ (n + 1 + 1)) }
              else { val := k + 1, isLt := (_ : Nat.succ k < Nat.succ (n + 1 + 1)) }) ≠
              0)
      else
        Fin.castLT
          (if k < i then { val := k, isLt := (_ : k < Nat.succ (n + 1 + 1)) }
          else { val := k + 1, isLt := (_ : Nat.succ k < Nat.succ (n + 1 + 1)) })
          (_ :
            ↑(if k < i then { val := k, isLt := (_ : k < Nat.succ (n + 1 + 1)) }
                else { val := k + 1, isLt := (_ : Nat.succ k < Nat.succ (n + 1 + 1)) }) <
              n + 1 + 1)) =
    ↑(if
          ↑(if h : { val := j, isLt := (_ : j < Nat.succ (n + 1)) } < { val := k, isLt := hk } then
                Fin.pred { val := k, isLt := hk } (_ : { val := k, isLt := hk } ≠ 0)
              else { val := k, isLt := (_ : ↑{ val := k, isLt := hk } < n + 1) }) <
            i then
        Fin.castSucc
          (if h : { val := j, isLt := (_ : j < Nat.succ (n + 1)) } < { val := k, isLt := hk } then
            Fin.pred { val := k, isLt := hk } (_ : { val := k, isLt := hk } ≠ 0)
          else { val := k, isLt := (_ : ↑{ val := k, isLt := hk } < n + 1) })
      else
        Fin.succ
          (if h : { val := j, isLt := (_ : j < Nat.succ (n + 1)) } < { val := k, isLt := hk } then
            Fin.pred { val := k, isLt := hk } (_ : { val := k, isLt := hk } ≠ 0)
          else { val := k, isLt := (_ : ↑{ val := k, isLt := hk } < n + 1) }))
[PROOFSTEP]
simp [Fin.lt_iff_val_lt_val, Fin.ite_val, Fin.dite_val]
[GOAL]
case mk.mk.a.h.h.mk.h
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
⊢ (if j + 1 < if k < i then k else k + 1 then (if k < i then k else k + 1) - 1 else if k < i then k else k + 1) =
    if (if j < k then k - 1 else k) < i then if j < k then k - 1 else k else (if j < k then k - 1 else k) + 1
[PROOFSTEP]
split_ifs
[GOAL]
case pos
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : k < i
h✝² : j + 1 < k
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k - 1 = k - 1
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : k < i
h✝² : j + 1 < k
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k - 1 = k - 1 + 1
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝² : k < i
h✝¹ : j + 1 < k
h✝ : ¬j < k
⊢ k - 1 = k
case pos
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : k < i
h✝² : ¬j + 1 < k
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k = k - 1
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : k < i
h✝² : ¬j + 1 < k
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k = k - 1 + 1
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝² : k < i
h✝¹ : ¬j + 1 < k
h✝ : ¬j < k
⊢ k = k
case pos
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : ¬k < i
h✝² : j + 1 < k + 1
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k + 1 - 1 = k - 1
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : ¬k < i
h✝² : j + 1 < k + 1
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k + 1 - 1 = k - 1 + 1
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝² : ¬k < i
h✝¹ : j + 1 < k + 1
h✝ : ¬j < k
⊢ k + 1 - 1 = k + 1
case pos
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : ¬k < i
h✝² : ¬j + 1 < k + 1
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k + 1 = k - 1
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : ¬k < i
h✝² : ¬j + 1 < k + 1
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k + 1 = k - 1 + 1
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝² : ¬k < i
h✝¹ : ¬j + 1 < k + 1
h✝ : ¬j < k
⊢ k + 1 = k + 1
[PROOFSTEP]
all_goals try simp <;> linarith
[GOAL]
case pos
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : k < i
h✝² : j + 1 < k
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k - 1 = k - 1
[PROOFSTEP]
try simp <;> linarith
[GOAL]
case pos
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : k < i
h✝² : j + 1 < k
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k - 1 = k - 1
[PROOFSTEP]
simp
[GOAL]
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : k < i
h✝² : j + 1 < k
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k - 1 = k - 1 + 1
[PROOFSTEP]
try simp <;> linarith
[GOAL]
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : k < i
h✝² : j + 1 < k
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k - 1 = k - 1 + 1
[PROOFSTEP]
simp
[GOAL]
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : k < i
h✝² : j + 1 < k
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝² : k < i
h✝¹ : j + 1 < k
h✝ : ¬j < k
⊢ k - 1 = k
[PROOFSTEP]
try simp <;> linarith
[GOAL]
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝² : k < i
h✝¹ : j + 1 < k
h✝ : ¬j < k
⊢ k - 1 = k
[PROOFSTEP]
simp
[GOAL]
case pos
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : k < i
h✝² : ¬j + 1 < k
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k = k - 1
[PROOFSTEP]
try simp <;> linarith
[GOAL]
case pos
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : k < i
h✝² : ¬j + 1 < k
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k = k - 1
[PROOFSTEP]
simp
[GOAL]
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : k < i
h✝² : ¬j + 1 < k
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k = k - 1 + 1
[PROOFSTEP]
try simp <;> linarith
[GOAL]
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : k < i
h✝² : ¬j + 1 < k
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k = k - 1 + 1
[PROOFSTEP]
simp
[GOAL]
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝² : k < i
h✝¹ : ¬j + 1 < k
h✝ : ¬j < k
⊢ k = k
[PROOFSTEP]
try simp <;> linarith
[GOAL]
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝² : k < i
h✝¹ : ¬j + 1 < k
h✝ : ¬j < k
⊢ k = k
[PROOFSTEP]
simp
[GOAL]
case pos
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : ¬k < i
h✝² : j + 1 < k + 1
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k + 1 - 1 = k - 1
[PROOFSTEP]
try simp <;> linarith
[GOAL]
case pos
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : ¬k < i
h✝² : j + 1 < k + 1
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k + 1 - 1 = k - 1
[PROOFSTEP]
simp
[GOAL]
case pos
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : ¬k < i
h✝² : j + 1 < k + 1
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k = k - 1
[PROOFSTEP]
linarith
[GOAL]
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : ¬k < i
h✝² : j + 1 < k + 1
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k + 1 - 1 = k - 1 + 1
[PROOFSTEP]
try simp <;> linarith
[GOAL]
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : ¬k < i
h✝² : j + 1 < k + 1
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k + 1 - 1 = k - 1 + 1
[PROOFSTEP]
simp
[GOAL]
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : ¬k < i
h✝² : j + 1 < k + 1
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k = k - 1 + 1
[PROOFSTEP]
linarith
[GOAL]
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝² : ¬k < i
h✝¹ : j + 1 < k + 1
h✝ : ¬j < k
⊢ k + 1 - 1 = k + 1
[PROOFSTEP]
try simp <;> linarith
[GOAL]
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝² : ¬k < i
h✝¹ : j + 1 < k + 1
h✝ : ¬j < k
⊢ k + 1 - 1 = k + 1
[PROOFSTEP]
simp
[GOAL]
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝² : ¬k < i
h✝¹ : j + 1 < k + 1
h✝ : ¬j < k
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case pos
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : ¬k < i
h✝² : ¬j + 1 < k + 1
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k + 1 = k - 1
[PROOFSTEP]
try simp <;> linarith
[GOAL]
case pos
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : ¬k < i
h✝² : ¬j + 1 < k + 1
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k + 1 = k - 1
[PROOFSTEP]
simp
[GOAL]
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : ¬k < i
h✝² : ¬j + 1 < k + 1
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k + 1 = k - 1 + 1
[PROOFSTEP]
try simp <;> linarith
[GOAL]
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : ¬k < i
h✝² : ¬j + 1 < k + 1
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k + 1 = k - 1 + 1
[PROOFSTEP]
simp
[GOAL]
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : ¬k < i
h✝² : ¬j + 1 < k + 1
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k = k - 1
[PROOFSTEP]
linarith
[GOAL]
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝² : ¬k < i
h✝¹ : ¬j + 1 < k + 1
h✝ : ¬j < k
⊢ k + 1 = k + 1
[PROOFSTEP]
try simp <;> linarith
[GOAL]
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝² : ¬k < i
h✝¹ : ¬j + 1 < k + 1
h✝ : ¬j < k
⊢ k + 1 = k + 1
[PROOFSTEP]
simp
[GOAL]
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝² : k < i
h✝¹ : j + 1 < k
h✝ : ¬j < k
⊢ k - 1 = k
case pos
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : k < i
h✝² : ¬j + 1 < k
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k = k - 1
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : k < i
h✝² : ¬j + 1 < k
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k = k - 1 + 1
case pos
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : ¬k < i
h✝² : j + 1 < k + 1
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k + 1 - 1 = k - 1
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : ¬k < i
h✝² : j + 1 < k + 1
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k + 1 - 1 = k - 1 + 1
case pos
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : ¬k < i
h✝² : ¬j + 1 < k + 1
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k + 1 = k - 1
[PROOFSTEP]
all_goals cases k <;> simp at * <;> linarith
[GOAL]
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝² : k < i
h✝¹ : j + 1 < k
h✝ : ¬j < k
⊢ k - 1 = k
[PROOFSTEP]
cases k
[GOAL]
case neg.zero
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : i ≤ j
hk : Nat.zero < n + 1 + 1
h✝² : Nat.zero < i
h✝¹ : j + 1 < Nat.zero
h✝ : ¬j < Nat.zero
⊢ Nat.zero - 1 = Nat.zero
[PROOFSTEP]
simp at *
[GOAL]
case neg.succ
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : i ≤ j
n✝ : ℕ
hk : Nat.succ n✝ < n + 1 + 1
h✝² : Nat.succ n✝ < i
h✝¹ : j + 1 < Nat.succ n✝
h✝ : ¬j < Nat.succ n✝
⊢ Nat.succ n✝ - 1 = Nat.succ n✝
[PROOFSTEP]
simp at *
[GOAL]
case neg.succ
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : i ≤ j
n✝ : ℕ
hk : Nat.succ n✝ < n + 1 + 1
h✝² : Nat.succ n✝ < i
h✝¹ : j + 1 < Nat.succ n✝
h✝ : Nat.succ n✝ ≤ j
⊢ n✝ = Nat.succ n✝
[PROOFSTEP]
linarith
[GOAL]
case pos
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : k < i
h✝² : ¬j + 1 < k
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k = k - 1
[PROOFSTEP]
cases k
[GOAL]
case pos.zero
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : i ≤ j
hk : Nat.zero < n + 1 + 1
h✝³ : Nat.zero < i
h✝² : ¬j + 1 < Nat.zero
h✝¹ : j < Nat.zero
h✝ : Nat.zero - 1 < i
⊢ Nat.zero = Nat.zero - 1
[PROOFSTEP]
simp at *
[GOAL]
case pos.succ
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : i ≤ j
n✝ : ℕ
hk : Nat.succ n✝ < n + 1 + 1
h✝³ : Nat.succ n✝ < i
h✝² : ¬j + 1 < Nat.succ n✝
h✝¹ : j < Nat.succ n✝
h✝ : Nat.succ n✝ - 1 < i
⊢ Nat.succ n✝ = Nat.succ n✝ - 1
[PROOFSTEP]
simp at *
[GOAL]
case pos.succ
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : i ≤ j
n✝ : ℕ
hk : Nat.succ n✝ < n + 1 + 1
h✝³ : Nat.succ n✝ < i
h✝² : j < Nat.succ n✝
h✝¹ : Nat.succ n✝ ≤ j + 1
h✝ : n✝ < i
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : k < i
h✝² : ¬j + 1 < k
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k = k - 1 + 1
[PROOFSTEP]
cases k
[GOAL]
case neg.zero
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : i ≤ j
hk : Nat.zero < n + 1 + 1
h✝³ : Nat.zero < i
h✝² : ¬j + 1 < Nat.zero
h✝¹ : j < Nat.zero
h✝ : ¬Nat.zero - 1 < i
⊢ Nat.zero = Nat.zero - 1 + 1
[PROOFSTEP]
simp at *
[GOAL]
case neg.succ
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : i ≤ j
n✝ : ℕ
hk : Nat.succ n✝ < n + 1 + 1
h✝³ : Nat.succ n✝ < i
h✝² : ¬j + 1 < Nat.succ n✝
h✝¹ : j < Nat.succ n✝
h✝ : ¬Nat.succ n✝ - 1 < i
⊢ Nat.succ n✝ = Nat.succ n✝ - 1 + 1
[PROOFSTEP]
simp at *
[GOAL]
case pos
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : ¬k < i
h✝² : j + 1 < k + 1
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k + 1 - 1 = k - 1
[PROOFSTEP]
cases k
[GOAL]
case pos.zero
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : i ≤ j
hk : Nat.zero < n + 1 + 1
h✝³ : ¬Nat.zero < i
h✝² : j + 1 < Nat.zero + 1
h✝¹ : j < Nat.zero
h✝ : Nat.zero - 1 < i
⊢ Nat.zero + 1 - 1 = Nat.zero - 1
[PROOFSTEP]
simp at *
[GOAL]
case pos.succ
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : i ≤ j
n✝ : ℕ
hk : Nat.succ n✝ < n + 1 + 1
h✝³ : ¬Nat.succ n✝ < i
h✝² : j + 1 < Nat.succ n✝ + 1
h✝¹ : j < Nat.succ n✝
h✝ : Nat.succ n✝ - 1 < i
⊢ Nat.succ n✝ + 1 - 1 = Nat.succ n✝ - 1
[PROOFSTEP]
simp at *
[GOAL]
case pos.succ
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : i ≤ j
n✝ : ℕ
hk : Nat.succ n✝ < n + 1 + 1
h✝³ : j < Nat.succ n✝
h✝² : i ≤ Nat.succ n✝
h✝¹ : j < n✝ + 1
h✝ : n✝ < i
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case neg
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : ¬k < i
h✝² : j + 1 < k + 1
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k + 1 - 1 = k - 1 + 1
[PROOFSTEP]
cases k
[GOAL]
case neg.zero
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : i ≤ j
hk : Nat.zero < n + 1 + 1
h✝³ : ¬Nat.zero < i
h✝² : j + 1 < Nat.zero + 1
h✝¹ : j < Nat.zero
h✝ : ¬Nat.zero - 1 < i
⊢ Nat.zero + 1 - 1 = Nat.zero - 1 + 1
[PROOFSTEP]
simp at *
[GOAL]
case neg.succ
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : i ≤ j
n✝ : ℕ
hk : Nat.succ n✝ < n + 1 + 1
h✝³ : ¬Nat.succ n✝ < i
h✝² : j + 1 < Nat.succ n✝ + 1
h✝¹ : j < Nat.succ n✝
h✝ : ¬Nat.succ n✝ - 1 < i
⊢ Nat.succ n✝ + 1 - 1 = Nat.succ n✝ - 1 + 1
[PROOFSTEP]
simp at *
[GOAL]
case pos
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
k : ℕ
hk : k < n + 1 + 1
H : i ≤ j
h✝³ : ¬k < i
h✝² : ¬j + 1 < k + 1
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k + 1 = k - 1
[PROOFSTEP]
cases k
[GOAL]
case pos.zero
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : i ≤ j
hk : Nat.zero < n + 1 + 1
h✝³ : ¬Nat.zero < i
h✝² : ¬j + 1 < Nat.zero + 1
h✝¹ : j < Nat.zero
h✝ : Nat.zero - 1 < i
⊢ Nat.zero + 1 = Nat.zero - 1
[PROOFSTEP]
simp at *
[GOAL]
case pos.succ
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : i ≤ j
n✝ : ℕ
hk : Nat.succ n✝ < n + 1 + 1
h✝³ : ¬Nat.succ n✝ < i
h✝² : ¬j + 1 < Nat.succ n✝ + 1
h✝¹ : j < Nat.succ n✝
h✝ : Nat.succ n✝ - 1 < i
⊢ Nat.succ n✝ + 1 = Nat.succ n✝ - 1
[PROOFSTEP]
simp at *
[GOAL]
case pos.succ
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : i ≤ j
n✝ : ℕ
hk : Nat.succ n✝ < n + 1 + 1
h✝³ : j < Nat.succ n✝
h✝² : i ≤ Nat.succ n✝
h✝¹ : n✝ + 1 ≤ j
h✝ : n✝ < i
⊢ Nat.succ n✝ + 1 = n✝
[PROOFSTEP]
linarith
[GOAL]
n : ℕ
i : Fin (n + 1)
⊢ δ (Fin.castSucc i) ≫ σ i = 𝟙 [n]
[PROOFSTEP]
rcases i with ⟨i, hi⟩
[GOAL]
case mk
n i : ℕ
hi : i < n + 1
⊢ δ (Fin.castSucc { val := i, isLt := hi }) ≫ σ { val := i, isLt := hi } = 𝟙 [n]
[PROOFSTEP]
ext ⟨j, hj⟩
[GOAL]
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 })
[PROOFSTEP]
simp at hj
[GOAL]
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 })
[PROOFSTEP]
dsimp [σ, δ, Fin.predAbove, Fin.succAbove]
[GOAL]
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 j < i 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 j < i then { val := j, isLt := (_ : j < Nat.succ (n + 1)) }
          else { val := j + 1, isLt := (_ : Nat.succ j < Nat.succ (n + 1)) })
          (_ :
            (if j < i 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 j < i then { val := j, isLt := (_ : j < Nat.succ (n + 1)) }
          else { val := j + 1, isLt := (_ : Nat.succ j < Nat.succ (n + 1)) })
          (_ :
            ↑(if j < i then { val := j, isLt := (_ : j < Nat.succ (n + 1)) }
                else { val := j + 1, isLt := (_ : Nat.succ j < Nat.succ (n + 1)) }) <
              n + 1)) =
    j
[PROOFSTEP]
simp [Fin.lt_iff_val_lt_val, Fin.ite_val, Fin.dite_val]
[GOAL]
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
[PROOFSTEP]
split_ifs
[GOAL]
case pos
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : j < i
h✝ : i < j
⊢ j - 1 = j
case neg
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : j < i
h✝ : ¬i < j
⊢ j = j
case pos
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : ¬j < i
h✝ : i < j + 1
⊢ j + 1 - 1 = j
case neg n i : ℕ hi : i < n + 1 j : ℕ hj : j < n + 1 h✝¹ : ¬j < i h✝ : ¬i < j + 1 ⊢ j + 1 = j
[PROOFSTEP]
any_goals simp
[GOAL]
case pos
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : j < i
h✝ : i < j
⊢ j - 1 = j
[PROOFSTEP]
simp
[GOAL]
case neg
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : j < i
h✝ : ¬i < j
⊢ j = j
[PROOFSTEP]
simp
[GOAL]
case pos
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : ¬j < i
h✝ : i < j + 1
⊢ j + 1 - 1 = j
[PROOFSTEP]
simp
[GOAL]
case neg
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : ¬j < i
h✝ : ¬i < j + 1
⊢ j + 1 = j
[PROOFSTEP]
simp
[GOAL]
case pos
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : j < i
h✝ : i < j
⊢ j - 1 = j
case neg n i : ℕ hi : i < n + 1 j : ℕ hj : j < n + 1 h✝¹ : ¬j < i h✝ : ¬i < j + 1 ⊢ False
[PROOFSTEP]
all_goals linarith
[GOAL]
case pos
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : j < i
h✝ : i < j
⊢ j - 1 = j
[PROOFSTEP]
linarith
[GOAL]
case neg
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
h✝¹ : ¬j < i
h✝ : ¬i < j + 1
⊢ False
[PROOFSTEP]
linarith
[GOAL]
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = Fin.castSucc i
⊢ δ j ≫ σ i = 𝟙 [n]
[PROOFSTEP]
subst H
[GOAL]
n : ℕ
i : Fin (n + 1)
⊢ δ (Fin.castSucc i) ≫ σ i = 𝟙 [n]
[PROOFSTEP]
rw [δ_comp_σ_self]
[GOAL]
n : ℕ
i : Fin (n + 1)
⊢ δ (Fin.succ i) ≫ σ i = 𝟙 [n]
[PROOFSTEP]
ext j
[GOAL]
case a.h.h.h
n : ℕ
i : Fin (n + 1)
j : Fin (len [n] + 1)
⊢ ↑(↑(Hom.toOrderHom (δ (Fin.succ i) ≫ σ i)) j) = ↑(↑(Hom.toOrderHom (𝟙 [n])) j)
[PROOFSTEP]
rcases i with ⟨i, _⟩
[GOAL]
case a.h.h.h.mk
n : ℕ
j : Fin (len [n] + 1)
i : ℕ
isLt✝ : i < n + 1
⊢ ↑(↑(Hom.toOrderHom (δ (Fin.succ { val := i, isLt := isLt✝ }) ≫ σ { val := i, isLt := isLt✝ })) j) =
    ↑(↑(Hom.toOrderHom (𝟙 [n])) j)
[PROOFSTEP]
rcases j with ⟨j, _⟩
[GOAL]
case a.h.h.h.mk.mk
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < len [n] + 1
⊢ ↑(↑(Hom.toOrderHom (δ (Fin.succ { val := i, isLt := isLt✝¹ }) ≫ σ { val := i, isLt := isLt✝¹ }))
        { val := j, isLt := isLt✝ }) =
    ↑(↑(Hom.toOrderHom (𝟙 [n])) { val := j, isLt := isLt✝ })
[PROOFSTEP]
dsimp [δ, σ, Fin.succAbove, Fin.predAbove]
[GOAL]
case a.h.h.h.mk.mk
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < len [n] + 1
⊢ ↑(if h :
          { val := i, isLt := (_ : i < Nat.succ (n + 1)) } <
            if j < i + 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 j < i + 1 then { val := j, isLt := (_ : j < Nat.succ (n + 1)) }
          else { val := j + 1, isLt := (_ : Nat.succ j < Nat.succ (n + 1)) })
          (_ :
            (if j < i + 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 j < i + 1 then { val := j, isLt := (_ : j < Nat.succ (n + 1)) }
          else { val := j + 1, isLt := (_ : Nat.succ j < Nat.succ (n + 1)) })
          (_ :
            ↑(if j < i + 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
[PROOFSTEP]
split_ifs
[GOAL]
case pos
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < len [n] + 1
h✝¹ : j < i + 1
h✝ : { val := i, isLt := (_ : i < Nat.succ (n + 1)) } < { val := j, isLt := (_ : j < Nat.succ (n + 1)) }
⊢ ↑(Fin.pred { val := j, isLt := (_ : j < Nat.succ (n + 1)) }
        (_ : { val := j, isLt := (_ : j < Nat.succ (n + 1)) } ≠ 0)) =
    j
[PROOFSTEP]
simp
[GOAL]
case neg
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < len [n] + 1
h✝¹ : j < i + 1
h✝ : ¬{ val := i, isLt := (_ : i < Nat.succ (n + 1)) } < { val := j, isLt := (_ : j < Nat.succ (n + 1)) }
⊢ ↑(Fin.castLT { val := j, isLt := (_ : j < Nat.succ (n + 1)) }
        (_ : ↑{ val := j, isLt := (_ : j < Nat.succ (n + 1)) } < n + 1)) =
    j
[PROOFSTEP]
simp
[GOAL]
case pos
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < len [n] + 1
h✝¹ : ¬j < i + 1
h✝ : { val := i, isLt := (_ : i < Nat.succ (n + 1)) } < { val := j + 1, isLt := (_ : Nat.succ j < Nat.succ (n + 1)) }
⊢ ↑(Fin.pred { val := j + 1, isLt := (_ : Nat.succ j < Nat.succ (n + 1)) }
        (_ : { val := j + 1, isLt := (_ : Nat.succ j < Nat.succ (n + 1)) } ≠ 0)) =
    j
[PROOFSTEP]
simp
[GOAL]
case neg
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < len [n] + 1
h✝¹ : ¬j < i + 1
h✝ : ¬{ val := i, isLt := (_ : i < Nat.succ (n + 1)) } < { val := j + 1, isLt := (_ : Nat.succ j < Nat.succ (n + 1)) }
⊢ ↑(Fin.castLT { val := j + 1, isLt := (_ : Nat.succ j < Nat.succ (n + 1)) }
        (_ : ↑{ val := j + 1, isLt := (_ : Nat.succ j < Nat.succ (n + 1)) } < n + 1)) =
    j
[PROOFSTEP]
simp
[GOAL]
case pos
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < len [n] + 1
h✝¹ : j < i + 1
h✝ : { val := i, isLt := (_ : i < Nat.succ (n + 1)) } < { val := j, isLt := (_ : j < Nat.succ (n + 1)) }
⊢ j - 1 = j
[PROOFSTEP]
simp at *
[GOAL]
case neg
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < len [n] + 1
h✝¹ : ¬j < i + 1
h✝ : ¬{ val := i, isLt := (_ : i < Nat.succ (n + 1)) } < { val := j + 1, isLt := (_ : Nat.succ j < Nat.succ (n + 1)) }
⊢ False
[PROOFSTEP]
simp at *
[GOAL]
case pos
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < len [n] + 1
h✝¹ : j < i + 1
h✝ : i < j
⊢ j - 1 = j
[PROOFSTEP]
linarith
[GOAL]
case neg
n i : ℕ
isLt✝¹ : i < n + 1
j : ℕ
isLt✝ : j < len [n] + 1
h✝¹ : i + 1 ≤ j
h✝ : j + 1 ≤ i
⊢ False
[PROOFSTEP]
linarith
[GOAL]
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = Fin.succ i
⊢ δ j ≫ σ i = 𝟙 [n]
[PROOFSTEP]
subst H
[GOAL]
n : ℕ
i : Fin (n + 1)
⊢ δ (Fin.succ i) ≫ σ i = 𝟙 [n]
[PROOFSTEP]
rw [δ_comp_σ_succ]
[GOAL]
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : Fin.castSucc j < i
⊢ δ (Fin.succ i) ≫ σ (Fin.castSucc j) = σ j ≫ δ i
[PROOFSTEP]
ext ⟨k, hk⟩
[GOAL]
case a.h.h.mk.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : Fin.castSucc j < i
k : ℕ
hk : k < len [n + 1] + 1
⊢ ↑(↑(Hom.toOrderHom (δ (Fin.succ i) ≫ σ (Fin.castSucc j))) { val := k, isLt := hk }) =
    ↑(↑(Hom.toOrderHom (σ j ≫ δ i)) { val := k, isLt := hk })
[PROOFSTEP]
rcases i with ⟨i, hi⟩
[GOAL]
case a.h.h.mk.h.mk
n : ℕ
j : Fin (n + 1)
k : ℕ
hk : k < len [n + 1] + 1
i : ℕ
hi : i < n + 2
H : Fin.castSucc j < { val := i, isLt := hi }
⊢ ↑(↑(Hom.toOrderHom (δ (Fin.succ { val := i, isLt := hi }) ≫ σ (Fin.castSucc j))) { val := k, isLt := hk }) =
    ↑(↑(Hom.toOrderHom (σ j ≫ δ { val := i, isLt := hi })) { val := k, isLt := hk })
[PROOFSTEP]
rcases j with ⟨j, hj⟩
[GOAL]
case a.h.h.mk.h.mk.mk
n k : ℕ
hk : k < len [n + 1] + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : Fin.castSucc { val := j, isLt := hj } < { val := i, isLt := hi }
⊢ ↑(↑(Hom.toOrderHom (δ (Fin.succ { val := i, isLt := hi }) ≫ σ (Fin.castSucc { val := j, isLt := hj })))
        { val := k, isLt := hk }) =
    ↑(↑(Hom.toOrderHom (σ { val := j, isLt := hj } ≫ δ { val := i, isLt := hi })) { val := k, isLt := hk })
[PROOFSTEP]
simp at H hk
[GOAL]
case a.h.h.mk.h.mk.mk
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
⊢ ↑(↑(Hom.toOrderHom (δ (Fin.succ { val := i, isLt := hi }) ≫ σ (Fin.castSucc { val := j, isLt := hj })))
        { val := k, isLt := hk }) =
    ↑(↑(Hom.toOrderHom (σ { val := j, isLt := hj } ≫ δ { val := i, isLt := hi })) { val := k, isLt := hk })
[PROOFSTEP]
dsimp [δ, σ, Fin.predAbove, Fin.succAbove]
[GOAL]
case a.h.h.mk.h.mk.mk
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
⊢ ↑(if h :
          { val := j, isLt := (_ : j < Nat.succ (n + 1 + 1)) } <
            if k < i + 1 then { val := k, isLt := (_ : k < Nat.succ (n + 1 + 1)) }
            else { val := k + 1, isLt := (_ : Nat.succ k < Nat.succ (n + 1 + 1)) } then
        Fin.pred
          (if k < i + 1 then { val := k, isLt := (_ : k < Nat.succ (n + 1 + 1)) }
          else { val := k + 1, isLt := (_ : Nat.succ k < Nat.succ (n + 1 + 1)) })
          (_ :
            (if k < i + 1 then { val := k, isLt := (_ : k < Nat.succ (n + 1 + 1)) }
              else { val := k + 1, isLt := (_ : Nat.succ k < Nat.succ (n + 1 + 1)) }) ≠
              0)
      else
        Fin.castLT
          (if k < i + 1 then { val := k, isLt := (_ : k < Nat.succ (n + 1 + 1)) }
          else { val := k + 1, isLt := (_ : Nat.succ k < Nat.succ (n + 1 + 1)) })
          (_ :
            ↑(if k < i + 1 then { val := k, isLt := (_ : k < Nat.succ (n + 1 + 1)) }
                else { val := k + 1, isLt := (_ : Nat.succ k < Nat.succ (n + 1 + 1)) }) <
              n + 1 + 1)) =
    ↑(if
          ↑(if h : { val := j, isLt := (_ : j < Nat.succ (n + 1)) } < { val := k, isLt := hk } then
                Fin.pred { val := k, isLt := hk } (_ : { val := k, isLt := hk } ≠ 0)
              else { val := k, isLt := (_ : ↑{ val := k, isLt := hk } < n + 1) }) <
            i then
        Fin.castSucc
          (if h : { val := j, isLt := (_ : j < Nat.succ (n + 1)) } < { val := k, isLt := hk } then
            Fin.pred { val := k, isLt := hk } (_ : { val := k, isLt := hk } ≠ 0)
          else { val := k, isLt := (_ : ↑{ val := k, isLt := hk } < n + 1) })
      else
        Fin.succ
          (if h : { val := j, isLt := (_ : j < Nat.succ (n + 1)) } < { val := k, isLt := hk } then
            Fin.pred { val := k, isLt := hk } (_ : { val := k, isLt := hk } ≠ 0)
          else { val := k, isLt := (_ : ↑{ val := k, isLt := hk } < n + 1) }))
[PROOFSTEP]
simp [Fin.lt_iff_val_lt_val, Fin.ite_val, Fin.dite_val]
[GOAL]
case a.h.h.mk.h.mk.mk
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
⊢ (if j < if k < i + 1 then k else k + 1 then (if k < i + 1 then k else k + 1) - 1
    else if k < i + 1 then k else k + 1) =
    if (if j < k then k - 1 else k) < i then if j < k then k - 1 else k else (if j < k then k - 1 else k) + 1
[PROOFSTEP]
split_ifs
[GOAL]
case pos
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝² : k < i + 1
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k - 1 = k - 1
case neg
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝² : k < i + 1
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k - 1 = k - 1 + 1
case pos
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝² : k < i + 1
h✝¹ : ¬j < k
h✝ : k < i
⊢ k = k
case neg
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝² : k < i + 1
h✝¹ : ¬j < k
h✝ : ¬k < i
⊢ k = k + 1
case pos
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : j < k + 1
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k + 1 - 1 = k - 1
case neg
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : j < k + 1
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k + 1 - 1 = k - 1 + 1
case pos
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : j < k + 1
h✝¹ : ¬j < k
h✝ : k < i
⊢ k + 1 - 1 = k
case neg
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : j < k + 1
h✝¹ : ¬j < k
h✝ : ¬k < i
⊢ k + 1 - 1 = k + 1
case pos
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : ¬j < k + 1
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k + 1 = k - 1
case neg
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : ¬j < k + 1
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k + 1 = k - 1 + 1
case pos
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : ¬j < k + 1
h✝¹ : ¬j < k
h✝ : k < i
⊢ k + 1 = k
case neg
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : ¬j < k + 1
h✝¹ : ¬j < k
h✝ : ¬k < i
⊢ k + 1 = k + 1
[PROOFSTEP]
all_goals try simp <;> linarith
[GOAL]
case pos
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝² : k < i + 1
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k - 1 = k - 1
[PROOFSTEP]
try simp <;> linarith
[GOAL]
case pos
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝² : k < i + 1
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k - 1 = k - 1
[PROOFSTEP]
simp
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝² : k < i + 1
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k - 1 = k - 1 + 1
[PROOFSTEP]
try simp <;> linarith
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝² : k < i + 1
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k - 1 = k - 1 + 1
[PROOFSTEP]
simp
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝² : k < i + 1
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case pos
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝² : k < i + 1
h✝¹ : ¬j < k
h✝ : k < i
⊢ k = k
[PROOFSTEP]
try simp <;> linarith
[GOAL]
case pos
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝² : k < i + 1
h✝¹ : ¬j < k
h✝ : k < i
⊢ k = k
[PROOFSTEP]
simp
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝² : k < i + 1
h✝¹ : ¬j < k
h✝ : ¬k < i
⊢ k = k + 1
[PROOFSTEP]
try simp <;> linarith
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝² : k < i + 1
h✝¹ : ¬j < k
h✝ : ¬k < i
⊢ k = k + 1
[PROOFSTEP]
simp
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝² : k < i + 1
h✝¹ : ¬j < k
h✝ : ¬k < i
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case pos
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : j < k + 1
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k + 1 - 1 = k - 1
[PROOFSTEP]
try simp <;> linarith
[GOAL]
case pos
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : j < k + 1
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k + 1 - 1 = k - 1
[PROOFSTEP]
simp
[GOAL]
case pos
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : j < k + 1
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k = k - 1
[PROOFSTEP]
linarith
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : j < k + 1
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k + 1 - 1 = k - 1 + 1
[PROOFSTEP]
try simp <;> linarith
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : j < k + 1
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k + 1 - 1 = k - 1 + 1
[PROOFSTEP]
simp
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : j < k + 1
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k = k - 1 + 1
[PROOFSTEP]
linarith
[GOAL]
case pos
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : j < k + 1
h✝¹ : ¬j < k
h✝ : k < i
⊢ k + 1 - 1 = k
[PROOFSTEP]
try simp <;> linarith
[GOAL]
case pos
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : j < k + 1
h✝¹ : ¬j < k
h✝ : k < i
⊢ k + 1 - 1 = k
[PROOFSTEP]
simp
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : j < k + 1
h✝¹ : ¬j < k
h✝ : ¬k < i
⊢ k + 1 - 1 = k + 1
[PROOFSTEP]
try simp <;> linarith
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : j < k + 1
h✝¹ : ¬j < k
h✝ : ¬k < i
⊢ k + 1 - 1 = k + 1
[PROOFSTEP]
simp
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : j < k + 1
h✝¹ : ¬j < k
h✝ : ¬k < i
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case pos
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : ¬j < k + 1
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k + 1 = k - 1
[PROOFSTEP]
try simp <;> linarith
[GOAL]
case pos
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : ¬j < k + 1
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k + 1 = k - 1
[PROOFSTEP]
simp
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : ¬j < k + 1
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k + 1 = k - 1 + 1
[PROOFSTEP]
try simp <;> linarith
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : ¬j < k + 1
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k + 1 = k - 1 + 1
[PROOFSTEP]
simp
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : ¬j < k + 1
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k = k - 1
[PROOFSTEP]
linarith
[GOAL]
case pos
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : ¬j < k + 1
h✝¹ : ¬j < k
h✝ : k < i
⊢ k + 1 = k
[PROOFSTEP]
try simp <;> linarith
[GOAL]
case pos
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : ¬j < k + 1
h✝¹ : ¬j < k
h✝ : k < i
⊢ k + 1 = k
[PROOFSTEP]
simp
[GOAL]
case pos
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : ¬j < k + 1
h✝¹ : ¬j < k
h✝ : k < i
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : ¬j < k + 1
h✝¹ : ¬j < k
h✝ : ¬k < i
⊢ k + 1 = k + 1
[PROOFSTEP]
try simp <;> linarith
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : ¬j < k + 1
h✝¹ : ¬j < k
h✝ : ¬k < i
⊢ k + 1 = k + 1
[PROOFSTEP]
simp
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝² : k < i + 1
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k - 1 = k - 1 + 1
case pos
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : j < k + 1
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k + 1 - 1 = k - 1
case neg
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : j < k + 1
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k + 1 - 1 = k - 1 + 1
case pos
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : ¬j < k + 1
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k + 1 = k - 1
[PROOFSTEP]
all_goals cases k <;> simp at * <;> linarith
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝² : k < i + 1
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k - 1 = k - 1 + 1
[PROOFSTEP]
cases k
[GOAL]
case neg.zero
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
hk : Nat.zero < n + 1 + 1
h✝² : Nat.zero < i + 1
h✝¹ : j < Nat.zero
h✝ : ¬Nat.zero - 1 < i
⊢ Nat.zero - 1 = Nat.zero - 1 + 1
[PROOFSTEP]
simp at *
[GOAL]
case neg.succ
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
n✝ : ℕ
hk : Nat.succ n✝ < n + 1 + 1
h✝² : Nat.succ n✝ < i + 1
h✝¹ : j < Nat.succ n✝
h✝ : ¬Nat.succ n✝ - 1 < i
⊢ Nat.succ n✝ - 1 = Nat.succ n✝ - 1 + 1
[PROOFSTEP]
simp at *
[GOAL]
case neg.succ
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
n✝ : ℕ
hk : Nat.succ n✝ < n + 1 + 1
h✝² : Nat.succ n✝ < i + 1
h✝¹ : j < Nat.succ n✝
h✝ : i ≤ n✝
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case pos
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : j < k + 1
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k + 1 - 1 = k - 1
[PROOFSTEP]
cases k
[GOAL]
case pos.zero
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
hk : Nat.zero < n + 1 + 1
h✝³ : ¬Nat.zero < i + 1
h✝² : j < Nat.zero + 1
h✝¹ : j < Nat.zero
h✝ : Nat.zero - 1 < i
⊢ Nat.zero + 1 - 1 = Nat.zero - 1
[PROOFSTEP]
simp at *
[GOAL]
case pos.succ
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
n✝ : ℕ
hk : Nat.succ n✝ < n + 1 + 1
h✝³ : ¬Nat.succ n✝ < i + 1
h✝² : j < Nat.succ n✝ + 1
h✝¹ : j < Nat.succ n✝
h✝ : Nat.succ n✝ - 1 < i
⊢ Nat.succ n✝ + 1 - 1 = Nat.succ n✝ - 1
[PROOFSTEP]
simp at *
[GOAL]
case pos.succ
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
n✝ : ℕ
hk : Nat.succ n✝ < n + 1 + 1
h✝³ : j < Nat.succ n✝ + 1
h✝² : j < Nat.succ n✝
h✝¹ : i + 1 ≤ Nat.succ n✝
h✝ : n✝ < i
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : j < k + 1
h✝¹ : j < k
h✝ : ¬k - 1 < i
⊢ k + 1 - 1 = k - 1 + 1
[PROOFSTEP]
cases k
[GOAL]
case neg.zero
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
hk : Nat.zero < n + 1 + 1
h✝³ : ¬Nat.zero < i + 1
h✝² : j < Nat.zero + 1
h✝¹ : j < Nat.zero
h✝ : ¬Nat.zero - 1 < i
⊢ Nat.zero + 1 - 1 = Nat.zero - 1 + 1
[PROOFSTEP]
simp at *
[GOAL]
case neg.succ
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
n✝ : ℕ
hk : Nat.succ n✝ < n + 1 + 1
h✝³ : ¬Nat.succ n✝ < i + 1
h✝² : j < Nat.succ n✝ + 1
h✝¹ : j < Nat.succ n✝
h✝ : ¬Nat.succ n✝ - 1 < i
⊢ Nat.succ n✝ + 1 - 1 = Nat.succ n✝ - 1 + 1
[PROOFSTEP]
simp at *
[GOAL]
case pos
n k : ℕ
hk : k < n + 1 + 1
i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
h✝³ : ¬k < i + 1
h✝² : ¬j < k + 1
h✝¹ : j < k
h✝ : k - 1 < i
⊢ k + 1 = k - 1
[PROOFSTEP]
cases k
[GOAL]
case pos.zero
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
hk : Nat.zero < n + 1 + 1
h✝³ : ¬Nat.zero < i + 1
h✝² : ¬j < Nat.zero + 1
h✝¹ : j < Nat.zero
h✝ : Nat.zero - 1 < i
⊢ Nat.zero + 1 = Nat.zero - 1
[PROOFSTEP]
simp at *
[GOAL]
case pos.succ
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
n✝ : ℕ
hk : Nat.succ n✝ < n + 1 + 1
h✝³ : ¬Nat.succ n✝ < i + 1
h✝² : ¬j < Nat.succ n✝ + 1
h✝¹ : j < Nat.succ n✝
h✝ : Nat.succ n✝ - 1 < i
⊢ Nat.succ n✝ + 1 = Nat.succ n✝ - 1
[PROOFSTEP]
simp at *
[GOAL]
case pos.succ
n i : ℕ
hi : i < n + 2
j : ℕ
hj : j < n + 1
H : j < i
n✝ : ℕ
hk : Nat.succ n✝ < n + 1 + 1
h✝³ : j < Nat.succ n✝
h✝² : i + 1 ≤ Nat.succ n✝
h✝¹ : Nat.succ n✝ + 1 ≤ j
h✝ : n✝ < i
⊢ Nat.succ n✝ + 1 = n✝
[PROOFSTEP]
linarith
[GOAL]
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : Fin.succ j < i
hi : i = 0
⊢ False
[PROOFSTEP]
simp only [Fin.not_lt_zero, hi] at H
[GOAL]
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : Fin.succ j < i
⊢ δ i ≫ σ j = σ (Fin.castLT j (_ : ↑j < n + 1)) ≫ δ (Fin.pred i (_ : i = 0 → False))
[PROOFSTEP]
rw [← δ_comp_σ_of_gt]
[GOAL]
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : Fin.succ j < i
⊢ δ i ≫ σ j = δ (Fin.succ (Fin.pred i (_ : i = 0 → False))) ≫ σ (Fin.castSucc (Fin.castLT j (_ : ↑j < n + 1)))
[PROOFSTEP]
simp
[GOAL]
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : Fin.succ j < i
⊢ Fin.castSucc (Fin.castLT j (_ : ↑j < n + 1)) < Fin.pred i (_ : i = 0 → False)
[PROOFSTEP]
rw [Fin.castSucc_castLT, ← Fin.succ_lt_succ_iff, Fin.succ_pred]
[GOAL]
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : Fin.succ j < i
⊢ Fin.succ j < i
[PROOFSTEP]
exact H
[GOAL]
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ σ (Fin.castSucc i) ≫ σ j = σ (Fin.succ j) ≫ σ i
[PROOFSTEP]
ext ⟨k, hk⟩
[GOAL]
case a.h.h.mk.h
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : ℕ
hk : k < len [n + 1 + 1] + 1
⊢ ↑(↑(Hom.toOrderHom (σ (Fin.castSucc i) ≫ σ j)) { val := k, isLt := hk }) =
    ↑(↑(Hom.toOrderHom (σ (Fin.succ j) ≫ σ i)) { val := k, isLt := hk })
[PROOFSTEP]
rcases i with ⟨i, hi⟩
[GOAL]
case a.h.h.mk.h.mk
n : ℕ
j : Fin (n + 1)
k : ℕ
hk : k < len [n + 1 + 1] + 1
i : ℕ
hi : i < n + 1
H : { val := i, isLt := hi } ≤ j
⊢ ↑(↑(Hom.toOrderHom (σ (Fin.castSucc { val := i, isLt := hi }) ≫ σ j)) { val := k, isLt := hk }) =
    ↑(↑(Hom.toOrderHom (σ (Fin.succ j) ≫ σ { val := i, isLt := hi })) { val := k, isLt := hk })
[PROOFSTEP]
rcases j with ⟨j, hj⟩
[GOAL]
case a.h.h.mk.h.mk.mk
n k : ℕ
hk : k < len [n + 1 + 1] + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : { val := i, isLt := hi } ≤ { val := j, isLt := hj }
⊢ ↑(↑(Hom.toOrderHom (σ (Fin.castSucc { val := i, isLt := hi }) ≫ σ { val := j, isLt := hj }))
        { val := k, isLt := hk }) =
    ↑(↑(Hom.toOrderHom (σ (Fin.succ { val := j, isLt := hj }) ≫ σ { val := i, isLt := hi })) { val := k, isLt := hk })
[PROOFSTEP]
simp at H hk
[GOAL]
case a.h.h.mk.h.mk.mk
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
⊢ ↑(↑(Hom.toOrderHom (σ (Fin.castSucc { val := i, isLt := hi }) ≫ σ { val := j, isLt := hj }))
        { val := k, isLt := hk }) =
    ↑(↑(Hom.toOrderHom (σ (Fin.succ { val := j, isLt := hj }) ≫ σ { val := i, isLt := hi })) { val := k, isLt := hk })
[PROOFSTEP]
dsimp [σ, Fin.predAbove]
[GOAL]
case a.h.h.mk.h.mk.mk
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
⊢ ↑(if h :
          { val := j, isLt := (_ : j < Nat.succ (n + 1)) } <
            if h : { val := i, isLt := (_ : i < Nat.succ (n + 1 + 1)) } < { val := k, isLt := hk } then
              Fin.pred { val := k, isLt := hk } (_ : { val := k, isLt := hk } ≠ 0)
            else { val := k, isLt := (_ : ↑{ val := k, isLt := hk } < n + 1 + 1) } then
        Fin.pred
          (if h : { val := i, isLt := (_ : i < Nat.succ (n + 1 + 1)) } < { val := k, isLt := hk } then
            Fin.pred { val := k, isLt := hk } (_ : { val := k, isLt := hk } ≠ 0)
          else { val := k, isLt := (_ : ↑{ val := k, isLt := hk } < n + 1 + 1) })
          (_ :
            (if h : { val := i, isLt := (_ : i < Nat.succ (n + 1 + 1)) } < { val := k, isLt := hk } then
                Fin.pred { val := k, isLt := hk } (_ : { val := k, isLt := hk } ≠ 0)
              else { val := k, isLt := (_ : ↑{ val := k, isLt := hk } < n + 1 + 1) }) ≠
              0)
      else
        Fin.castLT
          (if h : { val := i, isLt := (_ : i < Nat.succ (n + 1 + 1)) } < { val := k, isLt := hk } then
            Fin.pred { val := k, isLt := hk } (_ : { val := k, isLt := hk } ≠ 0)
          else { val := k, isLt := (_ : ↑{ val := k, isLt := hk } < n + 1 + 1) })
          (_ :
            ↑(if h : { val := i, isLt := (_ : i < Nat.succ (n + 1 + 1)) } < { val := k, isLt := hk } then
                  Fin.pred { val := k, isLt := hk } (_ : { val := k, isLt := hk } ≠ 0)
                else { val := k, isLt := (_ : ↑{ val := k, isLt := hk } < n + 1 + 1) }) <
              n + 1)) =
    ↑(if h :
          { val := i, isLt := (_ : i < Nat.succ (n + 1)) } <
            if h : { val := j + 1, isLt := (_ : j + 1 < Nat.succ (n + 1 + 1)) } < { val := k, isLt := hk } then
              Fin.pred { val := k, isLt := hk } (_ : { val := k, isLt := hk } ≠ 0)
            else { val := k, isLt := (_ : ↑{ val := k, isLt := hk } < n + 1 + 1) } then
        Fin.pred
          (if h : { val := j + 1, isLt := (_ : j + 1 < Nat.succ (n + 1 + 1)) } < { val := k, isLt := hk } then
            Fin.pred { val := k, isLt := hk } (_ : { val := k, isLt := hk } ≠ 0)
          else { val := k, isLt := (_ : ↑{ val := k, isLt := hk } < n + 1 + 1) })
          (_ :
            (if h : { val := j + 1, isLt := (_ : j + 1 < Nat.succ (n + 1 + 1)) } < { val := k, isLt := hk } then
                Fin.pred { val := k, isLt := hk } (_ : { val := k, isLt := hk } ≠ 0)
              else { val := k, isLt := (_ : ↑{ val := k, isLt := hk } < n + 1 + 1) }) ≠
              0)
      else
        Fin.castLT
          (if h : { val := j + 1, isLt := (_ : j + 1 < Nat.succ (n + 1 + 1)) } < { val := k, isLt := hk } then
            Fin.pred { val := k, isLt := hk } (_ : { val := k, isLt := hk } ≠ 0)
          else { val := k, isLt := (_ : ↑{ val := k, isLt := hk } < n + 1 + 1) })
          (_ :
            ↑(if h : { val := j + 1, isLt := (_ : j + 1 < Nat.succ (n + 1 + 1)) } < { val := k, isLt := hk } then
                  Fin.pred { val := k, isLt := hk } (_ : { val := k, isLt := hk } ≠ 0)
                else { val := k, isLt := (_ : ↑{ val := k, isLt := hk } < n + 1 + 1) }) <
              n + 1))
[PROOFSTEP]
simp [Fin.lt_iff_val_lt_val, Fin.ite_val]
[GOAL]
case a.h.h.mk.h.mk.mk
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
⊢ (if j < if i < k then k - 1 else k then (if i < k then k - 1 else k) - 1 else if i < k then k - 1 else k) =
    if i < if j + 1 < k then k - 1 else k then (if j + 1 < k then k - 1 else k) - 1 else if j + 1 < k then k - 1 else k
[PROOFSTEP]
split_ifs
[GOAL]
case pos
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝³ : i < k
h✝² : j < k - 1
h✝¹ : j + 1 < k
h✝ : i < k - 1
⊢ k - 1 - 1 = k - 1 - 1
case neg
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝³ : i < k
h✝² : j < k - 1
h✝¹ : j + 1 < k
h✝ : ¬i < k - 1
⊢ k - 1 - 1 = k - 1
case neg
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝² : i < k
h✝¹ : j < k - 1
h✝ : ¬j + 1 < k
⊢ k - 1 - 1 = k - 1
case pos
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝³ : i < k
h✝² : ¬j < k - 1
h✝¹ : j + 1 < k
h✝ : i < k - 1
⊢ k - 1 = k - 1 - 1
case neg
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝³ : i < k
h✝² : ¬j < k - 1
h✝¹ : j + 1 < k
h✝ : ¬i < k - 1
⊢ k - 1 = k - 1
case neg
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝² : i < k
h✝¹ : ¬j < k - 1
h✝ : ¬j + 1 < k
⊢ k - 1 = k - 1
case pos
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝³ : ¬i < k
h✝² : j < k
h✝¹ : j + 1 < k
h✝ : i < k - 1
⊢ k - 1 = k - 1 - 1
case neg
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝³ : ¬i < k
h✝² : j < k
h✝¹ : j + 1 < k
h✝ : ¬i < k - 1
⊢ k - 1 = k - 1
case neg
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝² : ¬i < k
h✝¹ : j < k
h✝ : ¬j + 1 < k
⊢ k - 1 = k
case pos
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝³ : ¬i < k
h✝² : ¬j < k
h✝¹ : j + 1 < k
h✝ : i < k - 1
⊢ k = k - 1 - 1
case neg
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝³ : ¬i < k
h✝² : ¬j < k
h✝¹ : j + 1 < k
h✝ : ¬i < k - 1
⊢ k = k - 1
case neg
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝² : ¬i < k
h✝¹ : ¬j < k
h✝ : ¬j + 1 < k
⊢ k = k
[PROOFSTEP]
all_goals try linarith
[GOAL]
case pos
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝³ : i < k
h✝² : j < k - 1
h✝¹ : j + 1 < k
h✝ : i < k - 1
⊢ k - 1 - 1 = k - 1 - 1
[PROOFSTEP]
try linarith
[GOAL]
case pos
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝³ : i < k
h✝² : j < k - 1
h✝¹ : j + 1 < k
h✝ : i < k - 1
⊢ k - 1 - 1 = k - 1 - 1
[PROOFSTEP]
linarith
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝³ : i < k
h✝² : j < k - 1
h✝¹ : j + 1 < k
h✝ : ¬i < k - 1
⊢ k - 1 - 1 = k - 1
[PROOFSTEP]
try linarith
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝³ : i < k
h✝² : j < k - 1
h✝¹ : j + 1 < k
h✝ : ¬i < k - 1
⊢ k - 1 - 1 = k - 1
[PROOFSTEP]
linarith
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝² : i < k
h✝¹ : j < k - 1
h✝ : ¬j + 1 < k
⊢ k - 1 - 1 = k - 1
[PROOFSTEP]
try linarith
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝² : i < k
h✝¹ : j < k - 1
h✝ : ¬j + 1 < k
⊢ k - 1 - 1 = k - 1
[PROOFSTEP]
linarith
[GOAL]
case pos
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝³ : i < k
h✝² : ¬j < k - 1
h✝¹ : j + 1 < k
h✝ : i < k - 1
⊢ k - 1 = k - 1 - 1
[PROOFSTEP]
try linarith
[GOAL]
case pos
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝³ : i < k
h✝² : ¬j < k - 1
h✝¹ : j + 1 < k
h✝ : i < k - 1
⊢ k - 1 = k - 1 - 1
[PROOFSTEP]
linarith
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝³ : i < k
h✝² : ¬j < k - 1
h✝¹ : j + 1 < k
h✝ : ¬i < k - 1
⊢ k - 1 = k - 1
[PROOFSTEP]
try linarith
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝³ : i < k
h✝² : ¬j < k - 1
h✝¹ : j + 1 < k
h✝ : ¬i < k - 1
⊢ k - 1 = k - 1
[PROOFSTEP]
linarith
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝² : i < k
h✝¹ : ¬j < k - 1
h✝ : ¬j + 1 < k
⊢ k - 1 = k - 1
[PROOFSTEP]
try linarith
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝² : i < k
h✝¹ : ¬j < k - 1
h✝ : ¬j + 1 < k
⊢ k - 1 = k - 1
[PROOFSTEP]
linarith
[GOAL]
case pos
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝³ : ¬i < k
h✝² : j < k
h✝¹ : j + 1 < k
h✝ : i < k - 1
⊢ k - 1 = k - 1 - 1
[PROOFSTEP]
try linarith
[GOAL]
case pos
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝³ : ¬i < k
h✝² : j < k
h✝¹ : j + 1 < k
h✝ : i < k - 1
⊢ k - 1 = k - 1 - 1
[PROOFSTEP]
linarith
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝³ : ¬i < k
h✝² : j < k
h✝¹ : j + 1 < k
h✝ : ¬i < k - 1
⊢ k - 1 = k - 1
[PROOFSTEP]
try linarith
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝³ : ¬i < k
h✝² : j < k
h✝¹ : j + 1 < k
h✝ : ¬i < k - 1
⊢ k - 1 = k - 1
[PROOFSTEP]
linarith
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝² : ¬i < k
h✝¹ : j < k
h✝ : ¬j + 1 < k
⊢ k - 1 = k
[PROOFSTEP]
try linarith
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝² : ¬i < k
h✝¹ : j < k
h✝ : ¬j + 1 < k
⊢ k - 1 = k
[PROOFSTEP]
linarith
[GOAL]
case pos
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝³ : ¬i < k
h✝² : ¬j < k
h✝¹ : j + 1 < k
h✝ : i < k - 1
⊢ k = k - 1 - 1
[PROOFSTEP]
try linarith
[GOAL]
case pos
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝³ : ¬i < k
h✝² : ¬j < k
h✝¹ : j + 1 < k
h✝ : i < k - 1
⊢ k = k - 1 - 1
[PROOFSTEP]
linarith
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝³ : ¬i < k
h✝² : ¬j < k
h✝¹ : j + 1 < k
h✝ : ¬i < k - 1
⊢ k = k - 1
[PROOFSTEP]
try linarith
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝³ : ¬i < k
h✝² : ¬j < k
h✝¹ : j + 1 < k
h✝ : ¬i < k - 1
⊢ k = k - 1
[PROOFSTEP]
linarith
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝² : ¬i < k
h✝¹ : ¬j < k
h✝ : ¬j + 1 < k
⊢ k = k
[PROOFSTEP]
try linarith
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝² : ¬i < k
h✝¹ : ¬j < k
h✝ : ¬j + 1 < k
⊢ k = k
[PROOFSTEP]
linarith
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝² : i < k
h✝¹ : j < k - 1
h✝ : ¬j + 1 < k
⊢ k - 1 - 1 = k - 1
case pos
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝³ : i < k
h✝² : ¬j < k - 1
h✝¹ : j + 1 < k
h✝ : i < k - 1
⊢ k - 1 = k - 1 - 1
[PROOFSTEP]
all_goals cases k <;> simp at *; linarith
[GOAL]
case neg
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝² : i < k
h✝¹ : j < k - 1
h✝ : ¬j + 1 < k
⊢ k - 1 - 1 = k - 1
[PROOFSTEP]
cases k
[GOAL]
case neg.zero
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
hk : Nat.zero < n + 1 + 1 + 1
h✝² : i < Nat.zero
h✝¹ : j < Nat.zero - 1
h✝ : ¬j + 1 < Nat.zero
⊢ Nat.zero - 1 - 1 = Nat.zero - 1
[PROOFSTEP]
simp at *
[GOAL]
case neg.succ
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
n✝ : ℕ
hk : Nat.succ n✝ < n + 1 + 1 + 1
h✝² : i < Nat.succ n✝
h✝¹ : j < Nat.succ n✝ - 1
h✝ : ¬j + 1 < Nat.succ n✝
⊢ Nat.succ n✝ - 1 - 1 = Nat.succ n✝ - 1
[PROOFSTEP]
simp at *
[GOAL]
case neg.succ
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
n✝ : ℕ
hk : Nat.succ n✝ < n + 1 + 1 + 1
h✝² : i < Nat.succ n✝
h✝¹ : j < n✝
h✝ : Nat.succ n✝ ≤ j + 1
⊢ n✝ - 1 = n✝
[PROOFSTEP]
linarith
[GOAL]
case pos
n k : ℕ
hk : k < n + 1 + 1 + 1
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
h✝³ : i < k
h✝² : ¬j < k - 1
h✝¹ : j + 1 < k
h✝ : i < k - 1
⊢ k - 1 = k - 1 - 1
[PROOFSTEP]
cases k
[GOAL]
case pos.zero
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
hk : Nat.zero < n + 1 + 1 + 1
h✝³ : i < Nat.zero
h✝² : ¬j < Nat.zero - 1
h✝¹ : j + 1 < Nat.zero
h✝ : i < Nat.zero - 1
⊢ Nat.zero - 1 = Nat.zero - 1 - 1
[PROOFSTEP]
simp at *
[GOAL]
case pos.succ
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
n✝ : ℕ
hk : Nat.succ n✝ < n + 1 + 1 + 1
h✝³ : i < Nat.succ n✝
h✝² : ¬j < Nat.succ n✝ - 1
h✝¹ : j + 1 < Nat.succ n✝
h✝ : i < Nat.succ n✝ - 1
⊢ Nat.succ n✝ - 1 = Nat.succ n✝ - 1 - 1
[PROOFSTEP]
simp at *
[GOAL]
case pos.succ
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
H : i ≤ j
n✝ : ℕ
hk : Nat.succ n✝ < n + 1 + 1 + 1
h✝³ : i < Nat.succ n✝
h✝² : j + 1 < Nat.succ n✝
h✝¹ : n✝ ≤ j
h✝ : i < n✝
⊢ n✝ = n✝ - 1
[PROOFSTEP]
linarith
[GOAL]
X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
⊢ X = Y
[PROOFSTEP]
suffices Fintype.card (Fin (X.len + 1)) = Fintype.card (Fin (Y.len + 1))
  by
  ext
  simpa
[GOAL]
X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
this : Fintype.card (Fin (len X + 1)) = Fintype.card (Fin (len Y + 1))
⊢ X = Y
[PROOFSTEP]
ext
[GOAL]
case a
X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
this : Fintype.card (Fin (len X + 1)) = Fintype.card (Fin (len Y + 1))
⊢ len X = len Y
[PROOFSTEP]
simpa
[GOAL]
X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
⊢ Fintype.card (Fin (len X + 1)) = Fintype.card (Fin (len Y + 1))
[PROOFSTEP]
apply Fintype.card_congr
[GOAL]
case f
X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
⊢ Fin (len X + 1) ≃ Fin (len Y + 1)
[PROOFSTEP]
exact Equiv.ulift.symm.trans (((skeletalFunctor.{0} ⋙ forget NonemptyFinLinOrdCat).mapIso I).toEquiv.trans Equiv.ulift)
[GOAL]
x✝¹ x✝ : SimplexCategory
f g : x✝¹ ⟶ x✝
h : skeletalFunctor.map f = skeletalFunctor.map g
⊢ f = g
[PROOFSTEP]
ext x : 3
[GOAL]
case a.h.h
x✝¹ x✝ : SimplexCategory
f g : x✝¹ ⟶ x✝
h : skeletalFunctor.map f = skeletalFunctor.map g
x : Fin (len x✝¹ + 1)
⊢ ↑(Hom.toOrderHom f) x = ↑(Hom.toOrderHom g) x
[PROOFSTEP]
apply ULift.up_injective.{v}
[GOAL]
case a.h.h.a
x✝¹ x✝ : SimplexCategory
f g : x✝¹ ⟶ x✝
h : skeletalFunctor.map f = skeletalFunctor.map g
x : Fin (len x✝¹ + 1)
⊢ { down := ↑(Hom.toOrderHom f) x } = { down := ↑(Hom.toOrderHom g) x }
[PROOFSTEP]
change (skeletalFunctor.{v}.map f) ⟨x⟩ = (skeletalFunctor.map g) ⟨x⟩
[GOAL]
case a.h.h.a
x✝¹ x✝ : SimplexCategory
f g : x✝¹ ⟶ x✝
h : skeletalFunctor.map f = skeletalFunctor.map g
x : Fin (len x✝¹ + 1)
⊢ ↑(skeletalFunctor.map f) { down := x } = ↑(skeletalFunctor.map g) { down := x }
[PROOFSTEP]
rw [h]
[GOAL]
X : NonemptyFinLinOrdCat
⊢ skeletalFunctor.obj [Fintype.card ↑X - 1] ≅ X
[PROOFSTEP]
have aux : Fintype.card X = Fintype.card X - 1 + 1 := (Nat.succ_pred_eq_of_pos <| Fintype.card_pos_iff.mpr ⟨⊥⟩).symm
[GOAL]
X : NonemptyFinLinOrdCat
aux : Fintype.card ↑X = Fintype.card ↑X - 1 + 1
⊢ skeletalFunctor.obj [Fintype.card ↑X - 1] ≅ X
[PROOFSTEP]
let f := monoEquivOfFin X aux
[GOAL]
X : NonemptyFinLinOrdCat
aux : Fintype.card ↑X = Fintype.card ↑X - 1 + 1
f : Fin (Fintype.card ↑X - 1 + 1) ≃o ↑X := monoEquivOfFin (↑X) aux
⊢ skeletalFunctor.obj [Fintype.card ↑X - 1] ≅ X
[PROOFSTEP]
have hf := (Finset.univ.orderEmbOfFin aux).strictMono
[GOAL]
X : NonemptyFinLinOrdCat
aux : Fintype.card ↑X = Fintype.card ↑X - 1 + 1
f : Fin (Fintype.card ↑X - 1 + 1) ≃o ↑X := monoEquivOfFin (↑X) aux
hf : StrictMono ↑(Finset.orderEmbOfFin Finset.univ aux)
⊢ skeletalFunctor.obj [Fintype.card ↑X - 1] ≅ X
[PROOFSTEP]
refine'
  { hom := ⟨fun i => f i.down, _⟩
    inv := ⟨fun i => ⟨f.symm i⟩, _⟩
    hom_inv_id := _
    inv_hom_id := _ }
[GOAL]
case refine'_1
X : NonemptyFinLinOrdCat
aux : Fintype.card ↑X = Fintype.card ↑X - 1 + 1
f : Fin (Fintype.card ↑X - 1 + 1) ≃o ↑X := monoEquivOfFin (↑X) aux
hf : StrictMono ↑(Finset.orderEmbOfFin Finset.univ aux)
⊢ Monotone fun i => ↑f i.down
[PROOFSTEP]
rintro ⟨i⟩ ⟨j⟩ h
[GOAL]
case refine'_1.up.up
X : NonemptyFinLinOrdCat
aux : Fintype.card ↑X = Fintype.card ↑X - 1 + 1
f : Fin (Fintype.card ↑X - 1 + 1) ≃o ↑X := monoEquivOfFin (↑X) aux
hf : StrictMono ↑(Finset.orderEmbOfFin Finset.univ aux)
i j : Fin (len [Fintype.card ↑X - 1] + 1)
h : { down := i } ≤ { down := j }
⊢ (fun i => ↑f i.down) { down := i } ≤ (fun i => ↑f i.down) { down := j }
[PROOFSTEP]
show f i ≤ f j
[GOAL]
case refine'_1.up.up
X : NonemptyFinLinOrdCat
aux : Fintype.card ↑X = Fintype.card ↑X - 1 + 1
f : Fin (Fintype.card ↑X - 1 + 1) ≃o ↑X := monoEquivOfFin (↑X) aux
hf : StrictMono ↑(Finset.orderEmbOfFin Finset.univ aux)
i j : Fin (len [Fintype.card ↑X - 1] + 1)
h : { down := i } ≤ { down := j }
⊢ ↑f i ≤ ↑f j
[PROOFSTEP]
exact hf.monotone h
[GOAL]
case refine'_2
X : NonemptyFinLinOrdCat
aux : Fintype.card ↑X = Fintype.card ↑X - 1 + 1
f : Fin (Fintype.card ↑X - 1 + 1) ≃o ↑X := monoEquivOfFin (↑X) aux
hf : StrictMono ↑(Finset.orderEmbOfFin Finset.univ aux)
⊢ Monotone fun i => { down := ↑(OrderIso.symm f) i }
[PROOFSTEP]
intro i j h
[GOAL]
case refine'_2
X : NonemptyFinLinOrdCat
aux : Fintype.card ↑X = Fintype.card ↑X - 1 + 1
f : Fin (Fintype.card ↑X - 1 + 1) ≃o ↑X := monoEquivOfFin (↑X) aux
hf : StrictMono ↑(Finset.orderEmbOfFin Finset.univ aux)
i j : ↑X
h : i ≤ j
⊢ (fun i => { down := ↑(OrderIso.symm f) i }) i ≤ (fun i => { down := ↑(OrderIso.symm f) i }) j
[PROOFSTEP]
show f.symm i ≤ f.symm j
[GOAL]
case refine'_2
X : NonemptyFinLinOrdCat
aux : Fintype.card ↑X = Fintype.card ↑X - 1 + 1
f : Fin (Fintype.card ↑X - 1 + 1) ≃o ↑X := monoEquivOfFin (↑X) aux
hf : StrictMono ↑(Finset.orderEmbOfFin Finset.univ aux)
i j : ↑X
h : i ≤ j
⊢ ↑(OrderIso.symm f) i ≤ ↑(OrderIso.symm f) j
[PROOFSTEP]
rw [← hf.le_iff_le]
[GOAL]
case refine'_2
X : NonemptyFinLinOrdCat
aux : Fintype.card ↑X = Fintype.card ↑X - 1 + 1
f : Fin (Fintype.card ↑X - 1 + 1) ≃o ↑X := monoEquivOfFin (↑X) aux
hf : StrictMono ↑(Finset.orderEmbOfFin Finset.univ aux)
i j : ↑X
h : i ≤ j
⊢ ↑(Finset.orderEmbOfFin Finset.univ aux) (↑(OrderIso.symm f) i) ≤
    ↑(Finset.orderEmbOfFin Finset.univ aux) (↑(OrderIso.symm f) j)
[PROOFSTEP]
show f (f.symm i) ≤ f (f.symm j)
[GOAL]
case refine'_2
X : NonemptyFinLinOrdCat
aux : Fintype.card ↑X = Fintype.card ↑X - 1 + 1
f : Fin (Fintype.card ↑X - 1 + 1) ≃o ↑X := monoEquivOfFin (↑X) aux
hf : StrictMono ↑(Finset.orderEmbOfFin Finset.univ aux)
i j : ↑X
h : i ≤ j
⊢ ↑f (↑(OrderIso.symm f) i) ≤ ↑f (↑(OrderIso.symm f) j)
[PROOFSTEP]
simpa only [OrderIso.apply_symm_apply]
[GOAL]
case refine'_3
X : NonemptyFinLinOrdCat
aux : Fintype.card ↑X = Fintype.card ↑X - 1 + 1
f : Fin (Fintype.card ↑X - 1 + 1) ≃o ↑X := monoEquivOfFin (↑X) aux
hf : StrictMono ↑(Finset.orderEmbOfFin Finset.univ aux)
⊢ { toFun := fun i => ↑f i.down,
        monotone' :=
          (_ :
            ∀ ⦃a b : ↑(skeletalFunctor.obj [Fintype.card ↑X - 1])⦄,
              a ≤ b → (fun i => ↑f i.down) a ≤ (fun i => ↑f i.down) b) } ≫
      { toFun := fun i => { down := ↑(OrderIso.symm f) i },
        monotone' := (_ : ∀ ⦃i j : ↑X⦄, i ≤ j → ↑(OrderIso.symm f) i ≤ ↑(OrderIso.symm f) j) } =
    𝟙 (skeletalFunctor.obj [Fintype.card ↑X - 1])
[PROOFSTEP]
ext1 ⟨i⟩
[GOAL]
case refine'_3.w.up
X : NonemptyFinLinOrdCat
aux : Fintype.card ↑X = Fintype.card ↑X - 1 + 1
f : Fin (Fintype.card ↑X - 1 + 1) ≃o ↑X := monoEquivOfFin (↑X) aux
hf : StrictMono ↑(Finset.orderEmbOfFin Finset.univ aux)
i : Fin (len [Fintype.card ↑X - 1] + 1)
⊢ ↑({ toFun := fun i => ↑f i.down,
            monotone' :=
              (_ :
                ∀ ⦃a b : ↑(skeletalFunctor.obj [Fintype.card ↑X - 1])⦄,
                  a ≤ b → (fun i => ↑f i.down) a ≤ (fun i => ↑f i.down) b) } ≫
          { toFun := fun i => { down := ↑(OrderIso.symm f) i },
            monotone' := (_ : ∀ ⦃i j : ↑X⦄, i ≤ j → ↑(OrderIso.symm f) i ≤ ↑(OrderIso.symm f) j) })
      { down := i } =
    ↑(𝟙 (skeletalFunctor.obj [Fintype.card ↑X - 1])) { down := i }
[PROOFSTEP]
exact congr_arg ULift.up (f.symm_apply_apply i)
[GOAL]
case refine'_4
X : NonemptyFinLinOrdCat
aux : Fintype.card ↑X = Fintype.card ↑X - 1 + 1
f : Fin (Fintype.card ↑X - 1 + 1) ≃o ↑X := monoEquivOfFin (↑X) aux
hf : StrictMono ↑(Finset.orderEmbOfFin Finset.univ aux)
⊢ { toFun := fun i => { down := ↑(OrderIso.symm f) i },
        monotone' := (_ : ∀ ⦃i j : ↑X⦄, i ≤ j → ↑(OrderIso.symm f) i ≤ ↑(OrderIso.symm f) j) } ≫
      { toFun := fun i => ↑f i.down,
        monotone' :=
          (_ :
            ∀ ⦃a b : ↑(skeletalFunctor.obj [Fintype.card ↑X - 1])⦄,
              a ≤ b → (fun i => ↑f i.down) a ≤ (fun i => ↑f i.down) b) } =
    𝟙 X
[PROOFSTEP]
ext1 i
[GOAL]
case refine'_4.w
X : NonemptyFinLinOrdCat
aux : Fintype.card ↑X = Fintype.card ↑X - 1 + 1
f : Fin (Fintype.card ↑X - 1 + 1) ≃o ↑X := monoEquivOfFin (↑X) aux
hf : StrictMono ↑(Finset.orderEmbOfFin Finset.univ aux)
i : (forget NonemptyFinLinOrdCat).obj X
⊢ ↑({ toFun := fun i => { down := ↑(OrderIso.symm f) i },
            monotone' := (_ : ∀ ⦃i j : ↑X⦄, i ≤ j → ↑(OrderIso.symm f) i ≤ ↑(OrderIso.symm f) j) } ≫
          { toFun := fun i => ↑f i.down,
            monotone' :=
              (_ :
                ∀ ⦃a b : ↑(skeletalFunctor.obj [Fintype.card ↑X - 1])⦄,
                  a ≤ b → (fun i => ↑f i.down) a ≤ (fun i => ↑f i.down) b) })
      i =
    ↑(𝟙 X) i
[PROOFSTEP]
exact f.apply_symm_apply i
[GOAL]
n : ℕ
⊢ len [0] ≤ n
[PROOFSTEP]
simp
[GOAL]
X✝ Y✝ : SimplexCategory
a₁✝ a₂✝ : X✝ ⟶ Y✝
h :
  (CategoryTheory.Functor.mk { obj := fun i => Fin (len i + 1), map := fun {X Y} f => ↑(Hom.toOrderHom f) }).map a₁✝ =
    (CategoryTheory.Functor.mk { obj := fun i => Fin (len i + 1), map := fun {X Y} f => ↑(Hom.toOrderHom f) }).map a₂✝
⊢ a₁✝ = a₂✝
[PROOFSTEP]
ext : 2
[GOAL]
case a.h
X✝ Y✝ : SimplexCategory
a₁✝ a₂✝ : X✝ ⟶ Y✝
h :
  (CategoryTheory.Functor.mk { obj := fun i => Fin (len i + 1), map := fun {X Y} f => ↑(Hom.toOrderHom f) }).map a₁✝ =
    (CategoryTheory.Functor.mk { obj := fun i => Fin (len i + 1), map := fun {X Y} f => ↑(Hom.toOrderHom f) }).map a₂✝
⊢ ↑(Hom.toOrderHom a₁✝) = ↑(Hom.toOrderHom a₂✝)
[PROOFSTEP]
exact h
[GOAL]
n m : SimplexCategory
f : n ⟶ m
⊢ Mono f ↔ Function.Injective ↑(Hom.toOrderHom f)
[PROOFSTEP]
rw [← Functor.mono_map_iff_mono skeletalEquivalence.functor.{0}]
[GOAL]
n m : SimplexCategory
f : n ⟶ m
⊢ Mono (skeletalEquivalence.functor.map f) ↔ Function.Injective ↑(Hom.toOrderHom f)
[PROOFSTEP]
dsimp only [skeletalEquivalence, Functor.asEquivalence_functor]
[GOAL]
n m : SimplexCategory
f : n ⟶ m
⊢ Mono (skeletalFunctor.map f) ↔ Function.Injective ↑(Hom.toOrderHom f)
[PROOFSTEP]
rw [NonemptyFinLinOrdCat.mono_iff_injective, skeletalFunctor.coe_map, Function.Injective.of_comp_iff ULift.up_injective,
  Function.Injective.of_comp_iff' _ ULift.down_bijective]
[GOAL]
n m : SimplexCategory
f : n ⟶ m
⊢ Epi f ↔ Function.Surjective ↑(Hom.toOrderHom f)
[PROOFSTEP]
rw [← Functor.epi_map_iff_epi skeletalEquivalence.functor.{0}]
[GOAL]
n m : SimplexCategory
f : n ⟶ m
⊢ Epi (skeletalEquivalence.functor.map f) ↔ Function.Surjective ↑(Hom.toOrderHom f)
[PROOFSTEP]
dsimp only [skeletalEquivalence, Functor.asEquivalence_functor]
[GOAL]
n m : SimplexCategory
f : n ⟶ m
⊢ Epi (skeletalFunctor.map f) ↔ Function.Surjective ↑(Hom.toOrderHom f)
[PROOFSTEP]
rw [NonemptyFinLinOrdCat.epi_iff_surjective, skeletalFunctor.coe_map,
  Function.Surjective.of_comp_iff' ULift.up_bijective, Function.Surjective.of_comp_iff _ ULift.down_surjective]
[GOAL]
x y : SimplexCategory
f : x ⟶ y
⊢ Mono f → len x ≤ len y
[PROOFSTEP]
intro hyp_f_mono
[GOAL]
x y : SimplexCategory
f : x ⟶ y
hyp_f_mono : Mono f
⊢ len x ≤ len y
[PROOFSTEP]
have f_inj : Function.Injective f.toOrderHom.toFun := mono_iff_injective.1 hyp_f_mono
[GOAL]
x y : SimplexCategory
f : x ⟶ y
hyp_f_mono : Mono f
f_inj : Function.Injective (Hom.toOrderHom f).toFun
⊢ len x ≤ len y
[PROOFSTEP]
simpa using Fintype.card_le_of_injective f.toOrderHom.toFun f_inj
[GOAL]
x y : SimplexCategory
f : x ⟶ y
⊢ Epi f → len y ≤ len x
[PROOFSTEP]
intro hyp_f_epi
[GOAL]
x y : SimplexCategory
f : x ⟶ y
hyp_f_epi : Epi f
⊢ len y ≤ len x
[PROOFSTEP]
have f_surj : Function.Surjective f.toOrderHom.toFun := epi_iff_surjective.1 hyp_f_epi
[GOAL]
x y : SimplexCategory
f : x ⟶ y
hyp_f_epi : Epi f
f_surj : Function.Surjective (Hom.toOrderHom f).toFun
⊢ len y ≤ len x
[PROOFSTEP]
simpa using Fintype.card_le_of_surjective f.toOrderHom.toFun f_surj
[GOAL]
n : ℕ
i : Fin (n + 2)
⊢ Mono (δ i)
[PROOFSTEP]
rw [mono_iff_injective]
[GOAL]
n : ℕ
i : Fin (n + 2)
⊢ Function.Injective ↑(Hom.toOrderHom (δ i))
[PROOFSTEP]
exact Fin.succAbove_right_injective
[GOAL]
n : ℕ
i : Fin (n + 1)
⊢ Epi (σ i)
[PROOFSTEP]
rw [epi_iff_surjective]
[GOAL]
n : ℕ
i : Fin (n + 1)
⊢ Function.Surjective ↑(Hom.toOrderHom (σ i))
[PROOFSTEP]
intro b
[GOAL]
n : ℕ
i : Fin (n + 1)
b : Fin (len [n] + 1)
⊢ ∃ a, ↑(Hom.toOrderHom (σ i)) a = b
[PROOFSTEP]
simp only [σ, mkHom, Hom.toOrderHom_mk, OrderHom.coe_mk]
[GOAL]
n : ℕ
i : Fin (n + 1)
b : Fin (len [n] + 1)
⊢ ∃ a, Fin.predAbove i a = b
[PROOFSTEP]
by_cases b ≤ i
[GOAL]
n : ℕ
i : Fin (n + 1)
b : Fin (len [n] + 1)
⊢ ∃ a, Fin.predAbove i a = b
[PROOFSTEP]
by_cases b ≤ i
[GOAL]
case pos
n : ℕ
i : Fin (n + 1)
b : Fin (len [n] + 1)
h : b ≤ i
⊢ ∃ a, Fin.predAbove i a = b
[PROOFSTEP]
use b
[GOAL]
case h
n : ℕ
i : Fin (n + 1)
b : Fin (len [n] + 1)
h : b ≤ i
⊢ Fin.predAbove i ↑↑b = b
[PROOFSTEP]
rw [Fin.predAbove_below i b (by simpa only [Fin.coe_eq_castSucc] using h)]
[GOAL]
n : ℕ
i : Fin (n + 1)
b : Fin (len [n] + 1)
h : b ≤ i
⊢ ↑↑b ≤ Fin.castSucc i
[PROOFSTEP]
simpa only [Fin.coe_eq_castSucc] using h
[GOAL]
case h
n : ℕ
i : Fin (n + 1)
b : Fin (len [n] + 1)
h : b ≤ i
⊢ Fin.castPred ↑↑b = b
[PROOFSTEP]
simp only [len_mk, Fin.coe_eq_castSucc, Fin.castPred_castSucc]
[GOAL]
case neg
n : ℕ
i : Fin (n + 1)
b : Fin (len [n] + 1)
h : ¬b ≤ i
⊢ ∃ a, Fin.predAbove i a = b
[PROOFSTEP]
use b.succ
[GOAL]
case h
n : ℕ
i : Fin (n + 1)
b : Fin (len [n] + 1)
h : ¬b ≤ i
⊢ Fin.predAbove i (Fin.succ b) = b
[PROOFSTEP]
rw [Fin.predAbove_above i b.succ _, Fin.pred_succ]
[GOAL]
n : ℕ
i : Fin (n + 1)
b : Fin (len [n] + 1)
h : ¬b ≤ i
⊢ Fin.castSucc i < Fin.succ b
n : ℕ i : Fin (n + 1) b : Fin (len [n] + 1) h : ¬b ≤ i ⊢ Fin.castSucc i < Fin.succ b
[PROOFSTEP]
rw [not_le] at h
[GOAL]
n : ℕ
i : Fin (n + 1)
b : Fin (len [n] + 1)
h : i < b
⊢ Fin.castSucc i < Fin.succ b
[PROOFSTEP]
rw [Fin.lt_iff_val_lt_val] at h ⊢
[GOAL]
n : ℕ
i : Fin (n + 1)
b : Fin (len [n] + 1)
h : ↑i < ↑b
⊢ ↑(Fin.castSucc i) < ↑(Fin.succ b)
[PROOFSTEP]
simpa only [Fin.val_succ, Fin.coe_castSucc] using Nat.lt.step h
[GOAL]
A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
y₁ y₂ : Fin (len B✝ + 1)
h : y₁ ≤ y₂
⊢ inv ((forget SimplexCategory).map f) y₁ ≤ inv ((forget SimplexCategory).map f) y₂
[PROOFSTEP]
by_cases h' : y₁ < y₂
[GOAL]
case pos
A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
y₁ y₂ : Fin (len B✝ + 1)
h : y₁ ≤ y₂
h' : y₁ < y₂
⊢ inv ((forget SimplexCategory).map f) y₁ ≤ inv ((forget SimplexCategory).map f) y₂
[PROOFSTEP]
by_contra h''
[GOAL]
case pos
A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
y₁ y₂ : Fin (len B✝ + 1)
h : y₁ ≤ y₂
h' : y₁ < y₂
h'' : ¬inv ((forget SimplexCategory).map f) y₁ ≤ inv ((forget SimplexCategory).map f) y₂
⊢ False
[PROOFSTEP]
apply not_le.mpr h'
[GOAL]
case pos
A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
y₁ y₂ : Fin (len B✝ + 1)
h : y₁ ≤ y₂
h' : y₁ < y₂
h'' : ¬inv ((forget SimplexCategory).map f) y₁ ≤ inv ((forget SimplexCategory).map f) y₂
⊢ y₂ ≤ y₁
[PROOFSTEP]
convert f.toOrderHom.monotone (le_of_not_ge h'')
[GOAL]
case h.e'_3
A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
y₁ y₂ : Fin (len B✝ + 1)
h : y₁ ≤ y₂
h' : y₁ < y₂
h'' : ¬inv ((forget SimplexCategory).map f) y₁ ≤ inv ((forget SimplexCategory).map f) y₂
⊢ y₂ = ↑(Hom.toOrderHom f) (inv ((forget SimplexCategory).map f) y₂)
case h.e'_4
A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
y₁ y₂ : Fin (len B✝ + 1)
h : y₁ ≤ y₂
h' : y₁ < y₂
h'' : ¬inv ((forget SimplexCategory).map f) y₁ ≤ inv ((forget SimplexCategory).map f) y₂
⊢ y₁ = ↑(Hom.toOrderHom f) (inv ((forget SimplexCategory).map f) y₁)
[PROOFSTEP]
all_goals exact (congr_hom (Iso.inv_hom_id (asIso ((forget SimplexCategory).map f))) _).symm
[GOAL]
case h.e'_3
A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
y₁ y₂ : Fin (len B✝ + 1)
h : y₁ ≤ y₂
h' : y₁ < y₂
h'' : ¬inv ((forget SimplexCategory).map f) y₁ ≤ inv ((forget SimplexCategory).map f) y₂
⊢ y₂ = ↑(Hom.toOrderHom f) (inv ((forget SimplexCategory).map f) y₂)
[PROOFSTEP]
exact (congr_hom (Iso.inv_hom_id (asIso ((forget SimplexCategory).map f))) _).symm
[GOAL]
case h.e'_4
A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
y₁ y₂ : Fin (len B✝ + 1)
h : y₁ ≤ y₂
h' : y₁ < y₂
h'' : ¬inv ((forget SimplexCategory).map f) y₁ ≤ inv ((forget SimplexCategory).map f) y₂
⊢ y₁ = ↑(Hom.toOrderHom f) (inv ((forget SimplexCategory).map f) y₁)
[PROOFSTEP]
exact (congr_hom (Iso.inv_hom_id (asIso ((forget SimplexCategory).map f))) _).symm
[GOAL]
case neg
A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
y₁ y₂ : Fin (len B✝ + 1)
h : y₁ ≤ y₂
h' : ¬y₁ < y₂
⊢ inv ((forget SimplexCategory).map f) y₁ ≤ inv ((forget SimplexCategory).map f) y₂
[PROOFSTEP]
rw [eq_of_le_of_not_lt h h']
[GOAL]
A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
⊢ f ≫
      Hom.mk
        { toFun := inv ((forget SimplexCategory).map f),
          monotone' :=
            (_ :
              ∀ (y₁ y₂ : Fin (len B✝ + 1)),
                y₁ ≤ y₂ → inv ((forget SimplexCategory).map f) y₁ ≤ inv ((forget SimplexCategory).map f) y₂) } =
    𝟙 A✝
[PROOFSTEP]
ext1
[GOAL]
case a
A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
⊢ Hom.toOrderHom
      (f ≫
        Hom.mk
          { toFun := inv ((forget SimplexCategory).map f),
            monotone' :=
              (_ :
                ∀ (y₁ y₂ : Fin (len B✝ + 1)),
                  y₁ ≤ y₂ → inv ((forget SimplexCategory).map f) y₁ ≤ inv ((forget SimplexCategory).map f) y₂) }) =
    Hom.toOrderHom (𝟙 A✝)
[PROOFSTEP]
ext1
[GOAL]
case a.h
A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
⊢ ↑(Hom.toOrderHom
        (f ≫
          Hom.mk
            { toFun := inv ((forget SimplexCategory).map f),
              monotone' :=
                (_ :
                  ∀ (y₁ y₂ : Fin (len B✝ + 1)),
                    y₁ ≤ y₂ → inv ((forget SimplexCategory).map f) y₁ ≤ inv ((forget SimplexCategory).map f) y₂) })) =
    ↑(Hom.toOrderHom (𝟙 A✝))
[PROOFSTEP]
exact Iso.hom_inv_id (asIso ((forget _).map f))
[GOAL]
A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
⊢ Hom.mk
        { toFun := inv ((forget SimplexCategory).map f),
          monotone' :=
            (_ :
              ∀ (y₁ y₂ : Fin (len B✝ + 1)),
                y₁ ≤ y₂ → inv ((forget SimplexCategory).map f) y₁ ≤ inv ((forget SimplexCategory).map f) y₂) } ≫
      f =
    𝟙 B✝
[PROOFSTEP]
ext1
[GOAL]
case a
A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
⊢ Hom.toOrderHom
      (Hom.mk
          { toFun := inv ((forget SimplexCategory).map f),
            monotone' :=
              (_ :
                ∀ (y₁ y₂ : Fin (len B✝ + 1)),
                  y₁ ≤ y₂ → inv ((forget SimplexCategory).map f) y₁ ≤ inv ((forget SimplexCategory).map f) y₂) } ≫
        f) =
    Hom.toOrderHom (𝟙 B✝)
[PROOFSTEP]
ext1
[GOAL]
case a.h
A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
⊢ ↑(Hom.toOrderHom
        (Hom.mk
            { toFun := inv ((forget SimplexCategory).map f),
              monotone' :=
                (_ :
                  ∀ (y₁ y₂ : Fin (len B✝ + 1)),
                    y₁ ≤ y₂ → inv ((forget SimplexCategory).map f) y₁ ≤ inv ((forget SimplexCategory).map f) y₂) } ≫
          f)) =
    ↑(Hom.toOrderHom (𝟙 B✝))
[PROOFSTEP]
exact Iso.inv_hom_id (asIso ((forget _).map f))
[GOAL]
x y : SimplexCategory
e : x ≅ y
i : Fin (len x + 1)
⊢ ↑(Hom.toOrderHom e.inv) (↑(Hom.toOrderHom e.hom) i) = i
[PROOFSTEP]
simpa only using congr_arg (fun φ => (Hom.toOrderHom φ) i) e.hom_inv_id
[GOAL]
x y : SimplexCategory
e : x ≅ y
i : Fin (len y + 1)
⊢ ↑(Hom.toOrderHom e.hom) (↑(Hom.toOrderHom e.inv) i) = i
[PROOFSTEP]
simpa only using congr_arg (fun φ => (Hom.toOrderHom φ) i) e.inv_hom_id
[GOAL]
x : SimplexCategory
e : x ≅ x
⊢ e = Iso.refl x
[PROOFSTEP]
have h : (Finset.univ : Finset (Fin (x.len + 1))).card = x.len + 1 := Finset.card_fin (x.len + 1)
[GOAL]
x : SimplexCategory
e : x ≅ x
h : Finset.card Finset.univ = len x + 1
⊢ e = Iso.refl x
[PROOFSTEP]
have eq₁ := Finset.orderEmbOfFin_unique' h fun i => Finset.mem_univ ((orderIsoOfIso e) i)
[GOAL]
x : SimplexCategory
e : x ≅ x
h : Finset.card Finset.univ = len x + 1
eq₁ : RelIso.toRelEmbedding (orderIsoOfIso e) = Finset.orderEmbOfFin Finset.univ h
⊢ e = Iso.refl x
[PROOFSTEP]
have eq₂ :=
  Finset.orderEmbOfFin_unique' h fun i =>
    Finset.mem_univ
      ((orderIsoOfIso (Iso.refl x)) i)
        -- Porting note: the proof was rewritten from this point in #3414 (reenableeta)
          -- It could be investigated again to see if the original can be restored.
[GOAL]
x : SimplexCategory
e : x ≅ x
h : Finset.card Finset.univ = len x + 1
eq₁ : RelIso.toRelEmbedding (orderIsoOfIso e) = Finset.orderEmbOfFin Finset.univ h
eq₂ : RelIso.toRelEmbedding (orderIsoOfIso (Iso.refl x)) = Finset.orderEmbOfFin Finset.univ h
⊢ e = Iso.refl x
[PROOFSTEP]
ext x
[GOAL]
case w.a.h.h.h
x✝ : SimplexCategory
e : x✝ ≅ x✝
h : Finset.card Finset.univ = len x✝ + 1
eq₁ : RelIso.toRelEmbedding (orderIsoOfIso e) = Finset.orderEmbOfFin Finset.univ h
eq₂ : RelIso.toRelEmbedding (orderIsoOfIso (Iso.refl x✝)) = Finset.orderEmbOfFin Finset.univ h
x : Fin (len x✝ + 1)
⊢ ↑(↑(Hom.toOrderHom e.hom) x) = ↑(↑(Hom.toOrderHom (Iso.refl x✝).hom) x)
[PROOFSTEP]
replace eq₁ := congr_arg (· x) eq₁
[GOAL]
case w.a.h.h.h
x✝ : SimplexCategory
e : x✝ ≅ x✝
h : Finset.card Finset.univ = len x✝ + 1
eq₂ : RelIso.toRelEmbedding (orderIsoOfIso (Iso.refl x✝)) = Finset.orderEmbOfFin Finset.univ h
x : Fin (len x✝ + 1)
eq₁ :
  (fun x_1 => ↑x_1 x) (RelIso.toRelEmbedding (orderIsoOfIso e)) =
    (fun x_1 => ↑x_1 x) (Finset.orderEmbOfFin Finset.univ h)
⊢ ↑(↑(Hom.toOrderHom e.hom) x) = ↑(↑(Hom.toOrderHom (Iso.refl x✝).hom) x)
[PROOFSTEP]
replace eq₂ := congr_arg (· x) eq₂.symm
[GOAL]
case w.a.h.h.h
x✝ : SimplexCategory
e : x✝ ≅ x✝
h : Finset.card Finset.univ = len x✝ + 1
x : Fin (len x✝ + 1)
eq₁ :
  (fun x_1 => ↑x_1 x) (RelIso.toRelEmbedding (orderIsoOfIso e)) =
    (fun x_1 => ↑x_1 x) (Finset.orderEmbOfFin Finset.univ h)
eq₂ :
  (fun x_1 => ↑x_1 x) (Finset.orderEmbOfFin Finset.univ h) =
    (fun x_1 => ↑x_1 x) (RelIso.toRelEmbedding (orderIsoOfIso (Iso.refl x✝)))
⊢ ↑(↑(Hom.toOrderHom e.hom) x) = ↑(↑(Hom.toOrderHom (Iso.refl x✝).hom) x)
[PROOFSTEP]
simp_all
[GOAL]
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
⊢ ∃ θ', θ = σ i ≫ θ'
[PROOFSTEP]
use δ i.succ ≫ θ
[GOAL]
case h
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
⊢ θ = σ i ≫ δ (Fin.succ i) ≫ θ
[PROOFSTEP]
ext1
[GOAL]
case h.a
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
⊢ Hom.toOrderHom θ = Hom.toOrderHom (σ i ≫ δ (Fin.succ i) ≫ θ)
[PROOFSTEP]
ext1
[GOAL]
case h.a.h
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
⊢ ↑(Hom.toOrderHom θ) = ↑(Hom.toOrderHom (σ i ≫ δ (Fin.succ i) ≫ θ))
[PROOFSTEP]
ext1 x
[GOAL]
case h.a.h.h
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
⊢ ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom (σ i ≫ δ (Fin.succ i) ≫ θ)) x
[PROOFSTEP]
simp only [Hom.toOrderHom_mk, Function.comp_apply, OrderHom.comp_coe, Hom.comp, smallCategory_comp, σ, mkHom,
  OrderHom.coe_mk]
[GOAL]
case h.a.h.h
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
⊢ ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) (↑(Hom.toOrderHom (δ (Fin.succ i))) (Fin.predAbove i x))
[PROOFSTEP]
by_cases h' : x ≤ Fin.castSucc i
[GOAL]
case pos
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h' : x ≤ Fin.castSucc i
⊢ ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) (↑(Hom.toOrderHom (δ (Fin.succ i))) (Fin.predAbove i x))
[PROOFSTEP]
rw [Fin.predAbove_below i x h']
[GOAL]
case pos
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h' : x ≤ Fin.castSucc i
⊢ ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) (↑(Hom.toOrderHom (δ (Fin.succ i))) (Fin.castPred x))
[PROOFSTEP]
have eq := Fin.castSucc_castPred (gt_of_gt_of_ge (Fin.castSucc_lt_last i) h')
[GOAL]
case pos
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h' : x ≤ Fin.castSucc i
eq : Fin.castSucc (Fin.castPred x) = x
⊢ ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) (↑(Hom.toOrderHom (δ (Fin.succ i))) (Fin.castPred x))
[PROOFSTEP]
dsimp [δ]
[GOAL]
case pos
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h' : x ≤ Fin.castSucc i
eq : Fin.castSucc (Fin.castPred x) = x
⊢ ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) (Fin.succAbove (Fin.succ i) (Fin.castPred x))
[PROOFSTEP]
erw [Fin.succAbove_below i.succ x.castPred _]
[GOAL]
case pos
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h' : x ≤ Fin.castSucc i
eq : Fin.castSucc (Fin.castPred x) = x
⊢ ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) (Fin.castSucc (Fin.castPred x))
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h' : x ≤ Fin.castSucc i
eq : Fin.castSucc (Fin.castPred x) = x
⊢ Fin.castSucc (Fin.castPred x) < Fin.succ i
[PROOFSTEP]
swap
[GOAL]
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h' : x ≤ Fin.castSucc i
eq : Fin.castSucc (Fin.castPred x) = x
⊢ Fin.castSucc (Fin.castPred x) < Fin.succ i
[PROOFSTEP]
rwa [eq, ← Fin.le_castSucc_iff]
[GOAL]
case pos
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h' : x ≤ Fin.castSucc i
eq : Fin.castSucc (Fin.castPred x) = x
⊢ ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) (Fin.castSucc (Fin.castPred x))
[PROOFSTEP]
rw [eq]
[GOAL]
case neg
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h' : ¬x ≤ Fin.castSucc i
⊢ ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) (↑(Hom.toOrderHom (δ (Fin.succ i))) (Fin.predAbove i x))
[PROOFSTEP]
simp only [not_le] at h'
[GOAL]
case neg
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h' : Fin.castSucc i < x
⊢ ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) (↑(Hom.toOrderHom (δ (Fin.succ i))) (Fin.predAbove i x))
[PROOFSTEP]
let y := x.pred <| by rintro (rfl : x = 0); simp at h'
[GOAL]
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h' : Fin.castSucc i < x
⊢ x ≠ 0
[PROOFSTEP]
rintro (rfl : x = 0)
[GOAL]
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
h' : Fin.castSucc i < 0
⊢ False
[PROOFSTEP]
simp at h'
[GOAL]
case neg
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h' : Fin.castSucc i < x
y : Fin (len [n + 1]) := Fin.pred x (_ : x = 0 → False)
⊢ ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) (↑(Hom.toOrderHom (δ (Fin.succ i))) (Fin.predAbove i x))
[PROOFSTEP]
have hy : x = y.succ := (Fin.succ_pred x _).symm
[GOAL]
case neg
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h' : Fin.castSucc i < x
y : Fin (len [n + 1]) := Fin.pred x (_ : x = 0 → False)
hy : x = Fin.succ y
⊢ ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) (↑(Hom.toOrderHom (δ (Fin.succ i))) (Fin.predAbove i x))
[PROOFSTEP]
rw [hy] at h' ⊢
[GOAL]
case neg
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h'✝ : Fin.castSucc i < x
y : Fin (len [n + 1]) := Fin.pred x (_ : x = 0 → False)
h' : Fin.castSucc i < Fin.succ y
hy : x = Fin.succ y
⊢ ↑(Hom.toOrderHom θ) (Fin.succ y) =
    ↑(Hom.toOrderHom θ) (↑(Hom.toOrderHom (δ (Fin.succ i))) (Fin.predAbove i (Fin.succ y)))
[PROOFSTEP]
rw [Fin.predAbove_above i y.succ h', Fin.pred_succ]
[GOAL]
case neg
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h'✝ : Fin.castSucc i < x
y : Fin (len [n + 1]) := Fin.pred x (_ : x = 0 → False)
h' : Fin.castSucc i < Fin.succ y
hy : x = Fin.succ y
⊢ ↑(Hom.toOrderHom θ) (Fin.succ y) = ↑(Hom.toOrderHom θ) (↑(Hom.toOrderHom (δ (Fin.succ i))) y)
[PROOFSTEP]
by_cases h'' : y = i
[GOAL]
case pos
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h'✝ : Fin.castSucc i < x
y : Fin (len [n + 1]) := Fin.pred x (_ : x = 0 → False)
h' : Fin.castSucc i < Fin.succ y
hy : x = Fin.succ y
h'' : y = i
⊢ ↑(Hom.toOrderHom θ) (Fin.succ y) = ↑(Hom.toOrderHom θ) (↑(Hom.toOrderHom (δ (Fin.succ i))) y)
[PROOFSTEP]
rw [h'']
[GOAL]
case pos
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h'✝ : Fin.castSucc i < x
y : Fin (len [n + 1]) := Fin.pred x (_ : x = 0 → False)
h' : Fin.castSucc i < Fin.succ y
hy : x = Fin.succ y
h'' : y = i
⊢ ↑(Hom.toOrderHom θ) (Fin.succ i) = ↑(Hom.toOrderHom θ) (↑(Hom.toOrderHom (δ (Fin.succ i))) i)
[PROOFSTEP]
refine' hi.symm.trans _
[GOAL]
case pos
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h'✝ : Fin.castSucc i < x
y : Fin (len [n + 1]) := Fin.pred x (_ : x = 0 → False)
h' : Fin.castSucc i < Fin.succ y
hy : x = Fin.succ y
h'' : y = i
⊢ ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (↑(Hom.toOrderHom (δ (Fin.succ i))) i)
[PROOFSTEP]
congr 1
[GOAL]
case pos.h.e_6.h
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h'✝ : Fin.castSucc i < x
y : Fin (len [n + 1]) := Fin.pred x (_ : x = 0 → False)
h' : Fin.castSucc i < Fin.succ y
hy : x = Fin.succ y
h'' : y = i
⊢ Fin.castSucc i = ↑(Hom.toOrderHom (δ (Fin.succ i))) i
[PROOFSTEP]
dsimp [δ]
[GOAL]
case pos.h.e_6.h
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h'✝ : Fin.castSucc i < x
y : Fin (len [n + 1]) := Fin.pred x (_ : x = 0 → False)
h' : Fin.castSucc i < Fin.succ y
hy : x = Fin.succ y
h'' : y = i
⊢ Fin.castSucc i = Fin.succAbove (Fin.succ i) i
[PROOFSTEP]
erw [Fin.succAbove_below i.succ]
[GOAL]
case pos.h.e_6.h.h
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h'✝ : Fin.castSucc i < x
y : Fin (len [n + 1]) := Fin.pred x (_ : x = 0 → False)
h' : Fin.castSucc i < Fin.succ y
hy : x = Fin.succ y
h'' : y = i
⊢ Fin.castSucc i < Fin.succ i
[PROOFSTEP]
exact Fin.lt_succ
[GOAL]
case neg
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h'✝ : Fin.castSucc i < x
y : Fin (len [n + 1]) := Fin.pred x (_ : x = 0 → False)
h' : Fin.castSucc i < Fin.succ y
hy : x = Fin.succ y
h'' : ¬y = i
⊢ ↑(Hom.toOrderHom θ) (Fin.succ y) = ↑(Hom.toOrderHom θ) (↑(Hom.toOrderHom (δ (Fin.succ i))) y)
[PROOFSTEP]
dsimp [δ]
[GOAL]
case neg
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h'✝ : Fin.castSucc i < x
y : Fin (len [n + 1]) := Fin.pred x (_ : x = 0 → False)
h' : Fin.castSucc i < Fin.succ y
hy : x = Fin.succ y
h'' : ¬y = i
⊢ ↑(Hom.toOrderHom θ) (Fin.succ (Fin.pred x (_ : x = 0 → False))) =
    ↑(Hom.toOrderHom θ) (Fin.succAbove (Fin.succ i) (Fin.pred x (_ : x = 0 → False)))
[PROOFSTEP]
erw [Fin.succAbove_above i.succ _]
[GOAL]
case neg
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h'✝ : Fin.castSucc i < x
y : Fin (len [n + 1]) := Fin.pred x (_ : x = 0 → False)
h' : Fin.castSucc i < Fin.succ y
hy : x = Fin.succ y
h'' : ¬y = i
⊢ Fin.succ i ≤ Fin.castSucc (Fin.pred x (_ : x = 0 → False))
[PROOFSTEP]
simp only [Fin.lt_iff_val_lt_val, Fin.le_iff_val_le_val, Fin.val_succ, Fin.coe_castSucc, Nat.lt_succ_iff,
  Fin.ext_iff] at h' h'' ⊢
[GOAL]
case neg
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h'✝ : Fin.castSucc i < x
y : Fin (len [n + 1]) := Fin.pred x (_ : x = 0 → False)
hy : x = Fin.succ y
h' : ↑i ≤ ↑(Fin.pred x (_ : x = 0 → False))
h'' : ¬↑(Fin.pred x (_ : x = 0 → False)) = ↑i
⊢ ↑i + 1 ≤ ↑(Fin.pred x (_ : x = 0 → False))
[PROOFSTEP]
cases' Nat.le.dest h' with c hc
[GOAL]
case neg.intro
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h'✝ : Fin.castSucc i < x
y : Fin (len [n + 1]) := Fin.pred x (_ : x = 0 → False)
hy : x = Fin.succ y
h' : ↑i ≤ ↑(Fin.pred x (_ : x = 0 → False))
h'' : ¬↑(Fin.pred x (_ : x = 0 → False)) = ↑i
c : ℕ
hc : ↑i + c = ↑(Fin.pred x (_ : x = 0 → False))
⊢ ↑i + 1 ≤ ↑(Fin.pred x (_ : x = 0 → False))
[PROOFSTEP]
cases c
[GOAL]
case neg.intro.zero
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h'✝ : Fin.castSucc i < x
y : Fin (len [n + 1]) := Fin.pred x (_ : x = 0 → False)
hy : x = Fin.succ y
h' : ↑i ≤ ↑(Fin.pred x (_ : x = 0 → False))
h'' : ¬↑(Fin.pred x (_ : x = 0 → False)) = ↑i
hc : ↑i + Nat.zero = ↑(Fin.pred x (_ : x = 0 → False))
⊢ ↑i + 1 ≤ ↑(Fin.pred x (_ : x = 0 → False))
[PROOFSTEP]
exfalso
[GOAL]
case neg.intro.zero.h
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h'✝ : Fin.castSucc i < x
y : Fin (len [n + 1]) := Fin.pred x (_ : x = 0 → False)
hy : x = Fin.succ y
h' : ↑i ≤ ↑(Fin.pred x (_ : x = 0 → False))
h'' : ¬↑(Fin.pred x (_ : x = 0 → False)) = ↑i
hc : ↑i + Nat.zero = ↑(Fin.pred x (_ : x = 0 → False))
⊢ False
[PROOFSTEP]
simp only [Nat.zero_eq, add_zero, len_mk, Fin.coe_pred, ge_iff_le] at hc
[GOAL]
case neg.intro.zero.h
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h'✝ : Fin.castSucc i < x
y : Fin (len [n + 1]) := Fin.pred x (_ : x = 0 → False)
hy : x = Fin.succ y
h' : ↑i ≤ ↑(Fin.pred x (_ : x = 0 → False))
h'' : ¬↑(Fin.pred x (_ : x = 0 → False)) = ↑i
hc : ↑i = ↑x - 1
⊢ False
[PROOFSTEP]
rw [hc] at h''
[GOAL]
case neg.intro.zero.h
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h'✝ : Fin.castSucc i < x
y : Fin (len [n + 1]) := Fin.pred x (_ : x = 0 → False)
hy : x = Fin.succ y
h' : ↑i ≤ ↑(Fin.pred x (_ : x = 0 → False))
h'' : ¬↑(Fin.pred x (_ : x = 0 → False)) = ↑x - 1
hc : ↑i = ↑x - 1
⊢ False
[PROOFSTEP]
exact h'' rfl
[GOAL]
case neg.intro.succ
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h'✝ : Fin.castSucc i < x
y : Fin (len [n + 1]) := Fin.pred x (_ : x = 0 → False)
hy : x = Fin.succ y
h' : ↑i ≤ ↑(Fin.pred x (_ : x = 0 → False))
h'' : ¬↑(Fin.pred x (_ : x = 0 → False)) = ↑i
n✝ : ℕ
hc : ↑i + Nat.succ n✝ = ↑(Fin.pred x (_ : x = 0 → False))
⊢ ↑i + 1 ≤ ↑(Fin.pred x (_ : x = 0 → False))
[PROOFSTEP]
rw [← hc]
[GOAL]
case neg.intro.succ
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
i : Fin (n + 1)
hi : ↑(Hom.toOrderHom θ) (Fin.castSucc i) = ↑(Hom.toOrderHom θ) (Fin.succ i)
x : Fin (len [n + 1] + 1)
h'✝ : Fin.castSucc i < x
y : Fin (len [n + 1]) := Fin.pred x (_ : x = 0 → False)
hy : x = Fin.succ y
h' : ↑i ≤ ↑(Fin.pred x (_ : x = 0 → False))
h'' : ¬↑(Fin.pred x (_ : x = 0 → False)) = ↑i
n✝ : ℕ
hc : ↑i + Nat.succ n✝ = ↑(Fin.pred x (_ : x = 0 → False))
⊢ ↑i + 1 ≤ ↑i + Nat.succ n✝
[PROOFSTEP]
simp only [add_le_add_iff_left, Nat.succ_eq_add_one, le_add_iff_nonneg_left, zero_le]
[GOAL]
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
hθ : ¬Function.Injective ↑(Hom.toOrderHom θ)
⊢ ∃ i θ', θ = σ i ≫ θ'
[PROOFSTEP]
simp only [Function.Injective, exists_prop, not_forall] at hθ
[GOAL]
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
hθ : ∃ x x_1, ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) x_1 ∧ ¬x = x_1
⊢ ∃ i θ', θ = σ i ≫ θ'
[PROOFSTEP]
have hθ₂ : ∃ x y : Fin (n + 2), (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y ∧ x < y :=
  by
  rcases hθ with ⟨x, y, ⟨h₁, h₂⟩⟩
  by_cases h : x < y
  · exact ⟨x, y, ⟨h₁, h⟩⟩
  · refine' ⟨y, x, ⟨h₁.symm, _⟩⟩
    cases' lt_or_eq_of_le (not_lt.mp h) with h' h'
    · exact h'
    · exfalso
      exact h₂ h'.symm
[GOAL]
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
hθ : ∃ x x_1, ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) x_1 ∧ ¬x = x_1
⊢ ∃ x y, ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) y ∧ x < y
[PROOFSTEP]
rcases hθ with ⟨x, y, ⟨h₁, h₂⟩⟩
[GOAL]
case intro.intro.intro
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
x y : Fin (len [n + 1] + 1)
h₁ : ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) y
h₂ : ¬x = y
⊢ ∃ x y, ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) y ∧ x < y
[PROOFSTEP]
by_cases h : x < y
[GOAL]
case pos
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
x y : Fin (len [n + 1] + 1)
h₁ : ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) y
h₂ : ¬x = y
h : x < y
⊢ ∃ x y, ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) y ∧ x < y
[PROOFSTEP]
exact ⟨x, y, ⟨h₁, h⟩⟩
[GOAL]
case neg
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
x y : Fin (len [n + 1] + 1)
h₁ : ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) y
h₂ : ¬x = y
h : ¬x < y
⊢ ∃ x y, ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) y ∧ x < y
[PROOFSTEP]
refine' ⟨y, x, ⟨h₁.symm, _⟩⟩
[GOAL]
case neg
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
x y : Fin (len [n + 1] + 1)
h₁ : ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) y
h₂ : ¬x = y
h : ¬x < y
⊢ y < x
[PROOFSTEP]
cases' lt_or_eq_of_le (not_lt.mp h) with h' h'
[GOAL]
case neg.inl
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
x y : Fin (len [n + 1] + 1)
h₁ : ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) y
h₂ : ¬x = y
h : ¬x < y
h' : y < x
⊢ y < x
[PROOFSTEP]
exact h'
[GOAL]
case neg.inr
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
x y : Fin (len [n + 1] + 1)
h₁ : ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) y
h₂ : ¬x = y
h : ¬x < y
h' : y = x
⊢ y < x
[PROOFSTEP]
exfalso
[GOAL]
case neg.inr.h
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
x y : Fin (len [n + 1] + 1)
h₁ : ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) y
h₂ : ¬x = y
h : ¬x < y
h' : y = x
⊢ False
[PROOFSTEP]
exact h₂ h'.symm
[GOAL]
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
hθ : ∃ x x_1, ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) x_1 ∧ ¬x = x_1
hθ₂ : ∃ x y, ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) y ∧ x < y
⊢ ∃ i θ', θ = σ i ≫ θ'
[PROOFSTEP]
rcases hθ₂ with ⟨x, y, ⟨h₁, h₂⟩⟩
[GOAL]
case intro.intro.intro
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
hθ : ∃ x x_1, ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) x_1 ∧ ¬x = x_1
x y : Fin (n + 2)
h₁ : ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) y
h₂ : x < y
⊢ ∃ i θ', θ = σ i ≫ θ'
[PROOFSTEP]
let z := x.castPred
[GOAL]
case intro.intro.intro
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
hθ : ∃ x x_1, ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) x_1 ∧ ¬x = x_1
x y : Fin (n + 2)
h₁ : ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) y
h₂ : x < y
z : Fin (n + 1) := Fin.castPred x
⊢ ∃ i θ', θ = σ i ≫ θ'
[PROOFSTEP]
use z
[GOAL]
case h
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
hθ : ∃ x x_1, ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) x_1 ∧ ¬x = x_1
x y : Fin (n + 2)
h₁ : ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) y
h₂ : x < y
z : Fin (n + 1) := Fin.castPred x
⊢ ∃ θ', θ = σ z ≫ θ'
[PROOFSTEP]
rw [← show Fin.castSucc z = x from Fin.castSucc_castPred (lt_of_lt_of_le h₂ (Fin.le_last y))] at h₁ h₂
[GOAL]
case h
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
hθ : ∃ x x_1, ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) x_1 ∧ ¬x = x_1
x y : Fin (n + 2)
z : Fin (n + 1) := Fin.castPred x
h₂ : Fin.castSucc z < y
h₁ : ↑(Hom.toOrderHom θ) (Fin.castSucc z) = ↑(Hom.toOrderHom θ) y
⊢ ∃ θ', θ = σ z ≫ θ'
[PROOFSTEP]
apply eq_σ_comp_of_not_injective'
[GOAL]
case h.hi
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
hθ : ∃ x x_1, ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) x_1 ∧ ¬x = x_1
x y : Fin (n + 2)
z : Fin (n + 1) := Fin.castPred x
h₂ : Fin.castSucc z < y
h₁ : ↑(Hom.toOrderHom θ) (Fin.castSucc z) = ↑(Hom.toOrderHom θ) y
⊢ ↑(Hom.toOrderHom θ) (Fin.castSucc z) = ↑(Hom.toOrderHom θ) (Fin.succ z)
[PROOFSTEP]
rw [Fin.castSucc_lt_iff_succ_le] at h₂
[GOAL]
case h.hi
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
hθ : ∃ x x_1, ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) x_1 ∧ ¬x = x_1
x y : Fin (n + 2)
z : Fin (n + 1) := Fin.castPred x
h₂ : Fin.succ z ≤ y
h₁ : ↑(Hom.toOrderHom θ) (Fin.castSucc z) = ↑(Hom.toOrderHom θ) y
⊢ ↑(Hom.toOrderHom θ) (Fin.castSucc z) = ↑(Hom.toOrderHom θ) (Fin.succ z)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case h.hi.a
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
hθ : ∃ x x_1, ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) x_1 ∧ ¬x = x_1
x y : Fin (n + 2)
z : Fin (n + 1) := Fin.castPred x
h₂ : Fin.succ z ≤ y
h₁ : ↑(Hom.toOrderHom θ) (Fin.castSucc z) = ↑(Hom.toOrderHom θ) y
⊢ ↑(Hom.toOrderHom θ) (Fin.castSucc z) ≤ ↑(Hom.toOrderHom θ) (Fin.succ z)
[PROOFSTEP]
exact θ.toOrderHom.monotone (le_of_lt (Fin.castSucc_lt_succ z))
[GOAL]
case h.hi.a
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
hθ : ∃ x x_1, ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) x_1 ∧ ¬x = x_1
x y : Fin (n + 2)
z : Fin (n + 1) := Fin.castPred x
h₂ : Fin.succ z ≤ y
h₁ : ↑(Hom.toOrderHom θ) (Fin.castSucc z) = ↑(Hom.toOrderHom θ) y
⊢ ↑(Hom.toOrderHom θ) (Fin.succ z) ≤ ↑(Hom.toOrderHom θ) (Fin.castSucc z)
[PROOFSTEP]
rw [h₁]
[GOAL]
case h.hi.a
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
hθ : ∃ x x_1, ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) x_1 ∧ ¬x = x_1
x y : Fin (n + 2)
z : Fin (n + 1) := Fin.castPred x
h₂ : Fin.succ z ≤ y
h₁ : ↑(Hom.toOrderHom θ) (Fin.castSucc z) = ↑(Hom.toOrderHom θ) y
⊢ ↑(Hom.toOrderHom θ) (Fin.succ z) ≤ ↑(Hom.toOrderHom θ) y
[PROOFSTEP]
exact θ.toOrderHom.monotone h₂
[GOAL]
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
i : Fin (n + 2)
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ i
⊢ ∃ θ', θ = θ' ≫ δ i
[PROOFSTEP]
by_cases i < Fin.last (n + 1)
[GOAL]
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
i : Fin (n + 2)
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ i
⊢ ∃ θ', θ = θ' ≫ δ i
[PROOFSTEP]
by_cases i < Fin.last (n + 1)
[GOAL]
case pos
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
i : Fin (n + 2)
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
⊢ ∃ θ', θ = θ' ≫ δ i
[PROOFSTEP]
use θ ≫ σ (Fin.castPred i)
[GOAL]
case h
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
i : Fin (n + 2)
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
⊢ θ = (θ ≫ σ (Fin.castPred i)) ≫ δ i
[PROOFSTEP]
ext1
[GOAL]
case h.a
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
i : Fin (n + 2)
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
⊢ Hom.toOrderHom θ = Hom.toOrderHom ((θ ≫ σ (Fin.castPred i)) ≫ δ i)
[PROOFSTEP]
ext1
[GOAL]
case h.a.h
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
i : Fin (n + 2)
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
⊢ ↑(Hom.toOrderHom θ) = ↑(Hom.toOrderHom ((θ ≫ σ (Fin.castPred i)) ≫ δ i))
[PROOFSTEP]
ext1 x
[GOAL]
case h.a.h.h
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
i : Fin (n + 2)
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (len Δ + 1)
⊢ ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom ((θ ≫ σ (Fin.castPred i)) ≫ δ i)) x
[PROOFSTEP]
simp only [Hom.toOrderHom_mk, Function.comp_apply, OrderHom.comp_coe, Hom.comp, smallCategory_comp]
[GOAL]
case h.a.h.h
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
i : Fin (n + 2)
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (len Δ + 1)
⊢ ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom (δ i)) (↑(Hom.toOrderHom (σ (Fin.castPred i))) (↑(Hom.toOrderHom θ) x))
[PROOFSTEP]
by_cases h' : θ.toOrderHom x ≤ i
[GOAL]
case pos
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
i : Fin (n + 2)
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (len Δ + 1)
h' : ↑(Hom.toOrderHom θ) x ≤ i
⊢ ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom (δ i)) (↑(Hom.toOrderHom (σ (Fin.castPred i))) (↑(Hom.toOrderHom θ) x))
[PROOFSTEP]
simp only [σ, mkHom, Hom.toOrderHom_mk, OrderHom.coe_mk]
[GOAL]
case pos
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
i : Fin (n + 2)
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (len Δ + 1)
h' : ↑(Hom.toOrderHom θ) x ≤ i
⊢ ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom (δ i)) (Fin.predAbove (Fin.castPred i) (↑(Hom.toOrderHom θ) x))
[PROOFSTEP]
rw [Fin.predAbove_below (Fin.castPred i) (θ.toOrderHom x) (by simpa [Fin.castSucc_castPred h] using h')]
[GOAL]
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
i : Fin (n + 2)
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (len Δ + 1)
h' : ↑(Hom.toOrderHom θ) x ≤ i
⊢ ↑(Hom.toOrderHom θ) x ≤ Fin.castSucc (Fin.castPred i)
[PROOFSTEP]
simpa [Fin.castSucc_castPred h] using h'
[GOAL]
case pos
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
i : Fin (n + 2)
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (len Δ + 1)
h' : ↑(Hom.toOrderHom θ) x ≤ i
⊢ ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom (δ i)) (Fin.castPred (↑(Hom.toOrderHom θ) x))
[PROOFSTEP]
dsimp [δ]
[GOAL]
case pos
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
i : Fin (n + 2)
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (len Δ + 1)
h' : ↑(Hom.toOrderHom θ) x ≤ i
⊢ ↑(Hom.toOrderHom θ) x = Fin.succAbove i (Fin.castPred (↑(Hom.toOrderHom θ) x))
[PROOFSTEP]
erw [Fin.succAbove_below i]
[GOAL]
case pos
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
i : Fin (n + 2)
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (len Δ + 1)
h' : ↑(Hom.toOrderHom θ) x ≤ i
⊢ ↑(Hom.toOrderHom θ) x = Fin.castSucc (Fin.castPred (↑(Hom.toOrderHom θ) x))
case pos.h
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
i : Fin (n + 2)
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (len Δ + 1)
h' : ↑(Hom.toOrderHom θ) x ≤ i
⊢ Fin.castSucc (Fin.castPred (↑(Hom.toOrderHom θ) x)) < i
[PROOFSTEP]
swap
[GOAL]
case pos.h
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
i : Fin (n + 2)
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (len Δ + 1)
h' : ↑(Hom.toOrderHom θ) x ≤ i
⊢ Fin.castSucc (Fin.castPred (↑(Hom.toOrderHom θ) x)) < i
[PROOFSTEP]
simp only [Fin.lt_iff_val_lt_val, Fin.coe_castSucc]
[GOAL]
case pos.h
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
i : Fin (n + 2)
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (len Δ + 1)
h' : ↑(Hom.toOrderHom θ) x ≤ i
⊢ ↑(Fin.castPred (↑(Hom.toOrderHom θ) x)) < ↑i
[PROOFSTEP]
exact lt_of_le_of_lt (Fin.coe_castPred_le_self _) (Fin.lt_iff_val_lt_val.mp ((Ne.le_iff_lt (hi x)).mp h'))
[GOAL]
case pos
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
i : Fin (n + 2)
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (len Δ + 1)
h' : ↑(Hom.toOrderHom θ) x ≤ i
⊢ ↑(Hom.toOrderHom θ) x = Fin.castSucc (Fin.castPred (↑(Hom.toOrderHom θ) x))
[PROOFSTEP]
rw [Fin.castSucc_castPred]
[GOAL]
case pos
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
i : Fin (n + 2)
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (len Δ + 1)
h' : ↑(Hom.toOrderHom θ) x ≤ i
⊢ ↑(Hom.toOrderHom θ) x < Fin.last (n + 1)
[PROOFSTEP]
apply lt_of_le_of_lt h' h
[GOAL]
case neg
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
i : Fin (n + 2)
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (len Δ + 1)
h' : ¬↑(Hom.toOrderHom θ) x ≤ i
⊢ ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom (δ i)) (↑(Hom.toOrderHom (σ (Fin.castPred i))) (↑(Hom.toOrderHom θ) x))
[PROOFSTEP]
simp only [not_le] at h'
[GOAL]
case neg
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
i : Fin (n + 2)
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (len Δ + 1)
h' : i < ↑(Hom.toOrderHom θ) x
⊢ ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom (δ i)) (↑(Hom.toOrderHom (σ (Fin.castPred i))) (↑(Hom.toOrderHom θ) x))
[PROOFSTEP]
simp only [σ, mkHom, Hom.toOrderHom_mk, OrderHom.coe_mk,
  Fin.predAbove_above (Fin.castPred i) (θ.toOrderHom x) (by simpa only [Fin.castSucc_castPred h] using h')]
[GOAL]
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
i : Fin (n + 2)
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (len Δ + 1)
h' : i < ↑(Hom.toOrderHom θ) x
⊢ Fin.castSucc (Fin.castPred i) < ↑(Hom.toOrderHom θ) x
[PROOFSTEP]
simpa only [Fin.castSucc_castPred h] using h'
[GOAL]
case neg
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
i : Fin (n + 2)
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (len Δ + 1)
h' : i < ↑(Hom.toOrderHom θ) x
⊢ ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom (δ i)) (Fin.pred (↑(Hom.toOrderHom θ) x) (_ : ↑(Hom.toOrderHom θ) x ≠ 0))
[PROOFSTEP]
dsimp [δ]
[GOAL]
case neg
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
i : Fin (n + 2)
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (len Δ + 1)
h' : i < ↑(Hom.toOrderHom θ) x
⊢ ↑(Hom.toOrderHom θ) x = Fin.succAbove i (Fin.pred (↑(Hom.toOrderHom θ) x) (_ : ↑(Hom.toOrderHom θ) x ≠ 0))
[PROOFSTEP]
erw [Fin.succAbove_above i _, Fin.succ_pred]
[GOAL]
case neg
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
i : Fin (n + 2)
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (len Δ + 1)
h' : i < ↑(Hom.toOrderHom θ) x
⊢ i ≤ Fin.castSucc (Fin.pred (↑(Hom.toOrderHom θ) x) (_ : ↑(Hom.toOrderHom θ) x ≠ 0))
[PROOFSTEP]
simpa only [Fin.le_iff_val_le_val, Fin.coe_castSucc, Fin.coe_pred] using Nat.le_pred_of_lt (Fin.lt_iff_val_lt_val.mp h')
[GOAL]
case neg
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
i : Fin (n + 2)
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ i
h : ¬i < Fin.last (n + 1)
⊢ ∃ θ', θ = θ' ≫ δ i
[PROOFSTEP]
obtain rfl := le_antisymm (Fin.le_last i) (not_lt.mp h)
[GOAL]
case neg
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ Fin.last (n + 1)
h : ¬Fin.last (n + 1) < Fin.last (n + 1)
⊢ ∃ θ', θ = θ' ≫ δ (Fin.last (n + 1))
[PROOFSTEP]
use θ ≫ σ (Fin.last _)
[GOAL]
case h
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ Fin.last (n + 1)
h : ¬Fin.last (n + 1) < Fin.last (n + 1)
⊢ θ = (θ ≫ σ (Fin.last n)) ≫ δ (Fin.last (n + 1))
[PROOFSTEP]
ext x : 4
[GOAL]
case h.a.h.h.h
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ Fin.last (n + 1)
h : ¬Fin.last (n + 1) < Fin.last (n + 1)
x : Fin (len Δ + 1)
⊢ ↑(↑(Hom.toOrderHom θ) x) = ↑(↑(Hom.toOrderHom ((θ ≫ σ (Fin.last n)) ≫ δ (Fin.last (n + 1)))) x)
[PROOFSTEP]
dsimp [δ, σ]
[GOAL]
case h.a.h.h.h
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ Fin.last (n + 1)
h : ¬Fin.last (n + 1) < Fin.last (n + 1)
x : Fin (len Δ + 1)
⊢ ↑(↑(Hom.toOrderHom θ) x) = ↑(Fin.succAbove (Fin.last (n + 1)) (Fin.castPred (↑(Hom.toOrderHom θ) x)))
[PROOFSTEP]
dsimp only [Fin.castPred]
[GOAL]
case h.a.h.h.h
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ Fin.last (n + 1)
h : ¬Fin.last (n + 1) < Fin.last (n + 1)
x : Fin (len Δ + 1)
⊢ ↑(↑(Hom.toOrderHom θ) x) = ↑(Fin.succAbove (Fin.last (n + 1)) (Fin.predAbove (Fin.last n) (↑(Hom.toOrderHom θ) x)))
[PROOFSTEP]
rw [Fin.predAbove_last, Fin.succAbove_last, Fin.castSucc_castPred]
[GOAL]
case h.a.h.h.h
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ Fin.last (n + 1)
h : ¬Fin.last (n + 1) < Fin.last (n + 1)
x : Fin (len Δ + 1)
⊢ ↑(Hom.toOrderHom θ) x < Fin.last (n + 1)
[PROOFSTEP]
exact (Ne.le_iff_lt (hi x)).mp (Fin.le_last _)
[GOAL]
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
hθ : ¬Function.Surjective ↑(Hom.toOrderHom θ)
⊢ ∃ i θ', θ = θ' ≫ δ i
[PROOFSTEP]
cases' not_forall.mp hθ with i hi
[GOAL]
case intro
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
hθ : ¬Function.Surjective ↑(Hom.toOrderHom θ)
i : Fin (len [n + 1] + 1)
hi : ¬∃ a, ↑(Hom.toOrderHom θ) a = i
⊢ ∃ i θ', θ = θ' ≫ δ i
[PROOFSTEP]
use i
[GOAL]
case h
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
hθ : ¬Function.Surjective ↑(Hom.toOrderHom θ)
i : Fin (len [n + 1] + 1)
hi : ¬∃ a, ↑(Hom.toOrderHom θ) a = i
⊢ ∃ θ', θ = θ' ≫ δ i
[PROOFSTEP]
exact eq_comp_δ_of_not_surjective' θ i (not_exists.mp hi)
[GOAL]
x : SimplexCategory
i : x ⟶ x
inst✝ : Mono i
⊢ i = 𝟙 x
[PROOFSTEP]
suffices IsIso i by apply eq_id_of_isIso
[GOAL]
x : SimplexCategory
i : x ⟶ x
inst✝ : Mono i
this : IsIso i
⊢ i = 𝟙 x
[PROOFSTEP]
apply eq_id_of_isIso
[GOAL]
x : SimplexCategory
i : x ⟶ x
inst✝ : Mono i
⊢ IsIso i
[PROOFSTEP]
apply isIso_of_bijective
[GOAL]
case hf
x : SimplexCategory
i : x ⟶ x
inst✝ : Mono i
⊢ Function.Bijective (Hom.toOrderHom i).toFun
[PROOFSTEP]
dsimp
[GOAL]
case hf
x : SimplexCategory
i : x ⟶ x
inst✝ : Mono i
⊢ Function.Bijective ↑(Hom.toOrderHom i)
[PROOFSTEP]
rw [Fintype.bijective_iff_injective_and_card i.toOrderHom, ← mono_iff_injective, eq_self_iff_true, and_true_iff]
[GOAL]
case hf
x : SimplexCategory
i : x ⟶ x
inst✝ : Mono i
⊢ Mono i
[PROOFSTEP]
infer_instance
[GOAL]
x : SimplexCategory
i : x ⟶ x
inst✝ : Epi i
⊢ i = 𝟙 x
[PROOFSTEP]
suffices IsIso i by
  haveI := this
  apply eq_id_of_isIso
[GOAL]
x : SimplexCategory
i : x ⟶ x
inst✝ : Epi i
this : IsIso i
⊢ i = 𝟙 x
[PROOFSTEP]
haveI := this
[GOAL]
x : SimplexCategory
i : x ⟶ x
inst✝ : Epi i
this✝ this : IsIso i
⊢ i = 𝟙 x
[PROOFSTEP]
apply eq_id_of_isIso
[GOAL]
x : SimplexCategory
i : x ⟶ x
inst✝ : Epi i
⊢ IsIso i
[PROOFSTEP]
apply isIso_of_bijective
[GOAL]
case hf
x : SimplexCategory
i : x ⟶ x
inst✝ : Epi i
⊢ Function.Bijective (Hom.toOrderHom i).toFun
[PROOFSTEP]
dsimp
[GOAL]
case hf
x : SimplexCategory
i : x ⟶ x
inst✝ : Epi i
⊢ Function.Bijective ↑(Hom.toOrderHom i)
[PROOFSTEP]
rw [Fintype.bijective_iff_surjective_and_card i.toOrderHom, ← epi_iff_surjective, eq_self_iff_true, and_true_iff]
[GOAL]
case hf
x : SimplexCategory
i : x ⟶ x
inst✝ : Epi i
⊢ Epi i
[PROOFSTEP]
infer_instance
[GOAL]
n : ℕ
θ : [n + 1] ⟶ [n]
inst✝ : Epi θ
⊢ ∃ i, θ = σ i
[PROOFSTEP]
rcases eq_σ_comp_of_not_injective θ
    (by
      by_contra h
      simpa using le_of_mono (mono_iff_injective.mpr h)) with
  ⟨i, θ', h⟩
[GOAL]
n : ℕ
θ : [n + 1] ⟶ [n]
inst✝ : Epi θ
⊢ ¬Function.Injective ↑(Hom.toOrderHom θ)
[PROOFSTEP]
by_contra h
[GOAL]
n : ℕ
θ : [n + 1] ⟶ [n]
inst✝ : Epi θ
h : Function.Injective ↑(Hom.toOrderHom θ)
⊢ False
[PROOFSTEP]
simpa using le_of_mono (mono_iff_injective.mpr h)
[GOAL]
case intro.intro
n : ℕ
θ : [n + 1] ⟶ [n]
inst✝ : Epi θ
i : Fin (n + 1)
θ' : [n] ⟶ [n]
h : θ = σ i ≫ θ'
⊢ ∃ i, θ = σ i
[PROOFSTEP]
use i
[GOAL]
case h
n : ℕ
θ : [n + 1] ⟶ [n]
inst✝ : Epi θ
i : Fin (n + 1)
θ' : [n] ⟶ [n]
h : θ = σ i ≫ θ'
⊢ θ = σ i
[PROOFSTEP]
haveI : Epi (σ i ≫ θ') := by
  rw [← h]
  infer_instance
[GOAL]
n : ℕ
θ : [n + 1] ⟶ [n]
inst✝ : Epi θ
i : Fin (n + 1)
θ' : [n] ⟶ [n]
h : θ = σ i ≫ θ'
⊢ Epi (σ i ≫ θ')
[PROOFSTEP]
rw [← h]
[GOAL]
n : ℕ
θ : [n + 1] ⟶ [n]
inst✝ : Epi θ
i : Fin (n + 1)
θ' : [n] ⟶ [n]
h : θ = σ i ≫ θ'
⊢ Epi θ
[PROOFSTEP]
infer_instance
[GOAL]
case h
n : ℕ
θ : [n + 1] ⟶ [n]
inst✝ : Epi θ
i : Fin (n + 1)
θ' : [n] ⟶ [n]
h : θ = σ i ≫ θ'
this : Epi (σ i ≫ θ')
⊢ θ = σ i
[PROOFSTEP]
haveI := CategoryTheory.epi_of_epi (σ i) θ'
[GOAL]
case h
n : ℕ
θ : [n + 1] ⟶ [n]
inst✝ : Epi θ
i : Fin (n + 1)
θ' : [n] ⟶ [n]
h : θ = σ i ≫ θ'
this✝ : Epi (σ i ≫ θ')
this : Epi θ'
⊢ θ = σ i
[PROOFSTEP]
rw [h, eq_id_of_epi θ', Category.comp_id]
[GOAL]
n : ℕ
θ : [n] ⟶ [n + 1]
inst✝ : Mono θ
⊢ ∃ i, θ = δ i
[PROOFSTEP]
rcases eq_comp_δ_of_not_surjective θ
    (by
      by_contra h
      simpa using le_of_epi (epi_iff_surjective.mpr h)) with
  ⟨i, θ', h⟩
[GOAL]
n : ℕ
θ : [n] ⟶ [n + 1]
inst✝ : Mono θ
⊢ ¬Function.Surjective ↑(Hom.toOrderHom θ)
[PROOFSTEP]
by_contra h
[GOAL]
n : ℕ
θ : [n] ⟶ [n + 1]
inst✝ : Mono θ
h : Function.Surjective ↑(Hom.toOrderHom θ)
⊢ False
[PROOFSTEP]
simpa using le_of_epi (epi_iff_surjective.mpr h)
[GOAL]
case intro.intro
n : ℕ
θ : [n] ⟶ [n + 1]
inst✝ : Mono θ
i : Fin (n + 2)
θ' : [n] ⟶ [n]
h : θ = θ' ≫ δ i
⊢ ∃ i, θ = δ i
[PROOFSTEP]
use i
[GOAL]
case h
n : ℕ
θ : [n] ⟶ [n + 1]
inst✝ : Mono θ
i : Fin (n + 2)
θ' : [n] ⟶ [n]
h : θ = θ' ≫ δ i
⊢ θ = δ i
[PROOFSTEP]
haveI : Mono (θ' ≫ δ i) := by
  rw [← h]
  infer_instance
[GOAL]
n : ℕ
θ : [n] ⟶ [n + 1]
inst✝ : Mono θ
i : Fin (n + 2)
θ' : [n] ⟶ [n]
h : θ = θ' ≫ δ i
⊢ Mono (θ' ≫ δ i)
[PROOFSTEP]
rw [← h]
[GOAL]
n : ℕ
θ : [n] ⟶ [n + 1]
inst✝ : Mono θ
i : Fin (n + 2)
θ' : [n] ⟶ [n]
h : θ = θ' ≫ δ i
⊢ Mono θ
[PROOFSTEP]
infer_instance
[GOAL]
case h
n : ℕ
θ : [n] ⟶ [n + 1]
inst✝ : Mono θ
i : Fin (n + 2)
θ' : [n] ⟶ [n]
h : θ = θ' ≫ δ i
this : Mono (θ' ≫ δ i)
⊢ θ = δ i
[PROOFSTEP]
haveI := CategoryTheory.mono_of_mono θ' (δ i)
[GOAL]
case h
n : ℕ
θ : [n] ⟶ [n + 1]
inst✝ : Mono θ
i : Fin (n + 2)
θ' : [n] ⟶ [n]
h : θ = θ' ≫ δ i
this✝ : Mono (θ' ≫ δ i)
this : Mono θ'
⊢ θ = δ i
[PROOFSTEP]
rw [h, eq_id_of_mono θ', Category.id_comp]
[GOAL]
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
hi : Mono i
hi' : Δ ≠ Δ'
⊢ len Δ' < len Δ
[PROOFSTEP]
rcases lt_or_eq_of_le (len_le_of_mono hi) with (h | h)
[GOAL]
case inl
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
hi : Mono i
hi' : Δ ≠ Δ'
h : len Δ' < len Δ
⊢ len Δ' < len Δ
[PROOFSTEP]
exact h
[GOAL]
case inr
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
hi : Mono i
hi' : Δ ≠ Δ'
h : len Δ' = len Δ
⊢ len Δ' < len Δ
[PROOFSTEP]
exfalso
[GOAL]
case inr.h
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
hi : Mono i
hi' : Δ ≠ Δ'
h : len Δ' = len Δ
⊢ False
[PROOFSTEP]
exact hi' (by ext; exact h.symm)
[GOAL]
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
hi : Mono i
hi' : Δ ≠ Δ'
h : len Δ' = len Δ
⊢ Δ = Δ'
[PROOFSTEP]
ext
[GOAL]
case a
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
hi : Mono i
hi' : Δ ≠ Δ'
h : len Δ' = len Δ
⊢ len Δ = len Δ'
[PROOFSTEP]
exact h.symm
[GOAL]
Δ Δ' Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ Δ'
inst✝¹ : Epi e
i : Δ' ⟶ Δ''
inst✝ : Mono i
fac : e ≫ i = φ
⊢ image φ = Δ'
[PROOFSTEP]
haveI := strongEpi_of_epi e
[GOAL]
Δ Δ' Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ Δ'
inst✝¹ : Epi e
i : Δ' ⟶ Δ''
inst✝ : Mono i
fac : e ≫ i = φ
this : StrongEpi e
⊢ image φ = Δ'
[PROOFSTEP]
let e := image.isoStrongEpiMono e i fac
[GOAL]
Δ Δ' Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e✝ : Δ ⟶ Δ'
inst✝¹ : Epi e✝
i : Δ' ⟶ Δ''
inst✝ : Mono i
fac : e✝ ≫ i = φ
this : StrongEpi e✝
e : Δ' ≅ image φ := image.isoStrongEpiMono e✝ i fac
⊢ image φ = Δ'
[PROOFSTEP]
ext
[GOAL]
case a
Δ Δ' Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e✝ : Δ ⟶ Δ'
inst✝¹ : Epi e✝
i : Δ' ⟶ Δ''
inst✝ : Mono i
fac : e✝ ≫ i = φ
this : StrongEpi e✝
e : Δ' ≅ image φ := image.isoStrongEpiMono e✝ i fac
⊢ len (image φ) = len Δ'
[PROOFSTEP]
exact le_antisymm (len_le_of_epi (inferInstance : Epi e.hom)) (len_le_of_mono (inferInstance : Mono e.hom))
[GOAL]
Δ Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ image φ
inst✝¹ : Epi e
i : image φ ⟶ Δ''
inst✝ : Mono i
fac : e ≫ i = φ
⊢ image.ι φ = i
[PROOFSTEP]
haveI := strongEpi_of_epi e
[GOAL]
Δ Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ image φ
inst✝¹ : Epi e
i : image φ ⟶ Δ''
inst✝ : Mono i
fac : e ≫ i = φ
this : StrongEpi e
⊢ image.ι φ = i
[PROOFSTEP]
rw [← image.isoStrongEpiMono_hom_comp_ι e i fac, SimplexCategory.eq_id_of_isIso (image.isoStrongEpiMono e i fac).hom,
  Category.id_comp]
[GOAL]
Δ Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ image φ
inst✝¹ : Epi e
i : image φ ⟶ Δ''
inst✝ : Mono i
fac : e ≫ i = φ
⊢ factorThruImage φ = e
[PROOFSTEP]
rw [← cancel_mono i, fac, ← image_ι_eq fac, image.fac]