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

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
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
i : Fin (n + 2)
hi : ∀ (x : Fin (len Δ + 1)), ↑(Hom.toOrderHom θ) x ≠ i
⊢ ∃ θ', θ = θ' ≫ δ i
by_cases i < Fin.last (n + 1)
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)
⊢ θ = (θ ≫ σ (Fin.castPred i)) ≫ δ i
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
use θ ≫ σ (Fin.castPred i)
case pos.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)
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)
⊢ θ = (θ ≫ σ (Fin.castPred i)) ≫ δ i
ext1
case pos.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))
case pos.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)
ext1
case pos.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
case pos.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))
ext1 x
case pos.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))
case pos.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
simp only [Hom.toOrderHom_mk, Function.comp_apply, OrderHom.comp_coe, Hom.comp,
  smallCategory_comp]
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))

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))
case pos.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))
by_cases h' : θ.toOrderHom x ≤ i
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))
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))
simp only [σ, mkHom, Hom.toOrderHom_mk, OrderHom.coe_fun_mk]
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))
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))
rw [Fin.predAbove_below (Fin.castPred i) (θ.toOrderHom x)
    (by simpa [Fin.castSucc_castPred h] using h')]
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))
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))
dsimp [δ]
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
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))
erw [Fin.succAbove_below i]
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

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
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
swap
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)
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))
rw [Fin.castSucc_castPred]
no goals
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)
apply lt_of_le_of_lt h' h
no goals
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)
simpa [Fin.castSucc_castPred h] using h'
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
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
simp only [Fin.lt_iff_val_lt_val, Fin.coe_castSucc]
no goals
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
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'))
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))
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))
simp only [not_le] at h'
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))
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))
simp only [σ, mkHom, Hom.toOrderHom_mk, OrderHom.coe_fun_mk,
  Fin.predAbove_above (Fin.castPred i) (θ.toOrderHom x)
    (by simpa only [Fin.castSucc_castPred h] using h')]
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))
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))
dsimp [δ]
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))
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))
erw [Fin.succAbove_above i _, Fin.succ_pred]
no goals
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))
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')
no goals
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
simpa only [Fin.castSucc_castPred h] using h'
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))
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
obtain rfl := le_antisymm (Fin.le_last i) (not_lt.mp h)
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)) ≫ δ (Fin.last (n + 1))
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))
use θ ≫ σ (Fin.last _)
case neg.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)
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)) ≫ δ (Fin.last (n + 1))
ext x : 4
case neg.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)))
case neg.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)
dsimp [δ, σ]
case neg.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)))
case neg.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)))
dsimp only [Fin.castPred]
case neg.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)
case neg.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)))
rw [Fin.predAbove_last, Fin.succAbove_last, Fin.castSucc_castPred]
no goals
case neg.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)
exact (Ne.le_iff_lt (hi x)).mp (Fin.le_last _)