-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem eq_σ_comp_of_not_injective {n : ℕ} {Δ' : SimplexCategory} (θ : mk (n + 1) ⟶ Δ')
    (hθ : ¬Function.Injective θ.toOrderHom) :
    ∃ (i : Fin (n + 1)) (θ' : mk n ⟶ Δ'), θ = σ i ≫ θ'

Proof state:
case pos
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
x y : Fin (⦋n + 1⦌.len + 1)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : ¬x = y
h : x < y
⊢ ∃ x y, (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y ∧ x < y

Tactic:
exact ⟨x, y, ⟨h₁, h⟩⟩

Result:
no goals

Proof state:
case h.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)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : x < y
⊢ (Hom.toOrderHom θ) (x.castPred ⋯).succ ≤ (Hom.toOrderHom θ) (x.castPred ⋯).castSucc

Tactic:
rw [Fin.castSucc_castPred, h₁]

Result:
case h.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)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : x < y
⊢ (Hom.toOrderHom θ) (x.castPred ⋯).succ ≤ (Hom.toOrderHom θ) y

Proof state:
case h.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)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : x < y
⊢ (Hom.toOrderHom θ) (x.castPred ⋯).succ ≤ (Hom.toOrderHom θ) y

Tactic:
exact θ.toOrderHom.monotone ((Fin.succ_castPred_le_iff _).mpr h₂)

Result:
no goals

Proof state:
case neg.inr
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
x y : Fin (⦋n + 1⦌.len + 1)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : ¬x = y
h : ¬x < y
h' : y = x
⊢ y < x

Tactic:
exfalso

Result:
case neg.inr
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
x y : Fin (⦋n + 1⦌.len + 1)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : ¬x = y
h : ¬x < y
h' : y = x
⊢ False

Proof state:
case neg.inl
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
x y : Fin (⦋n + 1⦌.len + 1)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : ¬x = y
h : ¬x < y
h' : y < x
⊢ y < x

Tactic:
exact h'

Result:
no goals

Proof state:
case neg
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
x y : Fin (⦋n + 1⦌.len + 1)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : ¬x = y
h : ¬x < y
⊢ ∃ x y, (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y ∧ x < y

Tactic:
refine ⟨y, x, ⟨h₁.symm, ?_⟩⟩

Result:
case neg
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
x y : Fin (⦋n + 1⦌.len + 1)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : ¬x = y
h : ¬x < y
⊢ y < x

Proof state:
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 ≫ θ'

Tactic:
rcases hθ₂ with ⟨x, y, ⟨h₁, h₂⟩⟩

Result:
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 ≫ θ'

Proof state:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
hθ : ¬Function.Injective ⇑(Hom.toOrderHom θ)
⊢ ∃ i θ', θ = σ i ≫ θ'

Tactic:
simp only [Function.Injective, exists_prop, not_forall] at hθ

Result:
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
hθ : ∃ x x_1, (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) x_1 ∧ ¬x = x_1
⊢ ∃ i θ', θ = σ i ≫ θ'

Proof state:
case h.hi
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
⊢ (Hom.toOrderHom θ) (x.castPred ⋯).castSucc = (Hom.toOrderHom θ) (x.castPred ⋯).succ

Tactic:
apply le_antisymm

Result:
case h.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)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : x < y
⊢ (Hom.toOrderHom θ) (x.castPred ⋯).castSucc ≤ (Hom.toOrderHom θ) (x.castPred ⋯).succ

case h.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)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : x < y
⊢ (Hom.toOrderHom θ) (x.castPred ⋯).succ ≤ (Hom.toOrderHom θ) (x.castPred ⋯).castSucc

Proof state:
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 ≫ θ'

Tactic:
use x.castPred ((Fin.le_last _).trans_lt' h₂).ne

Result:
case h
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
⊢ ∃ θ', θ = σ (x.castPred ⋯) ≫ θ'

Proof state:
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

Tactic:
rcases hθ with ⟨x, y, ⟨h₁, h₂⟩⟩

Result:
case intro.intro.intro
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
x y : Fin (⦋n + 1⦌.len + 1)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : ¬x = y
⊢ ∃ x y, (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y ∧ x < y

Proof state:
case neg
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
x y : Fin (⦋n + 1⦌.len + 1)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : ¬x = y
h : ¬x < y
⊢ y < x

Tactic:
rcases lt_or_eq_of_le (not_lt.mp h) with h' | h'

Result:
case neg.inl
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
x y : Fin (⦋n + 1⦌.len + 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 (⦋n + 1⦌.len + 1)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : ¬x = y
h : ¬x < y
h' : y = x
⊢ y < x

Proof state:
case neg.inr
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
x y : Fin (⦋n + 1⦌.len + 1)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : ¬x = y
h : ¬x < y
h' : y = x
⊢ False

Tactic:
exact h₂ h'.symm

Result:
no goals

Proof state:
case intro.intro.intro
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
x y : Fin (⦋n + 1⦌.len + 1)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : ¬x = y
⊢ ∃ x y, (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y ∧ x < y

Tactic:
by_cases h : x < y

Result:
case pos
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
x y : Fin (⦋n + 1⦌.len + 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 (⦋n + 1⦌.len + 1)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : ¬x = y
h : ¬x < y
⊢ ∃ x y, (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y ∧ x < y

Proof state:
case h.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)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : x < y
⊢ (Hom.toOrderHom θ) (x.castPred ⋯).castSucc ≤ (Hom.toOrderHom θ) (x.castPred ⋯).succ

Tactic:
exact θ.toOrderHom.monotone (le_of_lt (Fin.castSucc_lt_succ _))

Result:
no goals

Proof state:
case h
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
⊢ ∃ θ', θ = σ (x.castPred ⋯) ≫ θ'

Tactic:
apply eq_σ_comp_of_not_injective'

Result:
case h.hi
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
⊢ (Hom.toOrderHom θ) (x.castPred ⋯).castSucc = (Hom.toOrderHom θ) (x.castPred ⋯).succ