case mp
C : Type u_3
inst✝⁹ : Category C
inst✝⁸ : Preadditive C
𝕜 : Type u_1
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) = 1 → Nonempty (X ≅ Y)

case mpr
C : Type u_3
inst✝⁹ : Category C
inst✝⁸ : Preadditive C
𝕜 : Type u_1
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ Nonempty (X ≅ Y) → finrank 𝕜 (X ⟶ Y) = 1
C : Type u_3
inst✝⁹ : Category C
inst✝⁸ : Preadditive C
𝕜 : Type u_1
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) = 1 ↔ Nonempty (X ≅ Y)
fconstructor
case mp
C : Type u_3
inst✝⁹ : Category C
inst✝⁸ : Preadditive C
𝕜 : Type u_1
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
h : finrank 𝕜 (X ⟶ Y) = 1
⊢ Nonempty (X ≅ Y)
case mp
C : Type u_3
inst✝⁹ : Category C
inst✝⁸ : Preadditive C
𝕜 : Type u_1
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) = 1 → Nonempty (X ≅ Y)
intro h
case mp
C : Type u_3
inst✝⁹ : Category C
inst✝⁸ : Preadditive C
𝕜 : Type u_1
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
h : ∃ v _n, ∀ (w : X ⟶ Y), ∃ c, c • v = w
⊢ Nonempty (X ≅ Y)
case mp
C : Type u_3
inst✝⁹ : Category C
inst✝⁸ : Preadditive C
𝕜 : Type u_1
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
h : finrank 𝕜 (X ⟶ Y) = 1
⊢ Nonempty (X ≅ Y)
rw [finrank_eq_one_iff'] at h
case mp.intro.intro
C : Type u_3
inst✝⁹ : Category C
inst✝⁸ : Preadditive C
𝕜 : Type u_1
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ⟶ Y
nz : f ≠ 0
⊢ Nonempty (X ≅ Y)
case mp
C : Type u_3
inst✝⁹ : Category C
inst✝⁸ : Preadditive C
𝕜 : Type u_1
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
h : ∃ v _n, ∀ (w : X ⟶ Y), ∃ c, c • v = w
⊢ Nonempty (X ≅ Y)
obtain ⟨f, nz, -⟩ := h
case mp.intro.intro
C : Type u_3
inst✝⁹ : Category C
inst✝⁸ : Preadditive C
𝕜 : Type u_1
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ⟶ Y
nz : IsIso f
⊢ Nonempty (X ≅ Y)
case mp.intro.intro
C : Type u_3
inst✝⁹ : Category C
inst✝⁸ : Preadditive C
𝕜 : Type u_1
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ⟶ Y
nz : f ≠ 0
⊢ Nonempty (X ≅ Y)
rw [← isIso_iff_nonzero] at nz
no goals
case mp.intro.intro
C : Type u_3
inst✝⁹ : Category C
inst✝⁸ : Preadditive C
𝕜 : Type u_1
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ⟶ Y
nz : IsIso f
⊢ Nonempty (X ≅ Y)
exact ⟨asIso f⟩
case mpr.intro
C : Type u_3
inst✝⁹ : Category C
inst✝⁸ : Preadditive C
𝕜 : Type u_1
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ≅ Y
⊢ finrank 𝕜 (X ⟶ Y) = 1
case mpr
C : Type u_3
inst✝⁹ : Category C
inst✝⁸ : Preadditive C
𝕜 : Type u_1
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ Nonempty (X ≅ Y) → finrank 𝕜 (X ⟶ Y) = 1
rintro ⟨f⟩
case mpr.intro
C : Type u_3
inst✝⁹ : Category C
inst✝⁸ : Preadditive C
𝕜 : Type u_1
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ≅ Y
le_one : finrank 𝕜 (X ⟶ Y) ≤ 1
⊢ finrank 𝕜 (X ⟶ Y) = 1
case mpr.intro
C : Type u_3
inst✝⁹ : Category C
inst✝⁸ : Preadditive C
𝕜 : Type u_1
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ≅ Y
⊢ finrank 𝕜 (X ⟶ Y) = 1
have le_one := finrank_hom_simple_simple_le_one 𝕜 X Y
case mpr.intro
C : Type u_3
inst✝⁹ : Category C
inst✝⁸ : Preadditive C
𝕜 : Type u_1
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ≅ Y
le_one : finrank 𝕜 (X ⟶ Y) ≤ 1
zero_lt : 0 < finrank 𝕜 (X ⟶ Y)
⊢ finrank 𝕜 (X ⟶ Y) = 1
case mpr.intro
C : Type u_3
inst✝⁹ : Category C
inst✝⁸ : Preadditive C
𝕜 : Type u_1
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ≅ Y
le_one : finrank 𝕜 (X ⟶ Y) ≤ 1
⊢ finrank 𝕜 (X ⟶ Y) = 1
have zero_lt : 0 < finrank 𝕜 (X ⟶ Y) :=
  finrank_pos_iff_exists_ne_zero.mpr ⟨f.hom, (isIso_iff_nonzero f.hom).mp inferInstance⟩
no goals
case mpr.intro
C : Type u_3
inst✝⁹ : Category C
inst✝⁸ : Preadditive C
𝕜 : Type u_1
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ≅ Y
le_one : finrank 𝕜 (X ⟶ Y) ≤ 1
zero_lt : 0 < finrank 𝕜 (X ⟶ Y)
⊢ finrank 𝕜 (X ⟶ Y) = 1
linarith