awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M_1 M₁ M₂ : PresheafOfModules.{v, v₁, u₁, u} R
X_1 : Cᵒᵖ
hX_1 : Limits.IsInitial.{v₁, u₁} X_1
X : Cᵒᵖ
hX : Limits.IsInitial.{v₁, u₁} X
M N : PresheafOfModules.{v, v₁, u₁, u} R
f : M ⟶ N
Y Z : Cᵒᵖ
g : Y ⟶ Z
x : (↑((forgetToPresheafModuleCatObj X hX M).obj Y) : Type v)
⊢ Eq (α := (↑((forgetToPresheafModuleCatObj X hX N).obj Z) : Type v))
    ((ModuleCat.Hom.hom
            ((forgetToPresheafModuleCatObj X hX M).map g ≫
              ModuleCat.ofHom
                {
                  toFun :=
                    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Z) : Type u)) ↦
                          LinearMap.{u, u, v, v} (R := (↑(R.obj Z) : Type u)) (RingHom.id (↑(R.obj Z) : Type u))
                            (↑x1 : Type v) (↑x2 : Type v))
                          (CC := ModuleCat.carrier) (f.app Z)) :
                      (a : (↑(M.obj Z) : Type v)) → (↑(N.obj Z) : Type v)),
                  map_add' := ⋯, map_smul' := ⋯ }) :
          (a : (↑((forgetToPresheafModuleCatObj X hX M).obj Y) : Type v)) →
            (↑((forgetToPresheafModuleCatObj X hX N).obj Z) : Type v))
        x :
      (↑((forgetToPresheafModuleCatObj X hX N).obj Z) : Type v))
    ((ModuleCat.Hom.hom
            (ModuleCat.ofHom
                {
                  toFun :=
                    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj Y) : Type u)) ↦
                          LinearMap.{u, u, v, v} (R := (↑(R.obj Y) : Type u)) (RingHom.id (↑(R.obj Y) : Type u))
                            (↑x1 : Type v) (↑x2 : Type v))
                          (CC := ModuleCat.carrier) (f.app Y)) :
                      (a : (↑(M.obj Y) : Type v)) → (↑(N.obj Y) : Type v)),
                  map_add' := ⋯, map_smul' := ⋯ } ≫
              (forgetToPresheafModuleCatObj X hX N).map g) :
          (a : (↑((forgetToPresheafModuleCatObj X hX M).obj Y) : Type v)) →
            (↑((forgetToPresheafModuleCatObj X hX N).obj Z) : Type v))
        x :
      (↑((forgetToPresheafModuleCatObj X hX N).obj Z) : Type v))

Tactic:
exact naturality_apply f g x

Premises used: PresheafOfModules.naturality_apply
-- Module: Mathlib.Algebra.Category.ModuleCat.Products
Goal:
R : Type u
inst : Ring R
ι : Type v
Z : ι → ModuleCat R
s : Cone (Discrete.functor Z)
m : s.pt ⟶ (productCone.{u, v, w} Z).pt
w : ∀ (j : Discrete ι), m ≫ (productCone.{u, v, w} Z).π.app j = s.π.app j
hf :
  ∀ (x : (↑s.pt : Type (max v w))),
    Eq (α := (↑(productCone.{u, v, w} Z).pt : Type (max v w)))
      ((Hom.hom m : (a : (↑s.pt : Type (max v w))) → (↑(productCone Z).pt : Type (max v w))) x :
        (↑(productCone.{u, v, w} Z).pt : Type (max v w)))
      ((Hom.hom
              (↟(LinearMap.pi (φ := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) fun (j : ι) ↦
                  Hom.hom (s.π.app { as := j }))) :
            (a : (↑s.pt : Type (max v w))) → (↑(productCone Z).pt : Type (max v w)))
          x :
        (↑(productCone.{u, v, w} Z).pt : Type (max v w)))
⊢ m = ↟(LinearMap.pi (φ := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) fun (j : ι) ↦ Hom.hom (s.π.app { as := j }))

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.ModuleCat.Products
Goal:
R : Type u
inst : Ring R
ι : Type v
Z : ι → ModuleCat R
s : Cone (Discrete.functor Z)
m : s.pt ⟶ (productCone.{u, v, w} Z).pt
w : ∀ (j : Discrete ι), m ≫ (productCone.{u, v, w} Z).π.app j = s.π.app j
x : (↑s.pt : Type (max v w))
hf :
  ∀ (i : ι),
    Eq (α := (↑(Z i) : Type (max v w)))
      ((Hom.hom m : (a : (↑s.pt : Type (max v w))) → (↑(productCone Z).pt : Type (max v w))) x i :
        (↑(Z i) : Type (max v w)))
      ((Hom.hom
              (↟(LinearMap.pi (φ := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) fun (j : ι) ↦
                  Hom.hom (s.π.app { as := j }))) :
            (a : (↑s.pt : Type (max v w))) → (↑(productCone Z).pt : Type (max v w)))
          x i :
        (↑(Z i) : Type (max v w)))
⊢ Eq (α := (↑(productCone.{u, v, w} Z).pt : Type (max v w)))
    ((Hom.hom m : (a : (↑s.pt : Type (max v w))) → (↑(productCone Z).pt : Type (max v w))) x :
      (↑(productCone.{u, v, w} Z).pt : Type (max v w)))
    ((Hom.hom
            (↟(LinearMap.pi (φ := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) fun (j : ι) ↦
                Hom.hom (s.π.app { as := j }))) :
          (a : (↑s.pt : Type (max v w))) → (↑(productCone Z).pt : Type (max v w)))
        x :
      (↑(productCone.{u, v, w} Z).pt : Type (max v w)))

Tactic:
funext i
-- Module: Mathlib.Algebra.Category.ModuleCat.Products
Goal:
R : Type u
inst : Ring R
ι : Type v
Z : ι → ModuleCat R
s : Cone (Discrete.functor Z)
m : s.pt ⟶ (productCone.{u, v, w} Z).pt
w : ∀ (j : Discrete ι), m ≫ (productCone.{u, v, w} Z).π.app j = s.π.app j
x : (↑s.pt : Type (max v w))
i : ι
⊢ Eq (α := (↑(Z i) : Type (max v w)))
    ((Hom.hom m : (a : (↑s.pt : Type (max v w))) → (↑(productCone Z).pt : Type (max v w))) x i :
      (↑(Z i) : Type (max v w)))
    ((Hom.hom
            (↟(LinearMap.pi (φ := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) fun (j : ι) ↦
                Hom.hom (s.π.app { as := j }))) :
          (a : (↑s.pt : Type (max v w))) → (↑(productCone Z).pt : Type (max v w)))
        x i :
      (↑(Z i) : Type (max v w)))

Tactic:
DFunLike.congr_fun (congr_arg Hom.hom (w ⟨i⟩)) x

Premises used: DFunLike.congr_fun, CategoryTheory.Discrete.mk, congr_arg, ModuleCat.Hom.hom
-- Module: Mathlib.Algebra.Category.ModuleCat.Products
Goal:
R : Type u
inst : Ring R
ι : Type v
Z : ι → ModuleCat R
s : Cone (Discrete.functor Z)
m : s.pt ⟶ (productCone.{u, v, w} Z).pt
w : ∀ (j : Discrete ι), m ≫ (productCone.{u, v, w} Z).π.app j = s.π.app j
x : (↑s.pt : Type (max v w))
i : ι
⊢ Eq (α := (↑(Z i) : Type (max v w)))
    ((Hom.hom m : (a : (↑s.pt : Type (max v w))) → (↑(productCone Z).pt : Type (max v w))) x i :
      (↑(Z i) : Type (max v w)))
    ((Hom.hom
            (↟(LinearMap.pi (φ := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) fun (j : ι) ↦
                Hom.hom (s.π.app { as := j }))) :
          (a : (↑s.pt : Type (max v w))) → (↑(productCone Z).pt : Type (max v w)))
        x i :
      (↑(Z i) : Type (max v w)))

Tactic:
exact DFunLike.congr_fun (congr_arg Hom.hom (w ⟨i⟩)) x

Premises used: DFunLike.congr_fun, CategoryTheory.Discrete.mk, congr_arg, ModuleCat.Hom.hom
-- Module: Mathlib.Algebra.Category.ModuleCat.Products
Goal:
R : Type u
inst : Ring R
ι : Type v
Z : ι → ModuleCat R
inst_1 : HasProduct Z
i : ι
⊢ CategoryStruct.comp (Y := ∏ᶜ Z) (Iso.inv (piIsoPi.{u, v, w} Z)) (Pi.π Z i) =
    ↟(LinearMap.proj (φ := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) i)

Tactic:
limit.isoLimitCone_inv_π _ _

Premises used: CategoryTheory.Limits.limit.isoLimitCone_inv_π
-- Module: Mathlib.Algebra.Category.ModuleCat.Products
Goal:
R : Type u
inst : Ring R
ι : Type v
Z : ι → ModuleCat R
inst_1 : HasProduct Z
i : ι
⊢ Eq (α := ∏ᶜ Z ⟶ of R (↑(Z i) : Type (max v w)))
    (Iso.hom (piIsoPi.{u, v, w} Z) ≫ ↟(LinearMap.proj (φ := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) i)) (Pi.π Z i)

Tactic:
IsLimit.conePointUniqueUpToIso_inv_comp _ (limit.isLimit _) (Discrete.mk i)

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Discrete.mk, CategoryTheory.Limits.limit, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp
-- Module: Mathlib.Algebra.Category.ModuleCat.Products
Goal:
R : Type u
inst : Ring R
ι : Type v
Z : ι → ModuleCat R
inst_1 : DecidableEq ι
s : Cocone (Discrete.functor Z)
i : ι
hf :
  ∀ (x : (↑(Z i) : Type (max v w))),
    Eq (α := (↑s.pt : Type (max v w)))
      ((Hom.hom
              ((coproductCocone.{u, v, w} Z).ι.app { as := i : Discrete ι } ≫
                ↟(toModule R ι (M := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) (↑s.1 : Type (max v w)) fun (i : ι) ↦
                    Hom.hom (s.ι.app { as := i }))) :
            (a : (↑((Discrete.functor Z).obj { as := i }) : Type (max v w))) → (↑s.pt : Type (max v w)))
          x :
        (↑s.pt : Type (max v w)))
      ((Hom.hom (s.ι.app { as := i }) :
            (a : (↑((Discrete.functor Z).obj { as := i }) : Type (max v w))) → (↑s.pt : Type (max v w)))
          x :
        (↑s.pt : Type (max v w)))
⊢ Eq (α := Functor.obj (Discrete.functor Z) { as := i : Discrete ι } ⟶ s.pt)
    ((coproductCocone.{u, v, w} Z).ι.app { as := i : Discrete ι } ≫
      ↟(toModule R ι (M := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) (↑s.1 : Type (max v w)) fun (i : ι) ↦
          Hom.hom (s.ι.app { as := i })))
    (s.ι.app { as := i })

Tactic:
ext (x : Z i)
-- Module: Mathlib.Algebra.Category.ModuleCat.Products
Goal:
R : Type u
inst : Ring R
ι : Type v
Z : ι → ModuleCat R
inst_1 : DecidableEq ι
s : Cocone (Discrete.functor Z)
i : ι
x : (↑(Z i) : Type (max v w))
⊢ Eq (α := (↑s.pt : Type (max v w)))
    ((Hom.hom
            ((coproductCocone.{u, v, w} Z).ι.app { as := i : Discrete ι } ≫
              ↟(toModule R ι (M := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) (↑s.1 : Type (max v w)) fun (i : ι) ↦
                  Hom.hom (s.ι.app { as := i }))) :
          (a : (↑((Discrete.functor Z).obj { as := i }) : Type (max v w))) → (↑s.pt : Type (max v w)))
        x :
      (↑s.pt : Type (max v w)))
    ((Hom.hom (s.ι.app { as := i }) :
          (a : (↑((Discrete.functor Z).obj { as := i }) : Type (max v w))) → (↑s.pt : Type (max v w)))
        x :
      (↑s.pt : Type (max v w)))

Tactic:
simpa only [Discrete.functor_obj_eq_as, coproductCocone, Cofan.mk_pt, Functor.const_obj_obj,
      Cofan.mk_ι_app, hom_comp, LinearMap.coe_comp, Function.comp_apply] using
      DirectSum.toModule_lof (ι := ι) R (M := fun i ↦ Z i) i x

Premises used: ModuleCat.coproductCocone, CategoryTheory.Limits.Cofan.mk_ι_app, CategoryTheory.Limits.Cofan.mk_pt, CategoryTheory.Discrete.functor_obj_eq_as, LinearMap.coe_comp, DirectSum.toModule_lof, Function.comp_apply, CategoryTheory.Functor.const_obj_obj, ModuleCat.hom_comp
-- Module: Mathlib.Algebra.Category.ModuleCat.Products
Goal:
R : Type u
inst : Ring R
ι : Type v
Z : ι → ModuleCat R
inst_1 : DecidableEq ι
s : Cocone (Discrete.functor Z)
f : (coproductCocone.{u, v, w} Z).pt ⟶ s.pt
h : ∀ (j : Discrete ι), (coproductCocone.{u, v, w} Z).ι.app j ≫ f = s.ι.app j
hf :
  Hom.hom f =
    Hom.hom
      (↟(toModule R ι (M := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) (↑s.1 : Type (max v w)) fun (i : ι) ↦
          Hom.hom (s.ι.app { as := i })))
⊢ f =
    ↟(toModule R ι (M := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) (↑s.1 : Type (max v w)) fun (i : ι) ↦
        Hom.hom (s.ι.app { as := i }))

Tactic:
ext : 1
-- Module: Mathlib.Algebra.Category.ModuleCat.Products
Goal:
R : Type u
inst : Ring R
ι : Type v
Z : ι → ModuleCat R
inst_1 : DecidableEq ι
s : Cocone (Discrete.functor Z)
f : (coproductCocone.{u, v, w} Z).pt ⟶ s.pt
h : ∀ (j : Discrete ι), (coproductCocone.{u, v, w} Z).ι.app j ≫ f = s.ι.app j
⊢ Hom.hom f =
    Hom.hom
      (↟(toModule R ι (M := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) (↑s.1 : Type (max v w)) fun (i : ι) ↦
          Hom.hom (s.ι.app { as := i })))

Tactic:
DirectSum.linearMap_ext _ fun i ↦ ?_

Premises used: DirectSum.linearMap_ext, DirectSum
-- Module: Mathlib.Algebra.Category.ModuleCat.Products
Goal:
R : Type u
inst : Ring R
ι : Type v
Z : ι → ModuleCat R
inst_1 : DecidableEq ι
s : Cocone (Discrete.functor Z)
f : (coproductCocone.{u, v, w} Z).pt ⟶ s.pt
h : ∀ (j : Discrete ι), (coproductCocone.{u, v, w} Z).ι.app j ≫ f = s.ι.app j
hf :
  ∀ (i : ι),
    Hom.hom f ∘ₗ lof R ι (fun (i : ι) ↦ (↑(Z i) : Type (max v w))) i =
      Hom.hom
          (↟(toModule R ι (M := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) (↑s.1 : Type (max v w)) fun (i : ι) ↦
              Hom.hom (s.ι.app { as := i }))) ∘ₗ
        lof R ι (fun (i : ι) ↦ (↑(Z i) : Type (max v w))) i
⊢ Hom.hom f =
    Hom.hom
      (↟(toModule R ι (M := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) (↑s.1 : Type (max v w)) fun (i : ι) ↦
          Hom.hom (s.ι.app { as := i })))

Tactic:
refine DirectSum.linearMap_ext _ fun i ↦ ?_

Premises used: DirectSum.linearMap_ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Products
Goal:
R : Type u
inst : Ring R
ι : Type v
Z : ι → ModuleCat R
inst_1 : DecidableEq ι
s : Cocone (Discrete.functor Z)
f : (coproductCocone.{u, v, w} Z).pt ⟶ s.pt
h : ∀ (j : Discrete ι), (coproductCocone.{u, v, w} Z).ι.app j ≫ f = s.ι.app j
i : ι
hf :
  ∀ (x : (↑(Z i) : Type (max v w))),
    Eq (α := (↑s.pt : Type (max v w)))
      ((Hom.hom f ∘ₗ lof R ι (fun (i : ι) ↦ (↑(Z i) : Type (max v w))) i :
            (a : (↑(Z i) : Type (max v w))) → (↑s.pt : Type (max v w)))
          x :
        (↑s.pt : Type (max v w)))
      ((Hom.hom
                (↟(toModule R ι (M := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) (↑s.1 : Type (max v w)) fun (i : ι) ↦
                    Hom.hom (s.ι.app { as := i }))) ∘ₗ
              lof R ι (fun (i : ι) ↦ (↑(Z i) : Type (max v w))) i :
            (a : (↑(Z i) : Type (max v w))) → (↑s.pt : Type (max v w)))
          x :
        (↑s.pt : Type (max v w)))
⊢ Hom.hom f ∘ₗ lof R ι (fun (i : ι) ↦ (↑(Z i) : Type (max v w))) i =
    Hom.hom
        (↟(toModule R ι (M := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) (↑s.1 : Type (max v w)) fun (i : ι) ↦
            Hom.hom (s.ι.app { as := i }))) ∘ₗ
      lof R ι (fun (i : ι) ↦ (↑(Z i) : Type (max v w))) i

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.ModuleCat.Products
Goal:
R : Type u
inst : Ring R
ι : Type v
Z : ι → ModuleCat R
inst_1 : DecidableEq ι
s : Cocone (Discrete.functor Z)
f : (coproductCocone.{u, v, w} Z).pt ⟶ s.pt
h : ∀ (j : Discrete ι), (coproductCocone.{u, v, w} Z).ι.app j ≫ f = s.ι.app j
i : ι
x : (↑(Z i) : Type (max v w))
⊢ Eq (α := (↑s.pt : Type (max v w)))
    ((Hom.hom f ∘ₗ lof R ι (fun (i : ι) ↦ (↑(Z i) : Type (max v w))) i :
          (a : (↑(Z i) : Type (max v w))) → (↑s.pt : Type (max v w)))
        x :
      (↑s.pt : Type (max v w)))
    ((Hom.hom
              (↟(toModule R ι (M := fun (i : ι) ↦ (↑(Z i) : Type (max v w))) (↑s.1 : Type (max v w)) fun (i : ι) ↦
                  Hom.hom (s.ι.app { as := i }))) ∘ₗ
            lof R ι (fun (i : ι) ↦ (↑(Z i) : Type (max v w))) i :
          (a : (↑(Z i) : Type (max v w))) → (↑s.pt : Type (max v w)))
        x :
      (↑s.pt : Type (max v w)))

Tactic:
simpa only [LinearMap.coe_comp, Function.comp_apply, hom_ofHom, toModule_lof] using
      congr($(h ⟨i⟩) x)

Premises used: LinearMap.coe_comp, DirectSum.toModule_lof, Function.comp_apply, ModuleCat.hom_ofHom
-- Module: Mathlib.Algebra.Category.ModuleCat.Products
Goal:
R : Type u
inst : Ring R
ι : Type v
Z : ι → ModuleCat R
inst_1 : DecidableEq ι
inst_2 : HasCoproduct Z
i : ι
⊢ CategoryStruct.comp (Y := ∐ Z) (Sigma.ι Z i) (Iso.hom (coprodIsoDirectSum.{u, v, w} Z)) =
    ↟(lof R ι (fun (i : ι) ↦ (↑(Z i) : Type (max v w))) i)

Tactic:
colimit.isoColimitCocone_ι_hom _ _

Premises used: CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom
-- Module: Mathlib.Algebra.Category.ModuleCat.Products
Goal:
R : Type u
inst : Ring R
ι : Type v
Z : ι → ModuleCat R
inst_1 : DecidableEq ι
inst_2 : HasCoproduct Z
i : ι
⊢ Eq (α := of R (↑(Z i) : Type (max v w)) ⟶ ∐ Z)
    (↟(lof R ι (fun (i : ι) ↦ (↑(Z i) : Type (max v w))) i) ≫ Iso.inv (coprodIsoDirectSum.{u, v, w} Z)) (Sigma.ι Z i)

Tactic:
(coproductCoconeIsColimit Z).comp_coconePointUniqueUpToIso_hom (colimit.isColimit _) _

Premises used: ModuleCat.coproductCoconeIsColimit, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.colimit, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.Algebra.Category.ModuleCat.Projective
Goal:
R : Type u
inst : Ring R
P : ModuleCat.{v, u} R
inst_1 : Module.Projective.{u, v} R (↑P : Type v)
⊢ CategoryTheory.Projective P

Tactic:
⟨fun E X epi => ?_⟩

Premises used: CategoryTheory.Projective.mk
-- Module: Mathlib.Algebra.Category.ModuleCat.Projective
Goal:
R : Type u
inst : Ring R
P : ModuleCat.{v, u} R
inst_1 : Module.Projective.{u, v} R (↑P : Type v)
refine : ∀ {E X : ModuleCat.{v, u} R} (E_1 : P ⟶ X) (X_1 : E ⟶ X) (epi : Epi X_1), ∃ (f' : P ⟶ E), f' ≫ X_1 = E_1
⊢ CategoryTheory.Projective P

Tactic:
refine ⟨fun E X epi => ?_⟩
-- Module: Mathlib.Algebra.Category.ModuleCat.Projective
Goal:
R : Type u
inst : Ring R
P : ModuleCat.{v, u} R
inst_1 : Module.Projective.{u, v} R (↑P : Type v)
E_1 X_1 : ModuleCat.{v, u} R
E : P ⟶ X_1
X : E_1 ⟶ X_1
epi : Epi X
obtain : ∀ (f : (↑P : Type v) →ₗ[R] (↑E_1 : Type v)) (h : Hom.hom X ∘ₗ f = Hom.hom E), ∃ (f' : P ⟶ E_1), f' ≫ X = E
⊢ ∃ (f' : P ⟶ E_1), f' ≫ X = E

Tactic:
obtain ⟨f, h⟩ := Module.projective_lifting_property X.hom E.hom
    ((ModuleCat.epi_iff_surjective _).mp epi)

Premises used: ModuleCat.epi_iff_surjective, Iff.mp, Module.projective_lifting_property, ModuleCat.Hom.hom
-- Module: Mathlib.Algebra.Category.ModuleCat.Projective
Goal:
R : Type u
inst : Ring R
P : ModuleCat.{v, u} R
inst_1 : Module.Projective.{u, v} R (↑P : Type v)
E_1 X_1 : ModuleCat.{v, u} R
E : P ⟶ X_1
X : E_1 ⟶ X_1
epi : Epi X
f : (↑P : Type v) →ₗ[R] (↑E_1 : Type v)
h : Hom.hom X ∘ₗ f = Hom.hom E
⊢ ∃ (f' : P ⟶ E_1), f' ≫ X = E

Tactic:
⟨ofHom f, hom_ext h⟩

Premises used: Exists.intro, ModuleCat.hom_ext, ModuleCat.ofHom
-- Module: Mathlib.Algebra.Category.ModuleCat.Projective
Goal:
R : Type u
inst : Ring R
P : ModuleCat.{v, u} R
inst_1 : Module.Projective.{u, v} R (↑P : Type v)
E_1 X_1 : ModuleCat.{v, u} R
E : P ⟶ X_1
X : E_1 ⟶ X_1
epi : Epi X
f : (↑P : Type v) →ₗ[R] (↑E_1 : Type v)
h : Hom.hom X ∘ₗ f = Hom.hom E
⊢ ∃ (f' : P ⟶ E_1), f' ≫ X = E

Tactic:
exact ⟨ofHom f, hom_ext h⟩
-- Module: Mathlib.Algebra.Category.ModuleCat.Projective
Goal:
R : Type u
inst : Ring R
P : ModuleCat.{v, u} R
inst_1 : Small.{v, u} R
inst_2 : CategoryTheory.Projective P
⊢ Module.Projective.{u, v} R (↑P : Type v)

Tactic:
Module.Projective.of_lifting_property ?_

Premises used: Module.Projective.of_lifting_property
-- Module: Mathlib.Algebra.Category.ModuleCat.Projective
Goal:
R : Type u
inst : Ring R
P : ModuleCat.{v, u} R
inst_1 : Small.{v, u} R
inst_2 : CategoryTheory.Projective P
refine :
  ∀ {M N : Type v} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N]
    (f : M →ₗ[R] N) (g : (↑P : Type v) →ₗ[R] N),
    Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N) → ∃ (h : (↑P : Type v) →ₗ[R] M), f ∘ₗ h = g
⊢ Module.Projective.{u, v} R (↑P : Type v)

Tactic:
refine Module.Projective.of_lifting_property ?_

Premises used: Module.Projective.of_lifting_property
-- Module: Mathlib.Algebra.Category.ModuleCat.Projective
Goal:
R : Type u
inst : Ring R
P : ModuleCat.{v, u} R
inst_1 : Small.{v, u} R
inst_2 : CategoryTheory.Projective P
M : Type v
_ :
  ∀ {N : Type v} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N]
    (f : M →ₗ[R] N) (g : (↑P : Type v) →ₗ[R] N),
    Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N) → ∃ (h : (↑P : Type v) →ₗ[R] M), f ∘ₗ h = g
⊢ ∀ {N : Type v} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N]
    (f : M →ₗ[R] N) (g : (↑P : Type v) →ₗ[R] N),
    Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N) → ∃ (h : (↑P : Type v) →ₗ[R] M), f ∘ₗ h = g

Tactic:
_
-- Module: Mathlib.Algebra.Category.ModuleCat.Projective
Goal:
R : Type u
inst : Ring R
P : ModuleCat.{v, u} R
inst_1 : Small.{v, u} R
inst_2 : CategoryTheory.Projective P
M N : Type v
_ :
  ∀ [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N] (f : M →ₗ[R] N)
    (g : (↑P : Type v) →ₗ[R] N),
    Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N) → ∃ (h : (↑P : Type v) →ₗ[R] M), f ∘ₗ h = g
⊢ ∀ [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N] (f : M →ₗ[R] N)
    (g : (↑P : Type v) →ₗ[R] N),
    Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N) → ∃ (h : (↑P : Type v) →ₗ[R] M), f ∘ₗ h = g

Tactic:
_
-- Module: Mathlib.Algebra.Category.ModuleCat.Projective
Goal:
R : Type u
inst : Ring R
P : ModuleCat.{v, u} R
inst_1 : Small.{v, u} R
inst_2 : CategoryTheory.Projective P
M N : Type v
inst_3 : AddCommGroup M
_ :
  ∀ [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N] (f : M →ₗ[R] N) (g : (↑P : Type v) →ₗ[R] N),
    Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N) → ∃ (h : (↑P : Type v) →ₗ[R] M), f ∘ₗ h = g
⊢ ∀ [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N] (f : M →ₗ[R] N) (g : (↑P : Type v) →ₗ[R] N),
    Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N) → ∃ (h : (↑P : Type v) →ₗ[R] M), f ∘ₗ h = g

Tactic:
_
-- Module: Mathlib.Algebra.Category.ModuleCat.Projective
Goal:
R : Type u
inst : Ring R
P : ModuleCat.{v, u} R
inst_1 : Small.{v, u} R
inst_2 : CategoryTheory.Projective P
M N : Type v
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
_ :
  ∀ [inst_5 : Module R M] [inst_6 : Module R N] (f : M →ₗ[R] N) (g : (↑P : Type v) →ₗ[R] N),
    Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N) → ∃ (h : (↑P : Type v) →ₗ[R] M), f ∘ₗ h = g
⊢ ∀ [inst_5 : Module R M] [inst_6 : Module R N] (f : M →ₗ[R] N) (g : (↑P : Type v) →ₗ[R] N),
    Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N) → ∃ (h : (↑P : Type v) →ₗ[R] M), f ∘ₗ h = g

Tactic:
_
-- Module: Mathlib.Algebra.Category.ModuleCat.Projective
Goal:
R : Type u
inst : Ring R
P : ModuleCat.{v, u} R
inst_1 : Small.{v, u} R
inst_2 : CategoryTheory.Projective P
M N : Type v
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
_ :
  ∀ [inst_6 : Module R N] (f : M →ₗ[R] N) (g : (↑P : Type v) →ₗ[R] N),
    Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N) → ∃ (h : (↑P : Type v) →ₗ[R] M), f ∘ₗ h = g
⊢ ∀ [inst_6 : Module R N] (f : M →ₗ[R] N) (g : (↑P : Type v) →ₗ[R] N),
    Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N) → ∃ (h : (↑P : Type v) →ₗ[R] M), f ∘ₗ h = g

Tactic:
_
-- Module: Mathlib.Algebra.Category.ModuleCat.Projective
Goal:
R : Type u
inst : Ring R
P : ModuleCat.{v, u} R
inst_1 : Small.{v, u} R
inst_2 : CategoryTheory.Projective P
M N : Type v
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
f : M →ₗ[R] N
g : (↑P : Type v) →ₗ[R] N
s : Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Epi (↟f)

Tactic:
have : Epi (↟f) := (ModuleCat.epi_iff_surjective (↟f)).mpr s
-- Module: Mathlib.Algebra.Category.ModuleCat.Projective
Goal:
R : Type u
inst : Ring R
P : ModuleCat.{v, u} R
inst_1 : Small.{v, u} R
inst_2 : CategoryTheory.Projective P
M N : Type v
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
f : M →ₗ[R] N
g : (↑P : Type v) →ₗ[R] N
s : Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N)
this : Epi (↟f)
⊢ ∃ (h : (↑P : Type v) →ₗ[R] M), f ∘ₗ h = g

Tactic:
⟨(Projective.factorThru (↟g) (↟f)).hom,
    ModuleCat.hom_ext_iff.mp <| Projective.factorThru_comp (↟g) (↟f)⟩

Premises used: CategoryTheory.Projective.factorThru, ModuleCat.hom_ext_iff, CategoryTheory.Projective.factorThru_comp, Exists.intro, Iff.mp, ModuleCat.ofHom, ModuleCat.Hom.hom
-- Module: Mathlib.Algebra.Category.ModuleCat.Projective
Goal:
R : Type u
inst : Ring R
P : ModuleCat.{v, u} R
inst_1 : Small.{v, u} R
inst_2 : CategoryTheory.Projective P
M N : Type v
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
f : M →ₗ[R] N
g : (↑P : Type v) →ₗ[R] N
s : Function.Surjective (α := M) (β := N) (⇑f : (a : M) → N)
this : Epi (↟f)
⊢ ∃ (h : (↑P : Type v) →ₗ[R] M), f ∘ₗ h = g

Tactic:
exact ⟨(Projective.factorThru (↟g) (↟f)).hom,
    ModuleCat.hom_ext_iff.mp <| Projective.factorThru_comp (↟g) (↟f)⟩
-- Module: Mathlib.Algebra.Category.ModuleCat.Projective
Goal:
R : Type u
inst : Ring R
inst_1 : Small.{v, u} R
P : Type v
inst_2 : AddCommGroup P
inst_3 : Module R P
⊢ Module.Projective R P ↔ CategoryTheory.Projective (C := ModuleCat.{v, u} R) (of R P)

Tactic:
⟨fun _ => (of R P).projective_of_categoryTheory_projective,
    fun _ => (of R P).projective_of_module_projective⟩

Premises used: ModuleCat.of, ModuleCat.projective_of_categoryTheory_projective, Iff.intro, ModuleCat.projective_of_module_projective
-- Module: Mathlib.Algebra.Category.ModuleCat.Projective
Goal:
R : Type u
inst : Ring R
M : ModuleCat.{v, u} R
ι : Type w
b : Basis.{w, u, v} ι R (↑M : Type v)
⊢ CategoryTheory.Projective M

Tactic:
have : Module.Projective R M := Module.Projective.of_basis b
  M.projective_of_categoryTheory_projective

Premises used: ModuleCat.projective_of_categoryTheory_projective, Module.Projective.of_basis