awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h : finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = 1
⊢ ∃ (v : X ⟶ Y), v ≠ 0 ∧ ∀ (w : X ⟶ Y), ∃ (c : 𝕜), c • v = w

Tactic:
rw [finrank_eq_one_iff'] at h

Premises used: finrank_eq_one_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
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
mp : ∀ (f : X ⟶ Y) (nz : f ≠ 0), Nonempty.{v_1 + 1} (X ≅ Y)
⊢ Nonempty.{v_1 + 1} (X ≅ Y)

Tactic:
obtain ⟨f, nz, -⟩ := h
-- 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
f : X ⟶ Y
nz : f ≠ 0
⊢ IsIso f

Tactic:
rw [← isIso_iff_nonzero] at nz

Premises used: 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 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 : IsIso f
⊢ Nonempty.{v_1 + 1} (X ≅ Y)

Tactic:
⟨asIso f⟩

Premises used: Nonempty.intro, 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
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 : IsIso f
⊢ Nonempty.{v_1 + 1} (X ≅ Y)

Tactic:
exact ⟨asIso 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
f : X ≅ Y
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ Y) ≤ 1

Tactic:
have le_one := finrank_hom_simple_simple_le_one 𝕜 X Y
-- 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
f : X ≅ Y
le_one : finrank.{u_2, v_1} 𝕜 (X ⟶ Y) ≤ 1
⊢ 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⟩
-- 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
f : X ≅ Y
le_one : finrank.{u_2, v_1} 𝕜 (X ⟶ Y) ≤ 1
zero_lt : 0 < finrank.{u_2, v_1} 𝕜 (X ⟶ Y)
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = 1

Tactic:
lia
-- 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
rw : finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = 0 ↔ ¬finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = 1
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = 0 ↔ IsEmpty.{v_1 + 1} (X ≅ Y)

Tactic:
rw [← not_nonempty_iff, ← not_congr (finrank_hom_simple_simple_eq_one_iff 𝕜 X Y)]

Premises used: CategoryTheory.finrank_hom_simple_simple_eq_one_iff, not_nonempty_iff, not_congr
-- 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
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ Y) ≤ 1

Tactic:
have := finrank_hom_simple_simple_le_one 𝕜 X Y
-- 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
this : finrank.{u_2, v_1} 𝕜 (X ⟶ Y) ≤ 1
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = 0 ↔ ¬finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = 1

Tactic:
lia
-- 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 : ∀ (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
neg : ∀ (h : ¬Nonempty.{v_1 + 1} (X ≅ Y)), finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = 0
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = if Nonempty.{v_1 + 1} (X ≅ Y) then 1 else 0

Tactic:
split_ifs with h
-- 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 : ∀ (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
h : Nonempty.{v_1 + 1} (X ≅ Y)
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = 1

Tactic:
(finrank_hom_simple_simple_eq_one_iff 𝕜 X Y).2 h

Premises used: Iff.mpr, CategoryTheory.finrank_hom_simple_simple_eq_one_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
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
h : Nonempty.{v_1 + 1} (X ≅ Y)
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = 1

Tactic:
exact (finrank_hom_simple_simple_eq_one_iff 𝕜 X Y).2 h

Premises used: Iff.mpr, CategoryTheory.finrank_hom_simple_simple_eq_one_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
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
h : ¬Nonempty.{v_1 + 1} (X ≅ Y)
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = 0

Tactic:
(finrank_hom_simple_simple_eq_zero_iff 𝕜 X Y).2 (not_nonempty_iff.mp h)

Premises used: Iff.mpr, CategoryTheory.finrank_hom_simple_simple_eq_zero_iff, not_nonempty_iff, Iff.mp
-- 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 : ∀ (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
h : ¬Nonempty.{v_1 + 1} (X ≅ Y)
⊢ finrank.{u_2, v_1} 𝕜 (X ⟶ Y) = 0

Tactic:
exact (finrank_hom_simple_simple_eq_zero_iff 𝕜 X Y).2 (not_nonempty_iff.mp h)

Premises used: Iff.mpr, CategoryTheory.finrank_hom_simple_simple_eq_zero_iff, not_nonempty_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Preadditive.Transfer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
hF : F.FullyFaithful
P Q R : C
f f' : P ⟶ Q
g : Q ⟶ R
⊢ F.map ((f + f') ≫ g) = F.map (f ≫ g + f' ≫ g)

Tactic:
simp [Equiv.add_def]

Premises used: Equiv.add_def
-- Module: Mathlib.CategoryTheory.Preadditive.Transfer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
hF : F.FullyFaithful
P Q R : C
f : P ⟶ Q
g g' : Q ⟶ R
⊢ F.map (f ≫ (g + g')) = F.map (f ≫ g + f ≫ g')

Tactic:
simp [Equiv.add_def]

Premises used: Equiv.add_def
-- Module: Mathlib.CategoryTheory.Preadditive.Transfer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
hF : F.FullyFaithful
this : Preadditive.{v₁, u₁} C := Preadditive.ofFullyFaithful hF
⊢ ∀ {X Y : C} {f g : X ⟶ Y}, F.map (f + g) = F.map f + F.map g

Tactic:
simp [Equiv.add_def]

Premises used: Equiv.add_def
-- Module: Mathlib.CategoryTheory.Preadditive.Transfer
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Preadditive.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
⊢ e.inverse.Additive

Tactic:
letI : Preadditive C := ofFullyFaithful e.fullyFaithfulFunctor
  letI : e.functor.Additive := e.fullyFaithfulFunctor.additive_ofFullyFaithful
  e.inverse_additive

Premises used: CategoryTheory.Equivalence.inverse_additive
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
⊢ Eq (α := C ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v))
    (preadditiveYoneda ⋙
      obj (whiskeringRight Cᵒᵖ AddCommGrpCat (Type v))
        (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
          AddCommGrpCat.carrier)))
    yoneda

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.yoneda, CategoryTheory.Functor.whiskerRight, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
⊢ Eq (α := Cᵒᵖ ⥤ C ⥤ Type v)
    (preadditiveCoyoneda ⋙
      obj (whiskeringRight C AddCommGrpCat (Type v))
        (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
          AddCommGrpCat.carrier)))
    coyoneda

Tactic:
rfl

Premises used: CategoryTheory.Functor.flip, CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskerRight, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
⊢ Full (C := C) preadditiveYoneda

Tactic:
let _ : Functor.Full (preadditiveYoneda ⋙
      (whiskeringRight Cᵒᵖ AddCommGrpCat (Type v)).obj (forget AddCommGrpCat)) :=
    Yoneda.yoneda_full
  Functor.Full.of_comp_faithful preadditiveYoneda
    ((whiskeringRight Cᵒᵖ AddCommGrpCat (Type v)).obj (forget AddCommGrpCat))

Premises used: CategoryTheory.preadditiveYoneda, Opposite, CategoryTheory.Functor.whiskeringRight, CategoryTheory.Yoneda.yoneda_full, AddCommGrpCat, CategoryTheory.forget, CategoryTheory.Functor.Full.of_comp_faithful, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
⊢ Full (C := Cᵒᵖ) preadditiveCoyoneda

Tactic:
let _ : Functor.Full (preadditiveCoyoneda ⋙
      (whiskeringRight C AddCommGrpCat (Type v)).obj (forget AddCommGrpCat)) :=
    Coyoneda.coyoneda_full
  Functor.Full.of_comp_faithful preadditiveCoyoneda
    ((whiskeringRight C AddCommGrpCat (Type v)).obj (forget AddCommGrpCat))

Premises used: CategoryTheory.Functor.whiskeringRight, AddCommGrpCat, CategoryTheory.forget, CategoryTheory.Coyoneda.coyoneda_full, CategoryTheory.preadditiveCoyoneda, CategoryTheory.Functor.Full.of_comp_faithful, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
⊢ Faithful (C := C) preadditiveYoneda

Tactic:
Functor.Faithful.of_comp_eq whiskering_preadditiveYoneda

Premises used: CategoryTheory.whiskering_preadditiveYoneda, CategoryTheory.Functor.Faithful.of_comp_eq
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
⊢ Faithful (C := Cᵒᵖ) preadditiveCoyoneda

Tactic:
Functor.Faithful.of_comp_eq whiskering_preadditiveCoyoneda

Premises used: CategoryTheory.Functor.Faithful.of_comp_eq, CategoryTheory.whiskering_preadditiveCoyoneda
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Injective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : C
rw :
  Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj yoneda J) ↔
    Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj preadditiveYoneda J)
⊢ Injective.{v, u} J ↔ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj preadditiveYoneda J)

Tactic:
rw [injective_iff_preservesEpimorphisms_yoneda_obj]

Premises used: CategoryTheory.Injective.injective_iff_preservesEpimorphisms_yoneda_obj
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Injective
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)

Tactic:
⟨fun h : (preadditiveYoneda.obj J ⋙ (forget AddCommGrpCat)).PreservesEpimorphisms => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Injective
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)
refine_2 :
  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 yoneda J) ↔
    Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj preadditiveYoneda J)

Tactic:
refine
    ⟨fun h : (preadditiveYoneda.obj J ⋙ (forget AddCommGrpCat)).PreservesEpimorphisms => ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Injective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : C
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:
Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveYoneda.obj J) (forget _)

Premises used: CategoryTheory.Functor.preservesEpimorphisms_of_preserves_of_reflects, CategoryTheory.preadditiveYoneda, CategoryTheory.forget, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Injective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : C
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:
exact
      Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveYoneda.obj J) (forget _)

Premises used: CategoryTheory.Functor.preservesEpimorphisms_of_preserves_of_reflects, CategoryTheory.preadditiveYoneda, CategoryTheory.forget, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Injective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : C
h : Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj preadditiveYoneda J)
⊢ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj yoneda J)

Tactic:
(inferInstance : (preadditiveYoneda.obj J ⋙ forget _).PreservesEpimorphisms)

Premises used: CategoryTheory.Functor.comp, inferInstance
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Injective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : C
h : Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj preadditiveYoneda J)
⊢ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj yoneda J)

Tactic:
exact (inferInstance : (preadditiveYoneda.obj J ⋙ forget _).PreservesEpimorphisms)

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Injective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : C
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)
⊢ Injective.{v, u} J ↔ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End J)) (preadditiveYonedaObj J)

Tactic:
rw [injective_iff_preservesEpimorphisms_yoneda_obj]

Premises used: CategoryTheory.Injective.injective_iff_preservesEpimorphisms_yoneda_obj
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Injective
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)

Tactic:
⟨fun h : (preadditiveYonedaObj J ⋙ (forget <| ModuleCat (End J))).PreservesEpimorphisms =>
    ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Injective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : C
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)
refine_2 :
  Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End J)) (preadditiveYonedaObj J) →
    Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj yoneda J)
⊢ 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:
refine ⟨fun h : (preadditiveYonedaObj J ⋙ (forget <| ModuleCat (End J))).PreservesEpimorphisms =>
    ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Injective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : C
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:
Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveYonedaObj J) (forget _)

Premises used: CategoryTheory.Functor.preservesEpimorphisms_of_preserves_of_reflects, CategoryTheory.forget, CategoryTheory.preadditiveYonedaObj
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Injective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : C
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:
exact
      Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveYonedaObj J) (forget _)

Premises used: CategoryTheory.Functor.preservesEpimorphisms_of_preserves_of_reflects, CategoryTheory.forget, CategoryTheory.preadditiveYonedaObj
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Injective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : C
h : Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End J)) (preadditiveYonedaObj J)
⊢ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj yoneda J)

Tactic:
(inferInstance : (preadditiveYonedaObj J ⋙ forget _).PreservesEpimorphisms)

Premises used: CategoryTheory.Functor.comp, inferInstance
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Injective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : C
h : Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End J)) (preadditiveYonedaObj J)
⊢ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj yoneda J)

Tactic:
exact (inferInstance : (preadditiveYonedaObj J ⋙ forget _).PreservesEpimorphisms)

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X : C
⊢ PreservesLimits.{v, v, u, v + 1} (D := ModuleCat (End X)) (preadditiveYonedaObj X)

Tactic:
have : PreservesLimits (preadditiveYonedaObj X ⋙ forget _) :=
    (inferInstance : PreservesLimits (yoneda.obj X))
  preservesLimits_of_reflects_of_preserves _ (forget _)

Premises used: ModuleCat, inferInstance, CategoryTheory.End, CategoryTheory.forget, CategoryTheory.Limits.preservesLimits_of_reflects_of_preserves, CategoryTheory.preadditiveYonedaObj
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X : C
⊢ PreservesLimits.{v, v, u, v + 1} (D := ModuleCat (End X)ᵐᵒᵖ) (preadditiveCoyonedaObj X)

Tactic:
have : PreservesLimits (preadditiveCoyonedaObj X ⋙ forget _) :=
    (inferInstance : PreservesLimits (coyoneda.obj (op X)))
  preservesLimits_of_reflects_of_preserves _ (forget _)

Premises used: ModuleCat, MulOpposite, inferInstance, CategoryTheory.preadditiveCoyonedaObj, CategoryTheory.End, CategoryTheory.forget, CategoryTheory.Limits.preservesLimits_of_reflects_of_preserves
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X : C
⊢ PreservesLimits.{v, v, u, v + 1} (Functor.obj preadditiveYoneda X)

Tactic:
show PreservesLimits (preadditiveYonedaObj X ⋙ forget₂ _ _) from inferInstance

Premises used: CategoryTheory.Functor.comp, inferInstance