mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.Augment

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

Tactic:
aesop

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

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

Tactic:
aesop

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

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

Tactic:
aesop

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

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

Tactic:
aesop

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

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

Tactic:
aesop

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

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

Tactic:
aesop

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

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

Tactic:
aesop

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

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

Tactic:
aesop

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
⊢ ExtraDegeneracy.s f S 0 ≫ f.augmentedCechNerve.left.δ 1 =
    f.augmentedCechNerve.hom.app (op ⦋0⦌) ≫ S.section_ ≫ WidePullback.lift f.hom (fun x ↦ 𝟙 f.left) ⋯

Tactic:
dsimp [SimplicialObject.δ, SimplexCategory.δ]
    ext j
    · fin_cases j
      simp
    · simp

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

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝ : TotalComplexShape c₁ c₂ c₁₂
this : TotalComplexShape c₂ c₁ c₁₂ := symm c₁ c₂ c₁₂
i₁✝ i₁'✝ : I₁
x✝¹ : c₁.Rel i₁✝ i₁'✝
x✝ : I₂
⊢ 1 * c₁.ε₁ c₂ c₁₂ (i₁✝, x✝) = c₂.ε₂ c₁ c₁₂ (x✝, i₁✝) * 1

Tactic:
aesop

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

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝ : TotalComplexShape c₁ c₂ c₁₂
this : TotalComplexShape c₂ c₁ c₁₂ := symm c₁ c₂ c₁₂
x✝¹ : I₁
x✝ : I₂
⊢ ∀ {i₂' : I₂}, c₂.Rel x✝ i₂' → 1 * c₁.ε₂ c₂ c₁₂ (x✝¹, x✝) = c₂.ε₁ c₁ c₁₂ (x✝, x✝¹) * 1

Tactic:
aesop

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
F : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
p : I₁ × I₂ × I₃ → J
X₁ Y₁ : GradedObject I₁ C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : GradedObject I₃ C₃
f₃ : X₃ ⟶ Y₃
inst✝¹ : ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
inst✝ : ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).HasMap p
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : p (i₁, i₂, i₃) = j
⊢ ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ mapTrifunctorMapMap F p f₁ f₂ f₃ j =
    ((F.map (f₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫
      ((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫
        ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃) ≫ ιMapTrifunctorMapObj F p Y₁ Y₂ Y₃ i₁ i₂ i₃ j h

Tactic:
dsimp only [ιMapTrifunctorMapObj, mapTrifunctorMapMap]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
F : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
p : I₁ × I₂ × I₃ → J
X₁ Y₁ : GradedObject I₁ C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : GradedObject I₃ C₃
f₃ : X₃ ⟶ Y₃
inst✝¹ : ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
inst✝ : ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).HasMap p
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : p (i₁, i₂, i₃) = j
⊢ ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).ιMapObj p (i₁, i₂, i₃) j h ≫
      mapMap
        ((((mapTrifunctor F I₁ I₂ I₃).map f₁).app X₂).app X₃ ≫
          (((mapTrifunctor F I₁ I₂ I₃).obj Y₁).map f₂).app X₃ ≫ (((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).map f₃)
        p j =
    ((F.map (f₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫
      ((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫
        ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃) ≫
          ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h
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₁₂'
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₁₂ (i₁, i₂) • (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.d₁ c₁₂ (c₁.next i₁) i₂ i₁₂'' = 0

Tactic:
by_cases h₄ : c₁.Rel (c₁.next i₁) (c₁.next (c₁.next 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₁₂'' : I₁₂
h₁ : c₁₂.Rel 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₁)
h₄ : c₁.Rel (c₁.next i₁) (c₁.next (c₁.next i₁))
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) • (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.d₁ c₁₂ (c₁.next i₁) i₂ i₁₂'' = 0

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₁₂'
h₂ : c₁₂.Rel i₁₂' i₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₃ : c₁.Rel i₁ (c₁.next i₁)
h₄ : ¬c₁.Rel (c₁.next i₁) (c₁.next (c₁.next i₁))
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) • (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.d₁ c₁₂ (c₁.next i₁) i₂ i₁₂'' = 0
Module: Mathlib.CategoryTheory.GradedObject.Associator

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst✝⁹ : Category.{v_1, u_1} C₁
inst✝⁸ : Category.{v_2, u_2} C₂
inst✝⁷ : Category.{v_3, u_5} C₃
inst✝⁶ : Category.{v_4, u_6} C₄
inst✝⁵ : Category.{v_5, u_3} C₁₂
inst✝⁴ : Category.{v_6, u_4} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData r
ρ₂₃ : BifunctorComp₂₃IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝³ : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst✝² : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
inst✝¹ : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst✝ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H₁₂ : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
H₂₃ : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
⊢ ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫
      (mapBifunctorComp₁₂MapObjIso F₁₂ G ρ₁₂ X₁ X₂ X₃).inv j ≫
        mapMap ((((mapTrifunctorMapNatTrans associator.hom I₁ I₂ I₃).app X₁).app X₂).app X₃) r j ≫
          (mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃).hom j =
    ((associator.hom.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫
      ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h

Tactic:
ι_mapBifunctorComp₁₂MapObjIso_inv_assoc,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst✝⁹ : Category.{v_1, u_1} C₁
inst✝⁸ : Category.{v_2, u_2} C₂
inst✝⁷ : Category.{v_3, u_5} C₃
inst✝⁶ : Category.{v_4, u_6} C₄
inst✝⁵ : Category.{v_5, u_3} C₁₂
inst✝⁴ : Category.{v_6, u_4} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData r
ρ₂₃ : BifunctorComp₂₃IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝³ : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst✝² : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
inst✝¹ : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst✝ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H₁₂ : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
H₂₃ : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
⊢ ιMapTrifunctorMapObj (bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ i₁ i₂ i₃ j h ≫
      mapMap ((((mapTrifunctorMapNatTrans associator.hom I₁ I₂ I₃).app X₁).app X₂).app X₃) r j ≫
        (mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃).hom j =
    ((associator.hom.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫
      ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: 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 L M : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
ψ : L ⟶ M
c₁₂ : ComplexShape I₁₂
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : DecidableEq I₁₂
inst✝² : K.HasTotal c₁₂
inst✝¹ : L.HasTotal c₁₂
inst✝ : M.HasTotal c₁₂
⊢ (HomologicalComplex.forget C c₁₂).map (map (φ ≫ ψ) c₁₂) =
    (HomologicalComplex.forget C c₁₂).map (map φ c₁₂ ≫ map ψ c₁₂)

Tactic:
exact GradedObject.mapMap_comp (toGradedObjectMap φ) (toGradedObjectMap ψ) _

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫
      (total.map ((shiftFunctor₁ C x).map f) (up ℤ)).f n ≫ (L.totalShift₁Iso x).hom.f n =
    ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫ (K.totalShift₁Iso x).hom.f n ≫ (total.map f (up ℤ)).f (n + x)

Tactic:
ιTotal_map_assoc,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ (((shiftFunctor₁ C x).map f).f i₁).f i₂ ≫
      ((shiftFunctor₁ C x).obj L).ιTotal (up ℤ) i₁ i₂ n h ≫ (L.totalShift₁Iso x).hom.f n =
    ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫ (K.totalShift₁Iso x).hom.f n ≫ (total.map f (up ℤ)).f (n + x)
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ (f.f (i₁ + x)).f i₂ ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ =
    K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫ (total.map f (up ℤ)).f (n + x)

Tactic:
ιTotal_map

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ (f.f (i₁ + x)).f i₂ ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ =
    (f.f (i₁ + x)).f i₂ ≫ L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
y : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫
      (total.map ((shiftFunctor₂ C y).map f) (up ℤ)).f n ≫ (L.totalShift₂Iso y).hom.f n =
    ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫ (K.totalShift₂Iso y).hom.f n ≫ (total.map f (up ℤ)).f (n + y)

Tactic:
ιTotal_map_assoc,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
y : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ (((shiftFunctor₂ C y).map f).f i₁).f i₂ ≫
      ((shiftFunctor₂ C y).obj L).ιTotal (up ℤ) i₁ i₂ n h ≫ (L.totalShift₂Iso y).hom.f n =
    ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫ (K.totalShift₂Iso y).hom.f n ≫ (total.map f (up ℤ)).f (n + y)
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
y : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ (i₁ * y).negOnePow • (f.f i₁).f (i₂ + y) ≫ L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ =
    (i₁ * y).negOnePow • K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ (total.map f (up ℤ)).f (n + y)

Tactic:
ιTotal_map

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
y : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ (i₁ * y).negOnePow • (f.f i₁).f (i₂ + y) ≫ L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ =
    (i₁ * y).negOnePow • (f.f i₁).f (i₂ + y) ≫ L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n n₁ n₂ : ℤ
h : n₁ + n₂ = n
⊢ (((shiftFunctor₂ C y).obj K).shiftFunctor₁XXIso n₁ x (n₁ + x) ⋯ n₂).hom ≫
      ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) (n₁ + x) n₂ (n + x) ⋯ ≫
        (CochainComplex.shiftFunctorObjXIso (((shiftFunctor₂ C y).obj K).total (up ℤ)) x n (n + x) ⋯).inv ≫
          (K.totalShift₂Iso y).hom.f (n + x) =
    (x * y).negOnePow •
      ((shiftFunctor₁ C x).obj ((shiftFunctor₂ C y).obj K)).ιTotal (up ℤ) n₁ n₂ n h ≫
        (total.map ((shiftFunctor₁₂CommIso C x y).hom.app K) (up ℤ)).f n ≫
          (((shiftFunctor₁ C x).obj K).totalShift₂Iso y).hom.f n ≫
            (K.totalShift₁Iso x).hom.f (n + y) ≫
              ((shiftFunctorComm (CochainComplex C ℤ) x y).hom.app (K.total (up ℤ))).f n

Tactic:
ιTotal_map_assoc,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n n₁ n₂ : ℤ
h : n₁ + n₂ = n
⊢ (((shiftFunctor₂ C y).obj K).shiftFunctor₁XXIso n₁ x (n₁ + x) ⋯ n₂).hom ≫
      ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) (n₁ + x) n₂ (n + x) ⋯ ≫
        (CochainComplex.shiftFunctorObjXIso (((shiftFunctor₂ C y).obj K).total (up ℤ)) x n (n + x) ⋯).inv ≫
          (K.totalShift₂Iso y).hom.f (n + x) =
    (x * y).negOnePow •
      (((shiftFunctor₁₂CommIso C x y).hom.app K).f n₁).f n₂ ≫
        ((shiftFunctor₂ C y).obj ((shiftFunctor₁ C x).obj K)).ιTotal (up ℤ) n₁ n₂ n h ≫
          (((shiftFunctor₁ C x).obj K).totalShift₂Iso y).hom.f n ≫
            (K.totalShift₁Iso x).hom.f (n + y) ≫
              ((shiftFunctorComm (CochainComplex C ℤ) x y).hom.app (K.total (up ℤ))).f n
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n m✝ p : ℤ
α₁ α₂ : Cocycle K L n
m : ℤ
hm : m + 1 = n
β₁ : Cochain K L m
hβ₁ : δ m n β₁ = ↑α₁
hm' : m + 1 = n
β₂ : Cochain K L m
hβ₂ : δ m n β₂ = ↑α₂
⊢ δ m n (β₁ + β₂) = ↑(α₁ + α₂)

Tactic:
aesop

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n m✝ p : ℤ
α : Cocycle K L n
m : ℤ
hm : m + 1 = n
β : Cochain K L m
hβ : δ m n β = ↑α
⊢ δ m n (-β) = ↑(-α)

Tactic:
aesop

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

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
L : CochainComplex C ℤ
x✝ : L.IsKInjective
K : HomologicalComplex C (ComplexShape.up ℤ)
hK : K.Acyclic
f : K ⟶ L
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f = 0

Tactic:
HomotopyCategory.eq_of_homotopy f 0 (IsKInjective.homotopyZero f hK),

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
L : CochainComplex C ℤ
x✝ : L.IsKInjective
K : HomologicalComplex C (ComplexShape.up ℤ)
hK : K.Acyclic
f : K ⟶ L
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map 0 = 0
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

Goal state before:
pp: case pos.e_a
ι : 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 : ι
⊢ (K.extendXIso e ⋯).hom ≫ (prevD i) h.hom ≫ (L.extendXIso e ⋯).inv = (prevD (e.f i)) (extend.hom e h.hom)

Tactic:
· by_cases hi : c.Rel (c.prev i) i
        · have hi' : c'.Rel (e.f (c.prev i)) (e.f i) := by rwa [e.rel_iff]
          simp [prevD_eq _ hi, prevD_eq _ hi', extend.hom_eq _ _ rfl rfl,
            extend_d_eq _ _ rfl rfl]
        · rw [prevD_eq_zero _ _ hi]
          by_cases hi' : c'.Rel (c'.prev (e.f i)) (e.f i)
          · simp [prevD_eq _ hi', L.extend_d_to_eq_zero _ _ _ _ rfl hi]
          · simp [prevD_eq_zero _ _ hi']

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.le n ≤ t.le (n + ↑a)
H_zero : H 0
H_one : H 1
a b c : ℕ
h : a + b = c
ha : H a
hb : H b
n : ℤ
⊢ t.le n ≤ t.le (n + ↑a + ↑b)

Tactic:
exact (ha n).trans (hb (n + a))

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.le n ≤ t.le (n + ↑a)
H_zero : H 0
H_one : H 1
H_add : ∀ (a b c : ℕ), a + b = c → H a → H b → H c
a : ℕ
⊢ H a

Tactic:
induction a with

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.ge (n + ↑a) ≤ t.ge n
H_zero : H 0
H_one : H 1
H_add : ∀ (a b c : ℕ), a + b = c → H a → H b → H c
a : ℕ
⊢ H a

Tactic:
induction a with

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝³ : e.IsRelIff
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
K L : HomologicalComplex C c
φ : K ⟶ L
⊢ ∃ a, (e.extendHomotopyFunctor C).map a = (HomotopyCategory.quotient C c').map ((e.extendFunctor C).map φ)

Tactic:
exact ⟨(HomotopyCategory.quotient _ _).map φ, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

Goal state before:
pp: case hX
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
t : TStructure C
X Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ < n₁
inst✝¹ : t.IsLE X n₀
inst✝ : t.IsGE Y n₁
this✝¹ : t.IsLE ((shiftFunctor C n₀).obj X) 0
this✝ : t.IsGE ((shiftFunctor C n₀).obj Y) (n₁ - n₀)
this : t.IsGE ((shiftFunctor C n₀).obj Y) 1
⊢ t.le 0 ((shiftFunctor C n₀).obj X)

Tactic:
apply t.le_of_isLE

Goal state after: