-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem eq_comp_δ_of_not_surjective' {n : ℕ} {Δ : SimplexCategory} (θ : Δ ⟶ mk (n + 1))
    (i : Fin (n + 2)) (hi : ∀ x, θ.toOrderHom x ≠ i) : ∃ θ' : Δ ⟶ mk n, θ = θ' ≫ δ i

Proof state:
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ i
⊢ ∃ θ', θ = θ' ≫ δ i

Tactic:
by_cases h : i < Fin.last (n + 1)

Result:
case pos
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
⊢ ∃ θ', θ = θ' ≫ δ i

case neg
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ i
h : ¬i < Fin.last (n + 1)
⊢ ∃ θ', θ = θ' ≫ δ i

Proof state:
case pos
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (Δ.len + 1)
h' : (Hom.toOrderHom θ) x ≤ i
⊢ (Hom.toOrderHom θ) x = i.succAbove (((Hom.toOrderHom θ) x).castPred ⋯)

Tactic:
rw [Fin.succAbove_of_castSucc_lt i]

Result:
case pos
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (Δ.len + 1)
h' : (Hom.toOrderHom θ) x ≤ i
⊢ (Hom.toOrderHom θ) x = (((Hom.toOrderHom θ) x).castPred ⋯).castSucc

case pos.h
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (Δ.len + 1)
h' : (Hom.toOrderHom θ) x ≤ i
⊢ (((Hom.toOrderHom θ) x).castPred ⋯).castSucc < i

Proof state:
case neg
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (Δ.len + 1)
h' : i < (Hom.toOrderHom θ) x
⊢ i ≤ (((Hom.toOrderHom θ) x).pred ⋯).castSucc

Tactic:
exact Nat.le_sub_one_of_lt (Fin.lt_iff_val_lt_val.mp h')

Result:
no goals

Proof state:
case neg
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (Δ.len + 1)
h' : ¬(Hom.toOrderHom θ) x ≤ i
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom (δ i)) ((Hom.toOrderHom (σ (i.castPred ⋯))) ((Hom.toOrderHom θ) x))

Tactic:
simp only [not_le] at h'

Result:
case neg
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (Δ.len + 1)
h' : i < (Hom.toOrderHom θ) x
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom (δ i)) ((Hom.toOrderHom (σ (i.castPred ⋯))) ((Hom.toOrderHom θ) x))

Proof state:
case pos
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (Δ.len + 1)
h' : (Hom.toOrderHom θ) x ≤ i
⊢ (Hom.toOrderHom θ) x = (((Hom.toOrderHom θ) x).castPred ⋯).castSucc

Tactic:
rw [Fin.castSucc_castPred]

Result:
no goals

Proof state:
case pos
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (Δ.len + 1)
h' : (Hom.toOrderHom θ) x ≤ i
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom (δ i)) ((Hom.toOrderHom (σ (i.castPred ⋯))) ((Hom.toOrderHom θ) x))

Tactic:
simp only [σ, mkHom, Hom.toOrderHom_mk, OrderHom.coe_mk]

Result:
case pos
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (Δ.len + 1)
h' : (Hom.toOrderHom θ) x ≤ i
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom (δ i)) ((i.castPred ⋯).predAbove ((Hom.toOrderHom θ) x))

Proof state:
case neg
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ Fin.last (n + 1)
h : ¬Fin.last (n + 1) < Fin.last (n + 1)
⊢ ∃ θ', θ = θ' ≫ δ (Fin.last (n + 1))

Tactic:
use θ ≫ σ (Fin.last _)

Result:
case h
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ Fin.last (n + 1)
h : ¬Fin.last (n + 1) < Fin.last (n + 1)
⊢ θ = (θ ≫ σ (Fin.last n)) ≫ δ (Fin.last (n + 1))

Proof state:
case h
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ Fin.last (n + 1)
h : ¬Fin.last (n + 1) < Fin.last (n + 1)
⊢ θ = (θ ≫ σ (Fin.last n)) ≫ δ (Fin.last (n + 1))

Tactic:
ext x : 3

Result:
case h.a.h.h
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ Fin.last (n + 1)
h : ¬Fin.last (n + 1) < Fin.last (n + 1)
x : Fin (Δ.len + 1)
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom ((θ ≫ σ (Fin.last n)) ≫ δ (Fin.last (n + 1)))) x

Proof state:
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ Fin.last (n + 1)
h : ¬Fin.last (n + 1) < Fin.last (n + 1)
x : Fin (Δ.len + 1)
⊢ ¬(Hom.toOrderHom θ) x = Fin.last (n + 1)

Tactic:
simpa using hi x

Result:
no goals

Proof state:
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (Δ.len + 1)
h' : i < (Hom.toOrderHom θ) x
⊢ (i.castPred ⋯).castSucc < (Hom.toOrderHom θ) x

Tactic:
rwa [Fin.castSucc_castPred]

Result:
no goals

Proof state:
case pos.h
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (Δ.len + 1)
h' : (Hom.toOrderHom θ) x ≤ i
⊢ (((Hom.toOrderHom θ) x).castPred ⋯).castSucc < i

Tactic:
rw [(hi x).le_iff_lt] at h'

Result:
case pos.h
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (Δ.len + 1)
h'✝ : (Hom.toOrderHom θ) x ≤ i
h' : (Hom.toOrderHom θ) x < i
⊢ (((Hom.toOrderHom θ) x).castPred ⋯).castSucc < i

Proof state:
case h.a.h.h
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ Fin.last (n + 1)
h : ¬Fin.last (n + 1) < Fin.last (n + 1)
x : Fin (Δ.len + 1)
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom ((θ ≫ σ (Fin.last n)) ≫ δ (Fin.last (n + 1)))) x

Tactic:
dsimp [δ, σ]

Result:
case h.a.h.h
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ Fin.last (n + 1)
h : ¬Fin.last (n + 1) < Fin.last (n + 1)
x : Fin (Δ.len + 1)
⊢ (Hom.toOrderHom θ) x = (Fin.last (n + 1)).succAbove ((Fin.last n).predAbove ((Hom.toOrderHom θ) x))

Proof state:
case neg
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ i
h : ¬i < Fin.last (n + 1)
⊢ ∃ θ', θ = θ' ≫ δ i

Tactic:
obtain rfl := le_antisymm (Fin.le_last i) (not_lt.mp h)

Result:
case neg
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ Fin.last (n + 1)
h : ¬Fin.last (n + 1) < Fin.last (n + 1)
⊢ ∃ θ', θ = θ' ≫ δ (Fin.last (n + 1))

Proof state:
case neg
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
x : Fin (Δ.len + 1)
h' : i < (Hom.toOrderHom θ) x
⊢ (Hom.toOrderHom θ) x = (((Hom.toOrderHom θ) x).pred ⋯).succ

Tactic:
rw [Fin.succ_pred]

Result:
no goals