awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings
Goal:
C : Type u'
inst : Category.{v', u'} C
R R' : CategoryTheory.Functor.{v', u, u', u + 1} Cᵒᵖ RingCat
α : R ⟶ R'
X_1 Y_1 : PresheafOfModules.{v, v', u', u} R'
φ' : X_1 ⟶ Y_1
X Y : Cᵒᵖ
f : X ⟶ Y
x : (↑((X_1.restrictScalarsObj α).obj X) : Type v)
⊢ Eq (α := (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj ((Y_1.restrictScalarsObj α).obj Y)) : Type v))
    ((ModuleCat.Hom.hom
            ((X_1.restrictScalarsObj α).map f ≫
              (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
                ((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app Y))).map (φ'.app Y))) :
          (a : (↑((X_1.restrictScalarsObj α).obj X) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj ((Y_1.restrictScalarsObj α).obj Y)) :
              Type v))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj ((Y_1.restrictScalarsObj α).obj Y)) : Type v))
    ((ModuleCat.Hom.hom
            ((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app X))).map (φ'.app X) ≫
              (Y_1.restrictScalarsObj α).map f) :
          (a : (↑((X_1.restrictScalarsObj α).obj X) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj ((Y_1.restrictScalarsObj α).obj Y)) :
              Type v))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj ((Y_1.restrictScalarsObj α).obj Y)) : Type v))

Tactic:
naturality_apply φ' f x

Premises used: PresheafOfModules.naturality_apply
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings
Goal:
C : Type u'
inst : Category.{v', u'} C
R R' : CategoryTheory.Functor.{v', u, u', u + 1} Cᵒᵖ RingCat
α : R ⟶ R'
X_1 Y_1 : PresheafOfModules.{v, v', u', u} R'
φ' : X_1 ⟶ Y_1
X Y : Cᵒᵖ
f : X ⟶ Y
x : (↑((X_1.restrictScalarsObj α).obj X) : Type v)
⊢ Eq (α := (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj ((Y_1.restrictScalarsObj α).obj Y)) : Type v))
    ((ModuleCat.Hom.hom
            ((X_1.restrictScalarsObj α).map f ≫
              (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
                ((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app Y))).map (φ'.app Y))) :
          (a : (↑((X_1.restrictScalarsObj α).obj X) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj ((Y_1.restrictScalarsObj α).obj Y)) :
              Type v))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj ((Y_1.restrictScalarsObj α).obj Y)) : Type v))
    ((ModuleCat.Hom.hom
            ((ModuleCat.restrictScalars (RingCat.Hom.hom (α.app X))).map (φ'.app X) ≫
              (Y_1.restrictScalarsObj α).map f) :
          (a : (↑((X_1.restrictScalarsObj α).obj X) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj ((Y_1.restrictScalarsObj α).obj Y)) :
              Type v))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj ((Y_1.restrictScalarsObj α).obj Y)) : Type v))

Tactic:
exact naturality_apply φ' f x

Premises used: PresheafOfModules.naturality_apply
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings
Goal:
C : Type u'
inst : Category.{v', u'} C
R R' : CategoryTheory.Functor.{v', u, u', u + 1} Cᵒᵖ RingCat
⊢ (restrictScalars (𝟙 R)).Full

Tactic:
inferInstanceAs (𝟭 _).Full

Premises used: _private.0.PresheafOfModules.instFullRestrictScalarsIdFunctorOppositeRingCat._proof_1
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : IsCofiltered.{v, u} C
inst_3 : InitiallySmall.{w, v, u} C
R : CategoryTheory.Functor.{v, w, u, w + 1} Cᵒᵖ RingCat
cR : Cocone R
hcR : IsColimit cR
M : ModuleCat (↑cR.pt : Type w)
X Y : Cᵒᵖ
f : X ⟶ Y
a :
  ∀ (x : (↑(R.obj X) : Type w)),
    Eq (α := (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const Cᵒᵖ) cR.pt) X) : Type w))
      ((RingCat.Hom.hom (cR.ι.app X) :
            (a : (↑(R.obj X) : Type w)) → (↑(((Functor.const Cᵒᵖ).obj cR.pt).obj X) : Type w))
          x :
        (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const Cᵒᵖ) cR.pt) X) : Type w))
      (((RingCat.Hom.hom (cR.ι.app Y)).comp (RingCat.Hom.hom (R.map f)) :
            (a : (↑(R.obj X) : Type w)) → (↑(((Functor.const Cᵒᵖ).obj cR.pt).obj X) : Type w))
          x :
        (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const Cᵒᵖ) cR.pt) X) : Type w))
⊢ RingCat.Hom.hom (cR.ι.app X) = (RingCat.Hom.hom (cR.ι.app Y)).comp (RingCat.Hom.hom (R.map f))

Tactic:
ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : IsCofiltered.{v, u} C
inst_3 : InitiallySmall.{w, v, u} C
R : CategoryTheory.Functor.{v, w, u, w + 1} Cᵒᵖ RingCat
cR : Cocone R
hcR : IsColimit cR
M : ModuleCat (↑cR.pt : Type w)
X Y : Cᵒᵖ
f : X ⟶ Y
x : (↑(R.obj X) : Type w)
a :
  Eq (α := (↑cR.pt : Type w))
    ((RingCat.Hom.hom (cR.ι.app X) : (a : (↑(R.obj X) : Type w)) → (↑cR.pt : Type w)) x : (↑cR.pt : Type w))
    (((RingCat.Hom.hom (cR.ι.app Y)).comp (RingCat.Hom.hom (R.map f)) : (a : (↑(R.obj X) : Type w)) → (↑cR.pt : Type w))
        x :
      (↑cR.pt : Type w))
⊢ Eq (α := (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const Cᵒᵖ) cR.pt) X) : Type w))
    ((RingCat.Hom.hom (cR.ι.app X) : (a : (↑(R.obj X) : Type w)) → (↑(((Functor.const Cᵒᵖ).obj cR.pt).obj X) : Type w))
        x :
      (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const Cᵒᵖ) cR.pt) X) : Type w))
    (((RingCat.Hom.hom (cR.ι.app Y)).comp (RingCat.Hom.hom (R.map f)) :
          (a : (↑(R.obj X) : Type w)) → (↑(((Functor.const Cᵒᵖ).obj cR.pt).obj X) : Type w))
        x :
      (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const Cᵒᵖ) cR.pt) X) : Type w))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : IsCofiltered.{v, u} C
inst_3 : InitiallySmall.{w, v, u} C
R : CategoryTheory.Functor.{v, w, u, w + 1} Cᵒᵖ RingCat
cR : Cocone R
hcR : IsColimit cR
M : ModuleCat (↑cR.pt : Type w)
X Y : Cᵒᵖ
f : X ⟶ Y
x : (↑(R.obj X) : Type w)
a :
  Eq (α := (↑cR.pt : Type w))
    ((RingCat.Hom.hom (R.map f ≫ cR.ι.app Y) : (a : (↑(R.obj X) : Type w)) → (↑cR.pt : Type w)) x : (↑cR.pt : Type w))
    (((RingCat.Hom.hom (cR.ι.app Y)).comp (RingCat.Hom.hom (R.map f)) : (a : (↑(R.obj X) : Type w)) → (↑cR.pt : Type w))
        x :
      (↑cR.pt : Type w))
⊢ Eq (α := (↑cR.pt : Type w))
    ((RingCat.Hom.hom (cR.ι.app X) : (a : (↑(R.obj X) : Type w)) → (↑cR.pt : Type w)) x : (↑cR.pt : Type w))
    (((RingCat.Hom.hom (cR.ι.app Y)).comp (RingCat.Hom.hom (R.map f)) : (a : (↑(R.obj X) : Type w)) → (↑cR.pt : Type w))
        x :
      (↑cR.pt : Type w))

Tactic:
rw [← Cocone.w cR f]

Premises used: CategoryTheory.Limits.Cocone.w
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : IsCofiltered.{v, u} C
inst_3 : InitiallySmall.{w, v, u} C
R : CategoryTheory.Functor.{v, w, u, w + 1} Cᵒᵖ RingCat
cR : Cocone R
hcR : IsColimit cR
M : ModuleCat (↑cR.pt : Type w)
X Y : Cᵒᵖ
f : X ⟶ Y
x : (↑(R.obj X) : Type w)
a :
  Eq (α := (↑cR.pt : Type w))
    (((RingCat.Hom.hom (cR.ι.app Y)).comp (RingCat.Hom.hom (R.map f)) : (a : (↑(R.obj X) : Type w)) → (↑cR.pt : Type w))
        x :
      (↑cR.pt : Type w))
    (((RingCat.Hom.hom (cR.ι.app Y)).comp (RingCat.Hom.hom (R.map f)) : (a : (↑(R.obj X) : Type w)) → (↑cR.pt : Type w))
        x :
      (↑cR.pt : Type w))
⊢ Eq (α := (↑cR.pt : Type w))
    ((RingCat.Hom.hom (R.map f ≫ cR.ι.app Y) : (a : (↑(R.obj X) : Type w)) → (↑cR.pt : Type w)) x : (↑cR.pt : Type w))
    (((RingCat.Hom.hom (cR.ι.app Y)).comp (RingCat.Hom.hom (R.map f)) : (a : (↑(R.obj X) : Type w)) → (↑cR.pt : Type w))
        x :
      (↑cR.pt : Type w))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : IsCofiltered.{v, u} C
inst_3 : InitiallySmall.{w, v, u} C
R : CategoryTheory.Functor.{v, w, u, w + 1} Cᵒᵖ RingCat
cR : Cocone R
hcR : IsColimit cR
M : ModuleCat (↑cR.pt : Type w)
X Y : Cᵒᵖ
f : X ⟶ Y
x : (↑(R.obj X) : Type w)
⊢ Eq (α := (↑cR.pt : Type w))
    (((RingCat.Hom.hom (cR.ι.app Y)).comp (RingCat.Hom.hom (R.map f)) : (a : (↑(R.obj X) : Type w)) → (↑cR.pt : Type w))
        x :
      (↑cR.pt : Type w))
    (((RingCat.Hom.hom (cR.ι.app Y)).comp (RingCat.Hom.hom (R.map f)) : (a : (↑(R.obj X) : Type w)) → (↑cR.pt : Type w))
        x :
      (↑cR.pt : Type w))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : IsCofiltered.{v, u} C
inst_3 : InitiallySmall.{w, v, u} C
R : CategoryTheory.Functor.{v, w, u, w + 1} Cᵒᵖ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
U : Cᵒᵖ
x :
  (tensorObj (𝒞 := Functor.category)
        (R ⋙ forget RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC := RingCat.carrier))
        (M.presheaf ⋙
          forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
            AddCommGrpCat.carrier))).obj
    U
r : (↑(R.obj U) : Type w)
m : (↑(M.obj U) : Type w)
⊢ Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const Cᵒᵖ) (ModuleColimit hcR hcM)) U

Tactic:
exact cM.ι.app U (r • m)

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.Cocone.ι, HSMul.hSMul, DFunLike.coe, CategoryTheory.NatTrans.app
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : IsCofiltered.{v, u} C
inst_3 : InitiallySmall.{w, v, u} C
R : CategoryTheory.Functor.{v, w, u, w + 1} Cᵒᵖ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
U : Cᵒᵖ
r : (↑(R.obj U) : Type w)
m : (↑(M.obj U) : Type w)
⊢ HSMul.hSMul (α := (↑cR.pt : Type w)) (β := ModuleColimit hcR hcM)
      ((ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) r : (↑cR.pt : Type w))
      ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM) =
    (ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) (r • m)

Tactic:
ConcreteCategory.congr_hom (((isColimitOfPreserves (forget _) hcR).tensor
    (isColimitOfPreserves (forget _) hcM)).fac (coconeSMul hcR hcM) U) ⟨r, m⟩

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.IsColimit.tensor, PresheafOfModules.ModuleColimit.coconeSMul, CategoryTheory.forget, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Limits.isColimitOfPreserves, PresheafOfModules.ModuleColimit
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : IsCofiltered.{v, u} C
inst_3 : InitiallySmall.{w, v, u} C
R : CategoryTheory.Functor.{v, w, u, w + 1} Cᵒᵖ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
m : ModuleColimit hcR hcM
⊢ ∃ (U : Cᵒᵖ) (x : (↑(M.obj U) : Type w)), (ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) x = m

Tactic:
Types.jointly_surjective_of_isColimit
    (isColimitOfPreserves (forget AddCommGrpCat) hcM) m

Premises used: CategoryTheory.Limits.Types.jointly_surjective_of_isColimit, AddCommGrpCat, CategoryTheory.forget, CategoryTheory.Limits.isColimitOfPreserves, PresheafOfModules.ModuleColimit
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : IsCofiltered.{v, u} C
inst_3 : InitiallySmall.{w, v, u} C
R : CategoryTheory.Functor.{v, w, u, w + 1} Cᵒᵖ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
m : ModuleColimit hcR hcM
m' : ModuleColimit hcR hcM'
obtain :
  ∀ (U : Cᵒᵖ)
    (x :
      (M.presheaf ⋙
            forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              AddCommGrpCat.carrier)).obj
        U)
    (x' :
      (M'.presheaf ⋙
            forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              AddCommGrpCat.carrier)).obj
        U)
    (h :
      (ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app
                (Cocone.ι
                  (Cocone.tensor
                    (Functor.mapCocone
                      (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
                        (CC := AddCommGrpCat.carrier))
                      cM)
                    (Functor.mapCocone
                      (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
                        (CC := AddCommGrpCat.carrier))
                      cM')))
                U) :
            (a :
                (fun (X : Type w) ↦ X)
                  ((M.presheaf ⋙ forget AddCommGrpCat ⊗ M'.presheaf ⋙ forget AddCommGrpCat).obj U)) →
              (fun (X : Type w) ↦ X)
                (((Functor.const Cᵒᵖ).obj
                      (((forget AddCommGrpCat).mapCocone cM).tensor ((forget AddCommGrpCat).mapCocone cM')).pt).obj
                  U))
          (x, x') =
        (m, m')),
    ∃ (U : Cᵒᵖ) (x : (↑(M.obj U) : Type w)) (x' : (↑(M'.obj U) : Type w)),
      (ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) x = m ∧
        (ιM : (a : (↑(M'.obj U) : Type w)) → ModuleColimit hcR hcM') x' = m'
⊢ ∃ (U : Cᵒᵖ) (x : (↑(M.obj U) : Type w)) (x' : (↑(M'.obj U) : Type w)),
    (ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) x = m ∧
      (ιM : (a : (↑(M'.obj U) : Type w)) → ModuleColimit hcR hcM') x' = m'

Tactic:
obtain ⟨U, ⟨x, x'⟩, h⟩ := Types.jointly_surjective_of_isColimit
    ((isColimitOfPreserves (forget AddCommGrpCat) hcM).tensor
      (isColimitOfPreserves (forget AddCommGrpCat) hcM')) ⟨m, m'⟩

Premises used: CategoryTheory.Limits.IsColimit.tensor, Prod.mk, CategoryTheory.Limits.Types.jointly_surjective_of_isColimit, AddCommGrpCat, CategoryTheory.forget, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : IsCofiltered.{v, u} C
inst_3 : InitiallySmall.{w, v, u} C
R : CategoryTheory.Functor.{v, w, u, w + 1} Cᵒᵖ RingCat
cR : Cocone R
hcR : IsColimit cR
r : (↑cR.pt : Type w)
⊢ ∃ (U : Cᵒᵖ) (a : (↑(R.obj U) : Type w)), (ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) a = r

Tactic:
Types.jointly_surjective_of_isColimit
    (isColimitOfPreserves (forget RingCat) hcR) r

Premises used: RingCat, CategoryTheory.Limits.Types.jointly_surjective_of_isColimit, CategoryTheory.forget, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : IsCofiltered.{v, u} C
inst_3 : InitiallySmall.{w, v, u} C
R : CategoryTheory.Functor.{v, w, u, w + 1} Cᵒᵖ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
r : (↑cR.pt : Type w)
m : ModuleColimit hcR hcM
obtain :
  ∀ (U : Cᵒᵖ)
    (a :
      (R ⋙ forget RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC := RingCat.carrier)).obj
        U)
    (x :
      (M.presheaf ⋙
            forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              AddCommGrpCat.carrier)).obj
        U)
    (h :
      (ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app
                (Cocone.ι
                  (Cocone.tensor
                    (Functor.mapCocone
                      (forget RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
                        RingCat.carrier))
                      cR)
                    (Functor.mapCocone
                      (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
                        (CC := AddCommGrpCat.carrier))
                      cM)))
                U) :
            (a : (fun (X : Type w) ↦ X) ((R ⋙ forget RingCat ⊗ M.presheaf ⋙ forget AddCommGrpCat).obj U)) →
              (fun (X : Type w) ↦ X)
                (((Functor.const Cᵒᵖ).obj
                      (((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM)).pt).obj
                  U))
          (a, x) =
        (r, m)),
    ∃ (U : Cᵒᵖ) (a : (↑(R.obj U) : Type w)) (x : (↑(M.obj U) : Type w)),
      (ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) a = r ∧
        (ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) x = m
⊢ ∃ (U : Cᵒᵖ) (a : (↑(R.obj U) : Type w)) (x : (↑(M.obj U) : Type w)),
    (ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) a = r ∧
      (ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) x = m

Tactic:
obtain ⟨U, ⟨a, x⟩, h⟩ := Types.jointly_surjective_of_isColimit
    ((isColimitOfPreserves (forget RingCat) hcR).tensor
      (isColimitOfPreserves (forget AddCommGrpCat) hcM)) ⟨r, m⟩

Premises used: CategoryTheory.Limits.IsColimit.tensor, Prod.mk, RingCat, CategoryTheory.Limits.Types.jointly_surjective_of_isColimit, AddCommGrpCat, CategoryTheory.forget, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : IsCofiltered.{v, u} C
inst_3 : InitiallySmall.{w, v, u} C
R : CategoryTheory.Functor.{v, w, u, w + 1} Cᵒᵖ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
r₁ r₂ : (↑cR.pt : Type w)
m : ModuleColimit hcR hcM
obtain :
  ∀ (U : Cᵒᵖ) (r₁ r₂ : (↑(R.obj U) : Type w)) (m : (↑(M.obj U) : Type w)),
    HSMul.hSMul (β := ModuleColimit hcR hcM)
        (HMul.hMul (α := (↑cR.pt : Type w)) (β := (↑cR.pt : Type w))
          ((ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) r₁ : (↑cR.pt : Type w))
          ((ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) r₂ : (↑cR.pt : Type w)))
        ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM) =
      HSMul.hSMul (α := (↑cR.pt : Type w))
        ((ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) r₁ : (↑cR.pt : Type w))
        (HSMul.hSMul (α := (↑cR.pt : Type w)) (β := ModuleColimit hcR hcM)
          ((ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) r₂ : (↑cR.pt : Type w))
          ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM))
⊢ (r₁ * r₂) • m = r₁ • r₂ • m

Tactic:
obtain ⟨U, r₁, r₂, m, rfl, rfl, rfl⟩ := jointly_surjective₃ r₁ r₂ m

Premises used: PresheafOfModules.ModuleColimit.jointly_surjective₃, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : IsCofiltered.{v, u} C
inst_3 : InitiallySmall.{w, v, u} C
R : CategoryTheory.Functor.{v, w, u, w + 1} Cᵒᵖ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
U : Cᵒᵖ
r₁ r₂ : (↑(R.obj U) : Type w)
m : (↑(M.obj U) : Type w)
⊢ HSMul.hSMul (β := ModuleColimit hcR hcM)
      (HMul.hMul (α := (↑cR.pt : Type w)) (β := (↑cR.pt : Type w))
        ((ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) r₁ : (↑cR.pt : Type w))
        ((ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) r₂ : (↑cR.pt : Type w)))
      ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM) =
    HSMul.hSMul (α := (↑cR.pt : Type w))
      ((ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) r₁ : (↑cR.pt : Type w))
      (HSMul.hSMul (α := (↑cR.pt : Type w)) (β := ModuleColimit hcR hcM)
        ((ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) r₂ : (↑cR.pt : Type w))
        ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM))

Tactic:
simp only [smul_eq, ← mul_smul, ← map_mul]

Premises used: PresheafOfModules.ModuleColimit.smul_eq, map_mul, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : IsCofiltered.{v, u} C
inst_3 : InitiallySmall.{w, v, u} C
R : CategoryTheory.Functor.{v, w, u, w + 1} Cᵒᵖ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
m : ModuleColimit hcR hcM
obtain :
  ∀ (U : Cᵒᵖ) (m : (↑(M.obj U) : Type w)),
    HSMul.hSMul (α := (↑cR.pt : Type w)) (β := ModuleColimit hcR hcM) 1
        ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM) =
      (ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m
⊢ HSMul.hSMul (α := (↑cR.pt : Type w)) 1 m = m

Tactic:
obtain ⟨U, m, rfl⟩ := ιM_jointly_surjective m

Premises used: PresheafOfModules.ModuleColimit.ιM_jointly_surjective, rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : IsCofiltered.{v, u} C
inst_3 : InitiallySmall.{w, v, u} C
R : CategoryTheory.Functor.{v, w, u, w + 1} Cᵒᵖ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
U : Cᵒᵖ
m : (↑(M.obj U) : Type w)
⊢ HSMul.hSMul (α := (↑cR.pt : Type w)) (β := ModuleColimit hcR hcM) 1
      ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM) =
    (ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m

Tactic:
simpa using smul_eq hcR hcM 1 m

Premises used: PresheafOfModules.ModuleColimit.smul_eq, OfNat.ofNat
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
inst_2 : IsCofiltered.{v, u} C
inst_3 : InitiallySmall.{w, v, u} C
R : CategoryTheory.Functor.{v, w, u, w + 1} Cᵒᵖ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
r : (↑cR.pt : Type w)
obtain :
  ∀ (U : Cᵒᵖ) (r : (↑(R.obj U) : Type w)),
    HSMul.hSMul (α := (↑cR.pt : Type w)) (β := ModuleColimit hcR hcM)
        ((ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) r : (↑cR.pt : Type w)) 0 =
      0
⊢ HSMul.hSMul (β := ModuleColimit hcR hcM) r 0 = 0

Tactic:
obtain ⟨U, r, rfl⟩ := ιR_jointly_surjective hcR r

Premises used: PresheafOfModules.ModuleColimit.ιR_jointly_surjective, rfl