-- Mathlib/CategoryTheory/Preadditive/Schur.lean
theorem finrank_hom_simple_simple_le_one (X Y : C) [FiniteDimensional 𝕜 (X ⟶ X)] [Simple X]
    [Simple Y] : finrank 𝕜 (X ⟶ Y) ≤ 1

Proof state:
case inl
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Subsingleton (X ⟶ Y)
⊢ 0 ≤ 1

Tactic:
exact zero_le_one

Result:
no goals

Proof state:
case inr
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nontrivial (X ⟶ Y)
⊢ finrank 𝕜 (X ⟶ Y) ≤ 1

Tactic:
obtain ⟨f, nz⟩ := (nontrivial_iff_exists_ne 0).mp h

Result:
case inr.intro
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nontrivial (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
⊢ finrank 𝕜 (X ⟶ Y) ≤ 1

Proof state:
case inr.intro.intro
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nontrivial (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
fi : IsIso f
g : X ⟶ Y
c : 𝕜
w : c • 𝟙 X = g ≫ inv f
⊢ ∃ c, c • f = g

Tactic:
exact ⟨c, by simpa using w =≫ f⟩

Result:
no goals

Proof state:
case inr.intro
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nontrivial (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
fi : IsIso f
g : X ⟶ Y
⊢ ∃ c, c • f = g

Tactic:
obtain ⟨c, w⟩ := endomorphism_simple_eq_smul_id 𝕜 (g ≫ inv f)

Result:
case inr.intro.intro
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nontrivial (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
fi : IsIso f
g : X ⟶ Y
c : 𝕜
w : c • 𝟙 X = g ≫ inv f
⊢ ∃ c, c • f = g

Proof state:
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nontrivial (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
fi : IsIso f
g : X ⟶ Y
c : 𝕜
w : c • 𝟙 X = g ≫ inv f
⊢ c • f = g

Tactic:
simpa using w =≫ f

Result:
no goals

Proof state:
case inr.intro
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nontrivial (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
fi : IsIso f
⊢ ∀ (w : X ⟶ Y), ∃ c, c • f = w

Tactic:
intro g

Result:
case inr.intro
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nontrivial (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
fi : IsIso f
g : X ⟶ Y
⊢ ∃ c, c • f = g

Proof state:
case inl
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Subsingleton (X ⟶ Y)
⊢ finrank 𝕜 (X ⟶ Y) ≤ 1

Tactic:
rw [finrank_zero_of_subsingleton]

Result:
case inl
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Subsingleton (X ⟶ Y)
⊢ 0 ≤ 1

Proof state:
case inr.intro
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nontrivial (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
⊢ finrank 𝕜 (X ⟶ Y) ≤ 1

Tactic:
haveI fi := (isIso_iff_nonzero f).mpr nz

Result:
case inr.intro
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nontrivial (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
fi : IsIso f
⊢ finrank 𝕜 (X ⟶ Y) ≤ 1

Proof state:
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ finrank 𝕜 (X ⟶ Y) ≤ 1

Tactic:
obtain (h|h) := subsingleton_or_nontrivial (X ⟶ Y)

Result:
case inl
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Subsingleton (X ⟶ Y)
⊢ finrank 𝕜 (X ⟶ Y) ≤ 1

case inr
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nontrivial (X ⟶ Y)
⊢ finrank 𝕜 (X ⟶ Y) ≤ 1

Proof state:
case inr.intro
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nontrivial (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
fi : IsIso f
⊢ finrank 𝕜 (X ⟶ Y) ≤ 1

Tactic:
refine finrank_le_one f ?_

Result:
case inr.intro
C : Type u_1
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Preadditive C
𝕜 : Type u_2
inst✝⁶ : Field 𝕜
inst✝⁵ : IsAlgClosed 𝕜
inst✝⁴ : Linear 𝕜 C
inst✝³ : HasKernels C
X Y : C
inst✝² : FiniteDimensional 𝕜 (X ⟶ X)
inst✝¹ : Simple X
inst✝ : Simple Y
h : Nontrivial (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
fi : IsIso f
⊢ ∀ (w : X ⟶ Y), ∃ c, c • f = w