C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
⊢ IsIso f ↔ f ≠ 0
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
⊢ IsIso f ↔ f ≠ 0
haveI : Mono (f ≫ i.hom) := mono_comp _ _
case mp
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
⊢ IsIso f → f ≠ 0

case mpr
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
⊢ f ≠ 0 → IsIso f
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
⊢ IsIso f ↔ f ≠ 0
constructor
case mp
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : IsIso f
w : f = 0
⊢ False
case mp
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
⊢ IsIso f → f ≠ 0
intro h w
case j
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : IsIso f
w : f = 0
⊢ IsIso (f ≫ i.hom)

case mp
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : IsIso f
w : f = 0
j : IsIso (f ≫ i.hom)
⊢ False
case mp
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : IsIso f
w : f = 0
⊢ False
have j : IsIso (f ≫ i.hom)
case mp
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : IsIso f
w : f = 0
j : IsIso (f ≫ i.hom)
⊢ False
case j
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : IsIso f
w : f = 0
⊢ IsIso (f ≫ i.hom)

case mp
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : IsIso f
w : f = 0
j : IsIso (f ≫ i.hom)
⊢ False
infer_instance
case mp
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : IsIso f
w : f = 0
j✝ : IsIso (f ≫ i.hom)
j : f ≫ i.hom ≠ 0
⊢ False
case mp
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : IsIso f
w : f = 0
j : IsIso (f ≫ i.hom)
⊢ False
rw [Simple.mono_isIso_iff_nonzero] at j
case mp
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
m : Mono 0
this : Mono (0 ≫ i.hom)
h : IsIso 0
j✝ : IsIso (0 ≫ i.hom)
j : 0 ≫ i.hom ≠ 0
⊢ False
case mp
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : IsIso f
w : f = 0
j✝ : IsIso (f ≫ i.hom)
j : f ≫ i.hom ≠ 0
⊢ False
subst w
no goals
case mp
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
m : Mono 0
this : Mono (0 ≫ i.hom)
h : IsIso 0
j✝ : IsIso (0 ≫ i.hom)
j : 0 ≫ i.hom ≠ 0
⊢ False
simp at j
case mpr
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : f ≠ 0
⊢ IsIso f
case mpr
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
⊢ f ≠ 0 → IsIso f
intro h
case mpr
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : f ≠ 0
j : IsIso (f ≫ i.hom)
⊢ IsIso f
case mpr
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : f ≠ 0
⊢ IsIso f
have j : IsIso (f ≫ i.hom) := by
  apply isIso_of_mono_of_nonzero
  intro w
  apply h
  simpa using (cancel_mono i.inv).2 w
case mpr
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : f ≠ 0
j : IsIso (f ≫ i.hom)
⊢ IsIso ((f ≫ i.hom) ≫ i.inv)
case mpr
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : f ≠ 0
j : IsIso (f ≫ i.hom)
⊢ IsIso f
rw [← Category.comp_id f, ← i.hom_inv_id, ← Category.assoc]
no goals
case mpr
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : f ≠ 0
j : IsIso (f ≫ i.hom)
⊢ IsIso ((f ≫ i.hom) ≫ i.inv)
infer_instance
case w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : f ≠ 0
⊢ f ≫ i.hom ≠ 0
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : f ≠ 0
⊢ IsIso (f ≫ i.hom)
apply isIso_of_mono_of_nonzero
case w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : f ≠ 0
w : f ≫ i.hom = 0
⊢ False
case w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : f ≠ 0
⊢ f ≫ i.hom ≠ 0
intro w
case w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : f ≠ 0
w : f ≫ i.hom = 0
⊢ f = 0
case w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : f ≠ 0
w : f ≫ i.hom = 0
⊢ False
apply h
no goals
case w
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : f ≠ 0
w : f ≫ i.hom = 0
⊢ f = 0
simpa using (cancel_mono i.inv).2 w