C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : mk f = ⊤
⊢ IsIso (ofMkLEMk f (𝟙 Y) (_ : mk f ≤ ⊤))
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : mk f = ⊤
⊢ IsIso f
rw [← ofMkLEMk_comp h.le, Category.comp_id]
no goals
C : Type u₁
inst✝² : Category C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category D
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : mk f = ⊤
⊢ IsIso (ofMkLEMk f (𝟙 Y) (_ : mk f ≤ ⊤))
exact IsIso.of_iso (isoOfMkEqMk _ _ h)