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

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))
case 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))
by_cases h' : x ≤ Fin.castSucc i
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))
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))
rw [Fin.predAbove_below i x h']
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))
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))
have eq := Fin.castSucc_castPred (gt_of_gt_of_ge (Fin.castSucc_lt_last i) h')
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))
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))
dsimp [δ]
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
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))
erw [Fin.succAbove_below i.succ x.castPred _]
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

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))
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
swap
no goals
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))
rw [eq]
no goals
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
rwa [eq, ← Fin.le_castSucc_iff]
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))
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))
simp only [not_le] at h'
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))
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))
let y := x.pred (by rintro rfl ; simp at h')
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))
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))
have hy : x = y.succ := (Fin.succ_pred x _).symm
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)))
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))
rw [hy] at h' ⊢
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)
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)))
rw [Fin.predAbove_above i y.succ h', Fin.pred_succ]
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)

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)
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)
by_cases h'' : y = i
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
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
rintro rfl
no goals
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
simp at h'
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)
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)
rw [h'']
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)
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)
refine' hi.symm.trans _
case pos.e_a
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
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)
congr 1
case pos.e_a
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
case pos.e_a
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
dsimp [δ]
case pos.e_a.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
case pos.e_a
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
erw [Fin.succAbove_below i.succ]
no goals
case pos.e_a.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
exact Fin.lt_succ
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)))
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)
dsimp [δ]
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))
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)))
erw [Fin.succAbove_above i.succ _]
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))
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))
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''⊢
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))
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))
cases' Nat.le.dest h' with c hc
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))

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))
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))
cases c
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
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))
exfalso
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
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
simp only [Nat.zero_eq, add_zero, len_mk, Fin.coe_pred, ge_iff_le] at hc
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
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
rw [hc] at h''
no goals
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
exact h'' rfl
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✝
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))
rw [← hc]
no goals
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✝
simp only [add_le_add_iff_left, Nat.succ_eq_add_one, le_add_iff_nonneg_left, zero_le]