[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]
