[GOAL]
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{?u.1349, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x y : β
h : x = y
⊢ (fun b_1 => b_1 + { as := 1 }.as • b) x = (fun b_1 => b_1 + { as := 1 }.as • b) y
[PROOFSTEP]
cases h
[GOAL]
case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{?u.1349, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x : β
⊢ (fun b_1 => b_1 + { as := 1 }.as • b) x = (fun b_1 => b_1 + { as := 1 }.as • b) x
[PROOFSTEP]
rfl
[GOAL]
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{u_3, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x y : β
h : x = y
⊢ objEqToHom X h ≫ d X y =
    d X x ≫ objEqToHom X (_ : (fun b_1 => b_1 + { as := 1 }.as • b) x = (fun b_1 => b_1 + { as := 1 }.as • b) y)
[PROOFSTEP]
cases h
[GOAL]
case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{u_3, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x : β
⊢ objEqToHom X (_ : x = x) ≫ d X x =
    d X x ≫ objEqToHom X (_ : (fun b_1 => b_1 + { as := 1 }.as • b) x = (fun b_1 => b_1 + { as := 1 }.as • b) x)
[PROOFSTEP]
dsimp
[GOAL]
case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{u_3, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x : β
⊢ 𝟙 (obj X x) ≫ d X x = d X x ≫ 𝟙 (obj X (x + 1 • b))
[PROOFSTEP]
simp
[GOAL]
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{u_3, u_2} V
inst✝ : HasZeroMorphisms V
X✝ X Y : DifferentialObject ℤ (GradedObjectWithShift b V)
f : X ⟶ Y
x y : β
h : x = y
⊢ objEqToHom X h ≫ Hom.f f y = Hom.f f x ≫ objEqToHom Y h
[PROOFSTEP]
cases h
[GOAL]
case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{u_3, u_2} V
inst✝ : HasZeroMorphisms V
X✝ X Y : DifferentialObject ℤ (GradedObjectWithShift b V)
f : X ⟶ Y
x : β
⊢ objEqToHom X (_ : x = x) ≫ Hom.f f x = Hom.f f x ≫ objEqToHom Y (_ : x = x)
[PROOFSTEP]
simp
[GOAL]
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{u_3, u_2} V
inst✝ : HasZeroMorphisms V
X : HomologicalComplex V (ComplexShape.up' b)
x y z : β
h : y = z
⊢ d X x y ≫ eqToHom (_ : HomologicalComplex.X X y = HomologicalComplex.X X z) = d X x z
[PROOFSTEP]
cases h
[GOAL]
case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{u_3, u_2} V
inst✝ : HasZeroMorphisms V
X : HomologicalComplex V (ComplexShape.up' b)
x y : β
⊢ d X x y ≫ eqToHom (_ : HomologicalComplex.X X y = HomologicalComplex.X X y) = d X x y
[PROOFSTEP]
simp
[GOAL]
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{?u.42080, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
i j : β
h : i + b = j
⊢ i + 1 • b = j
[PROOFSTEP]
simp [h]
[GOAL]
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{?u.42080, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
i j : β
w : ¬ComplexShape.Rel (ComplexShape.up' b) i j
⊢ (fun i j => if h : i + b = j then DifferentialObject.d X i ≫ objEqToHom X (_ : i + 1 • b = j) else 0) i j = 0
[PROOFSTEP]
dsimp at w 
[GOAL]
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{?u.42080, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
i j : β
w : ¬i + b = j
⊢ (fun i j => if h : i + b = j then DifferentialObject.d X i ≫ objEqToHom X (_ : i + 1 • b = j) else 0) i j = 0
[PROOFSTEP]
convert dif_neg w
[GOAL]
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{?u.42080, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
i j k : β
hij : ComplexShape.Rel (ComplexShape.up' b) i j
hjk : ComplexShape.Rel (ComplexShape.up' b) j k
⊢ (fun i j => if h : i + b = j then DifferentialObject.d X i ≫ objEqToHom X (_ : i + 1 • b = j) else 0) i j ≫
      (fun i j => if h : i + b = j then DifferentialObject.d X i ≫ objEqToHom X (_ : i + 1 • b = j) else 0) j k =
    0
[PROOFSTEP]
dsimp at hij hjk 
[GOAL]
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{?u.42080, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
i j k : β
hij : i + b = j
hjk : j + b = k
⊢ (fun i j => if h : i + b = j then DifferentialObject.d X i ≫ objEqToHom X (_ : i + 1 • b = j) else 0) i j ≫
      (fun i j => if h : i + b = j then DifferentialObject.d X i ≫ objEqToHom X (_ : i + 1 • b = j) else 0) j k =
    0
[PROOFSTEP]
substs hij hjk
[GOAL]
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{?u.42080, u_2} V
inst✝ : HasZeroMorphisms V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
i : β
⊢ (fun i j => if h : i + b = j then DifferentialObject.d X i ≫ objEqToHom X (_ : i + 1 • b = j) else 0) i (i + b) ≫
      (fun i j => if h : i + b = j then DifferentialObject.d X i ≫ objEqToHom X (_ : i + 1 • b = j) else 0) (i + b)
        (i + b + b) =
    0
[PROOFSTEP]
simp
[GOAL]
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{?u.42080, u_2} V
inst✝ : HasZeroMorphisms V
X Y : DifferentialObject ℤ (GradedObjectWithShift b V)
f : X ⟶ Y
i j : β
h : ComplexShape.Rel (ComplexShape.up' b) i j
⊢ DifferentialObject.Hom.f f i ≫
      d
        ((fun X =>
            mk (fun i => obj X i) fun i j =>
              if h : i + b = j then DifferentialObject.d X i ≫ objEqToHom X (_ : i + 1 • b = j) else 0)
          Y)
        i j =
    d
        ((fun X =>
            mk (fun i => obj X i) fun i j =>
              if h : i + b = j then DifferentialObject.d X i ≫ objEqToHom X (_ : i + 1 • b = j) else 0)
          X)
        i j ≫
      DifferentialObject.Hom.f f j
[PROOFSTEP]
dsimp at h ⊢
[GOAL]
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{?u.42080, u_2} V
inst✝ : HasZeroMorphisms V
X Y : DifferentialObject ℤ (GradedObjectWithShift b V)
f : X ⟶ Y
i j : β
h : i + b = j
⊢ (DifferentialObject.Hom.f f i ≫
      if h : i + b = j then DifferentialObject.d Y i ≫ objEqToHom Y (_ : i + 1 • b = j) else 0) =
    (if h : i + b = j then DifferentialObject.d X i ≫ objEqToHom X (_ : i + 1 • b = j) else 0) ≫
      DifferentialObject.Hom.f f j
[PROOFSTEP]
subst h
[GOAL]
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{?u.42080, u_2} V
inst✝ : HasZeroMorphisms V
X Y : DifferentialObject ℤ (GradedObjectWithShift b V)
f : X ⟶ Y
i : β
⊢ (DifferentialObject.Hom.f f i ≫
      if h : i + b = i + b then DifferentialObject.d Y i ≫ objEqToHom Y (_ : i + 1 • b = i + b) else 0) =
    (if h : i + b = i + b then DifferentialObject.d X i ≫ objEqToHom X (_ : i + 1 • b = i + b) else 0) ≫
      DifferentialObject.Hom.f f (i + b)
[PROOFSTEP]
simp only [dite_true, Category.assoc, eqToHom_f']
  -- Porting note: this `rw` used to be part of the `simp`.
[GOAL]
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{?u.42080, u_2} V
inst✝ : HasZeroMorphisms V
X Y : DifferentialObject ℤ (GradedObjectWithShift b V)
f : X ⟶ Y
i : β
⊢ DifferentialObject.Hom.f f i ≫ DifferentialObject.d Y i ≫ objEqToHom Y (_ : i + 1 • b = i + b) =
    DifferentialObject.d X i ≫ DifferentialObject.Hom.f f (i + 1 • b) ≫ objEqToHom Y (_ : i + 1 • b = i + b)
[PROOFSTEP]
have : f.f i ≫ Y.d i = X.d i ≫ f.f _ := (congr_fun f.comm i).symm
[GOAL]
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{?u.42080, u_2} V
inst✝ : HasZeroMorphisms V
X Y : DifferentialObject ℤ (GradedObjectWithShift b V)
f : X ⟶ Y
i : β
this :
  DifferentialObject.Hom.f f i ≫ DifferentialObject.d Y i =
    DifferentialObject.d X i ≫ DifferentialObject.Hom.f f ((fun b_1 => b_1 + { as := 1 }.as • b) i)
⊢ DifferentialObject.Hom.f f i ≫ DifferentialObject.d Y i ≫ objEqToHom Y (_ : i + 1 • b = i + b) =
    DifferentialObject.d X i ≫ DifferentialObject.Hom.f f (i + 1 • b) ≫ objEqToHom Y (_ : i + 1 • b = i + b)
[PROOFSTEP]
rw [reassoc_of% this]
