awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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
h₃ : (↑(Fin.ofNat (m + 1) 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))

Tactic:
convert! σ_comp_σ_nat (n := m) a j (by grind) (by grind) (by grind)

Premises used: SimplexCategoryGenRel.σ_comp_σ_nat
-- 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
⊢ (↑(Fin.ofNat (m + 2) a) : ℕ) = a

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
⊢ (↑(Fin.ofNat (m + 1) j) : ℕ) = j

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
⊢ (↑(Fin.ofNat (m + 1 + 1) (j + 1)) : ℕ) = j + 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
⊢ (↑(Fin.ofNat (m + 1) a) : ℕ) = a

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
⊢ 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
-- 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_2 : a < m + 2
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))
⊢ standardσ (a :: simplicialInsert (j + 1) L) ⋯ = standardσ (a :: L) ⋯ ≫ σ (Fin.ofNat (m + 1) j)

Tactic:
grind [standardσ_cons]

Premises used: SimplexCategoryGenRel.standardσ_cons
-- 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₁
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)
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) ⋯ = 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σ (simplicialInsert j (a :: L)) ⋯ = standardσ (a :: L) ⋯ ≫ σ (Fin.ofNat (m + 1) j)
⊢ standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (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]

Premises used: SimplexCategoryGenRel.simplicialInsert, SimplexCategoryGenRel.standardσ_cons, SimplexCategoryGenRel.standardσ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
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
rw : (mk m).1 + b = (mk (m + b)).1
⊢ y.1 + L.length = x.1

Tactic:
rw [h, h₁.symm, h₂]

Premises used: Eq.symm
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
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
⊢ (mk m).1 + b = (mk (m + b)).1

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
n : SimplexCategoryGenRel
right : Eq (α := n ⟶ n) (𝟙 n) (standardσ [] ⋯)
⊢ ∃ (L : List ℕ) (m : ℕ) (b : ℕ) (h₁ : mk m = n) (h₂ : n = mk (m + b)) (h : L.length = b),
    IsAdmissible m L ∧ 𝟙 n = standardσ L ⋯

Tactic:
use [], n.len, 0, rfl, rfl, rfl, IsAdmissible.nil _

Premises used: SimplexCategoryGenRel.len, SimplexCategoryGenRel.IsAdmissible.nil, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
n : SimplexCategoryGenRel
⊢ Eq (α := n ⟶ n) (𝟙 n) (standardσ [] ⋯)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
m : ℕ
k : Fin (m + 1)
right : σ k = standardσ [(↑k : ℕ)] ⋯
⊢ ∃ (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 ⋯

Tactic:
use [k.val], m, 1, rfl, rfl, rfl, IsAdmissible.singleton k.is_le

Premises used: Fin.is_le, Fin.val, SimplexCategoryGenRel.IsAdmissible.singleton, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
x y : SimplexCategoryGenRel
f : x ⟶ y
m : ℕ
k : Fin (m + 1)
⊢ σ k = standardσ [(↑k : ℕ)] ⋯

Tactic:
simp [standardσ]

Premises used: SimplexCategoryGenRel.standardσ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
x y : SimplexCategoryGenRel
f_1 : x ⟶ y
x_1 y_1 : SimplexCategoryGenRel
f : x_1 ⟶ y_1
hf : degeneracies f
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 ⋯
⊢ ∃ (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 ⋯

Tactic:
cases hf with | @σ m k =>
    use [k.val], m, 1, rfl, rfl, rfl, IsAdmissible.singleton k.is_le
    simp [standardσ]

Premises used: SimplexCategoryGenRel.σ, SimplexCategoryGenRel.standardσ, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
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 ⋯
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₁ ⋯),
    ∃ (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 ⋯
⊢ ∃ (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 ⋯

Tactic:
obtain ⟨L₁, m₁, b₁, h₁', rfl, h', hL₁, e₁⟩ := h_rec

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
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₁ ⋯
⊢ m₁ = m + 1

Tactic:
congrArg (fun x ↦ x.len) h₁'

Premises used: congrArg, SimplexCategoryGenRel.len
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
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₁ ⋯
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₁ ⋯),
    ∃ (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 ⋯
⊢ ∃ (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 ⋯

Tactic:
obtain rfl : m₁ = m + 1 := congrArg (fun x ↦ x.len) h₁'

Premises used: congrArg, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
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₁ ⋯
⊢ mk (m + 1 + b₁) = mk (m + (b₁ + 1))

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
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₁ ⋯
⊢ (simplicialInsert (↑k : ℕ) L₁).length = b₁ + 1

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
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₁ ⋯
⊢ IsAdmissible m (simplicialInsert (↑k : ℕ) L₁)

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
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₁ ⋯
right : g ≫ σ k = standardσ (simplicialInsert (↑k : ℕ) 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 ⋯

Tactic:
use simplicialInsert k.val L₁, m, b₁ + 1, rfl, by grind, by grind, by grind

Premises used: SimplexCategoryGenRel.simplicialInsert, Fin.val, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
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₁ ⋯
right :
  ∀ (hg : degeneracies.multiplicativeClosure (standardσ L₁ ⋯)),
    standardσ L₁ ⋯ ≫ σ k = standardσ (simplicialInsert (↑k : ℕ) L₁) ⋯
⊢ g ≫ σ k = standardσ (simplicialInsert (↑k : ℕ) L₁) ⋯

Tactic:
subst_vars
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
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₁ ⋯)
⊢ m + L₁.length + 1 + List.length (α := ℕ) [] = m + 1 + L₁.length

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
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₁ ⋯)
⊢ Eq (α := mk (m + 1 + L₁.length) ⟶ mk m) (standardσ [] ⋯ ≫ standardσ L₁ ⋯ ≫ σ (Fin.ofNat (m + 1) (↑k : ℕ)))
    (standardσ [] ⋯ ≫ standardσ (simplicialInsert (↑k : ℕ) L₁) ⋯)

Tactic:
have := standardσ (m₁ := m + 1 + L₁.length) [] (by grind) ≫=
      (standardσ_simplicialInsert L₁ hL₁ k k.prop _ rfl).symm
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
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₁ ⋯)
this :
  Eq (α := mk (m + 1 + L₁.length) ⟶ mk m) (standardσ [] ⋯ ≫ standardσ L₁ ⋯ ≫ σ (Fin.ofNat (m + 1) (↑k : ℕ)))
    (standardσ [] ⋯ ≫ standardσ (simplicialInsert (↑k : ℕ) L₁) ⋯)
⊢ standardσ L₁ ⋯ ≫ σ k = standardσ (simplicialInsert (↑k : ℕ) L₁) ⋯

Tactic:
simp_all [Fin.ofNat_eq_cast, Fin.cast_val_eq_self, standardσ_comp_standardσ_assoc,
      standardσ_comp_standardσ]

Premises used: Fin.ofNat_eq_cast, SimplexCategoryGenRel.standardσ_comp_standardσ_assoc, Fin.cast_val_eq_self, SimplexCategoryGenRel.standardσ_comp_standardσ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
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 ⋯
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 ⋯),
    ∃ (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 ⋯
⊢ ∃ (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 ⋯

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σ]

Premises used: Fin.ofNat_eq_cast, SimplexCategoryGenRel.standardσ_comp_standardσ_assoc, SimplexCategoryGenRel.σ, Fin.cast_val_eq_self, SimplexCategoryGenRel.standardσ_comp_standardσ, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
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 ⋯
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 ⋯),
    ∃ (L : List ℕ) (m : ℕ) (b : ℕ) (h₁ : mk m = x') (h₂ : x = mk (m + b)) (h : L.length = b),
      IsAdmissible m L ∧ g ≫ g' = 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 ⋯

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σ]

Premises used: Fin.ofNat_eq_cast, SimplexCategoryGenRel.standardσ_comp_standardσ_assoc, id, SimplexCategoryGenRel.σ, Fin.cast_val_eq_self, SimplexCategoryGenRel.standardσ, SimplexCategoryGenRel.IsAdmissible.nil, SimplexCategoryGenRel.standardσ_comp_standardσ, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
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)
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)
⊢ 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)

Tactic:
induction L generalizing m k
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
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:
grind [→ IsAdmissible.singleton]

Premises used: SimplexCategoryGenRel.IsAdmissible.singleton
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
head : ℕ
tail : List ℕ
tail_ih :
  ∀ {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:
grind [→ IsAdmissible.singleton]

Premises used: SimplexCategoryGenRel.IsAdmissible.singleton
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
j m : ℕ
hL : IsAdmissible m []
hj₁ : j < m + List.length (α := ℕ) []
hj₂ : simplicialEvalσ [] j = simplicialEvalσ [] (j + 1)
⊢ Membership.mem (γ := List ℕ) [] j

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
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)
⊢ ∀ ⦃b : ℕ⦄, a + 1 ≤ b → simplicialEvalσ L (a + 1) ≤ simplicialEvalσ L b

Tactic:
have := simplicialEvalσ_monotone L (a := a + 1)
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
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
cons₂ : ∀ (h : a < j), j ∈ a :: L
⊢ j ∈ a :: L

Tactic:
rcases lt_trichotomy j a with h | h | h

Premises used: lt_trichotomy
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
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
h : j < a
⊢ j ∈ a :: L

Tactic:
grind