C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝ : IsIso (biprod.map f g)
t :
  (fun p => biprod.inl ≫ p ≫ biprod.fst) (biprod.map f g ≫ inv (biprod.map f g)) =
    (fun p => biprod.inl ≫ p ≫ biprod.fst) (𝟙 (W ⊞ X))
⊢ f ≫ biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst = 𝟙 W
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝ : IsIso (biprod.map f g)
⊢ f ≫ biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst = 𝟙 W
have t := congrArg (fun p : W ⊞ X ⟶ W ⊞ X => biprod.inl ≫ p ≫ biprod.fst)
  (IsIso.hom_inv_id (biprod.map f g))
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝ : IsIso (biprod.map f g)
t : f ≫ biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst = biprod.inl ≫ biprod.fst
⊢ f ≫ biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst = 𝟙 W
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝ : IsIso (biprod.map f g)
t :
  (fun p => biprod.inl ≫ p ≫ biprod.fst) (biprod.map f g ≫ inv (biprod.map f g)) =
    (fun p => biprod.inl ≫ p ≫ biprod.fst) (𝟙 (W ⊞ X))
⊢ f ≫ biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst = 𝟙 W
simp only [Category.id_comp, Category.assoc, biprod.inl_map_assoc] at t
no goals
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝ : IsIso (biprod.map f g)
t : f ≫ biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst = biprod.inl ≫ biprod.fst
⊢ f ≫ biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst = 𝟙 W
simp [t]
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝ : IsIso (biprod.map f g)
t :
  (fun p => biprod.inl ≫ p ≫ biprod.fst) (inv (biprod.map f g) ≫ biprod.map f g) =
    (fun p => biprod.inl ≫ p ≫ biprod.fst) (𝟙 (Y ⊞ Z))
⊢ (biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst) ≫ f = 𝟙 Y
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝ : IsIso (biprod.map f g)
⊢ (biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst) ≫ f = 𝟙 Y
have t := congrArg (fun p : Y ⊞ Z ⟶ Y ⊞ Z => biprod.inl ≫ p ≫ biprod.fst)
  (IsIso.inv_hom_id (biprod.map f g))
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝ : IsIso (biprod.map f g)
t : biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst ≫ f = biprod.inl ≫ biprod.fst
⊢ (biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst) ≫ f = 𝟙 Y
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝ : IsIso (biprod.map f g)
t :
  (fun p => biprod.inl ≫ p ≫ biprod.fst) (inv (biprod.map f g) ≫ biprod.map f g) =
    (fun p => biprod.inl ≫ p ≫ biprod.fst) (𝟙 (Y ⊞ Z))
⊢ (biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst) ≫ f = 𝟙 Y
simp only [Category.id_comp, Category.assoc, biprod.map_fst] at t
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝ : IsIso (biprod.map f g)
t : biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst ≫ f = biprod.inl ≫ biprod.fst
⊢ biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst ≫ f = 𝟙 Y
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝ : IsIso (biprod.map f g)
t : biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst ≫ f = biprod.inl ≫ biprod.fst
⊢ (biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst) ≫ f = 𝟙 Y
simp only [Category.assoc]
no goals
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝ : IsIso (biprod.map f g)
t : biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst ≫ f = biprod.inl ≫ biprod.fst
⊢ biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst ≫ f = 𝟙 Y
simp [t]