awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Resolution (goal)
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 : ℕ
zero : Projective.{v, u} (X.{v, u, 0} (Functor.obj (single₀ C) Z) 0)
⊢ Projective.{v, u} (X.{v, u, 0} (Functor.obj (single₀ C) Z) n)
have succ : ∀ (n : ℕ), Projective.{v, u} (X.{v, u, 0} (Functor.obj (single₀ C) Z) (n + 1))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Resolution (goal)
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 : ℕ
⊢ Projective.{v, u} (X.{v, u, 0} (Functor.obj (single₀ C) Z) (n + 1))
have succ : IsZero.{v, u} (X.{v, u, 0} (Functor.obj (single₀ C) Z) (n + 1))
Tactic: apply IsZero.projective
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Projective.Resolution (goal)
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 : ℕ
⊢ IsZero.{v, u} (X.{v, u, 0} (Functor.obj (single₀ C) Z) (n + 1))
have succ : n + 1 ≠ 0
Tactic: apply HomologicalComplex.isZero_single_obj_X
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (goal)
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
⊢ False
have apply : Eq.{v_1 + 1} (α := X ⟶ X) (𝟙 X) 0
Tactic: apply id_nonzero X
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (goal)
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
⊢ (f * if h : f = 0 then 0 else inv f) = 1
have dsimp : (if h : f = 0 then 0 else inv f) ≫ f = 𝟙 X
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (goal)
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
⊢ (if h : f = 0 then 0 else inv f) ≫ f = 𝟙 X
have rw : inv f ≫ f = 𝟙 X
Tactic: rw [dif_neg hf]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (hypothesis)
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
⊢ inv f ≫ f = 𝟙 X
have this : IsIso f
Tactic: haveI := isIso_of_hom_simple hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (hypothesis)
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
⊢ f = 0
have p : ¬IsIso f ↔ ¬f ≠ 0
Tactic: have p := not_congr (isIso_iff_nonzero f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (hypothesis)
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
have p₁ : ¬IsIso f ↔ f = 0
Tactic: simp only [Classical.not_not, Ne] at p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (hypothesis)
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)
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ X) = 1
have id_nonzero : Ne.{v_1 + 1} (α := X ⟶ X) (𝟙 X) 0
Tactic: have id_nonzero := (isIso_iff_nonzero (𝟙 X)).mp (by infer_instance)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (goal)
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
have refine : ∀ (w : X ⟶ X), ∃ (c : 𝕜), HSMul.hSMul (β := X ⟶ X) c (𝟙 X) = w
Tactic: refine finrank_eq_one (𝟙 X) id_nonzero ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (hypothesis)
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
⊢ ∃ (c : 𝕜), HSMul.hSMul (β := X ⟶ X) c (𝟙 X) = f
have this : Nontrivial.{v_1} (End X)
Tactic: have : Nontrivial (End X) := nontrivial_of_ne _ _ id_nonzero
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (hypothesis)
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)
⊢ ∃ (c : 𝕜), HSMul.hSMul (β := X ⟶ X) c (𝟙 X) = f
have this₁ : FiniteDimensional.{u_2, v_1} 𝕜 (End X)
Tactic: have : FiniteDimensional 𝕜 (End X) := I
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (goal)
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 : 𝕜), HSMul.hSMul (β := X ⟶ X) c (𝟙 X) = f
have obtain : ∀ (c : 𝕜) (nu : c ∈ spectrum 𝕜 (End.of f)), ∃ (c : 𝕜), HSMul.hSMul (β := X ⟶ X) c (𝟙 X) = f
Tactic: obtain ⟨c, nu⟩ := spectrum.nonempty_of_isAlgClosed_of_finiteDimensional 𝕜 (End.of f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (goal)
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)
⊢ ∃ (c : 𝕜), HSMul.hSMul (β := X ⟶ X) c (𝟙 X) = f
have h : HSMul.hSMul (β := X ⟶ X) c (𝟙 X) = f
Tactic: use c
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (hypothesis)
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)
⊢ HSMul.hSMul (β := X ⟶ X) c (𝟙 X) = f
have nu₁ : 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
Cleared hypotheses: nu
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (goal)
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
⊢ f * g = g * f
have obtain : ∀ (c : 𝕜), HSMul.hSMul (β := X ⟶ X) c (𝟙 X) * g = g * HSMul.hSMul (β := X ⟶ X) c (𝟙 X)
Tactic: obtain ⟨c, rfl⟩ := endomorphism_simple_eq_smul_id 𝕜 f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (goal)
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 : 𝕜
⊢ HSMul.hSMul (β := X ⟶ X) c (𝟙 X) * g = g * HSMul.hSMul (β := X ⟶ X) c (𝟙 X)
have 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)
Tactic: obtain ⟨d, rfl⟩ := endomorphism_simple_eq_smul_id 𝕜 g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (goal)
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
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ Y) ≤ 1
have inl : ∀ (h : Subsingleton.{v_1 + 1} (X ⟶ Y)), finrank.{u_2, v_1} 𝕜 (X ⟶ Y) ≤ 1
Tactic: obtain (h | h) := subsingleton_or_nontrivial (X ⟶ Y)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (goal)
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
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ Y) ≤ 1
have inr : ∀ (h : Nontrivial.{v_1} (X ⟶ Y)), finrank.{u_2, v_1} 𝕜 (X ⟶ Y) ≤ 1
Tactic: obtain (h | h) := subsingleton_or_nontrivial (X ⟶ Y)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (goal)
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)
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ Y) ≤ 1
have inl : LE.le (α := ℕ) 0 1
Tactic: rw [finrank_zero_of_subsingleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (goal)
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)
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ Y) ≤ 1
have inr : ∀ (f : X ⟶ Y) (nz : f ≠ 0), finrank.{u_2, v_1} 𝕜 (X ⟶ Y) ≤ 1
Tactic: obtain ⟨f, nz⟩ := (nontrivial_iff_exists_ne 0).mp h
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (hypothesis)
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
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ Y) ≤ 1
have fi : IsIso f
Tactic: haveI fi := (isIso_iff_nonzero f).mpr nz
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (goal)
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
have inr : ∀ (w : X ⟶ Y), ∃ (c : 𝕜), c • f = w
Tactic: refine finrank_le_one f ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (goal)
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 : 𝕜), c • f = g
have inr : ∀ (c : 𝕜) (w : HSMul.hSMul (β := X ⟶ X) c (𝟙 X) = g ≫ inv f), ∃ (c : 𝕜), c • f = g
Tactic: obtain ⟨c, w⟩ := endomorphism_simple_eq_smul_id 𝕜 (g ≫ inv f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (goal)
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
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = 1 ↔ Nonempty.{v_1 + 1} (X ≅ Y)
have mp : finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = 1 → Nonempty.{v_1 + 1} (X ≅ Y)
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (goal)
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)
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = 1 ↔ Nonempty.{v_1 + 1} (X ≅ Y)
have mpr : Nonempty.{v_1 + 1} (X ≅ Y) → finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = 1
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (hypothesis)
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
h : finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = 1
⊢ Nonempty.{v_1 + 1} (X ≅ Y)
have h₁ : ∃ (v : X ⟶ Y), v ≠ 0 ∧ ∀ (w : X ⟶ Y), ∃ (c : 𝕜), c • v = w
Tactic: rw [finrank_eq_one_iff'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (goal)
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
h : ∃ (v : X ⟶ Y), v ≠ 0 ∧ ∀ (w : X ⟶ Y), ∃ (c : 𝕜), c • v = w
⊢ Nonempty.{v_1 + 1} (X ≅ Y)
have mp : ∀ (f : X ⟶ Y) (nz : f ≠ 0), Nonempty.{v_1 + 1} (X ≅ Y)
Tactic: obtain ⟨f, nz, -⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (hypothesis)
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
f : X ⟶ Y
nz : f ≠ 0
⊢ Nonempty.{v_1 + 1} (X ≅ Y)
have nz₁ : IsIso f
Tactic: rw [← isIso_iff_nonzero] at nz
Cleared hypotheses: nz
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (hypothesis)
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
f : X ≅ Y
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = 1
have le_one : finrank.{u_2, v_1} 𝕜 (X ⟶ Y) ≤ 1
Tactic: have le_one := finrank_hom_simple_simple_le_one 𝕜 X Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (hypothesis)
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
f : X ≅ Y
le_one : finrank.{u_2, v_1} 𝕜 (X ⟶ Y) ≤ 1
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = 1
have zero_lt : 0 < finrank.{u_2, v_1} 𝕜 (X ⟶ Y)
Tactic: have zero_lt : 0 < finrank 𝕜 (X ⟶ Y) :=
      finrank_pos_iff_exists_ne_zero.mpr ⟨f.hom, (isIso_iff_nonzero f.hom).mp inferInstance⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (goal)
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
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = 0 ↔ IsEmpty.{v_1 + 1} (X ≅ Y)
have rw : finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = 0 ↔ ¬finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = 1
Tactic: rw [← not_nonempty_iff, ← not_congr (finrank_hom_simple_simple_eq_one_iff 𝕜 X Y)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (hypothesis)
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
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = 0 ↔ ¬finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = 1
have this : finrank.{u_2, v_1} 𝕜 (X ⟶ Y) ≤ 1
Tactic: have := finrank_hom_simple_simple_le_one 𝕜 X Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (goal)
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 : ∀ (X Y : C), FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ Y)
inst_7 : Simple.{v_1, u_1} X
inst_8 : Simple.{v_1, u_1} Y
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = if Nonempty.{v_1 + 1} (X ≅ Y) then 1 else 0
have pos : ∀ (h : Nonempty.{v_1 + 1} (X ≅ Y)), finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Schur (goal)
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 : ∀ (X Y : C), FiniteDimensional.{u_2, v_1} 𝕜 (X ⟶ Y)
inst_7 : Simple.{v_1, u_1} X
inst_8 : Simple.{v_1, u_1} Y
pos : ∀ (h : Nonempty.{v_1 + 1} (X ≅ Y)), finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = 1
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = if Nonempty.{v_1 + 1} (X ≅ Y) then 1 else 0
have neg : ∀ (h : ¬Nonempty.{v_1 + 1} (X ≅ Y)), finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Yoneda.Injective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : C
⊢ Injective.{v, u} J ↔ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj preadditiveYoneda J)
have rw : Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj yoneda J) ↔
  Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj preadditiveYoneda J)
Tactic: rw [injective_iff_preservesEpimorphisms_yoneda_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Yoneda.Injective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : C
⊢ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj yoneda J) ↔
    Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj preadditiveYoneda J)
have refine_1 : ∀
  (h :
    Functor.PreservesEpimorphisms
      (Functor.obj preadditiveYoneda J ⋙
        forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
          AddCommGrpCat.carrier))),
  Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj preadditiveYoneda J)
Tactic: refine
    ⟨fun h : (preadditiveYoneda.obj J ⋙ (forget AddCommGrpCat)).PreservesEpimorphisms => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Yoneda.Injective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : C
refine_1 :
  ∀
    (h :
      Functor.PreservesEpimorphisms
        (Functor.obj preadditiveYoneda J ⋙
          forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier))),
    Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj preadditiveYoneda J)
⊢ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj yoneda J) ↔
    Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj preadditiveYoneda J)
have refine_2 : Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj preadditiveYoneda J) →
  Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj yoneda J)
Tactic: refine
    ⟨fun h : (preadditiveYoneda.obj J ⋙ (forget AddCommGrpCat)).PreservesEpimorphisms => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Yoneda.Injective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : C
⊢ Injective.{v, u} J ↔ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End J)) (preadditiveYonedaObj J)
have rw : Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj yoneda J) ↔
  Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End J)) (preadditiveYonedaObj J)
Tactic: rw [injective_iff_preservesEpimorphisms_yoneda_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Yoneda.Injective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : C
⊢ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj yoneda J) ↔
    Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End J)) (preadditiveYonedaObj J)
have refine_1 : ∀
  (h :
    (preadditiveYonedaObj J ⋙
        forget (ModuleCat (End J)) (FC := fun (x1 x2 : ModuleCat (End J)) ↦
          LinearMap (R := End J) (RingHom.id (End J)) (↑x1 : Type v) (↑x2 : Type v)) (CC :=
          ModuleCat.carrier)).PreservesEpimorphisms),
  Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End J)) (preadditiveYonedaObj J)
Tactic: refine ⟨fun h : (preadditiveYonedaObj J ⋙ (forget <| ModuleCat (End J))).PreservesEpimorphisms =>
    ?_, ?_⟩