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

Goal state before:
pp: case succ
j : ℕ
hj :
  ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : n + j = m),
    ↑i' = ↑i + j → δ₀Iter j h ≫ δ i' = δ i ≫ δ₀Iter j ⋯
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : n + (j + 1) = m
hi'' : ↑i' = ↑i + (j + 1)
⊢ δ₀Iter (j + 1) h ≫ δ i' = δ i ≫ δ₀Iter (j + 1) ⋯

Tactic:
rw [δ₀Iter_succ'_assoc .., δ₀Iter_succ' ..,
      ← reassoc_of% dsimp% δ_comp_δ (i := 0) (j := i) (by simp),
      ← hj _ i' _ (by grind)]

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
⊢ equivalenceRightToLeft X F (equivalenceLeftToRight X F A) = A

Tactic:
by ext <;> simp

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

Goal state before:
pp: X : SSet
s t : X.S
⊢ s ≤ t ↔ ∃ f, (ConcreteCategory.hom (X.map f.op)) t.simplex = s.simplex

Tactic:
le_def,

Goal state after:
X : SSet
s t : X.S
⊢ s.subcomplex ≤ t.subcomplex ↔ ∃ f, (ConcreteCategory.hom (X.map f.op)) t.simplex = s.simplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: case mpr
X : SSet
n : ℕ
x : X _⦋n + 1⦌
⊢ x ∈ ⋃ i, Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ X i)) → x ∈ X.degenerate (n + 1)

Tactic:
· intro hx
    simp only [Set.mem_iUnion, Set.mem_range] at hx
    obtain ⟨i, y, rfl⟩ := hx
    apply σ_mem_degenerate

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

Goal state before:
pp: X Y : SSet
⊢ ∀ (a : ⊥.toSSet ⟶ Y),
    a =
      {
        app := fun x ↦
          ↾fun x_1 ↦
            match x_1 with
            | ⟨val, h⟩ => ⋯.elim,
        naturality := ⋯ }

Tactic:
subsingleton

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ ⊤ ≤ (range f).preimage f

Tactic:
← image_le_iff,

Goal state after:
X Y : SSet
f : X ⟶ Y
⊢ ⊤.image f ≤ range f
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: case term
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
j✝ : ι
⊢ terminal.from (∏ᶜ fun x ↦ X) =
    limit.π (Discrete.functor fun x ↦ X) { as := j✝ } ≫ (wideCospan ι X).map (WidePullbackShape.Hom.term j✝)

Tactic:
subsingleton

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
s : Cone (wideCospan ι X)
j : WidePullbackShape ι
⊢ (Pi.lift fun j ↦ s.π.app (some j)) ≫
      { pt := ∏ᶜ fun x ↦ X,
              π :=
                {
                  app := fun X_1 ↦
                    Option.casesOn X_1
                      (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none)) fun i ↦
                      limit.π (Discrete.functor fun x ↦ X) { as := i },
                  naturality := ⋯ } }.π.app
        none =
    s.π.app none

Tactic:
subsingleton

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

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
inst✝ : IsIso f
x✝ : SimplexCategoryᵒᵖ
x : Y.obj x✝
hx : (ConcreteCategory.hom (inv (f.app x✝))) x ∈ A.obj x✝
⊢ (ConcreteCategory.hom ((inv f).app x✝)) x ∈ A.obj x✝ ∧
    (ConcreteCategory.hom (f.app x✝)) ((ConcreteCategory.hom ((inv f).app x✝)) x) = x

Tactic:
by simpa

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

Goal state before:
pp: X : SSet
A B : X.Subcomplex
h : ∀ (s : X.N), s.subcomplex ≤ A → s.subcomplex ≤ B
n : ℕ
x : ↑(X.nonDegenerate n)
hx : ↑x ∈ A.obj (Opposite.op ⦋n⦌)
⊢ (mk ↑x ⋯).subcomplex ≤ A

Tactic:
by simpa

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

Goal state before:
pp: X Y : Truncated 2
inst✝ : Subsingleton (X.obj (Opposite.op { obj := ⦋1⦌, property := _proof_2 }))
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := _proof_1 })
f g : Edge x y
⊢ f.edge = g.edge

Tactic:
subsingleton

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Quiver.IsThin C
n : SimplexCategoryᵒᵖ
x y : (nerve C).obj n
h : x.obj = y.obj
⊢ ∀ (i : ℕ) (hi : i < (unop n).len),
    ComposableArrows.map' x i (i + 1) ⋯ hi = eqToHom ⋯ ≫ ComposableArrows.map' y i (i + 1) ⋯ hi ≫ eqToHom ⋯

Tactic:
subsingleton

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
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
⊢ ((if hij : c.Rel i j then if hi : Even i then φ else ψ else 0) ≫
      if hij : c.Rel j k then if hi : Even j then φ else ψ else 0) =
    0

Tactic:
by
    have := hc i j hij
    split_ifs with hi hj hj
    · exact False.elim <| Nat.not_odd_iff_even.2 hi <| by simp_all [Nat.odd_add]
    · assumption
    · assumption
    · exact False.elim <| hj <| by simp_all [Nat.odd_add]

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:
simp [ιMapBifunctorMapObj, mapBifunctorMapMap]

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 simpa

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 : ℕ
⊢ (ComplexShape.down ℕ).Rel 0 0 →
    (match 0 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 0 0 =
      ((truncate.obj C).augment (C.d 1 0) ⋯).d 0 0 ≫
        match 0 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:
dsimp [augment, truncate]

Goal state after:
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)
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 : ℕ
⊢ (ComplexShape.down ℕ).Rel 0 (j + 1) →
    (match 0 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 0 (j + 1) =
      ((truncate.obj C).augment (C.d 1 0) ⋯).d 0 (j + 1) ≫
        match j + 1 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:
dsimp [augment, truncate]

Goal state after:
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))
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 : ℕ
⊢ (ComplexShape.down ℕ).Rel 1 0 →
    (match 1 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 1 0 =
      ((truncate.obj C).augment (C.d 1 0) ⋯).d 1 0 ≫
        match 0 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:
dsimp [augment, truncate]

Goal state after:
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)
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 : ℕ
⊢ (ComplexShape.down ℕ).Rel 1 (j + 1) →
    (match 1 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 1 (j + 1) =
      ((truncate.obj C).augment (C.d 1 0) ⋯).d 1 (j + 1) ≫
        match j + 1 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:
dsimp [augment, truncate]

Goal state after:
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))
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 : ℕ
⊢ (ComplexShape.down ℕ).Rel (n + 2) 0 →
    (match n + 2 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 (n + 2) 0 =
      ((truncate.obj C).augment (C.d 1 0) ⋯).d (n + 2) 0 ≫
        match 0 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:
dsimp [augment, truncate]

Goal state after:
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)
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 : ℕ
⊢ (ComplexShape.down ℕ).Rel (n + 2) (j + 1) →
    (match n + 2 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 (n + 2) (j + 1) =
      ((truncate.obj C).augment (C.d 1 0) ⋯).d (n + 2) (j + 1) ≫
        match j + 1 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:
dsimp [augment, truncate]

Goal state after:
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))
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 : ℕ
⊢ (ComplexShape.down ℕ).Rel 0 0 →
    (match 0 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))) ≫
        ((truncate.obj C).augment (C.d 1 0) ⋯).d 0 0 =
      C.d 0 0 ≫
        match 0 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))

Tactic:
dsimp [augment, truncate]

Goal state after:
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)
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 : ℕ
⊢ (ComplexShape.down ℕ).Rel 0 (j + 1) →
    (match 0 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))) ≫
        ((truncate.obj C).augment (C.d 1 0) ⋯).d 0 (j + 1) =
      C.d 0 (j + 1) ≫
        match j + 1 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))

Tactic:
dsimp [augment, truncate]

Goal state after:
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))
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 : ℕ
⊢ (ComplexShape.down ℕ).Rel 1 0 →
    (match 1 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))) ≫
        ((truncate.obj C).augment (C.d 1 0) ⋯).d 1 0 =
      C.d 1 0 ≫
        match 0 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))

Tactic:
dsimp [augment, truncate]

Goal state after:
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)
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 : ℕ
⊢ (ComplexShape.down ℕ).Rel 1 (j + 1) →
    (match 1 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))) ≫
        ((truncate.obj C).augment (C.d 1 0) ⋯).d 1 (j + 1) =
      C.d 1 (j + 1) ≫
        match j + 1 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))

Tactic:
dsimp [augment, truncate]

Goal state after:
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))
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 : ℕ
⊢ (ComplexShape.down ℕ).Rel (n + 2) 0 →
    (match n + 2 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))) ≫
        ((truncate.obj C).augment (C.d 1 0) ⋯).d (n + 2) 0 =
      C.d (n + 2) 0 ≫
        match 0 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))

Tactic:
dsimp [augment, truncate]

Goal state after:
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)
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 : ℕ
⊢ (ComplexShape.down ℕ).Rel (n + 2) (j + 1) →
    (match n + 2 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))) ≫
        ((truncate.obj C).augment (C.d 1 0) ⋯).d (n + 2) (j + 1) =
      C.d (n + 2) (j + 1) ≫
        match j + 1 with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))

Tactic:
dsimp [augment, truncate]

Goal state after:
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))
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:
match i with
          | 0 | 1 | n + 2 =>
          rcases j with - | j <;> dsimp [augment, truncate] <;> simp

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case e_a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
⊢ SimplexCategory.σ₀Iter n ⋯ = SimplexCategory.isTerminalZero.from ⦋n⦌

Tactic:
subsingleton

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

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 1))
d : ℕ
hd : #S ≤ d
m : ℕ
hm : #S = m + 1
⊢ Fintype.card ↥S = m + 1

Tactic:
by simpa

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: Δ : SimplexCategory
⊢ (↾fun x ↦ objMk ((OrderHom.const (Fin 1)) 0)) ≫ Limits.terminal.from (SSet.stdSimplex.obj Δ _⦋0⦌) = 𝟙 (⊤_ Type ?u.22)

Tactic:
subsingleton

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
⊢ range (yonedaEquiv.symm x) ≤ ofSimplex x

Tactic:
by simp [range_eq_ofSimplex]

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: Δ : SimplexCategory
n : ℕ
i : Fin (n + 1)
⊢ (↾fun f ↦ objEquiv.symm (shift (objEquiv f))) ≫ (stdSimplex.obj Δ).left.σ i.succ =
    (stdSimplex.obj Δ).left.σ i ≫ ↾fun f ↦ objEquiv.symm (shift (objEquiv f))

Tactic:
ext φ
    apply objEquiv.injective
    apply SimplexCategory.Hom.ext
    ext j : 2
    dsimp [SimplicialObject.σ, SimplexCategory.σ, SSet.stdSimplex, objEquiv, Equiv.ulift,
      uliftFunctor, Function.comp_def]
    cases j using Fin.cases <;> simp

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁹ : Category.{v_1, u_1} C₁
inst✝⁸ : Category.{v_2, u_2} C₂
inst✝⁷ : Category.{v_3, u_3} D
inst✝⁶ : Preadditive C₁
inst✝⁵ : HasZeroMorphisms C₂
inst✝⁴ : Preadditive D
K₁ L₁ : CochainComplex C₁ ℤ
f₁ : K₁ ⟶ L₁
K₂ : CochainComplex C₂ ℤ
F : C₁ ⥤ C₂ ⥤ D
inst✝³ : F.Additive
inst✝² : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
x : ℤ
inst✝¹ : K₁.HasMapBifunctor K₂ F
inst✝ : L₁.HasMapBifunctor K₂ F
⊢ mapBifunctorMap ((CategoryTheory.shiftFunctor (HomologicalComplex C₁ (ComplexShape.up ℤ)) x).map f₁) (𝟙 K₂) F
        (ComplexShape.up ℤ) ≫
      (L₁.mapBifunctorShift₁Iso K₂ F x).hom =
    (K₁.mapBifunctorShift₁Iso K₂ F x).hom ≫
      (CategoryTheory.shiftFunctor (CochainComplex D ℤ) x).map (mapBifunctorMap f₁ (𝟙 K₂) F (ComplexShape.up ℤ))

Tactic:
by
  ext n p q h
  simp [ι_mapBifunctorShift₁Iso_hom_f _ _ _ _ _ _ _ _ (p + x) (n + x) rfl rfl,
    ι_mapBifunctorShift₁Iso_hom_f_assoc _ _ _ _ _ _ _ _ (p + x) (n + x) rfl rfl]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
n p q p' q' : ℤ
hp : p = p'
hq : q = q'
⊢ ComplexShape.embeddingUpIntDownInt.f q = ComplexShape.embeddingUpIntDownInt.f q'

Tactic:
by simpa

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : HasZeroMorphisms C₁
inst✝⁴ : Preadditive C₂
inst✝³ : Preadditive D
K₁ : CochainComplex C₁ ℤ
K₂ : CochainComplex C₂ ℤ
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
y : ℤ
inst✝ : K₁.HasMapBifunctor K₂ F
n₁ n₂ n : ℤ
h : n₁ + n₂ = n
m₂ m : ℤ
hm₂ : m₂ = n₂ + y
hm : m = n + y
⊢ ((K₁.mapBifunctorHomologicalComplexShift₂Iso K₂ F y).hom.f n₁).f n₂ ≫
      ((n₁ * y).negOnePow •
        ((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂).shiftFunctor₂XXIso
              n₁ n₂ y m₂ hm₂).hom ≫
          (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂).ιTotal
              (ComplexShape.up ℤ) n₁ m₂ m ⋯ ≫
            (shiftFunctorObjXIso
                ((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂).total
                  (ComplexShape.up ℤ))
                y n m hm).inv) =
    (n₁ * y).negOnePow •
      (F.obj (K₁.X n₁)).map (XIsoOfEq K₂ ⋯).hom ≫
        K₁.ιMapBifunctor K₂ F n₁ m₂ m ⋯ ≫ (XIsoOfEq (K₁.mapBifunctor K₂ F) ⋯).inv

Tactic:
simp [HomologicalComplex₂.ιTotal, HomologicalComplex₂.shiftFunctor₂XXIso,
    HomologicalComplex.XIsoOfEq, eqToHom_map]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
j' : ι'
i : ι
hij' : ¬c'.Rel j' (e.f i)
⊢ extend.hom e h.hom (e.f i) j' = 0

Tactic:
by_cases hj' : ∃ j, e.f j = j'

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
j' : ι'
i : ι
hij' : ¬c'.Rel j' (e.f i)
hj' : ∃ j, e.f j = j'
⊢ extend.hom e h.hom (e.f i) j' = 0

case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
j' : ι'
i : ι
hij' : ¬c'.Rel j' (e.f i)
hj' : ¬∃ j, e.f j = j'
⊢ extend.hom e h.hom (e.f i) j' = 0
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
h : Homotopy (extendMap f e) (extendMap g e)
j' : ι'
i : ι
⊢ (h.ofExtend.extend e).hom (e.f i) j' = h.hom (e.f i) j'

Tactic:
by_cases hj' : ∃ j, e.f j = j'

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
h : Homotopy (extendMap f e) (extendMap g e)
j' : ι'
i : ι
hj' : ∃ j, e.f j = j'
⊢ (h.ofExtend.extend e).hom (e.f i) j' = h.hom (e.f i) j'

case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
h : Homotopy (extendMap f e) (extendMap g e)
j' : ι'
i : ι
hj' : ¬∃ j, e.f j = j'
⊢ (h.ofExtend.extend e).hom (e.f i) j' = h.hom (e.f i) j'