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 : ModuleCat (↑cR.pt : Type w)
X Y : Cᵒᵖ
f : X ⟶ Y
x : (↑(R.obj X) : Type w)
⊢ Eq (α := (↑cR.pt : Type w))
    ((RingCat.Hom.hom (cR.ι.app X) : (a : (↑(R.obj X) : Type w)) → (↑cR.pt : Type w)) x : (↑cR.pt : Type w))
    (((RingCat.Hom.hom (cR.ι.app Y)).comp (RingCat.Hom.hom (R.map f)) : (a : (↑(R.obj X) : Type w)) → (↑cR.pt : Type w))
        x :
      (↑cR.pt : Type w))
have a : Eq (α := (↑cR.pt : Type w))
  ((RingCat.Hom.hom (R.map f ≫ cR.ι.app Y) : (a : (↑(R.obj X) : Type w)) → (↑cR.pt : Type w)) x : (↑cR.pt : Type w))
  (((RingCat.Hom.hom (cR.ι.app Y)).comp (RingCat.Hom.hom (R.map f)) : (a : (↑(R.obj X) : Type w)) → (↑cR.pt : Type w))
      x :
    (↑cR.pt : Type w))
Tactic: rw [← Cocone.w cR f]
-- 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 : ModuleCat (↑cR.pt : Type w)
X Y : Cᵒᵖ
f : X ⟶ Y
x : (↑(R.obj X) : Type w)
⊢ Eq (α := (↑cR.pt : Type w))
    ((RingCat.Hom.hom (R.map f ≫ cR.ι.app Y) : (a : (↑(R.obj X) : Type w)) → (↑cR.pt : Type w)) x : (↑cR.pt : Type w))
    (((RingCat.Hom.hom (cR.ι.app Y)).comp (RingCat.Hom.hom (R.map f)) : (a : (↑(R.obj X) : Type w)) → (↑cR.pt : Type w))
        x :
      (↑cR.pt : Type w))
have a : Eq (α := (↑cR.pt : Type w))
  (((RingCat.Hom.hom (cR.ι.app Y)).comp (RingCat.Hom.hom (R.map f)) : (a : (↑(R.obj X) : Type w)) → (↑cR.pt : Type w))
      x :
    (↑cR.pt : Type w))
  (((RingCat.Hom.hom (cR.ι.app Y)).comp (RingCat.Hom.hom (R.map f)) : (a : (↑(R.obj X) : Type w)) → (↑cR.pt : Type w))
      x :
    (↑cR.pt : Type w))
Tactic: dsimp
-- 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 : ModuleColimit hcR hcM
m' : ModuleColimit hcR hcM'
⊢ ∃ (U : Cᵒᵖ) (x : (↑(M.obj U) : Type w)) (x' : (↑(M'.obj U) : Type w)),
    (ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) x = m ∧
      (ιM : (a : (↑(M'.obj U) : Type w)) → ModuleColimit hcR hcM') x' = m'
have obtain : ∀ (U : Cᵒᵖ)
  (x :
    (M.presheaf ⋙
          forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
            AddCommGrpCat.carrier)).obj
      U)
  (x' :
    (M'.presheaf ⋙
          forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
            AddCommGrpCat.carrier)).obj
      U)
  (h :
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app
              (Cocone.ι
                (Cocone.tensor
                  (Functor.mapCocone
                    (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
                      (CC := AddCommGrpCat.carrier))
                    cM)
                  (Functor.mapCocone
                    (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
                      (CC := AddCommGrpCat.carrier))
                    cM')))
              U) :
          (a :
              (fun (X : Type w) ↦ X) ((M.presheaf ⋙ forget AddCommGrpCat ⊗ M'.presheaf ⋙ forget AddCommGrpCat).obj U)) →
            (fun (X : Type w) ↦ X)
              (((Functor.const Cᵒᵖ).obj
                    (((forget AddCommGrpCat).mapCocone cM).tensor ((forget AddCommGrpCat).mapCocone cM')).pt).obj
                U))
        (x, x') =
      (m, m')),
  ∃ (U : Cᵒᵖ) (x : (↑(M.obj U) : Type w)) (x' : (↑(M'.obj U) : Type w)),
    (ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) x = m ∧
      (ιM : (a : (↑(M'.obj U) : Type w)) → ModuleColimit hcR hcM') x' = m'
Tactic: obtain ⟨U, ⟨x, x'⟩, h⟩ := Types.jointly_surjective_of_isColimit
    ((isColimitOfPreserves (forget AddCommGrpCat) hcM).tensor
      (isColimitOfPreserves (forget AddCommGrpCat) hcM')) ⟨m, 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
r : (↑cR.pt : Type w)
m : ModuleColimit hcR hcM
⊢ ∃ (U : Cᵒᵖ) (a : (↑(R.obj U) : Type w)) (x : (↑(M.obj U) : Type w)),
    (ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) a = r ∧
      (ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) x = m
have obtain : ∀ (U : Cᵒᵖ)
  (a :
    (R ⋙ forget RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC := RingCat.carrier)).obj
      U)
  (x :
    (M.presheaf ⋙
          forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
            AddCommGrpCat.carrier)).obj
      U)
  (h :
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app
              (Cocone.ι
                (Cocone.tensor
                  (Functor.mapCocone
                    (forget RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
                      RingCat.carrier))
                    cR)
                  (Functor.mapCocone
                    (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
                      (CC := AddCommGrpCat.carrier))
                    cM)))
              U) :
          (a : (fun (X : Type w) ↦ X) ((R ⋙ forget RingCat ⊗ M.presheaf ⋙ forget AddCommGrpCat).obj U)) →
            (fun (X : Type w) ↦ X)
              (((Functor.const Cᵒᵖ).obj
                    (((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM)).pt).obj
                U))
        (a, x) =
      (r, m)),
  ∃ (U : Cᵒᵖ) (a : (↑(R.obj U) : Type w)) (x : (↑(M.obj U) : Type w)),
    (ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) a = r ∧
      (ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) x = m
Tactic: obtain ⟨U, ⟨a, x⟩, h⟩ := Types.jointly_surjective_of_isColimit
    ((isColimitOfPreserves (forget RingCat) hcR).tensor
      (isColimitOfPreserves (forget AddCommGrpCat) hcM)) ⟨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
r₁ r₂ : (↑cR.pt : Type w)
m : ModuleColimit hcR hcM
⊢ ∃ (U : Cᵒᵖ) (a₁ : (↑(R.obj U) : Type w)) (a₂ : (↑(R.obj U) : Type w)) (x : (↑(M.obj U) : Type w)),
    (ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) a₁ = r₁ ∧
      (ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) a₂ = r₂ ∧
        (ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) x = m
have obtain : ∀ (U : Cᵒᵖ)
  (a₁ a₂ :
    (R ⋙ forget RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC := RingCat.carrier)).obj
      U)
  (x :
    (M.presheaf ⋙
          forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
            AddCommGrpCat.carrier)).obj
      U)
  (h :
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app
              (Cocone.ι
                (Cocone.tensor
                  (Functor.mapCocone
                    (forget RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
                      RingCat.carrier))
                    cR)
                  (Cocone.tensor
                    (Functor.mapCocone
                      (forget RingCat (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
                        RingCat.carrier))
                      cR)
                    (Functor.mapCocone
                      (forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w))
                        (CC := AddCommGrpCat.carrier))
                      cM))))
              U) :
          (a :
              (fun (X : Type w) ↦ X)
                ((R ⋙ forget RingCat ⊗ R ⋙ forget RingCat ⊗ M.presheaf ⋙ forget AddCommGrpCat).obj U)) →
            (fun (X : Type w) ↦ X)
              (((Functor.const Cᵒᵖ).obj
                    (((forget RingCat).mapCocone cR).tensor
                        (((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM))).pt).obj
                U))
        (a₁, a₂, x) =
      (r₁, r₂, m)),
  ∃ (U : Cᵒᵖ) (a₁ : (↑(R.obj U) : Type w)) (a₂ : (↑(R.obj U) : Type w)) (x : (↑(M.obj U) : Type w)),
    (ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) a₁ = r₁ ∧
      (ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) a₂ = r₂ ∧
        (ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) x = m
Tactic: obtain ⟨U, ⟨a₁, a₂, x⟩, h⟩ := Types.jointly_surjective_of_isColimit
    ((isColimitOfPreserves (forget RingCat) hcR).tensor
      ((isColimitOfPreserves (forget RingCat) hcR).tensor
        (isColimitOfPreserves (forget AddCommGrpCat) hcM))) ⟨r₁, 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''
r₁ r₂ : (↑cR.pt : Type w)
m : ModuleColimit hcR hcM
⊢ (r₁ * r₂) • m = r₁ • r₂ • m
have obtain : ∀ (U : Cᵒᵖ) (r₁ r₂ : (↑(R.obj U) : Type w)) (m : (↑(M.obj U) : Type w)),
  HSMul.hSMul (β := ModuleColimit hcR hcM)
      (HMul.hMul (α := (↑cR.pt : Type w)) (β := (↑cR.pt : Type w))
        ((ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) r₁ : (↑cR.pt : Type w))
        ((ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) r₂ : (↑cR.pt : Type w)))
      ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM) =
    HSMul.hSMul (α := (↑cR.pt : Type w))
      ((ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) r₁ : (↑cR.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))
Tactic: obtain ⟨U, r₁, r₂, m, rfl, rfl, rfl⟩ := jointly_surjective₃ r₁ r₂ m
Cleared hypotheses: r₁, 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''
m : ModuleColimit hcR hcM
⊢ HSMul.hSMul (α := (↑cR.pt : Type w)) 1 m = m
have obtain : ∀ (U : Cᵒᵖ) (m : (↑(M.obj U) : Type w)),
  HSMul.hSMul (α := (↑cR.pt : Type w)) (β := ModuleColimit hcR hcM) 1
      ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM) =
    (ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m
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'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
r : (↑cR.pt : Type w)
⊢ HSMul.hSMul (β := ModuleColimit hcR hcM) r 0 = 0
have obtain : ∀ (U : Cᵒᵖ) (r : (↑(R.obj U) : Type w)),
  HSMul.hSMul (α := (↑cR.pt : Type w)) (β := ModuleColimit hcR hcM)
      ((ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) r : (↑cR.pt : Type w)) 0 =
    0
Tactic: obtain ⟨U, r, rfl⟩ := ιR_jointly_surjective hcR r
Cleared hypotheses: r
-- 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''
r : (↑cR.pt : Type w)
m₁ m₂ : ModuleColimit hcR hcM
⊢ r • (m₁ + m₂) = r • m₁ + r • m₂
have obtain : ∀ (U : Cᵒᵖ) (r : (↑(R.obj U) : Type w)) (m₁ m₂ : (↑(M.obj U) : Type w)),
  HSMul.hSMul (α := (↑cR.pt : Type w)) ((ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) r : (↑cR.pt : Type w))
      (HAdd.hAdd (α := ModuleColimit hcR hcM) (β := ModuleColimit hcR hcM)
        ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m₁ : ModuleColimit hcR hcM)
        ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m₂ : ModuleColimit hcR hcM)) =
    HSMul.hSMul (α := (↑cR.pt : Type w)) (β := ModuleColimit hcR hcM)
        ((ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) r : (↑cR.pt : Type w))
        ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m₁ : ModuleColimit hcR hcM) +
      HSMul.hSMul (α := (↑cR.pt : Type w)) (β := ModuleColimit hcR hcM)
        ((ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) r : (↑cR.pt : Type w))
        ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m₂ : ModuleColimit hcR hcM)
Tactic: obtain ⟨U, r, m₁, m₂, rfl, rfl, rfl⟩ := jointly_surjective₃' r m₁ m₂
Cleared hypotheses: r, m₁, 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''
r₁ r₂ : (↑cR.pt : Type w)
m : ModuleColimit hcR hcM
⊢ (r₁ + r₂) • m = r₁ • m + r₂ • m
have obtain : ∀ (U : Cᵒᵖ) (r₁ r₂ : (↑(R.obj U) : Type w)) (m : (↑(M.obj U) : Type w)),
  HSMul.hSMul (β := ModuleColimit hcR hcM)
      (HAdd.hAdd (α := (↑cR.pt : Type w)) (β := (↑cR.pt : Type w))
        ((ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) r₁ : (↑cR.pt : Type w))
        ((ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) r₂ : (↑cR.pt : Type w)))
      ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM) =
    HSMul.hSMul (α := (↑cR.pt : Type w)) (β := ModuleColimit hcR hcM)
        ((ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) r₁ : (↑cR.pt : Type w))
        ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM) +
      HSMul.hSMul (α := (↑cR.pt : Type w)) (β := ModuleColimit hcR hcM)
        ((ιR cR : (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w)) r₂ : (↑cR.pt : Type w))
        ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM)
Tactic: obtain ⟨U, r₁, r₂, m, rfl, rfl, rfl⟩ := jointly_surjective₃ r₁ r₂ m
Cleared hypotheses: r₁, 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''
m : ModuleColimit hcR hcM
⊢ HSMul.hSMul (α := (↑cR.pt : Type w)) 0 m = 0
have obtain : ∀ (U : Cᵒᵖ) (m : (↑(M.obj U) : Type w)),
  HSMul.hSMul (α := (↑cR.pt : Type w)) (β := ModuleColimit hcR hcM) 0
      ((ιM : (a : (↑(M.obj U) : Type w)) → ModuleColimit hcR hcM) m : ModuleColimit hcR hcM) =
    0
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
N : ModuleCat (↑cR.pt : Type w)
α : ModuleColimit hcR hcM →+ (↑N : Type w)
h :
  ∀ (r : (↑cR.pt : Type w)) (m : ModuleColimit hcR hcM),
    (α : (a : ModuleColimit hcR hcM) → (↑N : Type w)) (r • m) =
      HSMul.hSMul (β := (↑N : Type w)) r ((α : (a : ModuleColimit hcR hcM) → (↑N : Type w)) m : (↑N : Type w))
U : Cᵒᵖ
r : (↑(R.obj U) : Type w)
m : (↑(M.obj U) : Type w)
⊢ Eq (α := (↑N : Type w))
    ((α : (a : ModuleColimit hcR hcM) → (↑N : Type w))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                AddCommGrpCat.carrier) (cM.ι.app U) :
              (a : (↑(M.obj U) : Type w)) → (↑cM.pt : Type w))
            (r • m) :
          (↑cM.pt : Type w)) :
      (↑N : Type w))
    ((α : (a : ModuleColimit hcR hcM) → (↑N : Type w))
        (HSMul.hSMul (α := (↑cR.pt : Type w)) (β := ModuleColimit hcR hcM)
          ((ConcreteCategory.hom (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC :=
                  RingCat.carrier) (cR.ι.app U) :
                (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w))
              r :
            (↑cR.pt : Type w))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
                  AddCommGrpCat.carrier) (cM.ι.app U) :
                (a : (↑(M.obj U) : Type w)) → (↑cM.pt : Type w))
              m :
            (↑cM.pt : Type w))) :
      (↑N : Type w))
have refine_2 : (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
        AddCommGrpCat.carrier) (cM.ι.app U) :
      (a : (↑(M.obj U) : Type w)) → (↑cM.pt : Type w))
    (r • m) =
  HSMul.hSMul (α := (↑cR.pt : Type w)) (β := ModuleColimit hcR hcM)
    ((ConcreteCategory.hom (FC := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CC := RingCat.carrier)
            (cR.ι.app U) :
          (a : (↑(R.obj U) : Type w)) → (↑cR.pt : Type w))
        r :
      (↑cR.pt : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CC :=
            AddCommGrpCat.carrier) (cM.ι.app U) :
          (a : (↑(M.obj U) : Type w)) → (↑cM.pt : Type w))
        m :
      (↑cM.pt : Type w))
Tactic: congr 1
-- 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
⊢ ∀ (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 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)
Tactic: obtain ⟨φ, hφ⟩ := (homEquiv' hcR hcM).surjective ((toPresheaf _).map ψ)