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''
N : ModuleCat (↑cR.pt : Type w)
ψ : M ⟶ (constFunctor cR).obj N
obtain :
  ∀ (φ : ModuleColimit hcR hcM →+ N.1)
    (hφ :
      (homEquiv' hcR hcM :
            (a : ModuleColimit hcR hcM →+ N.1) → M.presheaf ⟶ (Functor.const Cᵒᵖ).obj (AddCommGrpCat.of N.1))
          φ =
        (toPresheaf R).map ψ)
    (m : (↑cR.pt : Type w)) (x : 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)
        (m • x) =
      HSMul.hSMul (α := (↑cR.pt : Type w)) (β := (↑N : Type w))
        ((RingHom.id (↑cR.pt : Type w) : (a : (↑cR.pt : Type w)) → (↑cR.pt : Type w)) m : (↑cR.pt : 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)
⊢ ∀ (m : (↑cR.pt : Type w)) (x : 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)
        (m • x) =
      HSMul.hSMul (α := (↑cR.pt : Type w)) (β := (↑N : Type w))
        ((RingHom.id (↑cR.pt : Type w) : (a : (↑cR.pt : Type w)) → (↑cR.pt : Type w)) m : (↑cR.pt : 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)

Tactic:
obtain ⟨φ, hφ⟩ := (homEquiv' hcR hcM).surjective ((toPresheaf _).map ψ)

Premises used: PresheafOfModules.ModuleColimit.homEquiv', CategoryTheory.Functor.map, AddEquiv.surjective, PresheafOfModules.toPresheaf
-- 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
φ : ModuleColimit hcR hcM →+ N.1
hφ :
  (homEquiv' hcR hcM : (a : ModuleColimit hcR hcM →+ N.1) → M.presheaf ⟶ (Functor.const Cᵒᵖ).obj (AddCommGrpCat.of N.1))
      φ =
    (toPresheaf R).map ψ
simp :
  ∀ (m : (↑cR.pt : Type w)) (x : ModuleColimit hcR hcM),
    (φ : (a : ModuleColimit hcR hcM) → N.1) (m • x) =
      HSMul.hSMul (β := (↑N : Type w)) m ((φ : (a : ModuleColimit hcR hcM) → N.1) x : N.1)
⊢ ∀ (m : (↑cR.pt : Type w)) (x : 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)
        (m • x) =
      HSMul.hSMul (α := (↑cR.pt : Type w)) (β := (↑N : Type w))
        ((RingHom.id (↑cR.pt : Type w) : (a : (↑cR.pt : Type w)) → (↑cR.pt : Type w)) m : (↑cR.pt : 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)

Tactic:
simp only [← hφ, AddEquiv.symm_apply_apply, RingHom.id_apply]

Premises used: RingHom.id_apply, AddEquiv.symm_apply_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'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
N : ModuleCat (↑cR.pt : Type w)
ψ : M ⟶ (constFunctor cR).obj N
φ : ModuleColimit hcR hcM →+ N.1
hφ :
  (homEquiv' hcR hcM : (a : ModuleColimit hcR hcM →+ N.1) → M.presheaf ⟶ (Functor.const Cᵒᵖ).obj (AddCommGrpCat.of N.1))
      φ =
    (toPresheaf R).map ψ
⊢ ∀ (m : (↑cR.pt : Type w)) (x : ModuleColimit hcR hcM),
    (φ : (a : ModuleColimit hcR hcM) → N.1) (m • x) =
      HSMul.hSMul (β := (↑N : Type w)) m ((φ : (a : ModuleColimit hcR hcM) → N.1) x : N.1)

Tactic:
(map_smul_homEquiv'_iff hcR hcM φ).1 (fun U r m ↦ ?_)

Premises used: Iff.mp, PresheafOfModules.ModuleColimit.map_smul_homEquiv'_iff
-- 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
φ : ModuleColimit hcR hcM →+ N.1
hφ :
  (homEquiv' hcR hcM : (a : ModuleColimit hcR hcM →+ N.1) → M.presheaf ⟶ (Functor.const Cᵒᵖ).obj (AddCommGrpCat.of N.1))
      φ =
    (toPresheaf R).map ψ
refine :
  ∀ (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))
⊢ ∀ (m : (↑cR.pt : Type w)) (x : ModuleColimit hcR hcM),
    (φ : (a : ModuleColimit hcR hcM) → N.1) (m • x) =
      HSMul.hSMul (β := (↑N : Type w)) m ((φ : (a : ModuleColimit hcR hcM) → N.1) x : N.1)

Tactic:
refine (map_smul_homEquiv'_iff hcR hcM φ).1 (fun U r m ↦ ?_)

Premises used: Iff.mp, PresheafOfModules.ModuleColimit.map_smul_homEquiv'_iff
-- 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
φ : ModuleColimit hcR hcM →+ N.1
hφ :
  (homEquiv' hcR hcM : (a : ModuleColimit hcR hcM →+ N.1) → M.presheaf ⟶ (Functor.const Cᵒᵖ).obj (AddCommGrpCat.of N.1))
      φ =
    (toPresheaf R).map ψ
U : Cᵒᵖ
r : (↑(R.obj U) : Type w)
m : (↑(M.obj U) : Type w)
erw :
  (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) (ψ.app U) :
        (a : (↑(M.obj U) : Type w)) → (↑(((constFunctor cR).obj N).obj U) : 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 (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              AddCommGrpCat.carrier) (((toPresheaf R).map ψ).app U) :
            (a : (↑(M.obj U) : Type w)) → (↑N : Type w))
          m :
        (↑N : Type w))
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
          AddCommGrpCat.carrier) (((toPresheaf R).map ψ).app 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 (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              AddCommGrpCat.carrier) (((toPresheaf R).map ψ).app U) :
            (a : (↑(M.obj U) : Type w)) → (↑N : Type w))
          m :
        (↑N : Type w))

Tactic:
erw [toPresheaf_map_app_apply]

Premises used: PresheafOfModules.toPresheaf_map_app_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'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
N : ModuleCat (↑cR.pt : Type w)
ψ : M ⟶ (constFunctor cR).obj N
φ : ModuleColimit hcR hcM →+ N.1
hφ :
  (homEquiv' hcR hcM : (a : ModuleColimit hcR hcM →+ N.1) → M.presheaf ⟶ (Functor.const Cᵒᵖ).obj (AddCommGrpCat.of N.1))
      φ =
    (toPresheaf R).map ψ
U : Cᵒᵖ
r : (↑(R.obj U) : Type w)
m : (↑(M.obj U) : Type w)
rw :
  HSMul.hSMul (β := (↑(((constFunctor cR).obj N).obj U) : Type w)) r
      ((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) (ψ.app U) :
            (a : (↑(M.obj U) : Type w)) → (↑(((constFunctor cR).obj N).obj U) : Type w))
          m :
        (↑(((constFunctor cR).obj N).obj U) : Type w)) =
    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 (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              AddCommGrpCat.carrier) (((toPresheaf R).map ψ).app U) :
            (a : (↑(M.obj U) : Type w)) → (↑N : Type w))
          m :
        (↑N : Type w))
⊢ (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) (ψ.app U) :
        (a : (↑(M.obj U) : Type w)) → (↑(((constFunctor cR).obj N).obj U) : 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 (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              AddCommGrpCat.carrier) (((toPresheaf R).map ψ).app U) :
            (a : (↑(M.obj U) : Type w)) → (↑N : Type w))
          m :
        (↑N : Type w))

Tactic:
rw [map_smul]

Premises used: map_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''
N : ModuleCat (↑cR.pt : Type w)
ψ : M ⟶ (constFunctor cR).obj N
φ : ModuleColimit hcR hcM →+ N.1
hφ :
  (homEquiv' hcR hcM : (a : ModuleColimit hcR hcM →+ N.1) → M.presheaf ⟶ (Functor.const Cᵒᵖ).obj (AddCommGrpCat.of N.1))
      φ =
    (toPresheaf R).map ψ
U : Cᵒᵖ
r : (↑(R.obj U) : Type w)
m : (↑(M.obj U) : Type w)
⊢ HSMul.hSMul (β := (↑(((constFunctor cR).obj N).obj U) : Type w)) r
      ((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) (ψ.app U) :
            (a : (↑(M.obj U) : Type w)) → (↑(((constFunctor cR).obj N).obj U) : Type w))
          m :
        (↑(((constFunctor cR).obj N).obj U) : Type w)) =
    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 (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              AddCommGrpCat.carrier) (((toPresheaf R).map ψ).app U) :
            (a : (↑(M.obj U) : Type w)) → (↑N : Type w))
          m :
        (↑N : 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
N : ModuleCat (↑cR.pt : Type w)
α : ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM) ⟶ N
X : Cᵒᵖ
x : (↑(M.obj X) : Type w)
⊢ Eq (α := (↑(((constFunctor cR).obj N).obj X) : 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) (X := M.obj X) (Y := ((constFunctor cR).obj N).obj X)
            (Hom.app
              ((homEquiv hcR hcM :
                  (a : ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM) ⟶ N) → M ⟶ (constFunctor cR).obj N)
                α)
              X) :
          (a : (↑(M.obj X) : Type w)) → (↑(((constFunctor cR).obj N).obj X) : Type w))
        x :
      (↑(((constFunctor cR).obj N).obj X) : 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 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
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 N' : ModuleCat (↑cR.pt : Type w)
φ : ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM) ⟶ N
g : N ⟶ 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')
        (φ ≫ 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)
          φ ≫
        (constFunctor cR).map g :
      M ⟶ (constFunctor cR).obj N')

Tactic:
rfl

Premises used: ModuleCat.RestrictScalars.obj', PresheafOfModules.homMk, 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
N : ModuleCat (↑cR.pt : Type w)
β : M ⟶ (constFunctor cR).obj N
X : Cᵒᵖ
x : (↑(M.obj X) : Type w)
⊢ Eq (α := (↑N : 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)))
              _ (ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM)) _
              ((AddEquiv.symm (homEquiv hcR hcM) :
                    (a : M ⟶ (constFunctor cR).obj N) → ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM) ⟶ N)
                  β :
                ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM) ⟶ N) :
            LinearMap (R := (↑cR.pt : Type w)) (RingHom.id (↑cR.pt : Type w))
              (↑(ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM)) : Type w) (↑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))
    ((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 : (↑(M.obj X) : Type w)) → (↑(((constFunctor cR).obj N).obj X) : Type w))
        x :
      (↑(((constFunctor cR).obj N).obj X) : Type w))

Tactic:
homEquiv'_symm_apply ..

Premises used: PresheafOfModules.ModuleColimit.homEquiv'_symm_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
N : ModuleCat (↑cR.pt : Type w)
β : M ⟶ (constFunctor cR).obj N
X : Cᵒᵖ
x : (↑(M.obj X) : Type w)
⊢ Eq (α := (↑N : 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)))
              _ (ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM)) _
              ((AddEquiv.symm (homEquiv hcR hcM) :
                    (a : M ⟶ (constFunctor cR).obj N) → ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM) ⟶ N)
                  β :
                ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM) ⟶ N) :
            LinearMap (R := (↑cR.pt : Type w)) (RingHom.id (↑cR.pt : Type w))
              (↑(ModuleCat.of (↑cR.pt : Type w) (ModuleColimit hcR hcM)) : Type w) (↑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))
    ((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 : (↑(M.obj X) : Type w)) → (↑(((constFunctor cR).obj N).obj X) : Type w))
        x :
      (↑(((constFunctor cR).obj N).obj X) : Type w))

Tactic:
exact homEquiv'_symm_apply ..

Premises used: PresheafOfModules.ModuleColimit.homEquiv'_symm_apply