mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: case h_map
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
X : J ⥤ C
⊢ autoParam
    (∀ (X_1 Y : J) (f : X_1 ⟶ Y),
      ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).map f =
        eqToHom ⋯ ≫ (((Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).map f ≫ eqToHom ⋯)
    Functor.ext._auto_1

pp: case h_obj.h_obj
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
X : J ⥤ C
⊢ ∀ (X_1 : J),
    ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).obj X_1 =
      (((Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).obj X_1

Tactic:
·

Goal state after:
case h_map
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
X : J ⥤ C
⊢ autoParam
    (∀ (X_1 Y : J) (f : X_1 ⟶ Y),
      ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).map f =
        eqToHom ⋯ ≫ (((Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).map f ≫ eqToHom ⋯)
    Functor.ext._auto_1
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) hij).2 ≫ X.δ (φ (i, j) hij).1

Tactic:
·

Goal state after:
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) hij).2 ≫ X.δ (φ (i, j) hij).1
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: case h_obj.h_obj
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
X : J ⥤ C
⊢ ∀ (X_1 : J),
    ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).obj X_1 =
      (((Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).obj X_1

Tactic:
·

Goal state after:
case h_obj.h_obj
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
X : J ⥤ C
⊢ ∀ (X_1 : J),
    ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).obj X_1 =
      (((Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).obj X_1
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 (i.succ.succAbove k) = i.succAbove (j.predAbove k)

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 (i.succ.succAbove k) = 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 (i.succ.succAbove k) = i.succAbove (j.predAbove k)
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
⊢ j.castSucc.predAbove k.castSucc = i.succAbove (j.predAbove k)

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
⊢ j.castSucc.predAbove k.castSucc = i.succAbove (j.predAbove k)

Tactic:
·

Goal state after:
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
⊢ j.castSucc.predAbove k.castSucc = i.succAbove (j.predAbove k)
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
⊢ j.castSucc.predAbove k.castSucc = i.succAbove (j.predAbove k)

Tactic:
·

Goal state after:
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
⊢ j.castSucc.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 : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : i < k
⊢ j.castSucc.predAbove (i.succ.succAbove k) = 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 (i.succ.succAbove k) = i.succAbove (j.predAbove k)
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case h_map
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
⊢ autoParam
    (∀ (X Y : SimplicialObject C) (f : X ⟶ Y),
      (alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).map f =
        eqToHom ⋯ ≫ ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).map f ≫ eqToHom ⋯)
    Functor.ext._auto_1

pp: case h_obj
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
⊢ ∀ (X : SimplicialObject C),
    (alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).obj X =
      ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X

Tactic:
·

Goal state after:
case h_map
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
⊢ autoParam
    (∀ (X Y : SimplicialObject C) (f : X ⟶ Y),
      (alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).map f =
        eqToHom ⋯ ≫ ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).map f ≫ eqToHom ⋯)
    Functor.ext._auto_1
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
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
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
⊢ (j.castLT ⋯).castSucc < i.pred ⋯
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case h_obj
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
⊢ ∀ (X : SimplicialObject C),
    (alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).obj X =
      ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X

Tactic:
·

Goal state after:
case h_obj
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
⊢ ∀ (X : SimplicialObject C),
    (alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).obj X =
      ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X
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 (i.castSucc.predAbove k.succ.castSucc) = i.predAbove (j.succ.predAbove k.succ.castSucc)

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:
·

Goal state after:
case cast.succ.inl
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
⊢ j.predAbove (i.castSucc.predAbove k.succ.castSucc) = i.predAbove (j.succ.predAbove k.succ.castSucc)
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case h_obj.h_d
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
X : SimplicialObject C
⊢ ∀ (i j : ℕ),
    (ComplexShape.down ℕ).Rel i j →
      ((alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).obj X).d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ (((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X).d i j

pp: case h_obj.h_X
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
X : SimplicialObject C
⊢ ((alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).obj X).X =
    (((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X).X

Tactic:
·

Goal state after:
case h_obj.h_d
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
X : SimplicialObject C
⊢ ∀ (i j : ℕ),
    (ComplexShape.down ℕ).Rel i j →
      ((alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).obj X).d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ (((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X).d i j
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 ≤ j.predAbove k.castSucc

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

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 ≤ j.predAbove k.castSucc
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 ≤ j.predAbove k.castSucc

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 ≤ j.predAbove k.castSucc
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:
·

Goal state after:
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)
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case h_obj.h_X
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
X : SimplicialObject C
⊢ ((alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).obj X).X =
    (((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X).X

Tactic:
·

Goal state after:
case h_obj.h_X
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
X : SimplicialObject C
⊢ ((alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).obj X).X =
    (((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X).X
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

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

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

Tactic:
·

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

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

Tactic:
·

Goal state after:
case «1»
n : ℕ
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
⊢ ↑((Hom.toOrderHom (mkOfSucc i ≫ δ j)) ((fun i ↦ i) ⟨1, ⋯⟩)) =
    ↑((Hom.toOrderHom (mkOfSucc i.castSucc)) ((fun i ↦ i) ⟨1, ⋯⟩))
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

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 «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, ⋯⟩))
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

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

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 «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, ⋯⟩))
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
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».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.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) ≫ 𝟙 (Y✝.obj A.right) =
    (X✝.map (A.hom.app n) ≫ 𝟙 (X✝.obj A.right)) ≫ η.app A.right

Tactic:
rw [Category.comp_id, Category.comp_id, η.naturality]

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

Goal state before:
pp: n : ℕ
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
⊢ ↑i + 2 ≤ n + 1

Tactic:
by lia

Goal state after:
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 ≫ δ j)) ((fun i ↦ i) ⟨0, ⋯⟩)) =
    ↑((Hom.toOrderHom (intervalEdge (↑i) 2 ⋯)) ((fun i ↦ i) ⟨0, ⋯⟩))

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

Tactic:
·

Goal state after:
case «0»
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j = i.succ.castSucc
⊢ ↑((Hom.toOrderHom (mkOfSucc i ≫ δ j)) ((fun i ↦ i) ⟨0, ⋯⟩)) =
    ↑((Hom.toOrderHom (intervalEdge (↑i) 2 ⋯)) ((fun i ↦ i) ⟨0, ⋯⟩))
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 ≫ δ j)) ((fun i ↦ i) ⟨1, ⋯⟩)) =
    ↑((Hom.toOrderHom (intervalEdge (↑i) 2 ⋯)) ((fun i ↦ i) ⟨1, ⋯⟩))

Tactic:
·

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

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

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

Tactic:
·

Goal state after:
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 : ℕ
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J (Truncated C n)

Tactic:
by
  dsimp [Truncated]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J (Truncated C n)

Tactic:
by
  dsimp [Truncated]
  infer_instance

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

Goal state before:
pp: i n m : ℕ
hi : n + i = m
j : Fin (⦋n⦌.len + 1)
⊢ ↑j + i < ⦋m⦌.len + 1

Tactic:
by lia

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

Goal state before:
pp: i n m : ℕ
j : Fin (n + 1)
hi : autoParam (n + i = m) δ₀Iter_apply._auto_1
⊢ ↑j + i < ⦋m⦌.len + 1

Tactic:
by lia

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : n + 0 = m
hi'' : ↑i' = ↑i + 0
⊢ n = m

Tactic:
by lia

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
h : n + (i + 1) = m
⊢ X.δ₀Iter (i + 1) h = X.δ₀Iter i ⋯ ≫ X.δ 0

Tactic:
by
  dsimp [δ, δ₀Iter]
  rw [← Functor.map_comp, ← op_comp, SimplexCategory.δ₀Iter_succ' _ h]

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

Goal state before:
pp: n : ℕ
i i' : Fin (n + 2)
h : n + 0 = n
hi'' : ↑i' = ↑i + 0
⊢ i = i'

Tactic:
by lia

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

Goal state before:
pp: case pos
A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
y₁ y₂ : Fin (B✝.len + 1)
h : y₁ ≤ y₂
h' : y₁ < y₂
⊢ (ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₁ ≤
    (ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₂

pp: case neg
A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
y₁ y₂ : Fin (B✝.len + 1)
h : y₁ ≤ y₂
h' : ¬y₁ < y₂
⊢ (ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₁ ≤
    (ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₂

Tactic:
·

Goal state after:
case pos
A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
y₁ y₂ : Fin (B✝.len + 1)
h : y₁ ≤ y₂
h' : y₁ < y₂
⊢ (ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₁ ≤
    (ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₂
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case neg
A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
y₁ y₂ : Fin (B✝.len + 1)
h : y₁ ≤ y₂
h' : ¬y₁ < y₂
⊢ (ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₁ ≤
    (ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₂

Tactic:
·

Goal state after:
case neg
A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
y₁ y₂ : Fin (B✝.len + 1)
h : y₁ ≤ y₂
h' : ¬y₁ < y₂
⊢ (ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₁ ≤
    (ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₂
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi' : n + 0 = m
hj' : ↑j = ↑j' + 0
⊢ n = m

Tactic:
by lia

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

Goal state before:
pp: case pos
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h' : x ≤ i.castSucc
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) ((Hom.toOrderHom (δ i.succ)) (i.predAbove x))

pp: case neg
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h' : ¬x ≤ i.castSucc
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) ((Hom.toOrderHom (δ i.succ)) (i.predAbove x))

Tactic:
·

Goal state after:
case pos
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h' : x ≤ i.castSucc
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) ((Hom.toOrderHom (δ i.succ)) (i.predAbove x))
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: n : ℕ
j' j : Fin (n + 1)
hi' : n + 0 = n
hj' : ↑j = ↑j' + 0
⊢ j = j'

Tactic:
by lia

Goal state after: