awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.LeftResolution
Goal:
R : Type u
inst : Ring R
X : Type u
M N : ModuleCat R
f : Functor.obj (free R) X ⟶ N
p : M ⟶ N
hp :
  Function.Surjective (α := (↑M : Type u)) (β := (↑N : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) p) :
      (a : (↑M : Type u)) → (↑N : Type u))
obtain :
  ∀ (s : (↑N : Type u) → (↑M : Type u))
    (hs :
      Function.RightInverse s
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier)
              p) :
          (a : (↑M : Type u)) → (↑N : Type u))),
    ∃ (f' : Functor.obj (free R) X ⟶ M), f' ≫ p = f
⊢ ∃ (f' : Functor.obj (free R) X ⟶ M), f' ≫ p = f

Tactic:
obtain ⟨s, hs⟩ := hp.hasRightInverse

Premises used: Function.Surjective.hasRightInverse
-- Module: Mathlib.Algebra.Category.ModuleCat.LeftResolution
Goal:
R : Type u
inst : Ring R
X : Type u
M N : ModuleCat R
f : Functor.obj (free R) X ⟶ N
p : M ⟶ N
hp :
  Function.Surjective (α := (↑M : Type u)) (β := (↑N : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) p) :
      (a : (↑M : Type u)) → (↑N : Type u))
s : (↑N : Type u) → (↑M : Type u)
hs :
  Function.RightInverse s
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) p) :
      (a : (↑M : Type u)) → (↑N : Type u))
⊢ ∃ (f' : Functor.obj (free R) X ⟶ M), f' ≫ p = f

Tactic:
exact ⟨freeDesc (↾fun x ↦ s (f (freeMk x))), by cat_disch⟩
-- Module: Mathlib.Algebra.Category.ModuleCat.LeftResolution
Goal:
R : Type u
inst : Ring R
⊢ ∀ (X : ModuleCat R),
    isProjective (ModuleCat R)
      (Functor.obj (free R)
        (ToType (FC := fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CC := carrier) X))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Category.ModuleCat.Limits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
r : R
s : (j : J) → (↑(F.obj j) : Type w)
sh :
  s ∈
    (F ⋙
        forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
          (CC := carrier)).sections
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((F ⋙
                forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦
                  (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier)).map
            f) :
        (a : (fun (X : Type w) ↦ X) ((F ⋙ forget (ModuleCat R)).obj j)) →
          (fun (X : Type w) ↦ X) ((F ⋙ forget (ModuleCat R)).obj j'))
      ((r • s) j) =
    (r • s) j'

Tactic:
simpa [Functor.sections] using congr_arg (r • ·) (sh f)

Premises used: congr_arg, HSMul.hSMul, CategoryTheory.Functor.sections
-- Module: Mathlib.Algebra.Category.ModuleCat.Limits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
              (CC := carrier)).sections :
      Type (max v w))
⊢ Small.{w, max v w} ↥(sectionsSubmodule F)

Tactic:
inferInstanceAs <| Small.{w} (Functor.sections (F ⋙ forget (ModuleCat R)))

Premises used: _private.0.ModuleCat.instSmallSubtypeForallCarrierObjMemSubmoduleSectionsSubmodule._proof_1
-- Module: Mathlib.Algebra.Category.ModuleCat.Limits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
              (CC := carrier)).sections :
      Type (max v w))
j : J
x : R
x_1 :
  (Types.Small.limitCone
      (F ⋙
        forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
          (CC := carrier))).pt
⊢ (↑(HSMul.hSMul (β :=
            (↑(F ⋙
                    forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦
                      (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier)).sections :
              Type (max w v)))
            x
            ((Equiv.symm
                    (equivShrink
                      (↑(F ⋙
                              forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦
                                (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier)).sections :
                        Type (max w v))) :
                  (a : Shrink.{w, max v w} (↑(F ⋙ forget (ModuleCat R)).sections : Type (max w v))) →
                    (↑(F ⋙ forget (ModuleCat R)).sections : Type (max w v)))
                x_1 :
              (↑(F ⋙
                      forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦
                        (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier)).sections :
                Type (max w v)))) :
        (j : J) → ToType (F.obj j))
      j =
    HSMul.hSMul (β :=
      ToType (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier) (F.obj j)) x
      ((↑((Equiv.symm
                  (equivShrink
                    (↑(F ⋙
                            forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦
                              (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier)).sections :
                      Type (max w v))) :
                (a : Shrink.{w, max w v} (↑(F ⋙ forget (ModuleCat R)).sections : Type (max w v))) →
                  (↑(F ⋙ forget (ModuleCat R)).sections : Type (max w v)))
              x_1) :
          (j : J) → ToType (F.obj j))
        j)

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Limits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
              (CC := carrier)).sections :
      Type (max v w))
x x_1 : J
f : x ⟶ x_1
hf :
  ∀
    (x_2 :
      (↑(Functor.obj
            (Functor.obj (Functor.const J)
              (of R
                (Types.Small.limitCone
                    (F ⋙
                      forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦
                        (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier))).pt))
            x) :
        Type w)),
    Eq (α := (↑(F.obj x_1) : Type w))
      ((Hom.hom
              (CategoryTheory.Functor.map
                  (Functor.obj (Functor.const J)
                    (of R
                      (Types.Small.limitCone
                          (F ⋙
                            forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦
                              (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier))).pt))
                  f ≫
                ↟(limitπLinearMap F x_1)) :
            (a :
                (↑(((Functor.const J).obj (of R (Types.Small.limitCone (F ⋙ forget (ModuleCat R))).pt)).obj x) :
                  Type w)) →
              (↑(F.obj x_1) : Type w))
          x_2 :
        (↑(F.obj x_1) : Type w))
      ((Hom.hom (↟(limitπLinearMap F x) ≫ F.map f) :
            (a :
                (↑(((Functor.const J).obj (of R (Types.Small.limitCone (F ⋙ forget (ModuleCat R))).pt)).obj x) :
                  Type w)) →
              (↑(F.obj x_1) : Type w))
          x_2 :
        (↑(F.obj x_1) : Type w))
⊢ Eq.{w + 1} (α :=
    Functor.obj
        (Functor.obj (Functor.const J)
          (of R
            (Types.Small.limitCone
                (F ⋙
                  forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦
                    (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier))).pt))
        x ⟶
      F.obj x_1)
    (CategoryTheory.Functor.map
        (Functor.obj (Functor.const J)
          (of R
            (Types.Small.limitCone
                (F ⋙
                  forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦
                    (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier))).pt))
        f ≫
      ↟(limitπLinearMap F x_1))
    (↟(limitπLinearMap F x) ≫ F.map f)

Tactic:
ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Limits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
              (CC := carrier)).sections :
      Type (max v w))
x x_1 : J
f : x ⟶ x_1
x_2 :
  (↑(Functor.obj
        (Functor.obj (Functor.const J)
          (of R
            (Types.Small.limitCone
                (F ⋙
                  forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦
                    (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier))).pt))
        x) :
    Type w)
⊢ Eq (α := (↑(F.obj x_1) : Type w))
    ((Hom.hom
            (CategoryTheory.Functor.map
                (Functor.obj (Functor.const J)
                  (of R
                    (Types.Small.limitCone
                        (F ⋙
                          forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦
                            (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier))).pt))
                f ≫
              ↟(limitπLinearMap F x_1)) :
          (a :
              (↑(((Functor.const J).obj (of R (Types.Small.limitCone (F ⋙ forget (ModuleCat R))).pt)).obj x) :
                Type w)) →
            (↑(F.obj x_1) : Type w))
        x_2 :
      (↑(F.obj x_1) : Type w))
    ((Hom.hom (↟(limitπLinearMap F x) ≫ F.map f) :
          (a :
              (↑(((Functor.const J).obj (of R (Types.Small.limitCone (F ⋙ forget (ModuleCat R))).pt)).obj x) :
                Type w)) →
            (↑(F.obj x_1) : Type w))
        x_2 :
      (↑(F.obj x_1) : Type w))

Tactic:
simpa using (Types.Small.limitCone (F ⋙ forget _)).π.naturality_apply f _

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.NatTrans.naturality_apply, CategoryTheory.Limits.Types.Small.limitCone, CategoryTheory.Functor.comp, CategoryTheory.forget
-- Module: Mathlib.Algebra.Category.ModuleCat.Limits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
              (CC := carrier)).sections :
      Type (max v w))
s : Cone F
x y : (↑s.1 : Type w)
⊢ Subtype.mk (p :=
      fun
        (x :
          (j : J) →
            ToType (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier)
              (F.obj j)) ↦
      x ∈
        (F ⋙
            forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
              (CC := carrier)).sections)
      (fun (j : J) ↦
        HAdd.hAdd (α := (↑(F.obj j) : Type w)) (β := (↑(F.obj j) : Type w))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC :=
                  carrier) (s.π.app j) :
                (a : (↑s.pt : Type w)) → (↑(F.obj j) : Type w))
              x :
            (↑(F.obj j) : Type w))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC :=
                  carrier) (s.π.app j) :
                (a : (↑s.pt : Type w)) → (↑(F.obj j) : Type w))
              y :
            (↑(F.obj j) : Type w)))
      ⋯ =
    HAdd.hAdd (α :=
      (↑(F ⋙
              forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
                (CC := carrier)).sections :
        Type (max w v)))
      (Subtype.mk (p :=
        fun
          (x :
            (j : J) →
              ToType (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier)
                (F.obj j)) ↦
        x ∈
          (F ⋙
              forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
                (CC := carrier)).sections)
        (fun (j : J) ↦
          (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC :=
                carrier) (s.π.app j) :
              (a : (↑s.pt : Type w)) → (↑(F.obj j) : Type w))
            x)
        ⋯)
      (Subtype.mk (p :=
        fun
          (x :
            (j : J) →
              ToType (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier)
                (F.obj j)) ↦
        x ∈
          (F ⋙
              forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
                (CC := carrier)).sections)
        (fun (j : J) ↦
          (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC :=
                carrier) (s.π.app j) :
              (a : (↑s.pt : Type w)) → (↑(F.obj j) : Type w))
            y)
        ⋯)

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Limits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
              (CC := carrier)).sections :
      Type (max v w))
s : Cone F
r : R
x : (↑s.1 : Type w)
⊢ Subtype.mk (p :=
      fun
        (x :
          (j : J) →
            ToType (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier)
              (F.obj j)) ↦
      x ∈
        (F ⋙
            forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
              (CC := carrier)).sections)
      (fun (j : J) ↦
        HSMul.hSMul (β := (↑(F.obj j) : Type w)) r
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC :=
                  carrier) (s.π.app j) :
                (a : (↑s.pt : Type w)) → (↑(F.obj j) : Type w))
              x :
            (↑(F.obj j) : Type w)))
      ⋯ =
    HSMul.hSMul (β :=
      (↑(F ⋙
              forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
                (CC := carrier)).sections :
        Type (max w v)))
      r
      (Subtype.mk (p :=
        fun
          (x :
            (j : J) →
              ToType (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC := carrier)
                (F.obj j)) ↦
        x ∈
          (F ⋙
              forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
                (CC := carrier)).sections)
        (fun (j : J) ↦
          (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC :=
                carrier) (s.π.app j) :
              (a : (↑s.pt : Type w)) → (↑(F.obj j) : Type w))
            x)
        ⋯)

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Limits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
              (CC := carrier)).sections :
      Type (max v w))
⊢ HasLimit F

Tactic:
HasLimit.mk {
    cone := limitCone F
    isLimit := limitConeIsLimit F
  }

Premises used: ModuleCat.HasLimits.limitCone, CategoryTheory.Limits.HasLimit.mk, ModuleCat.HasLimits.limitConeIsLimit, CategoryTheory.Limits.LimitCone.mk
-- Module: Mathlib.Algebra.Category.ModuleCat.Limits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
              (CC := carrier)).sections :
      Type (max v w))
⊢ HasLimits (ModuleCat.{w, u} R)

Tactic:
ModuleCat.hasLimitsOfSize.{w, w, w, u}

Premises used: ModuleCat.hasLimitsOfSize
-- Module: Mathlib.Algebra.Category.ModuleCat.Limits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
              (CC := carrier)).sections :
      Type (max v w))
⊢ HasLimits.{u, u + 1} (ModuleCat R)

Tactic:
ModuleCat.hasLimitsOfSize.{u, u, u}

Premises used: ModuleCat.hasLimitsOfSize
-- Module: Mathlib.Algebra.Category.ModuleCat.Limits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
              (CC := carrier)).sections :
      Type (max v w))
⊢ PreservesLimit F
    (forget₂ (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC :=
      carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CD :=
      AddCommGrpCat.carrier))

Tactic:
preservesLimit_of_preserves_limit_cone (limitConeIsLimit F)
    (forget₂AddCommGroup_preservesLimitsAux F)

Premises used: ModuleCat.forget₂AddCommGroup_preservesLimitsAux, ModuleCat.HasLimits.limitConeIsLimit, CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone
-- Module: Mathlib.Algebra.Category.ModuleCat.Limits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
              (CC := carrier)).sections :
      Type (max v w))
⊢ PreservesLimits
    (forget₂ (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC :=
      carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CD :=
      AddCommGrpCat.carrier))

Tactic:
ModuleCat.forget₂AddCommGroup_preservesLimitsOfSize.{w, w}

Premises used: ModuleCat.forget₂AddCommGroup_preservesLimitsOfSize
-- Module: Mathlib.Algebra.Category.ModuleCat.Limits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
              (CC := carrier)).sections :
      Type (max v w))
⊢ PreservesLimits
    (forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC :=
      carrier))

Tactic:
ModuleCat.forget_preservesLimitsOfSize.{w, w}

Premises used: ModuleCat.forget_preservesLimitsOfSize
-- Module: Mathlib.Algebra.Category.ModuleCat.Limits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
c : Cone F
hc :
  IsLimit (F :=
    F ⋙
      forget₂ (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC :=
        carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CD :=
        AddCommGrpCat.carrier))
    (Functor.mapCone
      (forget₂ (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CD :=
        AddCommGrpCat.carrier))
      c)
⊢ HasLimit
    (F ⋙
      forget₂ (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC :=
        carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CD :=
        AddCommGrpCat.carrier))

Tactic:
have : HasLimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) := ⟨_, hc⟩
-- Module: Mathlib.Algebra.Category.ModuleCat.Limits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
c : Cone F
hc :
  IsLimit (F :=
    F ⋙
      forget₂ (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC :=
        carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CD :=
        AddCommGrpCat.carrier))
    (Functor.mapCone
      (forget₂ (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CD :=
        AddCommGrpCat.carrier))
      c)
this :
  HasLimit
    (F ⋙
      forget₂ (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC :=
        carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CD :=
        AddCommGrpCat.carrier))
⊢ Small.{w, max v w}
    (↑(F ⋙
            forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
              (CC := carrier)).sections :
      Type (max v w))

Tactic:
simpa only [AddCommGrpCat.hasLimit_iff_small_sections] using this

Premises used: AddCommGrpCat.hasLimit_iff_small_sections
-- Module: Mathlib.Algebra.Category.ModuleCat.Limits
Goal:
R : Type u
inst : Ring R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ ModuleCat.{w, u} R
c : Cone F
hc :
  IsLimit (F :=
    F ⋙
      forget₂ (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC :=
        carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CD :=
        AddCommGrpCat.carrier))
    (Functor.mapCone
      (forget₂ (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
        (CC := carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CD :=
        AddCommGrpCat.carrier))
      c)
this :
  HasLimit
    (F ⋙
      forget₂ (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w)) (CC :=
        carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{w}) ↦ (↑x1 : Type w) →+ (↑x2 : Type w)) (CD :=
        AddCommGrpCat.carrier))
⊢ Small.{w, max v w}
    (↑(F ⋙
            forget (ModuleCat.{w, u} R) (FC := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
              (CC := carrier)).sections :
      Type (max v w))

Tactic:
have : Small.{w} (Functor.sections (F ⋙ forget (ModuleCat R))) := by
      simpa only [AddCommGrpCat.hasLimit_iff_small_sections] using this