n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
hθ : ∃ x x_1, ↑(Hom.toOrderHom θ) x = ↑(Hom.toOrderHom θ) x_1 ∧ ¬x = x_1
⊢ ∃ i θ', θ = σ i ≫ θ'
n : ℕ
Δ' : SimplexCategory
θ : [n + 1] ⟶ Δ'
hθ : ¬Function.Injective ↑(Hom.toOrderHom θ)
⊢ ∃ i θ', θ = σ i ≫ θ'
simp only [Function.Injective, exists_prop, not_forall] at hθ
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 ≫ θ'
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 ≫ θ'
rcases hθ₂ with ⟨x, y, ⟨h₁, h₂⟩⟩
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 ≫ θ'
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 ≫ θ'
let z := x.castPred
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
⊢ ∃ θ', θ = σ z ≫ θ'
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 ≫ θ'
use z
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)
z : Fin (n + 1) := Fin.castPred x
h₂ : ↑Fin.castSucc z < y
h₁ : ↑(Hom.toOrderHom θ) (↑Fin.castSucc z) = ↑(Hom.toOrderHom θ) y
⊢ ∃ θ', θ = σ z ≫ θ'
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
⊢ ∃ θ', θ = σ z ≫ θ'
rw [← show Fin.castSucc z = x from
  Fin.castSucc_castPred (lt_of_lt_of_le h₂ (Fin.le_last y))] at h₁ h₂
case intro.intro.intro.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)
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)
z : Fin (n + 1) := Fin.castPred x
h₂ : ↑Fin.castSucc z < y
h₁ : ↑(Hom.toOrderHom θ) (↑Fin.castSucc z) = ↑(Hom.toOrderHom θ) y
⊢ ∃ θ', θ = σ z ≫ θ'
apply eq_σ_comp_of_not_injective'
case intro.intro.intro.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)
case intro.intro.intro.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)
rw [Fin.castSucc_lt_iff_succ_le] at h₂
case intro.intro.intro.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)

case intro.intro.intro.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)
case intro.intro.intro.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)
apply le_antisymm
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
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
rcases hθ with ⟨x, y, ⟨h₁, h₂⟩⟩
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

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
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
by_cases h : x < y
no goals
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
exact ⟨x, y, ⟨h₁, h⟩⟩
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
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
refine' ⟨y, x, ⟨h₁.symm, _⟩⟩
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

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
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
cases' lt_or_eq_of_le (not_lt.mp h) with h' h'
no goals
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
exact h'
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
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
exfalso
no goals
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
exact h₂ h'.symm
no goals
case intro.intro.intro.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)
exact θ.toOrderHom.monotone (le_of_lt (Fin.castSucc_lt_succ z))
case intro.intro.intro.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
case intro.intro.intro.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)
rw [h₁]
no goals
case intro.intro.intro.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
exact θ.toOrderHom.monotone h₂