awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
inst_3 : Projective.{v, u} Z
n : ℕ
succ : IsZero.{v, u} (X.{v, u, 0} (Functor.obj (single₀ C) Z) (n + 1))
⊢ Projective.{v, u} (X.{v, u, 0} (Functor.obj (single₀ C) Z) (n + 1))

Tactic:
apply IsZero.projective

Premises used: CategoryTheory.Limits.IsZero.projective
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
inst_3 : Projective.{v, u} Z
n : ℕ
succ : n + 1 ≠ 0
⊢ IsZero.{v, u} (X.{v, u, 0} (Functor.obj (single₀ C) Z) (n + 1))

Tactic:
apply HomologicalComplex.isZero_single_obj_X

Premises used: HomologicalComplex.isZero_single_obj_X
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
P : ProjectiveResolution.{v, u} Z
inst_3 : Projective.{v, u} Z
n : ℕ
⊢ n + 1 ≠ 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasKernels.{v_1, u_1} C
X Y : C
inst_3 : Simple.{v_1, u_1} X
f : X ⟶ Y
w : f ≠ 0
⊢ Mono f

Tactic:
Preadditive.mono_of_kernel_zero (kernel_zero_of_nonzero_from_simple w)

Premises used: CategoryTheory.kernel_zero_of_nonzero_from_simple, CategoryTheory.Preadditive.mono_of_kernel_zero
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasKernels.{v_1, u_1} C
X Y : C
inst_3 : Simple.{v_1, u_1} X
inst_4 : Simple.{v_1, u_1} Y
f : X ⟶ Y
w : f ≠ 0
⊢ IsIso f

Tactic:
haveI := mono_of_nonzero_from_simple w
  isIso_of_mono_of_nonzero w

Premises used: CategoryTheory.isIso_of_mono_of_nonzero
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasKernels.{v_1, u_1} C
X Y : C
inst_3 : Simple.{v_1, u_1} X
inst_4 : Simple.{v_1, u_1} Y
f : X ⟶ Y
I : IsIso f
h : f = 0
apply : Eq.{v_1 + 1} (α := X ⟶ X) (𝟙 X) 0
⊢ False

Tactic:
apply id_nonzero X

Premises used: CategoryTheory.id_nonzero
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasKernels.{v_1, u_1} C
X Y : C
inst_3 : Simple.{v_1, u_1} X
inst_4 : Simple.{v_1, u_1} Y
f : X ⟶ Y
I : IsIso f
h : f = 0
⊢ Eq.{v_1 + 1} (α := X ⟶ X) (𝟙 X) 0

Tactic:
simp only [← IsIso.hom_inv_id f, h, zero_comp]

Premises used: CategoryTheory.IsIso.hom_inv_id, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasKernels.{v_1, u_1} C
X : C
inst_3 : Simple.{v_1, u_1} X
f : End X
hf : f ≠ 0
dsimp : (if h : f = 0 then 0 else inv f) ≫ f = 𝟙 X
⊢ (f * if h : f = 0 then 0 else inv f) = 1

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasKernels.{v_1, u_1} C
X : C
inst_3 : Simple.{v_1, u_1} X
f : End X
hf : f ≠ 0
rw : inv f ≫ f = 𝟙 X
⊢ (if h : f = 0 then 0 else inv f) ≫ f = 𝟙 X

Tactic:
rw [dif_neg hf]

Premises used: dif_neg
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasKernels.{v_1, u_1} C
X : C
inst_3 : Simple.{v_1, u_1} X
f : End X
hf : f ≠ 0
⊢ IsIso f

Tactic:
haveI := isIso_of_hom_simple hf
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasKernels.{v_1, u_1} C
X : C
inst_3 : Simple.{v_1, u_1} X
f : End X
hf : f ≠ 0
this : IsIso f
⊢ inv f ≫ f = 𝟙 X

Tactic:
IsIso.inv_hom_id f

Premises used: CategoryTheory.IsIso.inv_hom_id, CategoryTheory.End
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasKernels.{v_1, u_1} C
X : C
inst_3 : Simple.{v_1, u_1} X
f : End X
hf : f ≠ 0
this : IsIso f
⊢ inv f ≫ f = 𝟙 X

Tactic:
exact IsIso.inv_hom_id f

Premises used: CategoryTheory.IsIso.inv_hom_id
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : DivisionRing 𝕜
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
X Y : C
inst_5 : Simple.{v_1, u_1} X
inst_6 : Simple.{v_1, u_1} Y
h : ∀ (a : X ≅ Y), False
f : X ⟶ Y
⊢ ¬IsIso f ↔ ¬f ≠ 0

Tactic:
have p := not_congr (isIso_iff_nonzero f)
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : DivisionRing 𝕜
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
X Y : C
inst_5 : Simple.{v_1, u_1} X
inst_6 : Simple.{v_1, u_1} Y
h : ∀ (a : X ≅ Y), False
f : X ⟶ Y
p : ¬IsIso f ↔ ¬f ≠ 0
⊢ ¬IsIso f ↔ f = 0

Tactic:
simp only [Classical.not_not, Ne] at p

Premises used: Classical.not_not, Ne
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : DivisionRing 𝕜
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
X Y : C
inst_5 : Simple.{v_1, u_1} X
inst_6 : Simple.{v_1, u_1} Y
h : ∀ (a : X ≅ Y), False
f : X ⟶ Y
p : ¬IsIso f ↔ f = 0
⊢ f = 0

Tactic:
p.mp fun _ => h (asIso f)

Premises used: Iff.mp, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : DivisionRing 𝕜
inst_3 : HasKernels.{v_1, u_1} C
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
X Y : C
inst_5 : Simple.{v_1, u_1} X
inst_6 : Simple.{v_1, u_1} Y
h : ∀ (a : X ≅ Y), False
f : X ⟶ Y
p : ¬IsIso f ↔ f = 0
⊢ f = 0

Tactic:
exact p.mp fun _ => h (asIso f)

Premises used: Iff.mp, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : IsAlgClosed 𝕜
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ X)
⊢ IsIso.{v_1, u_1} (𝟙 X)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : IsAlgClosed 𝕜
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ X)
⊢ Ne.{v_1 + 1} (α := X ⟶ X) (𝟙 X) 0

Tactic:
have id_nonzero := (isIso_iff_nonzero (𝟙 X)).mp (by infer_instance)
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : IsAlgClosed 𝕜
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ X)
id_nonzero : Ne.{v_1 + 1} (α := X ⟶ X) (𝟙 X) 0
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ X) = 1

Tactic:
finrank_eq_one (𝟙 X) id_nonzero ?_

Premises used: CategoryTheory.CategoryStruct.id, finrank_eq_one
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : IsAlgClosed 𝕜
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ X)
id_nonzero : Ne.{v_1 + 1} (α := X ⟶ X) (𝟙 X) 0
refine : ∀ (w : X ⟶ X), ∃ (c : 𝕜), HSMul.hSMul (β := X ⟶ X) c (𝟙 X) = w
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ X) = 1

Tactic:
refine finrank_eq_one (𝟙 X) id_nonzero ?_

Premises used: CategoryTheory.CategoryStruct.id, finrank_eq_one
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : IsAlgClosed 𝕜
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ X)
id_nonzero : Ne.{v_1 + 1} (α := X ⟶ X) (𝟙 X) 0
f : X ⟶ X
⊢ Nontrivial.{v_1} (End X)

Tactic:
have : Nontrivial (End X) := nontrivial_of_ne _ _ id_nonzero
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : IsAlgClosed 𝕜
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ X)
id_nonzero : Ne.{v_1 + 1} (α := X ⟶ X) (𝟙 X) 0
f : X ⟶ X
this : Nontrivial.{v_1} (End X)
⊢ FiniteDimensional.{u_2, v_1} 𝕜 (End X)

Tactic:
have : FiniteDimensional 𝕜 (End X) := I
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : IsAlgClosed 𝕜
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ X)
id_nonzero : Ne.{v_1 + 1} (α := X ⟶ X) (𝟙 X) 0
f : X ⟶ X
this_1 : Nontrivial.{v_1} (End X)
this : FiniteDimensional.{u_2, v_1} 𝕜 (End X)
obtain : ∀ (c : 𝕜) (nu : c ∈ spectrum 𝕜 (End.of f)), ∃ (c : 𝕜), HSMul.hSMul (β := X ⟶ X) c (𝟙 X) = f
⊢ ∃ (c : 𝕜), HSMul.hSMul (β := X ⟶ X) c (𝟙 X) = f

Tactic:
obtain ⟨c, nu⟩ := spectrum.nonempty_of_isAlgClosed_of_finiteDimensional 𝕜 (End.of f)

Premises used: spectrum.nonempty_of_isAlgClosed_of_finiteDimensional, CategoryTheory.End.of
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : IsAlgClosed 𝕜
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ X)
id_nonzero : Ne.{v_1 + 1} (α := X ⟶ X) (𝟙 X) 0
f : X ⟶ X
this_1 : Nontrivial.{v_1} (End X)
this : FiniteDimensional.{u_2, v_1} 𝕜 (End X)
c : 𝕜
nu : c ∈ spectrum 𝕜 (End.of f)
h : HSMul.hSMul (β := X ⟶ X) c (𝟙 X) = f
⊢ ∃ (c : 𝕜), HSMul.hSMul (β := X ⟶ X) c (𝟙 X) = f

Tactic:
use c
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : IsAlgClosed 𝕜
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ X)
id_nonzero : Ne.{v_1 + 1} (α := X ⟶ X) (𝟙 X) 0
f : X ⟶ X
this_1 : Nontrivial.{v_1} (End X)
this : FiniteDimensional.{u_2, v_1} 𝕜 (End X)
c : 𝕜
nu : c ∈ spectrum 𝕜 (End.of f)
⊢ End.of f = HSMul.hSMul (β := End X) c 1

Tactic:
rw [spectrum.mem_iff, IsUnit.sub_iff, isUnit_iff_isIso, isIso_iff_nonzero, Ne,
    Classical.not_not, sub_eq_zero, Algebra.algebraMap_eq_smul_one] at nu

Premises used: Classical.not_not, sub_eq_zero, CategoryTheory.isUnit_iff_isIso, IsUnit.sub_iff, Ne, Algebra.algebraMap_eq_smul_one, spectrum.mem_iff
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : IsAlgClosed 𝕜
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ X)
id_nonzero : Ne.{v_1 + 1} (α := X ⟶ X) (𝟙 X) 0
f : X ⟶ X
this_1 : Nontrivial.{v_1} (End X)
this : FiniteDimensional.{u_2, v_1} 𝕜 (End X)
c : 𝕜
nu : End.of f = HSMul.hSMul (β := End X) c 1
⊢ HSMul.hSMul (β := X ⟶ X) c (𝟙 X) = f

Tactic:
nu.symm

Premises used: Eq.symm
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : IsAlgClosed 𝕜
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ X)
id_nonzero : Ne.{v_1 + 1} (α := X ⟶ X) (𝟙 X) 0
f : X ⟶ X
this_1 : Nontrivial.{v_1} (End X)
this : FiniteDimensional.{u_2, v_1} 𝕜 (End X)
c : 𝕜
nu : End.of f = HSMul.hSMul (β := End X) c 1
⊢ HSMul.hSMul (β := X ⟶ X) c (𝟙 X) = f

Tactic:
exact nu.symm

Premises used: Eq.symm
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : IsAlgClosed 𝕜
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
inst_5 : HasKernels.{v_1, u_1} C
X : C
inst_6 : Simple.{v_1, u_1} X
inst_7 : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ X)
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ X) = 1

Tactic:
finrank_endomorphism_eq_one 𝕜 isIso_iff_nonzero

Premises used: CategoryTheory.finrank_endomorphism_eq_one, CategoryTheory.isIso_iff_nonzero
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : IsAlgClosed 𝕜
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
inst_5 : HasKernels.{v_1, u_1} C
X : C
inst_6 : Simple.{v_1, u_1} X
inst_7 : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ X)
f : X ⟶ X
⊢ ∃ (c : 𝕜), HSMul.hSMul (β := X ⟶ X) c (𝟙 X) = f

Tactic:
(finrank_eq_one_iff_of_nonzero' (𝟙 X) (id_nonzero X)).mp (finrank_endomorphism_simple_eq_one 𝕜 X)
    f

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.id_nonzero, Iff.mp, CategoryTheory.finrank_endomorphism_simple_eq_one, finrank_eq_one_iff_of_nonzero'
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : IsAlgClosed 𝕜
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
inst_5 : HasKernels.{v_1, u_1} C
X : C
inst_6 : Simple.{v_1, u_1} X
I : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ X)
f g : End X
obtain : ∀ (c : 𝕜), HSMul.hSMul (β := X ⟶ X) c (𝟙 X) * g = g * HSMul.hSMul (β := X ⟶ X) c (𝟙 X)
⊢ f * g = g * f

Tactic:
obtain ⟨c, rfl⟩ := endomorphism_simple_eq_smul_id 𝕜 f

Premises used: CategoryTheory.endomorphism_simple_eq_smul_id, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : IsAlgClosed 𝕜
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
inst_5 : HasKernels.{v_1, u_1} C
X : C
inst_6 : Simple.{v_1, u_1} X
I : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ X)
g : End X
c : 𝕜
obtain :
  ∀ (d : 𝕜),
    HSMul.hSMul (β := X ⟶ X) c (𝟙 X) * HSMul.hSMul (β := X ⟶ X) d (𝟙 X) =
      HSMul.hSMul (β := X ⟶ X) d (𝟙 X) * HSMul.hSMul (β := X ⟶ X) c (𝟙 X)
⊢ HSMul.hSMul (β := X ⟶ X) c (𝟙 X) * g = g * HSMul.hSMul (β := X ⟶ X) c (𝟙 X)

Tactic:
obtain ⟨d, rfl⟩ := endomorphism_simple_eq_smul_id 𝕜 g

Premises used: CategoryTheory.endomorphism_simple_eq_smul_id, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : IsAlgClosed 𝕜
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
inst_5 : HasKernels.{v_1, u_1} C
X : C
inst_6 : Simple.{v_1, u_1} X
I : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ X)
c d : 𝕜
⊢ HSMul.hSMul (β := X ⟶ X) c (𝟙 X) * HSMul.hSMul (β := X ⟶ X) d (𝟙 X) =
    HSMul.hSMul (β := X ⟶ X) d (𝟙 X) * HSMul.hSMul (β := X ⟶ X) c (𝟙 X)

Tactic:
simp [← mul_smul, mul_comm c d]

Premises used: mul_comm, SemigroupAction.mul_smul
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : IsAlgClosed 𝕜
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
inst_5 : HasKernels.{v_1, u_1} C
X : C
inst_6 : Simple.{v_1, u_1} X
I : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ X)
⊢ Field (End X)

Tactic:
exact
    { (inferInstance : DivisionRing (End X)) with
      mul_comm := fun f g => by
        obtain ⟨c, rfl⟩ := endomorphism_simple_eq_smul_id 𝕜 f
        obtain ⟨d, rfl⟩ := endomorphism_simple_eq_smul_id 𝕜 g
        simp [← mul_smul, mul_comm c d] }

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : IsAlgClosed 𝕜
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
inst_5 : HasKernels.{v_1, u_1} C
X : C
inst_6 : Simple.{v_1, u_1} X
I : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ X)
⊢ Field (End X)

Tactic:
classical exact
    { (inferInstance : DivisionRing (End X)) with
      mul_comm := fun f g => by
        obtain ⟨c, rfl⟩ := endomorphism_simple_eq_smul_id 𝕜 f
        obtain ⟨d, rfl⟩ := endomorphism_simple_eq_smul_id 𝕜 g
        simp [← mul_smul, mul_comm c d] }

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : IsAlgClosed 𝕜
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
inst_5 : HasKernels.{v_1, u_1} C
X Y : C
inst_6 : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ X)
inst_7 : Simple.{v_1, u_1} X
inst_8 : Simple.{v_1, u_1} Y
inl : ∀ (h : Subsingleton.{v_1 + 1} (X ⟶ Y)), finrank.{u_2, v_1} 𝕜 (X ⟶ Y) ≤ 1
inr : ∀ (h : Nontrivial.{v_1} (X ⟶ Y)), finrank.{u_2, v_1} 𝕜 (X ⟶ Y) ≤ 1
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ Y) ≤ 1

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

Premises used: Quiver.Hom, subsingleton_or_nontrivial
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : IsAlgClosed 𝕜
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
inst_5 : HasKernels.{v_1, u_1} C
X Y : C
inst_6 : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ X)
inst_7 : Simple.{v_1, u_1} X
inst_8 : Simple.{v_1, u_1} Y
h : Subsingleton.{v_1 + 1} (X ⟶ Y)
inl : LE.le (α := ℕ) 0 1
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ Y) ≤ 1

Tactic:
rw [finrank_zero_of_subsingleton]

Premises used: Module.finrank_zero_of_subsingleton
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : IsAlgClosed 𝕜
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
inst_5 : HasKernels.{v_1, u_1} C
X Y : C
inst_6 : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ X)
inst_7 : Simple.{v_1, u_1} X
inst_8 : Simple.{v_1, u_1} Y
h : Subsingleton.{v_1 + 1} (X ⟶ Y)
⊢ LE.le (α := ℕ) 0 1

Tactic:
zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : IsAlgClosed 𝕜
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
inst_5 : HasKernels.{v_1, u_1} C
X Y : C
inst_6 : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ X)
inst_7 : Simple.{v_1, u_1} X
inst_8 : Simple.{v_1, u_1} Y
h : Subsingleton.{v_1 + 1} (X ⟶ Y)
⊢ LE.le (α := ℕ) 0 1

Tactic:
exact zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : IsAlgClosed 𝕜
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
inst_5 : HasKernels.{v_1, u_1} C
X Y : C
inst_6 : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ X)
inst_7 : Simple.{v_1, u_1} X
inst_8 : Simple.{v_1, u_1} Y
h : Nontrivial.{v_1} (X ⟶ Y)
inr : ∀ (f : X ⟶ Y) (nz : f ≠ 0), finrank.{u_2, v_1} 𝕜 (X ⟶ Y) ≤ 1
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ Y) ≤ 1

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

Premises used: nontrivial_iff_exists_ne, Iff.mp, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : IsAlgClosed 𝕜
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
inst_5 : HasKernels.{v_1, u_1} C
X Y : C
inst_6 : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ X)
inst_7 : Simple.{v_1, u_1} X
inst_8 : Simple.{v_1, u_1} Y
h : Nontrivial.{v_1} (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
⊢ IsIso f

Tactic:
haveI fi := (isIso_iff_nonzero f).mpr nz
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : IsAlgClosed 𝕜
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
inst_5 : HasKernels.{v_1, u_1} C
X Y : C
inst_6 : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ X)
inst_7 : Simple.{v_1, u_1} X
inst_8 : Simple.{v_1, u_1} Y
h : Nontrivial.{v_1} (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
fi : IsIso f
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ Y) ≤ 1

Tactic:
finrank_le_one f ?_

Premises used: finrank_le_one
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : IsAlgClosed 𝕜
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
inst_5 : HasKernels.{v_1, u_1} C
X Y : C
inst_6 : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ X)
inst_7 : Simple.{v_1, u_1} X
inst_8 : Simple.{v_1, u_1} Y
h : Nontrivial.{v_1} (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
fi : IsIso f
inr : ∀ (w : X ⟶ Y), ∃ (c : 𝕜), c • f = w
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ Y) ≤ 1

Tactic:
refine finrank_le_one f ?_

Premises used: finrank_le_one
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : IsAlgClosed 𝕜
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
inst_5 : HasKernels.{v_1, u_1} C
X Y : C
inst_6 : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ X)
inst_7 : Simple.{v_1, u_1} X
inst_8 : Simple.{v_1, u_1} Y
h : Nontrivial.{v_1} (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
fi : IsIso f
g : X ⟶ Y
inr : ∀ (c : 𝕜) (w : HSMul.hSMul (β := X ⟶ X) c (𝟙 X) = g ≫ inv f), ∃ (c : 𝕜), c • f = g
⊢ ∃ (c : 𝕜), c • f = g

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

Premises used: CategoryTheory.endomorphism_simple_eq_smul_id, CategoryTheory.CategoryStruct.comp, CategoryTheory.inv
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : IsAlgClosed 𝕜
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
inst_5 : HasKernels.{v_1, u_1} C
X Y : C
inst_6 : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ X)
inst_7 : Simple.{v_1, u_1} X
inst_8 : Simple.{v_1, u_1} Y
h : Nontrivial.{v_1} (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
fi : IsIso f
g : X ⟶ Y
c : 𝕜
w : HSMul.hSMul (β := X ⟶ X) c (𝟙 X) = g ≫ inv f
⊢ c • f = g

Tactic:
simpa using w =≫ f
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : IsAlgClosed 𝕜
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
inst_5 : HasKernels.{v_1, u_1} C
X Y : C
inst_6 : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ X)
inst_7 : Simple.{v_1, u_1} X
inst_8 : Simple.{v_1, u_1} Y
h : Nontrivial.{v_1} (X ⟶ Y)
f : X ⟶ Y
nz : f ≠ 0
fi : IsIso f
g : X ⟶ Y
c : 𝕜
w : HSMul.hSMul (β := X ⟶ X) c (𝟙 X) = g ≫ inv f
⊢ ∃ (c : 𝕜), c • f = g

Tactic:
exact ⟨c, by simpa using w =≫ f⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Schur
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
𝕜 : Type u_2
inst_2 : Field 𝕜
inst_3 : IsAlgClosed 𝕜
inst_4 : Linear.{u_2, v_1, u_1} 𝕜 C
inst_5 : HasKernels.{v_1, u_1} C
X Y : C
inst_6 : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ X)
inst_7 : FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ Y)
inst_8 : Simple.{v_1, u_1} X
inst_9 : Simple.{v_1, u_1} Y
mp : finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = 1 → Nonempty.{v_1 + 1} (X ≅ Y)
mpr : Nonempty.{v_1 + 1} (X ≅ Y) → finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = 1
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = 1 ↔ Nonempty.{v_1 + 1} (X ≅ Y)

Tactic:
fconstructor