awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.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

Tactic:
simpa using smul_eq hcR hcM r 0

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)
m₁ m₂ : ModuleColimit hcR hcM
obtain :
  ∀ (U : Cᵒᵖ) (r : (↑(R.obj U) : Type w)) (m₁ m₂ : (↑(M.obj U) : Type w)),
    HSMul.hSMul (α := (↑cR.pt : Type w))
        ((ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) r : (↑cR.pt : Type w))
        (HAdd.hAdd (α := ModuleColimit hcR hcM) (β := ModuleColimit hcR hcM)
          ((ι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₂ : ModuleColimit hcR hcM)) =
      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) +
        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 • (m₁ + m₂) = r • m₁ + r • m₂

Tactic:
obtain ⟨U, r, m₁, m₂, rfl, rfl, rfl⟩ := jointly_surjective₃' r m₁ 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.obj U) : Type w)
m₁ m₂ : (↑(M.obj U) : Type w)
⊢ HSMul.hSMul (α := (↑cR.pt : Type w)) ((ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) r : (↑cR.pt : Type w))
      (HAdd.hAdd (α := ModuleColimit hcR hcM) (β := ModuleColimit hcR hcM)
        ((ι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₂ : ModuleColimit hcR hcM)) =
    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) +
      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, smul_add, ← map_add]

Premises used: map_add, PresheafOfModules.ModuleColimit.smul_eq, smul_add
-- 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)
        (HAdd.hAdd (α := (↑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)) (β := 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) +
        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₁ • m + 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)
      (HAdd.hAdd (α := (↑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)) (β := 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) +
      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, ← map_add, add_smul]

Premises used: map_add, PresheafOfModules.ModuleColimit.smul_eq, add_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) 0
        ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM) =
      0
⊢ HSMul.hSMul (α := (↑cR.pt : Type w)) 0 m = 0

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) 0
      ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM) =
    0

Tactic:
simpa using smul_eq hcR hcM 0 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
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
N : ModuleCat (↑cR.pt : Type w)
α : ModuleColimit hcR hcM →+ (↑N : Type w)
X : Cᵒᵖ
x : (↑(M.obj X) : Type w)
⊢ Eq (α := (↑N : Type w))
    ((@ConcreteCategory.hom _ AddCommGrpCat.instCategory
            (fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) AddCommGrpCat.carrier _ _
            (M.presheaf.obj X) (AddCommGrpCat.of (↑N : Type w))
            (NatTrans.app
                ((homEquiv' hcR hcM :
                    (a : ModuleColimit hcR hcM →+ (↑N : Type w)) →
                      M.presheaf ⟶ (Functor.const Cᵒᵖ).obj (AddCommGrpCat.of (↑N : Type w)))
                  α)
                X :
              M.presheaf.obj X ⟶
                Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const Cᵒᵖ) (AddCommGrpCat.of (↑N : Type w))) X) :
          (a : (↑(M.obj X) : Type w)) → (↑N : Type w))
        x :
      (↑N : Type w))
    ((α : (a : ModuleColimit hcR hcM) → (↑N : Type w))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                AddCommGrpCat.carrier) (cM.ι.app X) :
              (a : (↑(M.obj X) : Type w)) → (↑cM.pt : Type w))
            x :
          (↑cM.pt : Type w)) :
      (↑N : Type w))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
Goal:
C : Type u
inst : Category.{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
N : ModuleCat (↑cR.pt : Type w)
β : M.presheaf ⟶ Functor.obj (Functor.const Cᵒᵖ) (AddCommGrpCat.of (↑N : Type w))
X : Cᵒᵖ
x : (↑(M.obj X) : Type w)
⊢ Eq (α := (↑N : Type w))
    ((((AddEquiv.symm (homEquiv' hcR hcM) :
                (a : M.presheaf ⟶ (Functor.const Cᵒᵖ).obj (AddCommGrpCat.of (↑N : Type w))) →
                  ModuleColimit hcR hcM →+ (↑N : Type w))
              β :
            ModuleColimit hcR hcM →+ (↑N : Type w)) :
          (a : ModuleColimit hcR hcM) → (↑N : Type w))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                AddCommGrpCat.carrier) (cM.ι.app X) :
              (a : (↑(M.presheaf.obj X) : Type w)) → (↑(((Functor.const Cᵒᵖ).obj cM.pt).obj X) : Type w))
            x :
          (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const Cᵒᵖ) cM.pt) X) : Type w)) :
      (↑N : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
            AddCommGrpCat.carrier) (β.app X) :
          (a : (↑(M.presheaf.obj X) : Type w)) →
            (↑(((Functor.const Cᵒᵖ).obj (AddCommGrpCat.of (↑N : Type w))).obj X) : Type w))
        x :
      (↑(Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const Cᵒᵖ) (AddCommGrpCat.of (↑N : Type w))) X) : Type w))

Tactic:
ConcreteCategory.congr_hom (hcM.ι_app_homEquiv_symm β X) x

Premises used: CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Limits.IsColimit.ι_app_homEquiv_symm
-- 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
N : ModuleCat (↑cR.pt : Type w)
α : ModuleColimit hcR hcM →+ (↑N : Type w)
⊢ (∀ (U : Cᵒᵖ) (r : (↑(R.obj U) : Type w)) (m : (↑(M.obj U) : Type w)),
      (@ConcreteCategory.hom _ AddCommGrpCat.instCategory
              (fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) AddCommGrpCat.carrier _ _
              (M.presheaf.obj U) (AddCommGrpCat.of (↑N : Type w))
              (NatTrans.app
                  ((homEquiv' hcR hcM :
                      (a : ModuleColimit hcR hcM →+ (↑N : Type w)) →
                        M.presheaf ⟶ (Functor.const Cᵒᵖ).obj (AddCommGrpCat.of (↑N : Type w)))
                    α)
                  U :
                M.presheaf.obj U ⟶
                  Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const Cᵒᵖ) (AddCommGrpCat.of (↑N : Type w))) U) :
            (a : (↑(M.obj U) : Type w)) → (↑N : Type w))
          (r • m) =
        HSMul.hSMul (α := (↑cR.pt : Type w)) (β := (↑N : Type w))
          ((ConcreteCategory.hom (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
                  RingCat.carrier) (cR.ι.app U) :
                (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w))
              r :
            (↑cR.pt : Type w))
          ((@ConcreteCategory.hom _ AddCommGrpCat.instCategory
                  (fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) AddCommGrpCat.carrier _ _
                  (M.presheaf.obj U) (AddCommGrpCat.of (↑N : Type w))
                  (NatTrans.app
                      ((homEquiv' hcR hcM :
                          (a : ModuleColimit hcR hcM →+ (↑N : Type w)) →
                            M.presheaf ⟶ (Functor.const Cᵒᵖ).obj (AddCommGrpCat.of (↑N : Type w)))
                        α)
                      U :
                    M.presheaf.obj U ⟶
                      Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const Cᵒᵖ) (AddCommGrpCat.of (↑N : Type w)))
                        U) :
                (a : (↑(M.obj U) : Type w)) → (↑N : Type w))
              m :
            (↑N : Type w))) ↔
    ∀ (r : (↑cR.pt : Type w)) (m : ModuleColimit hcR hcM),
      (α : (a : ModuleColimit hcR hcM) → (↑N : Type w)) (r • m) =
        HSMul.hSMul (β := (↑N : Type w)) r ((α : (a : ModuleColimit hcR hcM) → (↑N : Type w)) m : (↑N : Type w))

Tactic:
⟨fun h r m ↦ ?_, fun h U r m ↦ ?_⟩

Premises used: Iff.intro
-- 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
N : ModuleCat (↑cR.pt : Type w)
α : ModuleColimit hcR hcM →+ (↑N : Type w)
h :
  ∀ (r : (↑cR.pt : Type w)) (m : ModuleColimit hcR hcM),
    (α : (a : ModuleColimit hcR hcM) → (↑N : Type w)) (r • m) =
      HSMul.hSMul (β := (↑N : Type w)) r ((α : (a : ModuleColimit hcR hcM) → (↑N : Type w)) m : (↑N : Type w))
U : Cᵒᵖ
r : (↑(R.obj U) : Type w)
m : (↑(M.obj U) : Type w)
refine_2 :
  (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
          AddCommGrpCat.carrier) (cM.ι.app U) :
        (a : (↑(M.obj U) : Type w)) → (↑cM.pt : Type w))
      (r • m) =
    HSMul.hSMul (α := (↑cR.pt : Type w)) (β := ModuleColimit hcR hcM)
      ((ConcreteCategory.hom (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC := RingCat.carrier)
              (cR.ι.app U) :
            (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w))
          r :
        (↑cR.pt : Type w))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              AddCommGrpCat.carrier) (cM.ι.app U) :
            (a : (↑(M.obj U) : Type w)) → (↑cM.pt : Type w))
          m :
        (↑cM.pt : Type w))
⊢ Eq (α := (↑N : Type w))
    ((α : (a : ModuleColimit hcR hcM) → (↑N : Type w))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                AddCommGrpCat.carrier) (cM.ι.app U) :
              (a : (↑(M.obj U) : Type w)) → (↑cM.pt : Type w))
            (r • m) :
          (↑cM.pt : Type w)) :
      (↑N : Type w))
    ((α : (a : ModuleColimit hcR hcM) → (↑N : Type w))
        (HSMul.hSMul (α := (↑cR.pt : Type w)) (β := ModuleColimit hcR hcM)
          ((ConcreteCategory.hom (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
                  RingCat.carrier) (cR.ι.app U) :
                (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w))
              r :
            (↑cR.pt : Type w))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                  AddCommGrpCat.carrier) (cM.ι.app U) :
                (a : (↑(M.obj U) : Type w)) → (↑cM.pt : Type w))
              m :
            (↑cM.pt : Type w))) :
      (↑N : Type w))

Tactic:
congr 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 : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
N : ModuleCat (↑cR.pt : Type w)
α : ModuleColimit hcR hcM →+ (↑N : Type w)
h :
  ∀ (r : (↑cR.pt : Type w)) (m : ModuleColimit hcR hcM),
    (α : (a : ModuleColimit hcR hcM) → (↑N : Type w)) (r • m) =
      HSMul.hSMul (β := (↑N : Type w)) r ((α : (a : ModuleColimit hcR hcM) → (↑N : Type w)) m : (↑N : Type w))
U : Cᵒᵖ
r : (↑(R.obj U) : Type w)
m : (↑(M.obj U) : Type w)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
          AddCommGrpCat.carrier) (cM.ι.app U) :
        (a : (↑(M.obj U) : Type w)) → (↑cM.pt : Type w))
      (r • m) =
    HSMul.hSMul (α := (↑cR.pt : Type w)) (β := ModuleColimit hcR hcM)
      ((ConcreteCategory.hom (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC := RingCat.carrier)
              (cR.ι.app U) :
            (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w))
          r :
        (↑cR.pt : Type w))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              AddCommGrpCat.carrier) (cM.ι.app U) :
            (a : (↑(M.obj U) : Type w)) → (↑cM.pt : Type w))
          m :
        (↑cM.pt : Type w))

Tactic:
(smul_eq ..).symm

Premises used: PresheafOfModules.ModuleColimit.smul_eq, Eq.symm
-- 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
N : ModuleCat (↑cR.pt : Type w)
α : ModuleColimit hcR hcM →+ (↑N : Type w)
h :
  ∀ (r : (↑cR.pt : Type w)) (m : ModuleColimit hcR hcM),
    (α : (a : ModuleColimit hcR hcM) → (↑N : Type w)) (r • m) =
      HSMul.hSMul (β := (↑N : Type w)) r ((α : (a : ModuleColimit hcR hcM) → (↑N : Type w)) m : (↑N : Type w))
U : Cᵒᵖ
r : (↑(R.obj U) : Type w)
m : (↑(M.obj U) : Type w)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
          AddCommGrpCat.carrier) (cM.ι.app U) :
        (a : (↑(M.obj U) : Type w)) → (↑cM.pt : Type w))
      (r • m) =
    HSMul.hSMul (α := (↑cR.pt : Type w)) (β := ModuleColimit hcR hcM)
      ((ConcreteCategory.hom (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC := RingCat.carrier)
              (cR.ι.app U) :
            (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w))
          r :
        (↑cR.pt : Type w))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              AddCommGrpCat.carrier) (cM.ι.app U) :
            (a : (↑(M.obj U) : Type w)) → (↑cM.pt : Type w))
          m :
        (↑cM.pt : Type w))

Tactic:
exact (smul_eq ..).symm

Premises used: PresheafOfModules.ModuleColimit.smul_eq, Eq.symm
-- 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''
N : ModuleCat (↑cR.pt : Type w)
ψ : M ⟶ (constFunctor cR).obj N
⊢ ∀ (x y : ModuleColimit hcR hcM),
    (((AddEquiv.symm (homEquiv' hcR hcM) :
                (a : M.presheaf ⟶ (Functor.const Cᵒᵖ).obj (AddCommGrpCat.of N.1)) → ModuleColimit hcR hcM →+ N.1)
              ((toPresheaf R).map ψ) :
            ModuleColimit hcR hcM →+ N.1) :
          (a : ModuleColimit hcR hcM) → N.1)
        (x + y) =
      HAdd.hAdd (α := (↑N : Type w)) (β := (↑N : Type w))
        ((((AddEquiv.symm (homEquiv' hcR hcM) :
                    (a : M.presheaf ⟶ (Functor.const Cᵒᵖ).obj (AddCommGrpCat.of N.1)) → ModuleColimit hcR hcM →+ N.1)
                  ((toPresheaf R).map ψ) :
                ModuleColimit hcR hcM →+ N.1) :
              (a : ModuleColimit hcR hcM) → N.1)
            x :
          N.1)
        ((((AddEquiv.symm (homEquiv' hcR hcM) :
                    (a : M.presheaf ⟶ (Functor.const Cᵒᵖ).obj (AddCommGrpCat.of N.1)) → ModuleColimit hcR hcM →+ N.1)
                  ((toPresheaf R).map ψ) :
                ModuleColimit hcR hcM →+ N.1) :
              (a : ModuleColimit hcR hcM) → N.1)
            y :
          N.1)

Tactic:
simp