awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
x y : ℕ
xs : List ℕ
h_1 :
  ∀ {m : ℕ},
    IsAdmissible m xs ↔
      List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) xs ∧
        ∀ (k : ℕ) (h : k < xs.length), getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) xs k h ≤ m + k
IH :
  ∀ (y : ℕ) {m : ℕ},
    IsAdmissible m (y :: xs) ↔
      List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) (y :: xs) ∧
        ∀ (k : ℕ) (h : k < (y :: xs).length),
          getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (y :: xs) k h ≤ m + k
m : ℕ
h_2 : x < y
h_3 : List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) (y :: xs)
h :
  ∀ (k : ℕ) (h : k < xs.length + 1 + 1),
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (x :: y :: xs) k h ≤ m + k
k : ℕ
h_4 : k < xs.length + 1
⊢ k + 1 < xs.length + 1 + 1

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
x y : ℕ
xs : List ℕ
h_1 :
  ∀ {m : ℕ},
    IsAdmissible m xs ↔
      List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) xs ∧
        ∀ (k : ℕ) (h : k < xs.length), getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) xs k h ≤ m + k
IH :
  ∀ (y : ℕ) {m : ℕ},
    IsAdmissible m (y :: xs) ↔
      List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) (y :: xs) ∧
        ∀ (k : ℕ) (h : k < (y :: xs).length),
          getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (y :: xs) k h ≤ m + k
m : ℕ
h_2 : x < y
h_3 : List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) (y :: xs)
h :
  ∀ (k : ℕ) (h : k < xs.length + 1 + 1),
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (x :: y :: xs) k h ≤ m + k
k : ℕ
h_4 : k < xs.length + 1
⊢ m + (k + 1) ≤ m + 1 + k

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
x y : ℕ
xs : List ℕ
h :
  ∀ {m : ℕ},
    IsAdmissible m xs ↔
      List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) xs ∧
        ∀ (k : ℕ) (h : k < xs.length), getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) xs k h ≤ m + k
IH :
  ∀ (y : ℕ) {m : ℕ},
    IsAdmissible m (y :: xs) ↔
      List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) (y :: xs) ∧
        ∀ (k : ℕ) (h : k < (y :: xs).length),
          getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (y :: xs) k h ≤ m + k
m : ℕ
⊢ x < y →
    List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) (y :: xs) →
      ((x ≤ m ∧
          ∀ (k : ℕ) (h : k < xs.length + 1),
            getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (y :: xs) k h ≤ m + 1 + k) ↔
        ∀ (k : ℕ) (h : k < xs.length + 1 + 1),
          getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (x :: y :: xs) k h ≤ m + k)

Tactic:
exact fun _ _ => ⟨fun h => by grind,
      fun h => ⟨h 0 (by grind), fun k _ => (h (k + 1) (by grind)).trans (by grind)⟩⟩
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m : ℕ
L : List ℕ
nil :
  ∀ {m : ℕ},
    IsAdmissible m [] ↔
      List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) [] ∧
        ∀ (k : ℕ) (h : k < List.length (α := ℕ) []),
          getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) [] k h ≤ m + k
singleton :
  ∀ (x : ℕ) {m : ℕ},
    IsAdmissible m [x] ↔
      List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) [x] ∧
        ∀ (k : ℕ) (h : k < [x].length), getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) [x] k h ≤ m + k
cons_cons :
  ∀ (x y : ℕ) (xs : List ℕ),
    (∀ {m : ℕ},
        IsAdmissible m xs ↔
          List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) xs ∧
            ∀ (k : ℕ) (h : k < xs.length),
              getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) xs k h ≤ m + k) →
      ∀
        (IH :
          ∀ (y : ℕ) {m : ℕ},
            IsAdmissible m (y :: xs) ↔
              List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) (y :: xs) ∧
                ∀ (k : ℕ) (h : k < (y :: xs).length),
                  getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (y :: xs) k h ≤ m + k)
        {m : ℕ},
        IsAdmissible m (x :: y :: xs) ↔
          List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) (x :: y :: xs) ∧
            ∀ (k : ℕ) (h : k < (x :: y :: xs).length),
              getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (x :: y :: xs) k h ≤ m + k
⊢ IsAdmissible m L ↔
    List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) L ∧
      ∀ (k : ℕ) (h : k < L.length), getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L k h ≤ m + k

Tactic:
induction L using List.twoStepInduction generalizing m with
  | nil => grind
  | singleton _ => simp
  | cons_cons _ _ _ _ IH =>
    simp_rw [isAdmissible_cons_cons_iff, IH, List.length_cons, and_assoc,
      List.isChain_cons_cons, and_assoc, and_congr_right_iff, and_comm]
    exact fun _ _ => ⟨fun h => by grind,
      fun h => ⟨h 0 (by grind), fun k _ => (h (k + 1) (by grind)).trans (by grind)⟩⟩

Premises used: List.length_cons, and_congr_right_iff, and_comm, List.isChain_cons_cons, and_assoc, Singleton.singleton, SimplexCategoryGenRel.isAdmissible_cons_cons_iff
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m : ℕ
L : List ℕ
rw :
  (List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) L ∧
      ∀ (k : ℕ) (h : k < L.length), getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L k h ≤ m + k) ↔
    List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) L ∧
      ∀ (k : ℕ) (h : k < L.length), getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L k h ≤ m + k
rw₁ rw₂ :
  (List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) L ∧
      ∀ (k : ℕ) (h : k < L.length), getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L k h ≤ m + k) ↔
    List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) L ∧
      ∀ (k : ℕ) (h : k < L.length), getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L k h ≤ m + k
⊢ IsAdmissible m L ↔
    List.Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) L ∧
      ∀ (k : ℕ) (h : k < L.length), getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L k h ≤ m + k

Tactic:
rw [isAdmissible_iff_isChain_and_le, List.isChain_iff_pairwise]

Premises used: SimplexCategoryGenRel.isAdmissible_iff_isChain_and_le, List.isChain_iff_pairwise
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m : ℕ
L : List ℕ
hL : List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) L
hL₂ : ∀ (k : ℕ) (h : k < L.length), getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L k h ≤ m + k
⊢ IsAdmissible m L

Tactic:
isAdmissible_iff_isChain_and_le.mpr ⟨hL, hL₂⟩

Premises used: Iff.mpr, SimplexCategoryGenRel.isAdmissible_iff_isChain_and_le, And.intro
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m : ℕ
L : List ℕ
hL : IsAdmissible m L
⊢ List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) L

Tactic:
(isAdmissible_iff_isChain_and_le.mp hL).1

Premises used: SimplexCategoryGenRel.isAdmissible_iff_isChain_and_le, And.left, Iff.mp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m : ℕ
L : List ℕ
hL : IsAdmissible m L
⊢ ∀ (k : ℕ) (h : k < L.length), getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L k h ≤ m + k

Tactic:
(isAdmissible_iff_isChain_and_le.mp hL).2

Premises used: SimplexCategoryGenRel.isAdmissible_iff_isChain_and_le, And.right, Iff.mp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m a : ℕ
L : List ℕ
h : IsAdmissible m (a :: L)
nil : ∀ (h : IsAdmissible m [a]), IsAdmissible (m + 1) []
cons : ∀ (head : ℕ) (tail : List ℕ) (h : IsAdmissible m (a :: head :: tail)), IsAdmissible (m + 1) (head :: tail)
⊢ IsAdmissible (m + 1) L

Tactic:
cases L
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m a : ℕ
h : IsAdmissible m [a]
⊢ IsAdmissible (m + 1) []

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m a head : ℕ
tail : List ℕ
h : IsAdmissible m (a :: head :: tail)
⊢ IsAdmissible (m + 1) (head :: tail)

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m a : ℕ
L : List ℕ
hL : IsAdmissible (m + 1) L
ha : a ≤ m
ha' : ∀ (x : 0 < L.length), a < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L 0 x
nil :
  ∀ (hL : IsAdmissible (m + 1) [])
    (ha' :
      ∀ (x : 0 < List.length (α := ℕ) []), a < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) [] 0 x),
    IsAdmissible m [a]
cons₁ :
  ∀ (head : ℕ) (tail : List ℕ) (hL : IsAdmissible (m + 1) (head :: tail))
    (ha' :
      ∀ (x : 0 < (head :: tail).length),
        a < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (head :: tail) 0 x),
    IsAdmissible m (a :: head :: tail)
⊢ IsAdmissible m (a :: L)

Tactic:
cases L
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m a : ℕ
ha : a ≤ m
hL : IsAdmissible (m + 1) []
ha' : ∀ (x : 0 < List.length (α := ℕ) []), a < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) [] 0 x
⊢ IsAdmissible m [a]

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m a : ℕ
ha : a ≤ m
head : ℕ
tail : List ℕ
hL : IsAdmissible (m + 1) (head :: tail)
ha' :
  ∀ (x : 0 < (head :: tail).length), a < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (head :: tail) 0 x
⊢ IsAdmissible m (a :: head :: tail)

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m : ℕ
L : List ℕ
hL : IsAdmissible m L
⊢ L.SortedLT

Tactic:
hL.isChain.sortedLT

Premises used: SimplexCategoryGenRel.IsAdmissible.isChain, List.IsChain.sortedLT
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m a : ℕ
L : List ℕ
hL : IsAdmissible m (a :: L)
⊢ ∀ a' ∈ L, a < a'

Tactic:
fun _ => L.rel_of_pairwise_cons hL.sortedLT.pairwise

Premises used: List.rel_of_pairwise_cons, List.SortedLT.pairwise, SimplexCategoryGenRel.IsAdmissible.sortedLT
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m : ℕ
L : List ℕ
hL : IsAdmissible m L
k : ℕ
hk : k < L.length
⊢ getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L k hk < m + L.length

Tactic:
(hL.le k hk).trans_lt (Nat.add_lt_add_left hk _)

Premises used: SimplexCategoryGenRel.IsAdmissible.le, Nat.add_lt_add_left, LE.le.trans_lt
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m_1 m_2 a b : ℕ
L_1 : List ℕ
m : ℕ
L : List ℕ
hl : IsAdmissible m L
k : ℕ
hK : k < L.length
⊢ getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L k hK ≤ m + k

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m_1 m_2 a_1 b : ℕ
L_1 : List ℕ
m a : ℕ
L : List ℕ
hl : IsAdmissible m (a :: L)
⊢ 0 < (a :: L).length

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m : ℕ
L : List ℕ
n : ℕ
hmn : m ≤ n
hL : IsAdmissible m L
⊢ List.IsChain (fun (x1 x2 : ℕ) ↦ x1 < x2) L

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m : ℕ
L : List ℕ
n : ℕ
hmn : m ≤ n
hL : IsAdmissible m L
⊢ ∀ (k : ℕ) (h : k < L.length), getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) L k h ≤ n + k

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
a : ℕ
L : List ℕ
nil : ∀ (a : ℕ), (simplicialInsert a []).length = List.length (α := ℕ) [] + 1
cons :
  ∀ (head : ℕ) (tail : List ℕ),
    (∀ (a : ℕ), (simplicialInsert a tail).length = tail.length + 1) →
      ∀ (a : ℕ), (simplicialInsert a (head :: tail)).length = (head :: tail).length + 1
⊢ (simplicialInsert a L).length = L.length + 1

Tactic:
induction L generalizing a
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
a : ℕ
⊢ (simplicialInsert a []).length = List.length (α := ℕ) [] + 1

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
head : ℕ
tail : List ℕ
tail_ih : ∀ (a : ℕ), (simplicialInsert a tail).length = tail.length + 1
a : ℕ
⊢ (simplicialInsert a (head :: tail)).length = (head :: tail).length + 1

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m : ℕ
hL : IsAdmissible (m + 1) []
j : ℕ
hj : j ≤ m
⊢ IsAdmissible m (simplicialInsert j [])

Tactic:
IsAdmissible.singleton hj

Premises used: SimplexCategoryGenRel.simplicialInsert, SimplexCategoryGenRel.IsAdmissible.singleton
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m : ℕ
hL : IsAdmissible (m + 1) []
j : ℕ
hj : j ≤ m
⊢ IsAdmissible m (simplicialInsert j [])

Tactic:
exact IsAdmissible.singleton hj

Premises used: SimplexCategoryGenRel.IsAdmissible.singleton
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
a : ℕ
L : List ℕ
h_rec : ∀ (m : ℕ) (hL : IsAdmissible (m + 1) L) (j : ℕ) (hj : j ≤ m), IsAdmissible m (simplicialInsert j L)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j ≤ m
cons :
  ∀ (h_rec : ∀ (m : ℕ) (hL : IsAdmissible (m + 1) []) (j : ℕ) (hj : j ≤ m), IsAdmissible m (simplicialInsert j []))
    (hL : IsAdmissible (m + 1) [a]), IsAdmissible m (simplicialInsert j [a])
cons₁ :
  ∀ (head : ℕ) (tail : List ℕ)
    (h_rec :
      ∀ (m : ℕ) (hL : IsAdmissible (m + 1) (head :: tail)) (j : ℕ) (hj : j ≤ m),
        IsAdmissible m (simplicialInsert j (head :: tail)))
    (hL : IsAdmissible (m + 1) (a :: head :: tail)), IsAdmissible m (simplicialInsert j (a :: head :: tail))
⊢ IsAdmissible m (simplicialInsert j (a :: L))

Tactic:
cases L
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
a m j : ℕ
hj : j ≤ m
h_rec : ∀ (m : ℕ) (hL : IsAdmissible (m + 1) []) (j : ℕ) (hj : j ≤ m), IsAdmissible m (simplicialInsert j [])
hL : IsAdmissible (m + 1) [a]
⊢ IsAdmissible m (simplicialInsert j [a])

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
a m j : ℕ
hj : j ≤ m
head : ℕ
tail : List ℕ
h_rec :
  ∀ (m : ℕ) (hL : IsAdmissible (m + 1) (head :: tail)) (j : ℕ) (hj : j ≤ m),
    IsAdmissible m (simplicialInsert j (head :: tail))
hL : IsAdmissible (m + 1) (a :: head :: tail)
⊢ IsAdmissible m (simplicialInsert j (a :: head :: tail))

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m : ℕ
L : List ℕ
hL : IsAdmissible (m + 1) L
j : ℕ
hj : j ≤ m
nil : ∀ (m : ℕ) (hL : IsAdmissible (m + 1) []) (j : ℕ) (hj : j ≤ m), IsAdmissible m (simplicialInsert j [])
cons :
  ∀ (a : ℕ) (L : List ℕ)
    (h_rec : ∀ (m : ℕ) (hL : IsAdmissible (m + 1) L) (j : ℕ) (hj : j ≤ m), IsAdmissible m (simplicialInsert j L))
    (m : ℕ) (hL : IsAdmissible (m + 1) (a :: L)) (j : ℕ) (hj : j ≤ m), IsAdmissible m (simplicialInsert j (a :: L))
⊢ IsAdmissible m (simplicialInsert j L)

Tactic:
induction L generalizing j m with
  | nil => exact IsAdmissible.singleton hj
  | cons a L h_rec => cases L <;> grind

Premises used: SimplexCategoryGenRel.IsAdmissible.singleton
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L : List ℕ
m₁ m₂ : ℕ
h : m₂ + List.length (α := ℕ) [] = m₁
⊢ mk m₁ = mk m₂

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L : List ℕ
m₁ m₂ a : ℕ
t : List ℕ
h : m₂ + (a :: t).length = m₁
⊢ m₂ + 1 + t.length = m₁

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m : ℕ
⊢ m + List.length (α := ℕ) [] = m

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
m : ℕ
⊢ standardσ [] ⋯ = 𝟙 (mk m)

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, SimplexCategoryGenRel.standardσ, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L : List ℕ
a m₁ m₂ : ℕ
h : m₂ + (a :: L).length = m₁
⊢ m₂ + 1 + L.length = m₁

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L : List ℕ
a m₁ m₂ : ℕ
h : m₂ + (a :: L).length = m₁
⊢ standardσ (a :: L) h = standardσ L ⋯ ≫ σ (Fin.ofNat (m₂ + 1) a)

Tactic:
rfl

Premises used: SimplexCategoryGenRel.standardσ, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L₁ L₂ : List ℕ
m₁ m₂ m₃ : ℕ
h : m₂ + L₁.length = m₁
h' : m₃ + L₂.length = m₂
⊢ m₃ + (L₂ ++ L₁).length = m₁

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L₁ : List ℕ
m₁ m₂ m₃ : ℕ
h : m₂ + L₁.length = m₁
h' : m₃ + List.length (α := ℕ) [] = m₂
⊢ m₃ = m₂

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L₁ : List ℕ
m₁ m₂ m₃ : ℕ
h : m₂ + L₁.length = m₁
h' : m₃ + List.length (α := ℕ) [] = m₂
nil :
  ∀ (h : m₃ + L₁.length = m₁) (h' : m₃ + List.length (α := ℕ) [] = m₃),
    standardσ L₁ h ≫ standardσ [] h' = standardσ ([] ++ L₁) ⋯
⊢ standardσ L₁ h ≫ standardσ [] h' = standardσ ([] ++ L₁) ⋯

Tactic:
obtain rfl : m₃ = m₂ := by grind

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L₁ : List ℕ
m₁ m₃ : ℕ
h : m₃ + L₁.length = m₁
h' : m₃ + List.length (α := ℕ) [] = m₃
⊢ standardσ L₁ h ≫ standardσ [] h' = standardσ ([] ++ L₁) ⋯

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
a : ℕ
t : List ℕ
H :
  ∀ (L₁ : List ℕ) {m₁ m₂ m₃ : ℕ} (h : m₂ + L₁.length = m₁) (h' : m₃ + t.length = m₂),
    standardσ L₁ h ≫ standardσ t h' = standardσ (t ++ L₁) ⋯
L₁ : List ℕ
m₁ m₂ m₃ : ℕ
h : m₂ + L₁.length = m₁
h' : m₃ + (t.length + 1) = m₂
⊢ m₂ = m₃ + t.length + 1

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
a : ℕ
t : List ℕ
H :
  ∀ (L₁ : List ℕ) {m₁ m₂ m₃ : ℕ} (h : m₂ + L₁.length = m₁) (h' : m₃ + t.length = m₂),
    standardσ L₁ h ≫ standardσ t h' = standardσ (t ++ L₁) ⋯
L₁ : List ℕ
m₁ m₂ m₃ : ℕ
h : m₂ + L₁.length = m₁
h' : m₃ + (t.length + 1) = m₂
cons :
  ∀ (h : m₃ + t.length + 1 + L₁.length = m₁) (h' : m₃ + (t.length + 1) = m₃ + t.length + 1),
    standardσ L₁ h ≫ standardσ t ⋯ ≫ σ (↑a : Fin (m₃ + 1)) = standardσ (t ++ L₁) ⋯ ≫ σ (↑a : Fin (m₃ + 1))
⊢ standardσ L₁ h ≫ standardσ t ⋯ ≫ σ (↑a : Fin (m₃ + 1)) = standardσ (t ++ L₁) ⋯ ≫ σ (↑a : Fin (m₃ + 1))

Tactic:
obtain rfl : m₂ = (m₃ + t.length) + 1 := by grind

Premises used: HAdd.hAdd, List.length, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
a : ℕ
t : List ℕ
H :
  ∀ (L₁ : List ℕ) {m₁ m₂ m₃ : ℕ} (h : m₂ + L₁.length = m₁) (h' : m₃ + t.length = m₂),
    standardσ L₁ h ≫ standardσ t h' = standardσ (t ++ L₁) ⋯
L₁ : List ℕ
m₁ m₃ : ℕ
h : m₃ + t.length + 1 + L₁.length = m₁
h' : m₃ + (t.length + 1) = m₃ + t.length + 1
⊢ m₃ + t.length + 1 + L₁.length = m₁

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
a : ℕ
t : List ℕ
H :
  ∀ (L₁ : List ℕ) {m₁ m₂ m₃ : ℕ} (h : m₂ + L₁.length = m₁) (h' : m₃ + t.length = m₂),
    standardσ L₁ h ≫ standardσ t h' = standardσ (t ++ L₁) ⋯
L₁ : List ℕ
m₁ m₃ : ℕ
h : m₃ + t.length + 1 + L₁.length = m₁
h' : m₃ + (t.length + 1) = m₃ + t.length + 1
⊢ m₃ + 1 + t.length = m₃ + t.length + 1

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
a : ℕ
t : List ℕ
H :
  ∀ (L₁ : List ℕ) {m₁ m₂ m₃ : ℕ} (h : m₂ + L₁.length = m₁) (h' : m₃ + t.length = m₂),
    standardσ L₁ h ≫ standardσ t h' = standardσ (t ++ L₁) ⋯
L₁ : List ℕ
m₁ m₃ : ℕ
h : m₃ + t.length + 1 + L₁.length = m₁
h' : m₃ + (t.length + 1) = m₃ + t.length + 1
⊢ standardσ L₁ h ≫ standardσ t ⋯ ≫ σ (↑a : Fin (m₃ + 1)) = standardσ (t ++ L₁) ⋯ ≫ σ (↑a : Fin (m₃ + 1))

Tactic:
simp [reassoc_of% (H L₁ (m₁ := m₁) (m₂ := m₃ + t.length + 1) (m₃ := m₃ + 1)
      (by grind) (by grind))]
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L₁ L₂ : List ℕ
m₁ m₂ m₃ : ℕ
h : m₂ + L₁.length = m₁
h' : m₃ + L₂.length = m₂
nil :
  ∀ (L₁ : List ℕ) {m₁ m₂ m₃ : ℕ} (h : m₂ + L₁.length = m₁) (h' : m₃ + List.length (α := ℕ) [] = m₂),
    standardσ L₁ h ≫ standardσ [] h' = standardσ ([] ++ L₁) ⋯
cons :
  ∀ (a : ℕ) (t : List ℕ)
    (H :
      ∀ (L₁ : List ℕ) {m₁ m₂ m₃ : ℕ} (h : m₂ + L₁.length = m₁) (h' : m₃ + t.length = m₂),
        standardσ L₁ h ≫ standardσ t h' = standardσ (t ++ L₁) ⋯)
    (L₁ : List ℕ) {m₁ m₂ m₃ : ℕ} (h : m₂ + L₁.length = m₁) (h' : m₃ + (a :: t).length = m₂),
    standardσ L₁ h ≫ standardσ (a :: t) h' = standardσ (a :: t ++ L₁) ⋯
⊢ standardσ L₁ h ≫ standardσ L₂ h' = standardσ (L₂ ++ L₁) ⋯

Tactic:
induction L₂ generalizing L₁ m₁ m₂ m₃ with
  | nil =>
    obtain rfl : m₃ = m₂ := by grind
    simp
  | cons a t H =>
    dsimp at h' ⊢
    obtain rfl : m₂ = (m₃ + t.length) + 1 := by grind
    simp [reassoc_of% (H L₁ (m₁ := m₁) (m₂ := m₃ + t.length + 1) (m₃ := m₃ + 1)
      (by grind) (by grind))]

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L : List ℕ
j : ℕ
hj : ∀ (k : ℕ), Membership.mem (γ := List ℕ) [] k → j ≤ k
⊢ simplicialEvalσ [] j = j

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L : List ℕ
j head : ℕ
tail : List ℕ
tail_ih : ∀ (hj : ∀ k ∈ tail, j ≤ k), simplicialEvalσ tail j = j
hj : ∀ k ∈ head :: tail, j ≤ k
⊢ j ≤ head ∧ ∀ x ∈ tail, j ≤ x

Tactic:
simp only [List.forall_mem_cons] at hj

Premises used: List.forall_mem_cons
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L : List ℕ
j head : ℕ
tail : List ℕ
tail_ih : ∀ (hj : ∀ k ∈ tail, j ≤ k), simplicialEvalσ tail j = j
hj : j ≤ head ∧ ∀ x ∈ tail, j ≤ x
⊢ simplicialEvalσ (head :: tail) j = j

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L : List ℕ
j : ℕ
hj : ∀ k ∈ L, j ≤ k
nil : ∀ (hj : ∀ (k : ℕ), Membership.mem (γ := List ℕ) [] k → j ≤ k), simplicialEvalσ [] j = j
cons :
  ∀ (head : ℕ) (tail : List ℕ),
    (∀ (hj : ∀ k ∈ tail, j ≤ k), simplicialEvalσ tail j = j) →
      ∀ (hj : ∀ k ∈ head :: tail, j ≤ k), simplicialEvalσ (head :: tail) j = j
⊢ simplicialEvalσ L j = j

Tactic:
induction L with | nil => grind | cons _ _ _ => simp only [List.forall_mem_cons] at hj; grind

Premises used: List.forall_mem_cons
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L : List ℕ
nil : Monotone (simplicialEvalσ [])
cons : ∀ (head : ℕ) (tail : List ℕ), Monotone (simplicialEvalσ tail) → Monotone (simplicialEvalσ (head :: tail))
⊢ Monotone (simplicialEvalσ L)

Tactic:
induction L
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
⊢ Monotone (simplicialEvalσ [])

Tactic:
grind [Monotone]

Premises used: Monotone
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
head : ℕ
tail : List ℕ
tail_ih : Monotone (simplicialEvalσ tail)
⊢ Monotone (simplicialEvalσ (head :: tail))

Tactic:
grind [Monotone]

Premises used: Monotone
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L : List ℕ
j m₁ m₂ : ℕ
hL : IsAdmissible m₂ []
hk : m₂ + List.length (α := ℕ) [] = m₁
hj : j < m₁ + 1
⊢ m₁ = m₂

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
Goal:
L : List ℕ
j m₁ m₂ : ℕ
hL : IsAdmissible m₂ []
hk : m₂ + List.length (α := ℕ) [] = m₁
hj : j < m₁ + 1
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
⊢ (↑((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

Premises used: rfl