mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: case «0»
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
⊢ ↑((Hom.toOrderHom (α.hom ≫ (inclusion 2).op.map (Hom.tr (mkOfSucc 1) ⋯ ⋯).op).unop) ((fun i ↦ i) ⟨0, ⋯⟩)) =
    ↑((Hom.toOrderHom α₀.hom.unop) ((fun i ↦ i) ⟨0, ⋯⟩))

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: case «1»
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
⊢ ↑((Hom.toOrderHom (α.hom ≫ (inclusion 2).op.map (Hom.tr (mkOfSucc 1) ⋯ ⋯).op).unop)
        ((fun i ↦ i) ⟨(unop ((inclusion 2).op.obj α₀.right)).len, ⋯⟩)) =
    ↑((Hom.toOrderHom α₀.hom.unop) ((fun i ↦ i) ⟨(unop ((inclusion 2).op.obj α₀.right)).len, ⋯⟩))

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: case «0»
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
β₀ : α ⟶ α₀ := homMk (Hom.tr (mkOfSucc 1) ⋯ ⋯).op ⋯
⊢ ↑((Hom.toOrderHom (α.hom ≫ (inclusion 2).op.map (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op).unop) ((fun i ↦ i) ⟨0, ⋯⟩)) =
    ↑((Hom.toOrderHom α₁.hom.unop) ((fun i ↦ i) ⟨0, ⋯⟩))

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: case «1»
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
β₀ : α ⟶ α₀ := homMk (Hom.tr (mkOfSucc 1) ⋯ ⋯).op ⋯
⊢ ↑((Hom.toOrderHom (α.hom ≫ (inclusion 2).op.map (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op).unop)
        ((fun i ↦ i) ⟨(unop ((inclusion 2).op.obj α₁.right)).len, ⋯⟩)) =
    ↑((Hom.toOrderHom α₁.hom.unop) ((fun i ↦ i) ⟨(unop ((inclusion 2).op.obj α₁.right)).len, ⋯⟩))

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: case «0»
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
β₀ : α ⟶ α₀ := homMk (Hom.tr (mkOfSucc 1) ⋯ ⋯).op ⋯
β₁ : α ⟶ α₁ := homMk (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op ⋯
⊢ ↑((Hom.toOrderHom (α.hom ≫ (inclusion 2).op.map (Hom.tr (mkOfSucc 0) ⋯ ⋯).op).unop) ((fun i ↦ i) ⟨0, ⋯⟩)) =
    ↑((Hom.toOrderHom α₂.hom.unop) ((fun i ↦ i) ⟨0, ⋯⟩))

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: case «1»
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
β₀ : α ⟶ α₀ := homMk (Hom.tr (mkOfSucc 1) ⋯ ⋯).op ⋯
β₁ : α ⟶ α₁ := homMk (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op ⋯
⊢ ↑((Hom.toOrderHom (α.hom ≫ (inclusion 2).op.map (Hom.tr (mkOfSucc 0) ⋯ ⋯).op).unop)
        ((fun i ↦ i) ⟨(unop ((inclusion 2).op.obj α₂.right)).len, ⋯⟩)) =
    ↑((Hom.toOrderHom α₂.hom.unop) ((fun i ↦ i) ⟨(unop ((inclusion 2).op.obj α₂.right)).len, ⋯⟩))

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: n : ℕ
i' : Fin (n + 2)
i : Fin (n + 1)
h : i' ≤ i.castSucc
⊢ δ i'.castSucc ≫ σ i.succ = σ i ≫ δ i'

Tactic:
rw [δ_comp_σ_of_le h]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: m a b : ℕ
L : List ℕ
⊢ a < b ∧ IsAdmissible (m + 1) (b :: L) ∧ a ≤ m → IsAdmissible m (a :: b :: L)

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case nil
m a : ℕ
⊢ IsAdmissible m [a] ↔ a ≤ m ∧ (∀ (x : 0 < [].length), a < [][0]) ∧ IsAdmissible (m + 1) []

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case cons
m a head✝ : ℕ
tail✝ : List ℕ
⊢ IsAdmissible m (a :: head✝ :: tail✝) ↔
    a ≤ m ∧ (∀ (x : 0 < (head✝ :: tail✝).length), a < (head✝ :: tail✝)[0]) ∧ IsAdmissible (m + 1) (head✝ :: tail✝)

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case nil
m : ℕ
⊢ IsAdmissible m [] ↔ List.IsChain (fun x1 x2 ↦ x1 < x2) [] ∧ ∀ (k : ℕ) (h : k < [].length), [][k] ≤ m + k

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: case «0»
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
β₀ : α ⟶ α₀ := homMk (Hom.tr (mkOfSucc 1) ⋯ ⋯).op ⋯
β₁ : α ⟶ α₁ := homMk (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op ⋯
β₂ : α ⟶ α₂ := homMk (Hom.tr (mkOfSucc 0) ⋯ ⋯).op ⋯
h₀ : (ConcreteCategory.hom (X.map α₀.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₀)) x
h₂ : (ConcreteCategory.hom (X.map α₂.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₂)) x
t : Fin (1 + 1)
⊢ ↑((Hom.toOrderHom (α.hom ≫ (mkOfSucc 0).op).unop) ((fun i ↦ i) ⟨0, ⋯⟩)) =
    ↑((Hom.toOrderHom α₂.hom.unop) ((fun i ↦ i) ⟨0, ⋯⟩))

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: case «1»
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
β₀ : α ⟶ α₀ := homMk (Hom.tr (mkOfSucc 1) ⋯ ⋯).op ⋯
β₁ : α ⟶ α₁ := homMk (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op ⋯
β₂ : α ⟶ α₂ := homMk (Hom.tr (mkOfSucc 0) ⋯ ⋯).op ⋯
h₀ : (ConcreteCategory.hom (X.map α₀.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₀)) x
h₂ : (ConcreteCategory.hom (X.map α₂.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₂)) x
t : Fin (1 + 1)
⊢ ↑((Hom.toOrderHom (α.hom ≫ (mkOfSucc 0).op).unop) ((fun i ↦ i) ⟨1, ⋯⟩)) =
    ↑((Hom.toOrderHom α₂.hom.unop) ((fun i ↦ i) ⟨1, ⋯⟩))

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: x✝² y✝ : ℕ
xs✝ : List ℕ
a✝ :
  ∀ {m : ℕ},
    IsAdmissible m xs✝ ↔ List.IsChain (fun x1 x2 ↦ x1 < x2) xs✝ ∧ ∀ (k : ℕ) (h : k < xs✝.length), xs✝[k] ≤ m + k
IH :
  ∀ (y : ℕ) {m : ℕ},
    IsAdmissible m (y :: xs✝) ↔
      List.IsChain (fun x1 x2 ↦ x1 < x2) (y :: xs✝) ∧ ∀ (k : ℕ) (h : k < (y :: xs✝).length), (y :: xs✝)[k] ≤ m + k
m : ℕ
x✝¹ : x✝² < y✝
x✝ : List.IsChain (fun x1 x2 ↦ x1 < x2) (y✝ :: xs✝)
h : x✝² ≤ m ∧ ∀ (k : ℕ) (h : k < xs✝.length + 1), (y✝ :: xs✝)[k] ≤ m + 1 + k
⊢ ∀ (k : ℕ) (h : k < xs✝.length + 1 + 1), (x✝² :: y✝ :: xs✝)[k] ≤ m + k

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: x✝² y✝ : ℕ
xs✝ : List ℕ
a✝ :
  ∀ {m : ℕ},
    IsAdmissible m xs✝ ↔ List.IsChain (fun x1 x2 ↦ x1 < x2) xs✝ ∧ ∀ (k : ℕ) (h : k < xs✝.length), xs✝[k] ≤ m + k
IH :
  ∀ (y : ℕ) {m : ℕ},
    IsAdmissible m (y :: xs✝) ↔
      List.IsChain (fun x1 x2 ↦ x1 < x2) (y :: xs✝) ∧ ∀ (k : ℕ) (h : k < (y :: xs✝).length), (y :: xs✝)[k] ≤ m + k
m : ℕ
x✝¹ : x✝² < y✝
x✝ : List.IsChain (fun x1 x2 ↦ x1 < x2) (y✝ :: xs✝)
h : ∀ (k : ℕ) (h : k < xs✝.length + 1 + 1), (x✝² :: y✝ :: xs✝)[k] ≤ m + k
⊢ 0 < xs✝.length + 1 + 1

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: x✝³ y✝ : ℕ
xs✝ : List ℕ
a✝ :
  ∀ {m : ℕ},
    IsAdmissible m xs✝ ↔ List.IsChain (fun x1 x2 ↦ x1 < x2) xs✝ ∧ ∀ (k : ℕ) (h : k < xs✝.length), xs✝[k] ≤ m + k
IH :
  ∀ (y : ℕ) {m : ℕ},
    IsAdmissible m (y :: xs✝) ↔
      List.IsChain (fun x1 x2 ↦ x1 < x2) (y :: xs✝) ∧ ∀ (k : ℕ) (h : k < (y :: xs✝).length), (y :: xs✝)[k] ≤ m + k
m : ℕ
x✝² : x✝³ < y✝
x✝¹ : List.IsChain (fun x1 x2 ↦ x1 < x2) (y✝ :: xs✝)
h : ∀ (k : ℕ) (h : k < xs✝.length + 1 + 1), (x✝³ :: y✝ :: xs✝)[k] ≤ m + k
k : ℕ
x✝ : k < xs✝.length + 1
⊢ k + 1 < xs✝.length + 1 + 1

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: x✝³ y✝ : ℕ
xs✝ : List ℕ
a✝ :
  ∀ {m : ℕ},
    IsAdmissible m xs✝ ↔ List.IsChain (fun x1 x2 ↦ x1 < x2) xs✝ ∧ ∀ (k : ℕ) (h : k < xs✝.length), xs✝[k] ≤ m + k
IH :
  ∀ (y : ℕ) {m : ℕ},
    IsAdmissible m (y :: xs✝) ↔
      List.IsChain (fun x1 x2 ↦ x1 < x2) (y :: xs✝) ∧ ∀ (k : ℕ) (h : k < (y :: xs✝).length), (y :: xs✝)[k] ≤ m + k
m : ℕ
x✝² : x✝³ < y✝
x✝¹ : List.IsChain (fun x1 x2 ↦ x1 < x2) (y✝ :: xs✝)
h : ∀ (k : ℕ) (h : k < xs✝.length + 1 + 1), (x✝³ :: y✝ :: xs✝)[k] ≤ m + k
k : ℕ
x✝ : k < xs✝.length + 1
⊢ m + (k + 1) ≤ m + 1 + k

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case nil
m a : ℕ
h : IsAdmissible m [a]
⊢ IsAdmissible (m + 1) []

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case cons
m a head✝ : ℕ
tail✝ : List ℕ
h : IsAdmissible m (a :: head✝ :: tail✝)
⊢ IsAdmissible (m + 1) (head✝ :: tail✝)

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case nil
m a : ℕ
ha : a ≤ m
hL : IsAdmissible (m + 1) []
ha' : ∀ (x : 0 < [].length), a < [][0]
⊢ IsAdmissible m [a]

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case cons
m a : ℕ
ha : a ≤ m
head✝ : ℕ
tail✝ : List ℕ
hL : IsAdmissible (m + 1) (head✝ :: tail✝)
ha' : ∀ (x : 0 < (head✝ :: tail✝).length), a < (head✝ :: tail✝)[0]
⊢ IsAdmissible m (a :: head✝ :: tail✝)

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: m✝¹ m✝ a b : ℕ
L✝ : List ℕ
m : ℕ
L : List ℕ
hl : IsAdmissible m L
k : ℕ
hK : k < L.length
⊢ L[k] ≤ m + k

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: m✝¹ m✝ a✝ b : ℕ
L✝ : List ℕ
m a : ℕ
L : List ℕ
hl : IsAdmissible m (a :: L)
⊢ 0 < (a :: L).length

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: m : ℕ
L : List ℕ
n : ℕ
hmn : m ≤ n
hL : IsAdmissible m L
⊢ List.IsChain (fun x1 x2 ↦ x1 < x2) L

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: m : ℕ
L : List ℕ
n : ℕ
hmn : m ≤ n
hL : IsAdmissible m L
⊢ ∀ (k : ℕ) (h : k < L.length), L[k] ≤ n + k

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case nil
a : ℕ
⊢ (simplicialInsert a []).length = [].length + 1

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case cons
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

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case cons.nil
a m j : ℕ
hj : j ≤ m
h_rec : ∀ (m : ℕ), IsAdmissible (m + 1) [] → ∀ j ≤ m, IsAdmissible m (simplicialInsert j [])
hL : IsAdmissible (m + 1) [a]
⊢ IsAdmissible m (simplicialInsert j [a])

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case cons.cons
a m j : ℕ
hj : j ≤ m
head✝ : ℕ
tail✝ : List ℕ
h_rec : ∀ (m : ℕ), IsAdmissible (m + 1) (head✝ :: tail✝) → ∀ j ≤ m, IsAdmissible m (simplicialInsert j (head✝ :: tail✝))
hL : IsAdmissible (m + 1) (a :: head✝ :: tail✝)
⊢ IsAdmissible m (simplicialInsert j (a :: head✝ :: tail✝))

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: L : List ℕ
m₁ m₂ : ℕ
h : m₂ + [].length = m₁
⊢ mk m₁ = mk m₂

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: L : List ℕ
m₁ m₂ a : ℕ
t : List ℕ
h : m₂ + (a :: t).length = m₁
⊢ m₂ + 1 + t.length = m₁

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: m : ℕ
⊢ m + [].length = m

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: L : List ℕ
a m₁ m₂ : ℕ
h : m₂ + (a :: L).length = m₁
⊢ m₂ + 1 + L.length = m₁

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: L₁ L₂ : List ℕ
m₁ m₂ m₃ : ℕ
h : m₂ + L₁.length = m₁
h' : m₃ + L₂.length = m₂
⊢ m₃ + (L₂ ++ L₁).length = m₁

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: L₁ : List ℕ
m₁ m₂ m₃ : ℕ
h : m₂ + L₁.length = m₁
h' : m₃ + [].length = m₂
⊢ m₃ = m₂

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: 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

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: 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

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: 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

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case nil
L : List ℕ
j : ℕ
hj : ∀ k ∈ [], j ≤ k
⊢ simplicialEvalσ [] j = j

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case cons
L : List ℕ
j head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : (∀ k ∈ tail✝, j ≤ k) → simplicialEvalσ tail✝ j = j
hj : j ≤ head✝ ∧ ∀ x ∈ tail✝, j ≤ x
⊢ simplicialEvalσ (head✝ :: tail✝) j = j

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: L : List ℕ
j m₁ m₂ : ℕ
hL : IsAdmissible m₂ []
hk : m₂ + [].length = m₁
hj : j < m₁ + 1
⊢ m₁ = m₂

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case pos
L✝ : List ℕ
j a : ℕ
L : List ℕ
h_rec :
  ∀ (m₁ m₂ : ℕ),
    IsAdmissible m₂ L →
      ∀ (hk : m₂ + L.length = m₁) (hj : j < m₁ + 1),
        ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L hk))) ⟨j, hj⟩) = simplicialEvalσ L j
m₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
t : Fin (m₂ + 2)
h₁ : hL.head.castSucc < t
h₂ : a < ↑t
⊢ ↑(t.pred ⋯) = ↑t - 1

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case neg
L✝ : List ℕ
j a : ℕ
L : List ℕ
h_rec :
  ∀ (m₁ m₂ : ℕ),
    IsAdmissible m₂ L →
      ∀ (hk : m₂ + L.length = m₁) (hj : j < m₁ + 1),
        ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L hk))) ⟨j, hj⟩) = 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
h₁ : a < ↑t
⊢ ↑(t.pred ⋯) = ↑t

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case pos
L✝ : List ℕ
j a : ℕ
L : List ℕ
h_rec :
  ∀ (m₁ m₂ : ℕ),
    IsAdmissible m₂ L →
      ∀ (hk : m₂ + L.length = m₁) (hj : j < m₁ + 1),
        ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L hk))) ⟨j, hj⟩) = 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
h₁ : ↑t ≤ a
⊢ ↑(t.castPred ⋯) = ↑t - 1

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case neg
L✝ : List ℕ
j a : ℕ
L : List ℕ
h_rec :
  ∀ (m₁ m₂ : ℕ),
    IsAdmissible m₂ L →
      ∀ (hk : m₂ + L.length = m₁) (hj : j < m₁ + 1),
        ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L hk))) ⟨j, hj⟩) = simplicialEvalσ L j
m₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
t : Fin (m₂ + 2)
h₁ : ¬hL.head.castSucc < t
h₂ : ¬a < ↑t
⊢ ↑(t.castPred ⋯) = ↑t

Tactic:
rfl

Goal state after: