awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor (goal)
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),
    (((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)
have 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)
Tactic: simp only [← hφ, AddEquiv.symm_apply_apply, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor (goal)
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)
have 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))
Tactic: refine (map_smul_homEquiv'_iff hcR hcM φ).1 (fun U r m ↦ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor (goal)
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)
⊢ (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))
have 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))
Tactic: erw [toPresheaf_map_app_apply]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor (goal)
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)
⊢ (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))
have 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))
Tactic: rw [map_smul]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor (hypothesis)
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'
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
          AddCommGrpCat.carrier) (Y := ((Cocone.precompose ((toPresheaf R).map f)).obj cM').pt)
          (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM')) :
        (a : (↑cM.pt : Type w)) → (↑((Cocone.precompose ((toPresheaf R).map f)).obj cM').pt : Type w))
      (HSMul.hSMul (α := (↑cR.pt : Type w)) (β := ModuleColimit hcR hcM)
        ((ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) r : (↑cR.pt : Type w))
        ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM)) =
    HSMul.hSMul (α := (↑cR.pt : Type w)) (β := ModuleColimit hcR hcM')
      ((RingHom.id (↑cR.pt : Type w) : (a : (↑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)) :
        (↑cR.pt : Type w))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
              AddCommGrpCat.carrier) (Y := ((Cocone.precompose ((toPresheaf R).map f)).obj cM').pt)
              (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM')) :
            (a : (↑cM.pt : Type w)) → (↑((Cocone.precompose ((toPresheaf R).map f)).obj cM').pt : Type w))
          ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM) :
        (↑((Cocone.precompose ((toPresheaf R).map f)).obj cM').pt : Type w))
have 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))
Tactic: have h₁ := ConcreteCategory.congr_hom (hcM.fac c U) (r • m)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor (goal)
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
⊢ 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
have 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)
Tactic: ext m
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor (goal)
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
⊢ 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)
have 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)
Tactic: obtain ⟨U, m, rfl⟩ := ιM_jointly_surjective m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor (goal)
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''
⊢ 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))
have 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'')
Tactic: ext m
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor (goal)
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
⊢ 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'')
have 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'')
Tactic: obtain ⟨U, m, rfl⟩ := ιM_jointly_surjective m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor (goal)
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 (α := (↑(((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))
have 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))
Tactic: simp only [homEquiv_app_apply, ModuleCat.hom_comp, ModuleCat.hom_ofHom, LinearMap.coe_comp,
    Function.comp_apply, comp_app]
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor (goal)
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 (α := (↑(((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))
have 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))
Tactic: apply congr_arg