mathlib-initiative/mathlib-tactics huggingface dataset:
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₂ 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
⊢ mapBifunctorMap f₁ f₂ F c =
    (K₁.mapBifunctorFlipIso K₂ F c).inv ≫ mapBifunctorMap f₂ f₁ F.flip c ≫ (L₁.mapBifunctorFlipIso L₂ F c).hom

Tactic:
by

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₂ 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
⊢ (K₁.mapBifunctorFlipIso K₂ F c).inv ≫ mapBifunctorMap f₂' f₁ F.flip c ≫ (L₁.mapBifunctorFlipIso L₂ F c).hom =
    mapBifunctorMap f₁ f₂' F c

Tactic:
by

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 y : ℤ
inst✝ : K.HasTotal (up ℤ)
n n' : ℤ
h : n + y = n'
⊢ ((((shiftFunctor₂ C y).obj K).totalDesc fun p q hpq ↦ (p * y).negOnePow • K.ιTotal (up ℤ) p (q + y) n' ⋯) ≫
      K.totalDesc fun p q hpq ↦
        (p * y).negOnePow •
          (XXIsoOfEq C (up ℤ) (up ℤ) K ⋯ ⋯).inv ≫ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) p (q - y) n ⋯) =
    𝟙 ((((shiftFunctor₂ C y).obj K).total (up ℤ)).X n)

Tactic:
by

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 y : ℤ
inst✝ : K.HasTotal (up ℤ)
n n' : ℤ
h : n + y = n'
⊢ ((K.totalDesc fun p q hpq ↦
        (p * y).negOnePow •
          (XXIsoOfEq C (up ℤ) (up ℤ) K ⋯ ⋯).inv ≫ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) p (q - y) n ⋯) ≫
      ((shiftFunctor₂ C y).obj K).totalDesc fun p q hpq ↦ (p * y).negOnePow • K.ιTotal (up ℤ) p (q + y) n' ⋯) =
    𝟙 ((K.total (up ℤ)).X n')

Tactic:
by

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₂ 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
⊢ c₂.π c₁ c (i₂, i₁) = j

Tactic:
by

Goal state after:
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
⊢ ι 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:
by

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₂ 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 (c₂.prev i₂, i₁) = j'

Tactic:
by

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 : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ (up ℤ).π (up ℤ) (up ℤ) (p + 1, q) = n₁

Tactic:
by

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 : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ (up ℤ).π (up ℤ) (up ℤ) (p + 1, q + y) = n₁'

Tactic:
by

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 : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
⊢ ((shiftFunctor₂ C y).obj K).D₁ (up ℤ) n₀ n₁ ≫ (K.totalShift₂XIso y n₁ n₁' h₁).hom =
    y.negOnePow • (K.totalShift₂XIso y n₀ n₀' h₀).hom ≫ K.D₁ (up ℤ) n₀' n₁'

Tactic:
by

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 : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ (up ℤ).π (up ℤ) (up ℤ) (p, q + 1) = n₁

Tactic:
by

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 : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ (up ℤ).π (up ℤ) (up ℤ) (p, q + 1 + y) = n₁'

Tactic:
by

Goal state after:
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₄
j j' : ι₄
inst✝ : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
i₁₂ : ι₁₂ := c₁.π c₂ c₁₂ (i₁, i₂)
h₁ : c₁₂.Rel i₁₂ (c₁₂.next i₁₂)
h₂ : c₁₂.π c₃ c₄ (c₁₂.next i₁₂, i₃) = j'
h₃ : c₁.Rel i₁ (c₁.next i₁)
h₄ : c₁.π c₂ c₁₂ (c₁.next i₁, i₂) = c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))
⊢ c₁.r c₂ c₃ c₁₂ c₄ (c₁.next i₁, i₂, i₃) = j'

Tactic:
by

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 : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
⊢ ((shiftFunctor₂ C y).obj K).D₂ (up ℤ) n₀ n₁ ≫ (K.totalShift₂XIso y n₁ n₁' h₁).hom =
    y.negOnePow • (K.totalShift₂XIso y n₀ n₀' h₀).hom ≫ K.D₂ (up ℤ) n₀' n₁'

Tactic:
by

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 y : ℤ
inst✝ : K.HasTotal (up ℤ)
n n' : ℤ
x✝ : (up ℤ).Rel n n'
⊢ (K.totalShift₂XIso y n (n + y) ⋯).hom ≫ ((shiftFunctor (HomologicalComplex C (up ℤ)) y).obj (K.total (up ℤ))).d n n' =
    (((shiftFunctor₂ C y).obj K).total (up ℤ)).d n n' ≫ (K.totalShift₂XIso y n' (n' + y) ⋯).hom

Tactic:
by

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 y : ℤ
inst✝ : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
b' : ℤ
hb' : b' = b + y
n' : ℤ
hn' : n' = n + y
⊢ (up ℤ).π (up ℤ) (up ℤ) (a, b') = n'

Tactic:
by

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₂ 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 (c₂.prev i₂, i₁) ≠ j'

Tactic:
by

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 : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
b' : ℤ
hb' : b' = b + y
n' : ℤ
hn' : n' = n + y
⊢ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) a b n h ≫ (K.totalShift₂Iso y).hom.f n =
    (a * y).negOnePow •
      (K.shiftFunctor₂XXIso a b y b' hb').hom ≫
        K.ιTotal (up ℤ) a b' n' ⋯ ≫ (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n n' hn').inv

Tactic:
by

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 y : ℤ
inst✝ : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
b' n' : ℤ
hb' : a + b' = n'
hn' : n' = n + y
⊢ b' = b + y

Tactic:
by

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 : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
b' : ℤ
hb' : a + b' = n + y
⊢ b = b' - y

Tactic:
by

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 : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
b' n' : ℤ
hb' : a + b' = n'
hn' : n' = n + y
⊢ K.ιTotal (up ℤ) a b' n' hb' ≫
      (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n n' hn').inv ≫ (K.totalShift₂Iso y).inv.f n =
    (a * y).negOnePow • (K.shiftFunctor₂XXIso a b y b' ⋯).inv ≫ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) a b n h

Tactic:
by

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₂ 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 ⋯))
⊢ hom₂ f₁ h₂ F c = H.hom

Tactic:
by

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
y : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
⊢ total.map ((shiftFunctor₂ C y).map f) (up ℤ) ≫ (L.totalShift₂Iso y).hom =
    (K.totalShift₂Iso y).hom ≫ (shiftFunctor (HomologicalComplex C (up ℤ)) y).map (total.map f (up ℤ))

Tactic:
by

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₂ 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 ⋯))
hom₂_eq : hom₂ f₁ h₂ F c = H.hom
j j' : J
h : ¬c.Rel j' j
⊢ hom₂ f₁ h₂ F c j j' = 0

Tactic:
by

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₂ 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 ⋯))
hom₂_eq : hom₂ f₁ h₂ F c = H.hom
j : J
⊢ (mapBifunctorMap f₁ f₂ F c).f j =
    (dNext j) (hom₂ f₁ h₂ F c) + (prevD j) (hom₂ f₁ h₂ F c) + (mapBifunctorMap f₁ f₂' F c).f j

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
x✝¹ x✝ : ℤ
⊢ (fun n ↦ -n) x✝¹ = (fun n ↦ -n) x✝ → x✝¹ = x✝

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ ∀ {i₁ i₂ : ℤ}, (up ℤ).Rel i₁ i₂ → (down ℤ).Rel (-i₁) (-i₂)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ ∀ (i₁ i₂ : ℤ), (down ℤ).Rel (embeddingUpIntDownInt.f i₁) (embeddingUpIntDownInt.f i₂) → (up ℤ).Rel i₁ i₂

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ ∀ {i₁ i₂ : ℤ}, (down ℤ).Rel i₁ i₂ → (up ℤ).Rel (-i₁) (-i₂)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ ∀ (i₁ i₂ : ℤ), (up ℤ).Rel (embeddingDownIntUpInt.f i₁) (embeddingDownIntUpInt.f i₂) → (down ℤ).Rel i₁ i₂

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℤ
n : ℤ
⊢ n = ComplexShape.embeddingUpIntDownInt.f (ComplexShape.embeddingDownIntUpInt.f n)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ ComplexShape.embeddingDownIntUpInt.f (ComplexShape.embeddingUpIntDownInt.f n) = n

Tactic:
by

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 f g
p q : ℤ
hpq : ¬(ComplexShape.up ℤ).Rel q p
⊢ (h.hom (-q) (-p)).op = 0

Tactic:
by

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
⊢ ∀ (i j : ℤ),
    (ComplexShape.up ℤ).Rel i j →
      (Iso.refl
              ((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj
                        ((CategoryTheory.shiftFunctor (HomologicalComplex C₁ (ComplexShape.up ℤ)) x).obj K₁)).obj
                    K₂).X
                i)).hom ≫
          ((HomologicalComplex₂.shiftFunctor₁ D x).obj
                (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj K₁).obj K₂)).d
            i j =
        (((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj
                    ((CategoryTheory.shiftFunctor (HomologicalComplex C₁ (ComplexShape.up ℤ)) x).obj K₁)).obj
                K₂).d
            i j ≫
          (Iso.refl
              ((((F.mapBifunctorHomologicalComplex (ComplexShape.up ℤ) (ComplexShape.up ℤ)).obj
                        ((CategoryTheory.shiftFunctor (HomologicalComplex C₁ (ComplexShape.up ℤ)) x).obj K₁)).obj
                    K₂).X
                j)).hom

Tactic:
by

Goal state after: