𝒜 : 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
⊢ (h.iso.hom ≫ biprod.fst) ≫ f + g ≫ biprod.inr ≫ h.iso.inv = 𝟙 B
𝒜 : 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
⊢ retraction h ≫ f + g ≫ section h = 𝟙 B
delta Splitting.section retraction
𝒜 : 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
⊢ h.iso.inv ≫ ((h.iso.hom ≫ biprod.fst) ≫ f + g ≫ biprod.inr ≫ h.iso.inv) ≫ h.iso.hom = h.iso.inv ≫ 𝟙 B ≫ 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
⊢ (h.iso.hom ≫ biprod.fst) ≫ f + g ≫ biprod.inr ≫ h.iso.inv = 𝟙 B
rw [← cancel_mono h.iso.hom, ← cancel_epi h.iso.inv]
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
⊢ h.iso.inv ≫ ((h.iso.hom ≫ biprod.fst) ≫ f + g ≫ biprod.inr ≫ h.iso.inv) ≫ h.iso.hom = h.iso.inv ≫ 𝟙 B ≫ h.iso.hom
simp only [Category.comp_id, Category.id_comp, Category.assoc, Iso.inv_hom_id_assoc,
  Iso.inv_hom_id, Limits.biprod.total, Preadditive.comp_add, Preadditive.add_comp,
  Splitting.comp_iso_eq_inl, Splitting.iso_comp_eq_snd_assoc]