mathlib-initiative/mathlib-tactics huggingface dataset:
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₁₂ 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:
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.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 : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
⊢ K.ιTotal c₁₂ i₁ i₂ i₁₂ h ≫ K.D₂ c₁₂ i₁₂ i₁₂' = K.d₂ c₁₂ i₁ i₂ i₁₂'

Tactic:
by
  apply totalAux.ιMapObj_D₂

Goal state after:
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
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : ¬c₁.Rel (c₁.prev i₁) i₁
h₄ : c₂.Rel i₂ (c₂.next i₂)
h₅ : c.Rel j (c.next j)
⊢ c₁.π c₂ c (i₁, c₂.next i₂) = c.next j

Tactic:
← ComplexShape.next_π₂ c₁ c i₁ h₄,

Goal state after:
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
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : ¬c₁.Rel (c₁.prev i₁) i₁
h₄ : c₂.Rel i₂ (c₂.next i₂)
h₅ : c.Rel j (c.next j)
⊢ c.next (c₁.π c₂ c (i₁, i₂)) = c.next j
Module: Mathlib.Algebra.Homology.BifunctorAssociator

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
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✝¹⁵ : HasZeroMorphisms C₁
inst✝¹⁴ : HasZeroMorphisms C₂
inst✝¹³ : HasZeroMorphisms C₃
inst✝¹² : Preadditive C₁₂
inst✝¹¹ : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
inst✝¹⁰ : F₁₂.PreservesZeroMorphisms
inst✝⁹ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝⁸ : G.Additive
inst✝⁷ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst✝⁶ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst✝⁵ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁴ : TotalComplexShape c₁₂ c₃ c₄
inst✝³ : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝² : DecidableEq ι₁₂
inst✝¹ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j j' : ι₄
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
inst✝ : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
⊢ ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h ≫ D₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' = d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'

Tactic:
simp [D₁]

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

Goal state before:
pp: case neg
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
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✝¹⁴ : HasZeroMorphisms C₁
inst✝¹³ : HasZeroMorphisms C₂
inst✝¹² : HasZeroMorphisms C₃
inst✝¹¹ : Preadditive C₁₂
inst✝¹⁰ : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
inst✝⁹ : F₁₂.PreservesZeroMorphisms
inst✝⁸ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝⁷ : G.Additive
inst✝⁶ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst✝⁵ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : TotalComplexShape c₁₂ c₃ c₄
inst✝² : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝¹ : DecidableEq ι₁₂
inst✝ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j j' : ι₄
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
h₁ : ¬c₃.Rel i₃ (c₃.next i₃)
⊢ (G.map (K₁.ιMapBifunctor K₂ F₁₂ c₁₂ i₁ i₂ (c₁.π c₂ c₁₂ (i₁, i₂)) ⋯)).app (K₃.X i₃) ≫
      mapBifunctor.d₂ (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄ (c₁.π c₂ c₁₂ (i₁, i₂)) i₃ j' =
    d₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'

Tactic:
· rw [mapBifunctor.d₂_eq_zero _ _ _ _ _ _ _ h₁, comp_zero,
      d₃_eq_zero _ _ _ _ _ _ _ _ _ _ _ h₁]

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

Goal state before:
pp: case neg
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₂ f₂' : K₂ ⟶ L₂
h₂ : Homotopy f₂ f₂'
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
this✝² : TotalComplexShape c₂ c₁ c := TotalComplexShape.symm c₁ c₂ c
this✝¹ : TotalComplexShapeSymmetry c₁ c₂ c := TotalComplexShape.symmSymmetry c₁ c₂ c
this✝ : F.flip.Additive
this : ∀ (X₁ : C₂), (F.flip.obj X₁).Additive
H : Homotopy (mapBifunctorMap f₁ f₂ F c) (mapBifunctorMap f₁ f₂' F c) :=
  (Homotopy.ofEq ⋯).trans
    ((((mapBifunctorMapHomotopy₁ h₂ f₁ F.flip c).compRight (L₁.mapBifunctorFlipIso L₂ F c).hom).compLeft
          (K₁.mapBifunctorFlipIso K₂ F c).inv).trans
      (Homotopy.ofEq ⋯))
j j' : J
i₁ : I₁
i₂ : I₂
hj : c₁.π c₂ c (i₁, i₂) = j
hj' : ¬c₁.π c₂ c (i₁, c₂.prev i₂) = j'
⊢ c₁.ε₂ c₂ c (i₁, c₂.prev i₂) •
      (F.map (f₁.f i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (h₂.hom i₂ (c₂.prev i₂)) ≫ L₁.ιMapBifunctorOrZero L₂ F c i₁ (c₂.prev i₂) j' =
    c₁.σ c₂ c i₁ i₂ •
      c₂.ε₁ c₁ c (c₂.prev i₂, i₁) •
        (F.map (f₁.f i₁)).app (K₂.X i₂) ≫
          (F.obj (L₁.X i₁)).map (h₂.hom i₂ (c₂.prev i₂)) ≫
            L₂.ιMapBifunctorOrZero L₁ F.flip c (c₂.prev i₂) i₁ j' ≫ (L₁.mapBifunctorFlipIso L₂ F c).hom.f j'

Tactic:
· rw [ιMapBifunctorOrZero_eq_zero _ _ _ _ _ _ _ hj',
        ιMapBifunctorOrZero_eq_zero _ _ _ _ _ _ _ (by rwa [ComplexShape.π_symm c₁ c₂ c]),
        comp_zero, comp_zero, smul_zero, zero_comp, comp_zero,
        comp_zero, smul_zero, smul_zero]

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₂ L₂ : CochainComplex C₂ ℤ
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
y : ℤ
inst✝ : K₁.HasMapBifunctor K₂ F
⊢ ∀ (i j : ℤ),
    (ComplexShape.up ℤ).Rel i j →
      (Hom.isoOfComponents
              (fun x ↦
                Iso.refl
                  (((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj
                            ((CategoryTheory.shiftFunctor (HomologicalComplex C₂ (ComplexShape.up ℤ)) y).obj K₂)).X
                        i).X
                    x))
              ⋯).hom ≫
          ((HomologicalComplex₂.shiftFunctor₂ D y).obj
                (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂)).d
            i j =
        (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj
                ((CategoryTheory.shiftFunctor (HomologicalComplex C₂ (ComplexShape.up ℤ)) y).obj K₂)).d
            i j ≫
          (Hom.isoOfComponents
              (fun x ↦
                Iso.refl
                  (((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj
                            ((CategoryTheory.shiftFunctor (HomologicalComplex C₂ (ComplexShape.up ℤ)) y).obj K₂)).X
                        j).X
                    x))
              ⋯).hom

Tactic:
intros
      ext
      dsimp
      simp only [id_comp, comp_id]

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₁.ιMapBifunctor ((CategoryTheory.shiftFunctor (CochainComplex C₂ ℤ) y).obj K₂) F n₁ n₂ n h ≫
      (HomologicalComplex₂.total.map (K₁.mapBifunctorHomologicalComplexShift₂Iso K₂ F y).hom (ComplexShape.up ℤ)).f n ≫
        ((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂).totalShift₂Iso
                y).hom.f
          n =
    (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 only [HomologicalComplex₂.ιTotal_map_assoc,
    HomologicalComplex₂.ι_totalShift₂Iso_hom_f _ _ _ _ _ _ _ hm₂ _ hm]

Goal state after:
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
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
⊢ (n₁ * y + x * y).negOnePow •
      𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫
        K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + x + y)) =
    (n₁ * y + x * y).negOnePow •
      ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) n₁ (n₂ + y) (n + y) ⋯ ≫
        (K.totalShift₁Iso x).hom.f (n + y) ≫ ((shiftFunctorComm (CochainComplex C ℤ) x y).hom.app (K.total (up ℤ))).f n

Tactic:
rw [id_comp, comp_id,
    ι_totalShift₁Iso_hom_f_assoc _ x n₁ (n₂ + y) (n + y) (by lia) _ rfl (n + x + y) (by lia),
    CochainComplex.shiftFunctorComm_hom_app_f]

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
⊢ (n₁ * y + x * y).negOnePow • K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ =
    (n₁ * y + x * y).negOnePow •
      (K.shiftFunctor₁XXIso n₁ x (n₁ + x) ⋯ (n₂ + y)).hom ≫
        K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ ≫
          (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x (n + y) (n + x + y) ⋯).inv ≫
            ((K.total (up ℤ)).XIsoOfEq ⋯).hom
Module: Mathlib.Algebra.Homology.CommSq

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (biprod.desc f (-g)) 0
m : s.pt ⟶ sq.kernelFork.pt
hm : m ≫ Fork.ι sq.kernelFork = s.ι
⊢ m = PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯

Tactic:
apply PullbackCone.IsLimit.hom_ext h

Goal state after:
case h₀
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (biprod.desc f (-g)) 0
m : s.pt ⟶ sq.kernelFork.pt
hm : m ≫ Fork.ι sq.kernelFork = s.ι
⊢ m ≫ (PullbackCone.mk fst snd ⋯).fst =
    PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ (PullbackCone.mk fst snd ⋯).fst

case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (biprod.desc f (-g)) 0
m : s.pt ⟶ sq.kernelFork.pt
hm : m ≫ Fork.ι sq.kernelFork = s.ι
⊢ m ≫ (PullbackCone.mk fst snd ⋯).snd =
    PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ (PullbackCone.mk fst snd ⋯).snd
Module: Mathlib.CategoryTheory.LiftingProperties.Limits

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst✝ : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
w : (s ≫ u) ≫ g' = f ≫ t ≫ v
⊢ t ≫ h.desc u ⋯.lift ⋯ ≫ g' = t ≫ v

Tactic:
h.inr_desc_assoc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst✝ : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
w : (s ≫ u) ≫ g' = f ≫ t ≫ v
⊢ ⋯.lift ≫ g' = t ≫ v
Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : CategoryWithCofibrations C
inst✝ : CategoryWithWeakEquivalences C
⊢ trivialCofibrations C f ↔ Cofibration f ∧ WeakEquivalence f

Tactic:
by
  rw [cofibration_iff, weakEquivalence_iff]
  rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ModelCategory C
A : C
P✝ : PathObject A
inst✝¹ : IsFibrant A
P P' : PathObject A
inst✝ : P'.IsGood
⊢ WeakEquivalence (P.trans P'.toPrepathObject).ι

Tactic:
have : WeakEquivalence (pullback.lift P.ι P'.ι (by simp) ≫
        pullback.fst P.p₁ P'.p₀ ≫ P.p₀) := by
      rw [pullback.lift_fst_assoc, PrepathObject.ι_p₀]
      infer_instance

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ModelCategory C
A : C
P✝ : PathObject A
inst✝¹ : IsFibrant A
P P' : PathObject A
inst✝ : P'.IsGood
this : WeakEquivalence (pullback.lift P.ι P'.ι ⋯ ≫ pullback.fst P.p₁ P'.p₀ ≫ P.p₀)
⊢ WeakEquivalence (P.trans P'.toPrepathObject).ι
Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject

Goal state before:
pp: case h₁
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
A : C
P✝ : PathObject A
inst✝² : IsFibrant A
P P' : PathObject A
inst✝¹ : P.IsGood
inst✝ : P'.IsGood
ψ : (P.trans P').P ⟶ P.P ⨯ A := ⋯
⊢ (ψ ≫ prod.map P.p₁ (𝟙 A)) ≫ prod.fst = (pullback.snd P.p₁ P'.p₀ ≫ P'.p) ≫ prod.fst

pp: case h₂
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
A : C
P✝ : PathObject A
inst✝² : IsFibrant A
P P' : PathObject A
inst✝¹ : P.IsGood
inst✝ : P'.IsGood
ψ : (P.trans P').P ⟶ P.P ⨯ A := ⋯
⊢ (ψ ≫ prod.map P.p₁ (𝟙 A)) ≫ prod.snd = (pullback.snd P.p₁ P'.p₀ ≫ P'.p) ≫ prod.snd

Tactic:
· simp [ψ, pullback.condition]

Goal state after:
case h₂
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
A : C
P✝ : PathObject A
inst✝² : IsFibrant A
P P' : PathObject A
inst✝¹ : P.IsGood
inst✝ : P'.IsGood
ψ : (P.trans P').P ⟶ P.P ⨯ A := ⋯
⊢ (ψ ≫ prod.map P.p₁ (𝟙 A)) ≫ prod.snd = (pullback.snd P.p₁ P'.p₀ ≫ P'.p) ≫ prod.snd
Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CategoryWithWeakEquivalences C
X Y : C
f g : X ⟶ Y
P : Cylinder X
h : P.LeftHomotopy f g
L : C ⥤ (weakEquivalences C).Localization := (weakEquivalences C).Q
⊢ L.map f = L.map g

Tactic:
suffices L.map P.i₀ = L.map P.i₁ by
    simp only [← h.h₀, ← h.h₁, L.map_comp, this]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CategoryWithWeakEquivalences C
X Y : C
f g : X ⟶ Y
P : Cylinder X
h : P.LeftHomotopy f g
L : C ⥤ (weakEquivalences C).Localization := (weakEquivalences C).Q
⊢ L.map P.i₀ = L.map P.i₁
Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : CategoryWithWeakEquivalences C
f g : X ⟶ Y
Z : C
i : Z ⟶ X
P : PathObject Y
h : P.RightHomotopy f g
⊢ RightHomotopyRel (i ≫ f) (i ≫ g)

Tactic:
exact (h.precomp i).rightHomotopyRel

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : P.IsTriangulated
⊢ P.op.trW = P.trW.op

Tactic:
ext X Y f

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : P.IsTriangulated
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ P.op.trW f ↔ P.trW.op f
Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus

Goal state before:
pp: case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K : CochainComplex C ℤ
n : ℤ
hn : K.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n - 1) isStrictlyGE_iff._auto_1
j : ℤ
hj : (ComplexShape.up ℤ).Rel i j
⊢ IsZero (K.X j)

Tactic:
simp only [ComplexShape.up_Rel] at hj
    exact K.isZero_of_isStrictlyGE n _ (by lia)

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁸ : Category.{?u.6, u_1} C
inst✝⁷ : Category.{?u.9, u_2} D
inst✝⁶ : Category.{?u.12, u_3} E
A : Type u_4
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift D A
inst✝³ : HasShift E A
F : SingleFunctors C E A
G : D ⥤ E
inst✝² : G.CommShift A
inst✝¹ : G.Full
inst✝ : G.Faithful
Φ : A → C ⥤ D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
n a a' : A
ha' : n + a = a'
⊢ (((F.lift G Φ hΦ).postcomp G).shiftIso n a a' ha').hom ≫ (hΦ a).hom =
    whiskerRight (hΦ a').hom (shiftFunctor E n) ≫ (F.shiftIso n a a' ha').hom

Tactic:
ext X
    have := (hΦ a).inv_hom_id_app X
    dsimp at this
    simp [map_lift_shiftIso_hom_app, this]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : Preadditive D
A : Type u_3
inst✝¹ : Category.{v_3, u_3} A
inst✝ : Abelian A
a : ℤ
⊢ (quasiIso A).inverseImage (shiftFunctor (Plus A) a) = quasiIso A

Tactic:
ext X Y f

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : Preadditive D
A : Type u_3
inst✝¹ : Category.{v_3, u_3} A
inst✝ : Abelian A
a : ℤ
X Y : Plus A
f : X ⟶ Y
⊢ (quasiIso A).inverseImage (shiftFunctor (Plus A) a) f ↔ quasiIso A f