[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
⊢ d C i j ≫ d C j k = 0
[PROOFSTEP]
by_cases hij : c.Rel i j
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
hij : ComplexShape.Rel c i j
⊢ d C i j ≫ d C j k = 0
[PROOFSTEP]
by_cases hjk : c.Rel j k
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
hij : ComplexShape.Rel c i j
hjk : ComplexShape.Rel c j k
⊢ d C i j ≫ d C j k = 0
[PROOFSTEP]
exact C.d_comp_d' i j k hij hjk
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
hij : ComplexShape.Rel c i j
hjk : ¬ComplexShape.Rel c j k
⊢ d C i j ≫ d C j k = 0
[PROOFSTEP]
rw [C.shape j k hjk, comp_zero]
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
hij : ¬ComplexShape.Rel c i j
⊢ d C i j ≫ d C j k = 0
[PROOFSTEP]
rw [C.shape i j hij, zero_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C₁ C₂ : HomologicalComplex V c
h_X : C₁.X = C₂.X
h_d :
  ∀ (i j : ι),
    ComplexShape.Rel c i j → d C₁ i j ≫ eqToHom (_ : X C₁ j = X C₂ j) = eqToHom (_ : X C₁ i = X C₂ i) ≫ d C₂ i j
⊢ C₁ = C₂
[PROOFSTEP]
obtain ⟨X₁, d₁, s₁, h₁⟩ := C₁
[GOAL]
case mk
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C₂ : HomologicalComplex V c
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬ComplexShape.Rel c i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → d₁ i j ≫ d₁ j k = 0
h_X : (mk X₁ d₁).X = C₂.X
h_d :
  ∀ (i j : ι),
    ComplexShape.Rel c i j →
      d (mk X₁ d₁) i j ≫ eqToHom (_ : X (mk X₁ d₁) j = X C₂ j) = eqToHom (_ : X (mk X₁ d₁) i = X C₂ i) ≫ d C₂ i j
⊢ mk X₁ d₁ = C₂
[PROOFSTEP]
obtain ⟨X₂, d₂, s₂, h₂⟩ := C₂
[GOAL]
case mk.mk
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬ComplexShape.Rel c i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → d₁ i j ≫ d₁ j k = 0
X₂ : ι → V
d₂ : (i j : ι) → X₂ i ⟶ X₂ j
s₂ : ∀ (i j : ι), ¬ComplexShape.Rel c i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → d₂ i j ≫ d₂ j k = 0
h_X : (mk X₁ d₁).X = (mk X₂ d₂).X
h_d :
  ∀ (i j : ι),
    ComplexShape.Rel c i j →
      d (mk X₁ d₁) i j ≫ eqToHom (_ : X (mk X₁ d₁) j = X (mk X₂ d₂) j) =
        eqToHom (_ : X (mk X₁ d₁) i = X (mk X₂ d₂) i) ≫ d (mk X₂ d₂) i j
⊢ mk X₁ d₁ = mk X₂ d₂
[PROOFSTEP]
dsimp at h_X 
[GOAL]
case mk.mk
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬ComplexShape.Rel c i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → d₁ i j ≫ d₁ j k = 0
X₂ : ι → V
d₂ : (i j : ι) → X₂ i ⟶ X₂ j
s₂ : ∀ (i j : ι), ¬ComplexShape.Rel c i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → d₂ i j ≫ d₂ j k = 0
h_X : X₁ = X₂
h_d :
  ∀ (i j : ι),
    ComplexShape.Rel c i j →
      d (mk X₁ d₁) i j ≫ eqToHom (_ : X (mk X₁ d₁) j = X (mk X₂ d₂) j) =
        eqToHom (_ : X (mk X₁ d₁) i = X (mk X₂ d₂) i) ≫ d (mk X₂ d₂) i j
⊢ mk X₁ d₁ = mk X₂ d₂
[PROOFSTEP]
subst h_X
[GOAL]
case mk.mk
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬ComplexShape.Rel c i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → d₁ i j ≫ d₁ j k = 0
d₂ : (i j : ι) → X₁ i ⟶ X₁ j
s₂ : ∀ (i j : ι), ¬ComplexShape.Rel c i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → d₂ i j ≫ d₂ j k = 0
h_d :
  ∀ (i j : ι),
    ComplexShape.Rel c i j →
      d (mk X₁ d₁) i j ≫ eqToHom (_ : X (mk X₁ d₁) j = X (mk X₁ d₂) j) =
        eqToHom (_ : X (mk X₁ d₁) i = X (mk X₁ d₂) i) ≫ d (mk X₁ d₂) i j
⊢ mk X₁ d₁ = mk X₁ d₂
[PROOFSTEP]
simp only [mk.injEq, heq_eq_eq, true_and]
[GOAL]
case mk.mk
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬ComplexShape.Rel c i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → d₁ i j ≫ d₁ j k = 0
d₂ : (i j : ι) → X₁ i ⟶ X₁ j
s₂ : ∀ (i j : ι), ¬ComplexShape.Rel c i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → d₂ i j ≫ d₂ j k = 0
h_d :
  ∀ (i j : ι),
    ComplexShape.Rel c i j →
      d (mk X₁ d₁) i j ≫ eqToHom (_ : X (mk X₁ d₁) j = X (mk X₁ d₂) j) =
        eqToHom (_ : X (mk X₁ d₁) i = X (mk X₁ d₂) i) ≫ d (mk X₁ d₂) i j
⊢ d₁ = d₂
[PROOFSTEP]
ext i j
[GOAL]
case mk.mk.h.h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬ComplexShape.Rel c i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → d₁ i j ≫ d₁ j k = 0
d₂ : (i j : ι) → X₁ i ⟶ X₁ j
s₂ : ∀ (i j : ι), ¬ComplexShape.Rel c i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → d₂ i j ≫ d₂ j k = 0
h_d :
  ∀ (i j : ι),
    ComplexShape.Rel c i j →
      d (mk X₁ d₁) i j ≫ eqToHom (_ : X (mk X₁ d₁) j = X (mk X₁ d₂) j) =
        eqToHom (_ : X (mk X₁ d₁) i = X (mk X₁ d₂) i) ≫ d (mk X₁ d₂) i j
i j : ι
⊢ d₁ i j = d₂ i j
[PROOFSTEP]
by_cases hij : c.Rel i j
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬ComplexShape.Rel c i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → d₁ i j ≫ d₁ j k = 0
d₂ : (i j : ι) → X₁ i ⟶ X₁ j
s₂ : ∀ (i j : ι), ¬ComplexShape.Rel c i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → d₂ i j ≫ d₂ j k = 0
h_d :
  ∀ (i j : ι),
    ComplexShape.Rel c i j →
      d (mk X₁ d₁) i j ≫ eqToHom (_ : X (mk X₁ d₁) j = X (mk X₁ d₂) j) =
        eqToHom (_ : X (mk X₁ d₁) i = X (mk X₁ d₂) i) ≫ d (mk X₁ d₂) i j
i j : ι
hij : ComplexShape.Rel c i j
⊢ d₁ i j = d₂ i j
[PROOFSTEP]
simpa only [comp_id, id_comp, eqToHom_refl] using h_d i j hij
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬ComplexShape.Rel c i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → d₁ i j ≫ d₁ j k = 0
d₂ : (i j : ι) → X₁ i ⟶ X₁ j
s₂ : ∀ (i j : ι), ¬ComplexShape.Rel c i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → d₂ i j ≫ d₂ j k = 0
h_d :
  ∀ (i j : ι),
    ComplexShape.Rel c i j →
      d (mk X₁ d₁) i j ≫ eqToHom (_ : X (mk X₁ d₁) j = X (mk X₁ d₂) j) =
        eqToHom (_ : X (mk X₁ d₁) i = X (mk X₁ d₂) i) ≫ d (mk X₁ d₂) i j
i j : ι
hij : ¬ComplexShape.Rel c i j
⊢ d₁ i j = d₂ i j
[PROOFSTEP]
rw [s₁ i j hij, s₂ i j hij]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p q : ι
h : p = q
⊢ X K p = X K q
[PROOFSTEP]
rw [h]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ p₃ : ι
h₁₂ : p₁ = p₂
h₂₃ : p₂ = p₃
⊢ (XIsoOfEq K h₁₂).hom ≫ (XIsoOfEq K h₂₃).hom = (XIsoOfEq K (_ : p₁ = p₃)).hom
[PROOFSTEP]
dsimp [XIsoOfEq]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ p₃ : ι
h₁₂ : p₁ = p₂
h₂₃ : p₂ = p₃
⊢ eqToHom (_ : X K p₁ = X K p₂) ≫ eqToHom (_ : X K p₂ = X K p₃) = eqToHom (_ : X K p₁ = X K p₃)
[PROOFSTEP]
simp only [eqToHom_trans]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ p₃ : ι
h₁₂ : p₁ = p₂
h₃₂ : p₃ = p₂
⊢ (XIsoOfEq K h₁₂).hom ≫ (XIsoOfEq K h₃₂).inv = (XIsoOfEq K (_ : p₁ = p₃)).hom
[PROOFSTEP]
dsimp [XIsoOfEq]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ p₃ : ι
h₁₂ : p₁ = p₂
h₃₂ : p₃ = p₂
⊢ eqToHom (_ : X K p₁ = X K p₂) ≫ eqToHom (_ : X K p₂ = X K p₃) = eqToHom (_ : X K p₁ = X K p₃)
[PROOFSTEP]
simp only [eqToHom_trans]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ p₃ : ι
h₂₁ : p₂ = p₁
h₂₃ : p₂ = p₃
⊢ (XIsoOfEq K h₂₁).inv ≫ (XIsoOfEq K h₂₃).hom = (XIsoOfEq K (_ : p₁ = p₃)).hom
[PROOFSTEP]
dsimp [XIsoOfEq]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ p₃ : ι
h₂₁ : p₂ = p₁
h₂₃ : p₂ = p₃
⊢ eqToHom (_ : X K p₁ = X K p₂) ≫ eqToHom (_ : X K p₂ = X K p₃) = eqToHom (_ : X K p₁ = X K p₃)
[PROOFSTEP]
simp only [eqToHom_trans]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ p₃ : ι
h₂₁ : p₂ = p₁
h₃₂ : p₃ = p₂
⊢ (XIsoOfEq K h₂₁).inv ≫ (XIsoOfEq K h₃₂).inv = (XIsoOfEq K (_ : p₁ = p₃)).hom
[PROOFSTEP]
dsimp [XIsoOfEq]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ p₃ : ι
h₂₁ : p₂ = p₁
h₃₂ : p₃ = p₂
⊢ eqToHom (_ : X K p₁ = X K p₂) ≫ eqToHom (_ : X K p₂ = X K p₃) = eqToHom (_ : X K p₁ = X K p₃)
[PROOFSTEP]
simp only [eqToHom_trans]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ : ι
h : p₁ = p₂
p₃ : ι
⊢ (XIsoOfEq K h).hom ≫ d K p₂ p₃ = d K p₁ p₃
[PROOFSTEP]
subst h
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₃ : ι
⊢ (XIsoOfEq K (_ : p₁ = p₁)).hom ≫ d K p₁ p₃ = d K p₁ p₃
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₂ p₁ : ι
h : p₂ = p₁
p₃ : ι
⊢ (XIsoOfEq K h).inv ≫ d K p₂ p₃ = d K p₁ p₃
[PROOFSTEP]
subst h
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₂ p₃ : ι
⊢ (XIsoOfEq K (_ : p₂ = p₂)).inv ≫ d K p₂ p₃ = d K p₂ p₃
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₂ p₃ : ι
h : p₂ = p₃
p₁ : ι
⊢ d K p₁ p₂ ≫ (XIsoOfEq K h).hom = d K p₁ p₃
[PROOFSTEP]
subst h
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₂ p₁ : ι
⊢ d K p₁ p₂ ≫ (XIsoOfEq K (_ : p₂ = p₂)).hom = d K p₁ p₂
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₂ p₃ : ι
h : p₃ = p₂
p₁ : ι
⊢ d K p₁ p₂ ≫ (XIsoOfEq K h).inv = d K p₁ p₃
[PROOFSTEP]
subst h
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₃ p₁ : ι
⊢ d K p₁ p₃ ≫ (XIsoOfEq K (_ : p₃ = p₃)).inv = d K p₁ p₃
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
⊢ ComplexShape.next (ComplexShape.down ℕ) 0 = 0
[PROOFSTEP]
classical
refine' dif_neg _
push_neg
intro
apply Nat.noConfusion
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
⊢ ComplexShape.next (ComplexShape.down ℕ) 0 = 0
[PROOFSTEP]
refine' dif_neg _
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
⊢ ¬∃ j, ComplexShape.Rel (ComplexShape.down ℕ) 0 j
[PROOFSTEP]
push_neg
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
⊢ ∀ (j : ℕ), ¬ComplexShape.Rel (ComplexShape.down ℕ) 0 j
[PROOFSTEP]
intro
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
j✝ : ℕ
⊢ ¬ComplexShape.Rel (ComplexShape.down ℕ) 0 j✝
[PROOFSTEP]
apply Nat.noConfusion
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
⊢ ComplexShape.prev (ComplexShape.up ℕ) 0 = 0
[PROOFSTEP]
classical
refine' dif_neg _
push_neg
intro
apply Nat.noConfusion
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
⊢ ComplexShape.prev (ComplexShape.up ℕ) 0 = 0
[PROOFSTEP]
refine' dif_neg _
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
⊢ ¬∃ i, ComplexShape.Rel (ComplexShape.up ℕ) i 0
[PROOFSTEP]
push_neg
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
⊢ ∀ (i : ℕ), ¬ComplexShape.Rel (ComplexShape.up ℕ) i 0
[PROOFSTEP]
intro
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
i✝ : ℕ
⊢ ¬ComplexShape.Rel (ComplexShape.up ℕ) i✝ 0
[PROOFSTEP]
apply Nat.noConfusion
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C A B : HomologicalComplex V c
f : Hom A B
i j : ι
⊢ HomologicalComplex.Hom.f f i ≫ d B i j = d A i j ≫ HomologicalComplex.Hom.f f j
[PROOFSTEP]
by_cases hij : c.Rel i j
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C A B : HomologicalComplex V c
f : Hom A B
i j : ι
hij : ComplexShape.Rel c i j
⊢ HomologicalComplex.Hom.f f i ≫ d B i j = d A i j ≫ HomologicalComplex.Hom.f f j
[PROOFSTEP]
exact f.comm' i j hij
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C A B : HomologicalComplex V c
f : Hom A B
i j : ι
hij : ¬ComplexShape.Rel c i j
⊢ HomologicalComplex.Hom.f f i ≫ d B i j = d A i j ≫ HomologicalComplex.Hom.f f j
[PROOFSTEP]
rw [A.shape i j hij, B.shape i j hij, comp_zero, zero_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C✝ C D : HomologicalComplex V c
f g : C ⟶ D
h : ∀ (i : ι), Hom.f f i = Hom.f g i
⊢ f = g
[PROOFSTEP]
apply Hom.ext
[GOAL]
case f
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C✝ C D : HomologicalComplex V c
f g : C ⟶ D
h : ∀ (i : ι), Hom.f f i = Hom.f g i
⊢ f.f = g.f
[PROOFSTEP]
funext
[GOAL]
case f.h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C✝ C D : HomologicalComplex V c
f g : C ⟶ D
h : ∀ (i : ι), Hom.f f i = Hom.f g i
x✝ : ι
⊢ Hom.f f x✝ = Hom.f g x✝
[PROOFSTEP]
apply h
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ : HomologicalComplex V c
h : C₁ = C₂
n : ι
⊢ Hom.f (eqToHom h) n = eqToHom (_ : X C₁ n = X C₂ n)
[PROOFSTEP]
subst h
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ : HomologicalComplex V c
n : ι
⊢ Hom.f (eqToHom (_ : C₁ = C₁)) n = eqToHom (_ : X C₁ n = X C₁ n)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ : HomologicalComplex V c
⊢ Function.Injective fun f => f.f
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasZeroObject V
⊢ IsZero zero
[PROOFSTEP]
refine' ⟨fun X => ⟨⟨⟨0⟩, fun f => _⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => _⟩⟩⟩
[GOAL]
case refine'_1
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : zero ⟶ X
⊢ f = default
case refine'_2
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : X ⟶ zero
⊢ f = default
[PROOFSTEP]
all_goals
  ext
  dsimp [zero]
  apply Subsingleton.elim
[GOAL]
case refine'_1
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : zero ⟶ X
⊢ f = default
[PROOFSTEP]
ext
[GOAL]
case refine'_1.h
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : zero ⟶ X
i✝ : ι
⊢ Hom.f f i✝ = Hom.f default i✝
[PROOFSTEP]
dsimp [zero]
[GOAL]
case refine'_1.h
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : zero ⟶ X
i✝ : ι
⊢ Hom.f f i✝ = 0
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
case refine'_2
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : X ⟶ zero
⊢ f = default
[PROOFSTEP]
ext
[GOAL]
case refine'_2.h
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : X ⟶ zero
i✝ : ι
⊢ Hom.f f i✝ = Hom.f default i✝
[PROOFSTEP]
dsimp [zero]
[GOAL]
case refine'_2.h
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : X ⟶ zero
i✝ : ι
⊢ Hom.f f i✝ = 0
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j j' : ι
rij : ComplexShape.Rel c i j
rij' : ComplexShape.Rel c i j'
⊢ d C i j' ≫ eqToHom (_ : X C j' = X C j) = d C i j
[PROOFSTEP]
obtain rfl := c.next_eq rij rij'
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
rij rij' : ComplexShape.Rel c i j
⊢ d C i j ≫ eqToHom (_ : X C j = X C j) = d C i j
[PROOFSTEP]
simp only [eqToHom_refl, comp_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i i' j : ι
rij : ComplexShape.Rel c i j
rij' : ComplexShape.Rel c i' j
⊢ eqToHom (_ : X C i = X C i') ≫ d C i' j = d C i j
[PROOFSTEP]
obtain rfl := c.prev_eq rij rij'
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
rij rij' : ComplexShape.Rel c i j
⊢ eqToHom (_ : X C i = X C i) ≫ d C i j = d C i j
[PROOFSTEP]
simp only [eqToHom_refl, id_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
i j j' : ι
r : ComplexShape.Rel c i j
r' : ComplexShape.Rel c i j'
⊢ kernelSubobject (d C i j) = kernelSubobject (d C i j')
[PROOFSTEP]
rw [← d_comp_eqToHom C r r']
[GOAL]
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
i j j' : ι
r : ComplexShape.Rel c i j
r' : ComplexShape.Rel c i j'
⊢ kernelSubobject (d C i j' ≫ eqToHom (_ : X C j' = X C j)) = kernelSubobject (d C i j')
[PROOFSTEP]
apply kernelSubobject_comp_mono
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝¹ : HasImages V
inst✝ : HasEqualizers V
i i' j : ι
r : ComplexShape.Rel c i j
r' : ComplexShape.Rel c i' j
⊢ imageSubobject (d C i j) = imageSubobject (d C i' j)
[PROOFSTEP]
rw [← eqToHom_comp_d C r r']
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝¹ : HasImages V
inst✝ : HasEqualizers V
i i' j : ι
r : ComplexShape.Rel c i j
r' : ComplexShape.Rel c i' j
⊢ imageSubobject (eqToHom (_ : X C i = X C i') ≫ d C i' j) = imageSubobject (d C i' j)
[PROOFSTEP]
apply imageSubobject_iso_comp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
r : ComplexShape.Rel c i j
⊢ xPrev C j = X C i
[PROOFSTEP]
rw [← c.prev_eq' r]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j : ι
h : ¬ComplexShape.Rel c (ComplexShape.prev c j) j
⊢ ComplexShape.prev c j = j
[PROOFSTEP]
dsimp [ComplexShape.prev]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j : ι
h : ¬ComplexShape.Rel c (ComplexShape.prev c j) j
⊢ (if h : ∃ i, ComplexShape.Rel c i j then Exists.choose h else j) = j
[PROOFSTEP]
rw [dif_neg]
[GOAL]
case hnc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j : ι
h : ¬ComplexShape.Rel c (ComplexShape.prev c j) j
⊢ ¬∃ i, ComplexShape.Rel c i j
[PROOFSTEP]
push_neg
[GOAL]
case hnc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j : ι
h : ¬ComplexShape.Rel c (ComplexShape.prev c j) j
⊢ ∀ (i : ι), ¬ComplexShape.Rel c i j
[PROOFSTEP]
intro i hi
[GOAL]
case hnc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j : ι
h : ¬ComplexShape.Rel c (ComplexShape.prev c j) j
i : ι
hi : ComplexShape.Rel c i j
⊢ False
[PROOFSTEP]
have : c.prev j = i := c.prev_eq' hi
[GOAL]
case hnc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j : ι
h : ¬ComplexShape.Rel c (ComplexShape.prev c j) j
i : ι
hi : ComplexShape.Rel c i j
this : ComplexShape.prev c j = i
⊢ False
[PROOFSTEP]
rw [this] at h 
[GOAL]
case hnc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j i : ι
h : ¬ComplexShape.Rel c i j
hi : ComplexShape.Rel c i j
this : ComplexShape.prev c j = i
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
r : ComplexShape.Rel c i j
⊢ xNext C i = X C j
[PROOFSTEP]
rw [← c.next_eq' r]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i : ι
h : ¬ComplexShape.Rel c i (ComplexShape.next c i)
⊢ ComplexShape.next c i = i
[PROOFSTEP]
dsimp [ComplexShape.next]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i : ι
h : ¬ComplexShape.Rel c i (ComplexShape.next c i)
⊢ (if h : ∃ j, ComplexShape.Rel c i j then Exists.choose h else i) = i
[PROOFSTEP]
rw [dif_neg]
[GOAL]
case hnc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i : ι
h : ¬ComplexShape.Rel c i (ComplexShape.next c i)
⊢ ¬∃ j, ComplexShape.Rel c i j
[PROOFSTEP]
rintro ⟨j, hj⟩
[GOAL]
case hnc.intro
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i : ι
h : ¬ComplexShape.Rel c i (ComplexShape.next c i)
j : ι
hj : ComplexShape.Rel c i j
⊢ False
[PROOFSTEP]
have : c.next i = j := c.next_eq' hj
[GOAL]
case hnc.intro
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i : ι
h : ¬ComplexShape.Rel c i (ComplexShape.next c i)
j : ι
hj : ComplexShape.Rel c i j
this : ComplexShape.next c i = j
⊢ False
[PROOFSTEP]
rw [this] at h 
[GOAL]
case hnc.intro
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
h : ¬ComplexShape.Rel c i j
hj : ComplexShape.Rel c i j
this : ComplexShape.next c i = j
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
r : ComplexShape.Rel c i j
⊢ dTo C j = (xPrevIso C r).hom ≫ d C i j
[PROOFSTEP]
obtain rfl := c.prev_eq' r
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j : ι
r : ComplexShape.Rel c (ComplexShape.prev c j) j
⊢ dTo C j = (xPrevIso C r).hom ≫ d C (ComplexShape.prev c j) j
[PROOFSTEP]
exact (Category.id_comp _).symm
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
r : ComplexShape.Rel c i j
⊢ dFrom C i = d C i j ≫ (xNextIso C r).inv
[PROOFSTEP]
obtain rfl := c.next_eq' r
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i : ι
r : ComplexShape.Rel c i (ComplexShape.next c i)
⊢ dFrom C i = d C i (ComplexShape.next c i) ≫ (xNextIso C r).inv
[PROOFSTEP]
exact (Category.comp_id _).symm
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
r : ComplexShape.Rel c i j
⊢ (xPrevIso C r).inv ≫ dTo C j = d C i j
[PROOFSTEP]
simp [C.dTo_eq r]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j : ι
h : ¬ComplexShape.Rel c (ComplexShape.prev c j) j
⊢ (xPrevIsoSelf C h).inv ≫ dTo C j = 0
[PROOFSTEP]
simp [h]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
r : ComplexShape.Rel c i j
⊢ dFrom C i ≫ (xNextIso C r).hom = d C i j
[PROOFSTEP]
simp [C.dFrom_eq r]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i : ι
h : ¬ComplexShape.Rel c i (ComplexShape.next c i)
⊢ dFrom C i ≫ (xNextIsoSelf C h).hom = 0
[PROOFSTEP]
simp [h]
[GOAL]
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
i j : ι
r : ComplexShape.Rel c i j
⊢ kernelSubobject (dFrom C i) = kernelSubobject (d C i j)
[PROOFSTEP]
rw [C.dFrom_eq r]
[GOAL]
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
i j : ι
r : ComplexShape.Rel c i j
⊢ kernelSubobject (d C i j ≫ (xNextIso C r).inv) = kernelSubobject (d C i j)
[PROOFSTEP]
apply kernelSubobject_comp_mono
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝¹ : HasImages V
inst✝ : HasEqualizers V
i j : ι
r : ComplexShape.Rel c i j
⊢ imageSubobject (dTo C j) = imageSubobject (d C i j)
[PROOFSTEP]
rw [C.dTo_eq r]
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝¹ : HasImages V
inst✝ : HasEqualizers V
i j : ι
r : ComplexShape.Rel c i j
⊢ imageSubobject ((xPrevIso C r).hom ≫ d C i j) = imageSubobject (d C i j)
[PROOFSTEP]
apply imageSubobject_iso_comp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → X C₁ i ≅ X C₂ i
hf : autoParam (∀ (i j : ι), ComplexShape.Rel c i j → (f i).hom ≫ d C₂ i j = d C₁ i j ≫ (f j).hom) _auto✝
i j : ι
hij : ComplexShape.Rel c i j
⊢ (f i).inv ≫ d C₁ i j = (f i).inv ≫ (d C₁ i j ≫ (f j).hom) ≫ (f j).inv
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → X C₁ i ≅ X C₂ i
hf : autoParam (∀ (i j : ι), ComplexShape.Rel c i j → (f i).hom ≫ d C₂ i j = d C₁ i j ≫ (f j).hom) _auto✝
i j : ι
hij : ComplexShape.Rel c i j
⊢ (f i).inv ≫ (d C₁ i j ≫ (f j).hom) ≫ (f j).inv = (f i).inv ≫ ((f i).hom ≫ d C₂ i j) ≫ (f j).inv
[PROOFSTEP]
rw [hf i j hij]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → X C₁ i ≅ X C₂ i
hf : autoParam (∀ (i j : ι), ComplexShape.Rel c i j → (f i).hom ≫ d C₂ i j = d C₁ i j ≫ (f j).hom) _auto✝
i j : ι
hij : ComplexShape.Rel c i j
⊢ (f i).inv ≫ ((f i).hom ≫ d C₂ i j) ≫ (f j).inv = d C₂ i j ≫ (f j).inv
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → X C₁ i ≅ X C₂ i
hf : autoParam (∀ (i j : ι), ComplexShape.Rel c i j → (f i).hom ≫ d C₂ i j = d C₁ i j ≫ (f j).hom) _auto✝
⊢ ((mk fun i => (f i).hom) ≫ mk fun i => (f i).inv) = 𝟙 C₁
[PROOFSTEP]
ext i
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → X C₁ i ≅ X C₂ i
hf : autoParam (∀ (i j : ι), ComplexShape.Rel c i j → (f i).hom ≫ d C₂ i j = d C₁ i j ≫ (f j).hom) _auto✝
i : ι
⊢ HomologicalComplex.Hom.f ((mk fun i => (f i).hom) ≫ mk fun i => (f i).inv) i = HomologicalComplex.Hom.f (𝟙 C₁) i
[PROOFSTEP]
exact (f i).hom_inv_id
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → X C₁ i ≅ X C₂ i
hf : autoParam (∀ (i j : ι), ComplexShape.Rel c i j → (f i).hom ≫ d C₂ i j = d C₁ i j ≫ (f j).hom) _auto✝
⊢ ((mk fun i => (f i).inv) ≫ mk fun i => (f i).hom) = 𝟙 C₂
[PROOFSTEP]
ext i
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → X C₁ i ≅ X C₂ i
hf : autoParam (∀ (i j : ι), ComplexShape.Rel c i j → (f i).hom ≫ d C₂ i j = d C₁ i j ≫ (f j).hom) _auto✝
i : ι
⊢ HomologicalComplex.Hom.f ((mk fun i => (f i).inv) ≫ mk fun i => (f i).hom) i = HomologicalComplex.Hom.f (𝟙 C₂) i
[PROOFSTEP]
exact (f i).inv_hom_id
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → X C₁ i ≅ X C₂ i
hf : ∀ (i j : ι), ComplexShape.Rel c i j → (f i).hom ≫ d C₂ i j = d C₁ i j ≫ (f j).hom
i : ι
⊢ isoApp (isoOfComponents f) i = f i
[PROOFSTEP]
ext
[GOAL]
case w
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → X C₁ i ≅ X C₂ i
hf : ∀ (i j : ι), ComplexShape.Rel c i j → (f i).hom ≫ d C₂ i j = d C₁ i j ≫ (f j).hom
i : ι
⊢ (isoApp (isoOfComponents f) i).hom = (f i).hom
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : Hom C₁ C₂
i j : ι
w : ComplexShape.Rel c i j
⊢ prev f j = (xPrevIso C₁ w).hom ≫ HomologicalComplex.Hom.f f i ≫ (xPrevIso C₂ w).inv
[PROOFSTEP]
obtain rfl := c.prev_eq' w
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : Hom C₁ C₂
j : ι
w : ComplexShape.Rel c (ComplexShape.prev c j) j
⊢ prev f j = (xPrevIso C₁ w).hom ≫ HomologicalComplex.Hom.f f (ComplexShape.prev c j) ≫ (xPrevIso C₂ w).inv
[PROOFSTEP]
simp only [xPrevIso, eqToIso_refl, Iso.refl_hom, Iso.refl_inv, comp_id, id_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : Hom C₁ C₂
i j : ι
w : ComplexShape.Rel c i j
⊢ next f i = (xNextIso C₁ w).hom ≫ HomologicalComplex.Hom.f f j ≫ (xNextIso C₂ w).inv
[PROOFSTEP]
obtain rfl := c.next_eq' w
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : Hom C₁ C₂
i : ι
w : ComplexShape.Rel c i (ComplexShape.next c i)
⊢ next f i = (xNextIso C₁ w).hom ≫ HomologicalComplex.Hom.f f (ComplexShape.next c i) ≫ (xNextIso C₂ w).inv
[PROOFSTEP]
simp only [xNextIso, eqToIso_refl, Iso.refl_hom, Iso.refl_inv, comp_id, id_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
i j : α
h : i = j + 1
⊢ X i = X (j + 1)
[PROOFSTEP]
rw [h]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
i j : α
w : ¬ComplexShape.Rel (ComplexShape.down α) i j
⊢ (fun i j => if h : i = j + 1 then eqToHom (_ : X i = X (j + 1)) ≫ d j else 0) i j = 0
[PROOFSTEP]
dsimp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
i j : α
w : ¬ComplexShape.Rel (ComplexShape.down α) i j
⊢ (if h : i = j + 1 then eqToHom (_ : X i = X (j + 1)) ≫ d j else 0) = 0
[PROOFSTEP]
rw [dif_neg (Ne.symm w)]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
i j k : α
hij : ComplexShape.Rel (ComplexShape.down α) i j
hjk : ComplexShape.Rel (ComplexShape.down α) j k
⊢ (fun i j => if h : i = j + 1 then eqToHom (_ : X i = X (j + 1)) ≫ d j else 0) i j ≫
      (fun i j => if h : i = j + 1 then eqToHom (_ : X i = X (j + 1)) ≫ d j else 0) j k =
    0
[PROOFSTEP]
dsimp at hij hjk 
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
i j k : α
hij : j + 1 = i
hjk : k + 1 = j
⊢ (fun i j => if h : i = j + 1 then eqToHom (_ : X i = X (j + 1)) ≫ d j else 0) i j ≫
      (fun i j => if h : i = j + 1 then eqToHom (_ : X i = X (j + 1)) ≫ d j else 0) j k =
    0
[PROOFSTEP]
substs hij hjk
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
k : α
⊢ (fun i j => if h : i = j + 1 then eqToHom (_ : X i = X (j + 1)) ≫ d j else 0) (k + 1 + 1) (k + 1) ≫
      (fun i j => if h : i = j + 1 then eqToHom (_ : X i = X (j + 1)) ≫ d j else 0) (k + 1) k =
    0
[PROOFSTEP]
simp only [eqToHom_refl, id_comp, dite_eq_ite, ite_true, sq]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
j : α
⊢ HomologicalComplex.d (of X d sq) (j + 1) j = d j
[PROOFSTEP]
dsimp [of]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
j : α
⊢ (if j + 1 = j + 1 then 𝟙 (X (j + 1)) ≫ d j else 0) = d j
[PROOFSTEP]
rw [if_pos rfl, Category.id_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
i j : α
h : i ≠ j + 1
⊢ HomologicalComplex.d (of X d sq) i j = 0
[PROOFSTEP]
dsimp [of]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
i j : α
h : i ≠ j + 1
⊢ (if h : i = j + 1 then eqToHom (_ : X i = X (j + 1)) ≫ d j else 0) = 0
[PROOFSTEP]
rw [dif_neg h]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d_X : (n : α) → X (n + 1) ⟶ X n
sq_X : ∀ (n : α), d_X (n + 1) ≫ d_X n = 0
Y : α → V
d_Y : (n : α) → Y (n + 1) ⟶ Y n
sq_Y : ∀ (n : α), d_Y (n + 1) ≫ d_Y n = 0
f : (i : α) → X i ⟶ Y i
comm : ∀ (i : α), f (i + 1) ≫ d_Y i = d_X i ≫ f i
n m : α
⊢ ComplexShape.Rel (ComplexShape.down α) n m →
    f n ≫ HomologicalComplex.d (of Y d_Y sq_Y) n m = HomologicalComplex.d (of X d_X sq_X) n m ≫ f m
[PROOFSTEP]
by_cases h : n = m + 1
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d_X : (n : α) → X (n + 1) ⟶ X n
sq_X : ∀ (n : α), d_X (n + 1) ≫ d_X n = 0
Y : α → V
d_Y : (n : α) → Y (n + 1) ⟶ Y n
sq_Y : ∀ (n : α), d_Y (n + 1) ≫ d_Y n = 0
f : (i : α) → X i ⟶ Y i
comm : ∀ (i : α), f (i + 1) ≫ d_Y i = d_X i ≫ f i
n m : α
h : n = m + 1
⊢ ComplexShape.Rel (ComplexShape.down α) n m →
    f n ≫ HomologicalComplex.d (of Y d_Y sq_Y) n m = HomologicalComplex.d (of X d_X sq_X) n m ≫ f m
[PROOFSTEP]
subst h
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d_X : (n : α) → X (n + 1) ⟶ X n
sq_X : ∀ (n : α), d_X (n + 1) ≫ d_X n = 0
Y : α → V
d_Y : (n : α) → Y (n + 1) ⟶ Y n
sq_Y : ∀ (n : α), d_Y (n + 1) ≫ d_Y n = 0
f : (i : α) → X i ⟶ Y i
comm : ∀ (i : α), f (i + 1) ≫ d_Y i = d_X i ≫ f i
m : α
⊢ ComplexShape.Rel (ComplexShape.down α) (m + 1) m →
    f (m + 1) ≫ HomologicalComplex.d (of Y d_Y sq_Y) (m + 1) m = HomologicalComplex.d (of X d_X sq_X) (m + 1) m ≫ f m
[PROOFSTEP]
simpa using comm m
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d_X : (n : α) → X (n + 1) ⟶ X n
sq_X : ∀ (n : α), d_X (n + 1) ≫ d_X n = 0
Y : α → V
d_Y : (n : α) → Y (n + 1) ⟶ Y n
sq_Y : ∀ (n : α), d_Y (n + 1) ≫ d_Y n = 0
f : (i : α) → X i ⟶ Y i
comm : ∀ (i : α), f (i + 1) ≫ d_Y i = d_X i ≫ f i
n m : α
h : ¬n = m + 1
⊢ ComplexShape.Rel (ComplexShape.down α) n m →
    f n ≫ HomologicalComplex.d (of Y d_Y sq_Y) n m = HomologicalComplex.d (of X d_X sq_X) n m ≫ f m
[PROOFSTEP]
rw [of_d_ne X _ _ h, of_d_ne Y _ _ h]
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d_X : (n : α) → X (n + 1) ⟶ X n
sq_X : ∀ (n : α), d_X (n + 1) ≫ d_X n = 0
Y : α → V
d_Y : (n : α) → Y (n + 1) ⟶ Y n
sq_Y : ∀ (n : α), d_Y (n + 1) ≫ d_Y n = 0
f : (i : α) → X i ⟶ Y i
comm : ∀ (i : α), f (i + 1) ≫ d_Y i = d_X i ≫ f i
n m : α
h : ¬n = m + 1
⊢ ComplexShape.Rel (ComplexShape.down α) n m → f n ≫ 0 = 0 ≫ f m
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ :
  (t : (X₀ : V) ×' (X₁ : V) ×' (X₂ : V) ×' (d₀ : X₁ ⟶ X₀) ×' (d₁ : X₂ ⟶ X₁) ×' d₁ ≫ d₀ = 0) →
    (X₃ : V) ×' (d₂ : X₃ ⟶ t.snd.snd.fst) ×' d₂ ≫ t.snd.snd.snd.snd.fst = 0
⊢ HomologicalComplex.d (mk X₀ X₁ X₂ d₀ d₁ s succ) 1 0 = d₀
[PROOFSTEP]
change ite (1 = 0 + 1) (𝟙 X₁ ≫ d₀) 0 = d₀
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ :
  (t : (X₀ : V) ×' (X₁ : V) ×' (X₂ : V) ×' (d₀ : X₁ ⟶ X₀) ×' (d₁ : X₂ ⟶ X₁) ×' d₁ ≫ d₀ = 0) →
    (X₃ : V) ×' (d₂ : X₃ ⟶ t.snd.snd.fst) ×' d₂ ≫ t.snd.snd.snd.snd.fst = 0
⊢ (if 1 = 0 + 1 then 𝟙 X₁ ≫ d₀ else 0) = d₀
[PROOFSTEP]
rw [if_pos rfl, Category.id_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ :
  (t : (X₀ : V) ×' (X₁ : V) ×' (X₂ : V) ×' (d₀ : X₁ ⟶ X₀) ×' (d₁ : X₂ ⟶ X₁) ×' d₁ ≫ d₀ = 0) →
    (X₃ : V) ×' (d₂ : X₃ ⟶ t.snd.snd.fst) ×' d₂ ≫ t.snd.snd.snd.snd.fst = 0
⊢ HomologicalComplex.d (mk X₀ X₁ X₂ d₀ d₁ s succ) 2 1 = d₁
[PROOFSTEP]
change ite (2 = 1 + 1) (𝟙 X₂ ≫ d₁) 0 = d₁
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ :
  (t : (X₀ : V) ×' (X₁ : V) ×' (X₂ : V) ×' (d₀ : X₁ ⟶ X₀) ×' (d₁ : X₂ ⟶ X₁) ×' d₁ ≫ d₀ = 0) →
    (X₃ : V) ×' (d₂ : X₃ ⟶ t.snd.snd.fst) ×' d₂ ≫ t.snd.snd.snd.snd.fst = 0
⊢ (if 2 = 1 + 1 then 𝟙 X₂ ≫ d₁ else 0) = d₁
[PROOFSTEP]
rw [if_pos rfl, Category.id_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ :
  (t : (X₀ : V) ×' (X₁ : V) ×' (X₂ : V) ×' (d₀ : X₁ ⟶ X₀) ×' (d₁ : X₂ ⟶ X₁) ×' d₁ ≫ d₀ = 0) →
    (X₃ : V) ×' (d₂ : X₃ ⟶ t.snd.snd.fst) ×' d₂ ≫ t.snd.snd.snd.snd.fst = 0
succ' : (t : (X₀ : V) × (X₁ : V) × (X₁ ⟶ X₀)) → (X₂ : V) ×' (d : X₂ ⟶ t.snd.fst) ×' d ≫ t.snd.snd = 0
⊢ HomologicalComplex.d (mk' X₀ X₁ d₀ succ') 1 0 = d₀
[PROOFSTEP]
change ite (1 = 0 + 1) (𝟙 X₁ ≫ d₀) 0 = d₀
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ :
  (t : (X₀ : V) ×' (X₁ : V) ×' (X₂ : V) ×' (d₀ : X₁ ⟶ X₀) ×' (d₁ : X₂ ⟶ X₁) ×' d₁ ≫ d₀ = 0) →
    (X₃ : V) ×' (d₂ : X₃ ⟶ t.snd.snd.fst) ×' d₂ ≫ t.snd.snd.snd.snd.fst = 0
succ' : (t : (X₀ : V) × (X₁ : V) × (X₁ ⟶ X₀)) → (X₂ : V) ×' (d : X₂ ⟶ t.snd.fst) ×' d ≫ t.snd.snd = 0
⊢ (if 1 = 0 + 1 then 𝟙 X₁ ≫ d₀ else 0) = d₀
[PROOFSTEP]
rw [if_pos rfl, Category.id_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
P Q : ChainComplex V ℕ
zero : HomologicalComplex.X P 0 ⟶ HomologicalComplex.X Q 0
one : HomologicalComplex.X P 1 ⟶ HomologicalComplex.X Q 1
one_zero_comm : one ≫ HomologicalComplex.d Q 1 0 = HomologicalComplex.d P 1 0 ≫ zero
succ :
  (n : ℕ) →
    (p :
        (f : HomologicalComplex.X P n ⟶ HomologicalComplex.X Q n) ×'
          (f' : HomologicalComplex.X P (n + 1) ⟶ HomologicalComplex.X Q (n + 1)) ×'
            f' ≫ HomologicalComplex.d Q (n + 1) n = HomologicalComplex.d P (n + 1) n ≫ f) →
      (f'' : HomologicalComplex.X P (n + 2) ⟶ HomologicalComplex.X Q (n + 2)) ×'
        f'' ≫ HomologicalComplex.d Q (n + 2) (n + 1) = HomologicalComplex.d P (n + 2) (n + 1) ≫ p.snd.fst
n m : ℕ
⊢ ComplexShape.Rel (ComplexShape.down ℕ) n m →
    (fun n => (mkHomAux P Q zero one one_zero_comm succ n).fst) n ≫ HomologicalComplex.d Q n m =
      HomologicalComplex.d P n m ≫ (fun n => (mkHomAux P Q zero one one_zero_comm succ n).fst) m
[PROOFSTEP]
rintro (rfl : m + 1 = n)
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
P Q : ChainComplex V ℕ
zero : HomologicalComplex.X P 0 ⟶ HomologicalComplex.X Q 0
one : HomologicalComplex.X P 1 ⟶ HomologicalComplex.X Q 1
one_zero_comm : one ≫ HomologicalComplex.d Q 1 0 = HomologicalComplex.d P 1 0 ≫ zero
succ :
  (n : ℕ) →
    (p :
        (f : HomologicalComplex.X P n ⟶ HomologicalComplex.X Q n) ×'
          (f' : HomologicalComplex.X P (n + 1) ⟶ HomologicalComplex.X Q (n + 1)) ×'
            f' ≫ HomologicalComplex.d Q (n + 1) n = HomologicalComplex.d P (n + 1) n ≫ f) →
      (f'' : HomologicalComplex.X P (n + 2) ⟶ HomologicalComplex.X Q (n + 2)) ×'
        f'' ≫ HomologicalComplex.d Q (n + 2) (n + 1) = HomologicalComplex.d P (n + 2) (n + 1) ≫ p.snd.fst
m : ℕ
⊢ (fun n => (mkHomAux P Q zero one one_zero_comm succ n).fst) (m + 1) ≫ HomologicalComplex.d Q (m + 1) m =
    HomologicalComplex.d P (m + 1) m ≫ (fun n => (mkHomAux P Q zero one one_zero_comm succ n).fst) m
[PROOFSTEP]
exact (mkHomAux P Q zero one one_zero_comm succ m).2.2
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
P Q : ChainComplex V ℕ
zero : HomologicalComplex.X P 0 ⟶ HomologicalComplex.X Q 0
one : HomologicalComplex.X P 1 ⟶ HomologicalComplex.X Q 1
one_zero_comm : one ≫ HomologicalComplex.d Q 1 0 = HomologicalComplex.d P 1 0 ≫ zero
succ :
  (n : ℕ) →
    (p :
        (f : HomologicalComplex.X P n ⟶ HomologicalComplex.X Q n) ×'
          (f' : HomologicalComplex.X P (n + 1) ⟶ HomologicalComplex.X Q (n + 1)) ×'
            f' ≫ HomologicalComplex.d Q (n + 1) n = HomologicalComplex.d P (n + 1) n ≫ f) →
      (f'' : HomologicalComplex.X P (n + 2) ⟶ HomologicalComplex.X Q (n + 2)) ×'
        f'' ≫ HomologicalComplex.d Q (n + 2) (n + 1) = HomologicalComplex.d P (n + 2) (n + 1) ≫ p.snd.fst
n : ℕ
⊢ HomologicalComplex.Hom.f (mkHom P Q zero one one_zero_comm succ) (n + 2) =
    (succ n
        { fst := HomologicalComplex.Hom.f (mkHom P Q zero one one_zero_comm succ) n,
          snd :=
            { fst := HomologicalComplex.Hom.f (mkHom P Q zero one one_zero_comm succ) (n + 1),
              snd :=
                (_ :
                  HomologicalComplex.Hom.f (mkHom P Q zero one one_zero_comm succ) (n + 1) ≫
                      HomologicalComplex.d Q (n + 1) n =
                    HomologicalComplex.d P (n + 1) n ≫
                      HomologicalComplex.Hom.f (mkHom P Q zero one one_zero_comm succ) n) } }).fst
[PROOFSTEP]
dsimp [mkHom, mkHomAux]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j : α
h : i + 1 = j
⊢ X (i + 1) = X j
[PROOFSTEP]
rw [h]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j : α
w : ¬ComplexShape.Rel (ComplexShape.up α) i j
⊢ (fun i j => if h : i + 1 = j then d i ≫ eqToHom (_ : X (i + 1) = X j) else 0) i j = 0
[PROOFSTEP]
dsimp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j : α
w : ¬ComplexShape.Rel (ComplexShape.up α) i j
⊢ (if h : i + 1 = j then d i ≫ eqToHom (_ : X (i + 1) = X j) else 0) = 0
[PROOFSTEP]
rw [dif_neg]
[GOAL]
case hnc
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j : α
w : ¬ComplexShape.Rel (ComplexShape.up α) i j
⊢ ¬i + 1 = j
[PROOFSTEP]
exact w
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
⊢ ComplexShape.Rel (ComplexShape.up α) i j →
    ComplexShape.Rel (ComplexShape.up α) j k →
      (fun i j => if h : i + 1 = j then d i ≫ eqToHom (_ : X (i + 1) = X j) else 0) i j ≫
          (fun i j => if h : i + 1 = j then d i ≫ eqToHom (_ : X (i + 1) = X j) else 0) j k =
        0
[PROOFSTEP]
dsimp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
⊢ i + 1 = j →
    j + 1 = k →
      ((if h : i + 1 = j then d i ≫ eqToHom (_ : X (i + 1) = X j) else 0) ≫
          if h : j + 1 = k then d j ≫ eqToHom (_ : X (j + 1) = X k) else 0) =
        0
[PROOFSTEP]
split_ifs with h h' h'
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
h : i + 1 = j
h' : j + 1 = k
⊢ i + 1 = j → j + 1 = k → (d i ≫ eqToHom (_ : X (i + 1) = X j)) ≫ d j ≫ eqToHom (_ : X (j + 1) = X k) = 0
[PROOFSTEP]
substs h h'
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i : α
⊢ i + 1 = i + 1 →
    i + 1 + 1 = i + 1 + 1 →
      (d i ≫ eqToHom (_ : X (i + 1) = X (i + 1))) ≫ d (i + 1) ≫ eqToHom (_ : X (i + 1 + 1) = X (i + 1 + 1)) = 0
[PROOFSTEP]
simp [sq]
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
h : i + 1 = j
h' : ¬j + 1 = k
⊢ i + 1 = j → j + 1 = k → (d i ≫ eqToHom (_ : X (i + 1) = X j)) ≫ 0 = 0
case pos
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
h : ¬i + 1 = j
h' : j + 1 = k
⊢ i + 1 = j → j + 1 = k → 0 ≫ d j ≫ eqToHom (_ : X (j + 1) = X k) = 0
case neg
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
h : ¬i + 1 = j
h' : ¬j + 1 = k
⊢ i + 1 = j → j + 1 = k → 0 ≫ 0 = 0
[PROOFSTEP]
all_goals simp
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
h : i + 1 = j
h' : ¬j + 1 = k
⊢ i + 1 = j → j + 1 = k → (d i ≫ eqToHom (_ : X (i + 1) = X j)) ≫ 0 = 0
[PROOFSTEP]
simp
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
h : ¬i + 1 = j
h' : j + 1 = k
⊢ i + 1 = j → j + 1 = k → 0 ≫ d j ≫ eqToHom (_ : X (j + 1) = X k) = 0
[PROOFSTEP]
simp
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
h : ¬i + 1 = j
h' : ¬j + 1 = k
⊢ i + 1 = j → j + 1 = k → 0 ≫ 0 = 0
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
j : α
⊢ HomologicalComplex.d (of X d sq) j (j + 1) = d j
[PROOFSTEP]
dsimp [of]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
j : α
⊢ (if j + 1 = j + 1 then d j ≫ 𝟙 (X (j + 1)) else 0) = d j
[PROOFSTEP]
rw [if_pos rfl, Category.comp_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j : α
h : i + 1 ≠ j
⊢ HomologicalComplex.d (of X d sq) i j = 0
[PROOFSTEP]
dsimp [of]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j : α
h : i + 1 ≠ j
⊢ (if h : i + 1 = j then d i ≫ eqToHom (_ : X (i + 1) = X j) else 0) = 0
[PROOFSTEP]
rw [dif_neg h]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d_X : (n : α) → X n ⟶ X (n + 1)
sq_X : ∀ (n : α), d_X n ≫ d_X (n + 1) = 0
Y : α → V
d_Y : (n : α) → Y n ⟶ Y (n + 1)
sq_Y : ∀ (n : α), d_Y n ≫ d_Y (n + 1) = 0
f : (i : α) → X i ⟶ Y i
comm : ∀ (i : α), f i ≫ d_Y i = d_X i ≫ f (i + 1)
n m : α
⊢ ComplexShape.Rel (ComplexShape.up α) n m →
    f n ≫ HomologicalComplex.d (of Y d_Y sq_Y) n m = HomologicalComplex.d (of X d_X sq_X) n m ≫ f m
[PROOFSTEP]
by_cases h : n + 1 = m
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d_X : (n : α) → X n ⟶ X (n + 1)
sq_X : ∀ (n : α), d_X n ≫ d_X (n + 1) = 0
Y : α → V
d_Y : (n : α) → Y n ⟶ Y (n + 1)
sq_Y : ∀ (n : α), d_Y n ≫ d_Y (n + 1) = 0
f : (i : α) → X i ⟶ Y i
comm : ∀ (i : α), f i ≫ d_Y i = d_X i ≫ f (i + 1)
n m : α
h : n + 1 = m
⊢ ComplexShape.Rel (ComplexShape.up α) n m →
    f n ≫ HomologicalComplex.d (of Y d_Y sq_Y) n m = HomologicalComplex.d (of X d_X sq_X) n m ≫ f m
[PROOFSTEP]
subst h
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d_X : (n : α) → X n ⟶ X (n + 1)
sq_X : ∀ (n : α), d_X n ≫ d_X (n + 1) = 0
Y : α → V
d_Y : (n : α) → Y n ⟶ Y (n + 1)
sq_Y : ∀ (n : α), d_Y n ≫ d_Y (n + 1) = 0
f : (i : α) → X i ⟶ Y i
comm : ∀ (i : α), f i ≫ d_Y i = d_X i ≫ f (i + 1)
n : α
⊢ ComplexShape.Rel (ComplexShape.up α) n (n + 1) →
    f n ≫ HomologicalComplex.d (of Y d_Y sq_Y) n (n + 1) = HomologicalComplex.d (of X d_X sq_X) n (n + 1) ≫ f (n + 1)
[PROOFSTEP]
simpa using comm n
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d_X : (n : α) → X n ⟶ X (n + 1)
sq_X : ∀ (n : α), d_X n ≫ d_X (n + 1) = 0
Y : α → V
d_Y : (n : α) → Y n ⟶ Y (n + 1)
sq_Y : ∀ (n : α), d_Y n ≫ d_Y (n + 1) = 0
f : (i : α) → X i ⟶ Y i
comm : ∀ (i : α), f i ≫ d_Y i = d_X i ≫ f (i + 1)
n m : α
h : ¬n + 1 = m
⊢ ComplexShape.Rel (ComplexShape.up α) n m →
    f n ≫ HomologicalComplex.d (of Y d_Y sq_Y) n m = HomologicalComplex.d (of X d_X sq_X) n m ≫ f m
[PROOFSTEP]
rw [of_d_ne X _ _ h, of_d_ne Y _ _ h]
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d_X : (n : α) → X n ⟶ X (n + 1)
sq_X : ∀ (n : α), d_X n ≫ d_X (n + 1) = 0
Y : α → V
d_Y : (n : α) → Y n ⟶ Y (n + 1)
sq_Y : ∀ (n : α), d_Y n ≫ d_Y (n + 1) = 0
f : (i : α) → X i ⟶ Y i
comm : ∀ (i : α), f i ≫ d_Y i = d_X i ≫ f (i + 1)
n m : α
h : ¬n + 1 = m
⊢ ComplexShape.Rel (ComplexShape.up α) n m → f n ≫ 0 = 0 ≫ f m
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ :
  (t : (X₀ : V) ×' (X₁ : V) ×' (X₂ : V) ×' (d₀ : X₀ ⟶ X₁) ×' (d₁ : X₁ ⟶ X₂) ×' d₀ ≫ d₁ = 0) →
    (X₃ : V) ×' (d₂ : t.snd.snd.fst ⟶ X₃) ×' t.snd.snd.snd.snd.fst ≫ d₂ = 0
⊢ HomologicalComplex.d (mk X₀ X₁ X₂ d₀ d₁ s succ) 0 1 = d₀
[PROOFSTEP]
change ite (1 = 0 + 1) (d₀ ≫ 𝟙 X₁) 0 = d₀
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ :
  (t : (X₀ : V) ×' (X₁ : V) ×' (X₂ : V) ×' (d₀ : X₀ ⟶ X₁) ×' (d₁ : X₁ ⟶ X₂) ×' d₀ ≫ d₁ = 0) →
    (X₃ : V) ×' (d₂ : t.snd.snd.fst ⟶ X₃) ×' t.snd.snd.snd.snd.fst ≫ d₂ = 0
⊢ (if 1 = 0 + 1 then d₀ ≫ 𝟙 X₁ else 0) = d₀
[PROOFSTEP]
rw [if_pos rfl, Category.comp_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ :
  (t : (X₀ : V) ×' (X₁ : V) ×' (X₂ : V) ×' (d₀ : X₀ ⟶ X₁) ×' (d₁ : X₁ ⟶ X₂) ×' d₀ ≫ d₁ = 0) →
    (X₃ : V) ×' (d₂ : t.snd.snd.fst ⟶ X₃) ×' t.snd.snd.snd.snd.fst ≫ d₂ = 0
⊢ HomologicalComplex.d (mk X₀ X₁ X₂ d₀ d₁ s succ) 1 2 = d₁
[PROOFSTEP]
change ite (2 = 1 + 1) (d₁ ≫ 𝟙 X₂) 0 = d₁
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ :
  (t : (X₀ : V) ×' (X₁ : V) ×' (X₂ : V) ×' (d₀ : X₀ ⟶ X₁) ×' (d₁ : X₁ ⟶ X₂) ×' d₀ ≫ d₁ = 0) →
    (X₃ : V) ×' (d₂ : t.snd.snd.fst ⟶ X₃) ×' t.snd.snd.snd.snd.fst ≫ d₂ = 0
⊢ (if 2 = 1 + 1 then d₁ ≫ 𝟙 X₂ else 0) = d₁
[PROOFSTEP]
rw [if_pos rfl, Category.comp_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ :
  (t : (X₀ : V) ×' (X₁ : V) ×' (X₂ : V) ×' (d₀ : X₀ ⟶ X₁) ×' (d₁ : X₁ ⟶ X₂) ×' d₀ ≫ d₁ = 0) →
    (X₃ : V) ×' (d₂ : t.snd.snd.fst ⟶ X₃) ×' t.snd.snd.snd.snd.fst ≫ d₂ = 0
succ' : (t : (X₀ : V) × (X₁ : V) × (X₀ ⟶ X₁)) → (X₂ : V) ×' (d : t.snd.fst ⟶ X₂) ×' t.snd.snd ≫ d = 0
⊢ HomologicalComplex.d (mk' X₀ X₁ d₀ succ') 0 1 = d₀
[PROOFSTEP]
change ite (1 = 0 + 1) (d₀ ≫ 𝟙 X₁) 0 = d₀
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ :
  (t : (X₀ : V) ×' (X₁ : V) ×' (X₂ : V) ×' (d₀ : X₀ ⟶ X₁) ×' (d₁ : X₁ ⟶ X₂) ×' d₀ ≫ d₁ = 0) →
    (X₃ : V) ×' (d₂ : t.snd.snd.fst ⟶ X₃) ×' t.snd.snd.snd.snd.fst ≫ d₂ = 0
succ' : (t : (X₀ : V) × (X₁ : V) × (X₀ ⟶ X₁)) → (X₂ : V) ×' (d : t.snd.fst ⟶ X₂) ×' t.snd.snd ≫ d = 0
⊢ (if 1 = 0 + 1 then d₀ ≫ 𝟙 X₁ else 0) = d₀
[PROOFSTEP]
rw [if_pos rfl, Category.comp_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
P Q : CochainComplex V ℕ
zero : HomologicalComplex.X P 0 ⟶ HomologicalComplex.X Q 0
one : HomologicalComplex.X P 1 ⟶ HomologicalComplex.X Q 1
one_zero_comm : zero ≫ HomologicalComplex.d Q 0 1 = HomologicalComplex.d P 0 1 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : HomologicalComplex.X P n ⟶ HomologicalComplex.X Q n) ×'
          (f' : HomologicalComplex.X P (n + 1) ⟶ HomologicalComplex.X Q (n + 1)) ×'
            f ≫ HomologicalComplex.d Q n (n + 1) = HomologicalComplex.d P n (n + 1) ≫ f') →
      (f'' : HomologicalComplex.X P (n + 2) ⟶ HomologicalComplex.X Q (n + 2)) ×'
        p.snd.fst ≫ HomologicalComplex.d Q (n + 1) (n + 2) = HomologicalComplex.d P (n + 1) (n + 2) ≫ f''
n m : ℕ
⊢ ComplexShape.Rel (ComplexShape.up ℕ) n m →
    (fun n => (mkHomAux P Q zero one one_zero_comm succ n).fst) n ≫ HomologicalComplex.d Q n m =
      HomologicalComplex.d P n m ≫ (fun n => (mkHomAux P Q zero one one_zero_comm succ n).fst) m
[PROOFSTEP]
rintro (rfl : n + 1 = m)
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
P Q : CochainComplex V ℕ
zero : HomologicalComplex.X P 0 ⟶ HomologicalComplex.X Q 0
one : HomologicalComplex.X P 1 ⟶ HomologicalComplex.X Q 1
one_zero_comm : zero ≫ HomologicalComplex.d Q 0 1 = HomologicalComplex.d P 0 1 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : HomologicalComplex.X P n ⟶ HomologicalComplex.X Q n) ×'
          (f' : HomologicalComplex.X P (n + 1) ⟶ HomologicalComplex.X Q (n + 1)) ×'
            f ≫ HomologicalComplex.d Q n (n + 1) = HomologicalComplex.d P n (n + 1) ≫ f') →
      (f'' : HomologicalComplex.X P (n + 2) ⟶ HomologicalComplex.X Q (n + 2)) ×'
        p.snd.fst ≫ HomologicalComplex.d Q (n + 1) (n + 2) = HomologicalComplex.d P (n + 1) (n + 2) ≫ f''
n : ℕ
⊢ (fun n => (mkHomAux P Q zero one one_zero_comm succ n).fst) n ≫ HomologicalComplex.d Q n (n + 1) =
    HomologicalComplex.d P n (n + 1) ≫ (fun n => (mkHomAux P Q zero one one_zero_comm succ n).fst) (n + 1)
[PROOFSTEP]
exact (mkHomAux P Q zero one one_zero_comm succ n).2.2
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
P Q : CochainComplex V ℕ
zero : HomologicalComplex.X P 0 ⟶ HomologicalComplex.X Q 0
one : HomologicalComplex.X P 1 ⟶ HomologicalComplex.X Q 1
one_zero_comm : zero ≫ HomologicalComplex.d Q 0 1 = HomologicalComplex.d P 0 1 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : HomologicalComplex.X P n ⟶ HomologicalComplex.X Q n) ×'
          (f' : HomologicalComplex.X P (n + 1) ⟶ HomologicalComplex.X Q (n + 1)) ×'
            f ≫ HomologicalComplex.d Q n (n + 1) = HomologicalComplex.d P n (n + 1) ≫ f') →
      (f'' : HomologicalComplex.X P (n + 2) ⟶ HomologicalComplex.X Q (n + 2)) ×'
        p.snd.fst ≫ HomologicalComplex.d Q (n + 1) (n + 2) = HomologicalComplex.d P (n + 1) (n + 2) ≫ f''
n : ℕ
⊢ HomologicalComplex.Hom.f (mkHom P Q zero one one_zero_comm succ) (n + 2) =
    (succ n
        { fst := HomologicalComplex.Hom.f (mkHom P Q zero one one_zero_comm succ) n,
          snd :=
            { fst := HomologicalComplex.Hom.f (mkHom P Q zero one one_zero_comm succ) (n + 1),
              snd :=
                (_ :
                  HomologicalComplex.Hom.f (mkHom P Q zero one one_zero_comm succ) n ≫
                      HomologicalComplex.d Q n (n + 1) =
                    HomologicalComplex.d P n (n + 1) ≫
                      HomologicalComplex.Hom.f (mkHom P Q zero one one_zero_comm succ) (n + 1)) } }).fst
[PROOFSTEP]
dsimp [mkHom, mkHomAux]
