mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℕ
hn : Even n
h₀ : n ≠ 0
⊢ ∀ (Z : C) (g : Z ⟶ (HomologicalComplex.sc (alternatingConst.obj X) n).X₂),
    g ≫ (HomologicalComplex.sc (alternatingConst.obj X) n).g = 0 → g = 0

Tactic:
by

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 : ℕ
hn : Odd n
⊢ (HomologicalComplex.sc (alternatingConst.obj X) n).g = 0

Tactic:
by

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 : ℕ
hn : Odd n
⊢ ∀ (Z : C) (g : (HomologicalComplex.sc (alternatingConst.obj X) n).X₂ ⟶ Z),
    (HomologicalComplex.sc (alternatingConst.obj X) n).f ≫ g = 0 → g = 0

Tactic:
by

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 : ℕ
hn : n = 0
⊢ (HomologicalComplex.sc (alternatingConst.obj X) n).f = 0

Tactic:
by

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 : ℕ
hn : n = 0
⊢ (HomologicalComplex.sc (alternatingConst.obj X) n).g = 0

Tactic:
by

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

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 : ℕ
⊢ HomologicalComplex.HasHomology (alternatingConst.obj X) n

Tactic:
by

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 : ℕ
hn : n ≠ 0
⊢ HomologicalComplex.ExactAt (alternatingConst.obj X) n

Tactic:
by

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 : C
⊢ ∀ (i j : ℕ),
    (ComplexShape.down ℕ).Rel i j →
      (Iso.refl (((Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C).obj X).X i)).hom ≫
          (ChainComplex.alternatingConst.obj X).d i j =
        ((Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C).obj X).d i j ≫
          (Iso.refl (((Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C).obj X).X j)).hom

Tactic:
by

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),
    (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C).map f ≫
        (HomologicalComplex.Hom.isoOfComponents
            (fun x ↦ Iso.refl (((Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C).obj Y).X x)) ⋯).hom =
      (HomologicalComplex.Hom.isoOfComponents
            (fun x ↦ Iso.refl (((Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C).obj X).X x)) ⋯).hom ≫
        ChainComplex.alternatingConst.map f

Tactic:
by

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₁
f : X₁ ⟶ X₂
Y₁ Y₂ : GradedObject J C₂
g : Y₁ ⟶ Y₂
inst✝¹ : (((mapBifunctor F I J).obj X₁).obj Y₁).HasMap p
inst✝ : (((mapBifunctor F I J).obj X₂).obj Y₂).HasMap p
i : I
j : J
k : K
h : p (i, j) = k
⊢ ιMapBifunctorMapObj F p X₁ Y₁ i j k h ≫ mapBifunctorMapMap F p f g k =
    (F.map (f i)).app (Y₁ j) ≫ (F.obj (X₂ i)).map (g j) ≫ ιMapBifunctorMapObj F p X₂ Y₂ i j k h

Tactic:
by

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 : GradedObject I C₁
Y : GradedObject J C₂
A : C₃
k : K
inst✝ : (((mapBifunctor F I J).obj X).obj Y).HasMap p
f g : mapBifunctorMapObj F p X Y k ⟶ A
h :
  ∀ (i : I) (j : J) (hij : p (i, j) = k),
    ιMapBifunctorMapObj F p X Y i j k hij ≫ f = ιMapBifunctorMapObj F p X Y i j k hij ≫ g
⊢ f = g

Tactic:
by

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 : GradedObject I C₁
Y : GradedObject J C₂
A : C₃
k : K
inst✝ : (((mapBifunctor F I J).obj X).obj Y).HasMap p
f : (i : I) → (j : J) → p (i, j) = k → ((F.obj (X i)).obj (Y j) ⟶ A)
i : I
j : J
hij : p (i, j) = k
⊢ ιMapBifunctorMapObj F p X Y i j k hij ≫ mapBifunctorMapObjDesc f = f i j hij

Tactic:
by

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₂
⊢ mapBifunctorMapMap F p e.hom e'.hom ≫ mapBifunctorMapMap F p e.inv e'.inv = 𝟙 (mapBifunctorMapObj F p X₁ Y₁)

Tactic:
by

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₂
⊢ mapBifunctorMapMap F p e.inv e'.inv ≫ mapBifunctorMapMap F p e.hom e'.hom = 𝟙 (mapBifunctorMapObj F p X₂ Y₂)

Tactic:
by

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
inst✝ : ∀ (X : GradedObject I C₁) (Y : GradedObject J C₂), (((mapBifunctor F I J).obj X).obj Y).HasMap p
X₁ X₂ : GradedObject I C₁
φ : X₁ ⟶ X₂
Y₁ Y₂ : GradedObject J C₂
ψ : Y₁ ⟶ Y₂
⊢ { obj := fun Y ↦ mapBifunctorMapObj F p X₁ Y, map := fun {X Y} ψ ↦ mapBifunctorMapMap F p (𝟙 X₁) ψ, map_id := ⋯,
            map_comp := ⋯ }.map
        ψ ≫
      mapBifunctorMapMap F p φ (𝟙 Y₂) =
    mapBifunctorMapMap F p φ (𝟙 Y₁) ≫
      { obj := fun Y ↦ mapBifunctorMapObj F p X₂ Y, map := fun {X Y} ψ ↦ mapBifunctorMapMap F p (𝟙 X₂) ψ, map_id := ⋯,
            map_comp := ⋯ }.map
        ψ

Tactic:
by

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
w : ¬(ComplexShape.down ℕ).Rel i j
⊢ ¬(ComplexShape.down ℕ).Rel (i + 1) (j + 1)

Tactic:
by

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

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

Goal state before:
pp: 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 j : ℕ
h : ¬(ComplexShape.down ℕ).Rel (i + 1) (j + 1)
⊢ (match i + 1, j + 1 with
    | 1, 0 => f
    | i.succ, j.succ => C.d i j
    | x, x_1 => 0) =
    0

Tactic:
simp only

Goal state after:
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 j : ℕ
h : ¬(ComplexShape.down ℕ).Rel (i + 1) (j + 1)
⊢ C.d i j = 0
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: 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 j : ℕ
h : ¬(ComplexShape.down ℕ).Rel (i + 1) (j + 1)
⊢ (match i + 1, j + 1 with
    | 1, 0 => f
    | i.succ, j.succ => C.d i j
    | x, x_1 => 0) =
    0

Tactic:
by

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

Goal state before:
pp: 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 j : ℕ
⊢ (C.augment f w).d (i + 1) (j + 1) = C.d i j

Tactic:
by

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

Goal state before:
pp: 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 j : ℕ
⊢ (ComplexShape.down ℕ).Rel i j → 𝟙 (C.X i) ≫ (truncate.obj (C.augment f w)).d i j = C.d i j ≫ 𝟙 (C.X j)

Tactic:
by

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

Goal state before:
pp: 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' := ⋯ } =
    𝟙 (truncate.obj (C.augment f w))

Tactic:
by

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

Goal state before:
pp: 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' := ⋯ } = 𝟙 C

Tactic:
by

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ C.d (i + 2) 0 = 0

Tactic:
by

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ (ComplexShape.down ℕ).Rel i j →
    (match i 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))) ≫
        C.d i j =
      ((truncate.obj C).augment (C.d 1 0) ⋯).d i j ≫
        match j 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))

Tactic:
by

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

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

Goal state before:
pp: n i : ℕ
x✝¹ x✝ : Δ[n] _⦋i⦌
h : (fun x j ↦ (Hom.toOrderHom (objEquiv x)) j) x✝¹ = (fun x j ↦ (Hom.toOrderHom (objEquiv x)) j) x✝
⊢ objEquiv x✝¹ = objEquiv x✝

Tactic:
by

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

Goal state before:
pp: n : ℕ
m : SimplexCategory
f : ⦋n + 1⦌ ⟶ m
i : Fin (n + 2)
⊢ (ConcreteCategory.hom (SimplicialObject.δ (stdSimplex.obj m) i)) (objEquiv.symm f) = objEquiv.symm (δ i ≫ f)

Tactic:
by

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

Goal state before:
pp: n : ℕ
m : SimplexCategory
f : ⦋n⦌ ⟶ m
i : Fin (n + 1)
⊢ (ConcreteCategory.hom (SimplicialObject.σ (stdSimplex.obj m) i)) (objEquiv.symm f) = objEquiv.symm (σ i ≫ f)

Tactic:
by

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

Goal state before:
pp: m₁ m₂ : SimplexCategoryᵒᵖ
f : m₁ ⟶ m₂
n : SimplexCategory
x : (stdSimplex.obj n).obj m₁
⊢ (ConcreteCategory.hom ((stdSimplex.obj n).map f)) x = objEquiv.symm (f.unop ≫ objEquiv x)

Tactic:
by

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

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

Goal state before:
pp: X : SSet
x : X _⦋0⦌
⊢ yonedaEquiv (const x) = x

Tactic:
by

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

Goal state before:
pp: X : SSet
x : X _⦋0⦌
⊢ yonedaEquiv.symm x = const x

Tactic:
by

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

Goal state before:
pp: X : SSet
n : SimplexCategory
x : X.obj (op n)
m : SimplexCategoryᵒᵖ
y : (stdSimplex.obj n).obj m
⊢ (ConcreteCategory.hom (X.map (objEquiv y).op)) x = (ConcreteCategory.hom ((yonedaEquiv.symm x).app m)) y

Tactic:
by

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

Goal state before:
pp: n : ℕ
x : Δ[n] _⦋0⦌
⊢ (fun i ↦ const n i (op ⦋0⦌)) ((fun x ↦ x 0) x) = x

Tactic:
by

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

Goal state before:
pp: ⊢ stdSimplex.δ 1 = SSet.const (obj₀Equiv.symm 0)

Tactic:
by

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

Goal state before:
pp: ⊢ stdSimplex.δ 0 = SSet.const (obj₀Equiv.symm 1)

Tactic:
by

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
hab : a ≤ b
⊢ Δ[n] _⦋1⦌

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
a b c : Fin (n + 1)
hab : a ≤ b
hbc : b ≤ c
⊢ Δ[n] _⦋2⦌

Tactic:
by

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

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 1))
U V : SimplexCategoryᵒᵖ
i : U ⟶ V
⊢ {f | Finset.image ⇑(Hom.toOrderHom (objEquiv f)) ⊤ ⊆ S} ⊆
    ⇑(ConcreteCategory.hom (Δ[n].map i)) ⁻¹' {f | Finset.image ⇑(Hom.toOrderHom (objEquiv f)) ⊤ ⊆ S}

Tactic:
by

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

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

Goal state before:
pp: 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' := ⋯ } =
    𝟙 ((truncate.obj C).augment (C.d 1 0) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : Augmented C
e : X ≅ Y
ed : X.ExtraDegeneracy
⊢ ((point.mapIso e).inv ≫ ed.s' ≫ (drop.mapIso e).hom.app (op ⦋0⦌)) ≫ Y.hom.app (op ⦋0⦌) = 𝟙 Y.right

Tactic:
by

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

Goal state before:
pp: n : ℕ
S₁ S₂ : Finset (Fin (n + 1))
⊢ face S₁ ⊓ face S₂ = face (S₁ ⊓ S₂)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : Augmented C
e : X ≅ Y
ed : X.ExtraDegeneracy
⊢ ((drop.mapIso e).inv.app (op ⦋0⦌) ≫ ed.s 0 ≫ (drop.mapIso e).hom.app (op ⦋0 + 1⦌)) ≫ Y.left.δ 1 =
    Y.hom.app (op ⦋0⦌) ≫ (point.mapIso e).inv ≫ ed.s' ≫ (drop.mapIso e).hom.app (op ⦋0⦌)

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ face ∅ = ⊥

Tactic:
by

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

Goal state before:
pp: 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' := ⋯ } =
    𝟙 C

Tactic:
by

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i j : ℕ
w : ¬(ComplexShape.up ℕ).Rel i j
⊢ C.d (i + 1) (j + 1) = 0

Tactic:
by

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

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

Goal state before:
pp: n : ℕ
⊢ face univ = ⊤

Tactic:
by

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

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : Augmented C
e : X ≅ Y
ed : X.ExtraDegeneracy
n : ℕ
⊢ ((drop.mapIso e).inv.app (op ⦋n⦌) ≫ ed.s n ≫ (drop.mapIso e).hom.app (op ⦋n + 1⦌)) ≫ Y.left.δ 0 = 𝟙 (Y.left _⦋n⦌)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : Augmented C
e : X ≅ Y
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
⊢ ((drop.mapIso e).inv.app (op ⦋n + 1⦌) ≫ ed.s (n + 1) ≫ (drop.mapIso e).hom.app (op ⦋n + 1 + 1⦌)) ≫ Y.left.δ i.succ =
    Y.left.δ i ≫ (drop.mapIso e).inv.app (op ⦋n⦌) ≫ ed.s n ≫ (drop.mapIso e).hom.app (op ⦋n + 1⦌)

Tactic:
by

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

Goal state before:
pp: X : SSet
m n : SimplexCategory
f : m ⟶ n
g : X.obj (op n)
⊢ stdSimplex.map f ≫ yonedaEquiv.symm g = yonedaEquiv.symm ((ConcreteCategory.hom (X.map f.op)) g)

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
n : SimplexCategory
f : stdSimplex.obj n ⟶ A.toSSet
⊢ ↑(yonedaEquiv f) = yonedaEquiv (f ≫ A.ι)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : Augmented C
e : X ≅ Y
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
⊢ ((drop.mapIso e).inv.app (op ⦋n⦌) ≫ ed.s n ≫ (drop.mapIso e).hom.app (op ⦋n + 1⦌)) ≫ Y.left.σ i.succ =
    Y.left.σ i ≫ (drop.mapIso e).inv.app (op ⦋n + 1⦌) ≫ ed.s (n + 1) ≫ (drop.mapIso e).hom.app (op ⦋n + 1 + 1⦌)

Tactic:
by

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

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 1))
i : Fin (n + 1)
h : obj₀Equiv.symm i ∈ (face S).obj (op ⦋0⦌)
⊢ i ∈ S

Tactic:
by

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

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 1))
i : Fin (n + 1)
⊢ i ∈ S → obj₀Equiv.symm i ∈ (face S).obj (op ⦋0⦌)

Tactic:
by

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
⊢ ed.section_.app (op ⦋0⦌) = ed.s'

Tactic:
by

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

Goal state before:
pp: n : ℕ
S₁ S₂ : Finset (Fin (n + 1))
⊢ face S₁ ≤ face S₂ ↔ S₁ ⊆ S₂

Tactic:
by

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 : SimplexCategoryᵒᵖ
⊢ ed.section_.app n ≫ X.hom.app n = 𝟙 X.right

Tactic:
by

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
⊢ ed.section_ ≫ X.hom = 𝟙 ((SimplicialObject.const C).obj X.right)

Tactic:
by

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

Goal state before:
pp: 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 j : ℕ
s : ¬(ComplexShape.up ℕ).Rel i j
⊢ (match i, j with
    | 0, 1 => f
    | i.succ, j.succ => C.d i j
    | x, x_1 => 0) =
    0

Tactic:
by

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 : ℕ
⊢ ed.s' ≫ X.left.σ₀Iter n ⋯ = ed.section_.app (op ⦋n⦌)

Tactic:
by

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)
⊢ ↑i.rev + ↑i = n

Tactic:
by

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)
⊢ ↑i.rev + 1 + ↑i = n + 1

Tactic:
by

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)
j : ℕ
hj : autoParam (j = ↑i.rev) h_eq._auto_1
⊢ j + ↑i = n

Tactic:
by

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)
j : ℕ
hj : autoParam (j = ↑i.rev) h_eq._auto_1
⊢ j + 1 + ↑i = n + 1

Tactic:
by

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)
j : ℕ
hj : j = ↑i.rev
⊢ h ed i = X.left.δ₀Iter ↑i ⋯ ≫ ed.s j ≫ X.left.σ₀Iter ↑i ⋯

Tactic:
by

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

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 : ℕ
⊢ h ed 0 ≫ X.left.δ 0 = (𝟙 X.left).app (op ⦋n⦌)

Tactic:
by

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
⊢ face S = Subcomplex.ofSimplex (objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom))

Tactic:
by

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

Goal state before:
pp: 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 j k✝ : ℕ
hij : (ComplexShape.up ℕ).Rel i j
hjk : (ComplexShape.up ℕ).Rel j k✝
k : ℕ
⊢ f ≫ C.d 0 (k + 1) = 0

Tactic:
by

Goal state after: