C : Type u_2
inst✝⁶ : Category C
inst✝⁵ : Preadditive C
𝕜 : Type u_3
inst✝⁴ : DivisionRing 𝕜
inst✝³ : HasKernels C
inst✝² : Linear 𝕜 C
X Y : C
inst✝¹ : Simple X
inst✝ : Simple Y
h : (X ≅ Y) → False
f : X ⟶ Y
p : ¬IsIso f ↔ ¬f ≠ 0
⊢ f = 0
C : Type u_2
inst✝⁶ : Category C
inst✝⁵ : Preadditive C
𝕜 : Type u_3
inst✝⁴ : DivisionRing 𝕜
inst✝³ : HasKernels C
inst✝² : Linear 𝕜 C
X Y : C
inst✝¹ : Simple X
inst✝ : Simple Y
h : (X ≅ Y) → False
f : X ⟶ Y
⊢ f = 0
have p := not_congr (isIso_iff_nonzero f)
C : Type u_2
inst✝⁶ : Category C
inst✝⁵ : Preadditive C
𝕜 : Type u_3
inst✝⁴ : DivisionRing 𝕜
inst✝³ : HasKernels C
inst✝² : Linear 𝕜 C
X Y : C
inst✝¹ : Simple X
inst✝ : Simple Y
h : (X ≅ Y) → False
f : X ⟶ Y
p : ¬IsIso f ↔ f = 0
⊢ f = 0
C : Type u_2
inst✝⁶ : Category C
inst✝⁵ : Preadditive C
𝕜 : Type u_3
inst✝⁴ : DivisionRing 𝕜
inst✝³ : HasKernels C
inst✝² : Linear 𝕜 C
X Y : C
inst✝¹ : Simple X
inst✝ : Simple Y
h : (X ≅ Y) → False
f : X ⟶ Y
p : ¬IsIso f ↔ ¬f ≠ 0
⊢ f = 0
simp only [Classical.not_not, Ne.def] at p
no goals
C : Type u_2
inst✝⁶ : Category C
inst✝⁵ : Preadditive C
𝕜 : Type u_3
inst✝⁴ : DivisionRing 𝕜
inst✝³ : HasKernels C
inst✝² : Linear 𝕜 C
X Y : C
inst✝¹ : Simple X
inst✝ : Simple Y
h : (X ≅ Y) → False
f : X ⟶ Y
p : ¬IsIso f ↔ f = 0
⊢ f = 0
refine' p.mp fun _ => h (asIso f)