mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
⊢ δ i ≫ δ j = δ i ≫ δ j

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
⊢ δ j ≫ δ (i.castLT ⋯).castSucc = δ j ≫ δ i

pp: n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
⊢ i.castLT ⋯ ≤ j

Tactic:
]

Goal state after:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
⊢ δ j ≫ δ (i.castLT ⋯).castSucc = δ j ≫ δ i

n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
⊢ i.castLT ⋯ ≤ j
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ δ i ≫ δ i.succ = δ i ≫ δ i.succ

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
⊢ (j.predAbove k).succ = (j.predAbove k).succ

pp: case inl.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
⊢ i ≤ (j.predAbove k).castSucc

Tactic:
]

Goal state after:
case inl.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
⊢ i ≤ (j.predAbove k).castSucc
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inl.h.inl
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
hjk : k ≤ j.castSucc
⊢ i ≤ k

Tactic:
]

Goal state after:
case inl.h.inl
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
hjk : k ≤ j.castSucc
⊢ i ≤ k
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inl.h.inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
hjk : j.castSucc < k
⊢ i < k

Tactic:
]

Goal state after:
case inl.h.inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
hjk : j.castSucc < k
⊢ i < k
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : k < i
⊢ j.succ.predAbove k.castSucc = i.succAbove (j.predAbove k)

Tactic:
]

Goal state after:
case inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : k < i
⊢ j.succ.predAbove k.castSucc = i.succAbove (j.predAbove k)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : k < i
hjk : k < j.castSucc
⊢ k = k

pp: case inr.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : k < i
hjk : k < j.castSucc
⊢ (k.castPred ⋯).castSucc < i

Tactic:
]

Goal state after:
case inr.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : k < i
hjk : k < j.castSucc
⊢ (k.castPred ⋯).castSucc < i
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
P✝ Q : Karoubi (J ⥤ C)
f : P✝ ⟶ Q
X : J
P : Karoubi (J ⥤ C)
j j' : J
φ : j ⟶ j'
h : P.p.app j ≫ P.p.app j = P.p.app j
⊢ P.p.app j ≫ P.p.app j ≫ P.p.app j ≫ P.X.map φ = P.p.app j ≫ P.X.map φ

Tactic:
]

Goal state after:
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
P✝ Q : Karoubi (J ⥤ C)
f : P✝ ⟶ Q
X : J
P : Karoubi (J ⥤ C)
j j' : J
φ : j ⟶ j'
h : P.p.app j ≫ P.p.app j = P.p.app j
⊢ P.p.app j ≫ P.p.app j ≫ P.p.app j ≫ P.X.map φ = P.p.app j ≫ P.X.map φ
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
P✝ Q : Karoubi (J ⥤ C)
f : P✝ ⟶ Q
X : J
P : Karoubi (J ⥤ C)
j j' : J
φ : j ⟶ j'
h : P.p.app j ≫ P.p.app j = P.p.app j
⊢ P.p.app j ≫ P.X.map φ = P.p.app j ≫ P.X.map φ

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inr.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : k < i
hjk : k < j.castSucc
⊢ k < i

Tactic:
]

Goal state after:
case inr.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : k < i
hjk : k < j.castSucc
⊢ k < i
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
P✝ Q✝ : Karoubi (J ⥤ C)
f✝ : P✝ ⟶ Q✝
X : J
P Q : Karoubi (J ⥤ C)
f : (karoubiFunctorCategoryEmbedding J C).obj P ⟶ (karoubiFunctorCategoryEmbedding J C).obj Q
j j' : J
φ : j ⟶ j'
⊢ P.X.map φ ≫ (f.app j').f = (f.app j).f ≫ (((karoubiFunctorCategoryEmbedding J C).obj Q).obj j).p ≫ Q.X.map φ

Tactic:
]

Goal state after:
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
P✝ Q✝ : Karoubi (J ⥤ C)
f✝ : P✝ ⟶ Q✝
X : J
P Q : Karoubi (J ⥤ C)
f : (karoubiFunctorCategoryEmbedding J C).obj P ⟶ (karoubiFunctorCategoryEmbedding J C).obj Q
j j' : J
φ : j ⟶ j'
⊢ P.X.map φ ≫ (f.app j').f = (f.app j).f ≫ (((karoubiFunctorCategoryEmbedding J C).obj Q).obj j).p ≫ Q.X.map φ
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
P✝ Q✝ : Karoubi (J ⥤ C)
f✝ : P✝ ⟶ Q✝
X : J
P Q : Karoubi (J ⥤ C)
f : (karoubiFunctorCategoryEmbedding J C).obj P ⟶ (karoubiFunctorCategoryEmbedding J C).obj Q
j j' : J
φ : j ⟶ j'
h : (P.p.app j ≫ P.X.map φ) ≫ (f.app j').f = (f.app j).f ≫ Q.p.app j ≫ Q.X.map φ
⊢ P.X.map φ ≫ (f.app j').f = P.X.map φ ≫ P.p.app j' ≫ (f.app j').f

Tactic:
]

Goal state after:
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
P✝ Q✝ : Karoubi (J ⥤ C)
f✝ : P✝ ⟶ Q✝
X : J
P Q : Karoubi (J ⥤ C)
f : (karoubiFunctorCategoryEmbedding J C).obj P ⟶ (karoubiFunctorCategoryEmbedding J C).obj Q
j j' : J
φ : j ⟶ j'
h : (P.p.app j ≫ P.X.map φ) ≫ (f.app j').f = (f.app j).f ≫ Q.p.app j ≫ Q.X.map φ
⊢ P.X.map φ ≫ (f.app j').f = P.X.map φ ≫ P.p.app j' ≫ (f.app j').f
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ 𝟙 ⦋n⦌ = 𝟙 ⦋n⦌

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case h.e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ X.δ j ≫ X.δ i = X.δ (i, j).2 ≫ X.δ (i, j).1

pp: case h.e_a.H
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ (i, j).2 ≤ (i, j).1.castSucc

Tactic:
]

Goal state after:
case h.e_a.H
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ (i, j).2 ≤ (i, j).1.castSucc
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
n : ℕ
⊢ ∑ j, f.app (op ⦋n + 1⦌) ≫ ((-1) ^ ↑j • Y.δ j) = ∑ j, ((-1) ^ ↑j • X.δ j) ≫ f.app (op ⦋n⦌)

Tactic:
]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
n : ℕ
⊢ ∑ j, f.app (op ⦋n + 1⦌) ≫ ((-1) ^ ↑j • Y.δ j) = ∑ j, ((-1) ^ ↑j • X.δ j) ≫ f.app (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
⊢ j.castSucc.predAbove k.castSucc = i.succAbove (j.predAbove k)

Tactic:
]

Goal state after:
case inl
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
⊢ j.castSucc.predAbove k.castSucc = i.succAbove (j.predAbove k)
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
n : ℕ
x✝¹ : Fin (n + 2)
x✝ : x✝¹ ∈ Finset.univ
⊢ (-1) ^ ↑x✝¹ • f.app (op ⦋n + 1⦌) ≫ Y.δ x✝¹ = (-1) ^ ↑x✝¹ • X.δ x✝¹ ≫ f.app (op ⦋n⦌)

Tactic:
]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
n : ℕ
x✝¹ : Fin (n + 2)
x✝ : x✝¹ ∈ Finset.univ
⊢ (-1) ^ ↑x✝¹ • f.app (op ⦋n + 1⦌) ≫ Y.δ x✝¹ = (-1) ^ ↑x✝¹ • X.δ x✝¹ ≫ f.app (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inl.inl
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
hjk : k ≤ j.castSucc
⊢ k = k

pp: case inl.inl.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
hjk : k ≤ j.castSucc
⊢ (k.castPred ⋯).castSucc < i

Tactic:
]

Goal state after:
case inl.inl.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
hjk : k ≤ j.castSucc
⊢ (k.castPred ⋯).castSucc < i
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inl.inl.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
hjk : k ≤ j.castSucc
⊢ k < i

Tactic:
]

Goal state after:
case inl.inl.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
hjk : k ≤ j.castSucc
⊢ k < i
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inl.inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
hjk : j.castSucc < k
⊢ k.castSucc.pred ⋯ = k.castSucc.pred ⋯

pp: case inl.inr.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
hjk : j.castSucc < k
⊢ (k.pred ⋯).castSucc < i

Tactic:
]

Goal state after:
case inl.inr.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
hjk : j.castSucc < k
⊢ (k.pred ⋯).castSucc < i
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inl.inr.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
hjk : j.castSucc < k
⊢ k ≤ i

Tactic:
]

Goal state after:
case inl.inr.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
hjk : j.castSucc < k
⊢ k ≤ i
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : i < k
⊢ j.castSucc.predAbove k.succ = i.succAbove (j.predAbove k)

Tactic:
]

Goal state after:
case inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : i < k
⊢ j.castSucc.predAbove k.succ = i.succAbove (j.predAbove k)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : i < k
hjk : j.castSucc < k
⊢ k = k

pp: case inr.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : i < k
hjk : j.castSucc < k
⊢ i ≤ (k.pred ⋯).castSucc

Tactic:
]

Goal state after:
case inr.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : i < k
hjk : j.castSucc < k
⊢ i ≤ (k.pred ⋯).castSucc
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inr.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : i < k
hjk : j.castSucc < k
⊢ i < k

Tactic:
]

Goal state after:
case inr.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : i < k
hjk : j.castSucc < k
⊢ i < k
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ δ i ≫ σ j = δ (i.pred ⋯).succ ≫ σ (j.castLT ⋯).castSucc

pp: n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ (j.castLT ⋯).castSucc < i.pred ⋯

Tactic:
]

Goal state after:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ δ i ≫ σ j = δ (i.pred ⋯).succ ≫ σ (j.castLT ⋯).castSucc

n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ (j.castLT ⋯).castSucc < i.pred ⋯
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ j.succ < i

Tactic:
]

Goal state after:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ j.succ < i
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ X.δ i.succ ≫ X.δ i = X.δ i.succ ≫ X.δ i

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case cast.succ.inl
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
⊢ j.predAbove k.castSucc = j.predAbove k.castSucc

pp: n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
⊢ i ≤ j.predAbove k.castSucc

Tactic:
]

Goal state after:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
⊢ i ≤ j.predAbove k.castSucc
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inl
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
hkj : k ≤ j
⊢ i ≤ k

Tactic:
]

Goal state after:
case inl
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
hkj : k ≤ j
⊢ i ≤ k
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inr
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
hkj : j < k
⊢ i < k

Tactic:
]

Goal state after:
case inr
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
hkj : j < k
⊢ i < k
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case cast.succ.inr
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : k < i
⊢ k.succ.castPred ⋯ = k.succ.castPred ⋯

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ 𝟙 (X _⦋n⦌) = 𝟙 (X _⦋n⦌)

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case cast.succ.inr
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : k < i
⊢ j.predAbove (i.castSucc.predAbove k.succ.castSucc) = i.predAbove (j.succ.predAbove k.succ.castSucc)

Tactic:
· simp_rw [Fin.predAbove_of_le_castSucc i.castSucc _ (Fin.castSucc_le_castSucc_iff.mpr
        (Fin.succ_le_castSucc_iff.mpr h)), Fin.castPred_castSucc, ← Fin.succ_castSucc,
        Fin.succ_predAbove_succ]
        rw [Fin.predAbove_of_le_castSucc _ k.castSucc
        (Fin.castSucc_le_castSucc_iff.mpr (h.le.trans H)),
        Fin.castPred_castSucc, Fin.predAbove_of_le_castSucc _ k.succ
        (Fin.succ_le_castSucc_iff.mpr (H.trans_lt' h)), Fin.predAbove_of_le_castSucc _ k.succ
        (Fin.succ_le_castSucc_iff.mpr h)]

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ ((AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)).d (n + 1) n).f =
    P.p.app (op ⦋n + 1⦌) ≫ (AlternatingFaceMapComplex.obj P.X).d (n + 1) n

Tactic:
simp only [AlternatingFaceMapComplex.obj_d_eq, Karoubi.sum_hom, Preadditive.comp_sum,
    Karoubi.zsmul_hom, Preadditive.comp_zsmul]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ ∑ x, (-1) ^ ↑x • (SimplicialObject.δ (KaroubiFunctorCategoryEmbedding.obj P) x).f =
    ∑ x, (-1) ^ ↑x • P.p.app (op ⦋n + 1⦌) ≫ P.X.δ x
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X : SimplicialObject C
n : ℕ
inst✝¹ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F
inst✝ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F
⊢ IsLeftKanExtension ((Truncated.sk n).obj ((truncation n).obj X))
    ((SimplexCategory.Truncated.inclusion n).op.lanUnit.app ((truncation n).obj X))

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X : SimplicialObject C
n : ℕ
inst✝¹ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F
inst✝ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F
⊢ IsLeftKanExtension ((Truncated.sk n).obj ((truncation n).obj X))
    ((SimplexCategory.Truncated.inclusion n).op.lanUnit.app ((truncation n).obj X))
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
⊢ X.hom.app (op ⦋0 + 1⦌) ≫ ((SimplicialObject.const C).obj X.right).δ 0 +
      -X.hom.app (op ⦋0 + 1⦌) ≫ ((SimplicialObject.const C).obj X.right).δ 1 =
    0

Tactic:
]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
⊢ X.hom.app (op ⦋0 + 1⦌) ≫ ((SimplicialObject.const C).obj X.right).δ 0 +
      -X.hom.app (op ⦋0 + 1⦌) ≫ ((SimplicialObject.const C).obj X.right).δ 1 =
    0
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X : SimplicialObject C
n : ℕ
inst✝¹ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F
inst✝ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F
⊢ IsRightKanExtension ((Truncated.cosk n).obj ((truncation n).obj X))
    ((SimplexCategory.Truncated.inclusion n).op.ranCounit.app ((truncation n).obj X))

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X : SimplicialObject C
n : ℕ
inst✝¹ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F
inst✝ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F
⊢ IsRightKanExtension ((Truncated.cosk n).obj ((truncation n).obj X))
    ((SimplexCategory.Truncated.inclusion n).op.ranCounit.app ((truncation n).obj X))
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case «0»
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ ↑((Hom.toOrderHom (mkOfSucc i)) ((fun i ↦ i) ⟨0, ⋯⟩)).succ =
    ↑((Hom.toOrderHom (mkOfSucc i.succ)) ((fun i ↦ i) ⟨0, ⋯⟩))

pp: case «0».h
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ j ≤ ((Hom.toOrderHom (mkOfSucc i)) ((fun i ↦ i) ⟨0, ⋯⟩)).castSucc

Tactic:
]

Goal state after:
case «0»
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ ↑((Hom.toOrderHom (mkOfSucc i)) ((fun i ↦ i) ⟨0, ⋯⟩)).succ =
    ↑((Hom.toOrderHom (mkOfSucc i.succ)) ((fun i ↦ i) ⟨0, ⋯⟩))

case «0».h
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ j ≤ ((Hom.toOrderHom (mkOfSucc i)) ((fun i ↦ i) ⟨0, ⋯⟩)).castSucc
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case «1»
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ ↑((Hom.toOrderHom (mkOfSucc i)) ((fun i ↦ i) ⟨1, ⋯⟩)).succ =
    ↑((Hom.toOrderHom (mkOfSucc i.succ)) ((fun i ↦ i) ⟨1, ⋯⟩))

pp: case «1».h
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ j ≤ ((Hom.toOrderHom (mkOfSucc i)) ((fun i ↦ i) ⟨1, ⋯⟩)).castSucc

Tactic:
]

Goal state after:
case «1»
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ ↑((Hom.toOrderHom (mkOfSucc i)) ((fun i ↦ i) ⟨1, ⋯⟩)).succ =
    ↑((Hom.toOrderHom (mkOfSucc i.succ)) ((fun i ↦ i) ⟨1, ⋯⟩))

case «1».h
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ j ≤ ((Hom.toOrderHom (mkOfSucc i)) ((fun i ↦ i) ⟨1, ⋯⟩)).castSucc
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X Y : SimplicialObject.Augmented C
f : X ⟶ Y
⊢ f.left.app (op ⦋0⦌) ≫ Y.hom.app (op ⦋0⦌) = X.hom.app (op ⦋0⦌) ≫ f.right

Tactic:
]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X Y : SimplicialObject.Augmented C
f : X ⟶ Y
⊢ f.left.app (op ⦋0⦌) ≫ Y.hom.app (op ⦋0⦌) = X.hom.app (op ⦋0⦌) ≫ f.right
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
A : Augmented C
n : SimplexCategoryᵒᵖ
⊢ η.app (A.left.obj n) ≫ Y✝.map (A.hom.app n) = η.app (A.left.obj n) ≫ Y✝.map (A.hom.app n)

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ X : SimplicialObject C
X₀ : C
f : X _⦋0⦌ ⟶ X₀
w : ∀ (i : SimplexCategory) (g₁ g₂ : ⦋0⦌ ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f
i j : SimplexCategoryᵒᵖ
g : i ⟶ j
⊢ X.map g.unop.op ≫ X.map (⦋0⦌.const (unop j) 0).op ≫ f = (X.map (⦋0⦌.const (unop i) 0).op ≫ f) ≫ 𝟙 X₀

Tactic:
]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ X : SimplicialObject C
X₀ : C
f : X _⦋0⦌ ⟶ X₀
w : ∀ (i : SimplexCategory) (g₁ g₂ : ⦋0⦌ ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f
i j : SimplexCategoryᵒᵖ
g : i ⟶ j
⊢ X.map g.unop.op ≫ X.map (⦋0⦌.const (unop j) 0).op ≫ f = (X.map (⦋0⦌.const (unop i) 0).op ≫ f) ≫ 𝟙 X₀
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case «1»
n : ℕ
i : Fin n
⊢ ↑i.succ.succ = ↑((Hom.toOrderHom (intervalEdge (↑i) 2 ⋯)) 1)

Tactic:
]

Goal state after:
case «1»
n : ℕ
i : Fin n
⊢ ↑i.succ.succ = ↑((Hom.toOrderHom (intervalEdge (↑i) 2 ⋯)) 1)
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
i : ℕ
⊢ (NormalizedMooreComplex.objX X (i + 1)).arrow ≫ ((-1) ^ ↑0 • X.δ 0) + 0 =
    NormalizedMooreComplex.objD X i ≫ (NormalizedMooreComplex.objX X i).arrow

pp: case h
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
i : ℕ
⊢ ∀ (a : Fin (i + 1)), (NormalizedMooreComplex.objX X (i + 1)).arrow ≫ ((-1) ^ ↑a.succ • X.δ a.succ) = 0

Tactic:
]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
i : ℕ
⊢ (NormalizedMooreComplex.objX X (i + 1)).arrow ≫ ((-1) ^ ↑0 • X.δ 0) + 0 =
    NormalizedMooreComplex.objD X i ≫ (NormalizedMooreComplex.objX X i).arrow

case h
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
i : ℕ
⊢ ∀ (a : Fin (i + 1)), (NormalizedMooreComplex.objX X (i + 1)).arrow ≫ ((-1) ^ ↑a.succ • X.δ a.succ) = 0
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n m : ℕ
h : n = m
⊢ ⦋m⦌ = ⦋m⦌

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ X.δ i ≫ X.δ i.succ = X.δ i ≫ X.δ i.succ

Tactic:
]

Goal state after: