awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h₁ : (↑(Fin.ofNat (m + 1) j) : ℕ) = j
⊢ 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 + 1) (j + 1)) : ℕ) = j + 1
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
h₁ : (↑(Fin.ofNat (m + 1) j) : ℕ) = j
h₂ : (↑(Fin.ofNat (m + 1 + 1) (j + 1)) : ℕ) = j + 1
⊢ 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) 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 (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_1 : ∀ (j k : ℕ) (h : j < k + 1), (↑(Fin.ofNat (k + 1) j) : ℕ) = j
this : a < m + 2
⊢ standardσ (a :: simplicialInsert (j + 1) L) ⋯ = standardσ (a :: L) ⋯ ≫ σ (Fin.ofNat (m + 1) j)
have this₁ : 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))
Tactic: have : σ (Fin.ofNat (m + 2) a) ≫ σ (.ofNat _ j) = σ (.ofNat _ (j + 1)) ≫ σ (.ofNat _ a) := by
        convert! σ_comp_σ_nat (n := m) a j (by grind) (by grind) (by grind) <;> grind
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
m : ℕ
L : List ℕ
hL : IsAdmissible (m + 1) L
j : ℕ
hj : j < m + 1
m₁ : ℕ
hm₁ : m + L.length + 1 = m₁
⊢ standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
have nil : ∀ {m : ℕ} (hL : IsAdmissible (m + 1) []) (j : ℕ) (hj : j < m + 1) (hm₁ : m + List.length (α := ℕ) [] + 1 = m₁),
  standardσ (simplicialInsert j []) sorry = standardσ [] sorry ≫ σ (Fin.ofNat (m + 1) j)
Tactic: induction L generalizing m j with
  | nil => simp [standardσ, simplicialInsert]
  | cons a L h_rec =>
    simp only [simplicialInsert]
    split_ifs
    · simp
    · have : ∀ (j k : ℕ) (h : j < (k + 1)), Fin.ofNat (k + 1) j = j := by simp -- helps grind below
      have : a < m + 2 := by grind -- helps grind below
      have : σ (Fin.ofNat (m + 2) a) ≫ σ (.ofNat _ j) = σ (.ofNat _ (j + 1)) ≫ σ (.ofNat _ a) := by
        convert! σ_comp_σ_nat (n := m) a j (by grind) (by grind) (by grind) <;> grind
      grind [standardσ_cons]
Cleared hypotheses: m, L, hL, j, hj, hm₁
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
m : ℕ
L : List ℕ
hL : IsAdmissible (m + 1) L
j : ℕ
hj : j < m + 1
m₁ : ℕ
hm₁ : m + L.length + 1 = m₁
nil :
  ∀ {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)
⊢ standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
have cons : ∀ (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) sorry = standardσ L sorry ≫ σ (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σ (simplicialInsert j (a :: L)) sorry = standardσ (a :: L) sorry ≫ σ (Fin.ofNat (m + 1) j)
Tactic: induction L generalizing m j with
  | nil => simp [standardσ, simplicialInsert]
  | cons a L h_rec =>
    simp only [simplicialInsert]
    split_ifs
    · simp
    · have : ∀ (j k : ℕ) (h : j < (k + 1)), Fin.ofNat (k + 1) j = j := by simp -- helps grind below
      have : a < m + 2 := by grind -- helps grind below
      have : σ (Fin.ofNat (m + 2) a) ≫ σ (.ofNat _ j) = σ (.ofNat _ (j + 1)) ≫ σ (.ofNat _ a) := by
        convert! σ_comp_σ_nat (n := m) a j (by grind) (by grind) (by grind) <;> grind
      grind [standardσ_cons]
Cleared hypotheses: m, L, hL, j, hj, hm₁
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
m_1 : ℕ
L_1 : List ℕ
x y : SimplexCategoryGenRel
f : x ⟶ y
hf : P_σ f
L : List ℕ
m b : ℕ
h₁ : mk m = y
h₂ : x = mk (m + b)
h : L.length = b
⊢ y.1 + L.length = x.1
have rw : (mk m).1 + b = (mk (m + b)).1
Tactic: rw [h, h₁.symm, h₂]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
n : SimplexCategoryGenRel
⊢ ∃ (L : List ℕ) (m : ℕ) (b : ℕ) (h₁ : mk m = n) (h₂ : n = mk (m + b)) (h : L.length = b),
    IsAdmissible m L ∧ 𝟙 n = standardσ L ⋯
have right : Eq (α := n ⟶ n) (𝟙 n) (standardσ [] sorry)
Tactic: use [], n.len, 0, rfl, rfl, rfl, IsAdmissible.nil _
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
m : ℕ
k : Fin (m + 1)
⊢ ∃ (L : List ℕ) (m_1 : ℕ) (b : ℕ) (h₁ : mk m_1 = mk m) (h₂ : mk (m + 1) = mk (m_1 + b)) (h : L.length = b),
    IsAdmissible m_1 L ∧ σ k = standardσ L ⋯
have right : σ k = standardσ [(↑k : ℕ)] sorry
Tactic: use [k.val], m, 1, rfl, rfl, rfl, IsAdmissible.singleton k.is_le
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
x y : SimplexCategoryGenRel
f_1 : x ⟶ y
x_1 y_1 : SimplexCategoryGenRel
f : x_1 ⟶ y_1
hf : degeneracies f
⊢ ∃ (L : List ℕ) (m : ℕ) (b : ℕ) (h₁ : mk m = y_1) (h₂ : x_1 = mk (m + b)) (h : L.length = b),
    IsAdmissible m L ∧ f = standardσ L ⋯
have of : ∀ {m : ℕ} (k : Fin (m + 1)),
  ∃ (L : List ℕ) (m_1 : ℕ) (b : ℕ) (h₁ : mk m_1 = mk m) (h₂ : mk (m + 1) = mk (m_1 + b)) (h : L.length = b),
    IsAdmissible m_1 L ∧ σ k = standardσ L sorry
Tactic: cases hf with | @σ m k =>
    use [k.val], m, 1, rfl, rfl, rfl, IsAdmissible.singleton k.is_le
    simp [standardσ]
Cleared hypotheses: x_1, y_1, f, hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
x_1 : SimplexCategoryGenRel
m : ℕ
k : Fin (m + 1)
g : x_1 ⟶ mk (m + 1)
hg : degeneracies.multiplicativeClosure g
h_rec :
  ∃ (L : List ℕ) (m_1 : ℕ) (b : ℕ) (h₁ : mk m_1 = mk (m + 1)) (h₂ : x_1 = mk (m_1 + b)) (h : L.length = b),
    IsAdmissible m_1 L ∧ g = standardσ L ⋯
⊢ ∃ (L : List ℕ) (m_1 : ℕ) (b : ℕ) (h₁ : mk m_1 = mk m) (h₂ : x_1 = mk (m_1 + b)) (h : L.length = b),
    IsAdmissible m_1 L ∧ g ≫ σ k = standardσ L ⋯
have comp_of : ∀ (L₁ : List ℕ) (m₁ b₁ : ℕ) (h₁' : mk m₁ = mk (m + 1)) (g : mk (m₁ + b₁) ⟶ mk (m + 1))
  (hg : degeneracies.multiplicativeClosure g) (h' : L₁.length = b₁) (hL₁ : IsAdmissible m₁ L₁)
  (e₁ : g = standardσ L₁ sorry),
  ∃ (L : List ℕ) (m_1 : ℕ) (b : ℕ) (h₁ : mk m_1 = mk m) (h₂ : mk (m₁ + b₁) = mk (m_1 + b)) (h : L.length = b),
    IsAdmissible m_1 L ∧ g ≫ σ k = standardσ L sorry
Tactic: obtain ⟨L₁, m₁, b₁, h₁', rfl, h', hL₁, e₁⟩ := h_rec
Cleared hypotheses: x_1, g, hg, h_rec
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
m : ℕ
k : Fin (m + 1)
L₁ : List ℕ
m₁ b₁ : ℕ
h₁' : mk m₁ = mk (m + 1)
g : mk (m₁ + b₁) ⟶ mk (m + 1)
hg : degeneracies.multiplicativeClosure g
h' : L₁.length = b₁
hL₁ : IsAdmissible m₁ L₁
e₁ : g = standardσ L₁ ⋯
⊢ ∃ (L : List ℕ) (m_1 : ℕ) (b : ℕ) (h₁ : mk m_1 = mk m) (h₂ : mk (m₁ + b₁) = mk (m_1 + b)) (h : L.length = b),
    IsAdmissible m_1 L ∧ g ≫ σ k = standardσ L ⋯
have comp_of : ∀ (h₁' : mk (m + 1) = mk (m + 1)) (g : mk (m + 1 + b₁) ⟶ mk (m + 1)) (hg : degeneracies.multiplicativeClosure g)
  (hL₁ : IsAdmissible (m + 1) L₁) (e₁ : g = standardσ L₁ sorry),
  ∃ (L : List ℕ) (m_1 : ℕ) (b : ℕ) (h₁ : mk m_1 = mk m) (h₂ : mk (m + 1 + b₁) = mk (m_1 + b)) (h : L.length = b),
    IsAdmissible m_1 L ∧ g ≫ σ k = standardσ L sorry
Tactic: obtain rfl : m₁ = m + 1 := congrArg (fun x ↦ x.len) h₁'
Cleared hypotheses: m₁, h₁', g, hg, hL₁, e₁
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
m : ℕ
k : Fin (m + 1)
L₁ : List ℕ
b₁ : ℕ
h' : L₁.length = b₁
h₁' : mk (m + 1) = mk (m + 1)
g : mk (m + 1 + b₁) ⟶ mk (m + 1)
hg : degeneracies.multiplicativeClosure g
hL₁ : IsAdmissible (m + 1) L₁
e₁ : g = standardσ L₁ ⋯
⊢ ∃ (L : List ℕ) (m_1 : ℕ) (b : ℕ) (h₁ : mk m_1 = mk m) (h₂ : mk (m + 1 + b₁) = mk (m_1 + b)) (h : L.length = b),
    IsAdmissible m_1 L ∧ g ≫ σ k = standardσ L ⋯
have right : g ≫ σ k = standardσ (simplicialInsert (↑k : ℕ) L₁) sorry
Tactic: use simplicialInsert k.val L₁, m, b₁ + 1, rfl, by grind, by grind, by grind
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
m : ℕ
k : Fin (m + 1)
L₁ : List ℕ
b₁ : ℕ
h' : L₁.length = b₁
h₁' : mk (m + 1) = mk (m + 1)
g : mk (m + 1 + b₁) ⟶ mk (m + 1)
hg : degeneracies.multiplicativeClosure g
hL₁ : IsAdmissible (m + 1) L₁
e₁ : g = standardσ L₁ ⋯
⊢ g ≫ σ k = standardσ (simplicialInsert (↑k : ℕ) L₁) ⋯
have right : ∀ (hg : degeneracies.multiplicativeClosure (standardσ L₁ sorry)),
  standardσ L₁ sorry ≫ σ k = standardσ (simplicialInsert (↑k : ℕ) L₁) sorry
Tactic: subst_vars
Cleared hypotheses: b₁, h', g, hg, e₁
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (hypothesis)
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
m : ℕ
k : Fin (m + 1)
L₁ : List ℕ
h₁' : mk (m + 1) = mk (m + 1)
hL₁ : IsAdmissible (m + 1) L₁
hg : degeneracies.multiplicativeClosure (standardσ L₁ ⋯)
⊢ standardσ L₁ ⋯ ≫ σ k = standardσ (simplicialInsert (↑k : ℕ) L₁) ⋯
have this : Eq (α := mk (m + 1 + L₁.length) ⟶ mk m) (standardσ [] sorry ≫ standardσ L₁ sorry ≫ σ (Fin.ofNat (m + 1) (↑k : ℕ)))
  (standardσ [] sorry ≫ standardσ (simplicialInsert (↑k : ℕ) L₁) sorry)
Tactic: have := standardσ (m₁ := m + 1 + L₁.length) [] (by grind) ≫=
      (standardσ_simplicialInsert L₁ hL₁ k k.prop _ rfl).symm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
x_1 j x' : SimplexCategoryGenRel
g : x_1 ⟶ j
g' : j ⟶ x'
hg : degeneracies.multiplicativeClosure g
hg' : degeneracies g'
h_rec :
  ∃ (L : List ℕ) (m : ℕ) (b : ℕ) (h₁ : mk m = j) (h₂ : x_1 = mk (m + b)) (h : L.length = b),
    IsAdmissible m L ∧ g = standardσ L ⋯
⊢ ∃ (L : List ℕ) (m : ℕ) (b : ℕ) (h₁ : mk m = x') (h₂ : x_1 = mk (m + b)) (h : L.length = b),
    IsAdmissible m L ∧ g ≫ g' = standardσ L ⋯
have comp_of : ∀ {m : ℕ} (k : Fin (m + 1)) (g : x_1 ⟶ mk (m + 1)) (hg : degeneracies.multiplicativeClosure g)
  (h_rec :
    ∃ (L : List ℕ) (m_1 : ℕ) (b : ℕ) (h₁ : mk m_1 = mk (m + 1)) (h₂ : x_1 = mk (m_1 + b)) (h : L.length = b),
      IsAdmissible m_1 L ∧ g = standardσ L sorry),
  ∃ (L : List ℕ) (m_1 : ℕ) (b : ℕ) (h₁ : mk m_1 = mk m) (h₂ : x_1 = mk (m_1 + b)) (h : L.length = b),
    IsAdmissible m_1 L ∧ g ≫ σ k = standardσ L sorry
Tactic: cases hg' with | @σ m k =>
    obtain ⟨L₁, m₁, b₁, h₁', rfl, h', hL₁, e₁⟩ := h_rec
    obtain rfl : m₁ = m + 1 := congrArg (fun x ↦ x.len) h₁'
    use simplicialInsert k.val L₁, m, b₁ + 1, rfl, by grind, by grind, by grind
    subst_vars
    have := standardσ (m₁ := m + 1 + L₁.length) [] (by grind) ≫=
      (standardσ_simplicialInsert L₁ hL₁ k k.prop _ rfl).symm
    simp_all [Fin.ofNat_eq_cast, Fin.cast_val_eq_self, standardσ_comp_standardσ_assoc,
      standardσ_comp_standardσ]
Cleared hypotheses: j, x', g, g', hg, hg', h_rec
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
hf : P_σ f
⊢ ∃ (L : List ℕ) (m : ℕ) (b : ℕ) (h₁ : mk m = y) (h₂ : x = mk (m + b)) (h : L.length = b),
    IsAdmissible m L ∧ f = standardσ L ⋯
have id : ∀ (n : SimplexCategoryGenRel),
  ∃ (L : List ℕ) (m : ℕ) (b : ℕ) (h₁ : mk m = n) (h₂ : n = mk (m + b)) (h : L.length = b),
    IsAdmissible m L ∧ 𝟙 n = standardσ L sorry
Tactic: induction hf with
  | id n =>
    use [], n.len, 0, rfl, rfl, rfl, IsAdmissible.nil _
    rfl
  | of f hf =>
    cases hf with | @σ m k =>
    use [k.val], m, 1, rfl, rfl, rfl, IsAdmissible.singleton k.is_le
    simp [standardσ]
  | @comp_of _ j x' g g' hg hg' h_rec =>
    cases hg' with | @σ m k =>
    obtain ⟨L₁, m₁, b₁, h₁', rfl, h', hL₁, e₁⟩ := h_rec
    obtain rfl : m₁ = m + 1 := congrArg (fun x ↦ x.len) h₁'
    use simplicialInsert k.val L₁, m, b₁ + 1, rfl, by grind, by grind, by grind
    subst_vars
    have := standardσ (m₁ := m + 1 + L₁.length) [] (by grind) ≫=
      (standardσ_simplicialInsert L₁ hL₁ k k.prop _ rfl).symm
    simp_all [Fin.ofNat_eq_cast, Fin.cast_val_eq_self, standardσ_comp_standardσ_assoc,
      standardσ_comp_standardσ]
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
hf : P_σ f
id :
  ∀ (n : SimplexCategoryGenRel),
    ∃ (L : List ℕ) (m : ℕ) (b : ℕ) (h₁ : mk m = n) (h₂ : n = mk (m + b)) (h : L.length = b),
      IsAdmissible m L ∧ 𝟙 n = standardσ L ⋯
⊢ ∃ (L : List ℕ) (m : ℕ) (b : ℕ) (h₁ : mk m = y) (h₂ : x = mk (m + b)) (h : L.length = b),
    IsAdmissible m L ∧ f = standardσ L ⋯
have of : ∀ {x y : SimplexCategoryGenRel} (f : x ⟶ y) (hf : degeneracies f),
  ∃ (L : List ℕ) (m : ℕ) (b : ℕ) (h₁ : mk m = y) (h₂ : x = mk (m + b)) (h : L.length = b),
    IsAdmissible m L ∧ f = standardσ L sorry
Tactic: induction hf with
  | id n =>
    use [], n.len, 0, rfl, rfl, rfl, IsAdmissible.nil _
    rfl
  | of f hf =>
    cases hf with | @σ m k =>
    use [k.val], m, 1, rfl, rfl, rfl, IsAdmissible.singleton k.is_le
    simp [standardσ]
  | @comp_of _ j x' g g' hg hg' h_rec =>
    cases hg' with | @σ m k =>
    obtain ⟨L₁, m₁, b₁, h₁', rfl, h', hL₁, e₁⟩ := h_rec
    obtain rfl : m₁ = m + 1 := congrArg (fun x ↦ x.len) h₁'
    use simplicialInsert k.val L₁, m, b₁ + 1, rfl, by grind, by grind, by grind
    subst_vars
    have := standardσ (m₁ := m + 1 + L₁.length) [] (by grind) ≫=
      (standardσ_simplicialInsert L₁ hL₁ k k.prop _ rfl).symm
    simp_all [Fin.ofNat_eq_cast, Fin.cast_val_eq_self, standardσ_comp_standardσ_assoc,
      standardσ_comp_standardσ]
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
hf : P_σ f
id :
  ∀ (n : SimplexCategoryGenRel),
    ∃ (L : List ℕ) (m : ℕ) (b : ℕ) (h₁ : mk m = n) (h₂ : n = mk (m + b)) (h : L.length = b),
      IsAdmissible m L ∧ 𝟙 n = standardσ L ⋯
of :
  ∀ {x y : SimplexCategoryGenRel} (f : x ⟶ y) (hf : degeneracies f),
    ∃ (L : List ℕ) (m : ℕ) (b : ℕ) (h₁ : mk m = y) (h₂ : x = mk (m + b)) (h : L.length = b),
      IsAdmissible m L ∧ f = standardσ L ⋯
⊢ ∃ (L : List ℕ) (m : ℕ) (b : ℕ) (h₁ : mk m = y) (h₂ : x = mk (m + b)) (h : L.length = b),
    IsAdmissible m L ∧ f = standardσ L ⋯
have comp_of : ∀ {x j x' : SimplexCategoryGenRel} (g : x ⟶ j) (g' : j ⟶ x') (hg : degeneracies.multiplicativeClosure g)
  (hg' : degeneracies g')
  (h_rec :
    ∃ (L : List ℕ) (m : ℕ) (b : ℕ) (h₁ : mk m = j) (h₂ : x = mk (m + b)) (h : L.length = b),
      IsAdmissible m L ∧ g = standardσ L sorry),
  ∃ (L : List ℕ) (m : ℕ) (b : ℕ) (h₁ : mk m = x') (h₂ : x = mk (m + b)) (h : L.length = b),
    IsAdmissible m L ∧ g ≫ g' = standardσ L sorry
Tactic: induction hf with
  | id n =>
    use [], n.len, 0, rfl, rfl, rfl, IsAdmissible.nil _
    rfl
  | of f hf =>
    cases hf with | @σ m k =>
    use [k.val], m, 1, rfl, rfl, rfl, IsAdmissible.singleton k.is_le
    simp [standardσ]
  | @comp_of _ j x' g g' hg hg' h_rec =>
    cases hg' with | @σ m k =>
    obtain ⟨L₁, m₁, b₁, h₁', rfl, h', hL₁, e₁⟩ := h_rec
    obtain rfl : m₁ = m + 1 := congrArg (fun x ↦ x.len) h₁'
    use simplicialInsert k.val L₁, m, b₁ + 1, rfl, by grind, by grind, by grind
    subst_vars
    have := standardσ (m₁ := m + 1 + L₁.length) [] (by grind) ≫=
      (standardσ_simplicialInsert L₁ hL₁ k k.prop _ rfl).symm
    simp_all [Fin.ofNat_eq_cast, Fin.cast_val_eq_self, standardσ_comp_standardσ_assoc,
      standardσ_comp_standardσ]
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
m : ℕ
L : List ℕ
hL : IsAdmissible m L
k : ℕ
hk : k < L.length
⊢ simplicialEvalσ L (getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L k hk) =
    simplicialEvalσ L (getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L k hk + 1)
have nil : ∀ {m : ℕ} (hL : IsAdmissible m []) {k : ℕ} {hk : k < List.length (α := ℕ) []},
  simplicialEvalσ [] (getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) [] k hk) =
    simplicialEvalσ [] (getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) [] k hk + 1)
Tactic: induction L generalizing m k
Cleared hypotheses: m, L, hL, k, hk
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
m : ℕ
L : List ℕ
hL : IsAdmissible m L
k : ℕ
hk : k < L.length
nil :
  ∀ {m : ℕ} (hL : IsAdmissible m []) {k : ℕ} {hk : k < List.length (α := ℕ) []},
    simplicialEvalσ [] (getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) [] k hk) =
      simplicialEvalσ [] (getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) [] k hk + 1)
⊢ simplicialEvalσ L (getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L k hk) =
    simplicialEvalσ L (getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L k hk + 1)
have cons : ∀ (head : ℕ) (tail : List ℕ),
  (∀ {m : ℕ} (hL : IsAdmissible m tail) {k : ℕ} {hk : k < tail.length},
      simplicialEvalσ tail (getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) tail k hk) =
        simplicialEvalσ tail (getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) tail k hk + 1)) →
    ∀ {m : ℕ} (hL : IsAdmissible m (head :: tail)) {k : ℕ} {hk : k < (head :: tail).length},
      simplicialEvalσ (head :: tail)
          (getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (head :: tail) k hk) =
        simplicialEvalσ (head :: tail)
          (getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (head :: tail) k hk + 1)
Tactic: induction L generalizing m k
Cleared hypotheses: m, L, hL, k, hk
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (hypothesis)
Goal:
j a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ} (hL : IsAdmissible m L) (hj₁ : j < m + L.length) (hj₂ : simplicialEvalσ L j = simplicialEvalσ L (j + 1)),
    j ∈ L
m : ℕ
hL : IsAdmissible m (a :: L)
hj₁ : j < m + (a :: L).length
hj₂ : simplicialEvalσ (a :: L) j = simplicialEvalσ (a :: L) (j + 1)
⊢ j ∈ a :: L
have this : ∀ ⦃b : ℕ⦄, a + 1 ≤ b → simplicialEvalσ L (a + 1) ≤ simplicialEvalσ L b
Tactic: have := simplicialEvalσ_monotone L (a := a + 1)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
j a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ} (hL : IsAdmissible m L) (hj₁ : j < m + L.length) (hj₂ : simplicialEvalσ L j = simplicialEvalσ L (j + 1)),
    j ∈ L
m : ℕ
hL : IsAdmissible m (a :: L)
hj₁ : j < m + (a :: L).length
hj₂ : simplicialEvalσ (a :: L) j = simplicialEvalσ (a :: L) (j + 1)
this : ∀ ⦃b : ℕ⦄, a + 1 ≤ b → simplicialEvalσ L (a + 1) ≤ simplicialEvalσ L b
⊢ j ∈ a :: L
have cons : ∀ (h : j < a), j ∈ a :: L
Tactic: rcases lt_trichotomy j a with h | h | h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
j a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ} (hL : IsAdmissible m L) (hj₁ : j < m + L.length) (hj₂ : simplicialEvalσ L j = simplicialEvalσ L (j + 1)),
    j ∈ L
m : ℕ
hL : IsAdmissible m (a :: L)
hj₁ : j < m + (a :: L).length
hj₂ : simplicialEvalσ (a :: L) j = simplicialEvalσ (a :: L) (j + 1)
this : ∀ ⦃b : ℕ⦄, a + 1 ≤ b → simplicialEvalσ L (a + 1) ≤ simplicialEvalσ L b
cons : ∀ (h : j < a), j ∈ a :: L
⊢ j ∈ a :: L
have cons₁ : ∀ (h : j = a), j ∈ a :: L
Tactic: rcases lt_trichotomy j a with h | h | h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
j a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ} (hL : IsAdmissible m L) (hj₁ : j < m + L.length) (hj₂ : simplicialEvalσ L j = simplicialEvalσ L (j + 1)),
    j ∈ L
m : ℕ
hL : IsAdmissible m (a :: L)
hj₁ : j < m + (a :: L).length
hj₂ : simplicialEvalσ (a :: L) j = simplicialEvalσ (a :: L) (j + 1)
this : ∀ ⦃b : ℕ⦄, a + 1 ≤ b → simplicialEvalσ L (a + 1) ≤ simplicialEvalσ L b
cons : ∀ (h : j < a), j ∈ a :: L
cons₁ : ∀ (h : j = a), j ∈ a :: L
⊢ j ∈ a :: L
have cons₂ : ∀ (h : a < j), j ∈ a :: L
Tactic: rcases lt_trichotomy j a with h | h | h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
m : ℕ
L : List ℕ
hL : IsAdmissible m L
j : ℕ
hj₁ : j < m + L.length
hj₂ : simplicialEvalσ L j = simplicialEvalσ L (j + 1)
⊢ j ∈ L
have nil : ∀ {m : ℕ} (hL : IsAdmissible m []) (hj₁ : j < m + List.length (α := ℕ) [])
  (hj₂ : simplicialEvalσ [] j = simplicialEvalσ [] (j + 1)), Membership.mem (γ := List ℕ) [] j
Tactic: induction L generalizing m with
  | nil => grind
  | cons a L h_rec =>
    have := simplicialEvalσ_monotone L (a := a + 1)
    rcases lt_trichotomy j a with h | h | h <;> grind
Cleared hypotheses: m, L, hL, hj₁, hj₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms (goal)
Goal:
m : ℕ
L : List ℕ
hL : IsAdmissible m L
j : ℕ
hj₁ : j < m + L.length
hj₂ : simplicialEvalσ L j = simplicialEvalσ L (j + 1)
nil :
  ∀ {m : ℕ} (hL : IsAdmissible m []) (hj₁ : j < m + List.length (α := ℕ) [])
    (hj₂ : simplicialEvalσ [] j = simplicialEvalσ [] (j + 1)), Membership.mem (γ := List ℕ) [] j
⊢ j ∈ L
have cons : ∀ (a : ℕ) (L : List ℕ)
  (h_rec :
    ∀ {m : ℕ} (hL : IsAdmissible m L) (hj₁ : j < m + L.length) (hj₂ : simplicialEvalσ L j = simplicialEvalσ L (j + 1)),
      j ∈ L)
  {m : ℕ} (hL : IsAdmissible m (a :: L)) (hj₁ : j < m + (a :: L).length)
  (hj₂ : simplicialEvalσ (a :: L) j = simplicialEvalσ (a :: L) (j + 1)), j ∈ a :: L
Tactic: induction L generalizing m with
  | nil => grind
  | cons a L h_rec =>
    have := simplicialEvalσ_monotone L (a := a + 1)
    rcases lt_trichotomy j a with h | h | h <;> grind
Cleared hypotheses: m, L, hL, hj₁, hj₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty (goal)
Goal:
d : ℕ
W : MorphismProperty (Truncated d)
inst : W.IsMultiplicative
n : ℕ
hn : n < d
i : Fin (n + 2)
⊢ { len := n : SimplexCategory }.len ≤ d
have dsimp : n ≤ d
Tactic: dsimp