[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i✝ : ι
f : (i j : ι) → X C i ⟶ X D j
i i' : ι
w : ComplexShape.Rel c i i'
⊢ ↑(dNext i) f = d C i i' ≫ f i' i
[PROOFSTEP]
obtain rfl := c.next_eq' w
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i✝ : ι
f : (i j : ι) → X C i ⟶ X D j
i : ι
w : ComplexShape.Rel c i (ComplexShape.next c i)
⊢ ↑(dNext i) f = d C i (ComplexShape.next c i) ≫ f (ComplexShape.next c i) i
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
f : (i j : ι) → X C i ⟶ X D j
j j' : ι
w : ComplexShape.Rel c j' j
⊢ ↑(prevD j) f = f j j' ≫ d D j' j
[PROOFSTEP]
obtain rfl := c.prev_eq' w
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
f : (i j : ι) → X C i ⟶ X D j
j : ι
w : ComplexShape.Rel c (ComplexShape.prev c j) j
⊢ ↑(prevD j) f = f j (ComplexShape.prev c j) ≫ d D (ComplexShape.prev c j) j
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h k : D ⟶ E
i : ι
f : (i j : ι) → X C i ⟶ X D j
g : D ⟶ E
j : ι
⊢ (↑(prevD j) fun i j => f i j ≫ Hom.f g j) = ↑(prevD j) f ≫ Hom.f g j
[PROOFSTEP]
dsimp [prevD]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h k : D ⟶ E
i : ι
f : (i j : ι) → X C i ⟶ X D j
g : D ⟶ E
j : ι
⊢ (f j (ComplexShape.prev c j) ≫ Hom.f g (ComplexShape.prev c j)) ≫ d E (ComplexShape.prev c j) j =
    (f j (ComplexShape.prev c j) ≫ d D (ComplexShape.prev c j) j) ≫ Hom.f g j
[PROOFSTEP]
simp only [Category.assoc, g.comm]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
f✝ g : C✝ ⟶ D✝
h k : D✝ ⟶ E
i✝ : ι
C D : ChainComplex V ℕ
i : ℕ
f : (i j : ℕ) → X C i ⟶ X D j
⊢ ↑(dNext i) f = d C i (i - 1) ≫ f (i - 1) i
[PROOFSTEP]
dsimp [dNext]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
f✝ g : C✝ ⟶ D✝
h k : D✝ ⟶ E
i✝ : ι
C D : ChainComplex V ℕ
i : ℕ
f : (i j : ℕ) → X C i ⟶ X D j
⊢ d C i (ComplexShape.next (ComplexShape.down ℕ) i) ≫ f (ComplexShape.next (ComplexShape.down ℕ) i) i =
    d C i (i - 1) ≫ f (i - 1) i
[PROOFSTEP]
cases i
[GOAL]
case zero
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
f✝ g : C✝ ⟶ D✝
h k : D✝ ⟶ E
i : ι
C D : ChainComplex V ℕ
f : (i j : ℕ) → X C i ⟶ X D j
⊢ d C Nat.zero (ComplexShape.next (ComplexShape.down ℕ) Nat.zero) ≫
      f (ComplexShape.next (ComplexShape.down ℕ) Nat.zero) Nat.zero =
    d C Nat.zero (Nat.zero - 1) ≫ f (Nat.zero - 1) Nat.zero
[PROOFSTEP]
simp only [shape, ChainComplex.next_nat_zero, ComplexShape.down_Rel, Nat.one_ne_zero, not_false_iff, zero_comp]
[GOAL]
case succ
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
f✝ g : C✝ ⟶ D✝
h k : D✝ ⟶ E
i : ι
C D : ChainComplex V ℕ
f : (i j : ℕ) → X C i ⟶ X D j
n✝ : ℕ
⊢ d C (Nat.succ n✝) (ComplexShape.next (ComplexShape.down ℕ) (Nat.succ n✝)) ≫
      f (ComplexShape.next (ComplexShape.down ℕ) (Nat.succ n✝)) (Nat.succ n✝) =
    d C (Nat.succ n✝) (Nat.succ n✝ - 1) ≫ f (Nat.succ n✝ - 1) (Nat.succ n✝)
[PROOFSTEP]
congr
[GOAL]
case succ.h.e_4.h.e_a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
f✝ g : C✝ ⟶ D✝
h k : D✝ ⟶ E
i : ι
C D : ChainComplex V ℕ
f : (i j : ℕ) → X C i ⟶ X D j
n✝ : ℕ
⊢ ComplexShape.next (ComplexShape.down ℕ) (Nat.succ n✝) = Nat.succ n✝ - 1
[PROOFSTEP]
simp
[GOAL]
case succ.h.e_6.e_8.h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
f✝ g : C✝ ⟶ D✝
h k : D✝ ⟶ E
i : ι
C D : ChainComplex V ℕ
f : (i j : ℕ) → X C i ⟶ X D j
n✝ : ℕ
⊢ ComplexShape.next (ComplexShape.down ℕ) (Nat.succ n✝) = Nat.succ n✝ - 1
[PROOFSTEP]
simp
[GOAL]
case succ.h.e_7.e_1
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
f✝ g : C✝ ⟶ D✝
h k : D✝ ⟶ E
i : ι
C D : ChainComplex V ℕ
f : (i j : ℕ) → X C i ⟶ X D j
n✝ : ℕ
⊢ ComplexShape.next (ComplexShape.down ℕ) (Nat.succ n✝) = Nat.succ n✝ - 1
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
f✝ g : C✝ ⟶ D✝
h k : D✝ ⟶ E
i✝ : ι
C D : CochainComplex V ℕ
i : ℕ
f : (i j : ℕ) → X C i ⟶ X D j
⊢ ↑(prevD i) f = f i (i - 1) ≫ d D (i - 1) i
[PROOFSTEP]
dsimp [prevD]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
f✝ g : C✝ ⟶ D✝
h k : D✝ ⟶ E
i✝ : ι
C D : CochainComplex V ℕ
i : ℕ
f : (i j : ℕ) → X C i ⟶ X D j
⊢ f i (ComplexShape.prev (ComplexShape.up ℕ) i) ≫ d D (ComplexShape.prev (ComplexShape.up ℕ) i) i =
    f i (i - 1) ≫ d D (i - 1) i
[PROOFSTEP]
cases i
[GOAL]
case zero
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
f✝ g : C✝ ⟶ D✝
h k : D✝ ⟶ E
i : ι
C D : CochainComplex V ℕ
f : (i j : ℕ) → X C i ⟶ X D j
⊢ f Nat.zero (ComplexShape.prev (ComplexShape.up ℕ) Nat.zero) ≫
      d D (ComplexShape.prev (ComplexShape.up ℕ) Nat.zero) Nat.zero =
    f Nat.zero (Nat.zero - 1) ≫ d D (Nat.zero - 1) Nat.zero
[PROOFSTEP]
simp only [shape, CochainComplex.prev_nat_zero, ComplexShape.up_Rel, Nat.one_ne_zero, not_false_iff, comp_zero]
[GOAL]
case succ
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
f✝ g : C✝ ⟶ D✝
h k : D✝ ⟶ E
i : ι
C D : CochainComplex V ℕ
f : (i j : ℕ) → X C i ⟶ X D j
n✝ : ℕ
⊢ f (Nat.succ n✝) (ComplexShape.prev (ComplexShape.up ℕ) (Nat.succ n✝)) ≫
      d D (ComplexShape.prev (ComplexShape.up ℕ) (Nat.succ n✝)) (Nat.succ n✝) =
    f (Nat.succ n✝) (Nat.succ n✝ - 1) ≫ d D (Nat.succ n✝ - 1) (Nat.succ n✝)
[PROOFSTEP]
congr
[GOAL]
case succ.h.e_4.h.e_a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
f✝ g : C✝ ⟶ D✝
h k : D✝ ⟶ E
i : ι
C D : CochainComplex V ℕ
f : (i j : ℕ) → X C i ⟶ X D j
n✝ : ℕ
⊢ ComplexShape.prev (ComplexShape.up ℕ) (Nat.succ n✝) = Nat.succ n✝ - 1
[PROOFSTEP]
simp
[GOAL]
case succ.h.e_6.e_2
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
f✝ g : C✝ ⟶ D✝
h k : D✝ ⟶ E
i : ι
C D : CochainComplex V ℕ
f : (i j : ℕ) → X C i ⟶ X D j
n✝ : ℕ
⊢ ComplexShape.prev (ComplexShape.up ℕ) (Nat.succ n✝) = Nat.succ n✝ - 1
[PROOFSTEP]
simp
[GOAL]
case succ.h.e_7.e_7.h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
f✝ g : C✝ ⟶ D✝
h k : D✝ ⟶ E
i : ι
C D : CochainComplex V ℕ
f : (i j : ℕ) → X C i ⟶ X D j
n✝ : ℕ
⊢ ComplexShape.prev (ComplexShape.up ℕ) (Nat.succ n✝) = Nat.succ n✝ - 1
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
h : Homotopy f g
i : ι
⊢ Hom.f (f - g) i = ((↑(dNext i) fun i j => hom h i j) + ↑(prevD i) fun i j => hom h i j) + Hom.f 0 i
[PROOFSTEP]
simp [h.comm]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
h : Homotopy (f - g) 0
i : ι
⊢ Hom.f f i = ((↑(dNext i) fun i j => hom h i j) + ↑(prevD i) fun i j => hom h i j) + Hom.f g i
[PROOFSTEP]
simpa [sub_eq_iff_eq_add] using h.comm i
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
⊢ Function.LeftInverse (fun h => mk fun i j => hom h i j) fun h => mk fun i j => hom h i j
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
⊢ Function.RightInverse (fun h => mk fun i j => hom h i j) fun h => mk fun i j => hom h i j
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
f g : C ⟶ D
h : Homotopy f g
i j : ι
w : ¬ComplexShape.Rel c j i
⊢ (-h.hom) i j = 0
[PROOFSTEP]
rw [Pi.neg_apply, Pi.neg_apply, h.zero i j w, neg_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
f g : C ⟶ D
h : Homotopy f g
i : ι
⊢ Hom.f g i = ↑(dNext i) (-h.hom) + ↑(prevD i) (-h.hom) + Hom.f f i
[PROOFSTEP]
rw [AddMonoidHom.map_neg, AddMonoidHom.map_neg, h.comm, ← neg_add, ← add_assoc, neg_add_self, zero_add]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h✝ k✝ : D ⟶ E
i✝ : ι
e f g : C ⟶ D
h : Homotopy e f
k : Homotopy f g
i j : ι
w : ¬ComplexShape.Rel c j i
⊢ (h.hom + k.hom) i j = 0
[PROOFSTEP]
rw [Pi.add_apply, Pi.add_apply, h.zero i j w, k.zero i j w, zero_add]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h✝ k✝ : D ⟶ E
i✝ : ι
e f g : C ⟶ D
h : Homotopy e f
k : Homotopy f g
i : ι
⊢ Hom.f e i = ↑(dNext i) (h.hom + k.hom) + ↑(prevD i) (h.hom + k.hom) + Hom.f g i
[PROOFSTEP]
rw [AddMonoidHom.map_add, AddMonoidHom.map_add, h.comm, k.comm]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h✝ k✝ : D ⟶ E
i✝ : ι
e f g : C ⟶ D
h : Homotopy e f
k : Homotopy f g
i : ι
⊢ ↑(dNext i) h.hom + ↑(prevD i) h.hom + (↑(dNext i) k.hom + ↑(prevD i) k.hom + Hom.f g i) =
    ↑(dNext i) h.hom + ↑(dNext i) k.hom + (↑(prevD i) h.hom + ↑(prevD i) k.hom) + Hom.f g i
[PROOFSTEP]
abel
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h✝ k✝ : D ⟶ E
i✝ : ι
e f g : C ⟶ D
h : Homotopy e f
k : Homotopy f g
i : ι
⊢ ↑(dNext i) h.hom + ↑(prevD i) h.hom + (↑(dNext i) k.hom + ↑(prevD i) k.hom + Hom.f g i) =
    ↑(dNext i) h.hom + ↑(dNext i) k.hom + (↑(prevD i) h.hom + ↑(prevD i) k.hom) + Hom.f g i
[PROOFSTEP]
abel
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
f₁ g₁ f₂ g₂ : C ⟶ D
h₁ : Homotopy f₁ g₁
h₂ : Homotopy f₂ g₂
i j : ι
hij : ¬ComplexShape.Rel c j i
⊢ (h₁.hom + h₂.hom) i j = 0
[PROOFSTEP]
rw [Pi.add_apply, Pi.add_apply, h₁.zero i j hij, h₂.zero i j hij, add_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
f₁ g₁ f₂ g₂ : C ⟶ D
h₁ : Homotopy f₁ g₁
h₂ : Homotopy f₂ g₂
i : ι
⊢ Hom.f (f₁ + f₂) i = ↑(dNext i) (h₁.hom + h₂.hom) + ↑(prevD i) (h₁.hom + h₂.hom) + Hom.f (g₁ + g₂) i
[PROOFSTEP]
simp only [HomologicalComplex.add_f_apply, h₁.comm, h₂.comm, AddMonoidHom.map_add]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
f₁ g₁ f₂ g₂ : C ⟶ D
h₁ : Homotopy f₁ g₁
h₂ : Homotopy f₂ g₂
i : ι
⊢ ↑(dNext i) h₁.hom + ↑(prevD i) h₁.hom + Hom.f g₁ i + (↑(dNext i) h₂.hom + ↑(prevD i) h₂.hom + Hom.f g₂ i) =
    ↑(dNext i) h₁.hom + ↑(dNext i) h₂.hom + (↑(prevD i) h₁.hom + ↑(prevD i) h₂.hom) + (Hom.f g₁ i + Hom.f g₂ i)
[PROOFSTEP]
abel
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
f₁ g₁ f₂ g₂ : C ⟶ D
h₁ : Homotopy f₁ g₁
h₂ : Homotopy f₂ g₂
i : ι
⊢ ↑(dNext i) h₁.hom + ↑(prevD i) h₁.hom + Hom.f g₁ i + (↑(dNext i) h₂.hom + ↑(prevD i) h₂.hom + Hom.f g₂ i) =
    ↑(dNext i) h₁.hom + ↑(dNext i) h₂.hom + (↑(prevD i) h₁.hom + ↑(prevD i) h₂.hom) + (Hom.f g₁ i + Hom.f g₂ i)
[PROOFSTEP]
abel
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
e f : C ⟶ D
h : Homotopy e f
g : D ⟶ E
i j : ι
w : ¬ComplexShape.Rel c j i
⊢ (fun i j => hom h i j ≫ Hom.f g j) i j = 0
[PROOFSTEP]
dsimp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
e f : C ⟶ D
h : Homotopy e f
g : D ⟶ E
i j : ι
w : ¬ComplexShape.Rel c j i
⊢ hom h i j ≫ Hom.f g j = 0
[PROOFSTEP]
rw [h.zero i j w, zero_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
e f : C ⟶ D
h : Homotopy e f
g : D ⟶ E
i : ι
⊢ Hom.f (e ≫ g) i =
    ((↑(dNext i) fun i j => hom h i j ≫ Hom.f g j) + ↑(prevD i) fun i j => hom h i j ≫ Hom.f g j) + Hom.f (f ≫ g) i
[PROOFSTEP]
rw [comp_f, h.comm i, dNext_comp_right, prevD_comp_right, Preadditive.add_comp, comp_f, Preadditive.add_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
f g : D ⟶ E
h : Homotopy f g
e : C ⟶ D
i j : ι
w : ¬ComplexShape.Rel c j i
⊢ (fun i j => Hom.f e i ≫ hom h i j) i j = 0
[PROOFSTEP]
dsimp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
f g : D ⟶ E
h : Homotopy f g
e : C ⟶ D
i j : ι
w : ¬ComplexShape.Rel c j i
⊢ Hom.f e i ≫ hom h i j = 0
[PROOFSTEP]
rw [h.zero i j w, comp_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
f g : D ⟶ E
h : Homotopy f g
e : C ⟶ D
i : ι
⊢ Hom.f (e ≫ f) i =
    ((↑(dNext i) fun i j => Hom.f e i ≫ hom h i j) + ↑(prevD i) fun i j => Hom.f e i ≫ hom h i j) + Hom.f (e ≫ g) i
[PROOFSTEP]
rw [comp_f, h.comm i, dNext_comp_left, prevD_comp_left, comp_f, Preadditive.comp_add, Preadditive.comp_add]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
hom : (i j : ι) → X C i ⟶ X D j
i j : ι
hij : ComplexShape.Rel c i j
⊢ (fun i => ↑(dNext i) hom + ↑(prevD i) hom) i ≫ d D i j = d C i j ≫ (fun i => ↑(dNext i) hom + ↑(prevD i) hom) j
[PROOFSTEP]
have eq1 : prevD i hom ≫ D.d i j = 0 := by
  simp only [prevD, AddMonoidHom.mk'_apply, Category.assoc, d_comp_d, comp_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
hom : (i j : ι) → X C i ⟶ X D j
i j : ι
hij : ComplexShape.Rel c i j
⊢ ↑(prevD i) hom ≫ d D i j = 0
[PROOFSTEP]
simp only [prevD, AddMonoidHom.mk'_apply, Category.assoc, d_comp_d, comp_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
hom : (i j : ι) → X C i ⟶ X D j
i j : ι
hij : ComplexShape.Rel c i j
eq1 : ↑(prevD i) hom ≫ d D i j = 0
⊢ (fun i => ↑(dNext i) hom + ↑(prevD i) hom) i ≫ d D i j = d C i j ≫ (fun i => ↑(dNext i) hom + ↑(prevD i) hom) j
[PROOFSTEP]
have eq2 : C.d i j ≫ dNext j hom = 0 := by simp only [dNext, AddMonoidHom.mk'_apply, d_comp_d_assoc, zero_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
hom : (i j : ι) → X C i ⟶ X D j
i j : ι
hij : ComplexShape.Rel c i j
eq1 : ↑(prevD i) hom ≫ d D i j = 0
⊢ d C i j ≫ ↑(dNext j) hom = 0
[PROOFSTEP]
simp only [dNext, AddMonoidHom.mk'_apply, d_comp_d_assoc, zero_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
hom : (i j : ι) → X C i ⟶ X D j
i j : ι
hij : ComplexShape.Rel c i j
eq1 : ↑(prevD i) hom ≫ d D i j = 0
eq2 : d C i j ≫ ↑(dNext j) hom = 0
⊢ (fun i => ↑(dNext i) hom + ↑(prevD i) hom) i ≫ d D i j = d C i j ≫ (fun i => ↑(dNext i) hom + ↑(prevD i) hom) j
[PROOFSTEP]
dsimp only
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
hom : (i j : ι) → X C i ⟶ X D j
i j : ι
hij : ComplexShape.Rel c i j
eq1 : ↑(prevD i) hom ≫ d D i j = 0
eq2 : d C i j ≫ ↑(dNext j) hom = 0
⊢ (↑(dNext i) hom + ↑(prevD i) hom) ≫ d D i j = d C i j ≫ (↑(dNext j) hom + ↑(prevD j) hom)
[PROOFSTEP]
rw [dNext_eq hom hij, prevD_eq hom hij, Preadditive.comp_add, Preadditive.add_comp, eq1, eq2, add_zero, zero_add,
  Category.assoc]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g✝ : C ⟶ D
h k : D ⟶ E
i : ι
hom : (i j : ι) → X C i ⟶ X D j
g : D ⟶ E
⊢ nullHomotopicMap hom ≫ g = nullHomotopicMap fun i j => hom i j ≫ Hom.f g j
[PROOFSTEP]
ext n
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g✝ : C ⟶ D
h k : D ⟶ E
i : ι
hom : (i j : ι) → X C i ⟶ X D j
g : D ⟶ E
n : ι
⊢ Hom.f (nullHomotopicMap hom ≫ g) n = Hom.f (nullHomotopicMap fun i j => hom i j ≫ Hom.f g j) n
[PROOFSTEP]
dsimp [nullHomotopicMap, fromNext, toPrev, AddMonoidHom.mk'_apply]
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g✝ : C ⟶ D
h k : D ⟶ E
i : ι
hom : (i j : ι) → X C i ⟶ X D j
g : D ⟶ E
n : ι
⊢ (dFrom C n ≫ hom (ComplexShape.next c n) n + hom n (ComplexShape.prev c n) ≫ dTo D n) ≫ Hom.f g n =
    dFrom C n ≫ hom (ComplexShape.next c n) n ≫ Hom.f g n +
      (hom n (ComplexShape.prev c n) ≫ Hom.f g (ComplexShape.prev c n)) ≫ dTo E n
[PROOFSTEP]
simp only [Preadditive.add_comp, Category.assoc, g.comm]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g✝ : C ⟶ D
h k : D ⟶ E
i : ι
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
g : D ⟶ E
⊢ nullHomotopicMap' hom ≫ g = nullHomotopicMap' fun i j hij => hom i j hij ≫ Hom.f g j
[PROOFSTEP]
ext n
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g✝ : C ⟶ D
h k : D ⟶ E
i : ι
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
g : D ⟶ E
n : ι
⊢ Hom.f (nullHomotopicMap' hom ≫ g) n = Hom.f (nullHomotopicMap' fun i j hij => hom i j hij ≫ Hom.f g j) n
[PROOFSTEP]
erw [nullHomotopicMap_comp]
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g✝ : C ⟶ D
h k : D ⟶ E
i : ι
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
g : D ⟶ E
n : ι
⊢ Hom.f (nullHomotopicMap fun i j => (dite (ComplexShape.Rel c j i) (hom i j) fun x => 0) ≫ Hom.f g j) n =
    Hom.f (nullHomotopicMap' fun i j hij => hom i j hij ≫ Hom.f g j) n
[PROOFSTEP]
congr
[GOAL]
case h.e_self.e_hom
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g✝ : C ⟶ D
h k : D ⟶ E
i : ι
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
g : D ⟶ E
n : ι
⊢ (fun i j => (dite (ComplexShape.Rel c j i) (hom i j) fun x => 0) ≫ Hom.f g j) = fun i j =>
    dite (ComplexShape.Rel c j i) ((fun i j hij => hom i j hij ≫ Hom.f g j) i j) fun x => 0
[PROOFSTEP]
ext i j
[GOAL]
case h.e_self.e_hom.h.h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g✝ : C ⟶ D
h k : D ⟶ E
i✝ : ι
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
g : D ⟶ E
n i j : ι
⊢ (dite (ComplexShape.Rel c j i) (hom i j) fun x => 0) ≫ Hom.f g j =
    dite (ComplexShape.Rel c j i) ((fun i j hij => hom i j hij ≫ Hom.f g j) i j) fun x => 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g✝ : C ⟶ D
h k : D ⟶ E
i✝ : ι
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
g : D ⟶ E
n i j : ι
h✝ : ComplexShape.Rel c j i
⊢ hom i j h✝ ≫ Hom.f g j = (fun i j hij => hom i j hij ≫ Hom.f g j) i j h✝
[PROOFSTEP]
rfl
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g✝ : C ⟶ D
h k : D ⟶ E
i✝ : ι
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
g : D ⟶ E
n i j : ι
h✝ : ¬ComplexShape.Rel c j i
⊢ 0 ≫ Hom.f g j = 0
[PROOFSTEP]
rw [zero_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
f : C ⟶ D
hom : (i j : ι) → X D i ⟶ X E j
⊢ f ≫ nullHomotopicMap hom = nullHomotopicMap fun i j => Hom.f f i ≫ hom i j
[PROOFSTEP]
ext n
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
f : C ⟶ D
hom : (i j : ι) → X D i ⟶ X E j
n : ι
⊢ Hom.f (f ≫ nullHomotopicMap hom) n = Hom.f (nullHomotopicMap fun i j => Hom.f f i ≫ hom i j) n
[PROOFSTEP]
dsimp [nullHomotopicMap, fromNext, toPrev, AddMonoidHom.mk'_apply]
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
f : C ⟶ D
hom : (i j : ι) → X D i ⟶ X E j
n : ι
⊢ Hom.f f n ≫ (dFrom D n ≫ hom (ComplexShape.next c n) n + hom n (ComplexShape.prev c n) ≫ dTo E n) =
    dFrom C n ≫ Hom.f f (ComplexShape.next c n) ≫ hom (ComplexShape.next c n) n +
      (Hom.f f n ≫ hom n (ComplexShape.prev c n)) ≫ dTo E n
[PROOFSTEP]
simp only [Preadditive.comp_add, Category.assoc, f.comm_assoc]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
f : C ⟶ D
hom : (i j : ι) → ComplexShape.Rel c j i → (X D i ⟶ X E j)
⊢ f ≫ nullHomotopicMap' hom = nullHomotopicMap' fun i j hij => Hom.f f i ≫ hom i j hij
[PROOFSTEP]
ext n
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
f : C ⟶ D
hom : (i j : ι) → ComplexShape.Rel c j i → (X D i ⟶ X E j)
n : ι
⊢ Hom.f (f ≫ nullHomotopicMap' hom) n = Hom.f (nullHomotopicMap' fun i j hij => Hom.f f i ≫ hom i j hij) n
[PROOFSTEP]
erw [comp_nullHomotopicMap]
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
f : C ⟶ D
hom : (i j : ι) → ComplexShape.Rel c j i → (X D i ⟶ X E j)
n : ι
⊢ Hom.f (nullHomotopicMap fun i j => Hom.f f i ≫ dite (ComplexShape.Rel c j i) (hom i j) fun x => 0) n =
    Hom.f (nullHomotopicMap' fun i j hij => Hom.f f i ≫ hom i j hij) n
[PROOFSTEP]
congr
[GOAL]
case h.e_self.e_hom
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
f : C ⟶ D
hom : (i j : ι) → ComplexShape.Rel c j i → (X D i ⟶ X E j)
n : ι
⊢ (fun i j => Hom.f f i ≫ dite (ComplexShape.Rel c j i) (hom i j) fun x => 0) = fun i j =>
    dite (ComplexShape.Rel c j i) ((fun i j hij => Hom.f f i ≫ hom i j hij) i j) fun x => 0
[PROOFSTEP]
ext i j
[GOAL]
case h.e_self.e_hom.h.h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i✝ : ι
f : C ⟶ D
hom : (i j : ι) → ComplexShape.Rel c j i → (X D i ⟶ X E j)
n i j : ι
⊢ (Hom.f f i ≫ dite (ComplexShape.Rel c j i) (hom i j) fun x => 0) =
    dite (ComplexShape.Rel c j i) ((fun i j hij => Hom.f f i ≫ hom i j hij) i j) fun x => 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i✝ : ι
f : C ⟶ D
hom : (i j : ι) → ComplexShape.Rel c j i → (X D i ⟶ X E j)
n i j : ι
h✝ : ComplexShape.Rel c j i
⊢ Hom.f f i ≫ hom i j h✝ = (fun i j hij => Hom.f f i ≫ hom i j hij) i j h✝
[PROOFSTEP]
rfl
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i✝ : ι
f : C ⟶ D
hom : (i j : ι) → ComplexShape.Rel c j i → (X D i ⟶ X E j)
n i j : ι
h✝ : ¬ComplexShape.Rel c j i
⊢ Hom.f f i ≫ 0 = 0
[PROOFSTEP]
rw [comp_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
W : Type u_2
inst✝² : Category.{?u.264735, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → X C i ⟶ X D j
i j : ι
⊢ X ((Functor.mapHomologicalComplex G c).obj C) i ⟶ X ((Functor.mapHomologicalComplex G c).obj D) j
[PROOFSTEP]
exact G.map (hom i j)
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → X C i ⟶ X D j
⊢ (Functor.mapHomologicalComplex G c).map (nullHomotopicMap hom) = nullHomotopicMap fun i j => G.map (hom i j)
[PROOFSTEP]
ext i
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → X C i ⟶ X D j
i : ι
⊢ Hom.f ((Functor.mapHomologicalComplex G c).map (nullHomotopicMap hom)) i =
    Hom.f (nullHomotopicMap fun i j => G.map (hom i j)) i
[PROOFSTEP]
dsimp [nullHomotopicMap, dNext, prevD]
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → X C i ⟶ X D j
i : ι
⊢ G.map
      (d C i (ComplexShape.next c i) ≫ hom (ComplexShape.next c i) i +
        hom i (ComplexShape.prev c i) ≫ d D (ComplexShape.prev c i) i) =
    G.map (d C i (ComplexShape.next c i)) ≫ G.map (hom (ComplexShape.next c i) i) +
      G.map (hom i (ComplexShape.prev c i)) ≫ G.map (d D (ComplexShape.prev c i) i)
[PROOFSTEP]
simp only [G.map_comp, Functor.map_add]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
W : Type u_2
inst✝² : Category.{?u.270178, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
i j : ι
hij : ComplexShape.Rel c j i
⊢ X ((Functor.mapHomologicalComplex G c).obj C) i ⟶ X ((Functor.mapHomologicalComplex G c).obj D) j
[PROOFSTEP]
exact G.map (hom i j hij)
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ (Functor.mapHomologicalComplex G c).map (nullHomotopicMap' hom) = nullHomotopicMap' fun i j hij => G.map (hom i j hij)
[PROOFSTEP]
ext n
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
n : ι
⊢ Hom.f ((Functor.mapHomologicalComplex G c).map (nullHomotopicMap' hom)) n =
    Hom.f (nullHomotopicMap' fun i j hij => G.map (hom i j hij)) n
[PROOFSTEP]
erw [map_nullHomotopicMap]
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
n : ι
⊢ Hom.f (nullHomotopicMap fun i j => G.map (dite (ComplexShape.Rel c j i) (hom i j) fun x => 0)) n =
    Hom.f (nullHomotopicMap' fun i j hij => G.map (hom i j hij)) n
[PROOFSTEP]
congr
[GOAL]
case h.e_self.e_hom
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
n : ι
⊢ (fun i j => G.map (dite (ComplexShape.Rel c j i) (hom i j) fun x => 0)) = fun i j =>
    dite (ComplexShape.Rel c j i) ((fun i j hij => G.map (hom i j hij)) i j) fun x => 0
[PROOFSTEP]
ext i j
[GOAL]
case h.e_self.e_hom.h.h
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
n i j : ι
⊢ G.map (dite (ComplexShape.Rel c j i) (hom i j) fun x => 0) =
    dite (ComplexShape.Rel c j i) ((fun i j hij => G.map (hom i j hij)) i j) fun x => 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
n i j : ι
h✝ : ComplexShape.Rel c j i
⊢ G.map (hom i j h✝) = (fun i j hij => G.map (hom i j hij)) i j h✝
[PROOFSTEP]
rfl
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : Functor.Additive G
hom : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
n i j : ι
h✝ : ¬ComplexShape.Rel c j i
⊢ G.map 0 = 0
[PROOFSTEP]
rw [G.map_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
hom : (i j : ι) → X C i ⟶ X D j
zero : ∀ (i j : ι), ¬ComplexShape.Rel c j i → hom i j = 0
⊢ ∀ (i : ι), Hom.f (nullHomotopicMap hom) i = ↑(dNext i) hom + ↑(prevD i) hom + Hom.f 0 i
[PROOFSTEP]
intro i
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
hom : (i j : ι) → X C i ⟶ X D j
zero : ∀ (i j : ι), ¬ComplexShape.Rel c j i → hom i j = 0
i : ι
⊢ Hom.f (nullHomotopicMap hom) i = ↑(dNext i) hom + ↑(prevD i) hom + Hom.f 0 i
[PROOFSTEP]
rw [HomologicalComplex.zero_f_apply, add_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
hom : (i j : ι) → X C i ⟶ X D j
zero : ∀ (i j : ι), ¬ComplexShape.Rel c j i → hom i j = 0
i : ι
⊢ Hom.f (nullHomotopicMap hom) i = ↑(dNext i) hom + ↑(prevD i) hom
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i : ι
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ Homotopy (nullHomotopicMap' h) 0
[PROOFSTEP]
apply nullHomotopy fun i j => dite (c.Rel j i) (h i j) fun _ => 0
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i : ι
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ ∀ (i j : ι), ¬ComplexShape.Rel c j i → (dite (ComplexShape.Rel c j i) (h i j) fun x => 0) = 0
[PROOFSTEP]
intro i j hij
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
i j : ι
hij : ¬ComplexShape.Rel c j i
⊢ (dite (ComplexShape.Rel c j i) (h i j) fun x => 0) = 0
[PROOFSTEP]
rw [dite_eq_right_iff]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
i j : ι
hij : ¬ComplexShape.Rel c j i
⊢ ∀ (h_1 : ComplexShape.Rel c j i), h i j h_1 = 0
[PROOFSTEP]
intro hij'
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
i j : ι
hij : ¬ComplexShape.Rel c j i
hij' : ComplexShape.Rel c j i
⊢ h i j hij' = 0
[PROOFSTEP]
exfalso
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
i j : ι
hij : ¬ComplexShape.Rel c j i
hij' : ComplexShape.Rel c j i
⊢ False
[PROOFSTEP]
exact hij hij'
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i k₂ k₁ k₀ : ι
r₂₁ : ComplexShape.Rel c k₂ k₁
r₁₀ : ComplexShape.Rel c k₁ k₀
hom : (i j : ι) → X C i ⟶ X D j
⊢ Hom.f (nullHomotopicMap hom) k₁ = d C k₁ k₀ ≫ hom k₀ k₁ + hom k₁ k₂ ≫ d D k₂ k₁
[PROOFSTEP]
dsimp only [nullHomotopicMap]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i k₂ k₁ k₀ : ι
r₂₁ : ComplexShape.Rel c k₂ k₁
r₁₀ : ComplexShape.Rel c k₁ k₀
hom : (i j : ι) → X C i ⟶ X D j
⊢ ↑(dNext k₁) hom + ↑(prevD k₁) hom = d C k₁ k₀ ≫ hom k₀ k₁ + hom k₁ k₂ ≫ d D k₂ k₁
[PROOFSTEP]
rw [dNext_eq hom r₁₀, prevD_eq hom r₂₁]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i k₂ k₁ k₀ : ι
r₂₁ : ComplexShape.Rel c k₂ k₁
r₁₀ : ComplexShape.Rel c k₁ k₀
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ Hom.f (nullHomotopicMap' h) k₁ = d C k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ d D k₂ k₁
[PROOFSTEP]
simp only [nullHomotopicMap']
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i k₂ k₁ k₀ : ι
r₂₁ : ComplexShape.Rel c k₂ k₁
r₁₀ : ComplexShape.Rel c k₁ k₀
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ Hom.f (nullHomotopicMap fun i j => dite (ComplexShape.Rel c j i) (h i j) fun x => 0) k₁ =
    d C k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ d D k₂ k₁
[PROOFSTEP]
rw [nullHomotopicMap_f r₂₁ r₁₀]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i k₂ k₁ k₀ : ι
r₂₁ : ComplexShape.Rel c k₂ k₁
r₁₀ : ComplexShape.Rel c k₁ k₀
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ (d C k₁ k₀ ≫ dite (ComplexShape.Rel c k₁ k₀) (h k₀ k₁) fun x => 0) +
      (dite (ComplexShape.Rel c k₂ k₁) (h k₁ k₂) fun x => 0) ≫ d D k₂ k₁ =
    d C k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ d D k₂ k₁
[PROOFSTEP]
split_ifs
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i k₂ k₁ k₀ : ι
r₂₁ : ComplexShape.Rel c k₂ k₁
r₁₀ : ComplexShape.Rel c k₁ k₀
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ d C k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ d D k₂ k₁ = d C k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ d D k₂ k₁
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i k₁ k₀ : ι
r₁₀ : ComplexShape.Rel c k₁ k₀
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
hom : (i j : ι) → X C i ⟶ X D j
⊢ Hom.f (nullHomotopicMap hom) k₀ = hom k₀ k₁ ≫ d D k₁ k₀
[PROOFSTEP]
dsimp only [nullHomotopicMap]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i k₁ k₀ : ι
r₁₀ : ComplexShape.Rel c k₁ k₀
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
hom : (i j : ι) → X C i ⟶ X D j
⊢ ↑(dNext k₀) hom + ↑(prevD k₀) hom = hom k₀ k₁ ≫ d D k₁ k₀
[PROOFSTEP]
rw [prevD_eq hom r₁₀, dNext, AddMonoidHom.mk'_apply, C.shape, zero_comp, zero_add]
[GOAL]
case a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i k₁ k₀ : ι
r₁₀ : ComplexShape.Rel c k₁ k₀
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
hom : (i j : ι) → X C i ⟶ X D j
⊢ ¬ComplexShape.Rel c k₀ (ComplexShape.next c k₀)
[PROOFSTEP]
exact hk₀ _
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i k₁ k₀ : ι
r₁₀ : ComplexShape.Rel c k₁ k₀
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ Hom.f (nullHomotopicMap' h) k₀ = h k₀ k₁ r₁₀ ≫ d D k₁ k₀
[PROOFSTEP]
simp only [nullHomotopicMap']
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i k₁ k₀ : ι
r₁₀ : ComplexShape.Rel c k₁ k₀
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ Hom.f (nullHomotopicMap fun i j => dite (ComplexShape.Rel c j i) (h i j) fun x => 0) k₀ = h k₀ k₁ r₁₀ ≫ d D k₁ k₀
[PROOFSTEP]
rw [nullHomotopicMap_f_of_not_rel_left r₁₀ hk₀]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i k₁ k₀ : ι
r₁₀ : ComplexShape.Rel c k₁ k₀
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ (dite (ComplexShape.Rel c k₁ k₀) (h k₀ k₁) fun x => 0) ≫ d D k₁ k₀ = h k₀ k₁ r₁₀ ≫ d D k₁ k₀
[PROOFSTEP]
split_ifs
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i k₁ k₀ : ι
r₁₀ : ComplexShape.Rel c k₁ k₀
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ h k₀ k₁ r₁₀ ≫ d D k₁ k₀ = h k₀ k₁ r₁₀ ≫ d D k₁ k₀
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i k₁ k₀ : ι
r₁₀ : ComplexShape.Rel c k₁ k₀
hk₁ : ∀ (l : ι), ¬ComplexShape.Rel c l k₁
hom : (i j : ι) → X C i ⟶ X D j
⊢ Hom.f (nullHomotopicMap hom) k₁ = d C k₁ k₀ ≫ hom k₀ k₁
[PROOFSTEP]
dsimp only [nullHomotopicMap]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i k₁ k₀ : ι
r₁₀ : ComplexShape.Rel c k₁ k₀
hk₁ : ∀ (l : ι), ¬ComplexShape.Rel c l k₁
hom : (i j : ι) → X C i ⟶ X D j
⊢ ↑(dNext k₁) hom + ↑(prevD k₁) hom = d C k₁ k₀ ≫ hom k₀ k₁
[PROOFSTEP]
rw [dNext_eq hom r₁₀, prevD, AddMonoidHom.mk'_apply, D.shape, comp_zero, add_zero]
[GOAL]
case a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i k₁ k₀ : ι
r₁₀ : ComplexShape.Rel c k₁ k₀
hk₁ : ∀ (l : ι), ¬ComplexShape.Rel c l k₁
hom : (i j : ι) → X C i ⟶ X D j
⊢ ¬ComplexShape.Rel c (ComplexShape.prev c k₁) k₁
[PROOFSTEP]
exact hk₁ _
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i k₁ k₀ : ι
r₁₀ : ComplexShape.Rel c k₁ k₀
hk₁ : ∀ (l : ι), ¬ComplexShape.Rel c l k₁
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ Hom.f (nullHomotopicMap' h) k₁ = d C k₁ k₀ ≫ h k₀ k₁ r₁₀
[PROOFSTEP]
simp only [nullHomotopicMap']
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i k₁ k₀ : ι
r₁₀ : ComplexShape.Rel c k₁ k₀
hk₁ : ∀ (l : ι), ¬ComplexShape.Rel c l k₁
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ Hom.f (nullHomotopicMap fun i j => dite (ComplexShape.Rel c j i) (h i j) fun x => 0) k₁ = d C k₁ k₀ ≫ h k₀ k₁ r₁₀
[PROOFSTEP]
rw [nullHomotopicMap_f_of_not_rel_right r₁₀ hk₁]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i k₁ k₀ : ι
r₁₀ : ComplexShape.Rel c k₁ k₀
hk₁ : ∀ (l : ι), ¬ComplexShape.Rel c l k₁
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ (d C k₁ k₀ ≫ dite (ComplexShape.Rel c k₁ k₀) (h k₀ k₁) fun x => 0) = d C k₁ k₀ ≫ h k₀ k₁ r₁₀
[PROOFSTEP]
split_ifs
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i k₁ k₀ : ι
r₁₀ : ComplexShape.Rel c k₁ k₀
hk₁ : ∀ (l : ι), ¬ComplexShape.Rel c l k₁
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ d C k₁ k₀ ≫ h k₀ k₁ r₁₀ = d C k₁ k₀ ≫ h k₀ k₁ r₁₀
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i k₀ : ι
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
hk₀' : ∀ (l : ι), ¬ComplexShape.Rel c l k₀
hom : (i j : ι) → X C i ⟶ X D j
⊢ Hom.f (nullHomotopicMap hom) k₀ = 0
[PROOFSTEP]
dsimp [nullHomotopicMap, dNext, prevD]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i k₀ : ι
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
hk₀' : ∀ (l : ι), ¬ComplexShape.Rel c l k₀
hom : (i j : ι) → X C i ⟶ X D j
⊢ d C k₀ (ComplexShape.next c k₀) ≫ hom (ComplexShape.next c k₀) k₀ +
      hom k₀ (ComplexShape.prev c k₀) ≫ d D (ComplexShape.prev c k₀) k₀ =
    0
[PROOFSTEP]
rw [C.shape, D.shape, zero_comp, comp_zero, add_zero]
[GOAL]
case a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i k₀ : ι
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
hk₀' : ∀ (l : ι), ¬ComplexShape.Rel c l k₀
hom : (i j : ι) → X C i ⟶ X D j
⊢ ¬ComplexShape.Rel c (ComplexShape.prev c k₀) k₀
[PROOFSTEP]
apply_assumption
[GOAL]
case a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i k₀ : ι
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
hk₀' : ∀ (l : ι), ¬ComplexShape.Rel c l k₀
hom : (i j : ι) → X C i ⟶ X D j
⊢ ¬ComplexShape.Rel c k₀ (ComplexShape.next c k₀)
[PROOFSTEP]
apply_assumption
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i k₀ : ι
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
hk₀' : ∀ (l : ι), ¬ComplexShape.Rel c l k₀
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ Hom.f (nullHomotopicMap' h) k₀ = 0
[PROOFSTEP]
simp only [nullHomotopicMap']
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i k₀ : ι
hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l
hk₀' : ∀ (l : ι), ¬ComplexShape.Rel c l k₀
h : (i j : ι) → ComplexShape.Rel c j i → (X C i ⟶ X D j)
⊢ Hom.f (nullHomotopicMap fun i j => dite (ComplexShape.Rel c j i) (h i j) fun x => 0) k₀ = 0
[PROOFSTEP]
apply nullHomotopicMap_f_eq_zero hk₀ hk₀'
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
j : ℕ
⊢ ↑(prevD j) f = f j (j + 1) ≫ d Q (j + 1) j
[PROOFSTEP]
dsimp [prevD]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
j : ℕ
⊢ f j (ComplexShape.prev (ComplexShape.down ℕ) j) ≫ d Q (ComplexShape.prev (ComplexShape.down ℕ) j) j =
    f j (j + 1) ≫ d Q (j + 1) j
[PROOFSTEP]
have : (ComplexShape.down ℕ).prev j = j + 1 := ChainComplex.prev ℕ j
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
j : ℕ
this : ComplexShape.prev (ComplexShape.down ℕ) j = j + 1
⊢ f j (ComplexShape.prev (ComplexShape.down ℕ) j) ≫ d Q (ComplexShape.prev (ComplexShape.down ℕ) j) j =
    f j (j + 1) ≫ d Q (j + 1) j
[PROOFSTEP]
congr 2
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : ChainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
i : ℕ
⊢ ↑(dNext (i + 1)) f = d P (i + 1) i ≫ f i (i + 1)
[PROOFSTEP]
dsimp [dNext]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : ChainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
i : ℕ
⊢ d P (i + 1) (ComplexShape.next (ComplexShape.down ℕ) (i + 1)) ≫
      f (ComplexShape.next (ComplexShape.down ℕ) (i + 1)) (i + 1) =
    d P (i + 1) i ≫ f i (i + 1)
[PROOFSTEP]
have : (ComplexShape.down ℕ).next (i + 1) = i := ChainComplex.next_nat_succ _
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : ChainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
i : ℕ
this : ComplexShape.next (ComplexShape.down ℕ) (i + 1) = i
⊢ d P (i + 1) (ComplexShape.next (ComplexShape.down ℕ) (i + 1)) ≫
      f (ComplexShape.next (ComplexShape.down ℕ) (i + 1)) (i + 1) =
    d P (i + 1) i ≫ f i (i + 1)
[PROOFSTEP]
congr 2
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
⊢ ↑(dNext 0) f = 0
[PROOFSTEP]
dsimp [dNext]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
⊢ d P 0 (ComplexShape.next (ComplexShape.down ℕ) 0) ≫ f (ComplexShape.next (ComplexShape.down ℕ) 0) 0 = 0
[PROOFSTEP]
rw [P.shape, zero_comp]
[GOAL]
case a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
⊢ ¬ComplexShape.Rel (ComplexShape.down ℕ) 0 (ComplexShape.next (ComplexShape.down ℕ) 0)
[PROOFSTEP]
rw [ChainComplex.next_nat_zero]
[GOAL]
case a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
⊢ ¬ComplexShape.Rel (ComplexShape.down ℕ) 0 0
[PROOFSTEP]
dsimp
[GOAL]
case a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
⊢ ¬0 + 1 = 0
[PROOFSTEP]
decide
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : X P 0 ⟶ X Q 1
comm_zero : Hom.f e 0 = zero ≫ d Q 1 0
one : X P 1 ⟶ X Q 2
comm_one : Hom.f e 1 = d P 1 0 ≫ zero + one ≫ d Q 2 1
succ :
  (n : ℕ) →
    (p :
        (f : X P n ⟶ X Q (n + 1)) ×'
          (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1)) →
      (f'' : X P (n + 2) ⟶ X Q (n + 3)) ×' Hom.f e (n + 2) = d P (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ d Q (n + 3) (n + 2)
⊢ Hom.f e 0 = dFrom P 0 ≫ 0 + (zero ≫ (xPrevIso Q (_ : 0 + 1 = 0 + 1)).inv) ≫ dTo Q 0
[PROOFSTEP]
simpa using comm_zero
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : X P 0 ⟶ X Q 1
comm_zero : Hom.f e 0 = zero ≫ d Q 1 0
one : X P 1 ⟶ X Q 2
comm_one : Hom.f e 1 = d P 1 0 ≫ zero + one ≫ d Q 2 1
succ :
  (n : ℕ) →
    (p :
        (f : X P n ⟶ X Q (n + 1)) ×'
          (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1)) →
      (f'' : X P (n + 2) ⟶ X Q (n + 3)) ×' Hom.f e (n + 2) = d P (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ d Q (n + 3) (n + 2)
n : ℕ
I : (f : X P n ⟶ X Q (n + 1)) ×'
  (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1) :=
  mkInductiveAux₁ e zero one comm_one succ n
⊢ Hom.f e (n + 1) =
    dFrom P (n + 1) ≫ (xNextIso P (_ : n + 1 = n + 1)).hom ≫ I.fst +
      (I.snd.fst ≫ (xPrevIso Q (_ : n + 1 + 1 = n + 1 + 1)).inv) ≫ dTo Q (n + 1)
[PROOFSTEP]
simpa using I.2.2
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : X P 0 ⟶ X Q 1
comm_zero : Hom.f e 0 = zero ≫ d Q 1 0
one : X P 1 ⟶ X Q 2
comm_one : Hom.f e 1 = d P 1 0 ≫ zero + one ≫ d Q 2 1
succ :
  (n : ℕ) →
    (p :
        (f : X P n ⟶ X Q (n + 1)) ×'
          (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1)) →
      (f'' : X P (n + 2) ⟶ X Q (n + 3)) ×' Hom.f e (n + 2) = d P (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ d Q (n + 3) (n + 2)
i j : ℕ
h : i + 1 = j
⊢ (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (xPrevIso Q h).hom =
    (xNextIso P h).inv ≫ (mkInductiveAux₂ e zero comm_zero one comm_one succ j).fst
[PROOFSTEP]
subst j
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : X P 0 ⟶ X Q 1
comm_zero : Hom.f e 0 = zero ≫ d Q 1 0
one : X P 1 ⟶ X Q 2
comm_one : Hom.f e 1 = d P 1 0 ≫ zero + one ≫ d Q 2 1
succ :
  (n : ℕ) →
    (p :
        (f : X P n ⟶ X Q (n + 1)) ×'
          (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1)) →
      (f'' : X P (n + 2) ⟶ X Q (n + 3)) ×' Hom.f e (n + 2) = d P (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ d Q (n + 3) (n + 2)
i : ℕ
⊢ (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (xPrevIso Q (_ : i + 1 = i + 1)).hom =
    (xNextIso P (_ : i + 1 = i + 1)).inv ≫ (mkInductiveAux₂ e zero comm_zero one comm_one succ (i + 1)).fst
[PROOFSTEP]
rcases i with (_ | _ | i)
[GOAL]
case zero
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : X P 0 ⟶ X Q 1
comm_zero : Hom.f e 0 = zero ≫ d Q 1 0
one : X P 1 ⟶ X Q 2
comm_one : Hom.f e 1 = d P 1 0 ≫ zero + one ≫ d Q 2 1
succ :
  (n : ℕ) →
    (p :
        (f : X P n ⟶ X Q (n + 1)) ×'
          (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1)) →
      (f'' : X P (n + 2) ⟶ X Q (n + 3)) ×' Hom.f e (n + 2) = d P (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ d Q (n + 3) (n + 2)
⊢ (mkInductiveAux₂ e zero comm_zero one comm_one succ Nat.zero).snd.fst ≫
      (xPrevIso Q (_ : Nat.zero + 1 = Nat.zero + 1)).hom =
    (xNextIso P (_ : Nat.zero + 1 = Nat.zero + 1)).inv ≫
      (mkInductiveAux₂ e zero comm_zero one comm_one succ (Nat.zero + 1)).fst
[PROOFSTEP]
simp [mkInductiveAux₂]
[GOAL]
case succ.zero
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : X P 0 ⟶ X Q 1
comm_zero : Hom.f e 0 = zero ≫ d Q 1 0
one : X P 1 ⟶ X Q 2
comm_one : Hom.f e 1 = d P 1 0 ≫ zero + one ≫ d Q 2 1
succ :
  (n : ℕ) →
    (p :
        (f : X P n ⟶ X Q (n + 1)) ×'
          (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1)) →
      (f'' : X P (n + 2) ⟶ X Q (n + 3)) ×' Hom.f e (n + 2) = d P (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ d Q (n + 3) (n + 2)
⊢ (mkInductiveAux₂ e zero comm_zero one comm_one succ (Nat.succ Nat.zero)).snd.fst ≫
      (xPrevIso Q (_ : Nat.succ Nat.zero + 1 = Nat.succ Nat.zero + 1)).hom =
    (xNextIso P (_ : Nat.succ Nat.zero + 1 = Nat.succ Nat.zero + 1)).inv ≫
      (mkInductiveAux₂ e zero comm_zero one comm_one succ (Nat.succ Nat.zero + 1)).fst
[PROOFSTEP]
simp [mkInductiveAux₂]
[GOAL]
case succ.succ
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : X P 0 ⟶ X Q 1
comm_zero : Hom.f e 0 = zero ≫ d Q 1 0
one : X P 1 ⟶ X Q 2
comm_one : Hom.f e 1 = d P 1 0 ≫ zero + one ≫ d Q 2 1
succ :
  (n : ℕ) →
    (p :
        (f : X P n ⟶ X Q (n + 1)) ×'
          (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1)) →
      (f'' : X P (n + 2) ⟶ X Q (n + 3)) ×' Hom.f e (n + 2) = d P (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ d Q (n + 3) (n + 2)
i : ℕ
⊢ (mkInductiveAux₂ e zero comm_zero one comm_one succ (Nat.succ (Nat.succ i))).snd.fst ≫
      (xPrevIso Q (_ : Nat.succ (Nat.succ i) + 1 = Nat.succ (Nat.succ i) + 1)).hom =
    (xNextIso P (_ : Nat.succ (Nat.succ i) + 1 = Nat.succ (Nat.succ i) + 1)).inv ≫
      (mkInductiveAux₂ e zero comm_zero one comm_one succ (Nat.succ (Nat.succ i) + 1)).fst
[PROOFSTEP]
simp [mkInductiveAux₂]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : X P 0 ⟶ X Q 1
comm_zero : Hom.f e 0 = zero ≫ d Q 1 0
one : X P 1 ⟶ X Q 2
comm_one : Hom.f e 1 = d P 1 0 ≫ zero + one ≫ d Q 2 1
succ :
  (n : ℕ) →
    (p :
        (f : X P n ⟶ X Q (n + 1)) ×'
          (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1)) →
      (f'' : X P (n + 2) ⟶ X Q (n + 3)) ×' Hom.f e (n + 2) = d P (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ d Q (n + 3) (n + 2)
i j : ℕ
w : ¬ComplexShape.Rel (ComplexShape.down ℕ) j i
⊢ (fun i j =>
        if h : i + 1 = j then (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (xPrevIso Q h).hom
        else 0)
      i j =
    0
[PROOFSTEP]
dsimp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : X P 0 ⟶ X Q 1
comm_zero : Hom.f e 0 = zero ≫ d Q 1 0
one : X P 1 ⟶ X Q 2
comm_one : Hom.f e 1 = d P 1 0 ≫ zero + one ≫ d Q 2 1
succ :
  (n : ℕ) →
    (p :
        (f : X P n ⟶ X Q (n + 1)) ×'
          (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1)) →
      (f'' : X P (n + 2) ⟶ X Q (n + 3)) ×' Hom.f e (n + 2) = d P (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ d Q (n + 3) (n + 2)
i j : ℕ
w : ¬ComplexShape.Rel (ComplexShape.down ℕ) j i
⊢ (if h : i + 1 = j then (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (xPrevIso Q h).hom else 0) = 0
[PROOFSTEP]
rw [dif_neg]
[GOAL]
case hnc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : X P 0 ⟶ X Q 1
comm_zero : Hom.f e 0 = zero ≫ d Q 1 0
one : X P 1 ⟶ X Q 2
comm_one : Hom.f e 1 = d P 1 0 ≫ zero + one ≫ d Q 2 1
succ :
  (n : ℕ) →
    (p :
        (f : X P n ⟶ X Q (n + 1)) ×'
          (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1)) →
      (f'' : X P (n + 2) ⟶ X Q (n + 3)) ×' Hom.f e (n + 2) = d P (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ d Q (n + 3) (n + 2)
i j : ℕ
w : ¬ComplexShape.Rel (ComplexShape.down ℕ) j i
⊢ ¬i + 1 = j
[PROOFSTEP]
exact w
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : X P 0 ⟶ X Q 1
comm_zero : Hom.f e 0 = zero ≫ d Q 1 0
one : X P 1 ⟶ X Q 2
comm_one : Hom.f e 1 = d P 1 0 ≫ zero + one ≫ d Q 2 1
succ :
  (n : ℕ) →
    (p :
        (f : X P n ⟶ X Q (n + 1)) ×'
          (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1)) →
      (f'' : X P (n + 2) ⟶ X Q (n + 3)) ×' Hom.f e (n + 2) = d P (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ d Q (n + 3) (n + 2)
i : ℕ
⊢ Hom.f e i =
    ((↑(dNext i) fun i j =>
          if h : i + 1 = j then (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (xPrevIso Q h).hom
          else 0) +
        ↑(prevD i) fun i j =>
          if h : i + 1 = j then (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (xPrevIso Q h).hom
          else 0) +
      Hom.f 0 i
[PROOFSTEP]
dsimp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : X P 0 ⟶ X Q 1
comm_zero : Hom.f e 0 = zero ≫ d Q 1 0
one : X P 1 ⟶ X Q 2
comm_one : Hom.f e 1 = d P 1 0 ≫ zero + one ≫ d Q 2 1
succ :
  (n : ℕ) →
    (p :
        (f : X P n ⟶ X Q (n + 1)) ×'
          (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1)) →
      (f'' : X P (n + 2) ⟶ X Q (n + 3)) ×' Hom.f e (n + 2) = d P (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ d Q (n + 3) (n + 2)
i : ℕ
⊢ Hom.f e i =
    (dFrom P i ≫
          ↑(fromNext i) fun i j =>
            if h : i + 1 = j then (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (xPrevIso Q h).hom
            else 0) +
        (↑(toPrev i) fun i j =>
            if h : i + 1 = j then (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (xPrevIso Q h).hom
            else 0) ≫
          dTo Q i +
      0
[PROOFSTEP]
simp only [add_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : X P 0 ⟶ X Q 1
comm_zero : Hom.f e 0 = zero ≫ d Q 1 0
one : X P 1 ⟶ X Q 2
comm_one : Hom.f e 1 = d P 1 0 ≫ zero + one ≫ d Q 2 1
succ :
  (n : ℕ) →
    (p :
        (f : X P n ⟶ X Q (n + 1)) ×'
          (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1)) →
      (f'' : X P (n + 2) ⟶ X Q (n + 3)) ×' Hom.f e (n + 2) = d P (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ d Q (n + 3) (n + 2)
i : ℕ
⊢ Hom.f e i =
    (dFrom P i ≫
        ↑(fromNext i) fun i j =>
          if h : i + 1 = j then (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (xPrevIso Q h).hom
          else 0) +
      (↑(toPrev i) fun i j =>
          if h : i + 1 = j then (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (xPrevIso Q h).hom
          else 0) ≫
        dTo Q i
[PROOFSTEP]
refine' (mkInductiveAux₂ e zero comm_zero one comm_one succ i).2.2.trans _
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : X P 0 ⟶ X Q 1
comm_zero : Hom.f e 0 = zero ≫ d Q 1 0
one : X P 1 ⟶ X Q 2
comm_one : Hom.f e 1 = d P 1 0 ≫ zero + one ≫ d Q 2 1
succ :
  (n : ℕ) →
    (p :
        (f : X P n ⟶ X Q (n + 1)) ×'
          (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1)) →
      (f'' : X P (n + 2) ⟶ X Q (n + 3)) ×' Hom.f e (n + 2) = d P (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ d Q (n + 3) (n + 2)
i : ℕ
⊢ dFrom P i ≫ (mkInductiveAux₂ e zero comm_zero one comm_one succ i).fst +
      (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ dTo Q i =
    (dFrom P i ≫
        ↑(fromNext i) fun i j =>
          if h : i + 1 = j then (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (xPrevIso Q h).hom
          else 0) +
      (↑(toPrev i) fun i j =>
          if h : i + 1 = j then (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (xPrevIso Q h).hom
          else 0) ≫
        dTo Q i
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : X P 0 ⟶ X Q 1
comm_zero : Hom.f e 0 = zero ≫ d Q 1 0
one : X P 1 ⟶ X Q 2
comm_one : Hom.f e 1 = d P 1 0 ≫ zero + one ≫ d Q 2 1
succ :
  (n : ℕ) →
    (p :
        (f : X P n ⟶ X Q (n + 1)) ×'
          (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1)) →
      (f'' : X P (n + 2) ⟶ X Q (n + 3)) ×' Hom.f e (n + 2) = d P (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ d Q (n + 3) (n + 2)
i : ℕ
⊢ (mkInductiveAux₂ e zero comm_zero one comm_one succ i).fst =
    ↑(fromNext i) fun i j =>
      if h : i + 1 = j then (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (xPrevIso Q h).hom else 0
[PROOFSTEP]
cases i
[GOAL]
case e_a.e_a.zero
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : X P 0 ⟶ X Q 1
comm_zero : Hom.f e 0 = zero ≫ d Q 1 0
one : X P 1 ⟶ X Q 2
comm_one : Hom.f e 1 = d P 1 0 ≫ zero + one ≫ d Q 2 1
succ :
  (n : ℕ) →
    (p :
        (f : X P n ⟶ X Q (n + 1)) ×'
          (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1)) →
      (f'' : X P (n + 2) ⟶ X Q (n + 3)) ×' Hom.f e (n + 2) = d P (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ d Q (n + 3) (n + 2)
⊢ (mkInductiveAux₂ e zero comm_zero one comm_one succ Nat.zero).fst =
    ↑(fromNext Nat.zero) fun i j =>
      if h : i + 1 = j then (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (xPrevIso Q h).hom else 0
[PROOFSTEP]
dsimp [fromNext, mkInductiveAux₂]
[GOAL]
case e_a.e_a.zero
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : X P 0 ⟶ X Q 1
comm_zero : Hom.f e 0 = zero ≫ d Q 1 0
one : X P 1 ⟶ X Q 2
comm_one : Hom.f e 1 = d P 1 0 ≫ zero + one ≫ d Q 2 1
succ :
  (n : ℕ) →
    (p :
        (f : X P n ⟶ X Q (n + 1)) ×'
          (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1)) →
      (f'' : X P (n + 2) ⟶ X Q (n + 3)) ×' Hom.f e (n + 2) = d P (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ d Q (n + 3) (n + 2)
⊢ 0 =
    if h : ComplexShape.next (ComplexShape.down ℕ) 0 + 1 = 0 then
      (match ComplexShape.next (ComplexShape.down ℕ) 0 with
            | 0 =>
              { fst := 0,
                snd :=
                  { fst := zero ≫ (xPrevIso Q mkInductiveAux₂.proof_1).inv,
                    snd := (_ : Hom.f e 0 = dFrom P 0 ≫ 0 + (zero ≫ (xPrevIso Q (_ : 0 + 1 = 0 + 1)).inv) ≫ dTo Q 0) } }
            | Nat.succ n =>
              { fst := (xNextIso P (_ : n + 1 = n + 1)).hom ≫ (mkInductiveAux₁ e zero one comm_one succ n).fst,
                snd :=
                  {
                    fst :=
                      (mkInductiveAux₁ e zero one comm_one succ n).snd.fst ≫
                        (xPrevIso Q (_ : n + 1 + 1 = n + 1 + 1)).inv,
                    snd :=
                      (_ :
                        Hom.f e (n + 1) =
                          dFrom P (n + 1) ≫
                              (xNextIso P (_ : n + 1 = n + 1)).hom ≫ (mkInductiveAux₁ e zero one comm_one succ n).fst +
                            ((mkInductiveAux₁ e zero one comm_one succ n).snd.fst ≫
                                (xPrevIso Q (_ : n + 1 + 1 = n + 1 + 1)).inv) ≫
                              dTo Q (n + 1)) } }).snd.fst ≫
        (xPrevIso Q h).hom
    else 0
[PROOFSTEP]
rw [dif_neg]
[GOAL]
case e_a.e_a.zero.hnc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : X P 0 ⟶ X Q 1
comm_zero : Hom.f e 0 = zero ≫ d Q 1 0
one : X P 1 ⟶ X Q 2
comm_one : Hom.f e 1 = d P 1 0 ≫ zero + one ≫ d Q 2 1
succ :
  (n : ℕ) →
    (p :
        (f : X P n ⟶ X Q (n + 1)) ×'
          (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1)) →
      (f'' : X P (n + 2) ⟶ X Q (n + 3)) ×' Hom.f e (n + 2) = d P (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ d Q (n + 3) (n + 2)
⊢ ¬ComplexShape.next (ComplexShape.down ℕ) 0 + 1 = 0
[PROOFSTEP]
simp only
[GOAL]
case e_a.e_a.succ
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : X P 0 ⟶ X Q 1
comm_zero : Hom.f e 0 = zero ≫ d Q 1 0
one : X P 1 ⟶ X Q 2
comm_one : Hom.f e 1 = d P 1 0 ≫ zero + one ≫ d Q 2 1
succ :
  (n : ℕ) →
    (p :
        (f : X P n ⟶ X Q (n + 1)) ×'
          (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1)) →
      (f'' : X P (n + 2) ⟶ X Q (n + 3)) ×' Hom.f e (n + 2) = d P (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ d Q (n + 3) (n + 2)
n✝ : ℕ
⊢ (mkInductiveAux₂ e zero comm_zero one comm_one succ (Nat.succ n✝)).fst =
    ↑(fromNext (Nat.succ n✝)) fun i j =>
      if h : i + 1 = j then (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (xPrevIso Q h).hom else 0
[PROOFSTEP]
dsimp [fromNext]
[GOAL]
case e_a.e_a.succ
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : X P 0 ⟶ X Q 1
comm_zero : Hom.f e 0 = zero ≫ d Q 1 0
one : X P 1 ⟶ X Q 2
comm_one : Hom.f e 1 = d P 1 0 ≫ zero + one ≫ d Q 2 1
succ :
  (n : ℕ) →
    (p :
        (f : X P n ⟶ X Q (n + 1)) ×'
          (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1)) →
      (f'' : X P (n + 2) ⟶ X Q (n + 3)) ×' Hom.f e (n + 2) = d P (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ d Q (n + 3) (n + 2)
n✝ : ℕ
⊢ (xNextIso P (_ : n✝ + 1 = n✝ + 1)).hom ≫ (mkInductiveAux₁ e zero one comm_one succ n✝).fst =
    if h : ComplexShape.next (ComplexShape.down ℕ) (Nat.succ n✝) + 1 = Nat.succ n✝ then
      (mkInductiveAux₂ e zero comm_zero one comm_one succ
              (ComplexShape.next (ComplexShape.down ℕ) (Nat.succ n✝))).snd.fst ≫
        (xPrevIso Q h).hom
    else 0
[PROOFSTEP]
simp only [ChainComplex.next_nat_succ, dite_true]
[GOAL]
case e_a.e_a.succ
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : X P 0 ⟶ X Q 1
comm_zero : Hom.f e 0 = zero ≫ d Q 1 0
one : X P 1 ⟶ X Q 2
comm_one : Hom.f e 1 = d P 1 0 ≫ zero + one ≫ d Q 2 1
succ :
  (n : ℕ) →
    (p :
        (f : X P n ⟶ X Q (n + 1)) ×'
          (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1)) →
      (f'' : X P (n + 2) ⟶ X Q (n + 3)) ×' Hom.f e (n + 2) = d P (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ d Q (n + 3) (n + 2)
n✝ : ℕ
⊢ (xNextIso P (_ : n✝ + 1 = n✝ + 1)).hom ≫ (mkInductiveAux₁ e zero one comm_one succ n✝).fst =
    (mkInductiveAux₂ e zero comm_zero one comm_one succ
            (ComplexShape.next (ComplexShape.down ℕ) (Nat.succ n✝))).snd.fst ≫
      (xPrevIso Q (_ : ComplexShape.next (ComplexShape.down ℕ) (Nat.succ n✝) + 1 = Nat.succ n✝)).hom
[PROOFSTEP]
rw [mkInductiveAux₃ e zero comm_zero one comm_one succ]
[GOAL]
case e_a.e_a.succ
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : X P 0 ⟶ X Q 1
comm_zero : Hom.f e 0 = zero ≫ d Q 1 0
one : X P 1 ⟶ X Q 2
comm_one : Hom.f e 1 = d P 1 0 ≫ zero + one ≫ d Q 2 1
succ :
  (n : ℕ) →
    (p :
        (f : X P n ⟶ X Q (n + 1)) ×'
          (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1)) →
      (f'' : X P (n + 2) ⟶ X Q (n + 3)) ×' Hom.f e (n + 2) = d P (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ d Q (n + 3) (n + 2)
n✝ : ℕ
⊢ (xNextIso P (_ : n✝ + 1 = n✝ + 1)).hom ≫ (mkInductiveAux₁ e zero one comm_one succ n✝).fst =
    (xNextIso P (_ : ComplexShape.next (ComplexShape.down ℕ) (Nat.succ n✝) + 1 = Nat.succ n✝)).inv ≫
      (mkInductiveAux₂ e zero comm_zero one comm_one succ (Nat.succ n✝)).fst
[PROOFSTEP]
dsimp [xNextIso]
[GOAL]
case e_a.e_a.succ
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : X P 0 ⟶ X Q 1
comm_zero : Hom.f e 0 = zero ≫ d Q 1 0
one : X P 1 ⟶ X Q 2
comm_one : Hom.f e 1 = d P 1 0 ≫ zero + one ≫ d Q 2 1
succ :
  (n : ℕ) →
    (p :
        (f : X P n ⟶ X Q (n + 1)) ×'
          (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1)) →
      (f'' : X P (n + 2) ⟶ X Q (n + 3)) ×' Hom.f e (n + 2) = d P (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ d Q (n + 3) (n + 2)
n✝ : ℕ
⊢ eqToHom (_ : xNext P (n✝ + 1) = X P n✝) ≫ (mkInductiveAux₁ e zero one comm_one succ n✝).fst =
    𝟙 (xNext P (Nat.succ n✝)) ≫
      eqToHom (_ : xNext P (n✝ + 1) = X P n✝) ≫ (mkInductiveAux₁ e zero one comm_one succ n✝).fst
[PROOFSTEP]
rw [Category.id_comp]
[GOAL]
case e_a.e_a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : X P 0 ⟶ X Q 1
comm_zero : Hom.f e 0 = zero ≫ d Q 1 0
one : X P 1 ⟶ X Q 2
comm_one : Hom.f e 1 = d P 1 0 ≫ zero + one ≫ d Q 2 1
succ :
  (n : ℕ) →
    (p :
        (f : X P n ⟶ X Q (n + 1)) ×'
          (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1)) →
      (f'' : X P (n + 2) ⟶ X Q (n + 3)) ×' Hom.f e (n + 2) = d P (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ d Q (n + 3) (n + 2)
i : ℕ
⊢ (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst =
    ↑(toPrev i) fun i j =>
      if h : i + 1 = j then (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (xPrevIso Q h).hom else 0
[PROOFSTEP]
dsimp [toPrev]
[GOAL]
case e_a.e_a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : X P 0 ⟶ X Q 1
comm_zero : Hom.f e 0 = zero ≫ d Q 1 0
one : X P 1 ⟶ X Q 2
comm_one : Hom.f e 1 = d P 1 0 ≫ zero + one ≫ d Q 2 1
succ :
  (n : ℕ) →
    (p :
        (f : X P n ⟶ X Q (n + 1)) ×'
          (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1)) →
      (f'' : X P (n + 2) ⟶ X Q (n + 3)) ×' Hom.f e (n + 2) = d P (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ d Q (n + 3) (n + 2)
i : ℕ
⊢ (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst =
    if h : i + 1 = ComplexShape.prev (ComplexShape.down ℕ) i then
      (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (xPrevIso Q h).hom
    else 0
[PROOFSTEP]
erw [dif_pos, Category.comp_id]
[GOAL]
case e_a.e_a.hc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : X P 0 ⟶ X Q 1
comm_zero : Hom.f e 0 = zero ≫ d Q 1 0
one : X P 1 ⟶ X Q 2
comm_one : Hom.f e 1 = d P 1 0 ≫ zero + one ≫ d Q 2 1
succ :
  (n : ℕ) →
    (p :
        (f : X P n ⟶ X Q (n + 1)) ×'
          (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1)) →
      (f'' : X P (n + 2) ⟶ X Q (n + 3)) ×' Hom.f e (n + 2) = d P (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ d Q (n + 3) (n + 2)
i : ℕ
⊢ i + 1 = ComplexShape.prev (ComplexShape.down ℕ) i
case e_a.e_a.hc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : X P 0 ⟶ X Q 1
comm_zero : Hom.f e 0 = zero ≫ d Q 1 0
one : X P 1 ⟶ X Q 2
comm_one : Hom.f e 1 = d P 1 0 ≫ zero + one ≫ d Q 2 1
succ :
  (n : ℕ) →
    (p :
        (f : X P n ⟶ X Q (n + 1)) ×'
          (f' : X P (n + 1) ⟶ X Q (n + 2)) ×' Hom.f e (n + 1) = d P (n + 1) n ≫ f + f' ≫ d Q (n + 2) (n + 1)) →
      (f'' : X P (n + 2) ⟶ X Q (n + 3)) ×' Hom.f e (n + 2) = d P (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ d Q (n + 3) (n + 2)
i : ℕ
⊢ i + 1 = ComplexShape.prev (ComplexShape.down ℕ) i
[PROOFSTEP]
simp only [ChainComplex.prev]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : CochainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
j : ℕ
⊢ ↑(dNext j) f = d P j (j + 1) ≫ f (j + 1) j
[PROOFSTEP]
dsimp [dNext]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : CochainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
j : ℕ
⊢ d P j (ComplexShape.next (ComplexShape.up ℕ) j) ≫ f (ComplexShape.next (ComplexShape.up ℕ) j) j =
    d P j (j + 1) ≫ f (j + 1) j
[PROOFSTEP]
have : (ComplexShape.up ℕ).next j = j + 1 := CochainComplex.next ℕ j
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : CochainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
j : ℕ
this : ComplexShape.next (ComplexShape.up ℕ) j = j + 1
⊢ d P j (ComplexShape.next (ComplexShape.up ℕ) j) ≫ f (ComplexShape.next (ComplexShape.up ℕ) j) j =
    d P j (j + 1) ≫ f (j + 1) j
[PROOFSTEP]
congr 2
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : CochainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
i : ℕ
⊢ ↑(prevD (i + 1)) f = f (i + 1) i ≫ d Q i (i + 1)
[PROOFSTEP]
dsimp [prevD]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : CochainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
i : ℕ
⊢ f (i + 1) (ComplexShape.prev (ComplexShape.up ℕ) (i + 1)) ≫
      d Q (ComplexShape.prev (ComplexShape.up ℕ) (i + 1)) (i + 1) =
    f (i + 1) i ≫ d Q i (i + 1)
[PROOFSTEP]
have : (ComplexShape.up ℕ).prev (i + 1) = i := CochainComplex.prev_nat_succ i
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : CochainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
i : ℕ
this : ComplexShape.prev (ComplexShape.up ℕ) (i + 1) = i
⊢ f (i + 1) (ComplexShape.prev (ComplexShape.up ℕ) (i + 1)) ≫
      d Q (ComplexShape.prev (ComplexShape.up ℕ) (i + 1)) (i + 1) =
    f (i + 1) i ≫ d Q i (i + 1)
[PROOFSTEP]
congr 2
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : CochainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
⊢ ↑(prevD 0) f = 0
[PROOFSTEP]
dsimp [prevD]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : CochainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
⊢ f 0 (ComplexShape.prev (ComplexShape.up ℕ) 0) ≫ d Q (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 = 0
[PROOFSTEP]
rw [Q.shape, comp_zero]
[GOAL]
case a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : CochainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
⊢ ¬ComplexShape.Rel (ComplexShape.up ℕ) (ComplexShape.prev (ComplexShape.up ℕ) 0) 0
[PROOFSTEP]
rw [CochainComplex.prev_nat_zero]
[GOAL]
case a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : CochainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
⊢ ¬ComplexShape.Rel (ComplexShape.up ℕ) 0 0
[PROOFSTEP]
dsimp
[GOAL]
case a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : CochainComplex V ℕ
f : (i j : ℕ) → X P i ⟶ X Q j
⊢ ¬0 + 1 = 0
[PROOFSTEP]
decide
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (n + 2) (n + 3) ≫ f''
⊢ Hom.f e 0 = 0 ≫ dTo Q 0 + dFrom P 0 ≫ (xNextIso P (_ : 0 + 1 = 0 + 1)).hom ≫ zero
[PROOFSTEP]
simpa using comm_zero
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (n + 2) (n + 3) ≫ f''
n : ℕ
I : (f : X P (n + 1) ⟶ X Q n) ×'
  (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f' :=
  mkCoinductiveAux₁ e zero one comm_one succ n
⊢ Hom.f e (n + 1) =
    (I.fst ≫ (xPrevIso Q (_ : n + 1 = n + 1)).inv) ≫ dTo Q (n + 1) +
      dFrom P (n + 1) ≫ (xNextIso P (_ : n + 1 + 1 = n + 1 + 1)).hom ≫ I.snd.fst
[PROOFSTEP]
simpa using I.2.2
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (n + 2) (n + 3) ≫ f''
i j : ℕ
h : i + 1 = j
⊢ (xNextIso P h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst =
    (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).fst ≫ (xPrevIso Q h).hom
[PROOFSTEP]
subst j
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (n + 2) (n + 3) ≫ f''
i : ℕ
⊢ (xNextIso P (_ : i + 1 = i + 1)).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst =
    (mkCoinductiveAux₂ e zero comm_zero one comm_one succ (i + 1)).fst ≫ (xPrevIso Q (_ : i + 1 = i + 1)).hom
[PROOFSTEP]
rcases i with (_ | _ | i)
[GOAL]
case zero
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (n + 2) (n + 3) ≫ f''
⊢ (xNextIso P (_ : Nat.zero + 1 = Nat.zero + 1)).inv ≫
      (mkCoinductiveAux₂ e zero comm_zero one comm_one succ Nat.zero).snd.fst =
    (mkCoinductiveAux₂ e zero comm_zero one comm_one succ (Nat.zero + 1)).fst ≫
      (xPrevIso Q (_ : Nat.zero + 1 = Nat.zero + 1)).hom
[PROOFSTEP]
simp [mkCoinductiveAux₂]
[GOAL]
case succ.zero
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (n + 2) (n + 3) ≫ f''
⊢ (xNextIso P (_ : Nat.succ Nat.zero + 1 = Nat.succ Nat.zero + 1)).inv ≫
      (mkCoinductiveAux₂ e zero comm_zero one comm_one succ (Nat.succ Nat.zero)).snd.fst =
    (mkCoinductiveAux₂ e zero comm_zero one comm_one succ (Nat.succ Nat.zero + 1)).fst ≫
      (xPrevIso Q (_ : Nat.succ Nat.zero + 1 = Nat.succ Nat.zero + 1)).hom
[PROOFSTEP]
simp [mkCoinductiveAux₂]
[GOAL]
case succ.succ
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (n + 2) (n + 3) ≫ f''
i : ℕ
⊢ (xNextIso P (_ : Nat.succ (Nat.succ i) + 1 = Nat.succ (Nat.succ i) + 1)).inv ≫
      (mkCoinductiveAux₂ e zero comm_zero one comm_one succ (Nat.succ (Nat.succ i))).snd.fst =
    (mkCoinductiveAux₂ e zero comm_zero one comm_one succ (Nat.succ (Nat.succ i) + 1)).fst ≫
      (xPrevIso Q (_ : Nat.succ (Nat.succ i) + 1 = Nat.succ (Nat.succ i) + 1)).hom
[PROOFSTEP]
simp [mkCoinductiveAux₂]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (n + 2) (n + 3) ≫ f''
i j : ℕ
w : ¬ComplexShape.Rel (ComplexShape.up ℕ) j i
⊢ (fun i j =>
        if h : j + 1 = i then (xNextIso P h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd.fst
        else 0)
      i j =
    0
[PROOFSTEP]
dsimp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (n + 2) (n + 3) ≫ f''
i j : ℕ
w : ¬ComplexShape.Rel (ComplexShape.up ℕ) j i
⊢ (if h : j + 1 = i then (xNextIso P h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd.fst else 0) =
    0
[PROOFSTEP]
rw [dif_neg]
[GOAL]
case hnc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (n + 2) (n + 3) ≫ f''
i j : ℕ
w : ¬ComplexShape.Rel (ComplexShape.up ℕ) j i
⊢ ¬j + 1 = i
[PROOFSTEP]
exact w
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (n + 2) (n + 3) ≫ f''
i : ℕ
⊢ Hom.f e i =
    ((↑(dNext i) fun i j =>
          if h : j + 1 = i then (xNextIso P h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd.fst
          else 0) +
        ↑(prevD i) fun i j =>
          if h : j + 1 = i then (xNextIso P h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd.fst
          else 0) +
      Hom.f 0 i
[PROOFSTEP]
dsimp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (n + 2) (n + 3) ≫ f''
i : ℕ
⊢ Hom.f e i =
    (dFrom P i ≫
          ↑(fromNext i) fun i j =>
            if h : j + 1 = i then (xNextIso P h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd.fst
            else 0) +
        (↑(toPrev i) fun i j =>
            if h : j + 1 = i then (xNextIso P h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd.fst
            else 0) ≫
          dTo Q i +
      0
[PROOFSTEP]
simp only [add_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (n + 2) (n + 3) ≫ f''
i : ℕ
⊢ Hom.f e i =
    (dFrom P i ≫
        ↑(fromNext i) fun i j =>
          if h : j + 1 = i then (xNextIso P h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd.fst
          else 0) +
      (↑(toPrev i) fun i j =>
          if h : j + 1 = i then (xNextIso P h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd.fst
          else 0) ≫
        dTo Q i
[PROOFSTEP]
rw [add_comm]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (n + 2) (n + 3) ≫ f''
i : ℕ
⊢ Hom.f e i =
    (↑(toPrev i) fun i j =>
          if h : j + 1 = i then (xNextIso P h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd.fst
          else 0) ≫
        dTo Q i +
      dFrom P i ≫
        ↑(fromNext i) fun i j =>
          if h : j + 1 = i then (xNextIso P h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd.fst
          else 0
[PROOFSTEP]
refine' (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).2.2.trans _
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (n + 2) (n + 3) ≫ f''
i : ℕ
⊢ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).fst ≫ dTo Q i +
      dFrom P i ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst =
    (↑(toPrev i) fun i j =>
          if h : j + 1 = i then (xNextIso P h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd.fst
          else 0) ≫
        dTo Q i +
      dFrom P i ≫
        ↑(fromNext i) fun i j =>
          if h : j + 1 = i then (xNextIso P h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd.fst
          else 0
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (n + 2) (n + 3) ≫ f''
i : ℕ
⊢ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).fst =
    ↑(toPrev i) fun i j =>
      if h : j + 1 = i then (xNextIso P h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd.fst else 0
[PROOFSTEP]
cases i
[GOAL]
case e_a.e_a.zero
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (n + 2) (n + 3) ≫ f''
⊢ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ Nat.zero).fst =
    ↑(toPrev Nat.zero) fun i j =>
      if h : j + 1 = i then (xNextIso P h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd.fst else 0
[PROOFSTEP]
dsimp [toPrev, mkCoinductiveAux₂]
[GOAL]
case e_a.e_a.zero
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (n + 2) (n + 3) ≫ f''
⊢ 0 =
    if h : ComplexShape.prev (ComplexShape.up ℕ) 0 + 1 = 0 then
      (xNextIso P h).inv ≫
        (match ComplexShape.prev (ComplexShape.up ℕ) 0 with
            | 0 =>
              { fst := 0,
                snd :=
                  { fst := (xNextIso P mkCoinductiveAux₂.proof_1).hom ≫ zero,
                    snd := (_ : Hom.f e 0 = 0 ≫ dTo Q 0 + dFrom P 0 ≫ (xNextIso P (_ : 0 + 1 = 0 + 1)).hom ≫ zero) } }
            | Nat.succ n =>
              { fst := (mkCoinductiveAux₁ e zero one comm_one succ n).fst ≫ (xPrevIso Q (_ : n + 1 = n + 1)).inv,
                snd :=
                  {
                    fst :=
                      (xNextIso P (_ : n + 1 + 1 = n + 1 + 1)).hom ≫
                        (mkCoinductiveAux₁ e zero one comm_one succ n).snd.fst,
                    snd :=
                      (_ :
                        Hom.f e (n + 1) =
                          ((mkCoinductiveAux₁ e zero one comm_one succ n).fst ≫ (xPrevIso Q (_ : n + 1 = n + 1)).inv) ≫
                              dTo Q (n + 1) +
                            dFrom P (n + 1) ≫
                              (xNextIso P (_ : n + 1 + 1 = n + 1 + 1)).hom ≫
                                (mkCoinductiveAux₁ e zero one comm_one succ n).snd.fst) } }).snd.fst
    else 0
[PROOFSTEP]
rw [dif_neg]
[GOAL]
case e_a.e_a.zero.hnc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (n + 2) (n + 3) ≫ f''
⊢ ¬ComplexShape.prev (ComplexShape.up ℕ) 0 + 1 = 0
[PROOFSTEP]
simp only
[GOAL]
case e_a.e_a.succ
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (n + 2) (n + 3) ≫ f''
n✝ : ℕ
⊢ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ (Nat.succ n✝)).fst =
    ↑(toPrev (Nat.succ n✝)) fun i j =>
      if h : j + 1 = i then (xNextIso P h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd.fst else 0
[PROOFSTEP]
dsimp [toPrev]
[GOAL]
case e_a.e_a.succ
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (n + 2) (n + 3) ≫ f''
n✝ : ℕ
⊢ (mkCoinductiveAux₁ e zero one comm_one succ n✝).fst ≫ (xPrevIso Q (_ : n✝ + 1 = n✝ + 1)).inv =
    if h : ComplexShape.prev (ComplexShape.up ℕ) (Nat.succ n✝) + 1 = Nat.succ n✝ then
      (xNextIso P h).inv ≫
        (mkCoinductiveAux₂ e zero comm_zero one comm_one succ
              (ComplexShape.prev (ComplexShape.up ℕ) (Nat.succ n✝))).snd.fst
    else 0
[PROOFSTEP]
simp only [CochainComplex.prev_nat_succ, dite_true]
[GOAL]
case e_a.e_a.succ
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (n + 2) (n + 3) ≫ f''
n✝ : ℕ
⊢ (mkCoinductiveAux₁ e zero one comm_one succ n✝).fst ≫ (xPrevIso Q (_ : n✝ + 1 = n✝ + 1)).inv =
    (xNextIso P (_ : ComplexShape.prev (ComplexShape.up ℕ) (Nat.succ n✝) + 1 = Nat.succ n✝)).inv ≫
      (mkCoinductiveAux₂ e zero comm_zero one comm_one succ
            (ComplexShape.prev (ComplexShape.up ℕ) (Nat.succ n✝))).snd.fst
[PROOFSTEP]
rw [mkCoinductiveAux₃ e zero comm_zero one comm_one succ]
[GOAL]
case e_a.e_a.succ
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (n + 2) (n + 3) ≫ f''
n✝ : ℕ
⊢ (mkCoinductiveAux₁ e zero one comm_one succ n✝).fst ≫ (xPrevIso Q (_ : n✝ + 1 = n✝ + 1)).inv =
    (mkCoinductiveAux₂ e zero comm_zero one comm_one succ (Nat.succ n✝)).fst ≫
      (xPrevIso Q (_ : ComplexShape.prev (ComplexShape.up ℕ) (Nat.succ n✝) + 1 = Nat.succ n✝)).hom
[PROOFSTEP]
dsimp [xPrevIso]
[GOAL]
case e_a.e_a.succ
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (n + 2) (n + 3) ≫ f''
n✝ : ℕ
⊢ (mkCoinductiveAux₁ e zero one comm_one succ n✝).fst ≫ eqToHom (_ : X Q n✝ = xPrev Q (n✝ + 1)) =
    ((mkCoinductiveAux₁ e zero one comm_one succ n✝).fst ≫ eqToHom (_ : X Q n✝ = xPrev Q (n✝ + 1))) ≫
      𝟙 (xPrev Q (Nat.succ n✝))
[PROOFSTEP]
rw [Category.comp_id]
[GOAL]
case e_a.e_a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (n + 2) (n + 3) ≫ f''
i : ℕ
⊢ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst =
    ↑(fromNext i) fun i j =>
      if h : j + 1 = i then (xNextIso P h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd.fst else 0
[PROOFSTEP]
dsimp [fromNext]
[GOAL]
case e_a.e_a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (n + 2) (n + 3) ≫ f''
i : ℕ
⊢ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst =
    if h : i + 1 = ComplexShape.next (ComplexShape.up ℕ) i then
      (xNextIso P h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst
    else 0
[PROOFSTEP]
erw [dif_pos, Category.id_comp]
[GOAL]
case e_a.e_a.hc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (n + 2) (n + 3) ≫ f''
i : ℕ
⊢ i + 1 = ComplexShape.next (ComplexShape.up ℕ) i
case e_a.e_a.hc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : X P 1 ⟶ X Q 0
comm_zero : Hom.f e 0 = d P 0 1 ≫ zero
one : X P 2 ⟶ X Q 1
comm_one : Hom.f e 1 = zero ≫ d Q 0 1 + d P 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : X P (n + 1) ⟶ X Q n) ×'
          (f' : X P (n + 2) ⟶ X Q (n + 1)) ×' Hom.f e (n + 1) = f ≫ d Q n (n + 1) + d P (n + 1) (n + 2) ≫ f') →
      (f'' : X P (n + 3) ⟶ X Q (n + 2)) ×' Hom.f e (n + 2) = p.snd.fst ≫ d Q (n + 1) (n + 2) + d P (n + 2) (n + 3) ≫ f''
i : ℕ
⊢ i + 1 = ComplexShape.next (ComplexShape.up ℕ) i
[PROOFSTEP]
simp only [CochainComplex.next]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C✝ D E : HomologicalComplex V c
f g : C✝ ⟶ D
h k : D ⟶ E
i : ι
C : HomologicalComplex V c
⊢ 𝟙 C ≫ 𝟙 C = 𝟙 C
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C✝ D E : HomologicalComplex V c
f g : C✝ ⟶ D
h k : D ⟶ E
i : ι
C : HomologicalComplex V c
⊢ 𝟙 C ≫ 𝟙 C = 𝟙 C
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C✝ D✝ E✝ : HomologicalComplex V c
f✝ g✝ : C✝ ⟶ D✝
h k : D✝ ⟶ E✝
i : ι
C D E : HomologicalComplex V c
f : HomotopyEquiv C D
g : HomotopyEquiv D E
⊢ Homotopy ((f.hom ≫ g.hom) ≫ g.inv ≫ f.inv) (𝟙 C)
[PROOFSTEP]
simpa using ((g.homotopyHomInvId.compRightId f.inv).compLeft f.hom).trans f.homotopyHomInvId
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C✝ D✝ E✝ : HomologicalComplex V c
f✝ g✝ : C✝ ⟶ D✝
h k : D✝ ⟶ E✝
i : ι
C D E : HomologicalComplex V c
f : HomotopyEquiv C D
g : HomotopyEquiv D E
⊢ Homotopy ((g.inv ≫ f.inv) ≫ f.hom ≫ g.hom) (𝟙 E)
[PROOFSTEP]
simpa using ((f.homotopyInvHomId.compRightId g.hom).compLeft g.inv).trans g.homotopyInvHomId
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝³ : HasEqualizers V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
h : Homotopy f g
i : ι
⊢ (homologyFunctor V c i).map f = (homologyFunctor V c i).map g
[PROOFSTEP]
dsimp [homologyFunctor]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝³ : HasEqualizers V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
h : Homotopy f g
i : ι
⊢ homology.map (_ : dTo C i ≫ dFrom C i = 0) (_ : dTo D i ≫ dFrom D i = 0) (Hom.sqTo f i) (Hom.sqFrom f i)
      (_ : (Hom.sqTo f i).right = (Hom.sqTo f i).right) =
    homology.map (_ : dTo C i ≫ dFrom C i = 0) (_ : dTo D i ≫ dFrom D i = 0) (Hom.sqTo g i) (Hom.sqFrom g i)
      (_ : (Hom.sqTo g i).right = (Hom.sqTo g i).right)
[PROOFSTEP]
apply eq_of_sub_eq_zero
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝³ : HasEqualizers V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
h : Homotopy f g
i : ι
⊢ homology.map (_ : dTo C i ≫ dFrom C i = 0) (_ : dTo D i ≫ dFrom D i = 0) (Hom.sqTo f i) (Hom.sqFrom f i)
        (_ : (Hom.sqTo f i).right = (Hom.sqTo f i).right) -
      homology.map (_ : dTo C i ≫ dFrom C i = 0) (_ : dTo D i ≫ dFrom D i = 0) (Hom.sqTo g i) (Hom.sqFrom g i)
        (_ : (Hom.sqTo g i).right = (Hom.sqTo g i).right) =
    0
[PROOFSTEP]
ext
[GOAL]
case h.p
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝³ : HasEqualizers V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
h : Homotopy f g
i : ι
⊢ homology.π (dTo C i) (dFrom C i) (_ : dTo C i ≫ dFrom C i = 0) ≫
      (homology.map (_ : dTo C i ≫ dFrom C i = 0) (_ : dTo D i ≫ dFrom D i = 0) (Hom.sqTo f i) (Hom.sqFrom f i)
          (_ : (Hom.sqTo f i).right = (Hom.sqTo f i).right) -
        homology.map (_ : dTo C i ≫ dFrom C i = 0) (_ : dTo D i ≫ dFrom D i = 0) (Hom.sqTo g i) (Hom.sqFrom g i)
          (_ : (Hom.sqTo g i).right = (Hom.sqTo g i).right)) =
    homology.π (dTo C i) (dFrom C i) (_ : dTo C i ≫ dFrom C i = 0) ≫ 0
[PROOFSTEP]
simp only [homology.π_map, comp_zero, Preadditive.comp_sub]
[GOAL]
case h.p
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝³ : HasEqualizers V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
h : Homotopy f g
i : ι
⊢ kernelSubobjectMap (Hom.sqFrom f i) ≫ homology.π (dTo D i) (dFrom D i) (_ : dTo D i ≫ dFrom D i = 0) -
      kernelSubobjectMap (Hom.sqFrom g i) ≫ homology.π (dTo D i) (dFrom D i) (_ : dTo D i ≫ dFrom D i = 0) =
    0
[PROOFSTEP]
dsimp [kernelSubobjectMap]
[GOAL]
case h.p
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝³ : HasEqualizers V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
h : Homotopy f g
i : ι
⊢ Subobject.factorThru (kernelSubobject (dFrom D i)) (Subobject.arrow (kernelSubobject (dFrom C i)) ≫ Hom.f f i)
          (_ :
            Subobject.Factors (kernelSubobject (dFrom D i))
              (Subobject.arrow (kernelSubobject (dFrom C i)) ≫ (Hom.sqFrom f i).left)) ≫
        homology.π (dTo D i) (dFrom D i) (_ : dTo D i ≫ dFrom D i = 0) -
      Subobject.factorThru (kernelSubobject (dFrom D i)) (Subobject.arrow (kernelSubobject (dFrom C i)) ≫ Hom.f g i)
          (_ :
            Subobject.Factors (kernelSubobject (dFrom D i))
              (Subobject.arrow (kernelSubobject (dFrom C i)) ≫ (Hom.sqFrom g i).left)) ≫
        homology.π (dTo D i) (dFrom D i) (_ : dTo D i ≫ dFrom D i = 0) =
    0
[PROOFSTEP]
simp_rw [h.comm i]
[GOAL]
case h.p
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝³ : HasEqualizers V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
h : Homotopy f g
i : ι
⊢ Subobject.factorThru (kernelSubobject (dFrom D i))
          (Subobject.arrow (kernelSubobject (dFrom C i)) ≫ (↑(dNext i) h.hom + ↑(prevD i) h.hom + Hom.f g i))
          (_ :
            Subobject.Factors (kernelSubobject (dFrom D i))
              (Subobject.arrow (kernelSubobject (dFrom C i)) ≫ (↑(dNext i) h.hom + ↑(prevD i) h.hom + Hom.f g i))) ≫
        homology.π (dTo D i) (dFrom D i) (_ : dTo D i ≫ dFrom D i = 0) -
      Subobject.factorThru (kernelSubobject (dFrom D i)) (Subobject.arrow (kernelSubobject (dFrom C i)) ≫ Hom.f g i)
          (_ :
            Subobject.Factors (kernelSubobject (dFrom D i))
              (Subobject.arrow (kernelSubobject (dFrom C i)) ≫ (Hom.sqFrom g i).left)) ≫
        homology.π (dTo D i) (dFrom D i) (_ : dTo D i ≫ dFrom D i = 0) =
    0
[PROOFSTEP]
simp only [zero_add, zero_comp, dNext_eq_dFrom_fromNext, kernelSubobject_arrow_comp_assoc, Preadditive.comp_add]
[GOAL]
case h.p
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝³ : HasEqualizers V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
h : Homotopy f g
i : ι
⊢ Subobject.factorThru (kernelSubobject (dFrom D i))
          (Subobject.arrow (kernelSubobject (dFrom C i)) ≫ ↑(prevD i) h.hom +
            Subobject.arrow (kernelSubobject (dFrom C i)) ≫ Hom.f g i)
          (_ :
            Subobject.Factors (kernelSubobject (dFrom D i))
              (Subobject.arrow (kernelSubobject (dFrom C i)) ≫ ↑(prevD i) h.hom +
                Subobject.arrow (kernelSubobject (dFrom C i)) ≫ Hom.f g i)) ≫
        homology.π (dTo D i) (dFrom D i) (_ : dTo D i ≫ dFrom D i = 0) -
      Subobject.factorThru (kernelSubobject (dFrom D i)) (Subobject.arrow (kernelSubobject (dFrom C i)) ≫ Hom.f g i)
          (_ :
            Subobject.Factors (kernelSubobject (dFrom D i))
              (Subobject.arrow (kernelSubobject (dFrom C i)) ≫ (Hom.sqFrom g i).left)) ≫
        homology.π (dTo D i) (dFrom D i) (_ : dTo D i ≫ dFrom D i = 0) =
    0
[PROOFSTEP]
rw [← Preadditive.sub_comp]
[GOAL]
case h.p
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝³ : HasEqualizers V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
h : Homotopy f g
i : ι
⊢ (Subobject.factorThru (kernelSubobject (dFrom D i))
          (Subobject.arrow (kernelSubobject (dFrom C i)) ≫ ↑(prevD i) h.hom +
            Subobject.arrow (kernelSubobject (dFrom C i)) ≫ Hom.f g i)
          (_ :
            Subobject.Factors (kernelSubobject (dFrom D i))
              (Subobject.arrow (kernelSubobject (dFrom C i)) ≫ ↑(prevD i) h.hom +
                Subobject.arrow (kernelSubobject (dFrom C i)) ≫ Hom.f g i)) -
        Subobject.factorThru (kernelSubobject (dFrom D i)) (Subobject.arrow (kernelSubobject (dFrom C i)) ≫ Hom.f g i)
          (_ :
            Subobject.Factors (kernelSubobject (dFrom D i))
              (Subobject.arrow (kernelSubobject (dFrom C i)) ≫ (Hom.sqFrom g i).left))) ≫
      homology.π (dTo D i) (dFrom D i) (_ : dTo D i ≫ dFrom D i = 0) =
    0
[PROOFSTEP]
simp only [CategoryTheory.Subobject.factorThru_add_sub_factorThru_right]
[GOAL]
case h.p
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝³ : HasEqualizers V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
h : Homotopy f g
i : ι
⊢ Subobject.factorThru (kernelSubobject (dFrom D i)) (Subobject.arrow (kernelSubobject (dFrom C i)) ≫ ↑(prevD i) h.hom)
        (_ :
          Subobject.Factors (kernelSubobject (dFrom D i))
            (Subobject.arrow (kernelSubobject (dFrom C i)) ≫ ↑(prevD i) h.hom)) ≫
      homology.π (dTo D i) (dFrom D i) (_ : dTo D i ≫ dFrom D i = 0) =
    0
[PROOFSTEP]
erw [Subobject.factorThru_ofLE (D.boundaries_le_cycles i)]
[GOAL]
case h.p
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝³ : HasEqualizers V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
h : Homotopy f g
i : ι
⊢ (Subobject.factorThru (boundaries D i) (Subobject.arrow (kernelSubobject (dFrom C i)) ≫ ↑(prevD i) h.hom) ?h.p ≫
        Subobject.ofLE (boundaries D i) (cycles D i) (_ : boundaries D i ≤ cycles D i)) ≫
      homology.π (dTo D i) (dFrom D i) (_ : dTo D i ≫ dFrom D i = 0) =
    0
[PROOFSTEP]
simp
[GOAL]
case h.p
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝³ : HasEqualizers V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
h : Homotopy f g
i : ι
⊢ Subobject.Factors (boundaries D i) (Subobject.arrow (kernelSubobject (dFrom C i)) ≫ ↑(prevD i) h.hom)
[PROOFSTEP]
rw [prevD_eq_toPrev_dTo, ← Category.assoc]
[GOAL]
case h.p
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝³ : HasEqualizers V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
h : Homotopy f g
i : ι
⊢ Subobject.Factors (boundaries D i) ((Subobject.arrow (kernelSubobject (dFrom C i)) ≫ ↑(toPrev i) h.hom) ≫ dTo D i)
[PROOFSTEP]
apply imageSubobject_factors_comp_self
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i✝ : ι
inst✝³ : HasEqualizers V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
f : HomotopyEquiv C D
i : ι
⊢ (homologyFunctor V c i).map f.hom ≫ (homologyFunctor V c i).map f.inv = 𝟙 ((homologyFunctor V c i).obj C)
[PROOFSTEP]
rw [← Functor.map_comp, homology_map_eq_of_homotopy f.homotopyHomInvId, CategoryTheory.Functor.map_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i✝ : ι
inst✝³ : HasEqualizers V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
f : HomotopyEquiv C D
i : ι
⊢ (homologyFunctor V c i).map f.inv ≫ (homologyFunctor V c i).map f.hom = 𝟙 ((homologyFunctor V c i).obj D)
[PROOFSTEP]
rw [← Functor.map_comp, homology_map_eq_of_homotopy f.homotopyInvHomId, CategoryTheory.Functor.map_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
W : Type u_2
inst✝² : Category.{?u.479401, u_2} W
inst✝¹ : Preadditive W
F : V ⥤ W
inst✝ : Additive F
f g : C ⟶ D
h : Homotopy f g
i j : ι
w : ¬ComplexShape.Rel c j i
⊢ (fun i j => F.map (Homotopy.hom h i j)) i j = 0
[PROOFSTEP]
dsimp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
W : Type u_2
inst✝² : Category.{?u.479401, u_2} W
inst✝¹ : Preadditive W
F : V ⥤ W
inst✝ : Additive F
f g : C ⟶ D
h : Homotopy f g
i j : ι
w : ¬ComplexShape.Rel c j i
⊢ F.map (Homotopy.hom h i j) = 0
[PROOFSTEP]
rw [h.zero i j w, F.map_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
W : Type u_2
inst✝² : Category.{?u.479401, u_2} W
inst✝¹ : Preadditive W
F : V ⥤ W
inst✝ : Additive F
f g : C ⟶ D
h : Homotopy f g
i : ι
⊢ Hom.f ((mapHomologicalComplex F c).map f) i =
    ((↑(dNext i) fun i j => F.map (Homotopy.hom h i j)) + ↑(prevD i) fun i j => F.map (Homotopy.hom h i j)) +
      Hom.f ((mapHomologicalComplex F c).map g) i
[PROOFSTEP]
have H := h.comm i
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
W : Type u_2
inst✝² : Category.{?u.479401, u_2} W
inst✝¹ : Preadditive W
F : V ⥤ W
inst✝ : Additive F
f g : C ⟶ D
h : Homotopy f g
i : ι
H : Hom.f f i = ↑(dNext i) h.hom + ↑(prevD i) h.hom + Hom.f g i
⊢ Hom.f ((mapHomologicalComplex F c).map f) i =
    ((↑(dNext i) fun i j => F.map (Homotopy.hom h i j)) + ↑(prevD i) fun i j => F.map (Homotopy.hom h i j)) +
      Hom.f ((mapHomologicalComplex F c).map g) i
[PROOFSTEP]
dsimp [dNext, prevD] at H ⊢
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
W : Type u_2
inst✝² : Category.{?u.479401, u_2} W
inst✝¹ : Preadditive W
F : V ⥤ W
inst✝ : Additive F
f g : C ⟶ D
h : Homotopy f g
i : ι
H :
  Hom.f f i =
    d C i (ComplexShape.next c i) ≫ Homotopy.hom h (ComplexShape.next c i) i +
        Homotopy.hom h i (ComplexShape.prev c i) ≫ d D (ComplexShape.prev c i) i +
      Hom.f g i
⊢ F.map (Hom.f f i) =
    F.map (d C i (ComplexShape.next c i)) ≫ F.map (Homotopy.hom h (ComplexShape.next c i) i) +
        F.map (Homotopy.hom h i (ComplexShape.prev c i)) ≫ F.map (d D (ComplexShape.prev c i) i) +
      F.map (Hom.f g i)
[PROOFSTEP]
simp [H]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i : ι
W : Type u_2
inst✝² : Category.{?u.486182, u_2} W
inst✝¹ : Preadditive W
F : V ⥤ W
inst✝ : Additive F
h : HomotopyEquiv C D
⊢ Homotopy ((mapHomologicalComplex F c).map h.hom ≫ (mapHomologicalComplex F c).map h.inv)
    (𝟙 ((mapHomologicalComplex F c).obj C))
[PROOFSTEP]
rw [← (F.mapHomologicalComplex c).map_comp, ← (F.mapHomologicalComplex c).map_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i : ι
W : Type u_2
inst✝² : Category.{?u.486182, u_2} W
inst✝¹ : Preadditive W
F : V ⥤ W
inst✝ : Additive F
h : HomotopyEquiv C D
⊢ Homotopy ((mapHomologicalComplex F c).map (h.hom ≫ h.inv)) ((mapHomologicalComplex F c).map (𝟙 C))
[PROOFSTEP]
exact F.mapHomotopy h.homotopyHomInvId
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i : ι
W : Type u_2
inst✝² : Category.{?u.486182, u_2} W
inst✝¹ : Preadditive W
F : V ⥤ W
inst✝ : Additive F
h : HomotopyEquiv C D
⊢ Homotopy ((mapHomologicalComplex F c).map h.inv ≫ (mapHomologicalComplex F c).map h.hom)
    (𝟙 ((mapHomologicalComplex F c).obj D))
[PROOFSTEP]
rw [← (F.mapHomologicalComplex c).map_comp, ← (F.mapHomologicalComplex c).map_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i : ι
W : Type u_2
inst✝² : Category.{?u.486182, u_2} W
inst✝¹ : Preadditive W
F : V ⥤ W
inst✝ : Additive F
h : HomotopyEquiv C D
⊢ Homotopy ((mapHomologicalComplex F c).map (h.inv ≫ h.hom)) ((mapHomologicalComplex F c).map (𝟙 D))
[PROOFSTEP]
exact F.mapHomotopy h.homotopyInvHomId
