case mk
𝒜 : Type u_1
inst✝³ : Category 𝒜
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₂
𝒜 : Type u_1
inst✝³ : Category 𝒜
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₂
obtain ⟨_⟩ := h
case mk.mk
𝒜 : Type u_1
inst✝³ : Category 𝒜
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₂
case mk
𝒜 : Type u_1
inst✝³ : Category 𝒜
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₂
obtain ⟨_⟩ := h'
case mk.mk.refine_1
𝒜 : Type u_1
inst✝³ : Category 𝒜
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 𝒜
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 𝒜
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 𝒜
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 𝒜
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 𝒜
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 𝒜
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 𝒜
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
𝒜 : Type u_1
inst✝³ : Category 𝒜
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₂
refine @Abelian.isIso_of_isIso_of_isIso_of_isIso_of_isIso 𝒜 _ _ 0 _ _ _ 0 _ _ _ 0 f g 0 f' g'
    0 i₁ i₂ i₃ ?_ comm₁ comm₂ 0 0 0 0 0 ?_ ?_ ?_ ?_ ?_ ?_ ?_ _ _ _ _
case mk.mk.refine_3
𝒜 : Type u_1
inst✝³ : Category 𝒜
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 𝒜
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 𝒜
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 𝒜
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 𝒜
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 𝒜
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_1
𝒜 : Type u_1
inst✝³ : Category 𝒜
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 𝒜
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 𝒜
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 𝒜
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 𝒜
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 𝒜
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 𝒜
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 𝒜
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
all_goals try simp
case mk.mk.refine_3
𝒜 : Type u_1
inst✝³ : Category 𝒜
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 𝒜
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 𝒜
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 𝒜
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_3
𝒜 : Type u_1
inst✝³ : Category 𝒜
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 𝒜
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 𝒜
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 𝒜
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 𝒜
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 𝒜
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
all_goals try assumption
case mk.mk.refine_5
𝒜 : Type u_1
inst✝³ : Category 𝒜
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 𝒜
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_3
𝒜 : Type u_1
inst✝³ : Category 𝒜
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 𝒜
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 𝒜
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 𝒜
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
all_goals try apply exact_zero_left_of_mono
no goals
case mk.mk.refine_5
𝒜 : Type u_1
inst✝³ : Category 𝒜
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 𝒜
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
all_goals rwa [← epi_iff_exact_zero_right ]
case mk.mk.refine_8
𝒜 : Type u_1
inst✝³ : Category 𝒜
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 𝒜
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
try simp
case mk.mk.refine_8
𝒜 : Type u_1
inst✝³ : Category 𝒜
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 𝒜
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
simp
case mk.mk.refine_8
𝒜 : Type u_1
inst✝³ : Category 𝒜
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 𝒜
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
try assumption
case mk.mk.refine_8
𝒜 : Type u_1
inst✝³ : Category 𝒜
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 𝒜
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
assumption
case mk.mk.refine_8
𝒜 : Type u_1
inst✝³ : Category 𝒜
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 𝒜
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
try apply exact_zero_left_of_mono
case mk.mk.refine_8
𝒜 : Type u_1
inst✝³ : Category 𝒜
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 𝒜
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
apply exact_zero_left_of_mono
no goals
case mk.mk.refine_8
𝒜 : Type u_1
inst✝³ : Category 𝒜
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
rwa [← epi_iff_exact_zero_right ]