[GOAL]
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
h : ShortExact f g
h' : ShortExact f' g'
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
⊢ IsIso i₂
[PROOFSTEP]
obtain ⟨_⟩ := h
[GOAL]
case mk
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
h' : ShortExact f' g'
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝ : Mono f
epi✝ : Epi g
exact✝ : Exact f g
⊢ IsIso i₂
[PROOFSTEP]
obtain ⟨_⟩ := h'
[GOAL]
case mk.mk
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ IsIso i₂
[PROOFSTEP]
refine
  @Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono 𝒜 _ _ 0 _ _ _ 0 _ _ _ 0 f g 0 f' g' 0 i₁ i₂ i₃ ?_ comm₁ comm₂ 0 0 0 0
    0 ?_ ?_ ?_ ?_ ?_ ?_ ?_ _ _ _ _
[GOAL]
case mk.mk.refine_1
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ 0 ≫ 0 = 0 ≫ i₁
case mk.mk.refine_2
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ i₃ ≫ 0 = 0 ≫ 0
case mk.mk.refine_3
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact 0 f
case mk.mk.refine_4
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact f g
case mk.mk.refine_5
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact g 0
case mk.mk.refine_6
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact 0 f'
case mk.mk.refine_7
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact f' g'
case mk.mk.refine_8
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact g' 0
[PROOFSTEP]
all_goals try simp
[GOAL]
case mk.mk.refine_1
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ 0 ≫ 0 = 0 ≫ i₁
[PROOFSTEP]
try simp
[GOAL]
case mk.mk.refine_1
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ 0 ≫ 0 = 0 ≫ i₁
[PROOFSTEP]
simp
[GOAL]
case mk.mk.refine_2
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ i₃ ≫ 0 = 0 ≫ 0
[PROOFSTEP]
try simp
[GOAL]
case mk.mk.refine_2
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ i₃ ≫ 0 = 0 ≫ 0
[PROOFSTEP]
simp
[GOAL]
case mk.mk.refine_3
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact 0 f
[PROOFSTEP]
try simp
[GOAL]
case mk.mk.refine_3
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact 0 f
[PROOFSTEP]
simp
[GOAL]
case mk.mk.refine_4
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact f g
[PROOFSTEP]
try simp
[GOAL]
case mk.mk.refine_4
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact f g
[PROOFSTEP]
simp
[GOAL]
case mk.mk.refine_5
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact g 0
[PROOFSTEP]
try simp
[GOAL]
case mk.mk.refine_5
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact g 0
[PROOFSTEP]
simp
[GOAL]
case mk.mk.refine_6
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact 0 f'
[PROOFSTEP]
try simp
[GOAL]
case mk.mk.refine_6
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact 0 f'
[PROOFSTEP]
simp
[GOAL]
case mk.mk.refine_7
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact f' g'
[PROOFSTEP]
try simp
[GOAL]
case mk.mk.refine_7
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact f' g'
[PROOFSTEP]
simp
[GOAL]
case mk.mk.refine_8
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact g' 0
[PROOFSTEP]
try simp
[GOAL]
case mk.mk.refine_8
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact g' 0
[PROOFSTEP]
simp
[GOAL]
case mk.mk.refine_3
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact 0 f
case mk.mk.refine_4
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact f g
case mk.mk.refine_5
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact g 0
case mk.mk.refine_6
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact 0 f'
case mk.mk.refine_7
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact f' g'
case mk.mk.refine_8
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact g' 0
[PROOFSTEP]
all_goals try assumption
[GOAL]
case mk.mk.refine_3
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact 0 f
[PROOFSTEP]
try assumption
[GOAL]
case mk.mk.refine_3
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact 0 f
[PROOFSTEP]
assumption
[GOAL]
case mk.mk.refine_4
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact f g
[PROOFSTEP]
try assumption
[GOAL]
case mk.mk.refine_4
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact f g
[PROOFSTEP]
assumption
[GOAL]
case mk.mk.refine_5
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact g 0
[PROOFSTEP]
try assumption
[GOAL]
case mk.mk.refine_5
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact g 0
[PROOFSTEP]
assumption
[GOAL]
case mk.mk.refine_6
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact 0 f'
[PROOFSTEP]
try assumption
[GOAL]
case mk.mk.refine_6
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact 0 f'
[PROOFSTEP]
assumption
[GOAL]
case mk.mk.refine_7
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact f' g'
[PROOFSTEP]
try assumption
[GOAL]
case mk.mk.refine_7
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact f' g'
[PROOFSTEP]
assumption
[GOAL]
case mk.mk.refine_8
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact g' 0
[PROOFSTEP]
try assumption
[GOAL]
case mk.mk.refine_8
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact g' 0
[PROOFSTEP]
assumption
[GOAL]
case mk.mk.refine_3
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact 0 f
case mk.mk.refine_5
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact g 0
case mk.mk.refine_6
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact 0 f'
case mk.mk.refine_8
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact g' 0
[PROOFSTEP]
all_goals try apply exact_zero_left_of_mono
[GOAL]
case mk.mk.refine_3
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact 0 f
[PROOFSTEP]
try apply exact_zero_left_of_mono
[GOAL]
case mk.mk.refine_3
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact 0 f
[PROOFSTEP]
apply exact_zero_left_of_mono
[GOAL]
case mk.mk.refine_5
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact g 0
[PROOFSTEP]
try apply exact_zero_left_of_mono
[GOAL]
case mk.mk.refine_5
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact g 0
[PROOFSTEP]
apply exact_zero_left_of_mono
[GOAL]
case mk.mk.refine_6
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact 0 f'
[PROOFSTEP]
try apply exact_zero_left_of_mono
[GOAL]
case mk.mk.refine_6
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact 0 f'
[PROOFSTEP]
apply exact_zero_left_of_mono
[GOAL]
case mk.mk.refine_8
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact g' 0
[PROOFSTEP]
try apply exact_zero_left_of_mono
[GOAL]
case mk.mk.refine_8
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact g' 0
[PROOFSTEP]
apply exact_zero_left_of_mono
[GOAL]
case mk.mk.refine_5
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact g 0
case mk.mk.refine_8
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact g' 0
[PROOFSTEP]
all_goals rwa [← epi_iff_exact_zero_right]
[GOAL]
case mk.mk.refine_5
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact g 0
[PROOFSTEP]
rwa [← epi_iff_exact_zero_right]
[GOAL]
case mk.mk.refine_8
𝒜 : Type u_1
inst✝³ : Category.{u_2, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Abelian 𝒜
i₁ : A ⟶ A'
i₂ : B ⟶ B'
i₃ : C ⟶ C'
comm₁ : autoParam (i₁ ≫ f' = f ≫ i₂) _auto✝
comm₂ : autoParam (i₂ ≫ g' = g ≫ i₃) _auto✝
inst✝¹ : IsIso i₁
inst✝ : IsIso i₃
mono✝¹ : Mono f
epi✝¹ : Epi g
exact✝¹ : Exact f g
mono✝ : Mono f'
epi✝ : Epi g'
exact✝ : Exact f' g'
⊢ Exact g' 0
[PROOFSTEP]
rwa [← epi_iff_exact_zero_right]
[GOAL]
𝒜 : Type u_1
inst✝¹ : Category.{?u.11269, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝ : Abelian 𝒜
h : ShortExact f g
i : A ⊞ C ⟶ B
h1 : biprod.inl ≫ i = f
h2 : i ≫ g = biprod.snd
this : IsIso i
⊢ f ≫ (asIso i).symm.hom = biprod.inl
[PROOFSTEP]
rw [Iso.symm_hom, asIso_inv, IsIso.comp_inv_eq, h1]
[GOAL]
𝒜 : Type u_1
inst✝¹ : Category.{?u.11269, u_1} 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝ : Abelian 𝒜
h : ShortExact f g
i : A ⊞ C ⟶ B
h1 : biprod.inl ≫ i = f
h2 : i ≫ g = biprod.snd
this : IsIso i
⊢ (asIso i).symm.hom ≫ biprod.snd = g
[PROOFSTEP]
rw [Iso.symm_hom, asIso_inv, IsIso.inv_comp_eq, h2]
[GOAL]
𝒜 : Type u_1
inst✝¹ : Category.{?u.20215, u_1} 𝒜
A B C A' B' C' : 𝒜
f✝ : A ⟶ B
g✝ : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝ : Abelian 𝒜
f : A ⟶ B
g : B ⟶ C
h : LeftSplit f g
⊢ f ≫ biprod.lift (Exists.choose (_ : ∃ φ, f ≫ φ = 𝟙 A)) g = biprod.inl
[PROOFSTEP]
ext
[GOAL]
case h₀
𝒜 : Type u_1
inst✝¹ : Category.{?u.20215, u_1} 𝒜
A B C A' B' C' : 𝒜
f✝ : A ⟶ B
g✝ : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝ : Abelian 𝒜
f : A ⟶ B
g : B ⟶ C
h : LeftSplit f g
⊢ (f ≫ biprod.lift (Exists.choose (_ : ∃ φ, f ≫ φ = 𝟙 A)) g) ≫ biprod.fst = biprod.inl ≫ biprod.fst
[PROOFSTEP]
simpa only [biprod.inl_fst, biprod.lift_fst, Category.assoc] using h.left_split.choose_spec
[GOAL]
case h₁
𝒜 : Type u_1
inst✝¹ : Category.{?u.20215, u_1} 𝒜
A B C A' B' C' : 𝒜
f✝ : A ⟶ B
g✝ : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝ : Abelian 𝒜
f : A ⟶ B
g : B ⟶ C
h : LeftSplit f g
⊢ (f ≫ biprod.lift (Exists.choose (_ : ∃ φ, f ≫ φ = 𝟙 A)) g) ≫ biprod.snd = biprod.inl ≫ biprod.snd
[PROOFSTEP]
simp only [biprod.inl_snd, biprod.lift_snd, Category.assoc, h.exact.w]
[GOAL]
𝒜 : Type u_1
inst✝¹ : Category.{?u.20215, u_1} 𝒜
A B C A' B' C' : 𝒜
f✝ : A ⟶ B
g✝ : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝ : Abelian 𝒜
f : A ⟶ B
g : B ⟶ C
h : LeftSplit f g
⊢ biprod.lift (Exists.choose (_ : ∃ φ, f ≫ φ = 𝟙 A)) g ≫ biprod.snd = g
[PROOFSTEP]
simp only [biprod.lift_snd]
[GOAL]
𝒜 : Type u_1
inst✝¹ : Category.{?u.22782, u_1} 𝒜
A B C A' B' C' : 𝒜
f✝ : A ⟶ B
g✝ : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝ : Abelian 𝒜
f : A ⟶ B
g : B ⟶ C
h : RightSplit f g
⊢ biprod.desc f (Exists.choose (_ : ∃ χ, χ ≫ g = 𝟙 C)) ≫ g = biprod.snd
[PROOFSTEP]
ext
[GOAL]
case h₀
𝒜 : Type u_1
inst✝¹ : Category.{?u.22782, u_1} 𝒜
A B C A' B' C' : 𝒜
f✝ : A ⟶ B
g✝ : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝ : Abelian 𝒜
f : A ⟶ B
g : B ⟶ C
h : RightSplit f g
⊢ biprod.inl ≫ biprod.desc f (Exists.choose (_ : ∃ χ, χ ≫ g = 𝟙 C)) ≫ g = biprod.inl ≫ biprod.snd
[PROOFSTEP]
rw [biprod.inl_snd, ← Category.assoc, biprod.inl_desc, h.exact.w]
[GOAL]
case h₁
𝒜 : Type u_1
inst✝¹ : Category.{?u.22782, u_1} 𝒜
A B C A' B' C' : 𝒜
f✝ : A ⟶ B
g✝ : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝ : Abelian 𝒜
f : A ⟶ B
g : B ⟶ C
h : RightSplit f g
⊢ biprod.inr ≫ biprod.desc f (Exists.choose (_ : ∃ χ, χ ≫ g = 𝟙 C)) ≫ g = biprod.inr ≫ biprod.snd
[PROOFSTEP]
rw [biprod.inr_snd, ← Category.assoc, biprod.inr_desc, h.right_split.choose_spec]


[GOAL]
ι : Type u_1
V : Type u
inst✝⁷ : Category.{v, u} V
inst✝⁶ : HasZeroMorphisms V
inst✝⁵ : HasZeroObject V
inst✝⁴ : HasEqualizers V
inst✝³ : HasImages V
inst✝² : HasImageMaps V
inst✝¹ : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
f : C ⟶ D
inst✝ : IsIso f
i : ι
⊢ IsIso ((homologyFunctor V c i).map f)
[PROOFSTEP]
change IsIso ((homologyFunctor V c i).mapIso (asIso f)).hom
[GOAL]
ι : Type u_1
V : Type u
inst✝⁷ : Category.{v, u} V
inst✝⁶ : HasZeroMorphisms V
inst✝⁵ : HasZeroObject V
inst✝⁴ : HasEqualizers V
inst✝³ : HasImages V
inst✝² : HasImageMaps V
inst✝¹ : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
f : C ⟶ D
inst✝ : IsIso f
i : ι
⊢ IsIso ((homologyFunctor V c i).mapIso (asIso f)).hom
[PROOFSTEP]
infer_instance
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
f : C ⟶ D
inst✝¹ : QuasiIso f
g : D ⟶ E
inst✝ : QuasiIso g
i : ι
⊢ IsIso ((homologyFunctor V c i).map (f ≫ g))
[PROOFSTEP]
rw [Functor.map_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
f : C ⟶ D
inst✝¹ : QuasiIso f
g : D ⟶ E
inst✝ : QuasiIso g
i : ι
⊢ IsIso ((homologyFunctor V c i).map f ≫ (homologyFunctor V c i).map g)
[PROOFSTEP]
infer_instance
[GOAL]
ι : Type u_1
V : Type u
inst✝¹³ : Category.{v, u} V
inst✝¹² : HasZeroMorphisms V
inst✝¹¹ : HasZeroObject V
inst✝¹⁰ : HasEqualizers V
inst✝⁹ : HasImages V
inst✝⁸ : HasImageMaps V
inst✝⁷ : HasCokernels V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
W : Type u_2
inst✝⁶ : Category.{u_3, u_2} W
inst✝⁵ : Preadditive W
inst✝⁴ : HasCokernels W
inst✝³ : HasImages W
inst✝² : HasEqualizers W
inst✝¹ : HasZeroObject W
inst✝ : HasImageMaps W
C D : HomologicalComplex W c
e : HomotopyEquiv C D
i : ι
⊢ IsIso ((homologyFunctor W c i).map e.hom)
[PROOFSTEP]
refine' ⟨⟨(homologyFunctor W c i).map e.inv, _⟩⟩
[GOAL]
ι : Type u_1
V : Type u
inst✝¹³ : Category.{v, u} V
inst✝¹² : HasZeroMorphisms V
inst✝¹¹ : HasZeroObject V
inst✝¹⁰ : HasEqualizers V
inst✝⁹ : HasImages V
inst✝⁸ : HasImageMaps V
inst✝⁷ : HasCokernels V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
W : Type u_2
inst✝⁶ : Category.{u_3, u_2} W
inst✝⁵ : Preadditive W
inst✝⁴ : HasCokernels W
inst✝³ : HasImages W
inst✝² : HasEqualizers W
inst✝¹ : HasZeroObject W
inst✝ : HasImageMaps W
C D : HomologicalComplex W c
e : HomotopyEquiv C D
i : ι
⊢ (homologyFunctor W c i).map e.hom ≫ (homologyFunctor W c i).map e.inv = 𝟙 ((homologyFunctor W c i).obj C) ∧
    (homologyFunctor W c i).map e.inv ≫ (homologyFunctor W c i).map e.hom = 𝟙 ((homologyFunctor W c i).obj D)
[PROOFSTEP]
simp only [← Functor.map_comp, ← (homologyFunctor W c i).map_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹³ : Category.{v, u} V
inst✝¹² : HasZeroMorphisms V
inst✝¹¹ : HasZeroObject V
inst✝¹⁰ : HasEqualizers V
inst✝⁹ : HasImages V
inst✝⁸ : HasImageMaps V
inst✝⁷ : HasCokernels V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
W : Type u_2
inst✝⁶ : Category.{u_3, u_2} W
inst✝⁵ : Preadditive W
inst✝⁴ : HasCokernels W
inst✝³ : HasImages W
inst✝² : HasEqualizers W
inst✝¹ : HasZeroObject W
inst✝ : HasImageMaps W
C D : HomologicalComplex W c
e : HomotopyEquiv C D
i : ι
⊢ (homologyFunctor W c i).map (e.hom ≫ e.inv) = (homologyFunctor W c i).map (𝟙 C) ∧
    (homologyFunctor W c i).map (e.inv ≫ e.hom) = (homologyFunctor W c i).map (𝟙 D)
[PROOFSTEP]
constructor
[GOAL]
case left
ι : Type u_1
V : Type u
inst✝¹³ : Category.{v, u} V
inst✝¹² : HasZeroMorphisms V
inst✝¹¹ : HasZeroObject V
inst✝¹⁰ : HasEqualizers V
inst✝⁹ : HasImages V
inst✝⁸ : HasImageMaps V
inst✝⁷ : HasCokernels V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
W : Type u_2
inst✝⁶ : Category.{u_3, u_2} W
inst✝⁵ : Preadditive W
inst✝⁴ : HasCokernels W
inst✝³ : HasImages W
inst✝² : HasEqualizers W
inst✝¹ : HasZeroObject W
inst✝ : HasImageMaps W
C D : HomologicalComplex W c
e : HomotopyEquiv C D
i : ι
⊢ (homologyFunctor W c i).map (e.hom ≫ e.inv) = (homologyFunctor W c i).map (𝟙 C)
[PROOFSTEP]
apply homology_map_eq_of_homotopy
[GOAL]
case right
ι : Type u_1
V : Type u
inst✝¹³ : Category.{v, u} V
inst✝¹² : HasZeroMorphisms V
inst✝¹¹ : HasZeroObject V
inst✝¹⁰ : HasEqualizers V
inst✝⁹ : HasImages V
inst✝⁸ : HasImageMaps V
inst✝⁷ : HasCokernels V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
W : Type u_2
inst✝⁶ : Category.{u_3, u_2} W
inst✝⁵ : Preadditive W
inst✝⁴ : HasCokernels W
inst✝³ : HasImages W
inst✝² : HasEqualizers W
inst✝¹ : HasZeroObject W
inst✝ : HasImageMaps W
C D : HomologicalComplex W c
e : HomotopyEquiv C D
i : ι
⊢ (homologyFunctor W c i).map (e.inv ≫ e.hom) = (homologyFunctor W c i).map (𝟙 D)
[PROOFSTEP]
apply homology_map_eq_of_homotopy
[GOAL]
case left.h
ι : Type u_1
V : Type u
inst✝¹³ : Category.{v, u} V
inst✝¹² : HasZeroMorphisms V
inst✝¹¹ : HasZeroObject V
inst✝¹⁰ : HasEqualizers V
inst✝⁹ : HasImages V
inst✝⁸ : HasImageMaps V
inst✝⁷ : HasCokernels V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
W : Type u_2
inst✝⁶ : Category.{u_3, u_2} W
inst✝⁵ : Preadditive W
inst✝⁴ : HasCokernels W
inst✝³ : HasImages W
inst✝² : HasEqualizers W
inst✝¹ : HasZeroObject W
inst✝ : HasImageMaps W
C D : HomologicalComplex W c
e : HomotopyEquiv C D
i : ι
⊢ Homotopy (e.hom ≫ e.inv) (𝟙 C)
case right.h
ι : Type u_1
V : Type u
inst✝¹³ : Category.{v, u} V
inst✝¹² : HasZeroMorphisms V
inst✝¹¹ : HasZeroObject V
inst✝¹⁰ : HasEqualizers V
inst✝⁹ : HasImages V
inst✝⁸ : HasImageMaps V
inst✝⁷ : HasCokernels V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
W : Type u_2
inst✝⁶ : Category.{u_3, u_2} W
inst✝⁵ : Preadditive W
inst✝⁴ : HasCokernels W
inst✝³ : HasImages W
inst✝² : HasEqualizers W
inst✝¹ : HasZeroObject W
inst✝ : HasImageMaps W
C D : HomologicalComplex W c
e : HomotopyEquiv C D
i : ι
⊢ Homotopy (e.inv ≫ e.hom) (𝟙 D)
[PROOFSTEP]
exacts [e.homotopyHomInvId, e.homotopyInvHomId]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹³ : Category.{v, u} V
inst✝¹² : HasZeroMorphisms V
inst✝¹¹ : HasZeroObject V
inst✝¹⁰ : HasEqualizers V
inst✝⁹ : HasImages V
inst✝⁸ : HasImageMaps V
inst✝⁷ : HasCokernels V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
W : Type u_2
inst✝⁶ : Category.{u_3, u_2} W
inst✝⁵ : Preadditive W
inst✝⁴ : HasCokernels W
inst✝³ : HasImages W
inst✝² : HasEqualizers W
inst✝¹ : HasZeroObject W
inst✝ : HasImageMaps W
C D : HomologicalComplex W c
e : HomotopyEquiv C D
i : ι
⊢ (asIso ((homologyFunctor W c i).map e.hom)).inv = (homologyFunctor W c i).map e.inv
[PROOFSTEP]
symm
[GOAL]
ι : Type u_1
V : Type u
inst✝¹³ : Category.{v, u} V
inst✝¹² : HasZeroMorphisms V
inst✝¹¹ : HasZeroObject V
inst✝¹⁰ : HasEqualizers V
inst✝⁹ : HasImages V
inst✝⁸ : HasImageMaps V
inst✝⁷ : HasCokernels V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
W : Type u_2
inst✝⁶ : Category.{u_3, u_2} W
inst✝⁵ : Preadditive W
inst✝⁴ : HasCokernels W
inst✝³ : HasImages W
inst✝² : HasEqualizers W
inst✝¹ : HasZeroObject W
inst✝ : HasImageMaps W
C D : HomologicalComplex W c
e : HomotopyEquiv C D
i : ι
⊢ (homologyFunctor W c i).map e.inv = (asIso ((homologyFunctor W c i).map e.hom)).inv
[PROOFSTEP]
haveI := e.toQuasiIso.1 i
[GOAL]
ι : Type u_1
V : Type u
inst✝¹³ : Category.{v, u} V
inst✝¹² : HasZeroMorphisms V
inst✝¹¹ : HasZeroObject V
inst✝¹⁰ : HasEqualizers V
inst✝⁹ : HasImages V
inst✝⁸ : HasImageMaps V
inst✝⁷ : HasCokernels V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
W : Type u_2
inst✝⁶ : Category.{u_3, u_2} W
inst✝⁵ : Preadditive W
inst✝⁴ : HasCokernels W
inst✝³ : HasImages W
inst✝² : HasEqualizers W
inst✝¹ : HasZeroObject W
inst✝ : HasImageMaps W
C D : HomologicalComplex W c
e : HomotopyEquiv C D
i : ι
this : IsIso ((homologyFunctor W c i).map e.hom)
⊢ (homologyFunctor W c i).map e.inv = (asIso ((homologyFunctor W c i).map e.hom)).inv
[PROOFSTEP]
simp only [← Iso.hom_comp_eq_id, asIso_hom, ← Functor.map_comp, ← (homologyFunctor W c i).map_id,
  homology_map_eq_of_homotopy e.homotopyHomInvId _]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{?u.22788, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
⊢ d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0
[PROOFSTEP]
rw [← f.2 1 0 rfl]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{?u.22788, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
⊢ HomologicalComplex.Hom.f f 1 ≫ d ((ChainComplex.single₀ W).obj Y) 1 0 = 0
[PROOFSTEP]
exact comp_zero
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
⊢ (toSingle₀CokernelAtZeroIso f).hom =
    cokernel.desc (d X 1 0) (HomologicalComplex.Hom.f f 0) (_ : d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0)
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
⊢ coequalizer.π (d X 1 0) 0 ≫ (toSingle₀CokernelAtZeroIso f).hom =
    coequalizer.π (d X 1 0) 0 ≫
      cokernel.desc (d X 1 0) (HomologicalComplex.Hom.f f 0) (_ : d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0)
[PROOFSTEP]
dsimp only [toSingle₀CokernelAtZeroIso, ChainComplex.homologyZeroIso, homologyOfZeroRight, homology.mapIso,
  ChainComplex.homologyFunctor0Single₀, cokernel.map]
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
⊢ coequalizer.π (d X 1 0) 0 ≫
      ((Iso.mk
                (homology.map (_ : dTo X 0 ≫ dFrom X 0 = 0) (_ : d X 1 0 ≫ 0 = 0)
                  (Arrow.isoMk (xPrevIso X ChainComplex.homologyZeroIso.proof_10)
                      (Iso.refl (Arrow.mk (dTo X 0)).right)).hom
                  (Arrow.isoMk (Iso.refl (Arrow.mk (dFrom X 0)).left) (Iso.refl (Arrow.mk (dFrom X 0)).right)).hom
                  (_ :
                    (Arrow.isoMk (xPrevIso X (_ : 0 + 1 = 0 + 1)) (Iso.refl (Arrow.mk (dTo X 0)).right)).hom.right =
                      (Arrow.isoMk (xPrevIso X (_ : 0 + 1 = 0 + 1)) (Iso.refl (Arrow.mk (dTo X 0)).right)).hom.right))
                (homology.map (_ : d X 1 0 ≫ 0 = 0) (_ : dTo X 0 ≫ dFrom X 0 = 0)
                  (Arrow.isoMk (xPrevIso X ChainComplex.homologyZeroIso.proof_10)
                      (Iso.refl (Arrow.mk (dTo X 0)).right)).inv
                  (Arrow.isoMk (Iso.refl (Arrow.mk (dFrom X 0)).left) (Iso.refl (Arrow.mk (dFrom X 0)).right)).inv
                  (_ :
                    (Arrow.isoMk (xPrevIso X ChainComplex.homologyZeroIso.proof_10)
                            (Iso.refl (Arrow.mk (dTo X 0)).right)).inv.right =
                      (Arrow.isoMk (Iso.refl (Arrow.mk (dFrom X 0)).left)
                            (Iso.refl (Arrow.mk (dFrom X 0)).right)).inv.left)) ≪≫
              cokernel.mapIso (imageToKernel (d X 1 0) 0 (_ : d X 1 0 ≫ 0 = 0)) (image.ι (d X 1 0))
                  (imageSubobjectIso (d X 1 0)) (kernelSubobjectIso 0 ≪≫ kernelZeroIsoSource)
                  (_ :
                    imageToKernel (d X 1 0) 0 (_ : d X 1 0 ≫ 0 = 0) ≫ (kernelSubobjectIso 0).hom ≫ kernel.ι 0 =
                      (imageSubobjectIso (d X 1 0)).hom ≫ image.ι (d X 1 0)) ≪≫
                cokernelImageι (d X 1 0)).symm ≪≫
          asIso ((homologyFunctor W (ComplexShape.down ℕ) 0).map f) ≪≫
            (NatIso.ofComponents fun X =>
                  homology.congr
                      (_ : dTo ((ChainComplex.single₀ W).obj X) 0 ≫ dFrom ((ChainComplex.single₀ W).obj X) 0 = 0)
                      (_ : 0 ≫ 0 = 0) (_ : 0 = 0)
                      (_ : d ((ChainComplex.single₀ W).obj X) 0 (ComplexShape.next (ComplexShape.down ℕ) 0) = 0) ≪≫
                    homologyZeroZero).app
              Y).hom =
    coequalizer.π (d X 1 0) 0 ≫
      cokernel.desc (d X 1 0) (HomologicalComplex.Hom.f f 0) (_ : d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0)
[PROOFSTEP]
dsimp [asIso]
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
⊢ cokernel.π (d X 1 0) ≫
      ((cokernel.desc (d X 1 0) (cokernel.π (image.ι (d X 1 0))) (_ : d X 1 0 ≫ cokernel.π (image.ι (d X 1 0)) = 0) ≫
            cokernel.map (image.ι (d X 1 0)) (imageToKernel (d X 1 0) 0 (_ : d X 1 0 ≫ 0 = 0))
              (imageSubobjectIso (d X 1 0)).inv (kernelZeroIsoSource.inv ≫ (kernelSubobjectIso 0).inv)
              (_ :
                image.ι (d X 1 0) ≫ (kernelSubobjectIso 0 ≪≫ kernelZeroIsoSource).inv =
                  (imageSubobjectIso (d X 1 0)).inv ≫ imageToKernel (d X 1 0) 0 (_ : d X 1 0 ≫ 0 = 0))) ≫
          homology.map (_ : d X 1 0 ≫ 0 = 0) (_ : dTo X 0 ≫ dFrom X 0 = 0)
            (Arrow.isoMk (xPrevIso X ChainComplex.homologyZeroIso.proof_10) (Iso.refl (HomologicalComplex.X X 0))).inv
            (Arrow.isoMk (Iso.refl (HomologicalComplex.X X 0)) (Iso.refl (xNext X 0))).inv
            (_ :
              (Arrow.isoMk (xPrevIso X ChainComplex.homologyZeroIso.proof_10)
                      (Iso.refl (HomologicalComplex.X X 0))).inv.right =
                (Arrow.isoMk (Iso.refl (HomologicalComplex.X X 0)) (Iso.refl (xNext X 0))).inv.left)) ≫
        homology.map (_ : dTo X 0 ≫ dFrom X 0 = 0)
            (_ : dTo ((ChainComplex.single₀ W).obj Y) 0 ≫ dFrom ((ChainComplex.single₀ W).obj Y) 0 = 0) (sqTo f 0)
            (sqFrom f 0) (_ : (sqTo f 0).right = (sqTo f 0).right) ≫
          homology.map (_ : dTo ((ChainComplex.single₀ W).obj Y) 0 ≫ dFrom ((ChainComplex.single₀ W).obj Y) 0 = 0)
              (_ : 0 ≫ 0 = 0) (CommaMorphism.mk (𝟙 (xPrev ((ChainComplex.single₀ W).obj Y) 0)) (𝟙 Y))
              (CommaMorphism.mk (𝟙 Y) (𝟙 (xNext ((ChainComplex.single₀ W).obj Y) 0)))
              (_ :
                (CommaMorphism.mk (𝟙 (Arrow.mk 0).left) (𝟙 (Arrow.mk 0).right)).right =
                  (CommaMorphism.mk (𝟙 (Arrow.mk 0).left) (𝟙 (Arrow.mk 0).right)).right) ≫
            homology.desc 0 0 (_ : 0 ≫ 0 = 0) (Subobject.arrow (kernelSubobject 0))
              (_ : imageToKernel 0 0 (_ : 0 ≫ 0 = 0) ≫ Subobject.arrow (kernelSubobject 0) = 0) =
    cokernel.π (d X 1 0) ≫
      cokernel.desc (d X 1 0) (HomologicalComplex.Hom.f f 0) (_ : d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0)
[PROOFSTEP]
simp only [cokernel.π_desc, Category.assoc, homology.map_desc, cokernel.π_desc_assoc]
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
⊢ kernelZeroIsoSource.inv ≫
      (kernelSubobjectIso 0).inv ≫
        cokernel.π (imageToKernel (d X 1 0) 0 (_ : d X 1 0 ≫ 0 = 0)) ≫
          homology.desc (d X 1 0) 0 (_ : d X 1 0 ≫ 0 = 0)
            (kernelSubobjectMap (Arrow.isoMk (Iso.refl (HomologicalComplex.X X 0)) (Iso.refl (xNext X 0))).inv ≫
              kernelSubobjectMap (sqFrom f 0) ≫
                kernelSubobjectMap (CommaMorphism.mk (𝟙 Y) (𝟙 (xNext ((ChainComplex.single₀ W).obj Y) 0))) ≫
                  Subobject.arrow (kernelSubobject 0))
            (_ :
              imageToKernel (d X 1 0) 0 (_ : d X 1 0 ≫ 0 = 0) ≫
                  kernelSubobjectMap (Arrow.isoMk (Iso.refl (HomologicalComplex.X X 0)) (Iso.refl (xNext X 0))).inv ≫
                    kernelSubobjectMap (sqFrom f 0) ≫
                      kernelSubobjectMap (CommaMorphism.mk (𝟙 Y) (𝟙 (xNext ((ChainComplex.single₀ W).obj Y) 0))) ≫
                        Subobject.arrow (kernelSubobject 0) =
                0) =
    HomologicalComplex.Hom.f f 0
[PROOFSTEP]
simp [homology.desc, Iso.refl_inv (X.X 0)]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
⊢ Epi (HomologicalComplex.Hom.f f 0)
[PROOFSTEP]
constructor
[GOAL]
case left_cancellation
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
⊢ ∀ {Z : W} (g h : HomologicalComplex.X ((ChainComplex.single₀ W).obj Y) 0 ⟶ Z),
    HomologicalComplex.Hom.f f 0 ≫ g = HomologicalComplex.Hom.f f 0 ≫ h → g = h
[PROOFSTEP]
intro Z g h Hgh
[GOAL]
case left_cancellation
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
Z : W
g h : HomologicalComplex.X ((ChainComplex.single₀ W).obj Y) 0 ⟶ Z
Hgh : HomologicalComplex.Hom.f f 0 ≫ g = HomologicalComplex.Hom.f f 0 ≫ h
⊢ g = h
[PROOFSTEP]
rw [← cokernel.π_desc (X.d 1 0) (f.f 0) (by rw [← f.2 1 0 rfl]; exact comp_zero), ←
  toSingle₀CokernelAtZeroIso_hom_eq] at Hgh
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
Z : W
g h : HomologicalComplex.X ((ChainComplex.single₀ W).obj Y) 0 ⟶ Z
Hgh : HomologicalComplex.Hom.f f 0 ≫ g = HomologicalComplex.Hom.f f 0 ≫ h
⊢ d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0
[PROOFSTEP]
rw [← f.2 1 0 rfl]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
Z : W
g h : HomologicalComplex.X ((ChainComplex.single₀ W).obj Y) 0 ⟶ Z
Hgh : HomologicalComplex.Hom.f f 0 ≫ g = HomologicalComplex.Hom.f f 0 ≫ h
⊢ HomologicalComplex.Hom.f f 1 ≫ d ((ChainComplex.single₀ W).obj Y) 1 0 = 0
[PROOFSTEP]
exact comp_zero
[GOAL]
case left_cancellation
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
Z : W
g h : HomologicalComplex.X ((ChainComplex.single₀ W).obj Y) 0 ⟶ Z
Hgh✝ : HomologicalComplex.Hom.f f 0 ≫ g = HomologicalComplex.Hom.f f 0 ≫ h
Hgh :
  (cokernel.π (d X 1 0) ≫ (toSingle₀CokernelAtZeroIso f).hom) ≫ g =
    (cokernel.π (d X 1 0) ≫ (toSingle₀CokernelAtZeroIso f).hom) ≫ h
⊢ g = h
[PROOFSTEP]
rw [(@cancel_epi _ _ _ _ _ _ (epi_comp _ _) _ _).1 Hgh]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
⊢ Exact (d X 1 0) (HomologicalComplex.Hom.f f 0)
[PROOFSTEP]
rw [Preadditive.exact_iff_homology_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
⊢ ∃ w, Nonempty (_root_.homology (d X 1 0) (HomologicalComplex.Hom.f f 0) w ≅ 0)
[PROOFSTEP]
have h : X.d 1 0 ≫ f.f 0 = 0 := by simp only [← f.2 1 0 rfl, ChainComplex.single₀_obj_X_d, comp_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
⊢ d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0
[PROOFSTEP]
simp only [← f.2 1 0 rfl, ChainComplex.single₀_obj_X_d, comp_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
h : d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0
⊢ ∃ w, Nonempty (_root_.homology (d X 1 0) (HomologicalComplex.Hom.f f 0) w ≅ 0)
[PROOFSTEP]
refine' ⟨h, Nonempty.intro (homologyIsoKernelDesc _ _ _ ≪≫ _)⟩
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
h : d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0
⊢ kernel (cokernel.desc (d X 1 0) (HomologicalComplex.Hom.f f 0) h) ≅ 0
[PROOFSTEP]
suffices IsIso (cokernel.desc _ _ h) by apply kernel.ofMono
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
h : d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0
this : IsIso (cokernel.desc (d X 1 0) (HomologicalComplex.Hom.f f 0) h)
⊢ kernel (cokernel.desc (d X 1 0) (HomologicalComplex.Hom.f f 0) h) ≅ 0
[PROOFSTEP]
apply kernel.ofMono
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
h : d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0
⊢ IsIso (cokernel.desc (d X 1 0) (HomologicalComplex.Hom.f f 0) h)
[PROOFSTEP]
rw [← toSingle₀CokernelAtZeroIso_hom_eq]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : ChainComplex W ℕ
Y : W
f : X ⟶ (ChainComplex.single₀ W).obj Y
hf✝ hf : QuasiIso f
h : d X 1 0 ≫ HomologicalComplex.Hom.f f 0 = 0
⊢ IsIso (toSingle₀CokernelAtZeroIso f).hom
[PROOFSTEP]
infer_instance
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{?u.68820, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0
[PROOFSTEP]
rw [f.2 0 1 rfl]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{?u.68820, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ d ((CochainComplex.single₀ W).obj Y) 0 1 ≫ HomologicalComplex.Hom.f f 1 = 0
[PROOFSTEP]
exact zero_comp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ (fromSingle₀KernelAtZeroIso f).inv =
    kernel.lift (d X 0 1) (HomologicalComplex.Hom.f f 0) (_ : HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0)
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ (fromSingle₀KernelAtZeroIso f).inv ≫ equalizer.ι (d X 0 1) 0 =
    kernel.lift (d X 0 1) (HomologicalComplex.Hom.f f 0) (_ : HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0) ≫
      equalizer.ι (d X 0 1) 0
[PROOFSTEP]
dsimp only [fromSingle₀KernelAtZeroIso, CochainComplex.homologyZeroIso, homologyOfZeroLeft, homology.mapIso,
  CochainComplex.homologyFunctor0Single₀, kernel.map]
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ ((Iso.mk
                (homology.map (_ : dTo X 0 ≫ dFrom X 0 = 0) (_ : 0 ≫ d X 0 1 = 0)
                  (Arrow.isoMk (xPrevIsoSelf X CochainComplex.homologyZeroIso.proof_9)
                      (Iso.refl (Arrow.mk (dTo X 0)).right)).hom
                  (Arrow.isoMk (Iso.refl (Arrow.mk (dFrom X 0)).left)
                      (xNextIso X CochainComplex.homologyZeroIso.proof_11)).hom
                  (_ : 𝟙 (HomologicalComplex.X X 0) = 𝟙 (HomologicalComplex.X X 0)))
                (homology.map (_ : 0 ≫ d X 0 1 = 0) (_ : dTo X 0 ≫ dFrom X 0 = 0)
                  (Arrow.isoMk (xPrevIsoSelf X CochainComplex.homologyZeroIso.proof_9)
                      (Iso.refl (Arrow.mk (dTo X 0)).right)).inv
                  (Arrow.isoMk (Iso.refl (Arrow.mk (dFrom X 0)).left)
                      (xNextIso X CochainComplex.homologyZeroIso.proof_11)).inv
                  (_ :
                    (Arrow.isoMk (xPrevIsoSelf X CochainComplex.homologyZeroIso.proof_9)
                            (Iso.refl (Arrow.mk (dTo X 0)).right)).inv.right =
                      (Arrow.isoMk (Iso.refl (Arrow.mk (dFrom X 0)).left)
                            (xNextIso X CochainComplex.homologyZeroIso.proof_11)).inv.left)) ≪≫
              (cokernelIsoOfEq (_ : imageToKernel 0 (d X 0 1) (_ : 0 ≫ d X 0 1 = 0) = 0) ≪≫ cokernelZeroIsoTarget) ≪≫
                kernelSubobjectIso (d X 0 1)).symm ≪≫
          (asIso ((homologyFunctor W (ComplexShape.up ℕ) 0).map f)).symm ≪≫
            (NatIso.ofComponents fun X =>
                  homology.congr
                      (_ : dTo ((CochainComplex.single₀ W).obj X) 0 ≫ dFrom ((CochainComplex.single₀ W).obj X) 0 = 0)
                      (_ : 0 ≫ 0 = 0)
                      (_ : d ((CochainComplex.single₀ W).obj X) (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 = 0)
                      (_ : 0 = 0) ≪≫
                    homologyZeroZero).app
              Y).inv ≫
      equalizer.ι (d X 0 1) 0 =
    kernel.lift (d X 0 1) (HomologicalComplex.Hom.f f 0) (_ : HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0) ≫
      equalizer.ι (d X 0 1) 0
[PROOFSTEP]
simp only [Iso.trans_inv, Iso.app_inv, Iso.symm_inv, Category.assoc, equalizer_as_kernel, kernel.lift_ι]
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ NatTrans.app
        (NatIso.ofComponents fun X =>
            homology.congr
                (_ : dTo ((CochainComplex.single₀ W).obj X) 0 ≫ dFrom ((CochainComplex.single₀ W).obj X) 0 = 0)
                (_ : 0 ≫ 0 = 0)
                (_ : d ((CochainComplex.single₀ W).obj X) (ComplexShape.prev (ComplexShape.up ℕ) 0) 0 = 0)
                (_ : 0 = 0) ≪≫
              homologyZeroZero).inv
        Y ≫
      (asIso ((homologyFunctor W (ComplexShape.up ℕ) 0).map f)).hom ≫
        (Iso.mk
                (homology.map (_ : dTo X 0 ≫ dFrom X 0 = 0) (_ : 0 ≫ d X 0 1 = 0)
                  (Arrow.isoMk (xPrevIsoSelf X CochainComplex.homologyZeroIso.proof_9)
                      (Iso.refl (Arrow.mk (dTo X 0)).right)).hom
                  (Arrow.isoMk (Iso.refl (Arrow.mk (dFrom X 0)).left)
                      (xNextIso X CochainComplex.homologyZeroIso.proof_11)).hom
                  (_ : 𝟙 (HomologicalComplex.X X 0) = 𝟙 (HomologicalComplex.X X 0)))
                (homology.map (_ : 0 ≫ d X 0 1 = 0) (_ : dTo X 0 ≫ dFrom X 0 = 0)
                  (Arrow.isoMk (xPrevIsoSelf X CochainComplex.homologyZeroIso.proof_9)
                      (Iso.refl (Arrow.mk (dTo X 0)).right)).inv
                  (Arrow.isoMk (Iso.refl (Arrow.mk (dFrom X 0)).left)
                      (xNextIso X CochainComplex.homologyZeroIso.proof_11)).inv
                  (_ :
                    (Arrow.isoMk (xPrevIsoSelf X CochainComplex.homologyZeroIso.proof_9)
                            (Iso.refl (Arrow.mk (dTo X 0)).right)).inv.right =
                      (Arrow.isoMk (Iso.refl (Arrow.mk (dFrom X 0)).left)
                            (xNextIso X CochainComplex.homologyZeroIso.proof_11)).inv.left)) ≪≫
              (cokernelIsoOfEq (_ : imageToKernel 0 (d X 0 1) (_ : 0 ≫ d X 0 1 = 0) = 0) ≪≫ cokernelZeroIsoTarget) ≪≫
                kernelSubobjectIso (d X 0 1)).hom ≫
          kernel.ι (d X 0 1) =
    HomologicalComplex.Hom.f f 0
[PROOFSTEP]
dsimp [asIso]
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ ((inv (Subobject.arrow (kernelSubobject 0)) ≫ homology.π 0 0 (_ : 0 ≫ 0 = 0)) ≫
        homology.map (_ : 0 ≫ 0 = 0)
          (_ : dTo ((CochainComplex.single₀ W).obj Y) 0 ≫ dFrom ((CochainComplex.single₀ W).obj Y) 0 = 0)
          (CommaMorphism.mk (𝟙 (xPrev ((CochainComplex.single₀ W).obj Y) 0)) (𝟙 Y))
          (CommaMorphism.mk (𝟙 Y) (𝟙 (xNext ((CochainComplex.single₀ W).obj Y) 0)))
          (_ :
            (CommaMorphism.mk (𝟙 (Arrow.mk 0).left) (𝟙 (Arrow.mk 0).right)).right =
              (CommaMorphism.mk (𝟙 (Arrow.mk 0).left) (𝟙 (Arrow.mk 0).right)).right)) ≫
      homology.map (_ : dTo ((CochainComplex.single₀ W).obj Y) 0 ≫ dFrom ((CochainComplex.single₀ W).obj Y) 0 = 0)
          (_ : dTo X 0 ≫ dFrom X 0 = 0) (sqTo f 0) (sqFrom f 0) (_ : (sqTo f 0).right = (sqTo f 0).right) ≫
        (homology.map (_ : dTo X 0 ≫ dFrom X 0 = 0) (_ : 0 ≫ d X 0 1 = 0)
              (Arrow.isoMk (xPrevIsoSelf X CochainComplex.homologyZeroIso.proof_9)
                  (Iso.refl (HomologicalComplex.X X 0))).hom
              (Arrow.isoMk (Iso.refl (HomologicalComplex.X X 0))
                  (xNextIso X CochainComplex.homologyZeroIso.proof_11)).hom
              (_ : 𝟙 (HomologicalComplex.X X 0) = 𝟙 (HomologicalComplex.X X 0)) ≫
            ((cokernelIsoOfEq (_ : imageToKernel 0 (d X 0 1) (_ : 0 ≫ d X 0 1 = 0) = 0)).hom ≫
                cokernelZeroIsoTarget.hom) ≫
              (kernelSubobjectIso (d X 0 1)).hom) ≫
          kernel.ι (d X 0 1) =
    HomologicalComplex.Hom.f f 0
[PROOFSTEP]
simp only [Category.assoc, homology.π_map, cokernelZeroIsoTarget_hom, cokernelIsoOfEq_hom_comp_desc,
  kernelSubobject_arrow, homology.π_map_assoc, IsIso.inv_comp_eq]
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ kernelSubobjectMap (CommaMorphism.mk (𝟙 Y) (𝟙 (xNext ((CochainComplex.single₀ W).obj Y) 0))) ≫
      kernelSubobjectMap (sqFrom f 0) ≫
        kernelSubobjectMap
            (Arrow.isoMk (Iso.refl (HomologicalComplex.X X 0))
                (xNextIso X CochainComplex.homologyZeroIso.proof_11)).hom ≫
          homology.π 0 (d X 0 1) (_ : 0 ≫ d X 0 1 = 0) ≫
            cokernel.desc (imageToKernel 0 (d X 0 1) (_ : 0 ≫ d X 0 1 = 0))
                (𝟙 (Subobject.underlying.obj (kernelSubobject (d X 0 1))))
                (_ :
                  imageToKernel 0 (d X 0 1) (_ : 0 ≫ d X 0 1 = 0) ≫
                      𝟙 (Subobject.underlying.obj (kernelSubobject (d X 0 1))) =
                    0) ≫
              Subobject.arrow (kernelSubobject (d X 0 1)) =
    Subobject.arrow (kernelSubobject 0) ≫ HomologicalComplex.Hom.f f 0
[PROOFSTEP]
simp [homology.π, kernelSubobjectMap_comp, Iso.refl_hom (X.X 0), Category.comp_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ Mono (HomologicalComplex.Hom.f f 0)
[PROOFSTEP]
constructor
[GOAL]
case right_cancellation
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ ∀ {Z : W} (g h : Z ⟶ HomologicalComplex.X ((CochainComplex.single₀ W).obj Y) 0),
    g ≫ HomologicalComplex.Hom.f f 0 = h ≫ HomologicalComplex.Hom.f f 0 → g = h
[PROOFSTEP]
intro Z g h Hgh
[GOAL]
case right_cancellation
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
Z : W
g h : Z ⟶ HomologicalComplex.X ((CochainComplex.single₀ W).obj Y) 0
Hgh : g ≫ HomologicalComplex.Hom.f f 0 = h ≫ HomologicalComplex.Hom.f f 0
⊢ g = h
[PROOFSTEP]
rw [← kernel.lift_ι (X.d 0 1) (f.f 0) (by rw [f.2 0 1 rfl]; exact zero_comp), ← fromSingle₀KernelAtZeroIso_inv_eq] at
  Hgh
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
Z : W
g h : Z ⟶ HomologicalComplex.X ((CochainComplex.single₀ W).obj Y) 0
Hgh : g ≫ HomologicalComplex.Hom.f f 0 = h ≫ HomologicalComplex.Hom.f f 0
⊢ HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0
[PROOFSTEP]
rw [f.2 0 1 rfl]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
Z : W
g h : Z ⟶ HomologicalComplex.X ((CochainComplex.single₀ W).obj Y) 0
Hgh : g ≫ HomologicalComplex.Hom.f f 0 = h ≫ HomologicalComplex.Hom.f f 0
⊢ d ((CochainComplex.single₀ W).obj Y) 0 1 ≫ HomologicalComplex.Hom.f f 1 = 0
[PROOFSTEP]
exact zero_comp
[GOAL]
case right_cancellation
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
Z : W
g h : Z ⟶ HomologicalComplex.X ((CochainComplex.single₀ W).obj Y) 0
Hgh✝ : g ≫ HomologicalComplex.Hom.f f 0 = h ≫ HomologicalComplex.Hom.f f 0
Hgh :
  g ≫ (fromSingle₀KernelAtZeroIso f).inv ≫ kernel.ι (d X 0 1) =
    h ≫ (fromSingle₀KernelAtZeroIso f).inv ≫ kernel.ι (d X 0 1)
⊢ g = h
[PROOFSTEP]
rw [(@cancel_mono _ _ _ _ _ _ (mono_comp _ _) _ _).1 Hgh]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ Exact (HomologicalComplex.Hom.f f 0) (d X 0 1)
[PROOFSTEP]
rw [Preadditive.exact_iff_homology_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ ∃ w, Nonempty (_root_.homology (HomologicalComplex.Hom.f f 0) (d X 0 1) w ≅ 0)
[PROOFSTEP]
have h : f.f 0 ≫ X.d 0 1 = 0 := by simp only [HomologicalComplex.Hom.comm, CochainComplex.single₀_obj_X_d, zero_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
⊢ HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0
[PROOFSTEP]
simp only [HomologicalComplex.Hom.comm, CochainComplex.single₀_obj_X_d, zero_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
h : HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0
⊢ ∃ w, Nonempty (_root_.homology (HomologicalComplex.Hom.f f 0) (d X 0 1) w ≅ 0)
[PROOFSTEP]
refine' ⟨h, Nonempty.intro (homologyIsoCokernelLift _ _ _ ≪≫ _)⟩
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
h : HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0
⊢ cokernel (kernel.lift (d X 0 1) (HomologicalComplex.Hom.f f 0) h) ≅ 0
[PROOFSTEP]
suffices IsIso (kernel.lift (X.d 0 1) (f.f 0) h) by apply cokernel.ofEpi
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
h : HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0
this : IsIso (kernel.lift (d X 0 1) (HomologicalComplex.Hom.f f 0) h)
⊢ cokernel (kernel.lift (d X 0 1) (HomologicalComplex.Hom.f f 0) h) ≅ 0
[PROOFSTEP]
apply cokernel.ofEpi
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
h : HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0
⊢ IsIso (kernel.lift (d X 0 1) (HomologicalComplex.Hom.f f 0) h)
[PROOFSTEP]
rw [← fromSingle₀KernelAtZeroIso_inv_eq f]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
inst✝⁶ : HasZeroObject V
inst✝⁵ : HasEqualizers V
inst✝⁴ : HasImages V
inst✝³ : HasImageMaps V
inst✝² : HasCokernels V
c : ComplexShape ι
C D E : HomologicalComplex V c
W : Type u_2
inst✝¹ : Category.{u_3, u_2} W
inst✝ : Abelian W
X : CochainComplex W ℕ
Y : W
f : (CochainComplex.single₀ W).obj Y ⟶ X
hf : QuasiIso f
h : HomologicalComplex.Hom.f f 0 ≫ d X 0 1 = 0
⊢ IsIso (fromSingle₀KernelAtZeroIso f).inv
[PROOFSTEP]
infer_instance
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁴ : Category.{v, u} V
inst✝¹³ : HasZeroMorphisms V
inst✝¹² : HasZeroObject V
inst✝¹¹ : HasEqualizers V
inst✝¹⁰ : HasImages V
inst✝⁹ : HasImageMaps V
inst✝⁸ : HasCokernels V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
A : Type u_2
inst✝⁷ : Category.{u_4, u_2} A
inst✝⁶ : Abelian A
B : Type u_3
inst✝⁵ : Category.{u_5, u_3} B
inst✝⁴ : Abelian B
F : A ⥤ B
inst✝³ : Additive F
inst✝² : PreservesFiniteLimits F
inst✝¹ : PreservesFiniteColimits F
inst✝ : Faithful F
C D : HomologicalComplex A c
f : C ⟶ D
hf : QuasiIso ((mapHomologicalComplex F c).map f)
i : ι
⊢ IsIso (F.map ((homologyFunctor A c i).map f))
[PROOFSTEP]
rw [← Functor.comp_map, ← NatIso.naturality_2 (F.homologyFunctorIso i) f, Functor.comp_map]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁴ : Category.{v, u} V
inst✝¹³ : HasZeroMorphisms V
inst✝¹² : HasZeroObject V
inst✝¹¹ : HasEqualizers V
inst✝¹⁰ : HasImages V
inst✝⁹ : HasImageMaps V
inst✝⁸ : HasCokernels V
c : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c
A : Type u_2
inst✝⁷ : Category.{u_4, u_2} A
inst✝⁶ : Abelian A
B : Type u_3
inst✝⁵ : Category.{u_5, u_3} B
inst✝⁴ : Abelian B
F : A ⥤ B
inst✝³ : Additive F
inst✝² : PreservesFiniteLimits F
inst✝¹ : PreservesFiniteColimits F
inst✝ : Faithful F
C D : HomologicalComplex A c
f : C ⟶ D
hf : QuasiIso ((mapHomologicalComplex F c).map f)
i : ι
⊢ IsIso
    (NatTrans.app (homologyFunctorIso F i).hom C ≫
      (homologyFunctor B c i).map ((mapHomologicalComplex F c).map f) ≫ NatTrans.app (homologyFunctorIso F i).inv D)
[PROOFSTEP]
infer_instance


[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.4444, u_1} C
inst✝ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
i j k : ι
hi : ComplexShape.prev c j = i
hk : ComplexShape.next c j = k
K : HomologicalComplex C c
⊢ (XIsoOfEq K hi).hom ≫ ((shortComplexFunctor' C c i j k).obj K).f =
    ((shortComplexFunctor C c j).obj K).f ≫ (Iso.refl ((shortComplexFunctor C c j).obj K).X₂).hom
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.4444, u_1} C
inst✝ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
i j k : ι
hi : ComplexShape.prev c j = i
hk : ComplexShape.next c j = k
K : HomologicalComplex C c
⊢ (Iso.refl ((shortComplexFunctor C c j).obj K).X₂).hom ≫ ((shortComplexFunctor' C c i j k).obj K).g =
    ((shortComplexFunctor C c j).obj K).g ≫ (XIsoOfEq K hk).hom
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.4444, u_1} C
inst✝ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
i j k : ι
hi : ComplexShape.prev c j = i
hk : ComplexShape.next c j = k
⊢ ∀ {X Y : HomologicalComplex C c} (f : X ⟶ Y),
    (shortComplexFunctor C c j).map f ≫
        ((fun K => ShortComplex.isoMk (XIsoOfEq K hi) (Iso.refl ((shortComplexFunctor C c j).obj K).X₂) (XIsoOfEq K hk))
            Y).hom =
      ((fun K => ShortComplex.isoMk (XIsoOfEq K hi) (Iso.refl ((shortComplexFunctor C c j).obj K).X₂) (XIsoOfEq K hk))
            X).hom ≫
        (shortComplexFunctor' C c i j k).map f
[PROOFSTEP]
aesop_cat


[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
C : HomologicalComplex (HomologicalComplex V c) c'
i : ι
j j' : ι'
w : ¬ComplexShape.Rel c' j j'
⊢ (fun j j' => Hom.f (d C j j') i) j j' = 0
[PROOFSTEP]
simp_all only [shape, zero_f]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
C : HomologicalComplex (HomologicalComplex V c) c'
i i' : ι
w : ¬ComplexShape.Rel c i i'
⊢ (fun i i' => Hom.mk fun j => d (X C j) i i') i i' = 0
[PROOFSTEP]
ext j
[GOAL]
case h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
C : HomologicalComplex (HomologicalComplex V c) c'
i i' : ι
w : ¬ComplexShape.Rel c i i'
j : ι'
⊢ Hom.f ((fun i i' => Hom.mk fun j => d (X C j) i i') i i') j = Hom.f 0 j
[PROOFSTEP]
exact (C.X j).shape i i' w
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
C : HomologicalComplex (HomologicalComplex V c) c'
i j : ι'
x✝ : ComplexShape.Rel c' i j
⊢ (fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) i ≫ d ((flip V c c' ⋙ flip V c' c).obj C) i j =
    d ((𝟭 (HomologicalComplex (HomologicalComplex V c) c')).obj C) i j ≫ (fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) j
[PROOFSTEP]
ext
[GOAL]
case h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
C : HomologicalComplex (HomologicalComplex V c) c'
i j : ι'
x✝ : ComplexShape.Rel c' i j
i✝ : ι
⊢ Hom.f ((fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) i ≫ d ((flip V c c' ⋙ flip V c' c).obj C) i j) i✝ =
    Hom.f
      (d ((𝟭 (HomologicalComplex (HomologicalComplex V c) c')).obj C) i j ≫
        (fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) j)
      i✝
[PROOFSTEP]
dsimp
[GOAL]
case h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
C : HomologicalComplex (HomologicalComplex V c) c'
i j : ι'
x✝ : ComplexShape.Rel c' i j
i✝ : ι
⊢ 𝟙 (X (X C i) i✝) ≫ Hom.f (d C i j) i✝ = Hom.f (d C i j) i✝ ≫ 𝟙 (X (X C j) i✝)
[PROOFSTEP]
simp only [Category.id_comp, Category.comp_id]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
C : HomologicalComplex (HomologicalComplex V c) c'
i j : ι'
x✝ : ComplexShape.Rel c' i j
⊢ (fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) i ≫ d ((𝟭 (HomologicalComplex (HomologicalComplex V c) c')).obj C) i j =
    d ((flip V c c' ⋙ flip V c' c).obj C) i j ≫ (fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) j
[PROOFSTEP]
ext
[GOAL]
case h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
C : HomologicalComplex (HomologicalComplex V c) c'
i j : ι'
x✝ : ComplexShape.Rel c' i j
i✝ : ι
⊢ Hom.f
      ((fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) i ≫
        d ((𝟭 (HomologicalComplex (HomologicalComplex V c) c')).obj C) i j)
      i✝ =
    Hom.f (d ((flip V c c' ⋙ flip V c' c).obj C) i j ≫ (fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) j) i✝
[PROOFSTEP]
dsimp
[GOAL]
case h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
C : HomologicalComplex (HomologicalComplex V c) c'
i j : ι'
x✝ : ComplexShape.Rel c' i j
i✝ : ι
⊢ 𝟙 (X (X C i) i✝) ≫ Hom.f (d C i j) i✝ = Hom.f (d C i j) i✝ ≫ 𝟙 (X (X C j) i✝)
[PROOFSTEP]
simp only [Category.id_comp, Category.comp_id]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
X Y : HomologicalComplex (HomologicalComplex V c) c'
f : X ⟶ Y
⊢ (𝟭 (HomologicalComplex (HomologicalComplex V c) c')).map f ≫
      ((fun C =>
            Iso.mk (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j))
              (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j)))
          Y).hom =
    ((fun C =>
            Iso.mk (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j))
              (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j)))
          X).hom ≫
      (flip V c c' ⋙ flip V c' c).map f
[PROOFSTEP]
ext
[GOAL]
case h.h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
X Y : HomologicalComplex (HomologicalComplex V c) c'
f : X ⟶ Y
i✝¹ : ι'
i✝ : ι
⊢ Hom.f
      (Hom.f
        ((𝟭 (HomologicalComplex (HomologicalComplex V c) c')).map f ≫
          ((fun C =>
                Iso.mk (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j))
                  (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j)))
              Y).hom)
        i✝¹)
      i✝ =
    Hom.f
      (Hom.f
        (((fun C =>
                Iso.mk (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j))
                  (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j)))
              X).hom ≫
          (flip V c c' ⋙ flip V c' c).map f)
        i✝¹)
      i✝
[PROOFSTEP]
dsimp
[GOAL]
case h.h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
X Y : HomologicalComplex (HomologicalComplex V c) c'
f : X ⟶ Y
i✝¹ : ι'
i✝ : ι
⊢ Hom.f (Hom.f f i✝¹) i✝ ≫ 𝟙 (HomologicalComplex.X (HomologicalComplex.X Y i✝¹) i✝) =
    𝟙 (HomologicalComplex.X (HomologicalComplex.X X i✝¹) i✝) ≫ Hom.f (Hom.f f i✝¹) i✝
[PROOFSTEP]
simp only [Category.id_comp, Category.comp_id]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
C : HomologicalComplex (HomologicalComplex V c') c
i j : ι
x✝ : ComplexShape.Rel c i j
⊢ (fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) i ≫ d ((𝟭 (HomologicalComplex (HomologicalComplex V c') c)).obj C) i j =
    d ((flip V c' c ⋙ flip V c c').obj C) i j ≫ (fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) j
[PROOFSTEP]
ext
[GOAL]
case h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
C : HomologicalComplex (HomologicalComplex V c') c
i j : ι
x✝ : ComplexShape.Rel c i j
i✝ : ι'
⊢ Hom.f
      ((fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) i ≫
        d ((𝟭 (HomologicalComplex (HomologicalComplex V c') c)).obj C) i j)
      i✝ =
    Hom.f (d ((flip V c' c ⋙ flip V c c').obj C) i j ≫ (fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) j) i✝
[PROOFSTEP]
dsimp
[GOAL]
case h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
C : HomologicalComplex (HomologicalComplex V c') c
i j : ι
x✝ : ComplexShape.Rel c i j
i✝ : ι'
⊢ 𝟙 (X (X C i) i✝) ≫ Hom.f (d C i j) i✝ = Hom.f (d C i j) i✝ ≫ 𝟙 (X (X C j) i✝)
[PROOFSTEP]
simp only [Category.id_comp, Category.comp_id]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
C : HomologicalComplex (HomologicalComplex V c') c
i j : ι
x✝ : ComplexShape.Rel c i j
⊢ (fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) i ≫ d ((flip V c' c ⋙ flip V c c').obj C) i j =
    d ((𝟭 (HomologicalComplex (HomologicalComplex V c') c)).obj C) i j ≫ (fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) j
[PROOFSTEP]
ext
[GOAL]
case h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
C : HomologicalComplex (HomologicalComplex V c') c
i j : ι
x✝ : ComplexShape.Rel c i j
i✝ : ι'
⊢ Hom.f ((fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) i ≫ d ((flip V c' c ⋙ flip V c c').obj C) i j) i✝ =
    Hom.f
      (d ((𝟭 (HomologicalComplex (HomologicalComplex V c') c)).obj C) i j ≫
        (fun i => Hom.mk fun j => 𝟙 (X (X C i) j)) j)
      i✝
[PROOFSTEP]
dsimp
[GOAL]
case h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
C : HomologicalComplex (HomologicalComplex V c') c
i j : ι
x✝ : ComplexShape.Rel c i j
i✝ : ι'
⊢ 𝟙 (X (X C i) i✝) ≫ Hom.f (d C i j) i✝ = Hom.f (d C i j) i✝ ≫ 𝟙 (X (X C j) i✝)
[PROOFSTEP]
simp only [Category.id_comp, Category.comp_id]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
X Y : HomologicalComplex (HomologicalComplex V c') c
f : X ⟶ Y
⊢ (flip V c' c ⋙ flip V c c').map f ≫
      ((fun C =>
            Iso.mk (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j))
              (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j)))
          Y).hom =
    ((fun C =>
            Iso.mk (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j))
              (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j)))
          X).hom ≫
      (𝟭 (HomologicalComplex (HomologicalComplex V c') c)).map f
[PROOFSTEP]
ext
[GOAL]
case h.h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
X Y : HomologicalComplex (HomologicalComplex V c') c
f : X ⟶ Y
i✝¹ : ι
i✝ : ι'
⊢ Hom.f
      (Hom.f
        ((flip V c' c ⋙ flip V c c').map f ≫
          ((fun C =>
                Iso.mk (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j))
                  (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j)))
              Y).hom)
        i✝¹)
      i✝ =
    Hom.f
      (Hom.f
        (((fun C =>
                Iso.mk (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j))
                  (Hom.mk fun i => Hom.mk fun j => 𝟙 (HomologicalComplex.X (HomologicalComplex.X C i) j)))
              X).hom ≫
          (𝟭 (HomologicalComplex (HomologicalComplex V c') c)).map f)
        i✝¹)
      i✝
[PROOFSTEP]
dsimp
[GOAL]
case h.h
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
ι' : Type u_2
c' : ComplexShape ι'
X Y : HomologicalComplex (HomologicalComplex V c') c
f : X ⟶ Y
i✝¹ : ι
i✝ : ι'
⊢ Hom.f (Hom.f f i✝¹) i✝ ≫ 𝟙 (HomologicalComplex.X (HomologicalComplex.X Y i✝¹) i✝) =
    𝟙 (HomologicalComplex.X (HomologicalComplex.X X i✝¹) i✝) ≫ Hom.f (Hom.f f i✝¹) i✝
[PROOFSTEP]
simp only [Category.id_comp, Category.comp_id]