[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.11796, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ S.f ≫ k = 0
[PROOFSTEP]
rw [hx, S.zero_assoc, zero_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ h.ι ≫ descQ h k (_ : S.f ≫ k = 0) = 0
[PROOFSTEP]
rw [show 0 = h.ι ≫ h.g' ≫ x by simp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ 0 = h.ι ≫ g' h ≫ x
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ h.ι ≫ descQ h k (_ : S.f ≫ k = 0) = h.ι ≫ g' h ≫ x
[PROOFSTEP]
congr 1
[GOAL]
case e_a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
k : S.X₂ ⟶ A
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ descQ h k (_ : S.f ≫ k = 0) = g' h ≫ x
[PROOFSTEP]
simp only [← cancel_epi h.p, hx, p_descQ, p_g'_assoc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
hf : S.f = 0
⊢ S.f ≫ 𝟙 S.X₂ = 0
[PROOFSTEP]
rw [hf, comp_id]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
hf : S.f = 0
⊢ descQ h (𝟙 S.X₂) (_ : S.f ≫ 𝟙 S.X₂ = 0) ≫ h.p = 𝟙 h.Q
[PROOFSTEP]
simp only [← cancel_epi h.p, p_descQ_assoc, id_comp, comp_id]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
hg : S.g = 0
⊢ IsIso h.ι
[PROOFSTEP]
have ⟨φ, hφ⟩ := KernelFork.IsLimit.lift' h.hι' (𝟙 _) (by rw [← cancel_epi h.p, id_comp, p_g', comp_zero, hg])
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
hg : S.g = 0
⊢ 𝟙 h.Q ≫ g' h = 0
[PROOFSTEP]
rw [← cancel_epi h.p, id_comp, p_g', comp_zero, hg]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
hg : S.g = 0
φ : h.Q ⟶ (KernelFork.ofι h.ι (_ : h.ι ≫ g' h = 0)).pt
hφ : φ ≫ Fork.ι (KernelFork.ofι h.ι (_ : h.ι ≫ g' h = 0)) = 𝟙 h.Q
⊢ IsIso h.ι
[PROOFSTEP]
dsimp at hφ
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
hg : S.g = 0
φ : h.Q ⟶ (KernelFork.ofι h.ι (_ : h.ι ≫ g' h = 0)).pt
hφ : φ ≫ h.ι = 𝟙 h.Q
⊢ IsIso h.ι
[PROOFSTEP]
exact ⟨φ, by rw [← cancel_mono h.ι, assoc, hφ, comp_id, id_comp], hφ⟩
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
hg : S.g = 0
φ : h.Q ⟶ (KernelFork.ofι h.ι (_ : h.ι ≫ g' h = 0)).pt
hφ : φ ≫ h.ι = 𝟙 h.Q
⊢ h.ι ≫ φ = 𝟙 h.H
[PROOFSTEP]
rw [← cancel_mono h.ι, assoc, hφ, comp_id, id_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.20229, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
⊢ S.f ≫ 𝟙 S.X₂ = 0
[PROOFSTEP]
rw [comp_id, hf]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.20229, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
⊢ (Iso.refl c.pt).hom ≫ Fork.ι (KernelFork.ofι (Fork.ι c) (_ : Fork.ι c ≫ S.g = 0)) = Fork.ι c
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
⊢ g' (ofIsLimitKernelFork S hf c hc) = S.g
[PROOFSTEP]
rw [← cancel_epi (ofIsLimitKernelFork S hf c hc).p, p_g', ofIsLimitKernelFork_p, id_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.25328, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
⊢ Cofork.π c ≫ (Iso.refl c.pt).hom = Cofork.π (CokernelCofork.ofπ (Cofork.π c) (_ : S.f ≫ Cofork.π c = 0))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.25328, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
⊢ Cofork.π c ≫
      𝟙 c.pt ≫
        IsColimit.desc (IsColimit.ofIsoColimit hc (Cofork.ext (Iso.refl c.pt)))
          (CokernelCofork.ofπ S.g (_ : S.f ≫ S.g = 0)) =
    Cofork.π c ≫ 0
[PROOFSTEP]
simp [hg]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.25328, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
⊢ Cofork.π c ≫
      IsColimit.desc (IsColimit.ofIsoColimit hc (Cofork.ext (Iso.refl c.pt)))
        (CokernelCofork.ofπ S.g (_ : S.f ≫ S.g = 0)) =
    Cofork.π c ≫ 0
[PROOFSTEP]
simp [hg]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
⊢ g' (ofIsColimitCokernelCofork S hg c hc) = 0
[PROOFSTEP]
rw [← cancel_epi (ofIsColimitCokernelCofork S hg c hc).p, p_g', hg, comp_zero]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.30991, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
hf : S.f = 0
hg : S.g = 0
⊢ S.f ≫ 𝟙 S.X₂ = 0
[PROOFSTEP]
rw [comp_id, hf]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.30991, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
hf : S.f = 0
hg : S.g = 0
⊢ 𝟙 S.X₂ ≫ IsColimit.desc (CokernelCofork.IsColimit.ofId S.f hf) (CokernelCofork.ofπ S.g (_ : S.f ≫ S.g = 0)) = 0
[PROOFSTEP]
change 𝟙 _ ≫ S.g = 0
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.30991, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
hf : S.f = 0
hg : S.g = 0
⊢ 𝟙 S.X₂ ≫ S.g = 0
[PROOFSTEP]
simp only [hg, comp_zero]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
hf : S.f = 0
hg : S.g = 0
⊢ g' (ofZeros S hf hg) = 0
[PROOFSTEP]
rw [← cancel_epi ((ofZeros S hf hg).p), comp_zero, p_g', hg]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.57832, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
ψ₁ ψ₂ : RightHomologyMapData φ h₁ h₂
⊢ ψ₁ = ψ₂
[PROOFSTEP]
have hQ : ψ₁.φQ = ψ₂.φQ := by rw [← cancel_epi h₁.p, commp, commp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.57832, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
ψ₁ ψ₂ : RightHomologyMapData φ h₁ h₂
⊢ ψ₁.φQ = ψ₂.φQ
[PROOFSTEP]
rw [← cancel_epi h₁.p, commp, commp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.57832, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
ψ₁ ψ₂ : RightHomologyMapData φ h₁ h₂
hQ : ψ₁.φQ = ψ₂.φQ
⊢ ψ₁ = ψ₂
[PROOFSTEP]
have hH : ψ₁.φH = ψ₂.φH := by rw [← cancel_mono h₂.ι, commι, commι, hQ]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.57832, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
ψ₁ ψ₂ : RightHomologyMapData φ h₁ h₂
hQ : ψ₁.φQ = ψ₂.φQ
⊢ ψ₁.φH = ψ₂.φH
[PROOFSTEP]
rw [← cancel_mono h₂.ι, commι, commι, hQ]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.57832, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
ψ₁ ψ₂ : RightHomologyMapData φ h₁ h₂
hQ : ψ₁.φQ = ψ₂.φQ
hH : ψ₁.φH = ψ₂.φH
⊢ ψ₁ = ψ₂
[PROOFSTEP]
cases ψ₁
[GOAL]
case mk
C : Type u_1
inst✝¹ : Category.{?u.57832, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
ψ₂ : RightHomologyMapData φ h₁ h₂
φQ✝ : h₁.Q ⟶ h₂.Q
φH✝ : h₁.H ⟶ h₂.H
commp✝ : h₁.p ≫ φQ✝ = φ.τ₂ ≫ h₂.p
commg'✝ : φQ✝ ≫ RightHomologyData.g' h₂ = RightHomologyData.g' h₁ ≫ φ.τ₃
commι✝ : φH✝ ≫ h₂.ι = h₁.ι ≫ φQ✝
hQ : (mk φQ✝ φH✝).φQ = ψ₂.φQ
hH : (mk φQ✝ φH✝).φH = ψ₂.φH
⊢ mk φQ✝ φH✝ = ψ₂
[PROOFSTEP]
cases ψ₂
[GOAL]
case mk.mk
C : Type u_1
inst✝¹ : Category.{?u.57832, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
φQ✝¹ : h₁.Q ⟶ h₂.Q
φH✝¹ : h₁.H ⟶ h₂.H
commp✝¹ : h₁.p ≫ φQ✝¹ = φ.τ₂ ≫ h₂.p
commg'✝¹ : φQ✝¹ ≫ RightHomologyData.g' h₂ = RightHomologyData.g' h₁ ≫ φ.τ₃
commι✝¹ : φH✝¹ ≫ h₂.ι = h₁.ι ≫ φQ✝¹
φQ✝ : h₁.Q ⟶ h₂.Q
φH✝ : h₁.H ⟶ h₂.H
commp✝ : h₁.p ≫ φQ✝ = φ.τ₂ ≫ h₂.p
commg'✝ : φQ✝ ≫ RightHomologyData.g' h₂ = RightHomologyData.g' h₁ ≫ φ.τ₃
commι✝ : φH✝ ≫ h₂.ι = h₁.ι ≫ φQ✝
hQ : (mk φQ✝¹ φH✝¹).φQ = (mk φQ✝ φH✝).φQ
hH : (mk φQ✝¹ φH✝¹).φH = (mk φQ✝ φH✝).φH
⊢ mk φQ✝¹ φH✝¹ = mk φQ✝ φH✝
[PROOFSTEP]
congr
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.60291, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
⊢ RightHomologyMapData φ h₁ h₂
[PROOFSTEP]
let φQ : h₁.Q ⟶ h₂.Q := h₁.descQ (φ.τ₂ ≫ h₂.p) (by rw [← φ.comm₁₂_assoc, h₂.wp, comp_zero])
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.60291, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
⊢ S₁.f ≫ φ.τ₂ ≫ h₂.p = 0
[PROOFSTEP]
rw [← φ.comm₁₂_assoc, h₂.wp, comp_zero]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.60291, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
φQ : h₁.Q ⟶ h₂.Q := RightHomologyData.descQ h₁ (φ.τ₂ ≫ h₂.p) (_ : S₁.f ≫ φ.τ₂ ≫ h₂.p = 0)
⊢ RightHomologyMapData φ h₁ h₂
[PROOFSTEP]
have commg' : φQ ≫ h₂.g' = h₁.g' ≫ φ.τ₃ := by
  rw [← cancel_epi h₁.p, RightHomologyData.p_descQ_assoc, assoc, RightHomologyData.p_g', φ.comm₂₃,
    RightHomologyData.p_g'_assoc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.60291, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
φQ : h₁.Q ⟶ h₂.Q := RightHomologyData.descQ h₁ (φ.τ₂ ≫ h₂.p) (_ : S₁.f ≫ φ.τ₂ ≫ h₂.p = 0)
⊢ φQ ≫ RightHomologyData.g' h₂ = RightHomologyData.g' h₁ ≫ φ.τ₃
[PROOFSTEP]
rw [← cancel_epi h₁.p, RightHomologyData.p_descQ_assoc, assoc, RightHomologyData.p_g', φ.comm₂₃,
  RightHomologyData.p_g'_assoc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.60291, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
φQ : h₁.Q ⟶ h₂.Q := RightHomologyData.descQ h₁ (φ.τ₂ ≫ h₂.p) (_ : S₁.f ≫ φ.τ₂ ≫ h₂.p = 0)
commg' : φQ ≫ RightHomologyData.g' h₂ = RightHomologyData.g' h₁ ≫ φ.τ₃
⊢ RightHomologyMapData φ h₁ h₂
[PROOFSTEP]
let φH : h₁.H ⟶ h₂.H := h₂.liftH (h₁.ι ≫ φQ) (by rw [assoc, commg', RightHomologyData.ι_g'_assoc, zero_comp])
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.60291, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
φQ : h₁.Q ⟶ h₂.Q := RightHomologyData.descQ h₁ (φ.τ₂ ≫ h₂.p) (_ : S₁.f ≫ φ.τ₂ ≫ h₂.p = 0)
commg' : φQ ≫ RightHomologyData.g' h₂ = RightHomologyData.g' h₁ ≫ φ.τ₃
⊢ (h₁.ι ≫ φQ) ≫ RightHomologyData.g' h₂ = 0
[PROOFSTEP]
rw [assoc, commg', RightHomologyData.ι_g'_assoc, zero_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.60291, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
φQ : h₁.Q ⟶ h₂.Q := RightHomologyData.descQ h₁ (φ.τ₂ ≫ h₂.p) (_ : S₁.f ≫ φ.τ₂ ≫ h₂.p = 0)
commg' : φQ ≫ RightHomologyData.g' h₂ = RightHomologyData.g' h₁ ≫ φ.τ₃
φH : h₁.H ⟶ h₂.H := RightHomologyData.liftH h₂ (h₁.ι ≫ φQ) (_ : (h₁.ι ≫ φQ) ≫ RightHomologyData.g' h₂ = 0)
⊢ RightHomologyMapData φ h₁ h₂
[PROOFSTEP]
exact ⟨φQ, φH, by simp, commg', by simp⟩
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.60291, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
φQ : h₁.Q ⟶ h₂.Q := RightHomologyData.descQ h₁ (φ.τ₂ ≫ h₂.p) (_ : S₁.f ≫ φ.τ₂ ≫ h₂.p = 0)
commg' : φQ ≫ RightHomologyData.g' h₂ = RightHomologyData.g' h₁ ≫ φ.τ₃
φH : h₁.H ⟶ h₂.H := RightHomologyData.liftH h₂ (h₁.ι ≫ φQ) (_ : (h₁.ι ≫ φQ) ≫ RightHomologyData.g' h₂ = 0)
⊢ h₁.p ≫ φQ = φ.τ₂ ≫ h₂.p
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.60291, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
φQ : h₁.Q ⟶ h₂.Q := RightHomologyData.descQ h₁ (φ.τ₂ ≫ h₂.p) (_ : S₁.f ≫ φ.τ₂ ≫ h₂.p = 0)
commg' : φQ ≫ RightHomologyData.g' h₂ = RightHomologyData.g' h₁ ≫ φ.τ₃
φH : h₁.H ⟶ h₂.H := RightHomologyData.liftH h₂ (h₁.ι ≫ φQ) (_ : (h₁.ι ≫ φQ) ≫ RightHomologyData.g' h₂ = 0)
⊢ φH ≫ h₂.ι = h₁.ι ≫ φQ
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
γ₁ γ₂ : RightHomologyMapData φ h₁ h₂
eq : γ₁ = γ₂
⊢ γ₁.φH = γ₂.φH
[PROOFSTEP]
rw [eq]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
γ₁ γ₂ : RightHomologyMapData φ h₁ h₂
eq : γ₁ = γ₂
⊢ γ₁.φQ = γ₂.φQ
[PROOFSTEP]
rw [eq]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.68471, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ✝ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
c₁ : KernelFork S₁.g
hc₁ : IsLimit c₁
hf₂ : S₂.f = 0
c₂ : KernelFork S₂.g
hc₂ : IsLimit c₂
f : c₁.pt ⟶ c₂.pt
comm : Fork.ι c₁ ≫ φ.τ₂ = f ≫ Fork.ι c₂
⊢ φ.τ₂ ≫ RightHomologyData.g' (RightHomologyData.ofIsLimitKernelFork S₂ hf₂ c₂ hc₂) =
    RightHomologyData.g' (RightHomologyData.ofIsLimitKernelFork S₁ hf₁ c₁ hc₁) ≫ φ.τ₃
[PROOFSTEP]
simp only [RightHomologyData.ofIsLimitKernelFork_g', φ.comm₂₃]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.88776, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : HasRightHomology S
⊢ Epi (pOpcycles S)
[PROOFSTEP]
dsimp only [pOpcycles]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.88776, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : HasRightHomology S
⊢ Epi (rightHomologyData S).p
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝² : Category.{?u.89155, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : HasRightHomology S
⊢ Mono (rightHomologyι S)
[PROOFSTEP]
dsimp only [rightHomologyι]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.89155, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : HasRightHomology S
⊢ Mono (rightHomologyData S).ι
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : HasRightHomology S
A : C
f₁ f₂ : A ⟶ rightHomology S
⊢ f₁ = f₂ ↔ f₁ ≫ rightHomologyι S = f₂ ≫ rightHomologyι S
[PROOFSTEP]
rw [cancel_mono]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : HasRightHomology S
A : C
f₁ f₂ : A ⟶ rightHomology S
h : f₁ ≫ rightHomologyι S = f₂ ≫ rightHomologyι S
⊢ f₁ = f₂
[PROOFSTEP]
simpa only [rightHomology_ext_iff]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : HasRightHomology S
A : C
f₁ f₂ : opcycles S ⟶ A
⊢ f₁ = f₂ ↔ pOpcycles S ≫ f₁ = pOpcycles S ≫ f₂
[PROOFSTEP]
rw [cancel_epi]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : HasRightHomology S
A : C
f₁ f₂ : opcycles S ⟶ A
h : pOpcycles S ≫ f₁ = pOpcycles S ≫ f₂
⊢ f₁ = f₂
[PROOFSTEP]
simpa only [opcycles_ext_iff]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.92901, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : HasRightHomology S
hf : S.f = 0
⊢ opcycles S ≅ S.X₂
[PROOFSTEP]
have := S.isIso_pOpcycles hf
[GOAL]
C : Type u_1
inst✝² : Category.{?u.92901, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : HasRightHomology S
hf : S.f = 0
this : IsIso (pOpcycles S)
⊢ opcycles S ≅ S.X₂
[PROOFSTEP]
exact (asIso S.pOpcycles).symm
[GOAL]
C : Type u_1
inst✝² : Category.{?u.95802, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : HasRightHomology S
hg : S.g = 0
⊢ opcycles S ≅ rightHomology S
[PROOFSTEP]
have := S.isIso_rightHomologyι hg
[GOAL]
C : Type u_1
inst✝² : Category.{?u.95802, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : HasRightHomology S
hg : S.g = 0
this : IsIso (rightHomologyι S)
⊢ opcycles S ≅ rightHomology S
[PROOFSTEP]
exact (asIso S.rightHomologyι).symm
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
⊢ opcyclesMap' φ h₁ h₂ ≫ RightHomologyData.g' h₂ = RightHomologyData.g' h₁ ≫ φ.τ₃
[PROOFSTEP]
simp only [← cancel_epi h₁.p, assoc, φ.comm₂₃, p_opcyclesMap'_assoc, RightHomologyData.p_g'_assoc,
  RightHomologyData.p_g']
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
h₃ : RightHomologyData S₃
⊢ rightHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = rightHomologyMap' φ₁ h₁ h₂ ≫ rightHomologyMap' φ₂ h₂ h₃
[PROOFSTEP]
let γ₁ := rightHomologyMapData φ₁ h₁ h₂
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
h₃ : RightHomologyData S₃
γ₁ : RightHomologyMapData φ₁ h₁ h₂ := rightHomologyMapData φ₁ h₁ h₂
⊢ rightHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = rightHomologyMap' φ₁ h₁ h₂ ≫ rightHomologyMap' φ₂ h₂ h₃
[PROOFSTEP]
let γ₂ := rightHomologyMapData φ₂ h₂ h₃
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
h₃ : RightHomologyData S₃
γ₁ : RightHomologyMapData φ₁ h₁ h₂ := rightHomologyMapData φ₁ h₁ h₂
γ₂ : RightHomologyMapData φ₂ h₂ h₃ := rightHomologyMapData φ₂ h₂ h₃
⊢ rightHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = rightHomologyMap' φ₁ h₁ h₂ ≫ rightHomologyMap' φ₂ h₂ h₃
[PROOFSTEP]
rw [γ₁.rightHomologyMap'_eq, γ₂.rightHomologyMap'_eq, (γ₁.comp γ₂).rightHomologyMap'_eq, RightHomologyMapData.comp_φH]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
h₃ : RightHomologyData S₃
⊢ opcyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = opcyclesMap' φ₁ h₁ h₂ ≫ opcyclesMap' φ₂ h₂ h₃
[PROOFSTEP]
let γ₁ := rightHomologyMapData φ₁ h₁ h₂
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
h₃ : RightHomologyData S₃
γ₁ : RightHomologyMapData φ₁ h₁ h₂ := rightHomologyMapData φ₁ h₁ h₂
⊢ opcyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = opcyclesMap' φ₁ h₁ h₂ ≫ opcyclesMap' φ₂ h₂ h₃
[PROOFSTEP]
let γ₂ := rightHomologyMapData φ₂ h₂ h₃
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ₁ : S₁ ⟶ S₂
φ₂ : S₂ ⟶ S₃
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
h₃ : RightHomologyData S₃
γ₁ : RightHomologyMapData φ₁ h₁ h₂ := rightHomologyMapData φ₁ h₁ h₂
γ₂ : RightHomologyMapData φ₂ h₂ h₃ := rightHomologyMapData φ₂ h₂ h₃
⊢ opcyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = opcyclesMap' φ₁ h₁ h₂ ≫ opcyclesMap' φ₂ h₂ h₃
[PROOFSTEP]
rw [γ₁.opcyclesMap'_eq, γ₂.opcyclesMap'_eq, (γ₁.comp γ₂).opcyclesMap'_eq, RightHomologyMapData.comp_φQ]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.122914, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
e : S₁ ≅ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
⊢ rightHomologyMap' e.hom h₁ h₂ ≫ rightHomologyMap' e.inv h₂ h₁ = 𝟙 h₁.H
[PROOFSTEP]
rw [← rightHomologyMap'_comp, e.hom_inv_id, rightHomologyMap'_id]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.122914, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
e : S₁ ≅ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
⊢ rightHomologyMap' e.inv h₂ h₁ ≫ rightHomologyMap' e.hom h₁ h₂ = 𝟙 h₂.H
[PROOFSTEP]
rw [← rightHomologyMap'_comp, e.inv_hom_id, rightHomologyMap'_id]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.125555, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
e : S₁ ≅ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
⊢ opcyclesMap' e.hom h₁ h₂ ≫ opcyclesMap' e.inv h₂ h₁ = 𝟙 h₁.Q
[PROOFSTEP]
rw [← opcyclesMap'_comp, e.hom_inv_id, opcyclesMap'_id]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.125555, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
e : S₁ ≅ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
⊢ opcyclesMap' e.inv h₂ h₁ ≫ opcyclesMap' e.hom h₁ h₂ = 𝟙 h₂.Q
[PROOFSTEP]
rw [← opcyclesMap'_comp, e.inv_hom_id, opcyclesMap'_id]
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.128180, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
e : S₁ ≅ S₂
inst✝¹ : HasRightHomology S₁
inst✝ : HasRightHomology S₂
⊢ rightHomologyMap e.hom ≫ rightHomologyMap e.inv = 𝟙 (rightHomology S₁)
[PROOFSTEP]
rw [← rightHomologyMap_comp, e.hom_inv_id, rightHomologyMap_id]
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.128180, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
e : S₁ ≅ S₂
inst✝¹ : HasRightHomology S₁
inst✝ : HasRightHomology S₂
⊢ rightHomologyMap e.inv ≫ rightHomologyMap e.hom = 𝟙 (rightHomology S₂)
[PROOFSTEP]
rw [← rightHomologyMap_comp, e.inv_hom_id, rightHomologyMap_id]
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.131838, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
e : S₁ ≅ S₂
inst✝¹ : HasRightHomology S₁
inst✝ : HasRightHomology S₂
⊢ opcyclesMap e.hom ≫ opcyclesMap e.inv = 𝟙 (opcycles S₁)
[PROOFSTEP]
rw [← opcyclesMap_comp, e.hom_inv_id, opcyclesMap_id]
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.131838, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
e : S₁ ≅ S₂
inst✝¹ : HasRightHomology S₁
inst✝ : HasRightHomology S₂
⊢ opcyclesMap e.inv ≫ opcyclesMap e.hom = 𝟙 (opcycles S₂)
[PROOFSTEP]
rw [← opcyclesMap_comp, e.inv_hom_id, opcyclesMap_id]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
inst✝ : HasRightHomology S
⊢ h.p ≫ (opcyclesIso h).inv = pOpcycles S
[PROOFSTEP]
dsimp [pOpcycles, RightHomologyData.opcyclesIso]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
inst✝ : HasRightHomology S
⊢ h.p ≫ opcyclesMap' (𝟙 S) h (rightHomologyData S) = (rightHomologyData S).p
[PROOFSTEP]
simp only [p_opcyclesMap', id_τ₂, id_comp]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
inst✝ : HasRightHomology S
⊢ pOpcycles S ≫ (opcyclesIso h).hom = h.p
[PROOFSTEP]
simp only [← h.p_comp_opcyclesIso_inv, assoc, Iso.inv_hom_id, comp_id]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
inst✝ : HasRightHomology S
⊢ (rightHomologyIso h).inv ≫ rightHomologyι S = h.ι ≫ (opcyclesIso h).inv
[PROOFSTEP]
dsimp only [rightHomologyι, rightHomologyIso, opcyclesIso, rightHomologyMapIso', opcyclesMapIso', Iso.refl]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
inst✝ : HasRightHomology S
⊢ rightHomologyMap' (𝟙 S) h (rightHomologyData S) ≫ (rightHomologyData S).ι =
    h.ι ≫ opcyclesMap' (𝟙 S) h (rightHomologyData S)
[PROOFSTEP]
rw [rightHomologyι_naturality']
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
inst✝ : HasRightHomology S
⊢ (rightHomologyIso h).hom ≫ h.ι = rightHomologyι S ≫ (opcyclesIso h).hom
[PROOFSTEP]
simp only [← cancel_mono h.opcyclesIso.inv, ← cancel_epi h.rightHomologyIso.inv, assoc, Iso.inv_hom_id_assoc,
  Iso.hom_inv_id, comp_id, rightHomologyIso_inv_comp_rightHomologyι]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : HasRightHomology S₁
inst✝ : HasRightHomology S₂
⊢ rightHomologyMap φ = (RightHomologyData.rightHomologyIso h₁).hom ≫ γ.φH ≫ (RightHomologyData.rightHomologyIso h₂).inv
[PROOFSTEP]
dsimp [RightHomologyData.rightHomologyIso, rightHomologyMapIso']
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : HasRightHomology S₁
inst✝ : HasRightHomology S₂
⊢ rightHomologyMap φ =
    rightHomologyMap' (𝟙 S₁) (rightHomologyData S₁) h₁ ≫ γ.φH ≫ rightHomologyMap' (𝟙 S₂) h₂ (rightHomologyData S₂)
[PROOFSTEP]
rw [← γ.rightHomologyMap'_eq, ← rightHomologyMap'_comp, ← rightHomologyMap'_comp, id_comp, comp_id]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : HasRightHomology S₁
inst✝ : HasRightHomology S₂
⊢ rightHomologyMap φ = rightHomologyMap' φ (rightHomologyData S₁) (rightHomologyData S₂)
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : HasRightHomology S₁
inst✝ : HasRightHomology S₂
⊢ opcyclesMap φ = (RightHomologyData.opcyclesIso h₁).hom ≫ γ.φQ ≫ (RightHomologyData.opcyclesIso h₂).inv
[PROOFSTEP]
dsimp [RightHomologyData.opcyclesIso, cyclesMapIso']
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : HasRightHomology S₁
inst✝ : HasRightHomology S₂
⊢ opcyclesMap φ = opcyclesMap' (𝟙 S₁) (rightHomologyData S₁) h₁ ≫ γ.φQ ≫ opcyclesMap' (𝟙 S₂) h₂ (rightHomologyData S₂)
[PROOFSTEP]
rw [← γ.opcyclesMap'_eq, ← opcyclesMap'_comp, ← opcyclesMap'_comp, id_comp, comp_id]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : HasRightHomology S₁
inst✝ : HasRightHomology S₂
⊢ opcyclesMap φ = opcyclesMap' φ (rightHomologyData S₁) (rightHomologyData S₂)
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : HasRightHomology S₁
inst✝ : HasRightHomology S₂
⊢ rightHomologyMap φ ≫ (RightHomologyData.rightHomologyIso h₂).hom = (RightHomologyData.rightHomologyIso h₁).hom ≫ γ.φH
[PROOFSTEP]
simp only [γ.rightHomologyMap_eq, assoc, Iso.inv_hom_id, comp_id]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : HasRightHomology S₁
inst✝ : HasRightHomology S₂
⊢ opcyclesMap φ ≫ (RightHomologyData.opcyclesIso h₂).hom = (RightHomologyData.opcyclesIso h₁).hom ≫ γ.φQ
[PROOFSTEP]
simp only [γ.opcyclesMap_eq, assoc, Iso.inv_hom_id, comp_id]
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.155614, u_1} C
inst✝ : HasZeroMorphisms C
S S₁✝ S₂✝ S₃ S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : LeftHomologyData S₁
h₂ : LeftHomologyData S₂
ψ : LeftHomologyMapData φ h₁ h₂
⊢ ((LeftHomologyData.op h₂).p ≫ ψ.φK.op).unop = ((opMap φ).τ₂ ≫ (LeftHomologyData.op h₁).p).unop
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.155614, u_1} C
inst✝ : HasZeroMorphisms C
S S₁✝ S₂✝ S₃ S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : LeftHomologyData S₁
h₂ : LeftHomologyData S₂
ψ : LeftHomologyMapData φ h₁ h₂
⊢ (ψ.φK.op ≫ RightHomologyData.g' (LeftHomologyData.op h₁)).unop =
    (RightHomologyData.g' (LeftHomologyData.op h₂) ≫ (opMap φ).τ₃).unop
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.155614, u_1} C
inst✝ : HasZeroMorphisms C
S S₁✝ S₂✝ S₃ S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : LeftHomologyData S₁
h₂ : LeftHomologyData S₂
ψ : LeftHomologyMapData φ h₁ h₂
⊢ (ψ.φH.op ≫ (LeftHomologyData.op h₁).ι).unop = ((LeftHomologyData.op h₂).ι ≫ ψ.φK.op).unop
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.158318, u_1} C
inst✝ : HasZeroMorphisms C
S S₁✝ S₂✝ S₃ : ShortComplex C
S₁ S₂ : ShortComplex Cᵒᵖ
φ : S₁ ⟶ S₂
h₁ : LeftHomologyData S₁
h₂ : LeftHomologyData S₂
ψ : LeftHomologyMapData φ h₁ h₂
⊢ ((LeftHomologyData.unop h₂).p ≫ ψ.φK.unop).op = ((unopMap φ).τ₂ ≫ (LeftHomologyData.unop h₁).p).op
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.158318, u_1} C
inst✝ : HasZeroMorphisms C
S S₁✝ S₂✝ S₃ : ShortComplex C
S₁ S₂ : ShortComplex Cᵒᵖ
φ : S₁ ⟶ S₂
h₁ : LeftHomologyData S₁
h₂ : LeftHomologyData S₂
ψ : LeftHomologyMapData φ h₁ h₂
⊢ (ψ.φK.unop ≫ RightHomologyData.g' (LeftHomologyData.unop h₁)).op =
    (RightHomologyData.g' (LeftHomologyData.unop h₂) ≫ (unopMap φ).τ₃).op
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.158318, u_1} C
inst✝ : HasZeroMorphisms C
S S₁✝ S₂✝ S₃ : ShortComplex C
S₁ S₂ : ShortComplex Cᵒᵖ
φ : S₁ ⟶ S₂
h₁ : LeftHomologyData S₁
h₂ : LeftHomologyData S₂
ψ : LeftHomologyMapData φ h₁ h₂
⊢ (ψ.φH.unop ≫ (LeftHomologyData.unop h₁).ι).op = ((LeftHomologyData.unop h₂).ι ≫ ψ.φK.unop).op
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.160823, u_1} C
inst✝ : HasZeroMorphisms C
S S₁✝ S₂✝ S₃ S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
ψ : RightHomologyMapData φ h₁ h₂
⊢ (ψ.φQ.op ≫ (RightHomologyData.op h₁).i).unop = ((RightHomologyData.op h₂).i ≫ (opMap φ).τ₂).unop
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.160823, u_1} C
inst✝ : HasZeroMorphisms C
S S₁✝ S₂✝ S₃ S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
ψ : RightHomologyMapData φ h₁ h₂
⊢ (LeftHomologyData.f' (RightHomologyData.op h₂) ≫ ψ.φQ.op).unop =
    ((opMap φ).τ₁ ≫ LeftHomologyData.f' (RightHomologyData.op h₁)).unop
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.160823, u_1} C
inst✝ : HasZeroMorphisms C
S S₁✝ S₂✝ S₃ S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
ψ : RightHomologyMapData φ h₁ h₂
⊢ ((RightHomologyData.op h₂).π ≫ ψ.φH.op).unop = (ψ.φQ.op ≫ (RightHomologyData.op h₁).π).unop
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.163518, u_1} C
inst✝ : HasZeroMorphisms C
S S₁✝ S₂✝ S₃ : ShortComplex C
S₁ S₂ : ShortComplex Cᵒᵖ
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
ψ : RightHomologyMapData φ h₁ h₂
⊢ (ψ.φQ.unop ≫ (RightHomologyData.unop h₁).i).op = ((RightHomologyData.unop h₂).i ≫ (unopMap φ).τ₂).op
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.163518, u_1} C
inst✝ : HasZeroMorphisms C
S S₁✝ S₂✝ S₃ : ShortComplex C
S₁ S₂ : ShortComplex Cᵒᵖ
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
ψ : RightHomologyMapData φ h₁ h₂
⊢ (LeftHomologyData.f' (RightHomologyData.unop h₂) ≫ ψ.φQ.unop).op =
    ((unopMap φ).τ₁ ≫ LeftHomologyData.f' (RightHomologyData.unop h₁)).op
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.163518, u_1} C
inst✝ : HasZeroMorphisms C
S S₁✝ S₂✝ S₃ : ShortComplex C
S₁ S₂ : ShortComplex Cᵒᵖ
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
ψ : RightHomologyMapData φ h₁ h₂
⊢ ((RightHomologyData.unop h₂).π ≫ ψ.φH.unop).op = (ψ.φQ.unop ≫ (RightHomologyData.unop h₁).π).op
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : LeftHomologyData S₁
h₂ : LeftHomologyData S₂
⊢ (leftHomologyMap' φ h₁ h₂).op = rightHomologyMap' (opMap φ) (LeftHomologyData.op h₂) (LeftHomologyData.op h₁)
[PROOFSTEP]
let γ : LeftHomologyMapData φ h₁ h₂ := leftHomologyMapData φ h₁ h₂
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : LeftHomologyData S₁
h₂ : LeftHomologyData S₂
γ : LeftHomologyMapData φ h₁ h₂ := leftHomologyMapData φ h₁ h₂
⊢ (leftHomologyMap' φ h₁ h₂).op = rightHomologyMap' (opMap φ) (LeftHomologyData.op h₂) (LeftHomologyData.op h₁)
[PROOFSTEP]
simp only [γ.leftHomologyMap'_eq, γ.op.rightHomologyMap'_eq, LeftHomologyMapData.op_φH]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : HasLeftHomology S₁
inst✝ : HasLeftHomology S₂
⊢ (leftHomologyMap φ).op = (rightHomologyOpIso S₂).inv ≫ rightHomologyMap (opMap φ) ≫ (rightHomologyOpIso S₁).hom
[PROOFSTEP]
dsimp [rightHomologyOpIso, RightHomologyData.rightHomologyIso, rightHomologyMap, leftHomologyMap]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : HasLeftHomology S₁
inst✝ : HasLeftHomology S₂
⊢ (leftHomologyMap' φ (leftHomologyData S₁) (leftHomologyData S₂)).op =
    rightHomologyMap' (𝟙 (op S₂)) (LeftHomologyData.op (leftHomologyData S₂)) (rightHomologyData (op S₂)) ≫
      rightHomologyMap' (opMap φ) (rightHomologyData (op S₂)) (rightHomologyData (op S₁)) ≫
        rightHomologyMap' (𝟙 (op S₁)) (rightHomologyData (op S₁)) (LeftHomologyData.op (leftHomologyData S₁))
[PROOFSTEP]
simp only [← rightHomologyMap'_comp, comp_id, id_comp, leftHomologyMap'_op]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
⊢ (rightHomologyMap' φ h₁ h₂).op = leftHomologyMap' (opMap φ) (RightHomologyData.op h₂) (RightHomologyData.op h₁)
[PROOFSTEP]
let γ : RightHomologyMapData φ h₁ h₂ := rightHomologyMapData φ h₁ h₂
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
γ : RightHomologyMapData φ h₁ h₂ := rightHomologyMapData φ h₁ h₂
⊢ (rightHomologyMap' φ h₁ h₂).op = leftHomologyMap' (opMap φ) (RightHomologyData.op h₂) (RightHomologyData.op h₁)
[PROOFSTEP]
simp only [γ.rightHomologyMap'_eq, γ.op.leftHomologyMap'_eq, RightHomologyMapData.op_φH]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : HasRightHomology S₁
inst✝ : HasRightHomology S₂
⊢ (rightHomologyMap φ).op = (leftHomologyOpIso S₂).inv ≫ leftHomologyMap (opMap φ) ≫ (leftHomologyOpIso S₁).hom
[PROOFSTEP]
dsimp [leftHomologyOpIso, LeftHomologyData.leftHomologyIso, leftHomologyMap, rightHomologyMap]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : HasRightHomology S₁
inst✝ : HasRightHomology S₂
⊢ (rightHomologyMap' φ (rightHomologyData S₁) (rightHomologyData S₂)).op =
    leftHomologyMap' (𝟙 (op S₂)) (RightHomologyData.op (rightHomologyData S₂)) (leftHomologyData (op S₂)) ≫
      leftHomologyMap' (opMap φ) (leftHomologyData (op S₂)) (leftHomologyData (op S₁)) ≫
        leftHomologyMap' (𝟙 (op S₁)) (leftHomologyData (op S₁)) (RightHomologyData.op (rightHomologyData S₁))
[PROOFSTEP]
simp only [← leftHomologyMap'_comp, comp_id, id_comp, rightHomologyMap'_op]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.173881, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : RightHomologyData S₁
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ RightHomologyData S₂
[PROOFSTEP]
haveI : Epi (opMap φ).τ₁ := by dsimp; infer_instance
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.173881, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : RightHomologyData S₁
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ Epi (opMap φ).τ₁
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.173881, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : RightHomologyData S₁
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ Epi φ.τ₃.op
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.173881, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : RightHomologyData S₁
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
this : Epi (opMap φ).τ₁
⊢ RightHomologyData S₂
[PROOFSTEP]
haveI : IsIso (opMap φ).τ₂ := by dsimp; infer_instance
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.173881, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : RightHomologyData S₁
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
this : Epi (opMap φ).τ₁
⊢ IsIso (opMap φ).τ₂
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.173881, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : RightHomologyData S₁
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
this : Epi (opMap φ).τ₁
⊢ IsIso φ.τ₂.op
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.173881, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : RightHomologyData S₁
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
this✝ : Epi (opMap φ).τ₁
this : IsIso (opMap φ).τ₂
⊢ RightHomologyData S₂
[PROOFSTEP]
haveI : Mono (opMap φ).τ₃ := by dsimp; infer_instance
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.173881, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : RightHomologyData S₁
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
this✝ : Epi (opMap φ).τ₁
this : IsIso (opMap φ).τ₂
⊢ Mono (opMap φ).τ₃
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.173881, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : RightHomologyData S₁
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
this✝ : Epi (opMap φ).τ₁
this : IsIso (opMap φ).τ₂
⊢ Mono φ.τ₁.op
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.173881, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : RightHomologyData S₁
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
this✝¹ : Epi (opMap φ).τ₁
this✝ : IsIso (opMap φ).τ₂
this : Mono (opMap φ).τ₃
⊢ RightHomologyData S₂
[PROOFSTEP]
exact (LeftHomologyData.ofEpiOfIsIsoOfMono' (opMap φ) h.op).unop
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : RightHomologyData S₁
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ (ofEpiOfIsIsoOfMono φ h).p = inv φ.τ₂ ≫ h.p
[PROOFSTEP]
simp [ofEpiOfIsIsoOfMono, opMap]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : RightHomologyData S₁
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ g' (ofEpiOfIsIsoOfMono φ h) = g' h ≫ φ.τ₃
[PROOFSTEP]
simp [ofEpiOfIsIsoOfMono, opMap]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.184271, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : RightHomologyData S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ RightHomologyData S₁
[PROOFSTEP]
haveI : Epi (opMap φ).τ₁ := by dsimp; infer_instance
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.184271, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : RightHomologyData S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ Epi (opMap φ).τ₁
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.184271, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : RightHomologyData S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ Epi φ.τ₃.op
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.184271, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : RightHomologyData S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
this : Epi (opMap φ).τ₁
⊢ RightHomologyData S₁
[PROOFSTEP]
haveI : IsIso (opMap φ).τ₂ := by dsimp; infer_instance
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.184271, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : RightHomologyData S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
this : Epi (opMap φ).τ₁
⊢ IsIso (opMap φ).τ₂
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.184271, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : RightHomologyData S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
this : Epi (opMap φ).τ₁
⊢ IsIso φ.τ₂.op
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.184271, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : RightHomologyData S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
this✝ : Epi (opMap φ).τ₁
this : IsIso (opMap φ).τ₂
⊢ RightHomologyData S₁
[PROOFSTEP]
haveI : Mono (opMap φ).τ₃ := by dsimp; infer_instance
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.184271, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : RightHomologyData S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
this✝ : Epi (opMap φ).τ₁
this : IsIso (opMap φ).τ₂
⊢ Mono (opMap φ).τ₃
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.184271, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : RightHomologyData S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
this✝ : Epi (opMap φ).τ₁
this : IsIso (opMap φ).τ₂
⊢ Mono φ.τ₁.op
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.184271, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : RightHomologyData S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
this✝¹ : Epi (opMap φ).τ₁
this✝ : IsIso (opMap φ).τ₂
this : Mono (opMap φ).τ₃
⊢ RightHomologyData S₁
[PROOFSTEP]
exact (LeftHomologyData.ofEpiOfIsIsoOfMono (opMap φ) h.op).unop
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : RightHomologyData S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ (ofEpiOfIsIsoOfMono' φ h).p = φ.τ₂ ≫ h.p
[PROOFSTEP]
simp [ofEpiOfIsIsoOfMono', opMap]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : RightHomologyData S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ g' (ofEpiOfIsIsoOfMono' φ h) ≫ φ.τ₃ = g' h
[PROOFSTEP]
rw [← cancel_epi (ofEpiOfIsIsoOfMono' φ h).p, p_g'_assoc, ofEpiOfIsIsoOfMono'_p, assoc, p_g', φ.comm₂₃]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.203472, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ IsIso (rightHomologyMap' φ h₁ h₂)
[PROOFSTEP]
let h₂' := RightHomologyData.ofEpiOfIsIsoOfMono φ h₁
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.203472, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
h₂' : RightHomologyData S₂ := RightHomologyData.ofEpiOfIsIsoOfMono φ h₁
⊢ IsIso (rightHomologyMap' φ h₁ h₂)
[PROOFSTEP]
haveI : IsIso (rightHomologyMap' φ h₁ h₂') :=
  by
  rw [(RightHomologyMapData.ofEpiOfIsIsoOfMono φ h₁).rightHomologyMap'_eq]
  dsimp
  infer_instance
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.203472, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
h₂' : RightHomologyData S₂ := RightHomologyData.ofEpiOfIsIsoOfMono φ h₁
⊢ IsIso (rightHomologyMap' φ h₁ h₂')
[PROOFSTEP]
rw [(RightHomologyMapData.ofEpiOfIsIsoOfMono φ h₁).rightHomologyMap'_eq]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.203472, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
h₂' : RightHomologyData S₂ := RightHomologyData.ofEpiOfIsIsoOfMono φ h₁
⊢ IsIso (RightHomologyMapData.ofEpiOfIsIsoOfMono φ h₁).φH
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.203472, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
h₂' : RightHomologyData S₂ := RightHomologyData.ofEpiOfIsIsoOfMono φ h₁
⊢ IsIso (𝟙 h₁.H)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.203472, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
h₂' : RightHomologyData S₂ := RightHomologyData.ofEpiOfIsIsoOfMono φ h₁
this : IsIso (rightHomologyMap' φ h₁ h₂')
⊢ IsIso (rightHomologyMap' φ h₁ h₂)
[PROOFSTEP]
have eq := rightHomologyMap'_comp φ (𝟙 S₂) h₁ h₂' h₂
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.203472, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
h₂' : RightHomologyData S₂ := RightHomologyData.ofEpiOfIsIsoOfMono φ h₁
this : IsIso (rightHomologyMap' φ h₁ h₂')
eq : rightHomologyMap' (φ ≫ 𝟙 S₂) h₁ h₂ = rightHomologyMap' φ h₁ h₂' ≫ rightHomologyMap' (𝟙 S₂) h₂' h₂
⊢ IsIso (rightHomologyMap' φ h₁ h₂)
[PROOFSTEP]
rw [comp_id] at eq
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.203472, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
h₂' : RightHomologyData S₂ := RightHomologyData.ofEpiOfIsIsoOfMono φ h₁
this : IsIso (rightHomologyMap' φ h₁ h₂')
eq : rightHomologyMap' φ h₁ h₂ = rightHomologyMap' φ h₁ h₂' ≫ rightHomologyMap' (𝟙 S₂) h₂' h₂
⊢ IsIso (rightHomologyMap' φ h₁ h₂)
[PROOFSTEP]
rw [eq]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.203472, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
h₂' : RightHomologyData S₂ := RightHomologyData.ofEpiOfIsIsoOfMono φ h₁
this : IsIso (rightHomologyMap' φ h₁ h₂')
eq : rightHomologyMap' φ h₁ h₂ = rightHomologyMap' φ h₁ h₂' ≫ rightHomologyMap' (𝟙 S₂) h₂' h₂
⊢ IsIso (rightHomologyMap' φ h₁ h₂' ≫ rightHomologyMap' (𝟙 S₂) h₂' h₂)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝⁶ : Category.{?u.205342, u_1} C
inst✝⁵ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝⁴ : HasRightHomology S₁
inst✝³ : HasRightHomology S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ IsIso (rightHomologyMap φ)
[PROOFSTEP]
dsimp only [rightHomologyMap]
[GOAL]
C : Type u_1
inst✝⁶ : Category.{?u.205342, u_1} C
inst✝⁵ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝⁴ : HasRightHomology S₁
inst✝³ : HasRightHomology S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ IsIso (rightHomologyMap' φ (rightHomologyData S₁) (rightHomologyData S₂))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝⁵ : Category.{?u.207199, u_1} C
inst✝⁴ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : HasKernels Cᵒᵖ
inst✝ : HasCokernels Cᵒᵖ
⊢ ∀ {X Y : (ShortComplex C)ᵒᵖ} (f : X ⟶ Y),
    (rightHomologyFunctor C).op.map f ≫ ((fun S => (leftHomologyOpIso S.unop).symm) Y).hom =
      ((fun S => (leftHomologyOpIso S.unop).symm) X).hom ≫ (opFunctor C ⋙ leftHomologyFunctor Cᵒᵖ).map f
[PROOFSTEP]
simp [rightHomologyMap_op]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{?u.214499, u_1} C
inst✝⁴ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : HasKernels Cᵒᵖ
inst✝ : HasCokernels Cᵒᵖ
⊢ ∀ {X Y : (ShortComplex C)ᵒᵖ} (f : X ⟶ Y),
    (leftHomologyFunctor C).op.map f ≫ ((fun S => (rightHomologyOpIso S.unop).symm) Y).hom =
      ((fun S => (rightHomologyOpIso S.unop).symm) X).hom ≫ (opFunctor C ⋙ rightHomologyFunctor Cᵒᵖ).map f
[PROOFSTEP]
simp [leftHomologyMap_op]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.224277, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝ : HasRightHomology S
A' : C
α : A ⟶ A'
⊢ S.f ≫ k ≫ α = 0
[PROOFSTEP]
rw [reassoc_of% hk, zero_comp]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝ : HasRightHomology S
A' : C
α : A ⟶ A'
⊢ descOpcycles S k hk ≫ α = descOpcycles S (k ≫ α) (_ : S.f ≫ k ≫ α = 0)
[PROOFSTEP]
simp only [← cancel_epi S.pOpcycles, p_descOpcycles_assoc, p_descOpcycles]
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.227378, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝¹ : HasRightHomology S
inst✝ : HasCokernel S.f
⊢ S.f ≫ cokernel.π S.f = 0
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.227378, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝¹ : HasRightHomology S
inst✝ : HasCokernel S.f
⊢ S.f ≫ pOpcycles S = 0
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝² : Category.{?u.231633, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝ : HasRightHomology S
x : S.X₃ ⟶ A
hx : k = S.g ≫ x
⊢ S.f ≫ k = 0
[PROOFSTEP]
rw [hx, S.zero_assoc, zero_comp]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝ : HasRightHomology S
⊢ S.g = S.g ≫ 𝟙 S.X₃
[PROOFSTEP]
rw [comp_id]
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.236265, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝¹ : HasRightHomology S
φ : S₁ ⟶ S
inst✝ : HasRightHomology S₁
⊢ S₁.f ≫ φ.τ₂ ≫ k = 0
[PROOFSTEP]
rw [← φ.comm₁₂_assoc, hk, comp_zero]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝¹ : HasRightHomology S
φ : S₁ ⟶ S
inst✝ : HasRightHomology S₁
⊢ opcyclesMap φ ≫ descOpcycles S k hk = descOpcycles S₁ (φ.τ₂ ≫ k) (_ : S₁.f ≫ φ.τ₂ ≫ k = 0)
[PROOFSTEP]
simp only [← cancel_epi (S₁.pOpcycles), p_opcyclesMap_assoc, p_descOpcycles]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝ : HasRightHomology S
⊢ (opcyclesIso h).inv ≫ descOpcycles S k hk = descQ h k hk
[PROOFSTEP]
simp only [← cancel_epi h.p, p_comp_opcyclesIso_inv_assoc, p_descOpcycles, p_descQ]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : RightHomologyData S
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝ : HasRightHomology S
⊢ (opcyclesIso h).hom ≫ descQ h k hk = descOpcycles S k hk
[PROOFSTEP]
rw [← h.opcyclesIso_inv_comp_descOpcycles, Iso.hom_inv_id_assoc]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝¹ : HasRightHomology S
inst✝ : HasCokernel S.f
⊢ HasKernel (cokernel.desc S.f S.g (_ : S.f ≫ S.g = 0))
[PROOFSTEP]
let h := S.rightHomologyData
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝¹ : HasRightHomology S
inst✝ : HasCokernel S.f
h : RightHomologyData S := rightHomologyData S
⊢ HasKernel (cokernel.desc S.f S.g (_ : S.f ≫ S.g = 0))
[PROOFSTEP]
haveI : HasLimit (parallelPair h.g' 0) := ⟨⟨⟨_, h.hι'⟩⟩⟩
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝¹ : HasRightHomology S
inst✝ : HasCokernel S.f
h : RightHomologyData S := rightHomologyData S
this : HasLimit (parallelPair (RightHomologyData.g' h) 0)
⊢ HasKernel (cokernel.desc S.f S.g (_ : S.f ≫ S.g = 0))
[PROOFSTEP]
let e : parallelPair (cokernel.desc S.f S.g S.zero) 0 ≅ parallelPair h.g' 0 :=
  parallelPair.ext (IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) h.hp) (Iso.refl _)
    (coequalizer.hom_ext (by simp)) (by aesop_cat)
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝¹ : HasRightHomology S
inst✝ : HasCokernel S.f
h : RightHomologyData S := rightHomologyData S
this : HasLimit (parallelPair (RightHomologyData.g' h) 0)
⊢ coequalizer.π S.f 0 ≫
      (parallelPair (cokernel.desc S.f S.g (_ : S.f ≫ S.g = 0)) 0).map WalkingParallelPairHom.left ≫
        (Iso.refl ((parallelPair (cokernel.desc S.f S.g (_ : S.f ≫ S.g = 0)) 0).obj WalkingParallelPair.one)).hom =
    coequalizer.π S.f 0 ≫
      (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (parallelPair S.f 0)) h.hp).hom ≫
        (parallelPair (RightHomologyData.g' h) 0).map WalkingParallelPairHom.left
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝¹ : HasRightHomology S
inst✝ : HasCokernel S.f
h : RightHomologyData S := rightHomologyData S
this : HasLimit (parallelPair (RightHomologyData.g' h) 0)
⊢ (parallelPair (cokernel.desc S.f S.g (_ : S.f ≫ S.g = 0)) 0).map WalkingParallelPairHom.right ≫
      (Iso.refl ((parallelPair (cokernel.desc S.f S.g (_ : S.f ≫ S.g = 0)) 0).obj WalkingParallelPair.one)).hom =
    (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (parallelPair S.f 0)) h.hp).hom ≫
      (parallelPair (RightHomologyData.g' h) 0).map WalkingParallelPairHom.right
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝¹ : HasRightHomology S
inst✝ : HasCokernel S.f
h : RightHomologyData S := rightHomologyData S
this : HasLimit (parallelPair (RightHomologyData.g' h) 0)
e : parallelPair (cokernel.desc S.f S.g (_ : S.f ≫ S.g = 0)) 0 ≅ parallelPair (RightHomologyData.g' h) 0 :=
  parallelPair.ext (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (parallelPair S.f 0)) h.hp)
    (Iso.refl ((parallelPair (cokernel.desc S.f S.g (_ : S.f ≫ S.g = 0)) 0).obj WalkingParallelPair.one))
    (_ :
      (parallelPair (cokernel.desc S.f S.g (_ : S.f ≫ S.g = 0)) 0).map WalkingParallelPairHom.left ≫
          (Iso.refl ((parallelPair (cokernel.desc S.f S.g (_ : S.f ≫ S.g = 0)) 0).obj WalkingParallelPair.one)).hom =
        (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (parallelPair S.f 0)) h.hp).hom ≫
          (parallelPair (RightHomologyData.g' h) 0).map WalkingParallelPairHom.left)
    (_ :
      0 ≫ 𝟙 S.X₃ =
        (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (parallelPair S.f 0)) (rightHomologyData S).hp).hom ≫ 0)
⊢ HasKernel (cokernel.desc S.f S.g (_ : S.f ≫ S.g = 0))
[PROOFSTEP]
exact hasLimitOfIso e.symm
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₂✝ : IsIso φ.τ₂
h₁✝ : Epi φ.τ₁
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
⊢ IsIso (opcyclesMap' φ h₁ h₂)
[PROOFSTEP]
refine' ⟨h₂.descQ (inv φ.τ₂ ≫ h₁.p) _, _, _⟩
[GOAL]
case refine'_1
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₂✝ : IsIso φ.τ₂
h₁✝ : Epi φ.τ₁
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
⊢ S₂.f ≫ inv φ.τ₂ ≫ h₁.p = 0
[PROOFSTEP]
simp only [← cancel_epi φ.τ₁, comp_zero, φ.comm₁₂_assoc, IsIso.hom_inv_id_assoc, h₁.wp]
[GOAL]
case refine'_2
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₂✝ : IsIso φ.τ₂
h₁✝ : Epi φ.τ₁
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
⊢ opcyclesMap' φ h₁ h₂ ≫ RightHomologyData.descQ h₂ (inv φ.τ₂ ≫ h₁.p) (_ : S₂.f ≫ inv φ.τ₂ ≫ h₁.p = 0) = 𝟙 h₁.Q
[PROOFSTEP]
simp only [← cancel_epi h₁.p, p_opcyclesMap'_assoc, h₂.p_descQ, IsIso.hom_inv_id_assoc, comp_id]
[GOAL]
case refine'_3
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₂✝ : IsIso φ.τ₂
h₁✝ : Epi φ.τ₁
h₁ : RightHomologyData S₁
h₂ : RightHomologyData S₂
⊢ RightHomologyData.descQ h₂ (inv φ.τ₂ ≫ h₁.p) (_ : S₂.f ≫ inv φ.τ₂ ≫ h₁.p = 0) ≫ opcyclesMap' φ h₁ h₂ = 𝟙 h₂.Q
[PROOFSTEP]
simp only [← cancel_epi h₂.p, h₂.p_descQ_assoc, assoc, p_opcyclesMap', IsIso.inv_hom_id_assoc, comp_id]