case mk.intro.intro.intro.intro.intro.intro
𝒜 : Type u_1
inst✝³ : Category 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Preadditive 𝒜
inst✝¹ : HasKernels 𝒜
inst✝ : HasImages 𝒜
φ : B ⟶ A
χ : C ⟶ B
h1 : f ≫ g = 0
h2 : φ ≫ f + g ≫ χ = 𝟙 B
⊢ Exact f g
𝒜 : Type u_1
inst✝³ : Category 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Preadditive 𝒜
inst✝¹ : HasKernels 𝒜
inst✝ : HasImages 𝒜
h : Split f g
⊢ Exact f g
obtain ⟨φ, χ, -, -, h1, -, h2⟩ := h
no goals
case mk.intro.intro.intro.intro.intro.intro
𝒜 : Type u_1
inst✝³ : Category 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝² : Preadditive 𝒜
inst✝¹ : HasKernels 𝒜
inst✝ : HasImages 𝒜
φ : B ⟶ A
χ : C ⟶ B
h1 : f ≫ g = 0
h2 : φ ≫ f + g ≫ χ = 𝟙 B
⊢ Exact f g
exact exact_of_split h1 h2