awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Preadditive.Opposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (-f).unop = -f.unop

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Opposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
⊢ (f + g).op = f.op + g.op

Tactic:
rfl

Premises used: Quiver.Hom.op, Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Opposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
⊢ (f - g).op = f.op - g.op

Tactic:
rfl

Premises used: Quiver.Hom.op, Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Opposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : C
k : ℤ
f : X ⟶ Y
⊢ (k • f).op = k • f.op

Tactic:
rfl

Premises used: Quiver.Hom.op, Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Opposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : C
f : X ⟶ Y
⊢ (-f).op = -f.op

Tactic:
rfl

Premises used: Quiver.Hom.op, Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Opposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : Cᵒᵖ
ι : Type u_2
s : Finset ι
f : ι → (X ⟶ Y)
⊢ (s.sum f).unop = ∑ i ∈ s, (f i).unop

Tactic:
map_sum (unopHom X Y) _ _

Premises used: Quiver.Hom.unop, map_sum, CategoryTheory.unopHom
-- Module: Mathlib.CategoryTheory.Preadditive.Opposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : C
ι : Type u_2
s : Finset ι
f : ι → (X ⟶ Y)
⊢ (s.sum f).op = ∑ i ∈ s, (f i).op

Tactic:
map_sum (opHom X Y) _ _

Premises used: Quiver.Hom.op, CategoryTheory.opHom, map_sum
-- Module: Mathlib.CategoryTheory.Preadditive.Opposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
G : C
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ (x y : G ⟶ G),
    { unop' := x + y : PreOpposite (End G) } =
      { unop' := x : PreOpposite (End G) } + { unop' := y : PreOpposite (End G) }
⊢ ∀ (x y : G ⟶ G),
    { unop' := x + y : PreOpposite (End G) } =
      { unop' := x : PreOpposite (End G) } + { unop' := y : PreOpposite (End G) }

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Preadditive.Opposite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
G : C
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ (m : (End G)ᵐᵒᵖ) (x : G ⟶ G),
    { unop' := m • x : PreOpposite (End G) } =
      HSMul.hSMul (α := (End G)ᵐᵒᵖ) ((RingHom.id (End G)ᵐᵒᵖ : (a : (End G)ᵐᵒᵖ) → (End G)ᵐᵒᵖ) m : (End G)ᵐᵒᵖ)
        { unop' := x : PreOpposite (End G) }
⊢ ∀ (m : (End G)ᵐᵒᵖ) (x : G ⟶ G),
    { unop' := m • x : PreOpposite (End G) } =
      HSMul.hSMul (α := (End G)ᵐᵒᵖ) ((RingHom.id (End G)ᵐᵒᵖ : (a : (End G)ᵐᵒᵖ) → (End G)ᵐᵒᵖ) m : (End G)ᵐᵒᵖ)
        { unop' := x : PreOpposite (End G) }

Tactic:
cat_disch
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P X E : C
inst_1 : Projective.{v, u} P
f : P ⟶ X
e : E ⟶ X
inst_2 : Epi e
⊢ factorThru f e ≫ e = f

Tactic:
(Projective.factors f e).choose_spec

Premises used: Exists.choose_spec, CategoryTheory.Projective.factorThru, CategoryTheory.Projective.factors
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
⊢ Projective.{v, u} (C := C) 0

Tactic:
(isZero_zero C).projective

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.Limits.IsZero.projective
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P Q : C
i : P ≅ Q
h : Projective.{v, u} P
E X : C
f : Q ⟶ X
e : E ⟶ X
h_1 : Epi e
f' : P ⟶ E
hf' : f' ≫ e = i.hom ≫ f
⊢ (i.inv ≫ f') ≫ e = f

Tactic:
simp [hf']
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P Q : C
i : P ≅ Q
⊢ Projective.{v, u} P ↔ Projective.{v, u} Q

Tactic:
⟨of_iso i, of_iso i.symm⟩

Premises used: CategoryTheory.Projective.of_iso, Iff.intro, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst_1 : Category.{v, u} C
X E X_1 : Type u
f : X ⟶ X_1
e : E ⟶ X_1
h_1 : Epi e
he :
  Function.Surjective (α := (fun (X : Type u) ↦ X) E) (β := (fun (X : Type u) ↦ X) X_1)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) e) : (a : (fun (X : Type u) ↦ X) E) → (fun (X : Type u) ↦ X) X_1)
h :
  ∀ (x : X),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((↾fun (x : X) ↦
              Exists.choose (p := fun (a : E) ↦
                Eq (α := (fun (X : Type u) ↦ X) X_1)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) e :
                        (a : (fun (X : Type u) ↦ X) E) → (fun (X : Type u) ↦ X) X_1)
                      a :
                    (fun (X : Type u) ↦ X) X_1)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                        (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) X_1)
                      x :
                    (fun (X : Type u) ↦ X) X_1))
                ⋯) ≫
            e))
        x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) f).toFun x
⊢ (↾fun (x : X) ↦
        Exists.choose (p := fun (a : E) ↦
          Eq (α := (fun (X : Type u) ↦ X) X_1)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) e : (a : (fun (X : Type u) ↦ X) E) → (fun (X : Type u) ↦ X) X_1)
                a :
              (fun (X : Type u) ↦ X) X_1)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) X_1)
                x :
              (fun (X : Type u) ↦ X) X_1))
          ⋯) ≫
      e =
    f

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X E X_1 : Type u
f : X ⟶ X_1
e : E ⟶ X_1
h : Epi e
he :
  Function.Surjective (α := (fun (X : Type u) ↦ X) E) (β := (fun (X : Type u) ↦ X) X_1)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) e) : (a : (fun (X : Type u) ↦ X) E) → (fun (X : Type u) ↦ X) X_1)
x : X
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x : X) ↦
            Exists.choose (p := fun (a : E) ↦
              Eq (α := (fun (X : Type u) ↦ X) X_1)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) e :
                      (a : (fun (X : Type u) ↦ X) E) → (fun (X : Type u) ↦ X) X_1)
                    a :
                  (fun (X : Type u) ↦ X) X_1)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                      (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) X_1)
                    x :
                  (fun (X : Type u) ↦ X) X_1))
              ⋯) ≫
          e))
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) f).toFun x

Tactic:
(he (f x)).choose_spec

Premises used: Exists.choose_spec, CategoryTheory.ConcreteCategory.hom, Classical.choose, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst_1 : Category.{v, u} C
X E X_1 : Type u
f : X ⟶ X_1
e : E ⟶ X_1
h : Epi e
he :
  Function.Surjective (α := (fun (X : Type u) ↦ X) E) (β := (fun (X : Type u) ↦ X) X_1)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) e) : (a : (fun (X : Type u) ↦ X) E) → (fun (X : Type u) ↦ X) X_1)
x : X
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x : X) ↦
            Exists.choose (p := fun (a : E) ↦
              Eq (α := (fun (X : Type u) ↦ X) X_1)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) e :
                      (a : (fun (X : Type u) ↦ X) E) → (fun (X : Type u) ↦ X) X_1)
                    a :
                  (fun (X : Type u) ↦ X) X_1)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                      (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) X_1)
                    x :
                  (fun (X : Type u) ↦ X) X_1))
              ⋯) ≫
          e))
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) f).toFun x

Tactic:
exact (he (f x)).choose_spec

Premises used: Exists.choose_spec, CategoryTheory.ConcreteCategory.hom, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : C
⊢ Projective.{v, u} P ↔ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj coyoneda (op P))

Tactic:
⟨fun hP =>
    ⟨fun f _ =>
      (epi_iff_surjective _).2 fun g =>
        have : Projective (unop (op P)) := hP
        ⟨factorThru g f, factorThru_comp _ _⟩⟩,
    fun _ =>
    ⟨fun f e _ =>
      (epi_iff_surjective _).1 (inferInstance : Epi ((coyoneda.obj (op P)).map e)) f⟩⟩

Premises used: Iff.mpr, CategoryTheory.coyoneda, CategoryTheory.epi_iff_surjective, CategoryTheory.Projective.factorThru, inferInstance, CategoryTheory.Projective.mk, CategoryTheory.Functor.PreservesEpimorphisms.mk, CategoryTheory.Functor.map, CategoryTheory.Projective.factorThru_comp, Opposite.op, Iff.intro, Exists.intro, Iff.mp, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnoughProjectives.{v, u} C
X : C
⊢ Projective.{v, u} (over.{v, u} X)

Tactic:
(EnoughProjectives.presentation X).some.projective

Premises used: CategoryTheory.Projective.over, CategoryTheory.EnoughProjectives.presentation, Nonempty.some, CategoryTheory.ProjectivePresentation.projective
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnoughProjectives.{v, u} C
X : C
⊢ Epi.{v, u} (X := over.{v, u} X) (π X)

Tactic:
(EnoughProjectives.presentation X).some.epi

Premises used: CategoryTheory.Projective.over, CategoryTheory.EnoughProjectives.presentation, CategoryTheory.Projective.π, Nonempty.some, CategoryTheory.ProjectivePresentation.epi
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : EnoughProjectives.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
inst_3 : HasKernel f
⊢ Projective.{v, u} (syzygies f)

Tactic:
inferInstanceAs (Projective (over _))

Premises used: _private.0.CategoryTheory.Projective.instSyzygies._proof_1
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
inst_2 : G.PreservesEpimorphisms
P : C
hP : Projective.{v, u} P
E X : D
f : F.obj P ⟶ X
g : E ⟶ X
h : Epi g
rcases : ∀ (f' : P ⟶ G.obj E) (hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f), ∃ (f' : F.obj P ⟶ E), f' ≫ g = f
⊢ ∃ (f' : F.obj P ⟶ E), f' ≫ g = f

Tactic:
rcases hP.factors (adj.unit.app P ≫ G.map f) (G.map g) with ⟨f', hf'⟩

Premises used: CategoryTheory.Adjunction.unit, CategoryTheory.Functor.map, CategoryTheory.Projective.factors, CategoryTheory.CategoryStruct.comp, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
inst_2 : G.PreservesEpimorphisms
P : C
hP : Projective.{v, u} P
E X : D
f : F.obj P ⟶ X
g : E ⟶ X
h_1 : Epi g
f' : P ⟶ G.obj E
hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f
h : (F.map f' ≫ adj.counit.app E) ≫ g = f
⊢ ∃ (f' : F.obj P ⟶ E), f' ≫ g = f

Tactic:
use F.map f' ≫ adj.counit.app _

Premises used: CategoryTheory.Functor.map, CategoryTheory.Adjunction.counit, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
inst_2 : G.PreservesEpimorphisms
P : C
hP : Projective.{v, u} P
E X : D
f : F.obj P ⟶ X
g : E ⟶ X
h_1 : Epi g
f' : P ⟶ G.obj E
hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f
h : F.map (adj.unit.app P ≫ G.map f) ≫ adj.counit.app X = f
⊢ (F.map f' ≫ adj.counit.app E) ≫ g = f

Tactic:
rw [Category.assoc, ← Adjunction.counit_naturality, ← Category.assoc, ← F.map_comp, hf']

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Adjunction.counit_naturality, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
inst_2 : G.PreservesEpimorphisms
P : C
hP : Projective.{v, u} P
E X : D
f : F.obj P ⟶ X
g : E ⟶ X
h : Epi g
f' : P ⟶ G.obj E
hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f
⊢ F.map (adj.unit.app P ≫ G.map f) ≫ adj.counit.app X = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
inst_2 : F.Full
inst_3 : F.Faithful
P : C
hP : Projective.{v', u'} (F.obj P)
E X : C
f : P ⟶ X
g : E ⟶ X
h : Epi g
⊢ PreservesColimitsOfSize.{0, 0, v, v', u, u'} F

Tactic:
haveI := Adjunction.leftAdjoint_preservesColimits.{0, 0} adj
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
inst_2 : F.Full
inst_3 : F.Faithful
P : C
hP : Projective.{v', u'} (F.obj P)
E X : C
f : P ⟶ X
g : E ⟶ X
h : Epi g
this : PreservesColimitsOfSize.{0, 0, v, v', u, u'} F
rcases : ∀ (f' : F.obj P ⟶ F.obj E) (hf' : f' ≫ F.map g = F.map f), ∃ (f' : P ⟶ E), f' ≫ g = f
⊢ ∃ (f' : P ⟶ E), f' ≫ g = f

Tactic:
rcases (@hP).1 (F.map f) (F.map g) with ⟨f', hf'⟩

Premises used: CategoryTheory.Functor.map, CategoryTheory.Projective.factors
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
inst_2 : F.Full
inst_3 : F.Faithful
P : C
hP : Projective.{v', u'} (F.obj P)
E X : C
f : P ⟶ X
g : E ⟶ X
h_1 : Epi g
this : PreservesColimitsOfSize.{0, 0, v, v', u, u'} F
f' : F.obj P ⟶ F.obj E
hf' : f' ≫ F.map g = F.map f
h : (adj.unit.app P ≫ G.map f' ≫ inv (adj.unit.app E)) ≫ g = f
⊢ ∃ (f' : P ⟶ E), f' ≫ g = f

Tactic:
use adj.unit.app _ ≫ G.map f' ≫ (inv <| adj.unit.app _)

Premises used: CategoryTheory.Adjunction.unit, CategoryTheory.Functor.map, CategoryTheory.inv, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
inst_2 : F.Full
inst_3 : F.Faithful
P : C
hP : Projective.{v', u'} (F.obj P)
E X : C
f : P ⟶ X
g : E ⟶ X
h : Epi g
this : PreservesColimitsOfSize.{0, 0, v, v', u, u'} F
f' : F.obj P ⟶ F.obj E
hf' : f' ≫ F.map g = F.map f
⊢ F.map ((adj.unit.app P ≫ G.map f' ≫ inv (adj.unit.app E)) ≫ g) = F.map f

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
inst_2 : F.Full
inst_3 : F.Faithful
P : C
hP : Projective.{v', u'} (F.obj P)
E X : C
f : P ⟶ X
g : E ⟶ X
h : Epi g
this : PreservesColimitsOfSize.{0, 0, v, v', u, u'} F
f' : F.obj P ⟶ F.obj E
hf' : f' ≫ F.map g = F.map f
⊢ (adj.unit.app P ≫ G.map f' ≫ inv (adj.unit.app E)) ≫ g = f

Tactic:
exact F.map_injective (by simpa)

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_2 : F.Full
inst_3 : F.Faithful
inst_4 : F.PreservesEpimorphisms
P : C
hP : Projective.{v_1, u_1} (F.obj P)
E X : C
g : P ⟶ X
f : E ⟶ X
h : Epi f
obtain : ∀ (h : F.obj P ⟶ F.obj E) (fac : h ≫ F.map f = F.map g), ∃ (f' : P ⟶ E), f' ≫ f = g
⊢ ∃ (f' : P ⟶ E), f' ≫ f = g

Tactic:
obtain ⟨h, fac⟩ := hP.factors (F.map g) (F.map f)

Premises used: CategoryTheory.Functor.map, CategoryTheory.Projective.factors
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_2 : F.Full
inst_3 : F.Faithful
inst_4 : F.PreservesEpimorphisms
P : C
hP : Projective.{v_1, u_1} (F.obj P)
E X : C
g : P ⟶ X
f : E ⟶ X
h_1 : Epi f
h : F.obj P ⟶ F.obj E
fac : h ≫ F.map f = F.map g
⊢ F.map (F.preimage h ≫ f) = F.map g

Tactic:
simp [fac]
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{v, v_1, u, u_1} C D
inst_2 : F.Full
inst_3 : F.Faithful
inst_4 : F.PreservesEpimorphisms
P : C
hP : Projective.{v_1, u_1} (F.obj P)
E X : C
g : P ⟶ X
f : E ⟶ X
h_1 : Epi f
h : F.obj P ⟶ F.obj E
fac : h ≫ F.map f = F.map g
⊢ ∃ (f' : P ⟶ E), f' ≫ f = g

Tactic:
exact ⟨F.preimage h, F.map_injective (by simp [fac])⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Equivalence.{v, v', u, u'} C D
P : C
⊢ Projective.{v', u'} (F.functor.obj P) ↔ Projective.{v, u} P

Tactic:
⟨F.toAdjunction.projective_of_map_projective P, F.toAdjunction.map_projective P⟩

Premises used: CategoryTheory.Adjunction.projective_of_map_projective, Iff.intro, CategoryTheory.Equivalence.toAdjunction, CategoryTheory.Adjunction.map_projective
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Equivalence.{v, v', u, u'} C D
mp : EnoughProjectives.{v, u} C → EnoughProjectives.{v', u'} D
mpr : EnoughProjectives.{v', u'} D → EnoughProjectives.{v, u} C
⊢ EnoughProjectives.{v, u} C ↔ EnoughProjectives.{v', u'} D

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Equivalence.{v, v', u, u'} C D
H : EnoughProjectives.{v, u} C
mp : ∀ (X : D), Nonempty (ProjectivePresentation.{v', u'} X)
⊢ EnoughProjectives.{v', u'} D

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Equivalence.{v, v', u, u'} C D
H : EnoughProjectives.{v, u} C
X : D
mp : ProjectivePresentation.{v', u'} X
⊢ Nonempty (ProjectivePresentation.{v', u'} X)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Equivalence.{v, v', u, u'} C D
H : EnoughProjectives.{v', u'} D
mpr : ∀ (X : C), Nonempty (ProjectivePresentation.{v, u} X)
⊢ EnoughProjectives.{v, u} C

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Equivalence.{v, v', u, u'} C D
H : EnoughProjectives.{v', u'} D
X : C
mpr : ProjectivePresentation.{v, u} X
⊢ Nonempty (ProjectivePresentation.{v, u} X)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Equivalence.{v, v', u, u'} C D
H : EnoughProjectives.{v, u} C
X : D
⊢ ProjectivePresentation.{v', u'} X

Tactic:
exact F.symm.projectivePresentationOfMapProjectivePresentation _
      (Nonempty.some (H.presentation (F.inverse.obj X)))

Premises used: CategoryTheory.EnoughProjectives.presentation, Nonempty.some, CategoryTheory.Equivalence.projectivePresentationOfMapProjectivePresentation, CategoryTheory.Equivalence.symm, CategoryTheory.Functor.obj, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Equivalence.{v, v', u, u'} C D
H : EnoughProjectives.{v', u'} D
X : C
⊢ ProjectivePresentation.{v, u} X

Tactic:
exact F.projectivePresentationOfMapProjectivePresentation X
      (Nonempty.some (H.presentation (F.functor.obj X)))

Premises used: CategoryTheory.EnoughProjectives.presentation, Nonempty.some, CategoryTheory.Equivalence.functor, CategoryTheory.Equivalence.projectivePresentationOfMapProjectivePresentation, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : Retract X Y
p : Projective.{v, u} Y
⊢ Projective.{v, u} X

Tactic:
Projective.mk (fun {A B} f e _ ↦ ?_)

Premises used: CategoryTheory.Projective.mk
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : Retract X Y
p : Projective.{v, u} Y
refine : ∀ {A B : C} (f : X ⟶ B) (e : A ⟶ B), Epi e → ∃ (f' : X ⟶ A), f' ≫ e = f
⊢ Projective.{v, u} X

Tactic:
refine Projective.mk (fun {A B} f e _ ↦ ?_)

Premises used: CategoryTheory.Projective.mk
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : Retract X Y
p : Projective.{v, u} Y
A B : C
f : X ⟶ B
e : A ⟶ B
h_1 : Epi e
rcases : ∀ (g : Y ⟶ A) (hg : g ≫ e = h.r ≫ f), ∃ (f' : X ⟶ A), f' ≫ e = f
⊢ ∃ (f' : X ⟶ A), f' ≫ e = f

Tactic:
rcases p.factors (h.r ≫ f) e with ⟨g, hg⟩

Premises used: CategoryTheory.Projective.factors, CategoryTheory.Retract.r, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : Retract X Y
p : Projective.{v, u} Y
A B : C
f : X ⟶ B
e : A ⟶ B
h_1 : Epi e
g : Y ⟶ A
hg : g ≫ e = h.r ≫ f
h₁ : (h.i ≫ g) ≫ e = f
⊢ ∃ (f' : X ⟶ A), f' ≫ e = f

Tactic:
use h.i ≫ g

Premises used: CategoryTheory.Retract.i
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : Retract X Y
p : Projective.{v, u} Y
A B : C
f : X ⟶ B
e : A ⟶ B
h_1 : Epi e
g : Y ⟶ A
hg : g ≫ e = h.r ≫ f
⊢ (h.i ≫ g) ≫ e = f

Tactic:
simp [hg]
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Internal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : MonoidalClosed.{v_1, u_1} C
P : C
inst_3 : InternallyProjective.{v_1, u_1} P
⊢ PreservesEpimorphisms.{v_1, v_1, u_1, u_1} (ihom P)

Tactic:
isInternallyProjective.prop_of_is P

Premises used: CategoryTheory.isInternallyProjective, CategoryTheory.ObjectProperty.prop_of_is
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.Internal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : MonoidalClosed.{v_1, u_1} C
X Y : C
r : Retract Y X
inst_3 : InternallyProjective.{v_1, u_1} X
⊢ InternallyProjective.{v_1, u_1} Y

Tactic:
⟨isInternallyProjective.prop_of_retract r (isInternallyProjective.prop_of_is _)⟩

Premises used: CategoryTheory.isInternallyProjective, CategoryTheory.ObjectProperty.Is.mk, CategoryTheory.ObjectProperty.prop_of_retract, CategoryTheory.ObjectProperty.prop_of_is
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties
Goal:
C : Type u
inst : Category.{v, u} C
X Y P : C
p : X ⟶ Y
inst_1 : Epi p
inst_2 : Projective.{v, u} P
inst_3 : HasZeroObject.{v, u} C
i : 0 ⟶ P
⊢ HasLiftingProperty i p

Tactic:
Projective.hasLiftingProperty_of_isZero i p (isZero_zero C)

Premises used: CategoryTheory.Limits.isZero_zero, CategoryTheory.Projective.hasLiftingProperty_of_isZero
-- Module: Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
P Z : C
i : Z ⟶ P
hZ : IsZero.{v, u} Z
obtain : Projective.{v, u} P ↔ MorphismProperty.llp.{v, u} (MorphismProperty.epimorphisms C) (X := Z) (Y := P) 0
⊢ Projective.{v, u} P ↔ MorphismProperty.llp (MorphismProperty.epimorphisms C) i

Tactic:
obtain rfl := hZ.eq_of_src i 0

Premises used: CategoryTheory.Limits.IsZero.eq_of_src, OfNat.ofNat, rfl