case mp
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ IsIso inl → 𝟙 (X ⊞ Y) = fst ≫ inl

case mpr
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ 𝟙 (X ⊞ Y) = fst ≫ inl → IsIso inl
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ IsIso inl ↔ 𝟙 (X ⊞ Y) = fst ≫ inl
constructor
case mp
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
h : IsIso inl
⊢ 𝟙 (X ⊞ Y) = fst ≫ inl
case mp
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ IsIso inl → 𝟙 (X ⊞ Y) = fst ≫ inl
intro h
case mp
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
h : IsIso inl
this : inv inl ≫ inl ≫ fst = inv inl ≫ 𝟙 X
⊢ 𝟙 (X ⊞ Y) = fst ≫ inl
case mp
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
h : IsIso inl
⊢ 𝟙 (X ⊞ Y) = fst ≫ inl
have := (cancel_epi (inv biprod.inl : X ⊞ Y ⟶ X)).2 <| @biprod.inl_fst _ _ _ X Y _
case mp
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
h : IsIso inl
this : fst = inv inl
⊢ 𝟙 (X ⊞ Y) = fst ≫ inl
case mp
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
h : IsIso inl
this : inv inl ≫ inl ≫ fst = inv inl ≫ 𝟙 X
⊢ 𝟙 (X ⊞ Y) = fst ≫ inl
rw [IsIso.inv_hom_id_assoc, Category.comp_id] at this
no goals
case mp
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
h : IsIso inl
this : fst = inv inl
⊢ 𝟙 (X ⊞ Y) = fst ≫ inl
rw [this, IsIso.inv_hom_id]
case mpr
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
h : 𝟙 (X ⊞ Y) = fst ≫ inl
⊢ IsIso inl
case mpr
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ 𝟙 (X ⊞ Y) = fst ≫ inl → IsIso inl
intro h
no goals
case mpr
J : Type w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
h : 𝟙 (X ⊞ Y) = fst ≫ inl
⊢ IsIso inl
exact ⟨⟨biprod.fst, biprod.inl_fst, h.symm⟩⟩