mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Fin.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableEq α
a b c : α
hab : a < b
hbc : b < c
⊢ c ∈ {a, b, c}

Tactic:
simp

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

Goal state before:
pp: n : ℕ
α : Type u
inst✝ : Preorder α
e : α ≃o Fin (n + 1)
X✝ : SimplexCategory
F : Fin (X✝.len + 1) ⥤ Fin (⦋n⦌.len + 1)
x : Fin (X✝.len + 1)
⊢ ((fun F ↦ F ⋙ ⋯.functor) ((fun F ↦ F ⋙ ⋯.functor) F)).obj x = F.obj x

Tactic:
simp

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

Goal state before:
pp: n : ℕ
α : Type u
inst✝ : Preorder α
e : α ≃o Fin (n + 1)
X✝ : SimplexCategory
F : (nerve α).obj (op X✝)
x : Fin ((unop (op X✝)).len + 1)
⊢ ((fun F ↦ F ⋙ ⋯.functor) ((fun F ↦ F ⋙ ⋯.functor) F)).obj x = F.obj x

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x : C
⊢ ComposableArrows.hom ((ConcreteCategory.hom (SimplicialObject.σ (nerve C) 0)) (ComposableArrows.mk₀ x)) =
    eqToHom ⋯ ≫ (ComposableArrows.mk₁ (𝟙 x)).hom ≫ eqToHom ⋯

Tactic:
simp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
x : C
⊢ ((ConcreteCategory.hom (SimplicialObject.σ (nerve C) 0)) (ComposableArrows.mk₀ x)).hom = eqToHom ⋯
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom ((ConcreteCategory.hom (SimplicialObject.δ (nerve C) 2)) (ComposableArrows.mk₂ f g)) =
    eqToHom ⋯ ≫ (ComposableArrows.mk₁ f).hom ≫ eqToHom ⋯

Tactic:
simp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom ((ConcreteCategory.hom (SimplicialObject.δ (nerve C) 2)) (ComposableArrows.mk₂ f g)) = f
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom ((ConcreteCategory.hom (SimplicialObject.δ (nerve C) 0)) (ComposableArrows.mk₂ f g)) =
    eqToHom ⋯ ≫ (ComposableArrows.mk₁ g).hom ≫ eqToHom ⋯

Tactic:
simp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom ((ConcreteCategory.hom (SimplicialObject.δ (nerve C) 0)) (ComposableArrows.mk₂ f g)) = g
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom ((ConcreteCategory.hom (SimplicialObject.δ (nerve C) 1)) (ComposableArrows.mk₂ f g)) =
    eqToHom ⋯ ≫ (ComposableArrows.mk₁ (f ≫ g)).hom ≫ eqToHom ⋯

Tactic:
simp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom ((ConcreteCategory.hom (SimplicialObject.δ (nerve C) 1)) (ComposableArrows.mk₂ f g)) = f ≫ g
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
n : ℕ
x y : ComposableArrows C 0
e : Edge x y
⊢ nerveEquiv x = ComposableArrows.left e.edge

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
n : ℕ
x y : ComposableArrows C 0
e : Edge x y
⊢ ComposableArrows.right e.edge = nerveEquiv y

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
n : ℕ
x y : ComposableArrows C 0
f : nerveEquiv x ⟶ nerveEquiv y
⊢ (fun e ↦ eqToHom ⋯ ≫ ComposableArrows.hom e.edge ≫ eqToHom ⋯) ((fun f ↦ Edge.mk (ComposableArrows.mk₁ f) ⋯ ⋯) f) = f

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x y : C
e : Edge (nerveEquiv.symm x) (nerveEquiv.symm y)
⊢ x = nerveEquiv (nerveEquiv.symm x)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x y : C
e : Edge (nerveEquiv.symm x) (nerveEquiv.symm y)
⊢ nerveEquiv (nerveEquiv.symm y) = y

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.AlternatingConst

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
h : Even (n + 1)
⊢ n + 1 ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.AlternatingConst

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
i✝ : ℕ
⊢ ((Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C).map f✝ ≫
          (HomologicalComplex.Hom.isoOfComponents
              (fun x ↦ Iso.refl (((Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C).obj Y✝).X x))
              ⋯).hom).f
      i✝ =
    ((HomologicalComplex.Hom.isoOfComponents
              (fun x ↦ Iso.refl (((Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C).obj X✝).X x)) ⋯).hom ≫
          ChainComplex.alternatingConst.map f✝).f
      i✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Bifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C₁
inst✝³ : Category.{v_2, u_2} C₂
inst✝² : Category.{v_3, u_3} C₃
F : C₁ ⥤ C₂ ⥤ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X₁ X₂ : GradedObject I C₁
Y₁ Y₂ : GradedObject J C₂
inst✝¹ : (((mapBifunctor F I J).obj X₁).obj Y₁).HasMap p
inst✝ : (((mapBifunctor F I J).obj X₂).obj Y₂).HasMap p
e : X₁ ≅ X₂
e' : Y₁ ≅ Y₂
x✝ : K
i✝ : I
j✝ : J
hij✝ : p (i✝, j✝) = x✝
⊢ ιMapBifunctorMapObj F p X₁ Y₁ i✝ j✝ x✝ hij✝ ≫
      (mapBifunctorMapMap F p e.hom e'.hom ≫ mapBifunctorMapMap F p e.inv e'.inv) x✝ =
    ιMapBifunctorMapObj F p X₁ Y₁ i✝ j✝ x✝ hij✝ ≫ 𝟙 (mapBifunctorMapObj F p X₁ Y₁) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Bifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝⁴ : Category.{v_1, u_1} C₁
inst✝³ : Category.{v_2, u_2} C₂
inst✝² : Category.{v_3, u_3} C₃
F : C₁ ⥤ C₂ ⥤ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X₁ X₂ : GradedObject I C₁
Y₁ Y₂ : GradedObject J C₂
inst✝¹ : (((mapBifunctor F I J).obj X₁).obj Y₁).HasMap p
inst✝ : (((mapBifunctor F I J).obj X₂).obj Y₂).HasMap p
e : X₁ ≅ X₂
e' : Y₁ ≅ Y₂
x✝ : K
i✝ : I
j✝ : J
hij✝ : p (i✝, j✝) = x✝
⊢ ιMapBifunctorMapObj F p X₂ Y₂ i✝ j✝ x✝ hij✝ ≫
      (mapBifunctorMapMap F p e.inv e'.inv ≫ mapBifunctorMapMap F p e.hom e'.hom) x✝ =
    ιMapBifunctorMapObj F p X₂ Y₂ i✝ j✝ x✝ hij✝ ≫ 𝟙 (mapBifunctorMapObj F p X₂ Y₂) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroObject V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
⊢ (truncate.obj C).d 1 0 ≫ C.d 1 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
i : ℕ
⊢ (ComplexShape.down ℕ).Rel i 0 → 𝟙 (C.X i) ≫ (truncate.obj (C.augment f w)).d i 0 = C.d i 0 ≫ 𝟙 (C.X 0)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
i n✝ : ℕ
⊢ (ComplexShape.down ℕ).Rel i (n✝ + 1) →
    𝟙 (C.X i) ≫ (truncate.obj (C.augment f w)).d i (n✝ + 1) = C.d i (n✝ + 1) ≫ 𝟙 (C.X (n✝ + 1))

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
⊢ ({ f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ }).f 0 =
    (𝟙 (truncate.obj (C.augment f w))).f 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
i : ℕ
⊢ ({ f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ }).f
      (i + 1) =
    (𝟙 (truncate.obj (C.augment f w))).f (i + 1)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
⊢ ({ f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ }).f 0 =
    (𝟙 C).f 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
i : ℕ
⊢ ({ f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ }).f
      (i + 1) =
    (𝟙 C).f (i + 1)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ 1 = 0 → 𝟙 (C.X 0) ≫ C.d 0 0 = 0 ≫ 𝟙 (C.X 0)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ j + 1 + 1 = 0 → 𝟙 (C.X 0) ≫ C.d 0 (j + 1) = 0 ≫ 𝟙 (C.X (j + 1))

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ 1 = 1 →
    𝟙 (C.X 1) ≫ C.d 1 0 =
      (match 1, 0 with
        | 1, 0 => C.d 1 0
        | i.succ, j.succ => C.d (i + 1) (j + 1)
        | x, x_1 => 0) ≫
        𝟙 (C.X 0)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ j + 1 + 1 = 1 →
    𝟙 (C.X 1) ≫ C.d 1 (j + 1) =
      (match 1, j + 1 with
        | 1, 0 => C.d 1 0
        | i.succ, j.succ => C.d (i + 1) (j + 1)
        | x, x_1 => 0) ≫
        𝟙 (C.X (j + 1))

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i n : ℕ
⊢ 1 = n + 2 →
    𝟙 (C.X (n + 1 + 1)) ≫ C.d (n + 2) 0 =
      (match n + 2, 0 with
        | 1, 0 => C.d 1 0
        | i.succ, j.succ => C.d (i + 1) (j + 1)
        | x, x_1 => 0) ≫
        𝟙 (C.X 0)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i n j : ℕ
⊢ j + 1 + 1 = n + 2 →
    𝟙 (C.X (n + 1 + 1)) ≫ C.d (n + 2) (j + 1) =
      (match n + 2, j + 1 with
        | 1, 0 => C.d 1 0
        | i.succ, j.succ => C.d (i + 1) (j + 1)
        | x, x_1 => 0) ≫
        𝟙 (C.X (j + 1))

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ 1 = 0 → 𝟙 (C.X 0) ≫ 0 = C.d 0 0 ≫ 𝟙 (C.X 0)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ j + 1 + 1 = 0 → 𝟙 (C.X 0) ≫ 0 = C.d 0 (j + 1) ≫ 𝟙 (C.X (j + 1))

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ 1 = 1 →
    (𝟙 (C.X 1) ≫
        match 1, 0 with
        | 1, 0 => C.d 1 0
        | i.succ, j.succ => C.d (i + 1) (j + 1)
        | x, x_1 => 0) =
      C.d 1 0 ≫ 𝟙 (C.X 0)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ j + 1 + 1 = 1 →
    (𝟙 (C.X 1) ≫
        match 1, j + 1 with
        | 1, 0 => C.d 1 0
        | i.succ, j.succ => C.d (i + 1) (j + 1)
        | x, x_1 => 0) =
      C.d 1 (j + 1) ≫ 𝟙 (C.X (j + 1))

Tactic:
simp

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

Goal state before:
pp: n : SimplexCategory
m : SimplexCategoryᵒᵖ
a b : (stdSimplex.obj n).obj m
⊢ objEquiv a = objEquiv b ↔ a = b

Tactic:
simp

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

Goal state before:
pp: X : SSet
n : SimplexCategory
inst✝ : DecidableEq (X.obj (op n))
a b : stdSimplex.obj n ⟶ X
⊢ yonedaEquiv a = yonedaEquiv b ↔ a = b

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i n : ℕ
⊢ 1 = n + 2 →
    (𝟙 (C.X (n + 1 + 1)) ≫
        match n + 2, 0 with
        | 1, 0 => C.d 1 0
        | i.succ, j.succ => C.d (i + 1) (j + 1)
        | x, x_1 => 0) =
      C.d (n + 2) 0 ≫ 𝟙 (C.X 0)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i n j : ℕ
⊢ j + 1 + 1 = n + 2 →
    (𝟙 (C.X (n + 1 + 1)) ≫
        match n + 2, j + 1 with
        | 1, 0 => C.d 1 0
        | i.succ, j.succ => C.d (i + 1) (j + 1)
        | x, x_1 => 0) =
      C.d (n + 2) (j + 1) ≫ 𝟙 (C.X (j + 1))

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
⊢ ({
            f := fun x ↦
              match x with
              | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
              | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1)),
            comm' := ⋯ } ≫
          {
            f := fun x ↦
              match x with
              | 0 => 𝟙 (C.X 0)
              | n.succ => 𝟙 (C.X (n + 1)),
            comm' := ⋯ }).f
      0 =
    (𝟙 ((truncate.obj C).augment (C.d 1 0) ⋯)).f 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
n✝ : ℕ
⊢ ({
            f := fun x ↦
              match x with
              | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
              | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1)),
            comm' := ⋯ } ≫
          {
            f := fun x ↦
              match x with
              | 0 => 𝟙 (C.X 0)
              | n.succ => 𝟙 (C.X (n + 1)),
            comm' := ⋯ }).f
      (n✝ + 1) =
    (𝟙 ((truncate.obj C).augment (C.d 1 0) ⋯)).f (n✝ + 1)

Tactic:
simp

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

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 1))
d : ℕ
x : Δ[n] _⦋d⦌
⊢ x ∈ (face S).obj (op ⦋d⦌) ↔ ∀ (i : Fin (d + 1)), x i ∈ S

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
⊢ ({
            f := fun x ↦
              match x with
              | 0 => 𝟙 (C.X 0)
              | n.succ => 𝟙 (C.X (n + 1)),
            comm' := ⋯ } ≫
          {
            f := fun x ↦
              match x with
              | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
              | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1)),
            comm' := ⋯ }).f
      0 =
    (𝟙 C).f 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
n✝ : ℕ
⊢ ({
            f := fun x ↦
              match x with
              | 0 => 𝟙 (C.X 0)
              | n.succ => 𝟙 (C.X (n + 1)),
            comm' := ⋯ } ≫
          {
            f := fun x ↦
              match x with
              | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
              | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1)),
            comm' := ⋯ }).f
      (n✝ + 1) =
    (𝟙 C).f (n✝ + 1)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroObject V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
⊢ C.d 0 1 ≫ (truncate.obj C).d 0 1 = 0

Tactic:
simp

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
⊢ (ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋n⦌))) (yonedaEquiv (𝟙 Δ[n])) = x

Tactic:
simp

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

Goal state before:
pp: case a
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
⊢ Subcomplex.ofSimplex (objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom)) ≤ face S

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
⊢ n = ↑(Fin.rev 0)

Tactic:
simp

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

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
j : SimplexCategory
x✝ : (face S).toSSet.obj (op j)
x : Δ[n].obj (op j)
hx : x ∈ (face S).obj (op j)
i : Fin (j.len + 1)
⊢ (Hom.toOrderHom (objEquiv x)) i ∈ Finset.image ⇑(Hom.toOrderHom (objEquiv x)) ⊤

Tactic:
simp

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

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
j : SimplexCategory
f : j ⟶ ⦋m⦌
i : Fin (j.len + 1)
⊢ (Hom.toOrderHom
        ((fun x ↦
            match x with
            | ⟨x, hx⟩ => Hom.mk { toFun := fun i ↦ e.symm ⟨(Hom.toOrderHom (objEquiv x)) i, ⋯⟩, monotone' := ⋯ })
          ((fun f ↦
              ⟨objMk
                  ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp (e.toOrderEmbedding.toOrderHom.comp (Hom.toOrderHom f))),
                ⋯⟩)
            f)))
      i =
    (Hom.toOrderHom f) i

Tactic:
apply e.symm_apply_apply

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
⊢ X.hom.app (op ⦋n⦌) ≫ ed.s' ≫ X.left.σ₀Iter ↑(Fin.last n) ⋯ = X.hom.app (op ⦋n⦌) ≫ ed.section_.app (op ⦋n⦌)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
⊢ ↑i.castSucc.succ = ↑1 + ↑i

Tactic:
simp

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
⊢ ↑i + 1 = 1 + ↑i
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
j : Fin (n + 1)
⊢ j ∈
      ↑((Equiv.ofBijective
            (fun x ↦
              match x with
              | ⟨x, hx⟩ => ⟨Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ, ⋯⟩)
            ⋯)
          x) ↔
    ∃ i, ↑x i = j

Tactic:
simp

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

Goal state before:
pp: n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
i : Fin (d + 1)
⊢ i ∈ univ

Tactic:
simp

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

Goal state before:
pp: n d : ℕ
S : ↑{S | #S = d + 1}
A : Δ[n].Subcomplex
⊢ ↑(nonDegenerateEquiv'.symm S) ∈ A.obj (op ⦋d⦌) ↔ face ↑S ≤ A

Tactic:
obtain ⟨x, rfl⟩ := nonDegenerateEquiv'.{u}.surjective S

Goal state after:
n d : ℕ
A : Δ[n].Subcomplex
x : ↑(Δ[n].nonDegenerate d)
⊢ ↑(nonDegenerateEquiv'.symm (nonDegenerateEquiv' x)) ∈ A.obj (op ⦋d⦌) ↔ face ↑(nonDegenerateEquiv' x) ≤ A
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
⊢ Subcomplex.ofSimplex (objEquiv.symm (𝟙 ⦋n⦌)) ≤ ⊤

Tactic:
simp

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

Goal state before:
pp: n : ℕ
x✝¹ : SimplexCategoryᵒᵖ
f : unop x✝¹ ⟶ ⦋n⦌
x✝ : objEquiv.symm f ∈ ⊤.obj x✝¹
⊢ objEquiv.symm f ∈ (Subcomplex.ofSimplex (objEquiv.symm (𝟙 ⦋n⦌))).obj x✝¹

Tactic:
simp only [Subcomplex.mem_ofSimplex_obj_iff, op_unop]

Goal state after:
n : ℕ
x✝¹ : SimplexCategoryᵒᵖ
f : unop x✝¹ ⟶ ⦋n⦌
x✝ : objEquiv.symm f ∈ ⊤.obj x✝¹
⊢ ∃ f_1, (ConcreteCategory.hom (Δ[n].map f_1.op)) (objEquiv.symm (𝟙 ⦋n⦌)) = objEquiv.symm f
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i : ℕ
⊢ (ComplexShape.up ℕ).Rel i 0 → 𝟙 (C.X i) ≫ (truncate.obj (C.augment f w)).d i 0 = C.d i 0 ≫ 𝟙 (C.X 0)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i n✝ : ℕ
⊢ (ComplexShape.up ℕ).Rel i (n✝ + 1) →
    𝟙 (C.X i) ≫ (truncate.obj (C.augment f w)).d i (n✝ + 1) = C.d i (n✝ + 1) ≫ 𝟙 (C.X (n✝ + 1))

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
⊢ ({ f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ }).f 0 =
    (𝟙 (truncate.obj (C.augment f w))).f 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
n✝ : ℕ
⊢ ({ f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ }).f
      (n✝ + 1) =
    (𝟙 (truncate.obj (C.augment f w))).f (n✝ + 1)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
⊢ ({ f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ }).f 0 =
    (𝟙 C).f 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
n✝ : ℕ
⊢ ({ f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ }).f
      (n✝ + 1) =
    (𝟙 C).f (n✝ + 1)

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case zero
Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
φ : (stdSimplex.obj Δ).left _⦋n + 1⦌
⊢ shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down)) (i.succ.succAbove 0) =
    shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down) ∘ ⇑i.succAboveOrderEmb) 0

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case succ
Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
φ : (stdSimplex.obj Δ).left _⦋n + 1⦌
i✝ : Fin (unop (op ⦋n + 1⦌)).len
⊢ shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down)) (i.succ.succAbove i✝.succ) =
    shiftFun (⇑(SimplexCategory.Hom.toOrderHom φ.down) ∘ ⇑i.succAboveOrderEmb) i✝.succ

Tactic:
simp

Goal state after: