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'
N : ModuleCat (↑cR.pt : Type w)
f : M ⟶ M'
g : M' ⟶ (constFunctor cR).obj N
obtain :
  ∀ (g : ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM') ⟶ N),
    Eq (α := M ⟶ (constFunctor cR).obj N)
      ((homEquiv hcR hcM :
            (a : ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM) ⟶ N) → M ⟶ (constFunctor cR).obj N)
          ((AddEquiv.symm (homEquiv hcR hcM) :
              (a : M ⟶ (constFunctor cR).obj N) → ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM) ⟶ N)
            (f ≫
              (homEquiv hcR hcM' :
                  (a : ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM') ⟶ N) → M' ⟶ (constFunctor cR).obj N)
                g)) :
        M ⟶ (constFunctor cR).obj N)
      ((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) ≫
            (AddEquiv.symm (homEquiv hcR hcM') :
                (a : M' ⟶ (constFunctor cR).obj N) → ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM') ⟶ N)
              ((homEquiv hcR hcM' :
                  (a : ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM') ⟶ N) → M' ⟶ (constFunctor cR).obj N)
                g)) :
        M ⟶ (constFunctor cR).obj N)
⊢ Eq (α := M ⟶ (constFunctor cR).obj N)
    ((homEquiv hcR hcM : (a : ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM) ⟶ N) → M ⟶ (constFunctor cR).obj N)
        ((AddEquiv.symm (homEquiv hcR hcM) :
            (a : M ⟶ (constFunctor cR).obj N) → ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM) ⟶ N)
          (f ≫ g)) :
      M ⟶ (constFunctor cR).obj N)
    ((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) ≫
          (AddEquiv.symm (homEquiv hcR hcM') :
              (a : M' ⟶ (constFunctor cR).obj N) → ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM') ⟶ N)
            g) :
      M ⟶ (constFunctor cR).obj N)

Tactic:
obtain ⟨g, rfl⟩ := (homEquiv hcR hcM').surjective g

Premises used: PresheafOfModules.ModuleColimit.homEquiv, AddEquiv.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'
N : ModuleCat (↑cR.pt : Type w)
f : M ⟶ M'
g : ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM') ⟶ N
⊢ Eq (α := M ⟶ (constFunctor cR).obj N)
    ((homEquiv hcR hcM : (a : ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM) ⟶ N) → M ⟶ (constFunctor cR).obj N)
        ((AddEquiv.symm (homEquiv hcR hcM) :
            (a : M ⟶ (constFunctor cR).obj N) → ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM) ⟶ N)
          (f ≫
            (homEquiv hcR hcM' :
                (a : ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM') ⟶ N) → M' ⟶ (constFunctor cR).obj N)
              g)) :
      M ⟶ (constFunctor cR).obj N)
    ((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) ≫
          (AddEquiv.symm (homEquiv hcR hcM') :
              (a : M' ⟶ (constFunctor cR).obj N) → ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM') ⟶ N)
            ((homEquiv hcR hcM' :
                (a : ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM') ⟶ N) → M' ⟶ (constFunctor cR).obj N)
              g)) :
      M ⟶ (constFunctor cR).obj N)

Tactic:
simp [homEquiv_naturality_left]

Premises used: PresheafOfModules.ModuleColimit.homEquiv_naturality_left
-- 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
X Y Z : PresheafOfModules R
f : X ⟶ Y
g : Y ⟶ Z
hf :
  Eq (α :=
    LinearMap (R := (↑cR.pt : Type w)) (RingHom.id (↑cR.pt : Type w))
      (↑(ModuleCat.of (↑cR.pt : Type w)
            (ModuleColimit (cM := colimit.cocone X.presheaf) hcR (colimit.isColimit X.presheaf))) :
        Type w)
      (↑(ModuleCat.of (↑cR.pt : Type w)
            (ModuleColimit (cM := colimit.cocone Z.presheaf) hcR (colimit.isColimit Z.presheaf))) :
        Type w))
    (ModuleCat.Hom.hom
      (ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit X.presheaf) (colimit.isColimit Z.presheaf) (f ≫ g))))
    (ModuleCat.Hom.hom
      (CategoryStruct.comp (Y :=
        ModuleCat.of (↑cR.pt : Type w)
          (ModuleColimit (cM := colimit.cocone Y.presheaf) hcR (colimit.isColimit Y.presheaf)))
        (ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit X.presheaf) (colimit.isColimit Y.presheaf) f))
        (ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit Y.presheaf) (colimit.isColimit Z.presheaf) g))))
⊢ Eq (α :=
    Quiver.Hom (V := ModuleCat (↑cR.pt : Type w))
      (ModuleCat.of (↑cR.pt : Type w)
        (ModuleColimit (cM := colimit.cocone X.presheaf) hcR (colimit.isColimit X.presheaf)))
      (ModuleCat.of (↑cR.pt : Type w)
        (ModuleColimit (cM := colimit.cocone Z.presheaf) hcR (colimit.isColimit Z.presheaf))))
    (ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit X.presheaf) (colimit.isColimit Z.presheaf) (f ≫ g)))
    (CategoryStruct.comp (Y :=
      ModuleCat.of (↑cR.pt : Type w)
        (ModuleColimit (cM := colimit.cocone Y.presheaf) hcR (colimit.isColimit Y.presheaf)))
      (ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit X.presheaf) (colimit.isColimit Y.presheaf) f))
      (ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit Y.presheaf) (colimit.isColimit Z.presheaf) g)))

Tactic:
ext : 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
X Y Z : PresheafOfModules R
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    LinearMap (R := (↑cR.pt : Type w)) (RingHom.id (↑cR.pt : Type w))
      (↑(ModuleCat.of (↑cR.pt : Type w)
            (ModuleColimit (cM := colimit.cocone X.presheaf) hcR (colimit.isColimit X.presheaf))) :
        Type w)
      (↑(ModuleCat.of (↑cR.pt : Type w)
            (ModuleColimit (cM := colimit.cocone Z.presheaf) hcR (colimit.isColimit Z.presheaf))) :
        Type w))
    (ModuleCat.Hom.hom
      (ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit X.presheaf) (colimit.isColimit Z.presheaf) (f ≫ g))))
    (ModuleCat.Hom.hom
      (CategoryStruct.comp (Y :=
        ModuleCat.of (↑cR.pt : Type w)
          (ModuleColimit (cM := colimit.cocone Y.presheaf) hcR (colimit.isColimit Y.presheaf)))
        (ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit X.presheaf) (colimit.isColimit Y.presheaf) f))
        (ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit Y.presheaf) (colimit.isColimit Z.presheaf) g))))

Tactic:
(ModuleColimit.comp_map ..).symm

Premises used: PresheafOfModules.ModuleColimit.map, PresheafOfModules.ModuleColimit.comp_map, Eq.symm, 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
X Y Z : PresheafOfModules R
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    LinearMap (R := (↑cR.pt : Type w)) (RingHom.id (↑cR.pt : Type w))
      (↑(ModuleCat.of (↑cR.pt : Type w)
            (ModuleColimit (cM := colimit.cocone X.presheaf) hcR (colimit.isColimit X.presheaf))) :
        Type w)
      (↑(ModuleCat.of (↑cR.pt : Type w)
            (ModuleColimit (cM := colimit.cocone Z.presheaf) hcR (colimit.isColimit Z.presheaf))) :
        Type w))
    (ModuleCat.Hom.hom
      (ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit X.presheaf) (colimit.isColimit Z.presheaf) (f ≫ g))))
    (ModuleCat.Hom.hom
      (CategoryStruct.comp (Y :=
        ModuleCat.of (↑cR.pt : Type w)
          (ModuleColimit (cM := colimit.cocone Y.presheaf) hcR (colimit.isColimit Y.presheaf)))
        (ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit X.presheaf) (colimit.isColimit Y.presheaf) f))
        (ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit Y.presheaf) (colimit.isColimit Z.presheaf) g))))

Tactic:
exact (ModuleColimit.comp_map ..).symm

Premises used: PresheafOfModules.ModuleColimit.comp_map, 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
F : PresheafOfModules R
G : ModuleCat (↑cR.pt : Type w)
⊢ Adjunction.homEquiv (colimitAdjunction hcR) F G =
    (↑(ModuleColimit.homEquiv hcR (colimit.isColimit F.presheaf)) :
      (ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR (colimit.isColimit F.presheaf)) ⟶ G) ≃
        (F ⟶ (constFunctor cR).obj G))

Tactic:
simp [colimitAdjunction]

Premises used: PresheafOfModules.colimitAdjunction
-- 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
F : PresheafOfModules R
G : ModuleCat (↑cR.pt : Type w)
β : F ⟶ (constFunctor cR).obj G
X : Cᵒᵖ
m : (↑(F.obj X) : Type w)
⊢ Eq (α := (↑G : Type w))
    ((@ConcreteCategory.hom.{w, w, w + 1, w} _ (ModuleCat.moduleCategory (↑cR.pt : Type w))
            (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))
            ModuleCat.carrier
            (fun (X Y : ModuleCat (↑cR.pt : Type w)) ↦
              (LinearMap.instFunLike :
                FunLike (LinearMap (R := (↑cR.pt : Type w)) (RingHom.id (↑cR.pt : Type w)) (↑X : Type w) (↑Y : Type w))
                  (↑X : Type w) (↑Y : Type w)))
            _ ((colimitFunctor hcR).obj F) _
            (((↑(homEquiv hcR (colimit.isColimit F.presheaf)) :
                      (ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR (colimit.isColimit F.presheaf)) ⟶ G) ≃
                        (F ⟶ (constFunctor cR).obj G)).symm :
                  (a : F ⟶ (constFunctor cR).obj G) → (colimitFunctor hcR).obj F ⟶ G)
                β :
              (colimitFunctor hcR).obj F ⟶ G) :
          (a : (↑((colimitFunctor hcR).obj F) : Type w)) → (↑G : Type w))
        ((ιM : (a : (↑(F.obj X) : Type w)) → ModuleColimit hcR (colimit.isColimit F.presheaf)) m :
          ModuleColimit (cM := colimit.cocone F.presheaf) hcR (colimit.isColimit F.presheaf)) :
      (↑G : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj X) : Type w)) ↦
            LinearMap (R := (↑(R.obj X) : Type w)) (RingHom.id (↑(R.obj X) : Type w)) (↑x1 : Type w) (↑x2 : Type w))
            (CC := ModuleCat.carrier) (β.app X) :
          (a : (↑(F.obj X) : Type w)) → (↑(((constFunctor cR).obj G).obj X) : Type w))
        m :
      (↑(((constFunctor cR).obj G).obj X) : Type w))

Tactic:
apply homEquiv_symm_apply

Premises used: PresheafOfModules.ModuleColimit.homEquiv_symm_apply
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
X Y : Cᵒᵖ
f : X ⟶ Y
j : J
rw :
  ((evaluation R X).mapCocone c).ι.app j ≫
      c.pt.map f ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((hc Y).desc ((evaluation R Y).mapCocone s)) =
    ((evaluation R X).mapCocone s).ι.app j ≫ s.pt.map f
⊢ Eq (α := (F ⋙ evaluation R X).obj j ⟶ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (s.pt.obj Y))
    (((evaluation R X).mapCocone c).ι.app j ≫
        c.pt.map f ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((hc Y).desc ((evaluation R Y).mapCocone s)) :
      (F ⋙ evaluation R X).obj j ⟶ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (s.pt.obj Y))
    (((evaluation R X).mapCocone c).ι.app j ≫ (hc X).desc ((evaluation R X).mapCocone s) ≫ s.pt.map f :
      (F ⋙ evaluation R X).obj j ⟶ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (s.pt.obj Y))

Tactic:
rw [(hc X).fac_assoc ((evaluation R X).mapCocone s) j]

Premises used: PresheafOfModules.evaluation, CategoryTheory.Functor.mapCocone, CategoryTheory.Limits.IsColimit.fac_assoc
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
X Y : Cᵒᵖ
f : X ⟶ Y
j : J
⊢ (F.obj j).map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((c.ι.app j).app Y) =
    (c.ι.app j).app X ≫ (Functor.obj (Functor.obj (Functor.const J) c.pt) j).map f

Tactic:
have h₁ := (c.ι.app j).naturality f
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
X Y : Cᵒᵖ
f : X ⟶ Y
j : J
h₁ :
  (F.obj j).map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((c.ι.app j).app Y) =
    (c.ι.app j).app X ≫ (Functor.obj (Functor.obj (Functor.const J) c.pt) j).map f
⊢ ∀ (j : J),
    ((evaluation R Y).mapCocone c).ι.app j ≫ (hc Y).desc ((evaluation R Y).mapCocone s) =
      ((evaluation R Y).mapCocone s).ι.app j

Tactic:
have h₂ := (hc Y).fac ((evaluation R Y).mapCocone s)
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
X Y : Cᵒᵖ
f : X ⟶ Y
j : J
h₁ :
  (F.obj j).map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((c.ι.app j).app Y) =
    (c.ι.app j).app X ≫ (Functor.obj (Functor.obj (Functor.const J) c.pt) j).map f
h₂ :
  ∀ (j : J),
    ((evaluation R Y).mapCocone c).ι.app j ≫ (hc Y).desc ((evaluation R Y).mapCocone s) =
      ((evaluation R Y).mapCocone s).ι.app j
dsimp :
  (c.ι.app j).app X ≫
      c.pt.map f ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((hc Y).desc ((evaluation R Y).mapCocone s)) =
    (s.ι.app j).app X ≫ s.pt.map f
⊢ ((evaluation R X).mapCocone c).ι.app j ≫
      c.pt.map f ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((hc Y).desc ((evaluation R Y).mapCocone s)) =
    ((evaluation R X).mapCocone s).ι.app j ≫ s.pt.map f

Tactic:
dsimp at h₁ h₂ ⊢
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
X Y : Cᵒᵖ
f : X ⟶ Y
j : J
h₁ :
  (F.obj j).map f ≫ (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((c.ι.app j).app Y) =
    (c.ι.app j).app X ≫ c.pt.map f
h₂ : ∀ (j : J), (c.ι.app j).app Y ≫ (hc Y).desc ((evaluation R Y).mapCocone s) = (s.ι.app j).app Y
⊢ (c.ι.app j).app X ≫
      c.pt.map f ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((hc Y).desc ((evaluation R Y).mapCocone s)) =
    (s.ι.app j).app X ≫ s.pt.map f

Tactic:
simp only [← reassoc_of% h₁, ← Functor.map_comp, h₂, Hom.naturality]

Premises used: CategoryTheory.Functor.map_comp, PresheafOfModules.Hom.naturality
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
j : J
h :
  ∀ (X : Cᵒᵖ),
    Hom.app (c.ι.app j ≫ { app := fun (X : Cᵒᵖ) ↦ (hc X).desc ((evaluation R X).mapCocone s), naturality := ⋯ }) X =
      (s.ι.app j).app X
⊢ c.ι.app j ≫ { app := fun (X : Cᵒᵖ) ↦ (hc X).desc ((evaluation R X).mapCocone s), naturality := ⋯ } = s.ι.app j

Tactic:
ext1 X
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
j : J
X : Cᵒᵖ
⊢ Hom.app (c.ι.app j ≫ { app := fun (X : Cᵒᵖ) ↦ (hc X).desc ((evaluation R X).mapCocone s), naturality := ⋯ }) X =
    (s.ι.app j).app X

Tactic:
(hc X).fac ((evaluation R X).mapCocone s) j

Premises used: PresheafOfModules.evaluation, CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Functor.mapCocone
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
j : J
X : Cᵒᵖ
⊢ Hom.app (c.ι.app j ≫ { app := fun (X : Cᵒᵖ) ↦ (hc X).desc ((evaluation R X).mapCocone s), naturality := ⋯ }) X =
    (s.ι.app j).app X

Tactic:
exact (hc X).fac ((evaluation R X).mapCocone s) j

Premises used: PresheafOfModules.evaluation, CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Functor.mapCocone
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
h :
  ∀ (X : Cᵒᵖ),
    m.app X = Hom.app { app := fun (X : Cᵒᵖ) ↦ (hc X).desc ((evaluation R X).mapCocone s), naturality := ⋯ } X
⊢ m = { app := fun (X : Cᵒᵖ) ↦ (hc X).desc ((evaluation R X).mapCocone s), naturality := ⋯ }

Tactic:
ext1 X
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
X : Cᵒᵖ
h : ∀ (j : J), ((evaluation R X).mapCocone c).ι.app j ≫ m.app X = ((evaluation R X).mapCocone s).ι.app j
⊢ m.app X = Hom.app { app := fun (X : Cᵒᵖ) ↦ (hc X).desc ((evaluation R X).mapCocone s), naturality := ⋯ } X

Tactic:
apply (hc X).uniq ((evaluation R X).mapCocone s)

Premises used: PresheafOfModules.evaluation, CategoryTheory.Functor.mapCocone, CategoryTheory.Limits.IsColimit.uniq
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
X : Cᵒᵖ
j : J
h : (c.ι.app j).app X ≫ m.app X = (s.ι.app j).app X
⊢ ((evaluation R X).mapCocone c).ι.app j ≫ m.app X = ((evaluation R X).mapCocone s).ι.app j

Tactic:
dsimp
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
X : Cᵒᵖ
j : J
h : (c.ι.app j).app X ≫ m.app X = (c.ι.app j ≫ m).app X
⊢ (c.ι.app j).app X ≫ m.app X = (s.ι.app j).app X

Tactic:
rw [← hm]
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
X : Cᵒᵖ
j : J
⊢ (c.ι.app j).app X ≫ m.app X = (c.ι.app j ≫ m).app X

Tactic:
rfl