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

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

Tactic:
zsmul_comp

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

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

Tactic:
dsimp [δ]
  simp only [← X.map_comp, SimplexCategory.δ_comp_δ'' H]

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : CosimplicialObject C
n : ℕ
⊢ objD X n = (AlternatingFaceMapComplex.objD ((cosimplicialSimplicialEquiv C).functor.obj (op X)) n).unop

Tactic:
simp only [objD, AlternatingFaceMapComplex.objD, unop_sum, unop_zsmul]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : CosimplicialObject C
n : ℕ
⊢ ∑ i, (-1) ^ ↑i • X.δ i = ∑ i, (-1) ^ ↑i • (((cosimplicialSimplicialEquiv C).functor.obj (op X)).δ i).unop
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

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

Tactic:
zsmul_comp

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j m : ℕ
i' : Fin (m + 2)
h : n + j = m
hi'' : ↑i' = ↑i + j
⊢ δ₀Iter j h ≫ δ i' = δ i ≫ δ₀Iter j ⋯

Tactic:
induction j generalizing n m with

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j m : ℕ
i' : Fin (m + 2)
h : m + j = n
hi' : j < ↑i
hi'' : ↑i = ↑i' + j
⊢ δ i ≫ σ₀Iter j ⋯ = σ₀Iter j ⋯ ≫ δ i'

Tactic:
induction j generalizing n m with

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

Goal state before:
pp: X : SSet
x₂ : X.N
n₁ : ℕ
x₁ : X _⦋n₁⦌
hx₁ : x₁ ∈ X.nonDegenerate n₁
h : mk ↑⟨x₁, hx₁⟩ ⋯ ≤ x₂
h' : x₂ ≤ mk ↑⟨x₁, hx₁⟩ ⋯
⊢ mk ↑⟨x₁, hx₁⟩ ⋯ = x₂

Tactic:
obtain ⟨n₂, ⟨x₂, hx₂⟩, rfl⟩ := x₂.mk_surjective

Goal state after:
X : SSet
n₁ : ℕ
x₁ : X _⦋n₁⦌
hx₁ : x₁ ∈ X.nonDegenerate n₁
n₂ : ℕ
x₂ : X _⦋n₂⦌
hx₂ : x₂ ∈ X.nonDegenerate n₂
h : mk ↑⟨x₁, hx₁⟩ ⋯ ≤ mk ↑⟨x₂, hx₂⟩ ⋯
h' : mk ↑⟨x₂, hx₂⟩ ⋯ ≤ mk ↑⟨x₁, hx₁⟩ ⋯
⊢ mk ↑⟨x₁, hx₁⟩ ⋯ = mk ↑⟨x₂, hx₂⟩ ⋯
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
d : ℕ
s : X _⦋d⦌
hs : s ∈ X.nonDegenerate d
⊢ Subcomplex.ofSimplex ↑⟨d, ⟨s, hs⟩⟩.snd ≤ ⨆ s, s.subcomplex

Tactic:
exact le_trans (by rfl) (le_iSup _ (N.mk _ hs))

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

Goal state before:
pp: X Y : SSet
e : X ≅ Y
x y : X.N
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
⊢ (ConcreteCategory.hom (Y.map f.op)) ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋y.dim⦌))) y.simplex) =
      (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) x.simplex ↔
    (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex

Tactic:
← NatTrans.naturality_apply e.hom f.op

Goal state after:
X Y : SSet
e : X ≅ Y
x y : X.N
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
⊢ (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) ((ConcreteCategory.hom (X.map f.op)) y.simplex) =
      (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) x.simplex ↔
    (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate

Goal state before:
pp: case succ
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
⊢ (∃ i, s.obj i.castSucc = s.obj i.succ) ↔ ∃ x, ¬s.obj x.castSucc < s.obj x.succ

Tactic:
apply exists_congr

Goal state after:
case succ
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
⊢ ∀ (a : Fin (n + 1)), s.obj a.castSucc = s.obj a.succ ↔ ¬s.obj a.castSucc < s.obj a.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve

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

Tactic:
dsimp [homEquiv]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
x : C
⊢ 𝟙 (nerveEquiv (nerveEquiv.symm x)) ≫
      ComposableArrows.hom ((ConcreteCategory.hom (SimplicialObject.σ (nerve C) 0)) (nerveEquiv.symm x)) ≫
        𝟙 (ComposableArrows.right ((ConcreteCategory.hom (SimplicialObject.σ (nerve C) 0)) (nerveEquiv.symm x))) =
    𝟙 (nerveEquiv (nerveEquiv.symm x))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h' : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂)) :=
  Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂) ⋯ ⋯ ⋯
⊢ Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)) ↔ f₀₁ ≫ f₁₂ = f₀₂

Tactic:
refine ⟨fun ⟨h⟩ ↦ ?_, fun h ↦ ⟨by rwa [← h]⟩⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h' : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂)) :=
  Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂) ⋯ ⋯ ⋯
x✝ : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
⊢ f₀₁ ≫ f₁₂ = f₀₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

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

Tactic:
by
  refine ⟨fun h i hi ↦ ?_, fun h d a ha ↦ ha.trans h⟩
  simp only [← obj₀Equiv_symm_mem_face_iff.{u}] at hi ⊢
  exact h _ hi

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

Goal state before:
pp: n d : ℕ
s : Fin (d + 1) ↪o Fin (n + 1)
⊢ objEquiv.symm (Hom.mk s.toOrderHom) ∈ Δ[n].nonDegenerate d

Tactic:
simpa [mem_nonDegenerate_iff_strictMono] using! s.strictMono

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

Goal state before:
pp: n : ℕ
x : Δ[n] _⦋n⦌
⊢ x ∈ Δ[n].nonDegenerate n ↔ x ∈ {objEquiv.symm (𝟙 (unop (op ⦋n⦌)))}

Tactic:
simp only [Set.mem_singleton_iff]

Goal state after:
n : ℕ
x : Δ[n] _⦋n⦌
⊢ x ∈ Δ[n].nonDegenerate n ↔ x = objEquiv.symm (𝟙 ⦋n⦌)
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₁ : c₁.Rel i₁ (c₁.next i₁)
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂' = 0

Tactic:
K.d₁_eq_zero' c₁₂ h₁ i₂ i₁₂'

Goal state after:
case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₁ : c₁.Rel i₁ (c₁.next i₁)
⊢ 0 = 0

case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₁ : c₁.Rel i₁ (c₁.next i₁)
⊢ c₁.π c₂ c₁₂ (c₁.next i₁, i₂) ≠ i₁₂'
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
⊢ K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = 0

Tactic:
by_cases h₂ : c₁₂.Rel i₁₂' i₁₂''
    · ext ⟨i₁, i₂⟩ h
      simp only [totalAux.ιMapObj_D₁_assoc, comp_zero]
      by_cases h₃ : c₁.Rel i₁ (c₁.next i₁)
      · rw [totalAux.d₁_eq K c₁₂ h₃ i₂ i₁₂']; swap
        · rw [← ComplexShape.next_π₁ c₂ c₁₂ h₃ i₂, ← c₁₂.next_eq' h₁, h]
        simp only [Linear.units_smul_comp, assoc, totalAux.ιMapObj_D₁]
        by_cases h₄ : c₁.Rel (c₁.next i₁) (c₁.next (c₁.next i₁))
        · rw [totalAux.d₁_eq K c₁₂ h₄ i₂ i₁₂'', Linear.comp_units_smul,
            d_f_comp_d_f_assoc, zero_comp, smul_zero, smul_zero]
          rw [← ComplexShape.next_π₁ c₂ c₁₂ h₄, ← ComplexShape.next_π₁ c₂ c₁₂ h₃,
            h, c₁₂.next_eq' h₁, c₁₂.next_eq' h₂]
        · rw [K.d₁_eq_zero _ _ _ _ h₄, comp_zero, smul_zero]
      · rw [K.d₁_eq_zero c₁₂ _ _ _ h₃, zero_comp]
    · rw [K.D₁_shape c₁₂ _ _ h₂, comp_zero]

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

Goal state before:
pp: case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
⊢ K.D₂ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'' = 0

pp: case neg
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : ¬c₁₂.Rel i₁₂ i₁₂'
⊢ K.D₂ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'' = 0

Tactic:
· by_cases h₂ : c₁₂.Rel i₁₂' i₁₂''
    · ext ⟨i₁, i₂⟩ h
      simp only [totalAux.ιMapObj_D₂_assoc, comp_zero]
      by_cases h₃ : c₂.Rel i₂ (c₂.next i₂)
      · rw [totalAux.d₂_eq K c₁₂ i₁ h₃ i₁₂']; swap
        · rw [← ComplexShape.next_π₂ c₁ c₁₂ i₁ h₃, ← c₁₂.next_eq' h₁, h]
        simp only [Linear.units_smul_comp, assoc, totalAux.ιMapObj_D₂]
        by_cases h₄ : c₂.Rel (c₂.next i₂) (c₂.next (c₂.next i₂))
        · rw [totalAux.d₂_eq K c₁₂ i₁ h₄ i₁₂'', Linear.comp_units_smul,
            HomologicalComplex.d_comp_d_assoc, zero_comp, smul_zero, smul_zero]
          rw [← ComplexShape.next_π₂ c₁ c₁₂ i₁ h₄, ← ComplexShape.next_π₂ c₁ c₁₂ i₁ h₃,
            h, c₁₂.next_eq' h₁, c₁₂.next_eq' h₂]
        · rw [K.d₂_eq_zero c₁₂ _ _ _ h₄, comp_zero, smul_zero]
      · rw [K.d₂_eq_zero c₁₂ _ _ _ h₃, zero_comp]
    · rw [K.D₂_shape c₁₂ _ _ h₂, comp_zero]

Goal state after:
case neg
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : ¬c₁₂.Rel i₁₂ i₁₂'
⊢ K.D₂ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'' = 0
Module: Mathlib.Algebra.Homology.BifunctorHomotopy

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
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✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
i₁' : I₁
i₂ : I₂
j j' : J
h : c₁.π c₂ c (i₁', i₂) = j
⊢ K₁.ιMapBifunctor K₂ F c i₁' i₂ j h ≫ hom₁ h₁ f₂ F c j j' =
    c₁.ε₁ c₂ c (c₁.prev i₁', i₂) •
      (F.map (h₁.hom i₁' (c₁.prev i₁'))).app (K₂.X i₂) ≫
        (F.obj (L₁.X (c₁.prev i₁'))).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁') i₂ j'

Tactic:
simp [hom₁]

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Twist

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
a b c : A
X : t.Category
⊢ ((shiftFunctorAdd C (a + b) c).app X).hom ≫
      (↑(t.z (a + b) c)).app ((shiftFunctor C c).obj ((shiftFunctor C (a + b)).obj X)) ≫
        (shiftFunctor C c).map ((shiftFunctorAdd C a b).app X).hom ≫
          (shiftFunctor C c).map ((↑(t.z a b)).app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X))) =
    eqToHom ⋯ ≫
      ((shiftFunctorAdd C a (b + c)).app X).hom ≫
        (↑(t.z a (b + c))).app ((shiftFunctor C (b + c)).obj ((shiftFunctor C a).obj X)) ≫
          (↑(t.z b c)).app ((shiftFunctor C (b + c)).obj ((shiftFunctor C a).obj X)) ≫
            ((shiftFunctorAdd C b c).app ((shiftFunctor C a).obj X)).hom

Tactic:
CatCenter.naturality_assoc,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
a b c : A
X : t.Category
⊢ (↑(t.z (a + b) c)).app ((shiftFunctor C (a + b + c)).obj X) ≫
      ((shiftFunctorAdd C (a + b) c).app X).hom ≫
        (shiftFunctor C c).map ((shiftFunctorAdd C a b).app X).hom ≫
          (shiftFunctor C c).map ((↑(t.z a b)).app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X))) =
    eqToHom ⋯ ≫
      ((shiftFunctorAdd C a (b + c)).app X).hom ≫
        (↑(t.z a (b + c))).app ((shiftFunctor C (b + c)).obj ((shiftFunctor C a).obj X)) ≫
          (↑(t.z b c)).app ((shiftFunctor C (b + c)).obj ((shiftFunctor C a).obj X)) ≫
            ((shiftFunctorAdd C b c).app ((shiftFunctor C a).obj X)).hom
Module: Mathlib.CategoryTheory.Shift.Twist

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
a b c : A
X : t.Category
⊢ (↑(t.z (a + b) c)).app ((shiftFunctor C (a + b + c)).obj X) ≫
      ((shiftFunctorAdd C (a + b) c).app X).hom ≫
        (shiftFunctor C c).map ((shiftFunctorAdd C a b).app X).hom ≫
          (shiftFunctor C c).map ((↑(t.z a b)).app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X))) =
    eqToHom ⋯ ≫
      ((shiftFunctorAdd C a (b + c)).app X).hom ≫
        (↑(t.z a (b + c))).app ((shiftFunctor C (b + c)).obj ((shiftFunctor C a).obj X)) ≫
          (↑(t.z b c)).app ((shiftFunctor C (b + c)).obj ((shiftFunctor C a).obj X)) ≫
            ((shiftFunctorAdd C b c).app ((shiftFunctor C a).obj X)).hom

Tactic:
CatCenter.naturality_assoc,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
a b c : A
X : t.Category
⊢ (↑(t.z (a + b) c)).app ((shiftFunctor C (a + b + c)).obj X) ≫
      ((shiftFunctorAdd C (a + b) c).app X).hom ≫
        (shiftFunctor C c).map ((shiftFunctorAdd C a b).app X).hom ≫
          (shiftFunctor C c).map ((↑(t.z a b)).app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X))) =
    eqToHom ⋯ ≫
      (↑(t.z a (b + c))).app ((shiftFunctor C (a + (b + c))).obj X) ≫
        ((shiftFunctorAdd C a (b + c)).app X).hom ≫
          (↑(t.z b c)).app ((shiftFunctor C (b + c)).obj ((shiftFunctor C a).obj X)) ≫
            ((shiftFunctorAdd C b c).app ((shiftFunctor C a).obj X)).hom
Module: Mathlib.CategoryTheory.Shift.Twist

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
a b c : A
X : t.Category
⊢ (↑(t.z (a + b) c)).app ((shiftFunctor C (a + b + c)).obj X) ≫
      ((shiftFunctorAdd C (a + b) c).app X).hom ≫
        (shiftFunctor C c).map ((shiftFunctorAdd C a b).app X).hom ≫
          (shiftFunctor C c).map ((↑(t.z a b)).app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X))) =
    eqToHom ⋯ ≫
      (↑(t.z a (b + c))).app ((shiftFunctor C (a + (b + c))).obj X) ≫
        ((shiftFunctorAdd C a (b + c)).app X).hom ≫
          (↑(t.z b c)).app ((shiftFunctor C (b + c)).obj ((shiftFunctor C a).obj X)) ≫
            ((shiftFunctorAdd C b c).app ((shiftFunctor C a).obj X)).hom

Tactic:
CatCenter.naturality_assoc,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
a b c : A
X : t.Category
⊢ (↑(t.z (a + b) c)).app ((shiftFunctor C (a + b + c)).obj X) ≫
      ((shiftFunctorAdd C (a + b) c).app X).hom ≫
        (shiftFunctor C c).map ((shiftFunctorAdd C a b).app X).hom ≫
          (shiftFunctor C c).map ((↑(t.z a b)).app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X))) =
    (↑(t.z a (b + c))).app ((shiftFunctor C (a + b + c)).obj X) ≫
      eqToHom ⋯ ≫
        ((shiftFunctorAdd C a (b + c)).app X).hom ≫
          (↑(t.z b c)).app ((shiftFunctor C (b + c)).obj ((shiftFunctor C a).obj X)) ≫
            ((shiftFunctorAdd C b c).app ((shiftFunctor C a).obj X)).hom
Module: Mathlib.CategoryTheory.Shift.Twist

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
a b c : A
X : t.Category
⊢ (↑(t.z (a + b) c)).app ((shiftFunctor C (a + b + c)).obj X) ≫
      ((shiftFunctorAdd C (a + b) c).app X).hom ≫
        (shiftFunctor C c).map ((shiftFunctorAdd C a b).app X).hom ≫
          (shiftFunctor C c).map ((↑(t.z a b)).app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X))) =
    (↑(t.z a (b + c))).app ((shiftFunctor C (a + b + c)).obj X) ≫
      eqToHom ⋯ ≫
        ((shiftFunctorAdd C a (b + c)).app X).hom ≫
          (↑(t.z b c)).app ((shiftFunctor C (b + c)).obj ((shiftFunctor C a).obj X)) ≫
            ((shiftFunctorAdd C b c).app ((shiftFunctor C a).obj X)).hom

Tactic:
CatCenter.naturality_assoc,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
a b c : A
X : t.Category
⊢ (↑(t.z (a + b) c)).app ((shiftFunctor C (a + b + c)).obj X) ≫
      ((shiftFunctorAdd C (a + b) c).app X).hom ≫
        (shiftFunctor C c).map ((shiftFunctorAdd C a b).app X).hom ≫
          (shiftFunctor C c).map ((↑(t.z a b)).app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X))) =
    (↑(t.z a (b + c))).app ((shiftFunctor C (a + b + c)).obj X) ≫
      eqToHom ⋯ ≫
        (↑(t.z b c)).app ((shiftFunctor C (a + (b + c))).obj X) ≫
          ((shiftFunctorAdd C a (b + c)).app X).hom ≫ ((shiftFunctorAdd C b c).app ((shiftFunctor C a).obj X)).hom
Module: Mathlib.CategoryTheory.Shift.Twist

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
a b c : A
X : t.Category
⊢ (↑(t.z (a + b) c)).app ((shiftFunctor C (a + b + c)).obj X) ≫
      ((shiftFunctorAdd C (a + b) c).app X).hom ≫
        (shiftFunctor C c).map ((shiftFunctorAdd C a b).app X).hom ≫
          (shiftFunctor C c).map ((↑(t.z a b)).app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X))) =
    (↑(t.z a (b + c))).app ((shiftFunctor C (a + b + c)).obj X) ≫
      eqToHom ⋯ ≫
        (↑(t.z b c)).app ((shiftFunctor C (a + (b + c))).obj X) ≫
          ((shiftFunctorAdd C a (b + c)).app X).hom ≫ ((shiftFunctorAdd C b c).app ((shiftFunctor C a).obj X)).hom

Tactic:
CatCenter.naturality_assoc,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
a b c : A
X : t.Category
⊢ (↑(t.z (a + b) c)).app ((shiftFunctor C (a + b + c)).obj X) ≫
      ((shiftFunctorAdd C (a + b) c).app X).hom ≫
        (shiftFunctor C c).map ((shiftFunctorAdd C a b).app X).hom ≫
          (shiftFunctor C c).map ((↑(t.z a b)).app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X))) =
    (↑(t.z a (b + c))).app ((shiftFunctor C (a + b + c)).obj X) ≫
      (↑(t.z b c)).app ((shiftFunctor C (a + b + c)).obj X) ≫
        eqToHom ⋯ ≫
          ((shiftFunctorAdd C a (b + c)).app X).hom ≫ ((shiftFunctorAdd C b c).app ((shiftFunctor C a).obj X)).hom
Module: Mathlib.CategoryTheory.Shift.Twist

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
a b c : A
X : t.Category
⊢ (↑(t.z (a + b) c)).app ((shiftFunctor C (a + b + c)).obj X) ≫
      ((shiftFunctorAdd C (a + b) c).app X).hom ≫
        (↑(t.z a b)).app ((shiftFunctor C c).obj ((shiftFunctor C (a + b)).obj X)) ≫
          (shiftFunctor C c).map ((shiftFunctorAdd C a b).app X).hom =
    (↑(t.z a (b + c))).app ((shiftFunctor C (a + b + c)).obj X) ≫
      (↑(t.z b c)).app ((shiftFunctor C (a + b + c)).obj X) ≫
        eqToHom ⋯ ≫
          ((shiftFunctorAdd C a (b + c)).app X).hom ≫ ((shiftFunctorAdd C b c).app ((shiftFunctor C a).obj X)).hom

Tactic:
CatCenter.naturality_assoc,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
a b c : A
X : t.Category
⊢ (↑(t.z (a + b) c)).app ((shiftFunctor C (a + b + c)).obj X) ≫
      (↑(t.z a b)).app ((shiftFunctor C (a + b + c)).obj X) ≫
        ((shiftFunctorAdd C (a + b) c).app X).hom ≫ (shiftFunctor C c).map ((shiftFunctorAdd C a b).app X).hom =
    (↑(t.z a (b + c))).app ((shiftFunctor C (a + b + c)).obj X) ≫
      (↑(t.z b c)).app ((shiftFunctor C (a + b + c)).obj X) ≫
        eqToHom ⋯ ≫
          ((shiftFunctorAdd C a (b + c)).app X).hom ≫ ((shiftFunctorAdd C b c).app ((shiftFunctor C a).obj X)).hom
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
x : Cocycle K L n
h : x ∈ coboundaries K L n
⊢ toHom (mk x) = 0

Tactic:
← mk_eq_zero_iff

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
x : Cocycle K L n
h : mk x = 0
⊢ toHom (mk x) = 0
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
x : Cocycle K L n
h : mk x = 0
⊢ toHom (mk x) = 0

Tactic:
rw [h, map_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
x y : CohomologyClass K L n
h : toHom x = toHom y
⊢ x = y

Tactic:
obtain ⟨x, rfl⟩ := x.mk_surjective
    obtain ⟨y, rfl⟩ := y.mk_surjective
    rw [← sub_eq_zero, ← mk_sub, mk_eq_zero_iff, ← toHom_mk_eq_zero_iff,
      mk_sub, map_sub, h, sub_self]

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

Goal state before:
pp: 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
i : ι
hi : ¬c.Rel (c.prev i) i
hi' : ¬c'.Rel (c'.prev (e.f i)) (e.f i)
⊢ (K.extendXIso e ⋯).hom ≫ 0 ≫ (L.extendXIso e ⋯).inv = (prevD (e.f i)) (extend.hom e h.hom)

Tactic:
· simp [prevD_eq_zero _ _ hi']

Goal state after: