𝒜 : Type u_2
inst✝⁶ : Category 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ Exact biprod.inl biprod.snd

𝒜 : Type u_2
inst✝⁶ : Category 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ Arrow.mk f ≅ Arrow.mk biprod.inl

𝒜 : Type u_2
inst✝⁶ : Category 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ Arrow.mk g ≅ Arrow.mk biprod.snd

𝒜 : Type u_2
inst✝⁶ : Category 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ ?m.104433.hom.right = ?m.104434.hom.left
𝒜 : Type u_2
inst✝⁶ : Category 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ Exact f g
rw [exact_iff_exact_of_iso f g (biprod.inl : A ⟶ A ⊞ C) (biprod.snd : A ⊞ C ⟶ C) _ _ _]
no goals
𝒜 : Type u_2
inst✝⁶ : Category 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ Exact biprod.inl biprod.snd
exact exact_inl_snd _ _
𝒜 : Type u_2
inst✝⁶ : Category 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ (Iso.refl (Arrow.mk f).left).hom ≫ (Arrow.mk biprod.inl).hom = (Arrow.mk f).hom ≫ h.iso.hom
𝒜 : Type u_2
inst✝⁶ : Category 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ Arrow.mk f ≅ Arrow.mk biprod.inl
refine Arrow.isoMk (Iso.refl _) h.iso ?_
𝒜 : Type u_2
inst✝⁶ : Category 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ biprod.inl = biprod.inl
𝒜 : Type u_2
inst✝⁶ : Category 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ (Iso.refl (Arrow.mk f).left).hom ≫ (Arrow.mk biprod.inl).hom = (Arrow.mk f).hom ≫ h.iso.hom
simp only [Iso.refl_hom, Arrow.mk_hom, Category.id_comp, comp_iso_eq_inl]
no goals
𝒜 : Type u_2
inst✝⁶ : Category 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ biprod.inl = biprod.inl
rfl
𝒜 : Type u_2
inst✝⁶ : Category 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ h.iso.hom ≫ (Arrow.mk biprod.snd).hom = (Arrow.mk g).hom ≫ (Iso.refl (Arrow.mk g).right).hom
𝒜 : Type u_2
inst✝⁶ : Category 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ Arrow.mk g ≅ Arrow.mk biprod.snd
refine Arrow.isoMk h.iso (Iso.refl _) ?_
𝒜 : Type u_2
inst✝⁶ : Category 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ h.iso.hom ≫ biprod.snd = g ≫ 𝟙 C
𝒜 : Type u_2
inst✝⁶ : Category 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ h.iso.hom ≫ (Arrow.mk biprod.snd).hom = (Arrow.mk g).hom ≫ (Iso.refl (Arrow.mk g).right).hom
dsimp
no goals
𝒜 : Type u_2
inst✝⁶ : Category 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ h.iso.hom ≫ biprod.snd = g ≫ 𝟙 C
simp
no goals
𝒜 : Type u_2
inst✝⁶ : Category 𝒜
A B C A' B' C' : 𝒜
f : A ⟶ B
g : B ⟶ C
f' : A' ⟶ B'
g' : B' ⟶ C'
inst✝⁵ : Preadditive 𝒜
inst✝⁴ : HasBinaryBiproducts 𝒜
h : Splitting f g
inst✝³ : HasKernels 𝒜
inst✝² : HasImages 𝒜
inst✝¹ : HasZeroObject 𝒜
inst✝ : HasCokernels 𝒜
⊢ (Arrow.isoMk (Iso.refl (Arrow.mk f).left) h.iso).hom.right =
    (Arrow.isoMk h.iso (Iso.refl (Arrow.mk g).right)).hom.left
rfl