C : Type u
inst✝³ : Category C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : ¬IsZero Y
⊢ IsZero Z
C : Type u
inst✝³ : Category C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
⊢ IsZero Y ∨ IsZero Z
refine' or_iff_not_imp_left.mpr fun h => _
C : Type u
inst✝³ : Category C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : ¬biprod.inl = 0
⊢ IsZero Z
C : Type u
inst✝³ : Category C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : ¬IsZero Y
⊢ IsZero Z
rw [IsZero.iff_isSplitMono_eq_zero (biprod.inl : Y ⟶ Y ⊞ Z)] at h
C : Type u
inst✝³ : Category C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : biprod.inl ≠ 0
⊢ IsZero Z
C : Type u
inst✝³ : Category C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : ¬biprod.inl = 0
⊢ IsZero Z
change biprod.inl ≠ 0 at h
C : Type u
inst✝³ : Category C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : biprod.inl ≠ 0
this : Simple (Y ⊞ Z)
⊢ IsZero Z
C : Type u
inst✝³ : Category C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : biprod.inl ≠ 0
⊢ IsZero Z
have : Simple (Y ⊞ Z) := Simple.of_iso i.symm
C : Type u
inst✝³ : Category C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : IsIso biprod.inl
this : Simple (Y ⊞ Z)
⊢ IsZero Z
C : Type u
inst✝³ : Category C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : biprod.inl ≠ 0
this : Simple (Y ⊞ Z)
⊢ IsZero Z
rw [← Simple.mono_isIso_iff_nonzero biprod.inl] at h
no goals
C : Type u
inst✝³ : Category C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : IsIso biprod.inl
this : Simple (Y ⊞ Z)
⊢ IsZero Z
rwa [Biprod.isIso_inl_iff_isZero] at h