-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L : List ℕ
m₁ m₂ : ℕ
hL : IsAdmissible m₂ L
hk : m₂ + L.length = m₁
j : ℕ
hj : j < m₁ + 1
nil :
  ∀ (m₁ m₂ : ℕ) (hL : IsAdmissible m₂ []) (hk : m₂ + List.length (α := ℕ) [] = m₁) (hj : j < m₁ + 1),
    (↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ [] hk)) :
              (a : Fin ((toSimplexCategory.obj (mk m₁)).len + 1)) → Fin ((toSimplexCategory.obj (mk m₂)).len + 1))
            (⟨j, hj⟩ : Fin ((toSimplexCategory.obj (mk m₁)).len + 1))) :
        ℕ) =
      simplicialEvalσ [] j
cons :
  ∀ (a : ℕ) (L : List ℕ)
    (h_rec :
      ∀ (m₁ m₂ : ℕ) (hL : IsAdmissible m₂ L) (hk : m₂ + L.length = m₁) (hj : j < m₁ + 1),
        (↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L hk)) :
                  (a : Fin ((toSimplexCategory.obj (mk m₁)).len + 1)) → Fin ((toSimplexCategory.obj (mk m₂)).len + 1))
                (⟨j, hj⟩ : Fin ((toSimplexCategory.obj (mk m₁)).len + 1))) :
            ℕ) =
          simplicialEvalσ L j)
    (m₁ m₂ : ℕ) (hL : IsAdmissible m₂ (a :: L)) (hk : m₂ + (a :: L).length = m₁) (hj : j < m₁ + 1),
    (↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ (a :: L) hk)) :
              (a : Fin ((toSimplexCategory.obj (mk m₁)).len + 1)) → Fin ((toSimplexCategory.obj (mk m₂)).len + 1))
            (⟨j, hj⟩ : Fin ((toSimplexCategory.obj (mk m₁)).len + 1))) :
        ℕ) =
      simplicialEvalσ (a :: L) j
⊢ (↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L hk)) :
            (a : Fin ((toSimplexCategory.obj (mk m₁)).len + 1)) → Fin ((toSimplexCategory.obj (mk m₂)).len + 1))
          (⟨j, hj⟩ : Fin ((toSimplexCategory.obj (mk m₁)).len + 1))) :
      ℕ) =
    simplicialEvalσ L j

Tactic:
induction L generalizing m₁ m₂ with
  | nil =>
    obtain rfl : m₁ = m₂ := by grind
    simp [simplicialEvalσ]
  | cons a L h_rec =>
    simp only [List.length_cons] at hk
    subst hk
    set a₀ := hL.head
    have aux (t : Fin (m₂ + 2)) :
        (a₀.predAbove t : ℕ) = if a < ↑t then (t : ℕ) - 1 else ↑t := by
      simp only [Fin.predAbove, a₀]
      split_ifs with h₁ h₂ h₂
      · rfl
      · simp only [Fin.lt_def, Fin.val_castSucc, IsAdmissible.head_val] at h₁; grind
      · simp only [Fin.lt_def, Fin.val_castSucc, IsAdmissible.head_val, not_lt] at h₁; grind
      · rfl
    have := h_rec _ _ hL.of_cons (by grind) hj
    have ha₀ : Fin.ofNat (m₂ + 1) a = a₀ := by ext; simpa [a₀] using hL.head.prop
    simpa only [toSimplexCategory_obj_mk, SimplexCategory.len_mk, standardσ_cons, Functor.map_comp,
      toSimplexCategory_map_σ, SimplexCategory.σ, SimplexCategory.mkHom,
      SimplexCategory.comp_toOrderHom, SimplexCategory.Hom.toOrderHom_mk, OrderHom.comp_coe,
      Function.comp_apply, Fin.predAboveOrderHom_coe, simplicialEvalσ, ha₀, ← this] using aux _

Premises used: SimplexCategory.len_mk, List.length_cons, SimplexCategory.mkHom, SimplexCategoryGenRel.toSimplexCategory_map_σ, SimplexCategory.σ, SimplexCategoryGenRel.toSimplexCategory_obj_mk, SimplexCategoryGenRel.simplicialEvalσ, SimplexCategoryGenRel.standardσ_cons, Fin.predAboveOrderHom_coe, SimplexCategory.Hom.toOrderHom_mk, SimplexCategoryGenRel.IsAdmissible.head, OrderHom.comp_coe, CategoryTheory.Functor.map_comp, Function.comp_apply, SimplexCategory.comp_toOrderHom, rfl