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'_1 : PresheafOfModules R
cM'_1 : Cocone M'_1.presheaf
hcM'_1 : IsColimit cM'_1
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
f : M ⟶ M'
U : Cᵒᵖ
r : (↑(R.obj U) : Type w)
m : (↑(M.obj U) : Type w)
c : Cocone ((toPresheaf R).obj M) := (Cocone.precompose ((toPresheaf R).map f)).obj cM'
⊢ Eq (α := (↑c.pt : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
            AddCommGrpCat.carrier) (cM.ι.app U ≫ hcM.desc c) :
          (a : (↑(M.presheaf.obj U) : Type w)) → (↑c.pt : Type w))
        (r • m) :
      (↑c.pt : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
            AddCommGrpCat.carrier) (c.ι.app U) :
          (a : (↑(M.presheaf.obj U) : Type w)) → (↑c.pt : Type w))
        (r • m) :
      (↑c.pt : Type w))

Tactic:
have h₁ := ConcreteCategory.congr_hom (hcM.fac c U) (r • m)
-- 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'_1 : PresheafOfModules R
cM'_1 : Cocone M'_1.presheaf
hcM'_1 : IsColimit cM'_1
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
f : M ⟶ M'
U : Cᵒᵖ
r : (↑(R.obj U) : Type w)
m : (↑(M.obj U) : Type w)
c : Cocone ((toPresheaf R).obj M) := (Cocone.precompose ((toPresheaf R).map f)).obj cM'
h₁ :
  Eq (α := (↑c.pt : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
            AddCommGrpCat.carrier) (cM.ι.app U ≫ hcM.desc c) :
          (a : (↑(M.presheaf.obj U) : Type w)) → (↑c.pt : Type w))
        (r • m) :
      (↑c.pt : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
            AddCommGrpCat.carrier) (c.ι.app U) :
          (a : (↑(M.presheaf.obj U) : Type w)) → (↑c.pt : Type w))
        (r • m) :
      (↑c.pt : Type w))
⊢ Eq (α := (↑c.pt : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
            AddCommGrpCat.carrier) (cM.ι.app U ≫ hcM.desc c) :
          (a : (↑(M.presheaf.obj U) : Type w)) → (↑c.pt : Type w))
        m :
      (↑c.pt : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
            AddCommGrpCat.carrier) (c.ι.app U) :
          (a : (↑(M.presheaf.obj U) : Type w)) → (↑c.pt : Type w))
        m :
      (↑c.pt : Type w))

Tactic:
have h₂ := ConcreteCategory.congr_hom (hcM.fac c U) m
-- 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'_1 : PresheafOfModules R
cM'_1 : Cocone M'_1.presheaf
hcM'_1 : IsColimit cM'_1
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
f : M ⟶ M'
U : Cᵒᵖ
r : (↑(R.obj U) : Type w)
m : (↑(M.obj U) : Type w)
c : Cocone ((toPresheaf R).obj M) := (Cocone.precompose ((toPresheaf R).map f)).obj cM'
h₁ :
  Eq (α := (↑cM'.pt : Type w))
    ((AddMonoidHom.comp (AddCommGrpCat.Hom.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM')))
            (AddCommGrpCat.Hom.hom (cM.ι.app U)) :
          (a : (↑(M.obj U) : Type w)) → (↑cM'.pt : Type w))
        (r • m) :
      (↑cM'.pt : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
            AddCommGrpCat.carrier) (((toPresheaf R).map f).app U ≫ cM'.ι.app U) :
          (a : (↑(M.obj U) : Type w)) → (↑cM'.pt : Type w))
        (r • m) :
      (↑cM'.pt : Type w))
h₂ :
  Eq (α := (↑cM'.pt : Type w))
    ((AddMonoidHom.comp (AddCommGrpCat.Hom.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM')))
            (AddCommGrpCat.Hom.hom (cM.ι.app U)) :
          (a : (↑(M.obj U) : Type w)) → (↑cM'.pt : Type w))
        m :
      (↑cM'.pt : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
            AddCommGrpCat.carrier) (((toPresheaf R).map f).app U ≫ cM'.ι.app U) :
          (a : (↑(M.obj U) : Type w)) → (↑cM'.pt : Type w))
        m :
      (↑cM'.pt : Type w))
⊢ Eq (α := ModuleColimit hcR hcM')
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
            AddCommGrpCat.carrier) (((toPresheaf R).map f).app U ≫ cM'.ι.app U) :
          (a : (↑(M.obj U) : Type w)) → (↑cM'.pt : Type w))
        (r • m) :
      (↑cM'.pt : Type w))
    ((ιM : (a : (↑(M'.obj U) : Type w)) → ModuleColimit hcR hcM')
        ((ModuleCat.Hom.hom (f.app U) : (a : (↑(M.obj U) : Type w)) → (↑(M'.obj U) : Type w)) (r • m) :
          (↑(M'.obj U) : Type w)) :
      ModuleColimit hcR hcM')

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'
f : M ⟶ M'
U : Cᵒᵖ
m : (↑(M.obj U) : Type w)
⊢ Eq (α := ModuleColimit hcR hcM')
    ((map hcR hcM hcM' f : (a : ModuleColimit hcR hcM) → ModuleColimit hcR hcM')
        ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM) :
      ModuleColimit hcR hcM')
    ((ιM : (a : (↑(M'.obj U) : Type w)) → ModuleColimit hcR hcM')
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj U) : Type w)) ↦
                LinearMap (R := (↑(R.obj U) : Type w)) (RingHom.id (↑(R.obj U) : Type w)) (↑x1 : Type w) (↑x2 : Type w))
                (CC := ModuleCat.carrier) (f.app U) :
              (a : (↑(M.obj U) : Type w)) → (↑(M'.obj U) : Type w))
            m :
          (↑(M'.obj U) : Type w)) :
      ModuleColimit hcR hcM')

Tactic:
ConcreteCategory.congr_hom (hcM.fac ((Cocone.precompose ((toPresheaf _).map f)).obj cM') U) m

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.Cocone.precompose, CategoryTheory.Functor.map, PresheafOfModules.toPresheaf, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Functor.obj, 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
h :
  ∀ (m : ModuleColimit hcR hcM),
    Eq (α := ModuleColimit hcR hcM)
      ((map hcR hcM hcM (𝟙 M) : (a : ModuleColimit hcR hcM) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM)
      ((LinearMap.id : (a : ModuleColimit hcR hcM) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM)
⊢ Eq (α :=
    LinearMap (R := (↑cR.pt : Type w)) (RingHom.id (↑cR.pt : Type w)) (ModuleColimit hcR hcM) (ModuleColimit hcR hcM))
    (map hcR hcM hcM (𝟙 M)) LinearMap.id

Tactic:
ext m
-- 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
h :
  ∀ (U : Cᵒᵖ) (m : (↑(M.obj U) : Type w)),
    Eq (α := ModuleColimit hcR hcM)
      ((map hcR hcM hcM (𝟙 M) : (a : ModuleColimit hcR hcM) → ModuleColimit hcR hcM)
          ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM) :
        ModuleColimit hcR hcM)
      ((LinearMap.id : (a : ModuleColimit hcR hcM) → ModuleColimit hcR hcM)
          ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM) :
        ModuleColimit hcR hcM)
⊢ Eq (α := ModuleColimit hcR hcM)
    ((map hcR hcM hcM (𝟙 M) : (a : ModuleColimit hcR hcM) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM)
    ((LinearMap.id : (a : ModuleColimit hcR hcM) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM)

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
U : Cᵒᵖ
m : (↑(M.obj U) : Type w)
⊢ Eq (α := ModuleColimit hcR hcM)
    ((map hcR hcM hcM (𝟙 M) : (a : ModuleColimit hcR hcM) → ModuleColimit hcR hcM)
        ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM) :
      ModuleColimit hcR hcM)
    ((LinearMap.id : (a : ModuleColimit hcR hcM) → ModuleColimit hcR hcM)
        ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM) :
      ModuleColimit hcR hcM)

Tactic:
simp
-- 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'
f : M ⟶ M'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
g : M' ⟶ M''
h :
  ∀ (m : ModuleColimit hcR hcM),
    Eq (α := ModuleColimit hcR hcM'')
      ((map hcR hcM' hcM'' g ∘ₗ map hcR hcM hcM' f : (a : ModuleColimit hcR hcM) → ModuleColimit hcR hcM'') m :
        ModuleColimit hcR hcM'')
      ((map hcR hcM hcM'' (f ≫ g) : (a : ModuleColimit hcR hcM) → ModuleColimit hcR hcM'') m : ModuleColimit hcR hcM'')
⊢ Eq (α :=
    LinearMap (R := (↑cR.pt : Type w)) (RingHom.id (↑cR.pt : Type w)) (ModuleColimit hcR hcM) (ModuleColimit hcR hcM''))
    (map hcR hcM' hcM'' g ∘ₗ map hcR hcM hcM' f) (map hcR hcM hcM'' (f ≫ g))

Tactic:
ext m
-- 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'
f : M ⟶ M'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
g : M' ⟶ M''
m : ModuleColimit hcR hcM
h :
  ∀ (U : Cᵒᵖ) (m : (↑(M.obj U) : Type w)),
    Eq (α := ModuleColimit hcR hcM'')
      ((map hcR hcM' hcM'' g ∘ₗ map hcR hcM hcM' f : (a : ModuleColimit hcR hcM) → ModuleColimit hcR hcM'')
          ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM) :
        ModuleColimit hcR hcM'')
      ((map hcR hcM hcM'' (f ≫ g) : (a : ModuleColimit hcR hcM) → ModuleColimit hcR hcM'')
          ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM) :
        ModuleColimit hcR hcM'')
⊢ Eq (α := ModuleColimit hcR hcM'')
    ((map hcR hcM' hcM'' g ∘ₗ map hcR hcM hcM' f : (a : ModuleColimit hcR hcM) → ModuleColimit hcR hcM'') m :
      ModuleColimit hcR hcM'')
    ((map hcR hcM hcM'' (f ≫ g) : (a : ModuleColimit hcR hcM) → ModuleColimit hcR hcM'') m : ModuleColimit hcR hcM'')

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'
f : M ⟶ M'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
g : M' ⟶ M''
U : Cᵒᵖ
m : (↑(M.obj U) : Type w)
⊢ Eq (α := ModuleColimit hcR hcM'')
    ((map hcR hcM' hcM'' g ∘ₗ map hcR hcM hcM' f : (a : ModuleColimit hcR hcM) → ModuleColimit hcR hcM'')
        ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM) :
      ModuleColimit hcR hcM'')
    ((map hcR hcM hcM'' (f ≫ g) : (a : ModuleColimit hcR hcM) → ModuleColimit hcR hcM'')
        ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM) :
      ModuleColimit hcR hcM'')

Tactic:
simp
-- 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'
N : ModuleCat (↑cR.pt : Type w)
φ' : ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM') ⟶ N
f : M ⟶ M'
U : Cᵒᵖ
m : (↑(M.obj U) : Type w)
h :
  Eq (α := (↑(((constFunctor cR).obj N).obj U) : Type w))
    ((ModuleCat.Hom.hom φ' : (a : ModuleColimit hcR hcM') → (↑N : Type w))
        ((map hcR hcM hcM' f : (a : ModuleColimit hcR hcM) → ModuleColimit hcR hcM')
            ((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)) :
          ModuleColimit hcR hcM') :
      (↑N : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑cR.pt : Type w)) ↦
            LinearMap (R := (↑cR.pt : Type w)) (RingHom.id (↑cR.pt : Type w)) (↑x1 : Type w) (↑x2 : Type w)) (CC :=
            ModuleCat.carrier) φ' :
          (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))
            ((ModuleCat.Hom.hom (f.app U) : (a : (↑(M.obj U) : Type w)) → (↑(M'.obj U) : Type w)) m :
              (↑(M'.obj U) : Type w)) :
          (↑cM'.pt : Type w)) :
      (↑N : Type w))
⊢ Eq (α := (↑(((constFunctor cR).obj N).obj U) : Type w))
    ((ModuleCat.Hom.hom
            (Hom.app
              ((homEquiv hcR hcM :
                  (a : ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM) ⟶ N) → M ⟶ (constFunctor cR).obj N)
                (ModuleCat.ofHom (map hcR hcM hcM' f) ≫ φ'))
              U) :
          (a : (↑(M.obj U) : Type w)) → (↑(((constFunctor cR).obj N).obj U) : Type w))
        m :
      (↑(((constFunctor cR).obj N).obj U) : Type w))
    ((ModuleCat.Hom.hom
            (Hom.app
              (f ≫
                (homEquiv hcR hcM' :
                    (a : ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM') ⟶ N) → M' ⟶ (constFunctor cR).obj N)
                  φ')
              U) :
          (a : (↑(M.obj U) : Type w)) → (↑(((constFunctor cR).obj N).obj U) : Type w))
        m :
      (↑(((constFunctor cR).obj N).obj U) : Type w))

Tactic:
simp only [homEquiv_app_apply, ModuleCat.hom_comp, ModuleCat.hom_ofHom, LinearMap.coe_comp,
    Function.comp_apply, comp_app]

Premises used: PresheafOfModules.comp_app, PresheafOfModules.ModuleColimit.homEquiv_app_apply, LinearMap.coe_comp, Function.comp_apply, ModuleCat.hom_ofHom, ModuleCat.hom_comp
-- 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'
N : ModuleCat (↑cR.pt : Type w)
φ' : ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM') ⟶ N
f : M ⟶ M'
U : Cᵒᵖ
m : (↑(M.obj U) : Type w)
h :
  Eq (α := ModuleColimit hcR hcM')
    ((map hcR hcM hcM' f : (a : ModuleColimit hcR hcM) → ModuleColimit hcR hcM')
        ((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)) :
      ModuleColimit hcR hcM')
    ((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))
        ((ModuleCat.Hom.hom (f.app U) : (a : (↑(M.obj U) : Type w)) → (↑(M'.obj U) : Type w)) m :
          (↑(M'.obj U) : Type w)) :
      (↑cM'.pt : Type w))
⊢ Eq (α := (↑(((constFunctor cR).obj N).obj U) : Type w))
    ((ModuleCat.Hom.hom φ' : (a : ModuleColimit hcR hcM') → (↑N : Type w))
        ((map hcR hcM hcM' f : (a : ModuleColimit hcR hcM) → ModuleColimit hcR hcM')
            ((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)) :
          ModuleColimit hcR hcM') :
      (↑N : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑cR.pt : Type w)) ↦
            LinearMap (R := (↑cR.pt : Type w)) (RingHom.id (↑cR.pt : Type w)) (↑x1 : Type w) (↑x2 : Type w)) (CC :=
            ModuleCat.carrier) φ' :
          (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))
            ((ModuleCat.Hom.hom (f.app U) : (a : (↑(M.obj U) : Type w)) → (↑(M'.obj U) : Type w)) m :
              (↑(M'.obj U) : Type w)) :
          (↑cM'.pt : Type w)) :
      (↑N : Type w))

Tactic:
apply congr_arg

Premises used: congr_arg
-- 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'
N : ModuleCat (↑cR.pt : Type w)
φ' : ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM') ⟶ N
f : M ⟶ M'
U : Cᵒᵖ
m : (↑(M.obj U) : Type w)
⊢ Eq (α := ModuleColimit hcR hcM')
    ((map hcR hcM hcM' f : (a : ModuleColimit hcR hcM) → ModuleColimit hcR hcM')
        ((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)) :
      ModuleColimit hcR hcM')
    ((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))
        ((ModuleCat.Hom.hom (f.app U) : (a : (↑(M.obj U) : Type w)) → (↑(M'.obj U) : Type w)) m :
          (↑(M'.obj U) : Type w)) :
      (↑cM'.pt : Type w))

Tactic:
map_apply hcR hcM hcM' f m

Premises used: PresheafOfModules.ModuleColimit.map_apply
-- 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'
N : ModuleCat (↑cR.pt : Type w)
φ' : ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM') ⟶ N
f : M ⟶ M'
U : Cᵒᵖ
m : (↑(M.obj U) : Type w)
⊢ Eq (α := ModuleColimit hcR hcM')
    ((map hcR hcM hcM' f : (a : ModuleColimit hcR hcM) → ModuleColimit hcR hcM')
        ((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)) :
      ModuleColimit hcR hcM')
    ((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))
        ((ModuleCat.Hom.hom (f.app U) : (a : (↑(M.obj U) : Type w)) → (↑(M'.obj U) : Type w)) m :
          (↑(M'.obj U) : Type w)) :
      (↑cM'.pt : Type w))

Tactic:
exact map_apply hcR hcM hcM' f m

Premises used: PresheafOfModules.ModuleColimit.map_apply