awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
L : List ℕ
j 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
have nil : ∀ (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: obtain rfl : m₁ = m₂ := by grind
Cleared hypotheses: m₂, hL, hk
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
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
⊢ (↑((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
have cons : ∀ (hj : j < m₂ + (L.length + 1) + 1),
  (↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ (a :: L) sorry)) :
            (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: subst hk
Cleared hypotheses: m₁, hk, hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
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 : ℕ)
have simp : (↑(if h : hL.head.castSucc < t then t.pred sorry else t.castPred sorry) : ℕ) = if a < (↑t : ℕ) then (↑t : ℕ) - 1 else (↑t : ℕ)
Tactic: simp only [Fin.predAbove, a₀]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
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)
⊢ (↑(if h : hL.head.castSucc < t then t.pred ⋯ else t.castPred ⋯) : ℕ) = if a < (↑t : ℕ) then (↑t : ℕ) - 1 else (↑t : ℕ)
have pos : ∀ (h₁ : hL.head.castSucc < t) (h₂ : a < (↑t : ℕ)), (↑(t.pred sorry) : ℕ) = (↑t : ℕ) - 1
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
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
⊢ (↑(if h : hL.head.castSucc < t then t.pred ⋯ else t.castPred ⋯) : ℕ) = if a < (↑t : ℕ) then (↑t : ℕ) - 1 else (↑t : ℕ)
have neg : ∀ (h₁ : hL.head.castSucc < t) (h₂ : ¬a < (↑t : ℕ)), (↑(t.pred sorry) : ℕ) = (↑t : ℕ)
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
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 : ℕ)
⊢ (↑(if h : hL.head.castSucc < t then t.pred ⋯ else t.castPred ⋯) : ℕ) = if a < (↑t : ℕ) then (↑t : ℕ) - 1 else (↑t : ℕ)
have pos₁ : ∀ (h₁ : ¬hL.head.castSucc < t) (h₂ : a < (↑t : ℕ)), (↑(t.castPred sorry) : ℕ) = (↑t : ℕ) - 1
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
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
⊢ (↑(if h : hL.head.castSucc < t then t.pred ⋯ else t.castPred ⋯) : ℕ) = if a < (↑t : ℕ) then (↑t : ℕ) - 1 else (↑t : ℕ)
have neg₁ : ∀ (h₁ : ¬hL.head.castSucc < t) (h₂ : ¬a < (↑t : ℕ)), (↑(t.castPred sorry) : ℕ) = (↑t : ℕ)
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (hypothesis)
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 : ℕ)
have h₃ : a < (↑t : ℕ)
Tactic: simp only [Fin.lt_def, Fin.val_castSucc, IsAdmissible.head_val] at h₁
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (hypothesis)
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 : ℕ) - 1
have h₃ : (↑t : ℕ) ≤ a
Tactic: simp only [Fin.lt_def, Fin.val_castSucc, IsAdmissible.head_val, not_lt] at h₁
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (hypothesis)
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
⊢ (↑((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
have aux : ∀ (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
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (hypothesis)
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σ (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
have this : (↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L sorry)) :
          (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
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
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₀
have h : (↑(Fin.ofNat (m₂ + 1) a) : ℕ) = (↑a₀ : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (hypothesis)
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
⊢ (↑((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
have ha₀ : Fin.ofNat (m₂ + 1) a = a₀
Tactic: have ha₀ : Fin.ofNat (m₂ + 1) a = a₀ := by ext; simpa [a₀] using hL.head.prop
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
L : List ℕ
m₁ m₂ : ℕ
hL : IsAdmissible m₂ L
hk : m₂ + L.length = m₁
j : ℕ
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
have 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
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 _
Cleared hypotheses: m₁, m₂, hL, hk, hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
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
⊢ (↑((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
have 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
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 _
Cleared hypotheses: m₁, m₂, hL, hk, hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
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₁
⊢ standardσ (if j < a then j :: a :: L else a :: simplicialInsert (j + 1) L) ⋯ =
    standardσ (a :: L) ⋯ ≫ σ (Fin.ofNat (m + 1) j)
have pos : ∀ (h : j < a), standardσ (j :: a :: L) sorry = standardσ (a :: L) sorry ≫ σ (Fin.ofNat (m + 1) j)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
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)
⊢ standardσ (if j < a then j :: a :: L else a :: simplicialInsert (j + 1) L) ⋯ =
    standardσ (a :: L) ⋯ ≫ σ (Fin.ofNat (m + 1) j)
have neg : ∀ (h : ¬j < a), standardσ (a :: simplicialInsert (j + 1) L) sorry = standardσ (a :: L) sorry ≫ σ (Fin.ofNat (m + 1) j)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (hypothesis)
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σ (a :: simplicialInsert (j + 1) L) ⋯ = standardσ (a :: L) ⋯ ≫ σ (Fin.ofNat (m + 1) j)
have this : ∀ (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
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (hypothesis)
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
⊢ standardσ (a :: simplicialInsert (j + 1) L) ⋯ = standardσ (a :: L) ⋯ ≫ σ (Fin.ofNat (m + 1) j)
have this₁ : a < m + 2
Tactic: have : a < m + 2 := by grind
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
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
⊢ Eq (α := mk (m + 1 + 1) ⟶ mk m) (σ (Fin.ofNat (m + 2) a) ≫ σ (Fin.ofNat (m + 1) j))
    (σ (Fin.ofNat (m + 1 + 1) (j + 1)) ≫ σ (Fin.ofNat (m + 1) a))
have h : (↑(Fin.ofNat (m + 2) a) : ℕ) = a
Tactic: convert! σ_comp_σ_nat (n := m) a j (by grind) (by grind) (by grind)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
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_1 : ¬j < a
this_1 : ∀ (j k : ℕ) (h : j < k + 1), (↑(Fin.ofNat (k + 1) j) : ℕ) = j
this : a < m + 2
h : (↑(Fin.ofNat (m + 2) a) : ℕ) = a
⊢ Eq (α := mk (m + 1 + 1) ⟶ mk m) (σ (Fin.ofNat (m + 2) a) ≫ σ (Fin.ofNat (m + 1) j))
    (σ (Fin.ofNat (m + 1 + 1) (j + 1)) ≫ σ (Fin.ofNat (m + 1) a))
have h₁ : (↑(Fin.ofNat (m + 1) j) : ℕ) = j
Tactic: convert! σ_comp_σ_nat (n := m) a j (by grind) (by grind) (by grind)