awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L : List ℕ
j m₁ : ℕ
hj : j < m₁ + 1
hL : IsAdmissible m₁ []
hk : m₁ + List.length (α := ℕ) [] = m₁
⊢ (↑((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

Tactic:
simp [simplicialEvalσ]

Premises used: SimplexCategoryGenRel.simplicialEvalσ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L_1 : List ℕ
j 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₂ + (L.length + 1) = m₁
hj : j < m₁ + 1
cons :
  ∀ (hj : j < m₂ + (L.length + 1) + 1),
    (↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ (a :: L) ⋯)) :
              (a : Fin ((toSimplexCategory.obj (mk (m₂ + (L.length + 1)))).len + 1)) →
                Fin ((toSimplexCategory.obj (mk m₂)).len + 1))
            (⟨j, hj⟩ : Fin ((toSimplexCategory.obj (mk (m₂ + (L.length + 1)))).len + 1))) :
        ℕ) =
      simplicialEvalσ (a :: L) j
⊢ (↑((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

Tactic:
subst hk
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L_1 : List ℕ
j 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₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
t : Fin (m₂ + 2)
simp :
  (↑(if h : hL.head.castSucc < t then t.pred ⋯ else t.castPred ⋯) : ℕ) = if a < (↑t : ℕ) then (↑t : ℕ) - 1 else (↑t : ℕ)
⊢ (↑(a₀.predAbove t) : ℕ) = if a < (↑t : ℕ) then (↑t : ℕ) - 1 else (↑t : ℕ)

Tactic:
simp only [Fin.predAbove, a₀]

Premises used: Fin.predAbove
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L_1 : List ℕ
j 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₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
t : Fin (m₂ + 2)
pos : ∀ (h₁ : hL.head.castSucc < t) (h₂ : a < (↑t : ℕ)), (↑(t.pred ⋯) : ℕ) = (↑t : ℕ) - 1
neg : ∀ (h₁ : hL.head.castSucc < t) (h₂ : ¬a < (↑t : ℕ)), (↑(t.pred ⋯) : ℕ) = (↑t : ℕ)
pos₁ : ∀ (h₁ : ¬hL.head.castSucc < t) (h₂ : a < (↑t : ℕ)), (↑(t.castPred ⋯) : ℕ) = (↑t : ℕ) - 1
neg₁ : ∀ (h₁ : ¬hL.head.castSucc < t) (h₂ : ¬a < (↑t : ℕ)), (↑(t.castPred ⋯) : ℕ) = (↑t : ℕ)
⊢ (↑(if h : hL.head.castSucc < t then t.pred ⋯ else t.castPred ⋯) : ℕ) = if a < (↑t : ℕ) then (↑t : ℕ) - 1 else (↑t : ℕ)

Tactic:
split_ifs with h₁ h₂ h₂
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L_1 : List ℕ
j 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₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
t : Fin (m₂ + 2)
h₁ : hL.head.castSucc < t
h₂ : a < (↑t : ℕ)
⊢ (↑(t.pred ⋯) : ℕ) = (↑t : ℕ) - 1

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L_1 : List ℕ
j 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₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
t : Fin (m₂ + 2)
h₁ : hL.head.castSucc < t
h₂ : ¬a < (↑t : ℕ)
⊢ a < (↑t : ℕ)

Tactic:
simp only [Fin.lt_def, Fin.val_castSucc, IsAdmissible.head_val] at h₁

Premises used: SimplexCategoryGenRel.IsAdmissible.head_val, Fin.lt_def, Fin.val_castSucc
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L_1 : List ℕ
j 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₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
t : Fin (m₂ + 2)
h₁_1 : hL.head.castSucc < t
h₂ : ¬a < (↑t : ℕ)
h₁ : a < (↑t : ℕ)
⊢ (↑(t.pred ⋯) : ℕ) = (↑t : ℕ)

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L_1 : List ℕ
j 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₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
t : Fin (m₂ + 2)
h₁ : ¬hL.head.castSucc < t
h₂ : a < (↑t : ℕ)
⊢ (↑t : ℕ) ≤ a

Tactic:
simp only [Fin.lt_def, Fin.val_castSucc, IsAdmissible.head_val, not_lt] at h₁

Premises used: SimplexCategoryGenRel.IsAdmissible.head_val, Fin.lt_def, not_lt, Fin.val_castSucc
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L_1 : List ℕ
j 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₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
t : Fin (m₂ + 2)
h₁_1 : ¬hL.head.castSucc < t
h₂ : a < (↑t : ℕ)
h₁ : (↑t : ℕ) ≤ a
⊢ (↑(t.castPred ⋯) : ℕ) = (↑t : ℕ) - 1

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L_1 : List ℕ
j 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₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
t : Fin (m₂ + 2)
h₁ : ¬hL.head.castSucc < t
h₂ : ¬a < (↑t : ℕ)
⊢ (↑(t.castPred ⋯) : ℕ) = (↑t : ℕ)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L_1 : List ℕ
j 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₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
⊢ ∀ (t : Fin (m₂ + 2)), (↑(a₀.predAbove t) : ℕ) = if a < (↑t : ℕ) then (↑t : ℕ) - 1 else (↑t : ℕ)

Tactic:
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
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L_1 : List ℕ
j 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₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
aux : ∀ (t : Fin (m₂ + 2)), (↑(a₀.predAbove t) : ℕ) = if a < (↑t : ℕ) then (↑t : ℕ) - 1 else (↑t : ℕ)
⊢ m₂ + 1 + L.length = m₂ + (L.length + 1)

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L_1 : List ℕ
j 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₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
aux : ∀ (t : Fin (m₂ + 2)), (↑(a₀.predAbove t) : ℕ) = if a < (↑t : ℕ) then (↑t : ℕ) - 1 else (↑t : ℕ)
⊢ (↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L ⋯)) :
            (a : Fin ((toSimplexCategory.obj (mk (m₂ + (L.length + 1)))).len + 1)) →
              Fin ((toSimplexCategory.obj (mk (m₂ + 1))).len + 1))
          (⟨j, hj⟩ : Fin ((toSimplexCategory.obj (mk (m₂ + (L.length + 1)))).len + 1))) :
      ℕ) =
    simplicialEvalσ L j

Tactic:
have := h_rec _ _ hL.of_cons (by grind) hj
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L_1 : List ℕ
j 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₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
aux : ∀ (t : Fin (m₂ + 2)), (↑(a₀.predAbove t) : ℕ) = if a < (↑t : ℕ) then (↑t : ℕ) - 1 else (↑t : ℕ)
this :
  (↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L ⋯)) :
            (a : Fin ((toSimplexCategory.obj (mk (m₂ + (L.length + 1)))).len + 1)) →
              Fin ((toSimplexCategory.obj (mk (m₂ + 1))).len + 1))
          (⟨j, hj⟩ : Fin ((toSimplexCategory.obj (mk (m₂ + (L.length + 1)))).len + 1))) :
      ℕ) =
    simplicialEvalσ L j
h : (↑(Fin.ofNat (m₂ + 1) a) : ℕ) = (↑a₀ : ℕ)
⊢ Fin.ofNat (m₂ + 1) a = a₀

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L_1 : List ℕ
j 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₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
aux : ∀ (t : Fin (m₂ + 2)), (↑(a₀.predAbove t) : ℕ) = if a < (↑t : ℕ) then (↑t : ℕ) - 1 else (↑t : ℕ)
this :
  (↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L ⋯)) :
            (a : Fin ((toSimplexCategory.obj (mk (m₂ + (L.length + 1)))).len + 1)) →
              Fin ((toSimplexCategory.obj (mk (m₂ + 1))).len + 1))
          (⟨j, hj⟩ : Fin ((toSimplexCategory.obj (mk (m₂ + (L.length + 1)))).len + 1))) :
      ℕ) =
    simplicialEvalσ L j
⊢ (↑(Fin.ofNat (m₂ + 1) a) : ℕ) = (↑a₀ : ℕ)

Tactic:
simpa [a₀] using hL.head.prop

Premises used: Fin.prop, SimplexCategoryGenRel.IsAdmissible.head
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L_1 : List ℕ
j 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₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
aux : ∀ (t : Fin (m₂ + 2)), (↑(a₀.predAbove t) : ℕ) = if a < (↑t : ℕ) then (↑t : ℕ) - 1 else (↑t : ℕ)
this :
  (↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L ⋯)) :
            (a : Fin ((toSimplexCategory.obj (mk (m₂ + (L.length + 1)))).len + 1)) →
              Fin ((toSimplexCategory.obj (mk (m₂ + 1))).len + 1))
          (⟨j, hj⟩ : Fin ((toSimplexCategory.obj (mk (m₂ + (L.length + 1)))).len + 1))) :
      ℕ) =
    simplicialEvalσ L j
⊢ Fin.ofNat (m₂ + 1) a = a₀

Tactic:
have ha₀ : Fin.ofNat (m₂ + 1) a = a₀ := by ext; simpa [a₀] using hL.head.prop
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L_1 : List ℕ
j 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₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
aux : ∀ (t : Fin (m₂ + 2)), (↑(a₀.predAbove t) : ℕ) = if a < (↑t : ℕ) then (↑t : ℕ) - 1 else (↑t : ℕ)
this :
  (↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L ⋯)) :
            (a : Fin ((toSimplexCategory.obj (mk (m₂ + (L.length + 1)))).len + 1)) →
              Fin ((toSimplexCategory.obj (mk (m₂ + 1))).len + 1))
          (⟨j, hj⟩ : Fin ((toSimplexCategory.obj (mk (m₂ + (L.length + 1)))).len + 1))) :
      ℕ) =
    simplicialEvalσ L j
ha₀ : Fin.ofNat (m₂ + 1) a = a₀
⊢ (↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ (a :: L) ⋯)) :
            (a : Fin ((toSimplexCategory.obj (mk (m₂ + (L.length + 1)))).len + 1)) →
              Fin ((toSimplexCategory.obj (mk m₂)).len + 1))
          (⟨j, hj⟩ : Fin ((toSimplexCategory.obj (mk (m₂ + (L.length + 1)))).len + 1))) :
      ℕ) =
    simplicialEvalσ (a :: L) j

Tactic:
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, SimplexCategory.mkHom, SimplexCategoryGenRel.toSimplexCategory_map_σ, SimplexCategory.σ, SimplexCategoryGenRel.toSimplexCategory_obj_mk, SimplexCategoryGenRel.simplicialEvalσ, SimplexCategoryGenRel.standardσ_cons, Fin.predAboveOrderHom_coe, SimplexCategory.Hom.toOrderHom_mk, OrderHom.comp_coe, CategoryTheory.Functor.map_comp, Function.comp_apply, SimplexCategory.comp_toOrderHom
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m : ℕ
L : List ℕ
hL : IsAdmissible (m + 1) L
j : ℕ
hj : j < m + 1
m₁ : ℕ
hm₁ : m + L.length + 1 = m₁
⊢ m + (simplicialInsert j L).length = m₁

Tactic:
simpa only [simplicialInsert_length, add_assoc]

Premises used: SimplexCategoryGenRel.simplicialInsert_length, add_assoc
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m : ℕ
L : List ℕ
hL : IsAdmissible (m + 1) L
j : ℕ
hj : j < m + 1
m₁ : ℕ
hm₁ : m + L.length + 1 = m₁
⊢ m + 1 + L.length = m₁

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m₁ m : ℕ
hL : IsAdmissible (m + 1) []
j : ℕ
hj : j < m + 1
hm₁ : m + List.length (α := ℕ) [] + 1 = m₁
⊢ standardσ (simplicialInsert j []) ⋯ = standardσ [] ⋯ ≫ σ (Fin.ofNat (m + 1) j)

Tactic:
simp [standardσ, simplicialInsert]

Premises used: SimplexCategoryGenRel.simplicialInsert, SimplexCategoryGenRel.standardσ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ} (hL : IsAdmissible (m + 1) L) (j : ℕ) (hj : j < m + 1) (hm₁ : m + L.length + 1 = m₁),
    standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
pos : ∀ (h : j < a), standardσ (j :: a :: L) ⋯ = standardσ (a :: L) ⋯ ≫ σ (Fin.ofNat (m + 1) j)
neg : ∀ (h : ¬j < a), standardσ (a :: simplicialInsert (j + 1) L) ⋯ = standardσ (a :: L) ⋯ ≫ σ (Fin.ofNat (m + 1) j)
⊢ standardσ (if j < a then j :: a :: L else a :: simplicialInsert (j + 1) L) ⋯ =
    standardσ (a :: L) ⋯ ≫ σ (Fin.ofNat (m + 1) j)

Tactic:
split_ifs
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ} (hL : IsAdmissible (m + 1) L) (j : ℕ) (hj : j < m + 1) (hm₁ : m + L.length + 1 = m₁),
    standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
h : j < a
⊢ standardσ (j :: a :: L) ⋯ = standardσ (a :: L) ⋯ ≫ σ (Fin.ofNat (m + 1) j)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ} (hL : IsAdmissible (m + 1) L) (j : ℕ) (hj : j < m + 1) (hm₁ : m + L.length + 1 = m₁),
    standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
h : ¬j < a
⊢ ∀ (j k : ℕ) (h : j < k + 1), (↑(Fin.ofNat (k + 1) j) : ℕ) = j

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ} (hL : IsAdmissible (m + 1) L) (j : ℕ) (hj : j < m + 1) (hm₁ : m + L.length + 1 = m₁),
    standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
h : ¬j < a
⊢ ∀ (j k : ℕ) (h : j < k + 1), (↑(Fin.ofNat (k + 1) j) : ℕ) = j

Tactic:
have : ∀ (j k : ℕ) (h : j < (k + 1)), Fin.ofNat (k + 1) j = j := by simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ} (hL : IsAdmissible (m + 1) L) (j : ℕ) (hj : j < m + 1) (hm₁ : m + L.length + 1 = m₁),
    standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
h : ¬j < a
this : ∀ (j k : ℕ) (h : j < k + 1), (↑(Fin.ofNat (k + 1) j) : ℕ) = j
⊢ a < m + 2

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ} (hL : IsAdmissible (m + 1) L) (j : ℕ) (hj : j < m + 1) (hm₁ : m + L.length + 1 = m₁),
    standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
h : ¬j < a
this : ∀ (j k : ℕ) (h : j < k + 1), (↑(Fin.ofNat (k + 1) j) : ℕ) = j
⊢ a < m + 2

Tactic:
have : a < m + 2 := by grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ} (hL : IsAdmissible (m + 1) L) (j : ℕ) (hj : j < m + 1) (hm₁ : m + L.length + 1 = m₁),
    standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
h : ¬j < a
this_1 : ∀ (j k : ℕ) (h : j < k + 1), (↑(Fin.ofNat (k + 1) j) : ℕ) = j
this : a < m + 2
⊢ a < m + 1

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ} (hL : IsAdmissible (m + 1) L) (j : ℕ) (hj : j < m + 1) (hm₁ : m + L.length + 1 = m₁),
    standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
h : ¬j < a
this_1 : ∀ (j k : ℕ) (h : j < k + 1), (↑(Fin.ofNat (k + 1) j) : ℕ) = j
this : a < m + 2
⊢ j < m + 1

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ} (hL : IsAdmissible (m + 1) L) (j : ℕ) (hj : j < m + 1) (hm₁ : m + L.length + 1 = m₁),
    standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
h : ¬j < a
this_1 : ∀ (j k : ℕ) (h : j < k + 1), (↑(Fin.ofNat (k + 1) j) : ℕ) = j
this : a < m + 2
⊢ a ≤ j

Tactic:
grind