-- 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:
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 = i.succAbove (((Hom.toOrderHom θ) x).pred ⋯)

Tactic:
rw [Fin.succAbove_of_le_castSucc i _]

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 θ) x).pred ⋯).succ

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

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

Tactic:
ext x : 3

Result:
case h.a.h.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)
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom ((θ ≫ σ (i.castPred ⋯)) ≫ δ i)) x

Proof state:
case h.a.h.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)
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom (δ i)) ((Hom.toOrderHom (σ (i.castPred ⋯))) ((Hom.toOrderHom θ) x))

Tactic:
by_cases h' : θ.toOrderHom x ≤ 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 (δ i)) ((Hom.toOrderHom (σ (i.castPred ⋯))) ((Hom.toOrderHom θ) x))

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))

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 = i.succAbove ((i.castPred ⋯).predAbove ((Hom.toOrderHom θ) x))

Tactic:
rw [Fin.predAbove_of_castSucc_lt _ _ (by rwa [Fin.castSucc_castPred])]

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 = i.succAbove (((Hom.toOrderHom θ) x).pred ⋯)

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 =
    (if hi : (Hom.toOrderHom θ) x = Fin.last (n + 1) then Fin.last n else ((Hom.toOrderHom θ) x).castPred hi).castSucc

Tactic:
rw [dif_neg (by simpa using hi x), Fin.castSucc_castPred]

Result:
no goals

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 = (Fin.last (n + 1)).succAbove ((Fin.last n).predAbove ((Hom.toOrderHom θ) x))

Tactic:
simp_rw [Fin.succAbove_last, Fin.predAbove_last_apply]

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 =
    (if hi : (Hom.toOrderHom θ) x = Fin.last (n + 1) then Fin.last n else ((Hom.toOrderHom θ) x).castPred hi).castSucc

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' : (Hom.toOrderHom θ) x ≤ i
⊢ (Hom.toOrderHom θ) x ≤ (i.castPred ⋯).castSucc

Tactic:
rwa [Fin.castSucc_castPred]

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' : i < (Hom.toOrderHom θ) x
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom (δ i)) ((Hom.toOrderHom (σ (i.castPred ⋯))) ((Hom.toOrderHom θ) x))

Tactic:
dsimp [σ, δ]

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 = i.succAbove ((i.castPred ⋯).predAbove ((Hom.toOrderHom θ) x))

Proof state:
case h.a.h.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)
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom ((θ ≫ σ (i.castPred ⋯)) ≫ δ i)) x

Tactic:
simp only [len_mk, Category.assoc, comp_toOrderHom, OrderHom.comp_coe, Function.comp_apply]

Result:
case h.a.h.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)
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom (δ i)) ((Hom.toOrderHom (σ (i.castPred ⋯))) ((Hom.toOrderHom θ) x))

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
h' : (Hom.toOrderHom θ) x < i
⊢ (((Hom.toOrderHom θ) x).castPred ⋯).castSucc < i

Tactic:
exact h'

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 θ) x).castPred ⋯)

Tactic:
dsimp [δ]

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 = i.succAbove (((Hom.toOrderHom θ) x).castPred ⋯)

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)
⊢ ∃ θ', θ = θ' ≫ δ i

Tactic:
use θ ≫ σ (Fin.castPred i h.ne)

Result:
case h
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ i
h : i < Fin.last (n + 1)
⊢ θ = (θ ≫ σ (i.castPred ⋯)) ≫ δ 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 = (Hom.toOrderHom (δ i)) ((i.castPred ⋯).predAbove ((Hom.toOrderHom θ) x))

Tactic:
rw [Fin.predAbove_of_le_castSucc _ _ (by rwa [Fin.castSucc_castPred])]

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)) (((Hom.toOrderHom θ) x).castPred ⋯)