case inl
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
hi : Mono i
hi' : Δ ≠ Δ'
h : len Δ' < len Δ
⊢ len Δ' < len Δ

case inr
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
hi : Mono i
hi' : Δ ≠ Δ'
h : len Δ' = len Δ
⊢ len Δ' < len Δ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
hi : Mono i
hi' : Δ ≠ Δ'
⊢ len Δ' < len Δ
rcases lt_or_eq_of_le (len_le_of_mono hi) with (h | h)
no goals
case inl
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
hi : Mono i
hi' : Δ ≠ Δ'
h : len Δ' < len Δ
⊢ len Δ' < len Δ
exact h
case inr.h
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
hi : Mono i
hi' : Δ ≠ Δ'
h : len Δ' = len Δ
⊢ False
case inr
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
hi : Mono i
hi' : Δ ≠ Δ'
h : len Δ' = len Δ
⊢ len Δ' < len Δ
exfalso
no goals
case inr.h
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
hi : Mono i
hi' : Δ ≠ Δ'
h : len Δ' = len Δ
⊢ False
exact hi' (by ext ; exact h.symm)
case a
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
hi : Mono i
hi' : Δ ≠ Δ'
h : len Δ' = len Δ
⊢ len Δ = len Δ'
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
hi : Mono i
hi' : Δ ≠ Δ'
h : len Δ' = len Δ
⊢ Δ = Δ'
ext
no goals
case a
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
hi : Mono i
hi' : Δ ≠ Δ'
h : len Δ' = len Δ
⊢ len Δ = len Δ'
exact h.symm