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

Goal state before:
pp: case pos
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 i₁ (c₁.next i₁)
⊢ (F.map (K₁.d i₁ (c₁.next i₁))).app (K₂.X i₂) ≫
      (F.map (h₁.hom (c₁.next i₁) i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂ j h =
    c₁.ε₁ c₂ c (i₁, i₂) •
      (F.map (K₁.d i₁ (c₁.next i₁))).app (K₂.X i₂) ≫
        (c₁.ε₁ c₂ c (i₁, i₂) •
          (F.map (h₁.hom (c₁.next i₁) i₁)).app (K₂.X i₂) ≫
            (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c i₁ i₂ j)

Tactic:
Linear.comp_units_smul,

Goal state after:
case pos
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 i₁ (c₁.next i₁)
⊢ (F.map (K₁.d i₁ (c₁.next i₁))).app (K₂.X i₂) ≫
      (F.map (h₁.hom (c₁.next i₁) i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂ j h =
    c₁.ε₁ c₂ c (i₁, i₂) •
      c₁.ε₁ c₂ c (i₁, i₂) •
        (F.map (K₁.d i₁ (c₁.next i₁))).app (K₂.X i₂) ≫
          (F.map (h₁.hom (c₁.next i₁) i₁)).app (K₂.X i₂) ≫
            (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c i₁ i₂ j
Module: Mathlib.Algebra.Homology.BifunctorHomotopy

Goal state before:
pp: case pos
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₁
⊢ (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫
      (F.map (L₁.d (c₁.prev i₁) i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂ j h =
    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₂) ≫
          (c₁.ε₁ c₂ c (c₁.prev i₁, i₂) •
            ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).d (c₁.prev i₁) i₁).f i₂ ≫
              (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).ιTotal c i₁ i₂ j h)

Tactic:
Linear.comp_units_smul,

Goal state after:
case pos
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₁
⊢ (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫
      (F.map (L₁.d (c₁.prev i₁) i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂ j h =
    c₁.ε₁ c₂ c (c₁.prev i₁, i₂) •
      (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫
        (c₁.ε₁ c₂ c (c₁.prev i₁, i₂) •
          (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫
            ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).d (c₁.prev i₁) i₁).f i₂ ≫
              (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).ιTotal c i₁ i₂ j h)
Module: Mathlib.Algebra.Homology.BifunctorHomotopy

Goal state before:
pp: case pos
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₁
⊢ (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫
      (F.map (L₁.d (c₁.prev i₁) i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂ j h =
    c₁.ε₁ c₂ c (c₁.prev i₁, i₂) •
      (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫
        (c₁.ε₁ c₂ c (c₁.prev i₁, i₂) •
          (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫
            ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).d (c₁.prev i₁) i₁).f i₂ ≫
              (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).ιTotal c i₁ i₂ j h)

Tactic:
Linear.comp_units_smul,

Goal state after:
case pos
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₁
⊢ (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫
      (F.map (L₁.d (c₁.prev i₁) i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂ j h =
    c₁.ε₁ c₂ c (c₁.prev i₁, i₂) •
      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₂) ≫
            ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).d (c₁.prev i₁) i₁).f i₂ ≫
              (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).ιTotal c i₁ i₂ j h
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ (((shiftFunctor₁ C x).obj K).d₁ (up ℤ) p q n₁ ≫
      ((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq ↦ K.ιTotal (up ℤ) (p + x) q n₁' ⋯) =
    ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      (x.negOnePow •
        (((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq ↦ K.ιTotal (up ℤ) (p + x) q n₀' ⋯) ≫ K.D₁ (up ℤ) n₀' n₁')

Tactic:
Linear.comp_units_smul,

Goal state after:
case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ (((shiftFunctor₁ C x).obj K).d₁ (up ℤ) p q n₁ ≫
      ((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq ↦ K.ιTotal (up ℤ) (p + x) q n₁' ⋯) =
    x.negOnePow •
      ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
        (((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq ↦ K.ιTotal (up ℤ) (p + x) q n₀' ⋯) ≫ K.D₁ (up ℤ) n₀' n₁'
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ (((shiftFunctor₁ C x).obj K).d₂ (up ℤ) p q n₁ ≫
      ((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq ↦ K.ιTotal (up ℤ) (p + x) q n₁' ⋯) =
    ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      (x.negOnePow •
        (((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq ↦ K.ιTotal (up ℤ) (p + x) q n₀' ⋯) ≫ K.D₂ (up ℤ) n₀' n₁')

Tactic:
Linear.comp_units_smul,

Goal state after:
case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ (((shiftFunctor₁ C x).obj K).d₂ (up ℤ) p q n₁ ≫
      ((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq ↦ K.ιTotal (up ℤ) (p + x) q n₁' ⋯) =
    x.negOnePow •
      ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
        (((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq ↦ K.ιTotal (up ℤ) (p + x) q n₀' ⋯) ≫ K.D₂ (up ℤ) n₀' n₁'
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 : ℤ
inst✝ : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
a' : ℤ
ha' : a' = a + x
n' : ℤ
hn' : n' = n + x
⊢ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) a b n h ≫ (K.totalShift₁Iso x).hom.f n =
    (K.shiftFunctor₁XXIso a x a' ha' b).hom ≫
      K.ιTotal (up ℤ) a' b n' ⋯ ≫ (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n n' hn').inv

Tactic:
by
  subst ha' hn'
  dsimp [totalShift₁Iso, totalShift₁XIso]
  simp only [ι_totalDesc, comp_id, id_comp]

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

Goal state before:
pp: case pos
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₀
⊢ (((shiftFunctor₂ C y).obj K).d₁ (up ℤ) p q n₁ ≫
      ((shiftFunctor₂ C y).obj K).totalDesc fun p q hpq ↦ (p * y).negOnePow • K.ιTotal (up ℤ) p (q + y) n₁' ⋯) =
    ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      (y.negOnePow •
        (((shiftFunctor₂ C y).obj K).totalDesc fun p q hpq ↦ (p * y).negOnePow • K.ιTotal (up ℤ) p (q + y) n₀' ⋯) ≫
          K.D₁ (up ℤ) n₀' n₁')

Tactic:
Linear.comp_units_smul,

Goal state after:
case pos
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₀
⊢ (((shiftFunctor₂ C y).obj K).d₁ (up ℤ) p q n₁ ≫
      ((shiftFunctor₂ C y).obj K).totalDesc fun p q hpq ↦ (p * y).negOnePow • K.ιTotal (up ℤ) p (q + y) n₁' ⋯) =
    y.negOnePow •
      ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
        (((shiftFunctor₂ C y).obj K).totalDesc fun p q hpq ↦ (p * y).negOnePow • K.ιTotal (up ℤ) p (q + y) n₀' ⋯) ≫
          K.D₁ (up ℤ) n₀' n₁'
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: case pos
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₀
⊢ (K.d p (p + 1)).f (q + y) ≫ (((p + 1) * y).negOnePow • K.ιTotal (up ℤ) (p + 1) (q + y) n₁' ⋯) =
    (y.negOnePow * (p * y).negOnePow) • (K.d p (p + 1)).f (q + y) ≫ K.ιTotal (up ℤ) (p + 1) (q + y) n₁' ⋯

Tactic:
Linear.comp_units_smul,

Goal state after:
case pos
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₀
⊢ ((p + 1) * y).negOnePow • (K.d p (p + 1)).f (q + y) ≫ K.ιTotal (up ℤ) (p + 1) (q + y) n₁' ⋯ =
    (y.negOnePow * (p * y).negOnePow) • (K.d p (p + 1)).f (q + y) ≫ K.ιTotal (up ℤ) (p + 1) (q + y) n₁' ⋯
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_cases h : (up ℤ).Rel n₀ n₁
  · apply total.hom_ext
    intro p q hpq
    dsimp at h hpq
    dsimp [totalShift₂XIso]
    rw [ι_D₁_assoc, Linear.comp_units_smul, ι_totalDesc_assoc, Linear.units_smul_comp,
      ι_D₁, smul_smul, ((shiftFunctor₂ C y).obj K).d₁_eq _ rfl _ _ (by dsimp; lia),
      K.d₁_eq _ rfl _ _ (by dsimp; lia)]
    dsimp
    rw [one_smul, one_smul, Category.assoc, ι_totalDesc, Linear.comp_units_smul,
      ← Int.negOnePow_add]
    congr 2
    linarith
  · rw [D₁_shape _ _ _ _ h, zero_comp, D₁_shape, comp_zero, smul_zero]
    grind [up_Rel]

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

Goal state before:
pp: case pos
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₀
⊢ (((shiftFunctor₂ C y).obj K).d₂ (up ℤ) p q n₁ ≫
      ((shiftFunctor₂ C y).obj K).totalDesc fun p q hpq ↦ (p * y).negOnePow • K.ιTotal (up ℤ) p (q + y) n₁' ⋯) =
    ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
      (y.negOnePow •
        (((shiftFunctor₂ C y).obj K).totalDesc fun p q hpq ↦ (p * y).negOnePow • K.ιTotal (up ℤ) p (q + y) n₀' ⋯) ≫
          K.D₂ (up ℤ) n₀' n₁')

Tactic:
Linear.comp_units_smul,

Goal state after:
case pos
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₀
⊢ (((shiftFunctor₂ C y).obj K).d₂ (up ℤ) p q n₁ ≫
      ((shiftFunctor₂ C y).obj K).totalDesc fun p q hpq ↦ (p * y).negOnePow • K.ιTotal (up ℤ) p (q + y) n₁' ⋯) =
    y.negOnePow •
      ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) p q n₀ hpq ≫
        (((shiftFunctor₂ C y).obj K).totalDesc fun p q hpq ↦ (p * y).negOnePow • K.ιTotal (up ℤ) p (q + y) n₀' ⋯) ≫
          K.D₂ (up ℤ) n₀' n₁'
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: case pos
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₀
⊢ p.negOnePow •
      y.negOnePow • (K.X p).d (q + y) (q + 1 + y) ≫ ((p * y).negOnePow • K.ιTotal (up ℤ) p (q + 1 + y) n₁' ⋯) =
    (y.negOnePow * (p * y).negOnePow * p.negOnePow) •
      (K.X p).d (q + y) (q + 1 + y) ≫ K.ιTotal (up ℤ) p (q + 1 + y) n₁' ⋯

Tactic:
Linear.comp_units_smul,

Goal state after:
case pos
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₀
⊢ p.negOnePow • y.negOnePow • (p * y).negOnePow • (K.X p).d (q + y) (q + 1 + y) ≫ K.ιTotal (up ℤ) p (q + 1 + y) n₁' ⋯ =
    (y.negOnePow * (p * y).negOnePow * p.negOnePow) •
      (K.X p).d (q + y) (q + 1 + y) ≫ K.ιTotal (up ℤ) p (q + 1 + y) n₁' ⋯
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
      dsimp
      simp only [total_d, Preadditive.add_comp, Preadditive.comp_add, smul_add,
        Linear.comp_units_smul, K.D₁_totalShift₂XIso_hom y n n' _ _ rfl rfl,
        K.D₂_totalShift₂XIso_hom y n n' _ _ rfl rfl]

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 ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ (f.f i₁).f (i₂ + y) ≫ ((i₁ * y).negOnePow • 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:
Linear.comp_units_smul,

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 • K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯) ≫ (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 : HomologicalComplex₂ C (up ℤ) (up ℤ)
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n n₁ n₂ : ℤ
h : n₁ + n₂ = n
⊢ ((shiftFunctor₁ C x).obj ((shiftFunctor₂ C y).obj K)).ιTotal (up ℤ) n₁ n₂ n h ≫
      (((shiftFunctor₂ C y).obj K).totalShift₁Iso x).hom.f n ≫ (K.totalShift₂Iso y).hom.f (n + x) =
    ((shiftFunctor₁ C x).obj ((shiftFunctor₂ C y).obj K)).ιTotal (up ℤ) n₁ n₂ n h ≫
      ((x * y).negOnePow •
        (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:
Linear.comp_units_smul,

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 x).obj ((shiftFunctor₂ C y).obj K)).ιTotal (up ℤ) n₁ n₂ n h ≫
      (((shiftFunctor₂ C y).obj K).totalShift₁Iso x).hom.f n ≫ (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
Module: Mathlib.Algebra.Homology.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
ι : Type u_2
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
x₃ : ↑((forget₂ C Ab).obj (S.X₃.X i))
hx₃ : (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₃.d i j))) x₃ = 0
x₂ : ↑((forget₂ C Ab).obj (S.X₂.X i))
hx₂ : (ConcreteCategory.hom ((forget₂ C Ab).map (S.g.f i))) x₂ = x₃
x₁ : ↑((forget₂ C Ab).obj (S.X₁.X j))
hx₁ :
  (ConcreteCategory.hom ((forget₂ C Ab).map (S.f.f j))) x₁ = (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₂.d i j))) x₂
k : ι
hk : c.next j = k
| (ConcreteCategory.hom ((forget₂ C Ab).map (S.f.f j)))
    ((ConcreteCategory.hom ((forget₂ C Ab).map (S.X₁.iCycles j))) (S.X₁.cyclesMk x₁ k hk ⋯))

Tactic:
HomologicalComplex.i_cyclesMk,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
ι : Type u_2
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
x₃ : ↑((forget₂ C Ab).obj (S.X₃.X i))
hx₃ : (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₃.d i j))) x₃ = 0
x₂ : ↑((forget₂ C Ab).obj (S.X₂.X i))
hx₂ : (ConcreteCategory.hom ((forget₂ C Ab).map (S.g.f i))) x₂ = x₃
x₁ : ↑((forget₂ C Ab).obj (S.X₁.X j))
hx₁ :
  (ConcreteCategory.hom ((forget₂ C Ab).map (S.f.f j))) x₁ = (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₂.d i j))) x₂
k : ι
hk : c.next j = k
| (ConcreteCategory.hom ((forget₂ C Ab).map (S.f.f j))) x₁
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 ≫ (dNext i) h.hom ≫ (L.extendXIso e ⋯).inv = (dNext (e.f i)) (extend.hom e h.hom)

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 i (c.next i)
        · have hi' : c'.Rel (e.f i) (e.f (c.next i)) := by rwa [e.rel_iff]
          simp [dNext_eq _ hi, dNext_eq _ hi', extend.hom_eq _ _ rfl rfl,
            extend_d_eq _ _ rfl rfl]
        · rw [dNext_eq_zero _ _ hi]
          by_cases hi' : c'.Rel (e.f i) (c'.next (e.f i))
          · simp [dNext_eq _ hi', K.extend_d_from_eq_zero _ _ _ _ rfl hi]
          · simp [dNext_eq_zero _ _ hi']

Goal state after:
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)