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
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
hθ : ¬Function.Surjective ↑(Hom.toOrderHom θ)
⊢ ∃ i θ', θ = θ' ≫ δ i
cases' not_forall.mp hθ with i hi
case intro
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
hθ : ¬Function.Surjective ↑(Hom.toOrderHom θ)
i : Fin (len [n + 1] + 1)
hi : ¬∃ a, ↑(Hom.toOrderHom θ) a = i
⊢ ∃ θ', θ = θ' ≫ δ i
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
use i
no goals
case intro
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ [n + 1]
hθ : ¬Function.Surjective ↑(Hom.toOrderHom θ)
i : Fin (len [n + 1] + 1)
hi : ¬∃ a, ↑(Hom.toOrderHom θ) a = i
⊢ ∃ θ', θ = θ' ≫ δ i
exact eq_comp_δ_of_not_surjective' θ i (not_exists.mp hi)