awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : J ⥤ Type (max v u)
x : Cone F
x_1 : x.pt ⟶ (limitCone.{v, u, w} F).pt
w : ∀ (j : J), x_1 ≫ (limitCone.{v, u, w} F).π.app j = x.π.app j
h :
  ∀ (x_2 : x.pt),
    (hom (FC := TypeCat.Fun) x_1).toFun x_2 =
      TypeCat.Fun.toFun
        (hom (FC := TypeCat.Fun)
          (↾fun (v : x.pt) ↦
            Subtype.mk (p := fun (x : (j : J) → F.obj j) ↦ x ∈ F.sections)
              (fun (j : J) ↦
                (hom (FC := TypeCat.Fun) (x.π.app j) :
                    (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const J).obj x.pt).obj j)) →
                      (fun (X : Type (max u v)) ↦ X) (F.obj j))
                  v)
              ⋯))
        x_2
⊢ x_1 =
    ↾fun (v : x.pt) ↦
      Subtype.mk (p := fun (x : (j : J) → F.obj j) ↦ x ∈ F.sections)
        (fun (j : J) ↦
          (hom (FC := TypeCat.Fun) (x.π.app j) :
              (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const J).obj x.pt).obj j)) →
                (fun (X : Type (max u v)) ↦ X) (F.obj j))
            v)
        ⋯

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : J ⥤ Type (max v u)
x_1 : Cone F
x_2 : x_1.pt ⟶ (limitCone.{v, u, w} F).pt
w : ∀ (j : J), x_2 ≫ (limitCone.{v, u, w} F).π.app j = x_1.π.app j
x : x_1.pt
h :
  (↑((hom (FC := TypeCat.Fun) x_2).toFun x) : (j : J) → F.obj j) =
    (↑(TypeCat.Fun.toFun
          (hom (FC := TypeCat.Fun)
            (↾fun (v : x_1.pt) ↦
              Subtype.mk (p := fun (x : (j : J) → F.obj j) ↦ x ∈ F.sections)
                (fun (j : J) ↦
                  (hom (FC := TypeCat.Fun) (x_1.π.app j) :
                      (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const J).obj x_1.pt).obj j)) →
                        (fun (X : Type (max u v)) ↦ X) (F.obj j))
                    v)
                ⋯))
          x) :
      (j : J) → F.obj j)
⊢ (hom (FC := TypeCat.Fun) x_2).toFun x =
    TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (↾fun (v : x_1.pt) ↦
          Subtype.mk (p := fun (x : (j : J) → F.obj j) ↦ x ∈ F.sections)
            (fun (j : J) ↦
              (hom (FC := TypeCat.Fun) (x_1.π.app j) :
                  (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const J).obj x_1.pt).obj j)) →
                    (fun (X : Type (max u v)) ↦ X) (F.obj j))
                v)
            ⋯))
      x

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : J ⥤ Type (max v u)
x_1 : Cone F
x_2 : x_1.pt ⟶ (limitCone.{v, u, w} F).pt
w : ∀ (j : J), x_2 ≫ (limitCone.{v, u, w} F).π.app j = x_1.π.app j
x : x_1.pt
h :
  ∀ (j : J),
    (↑((hom (FC := TypeCat.Fun) x_2).toFun x) : (j : J) → F.obj j) j =
      (↑(TypeCat.Fun.toFun
              (hom (FC := TypeCat.Fun)
                (↾fun (v : x_1.pt) ↦
                  Subtype.mk (p := fun (x : (j : J) → F.obj j) ↦ x ∈ F.sections)
                    (fun (j : J) ↦
                      (hom (FC := TypeCat.Fun) (x_1.π.app j) :
                          (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const J).obj x_1.pt).obj j)) →
                            (fun (X : Type (max u v)) ↦ X) (F.obj j))
                        v)
                    ⋯))
              x) :
          (j : J) → F.obj j)
        j
⊢ (↑((hom (FC := TypeCat.Fun) x_2).toFun x) : (j : J) → F.obj j) =
    (↑(TypeCat.Fun.toFun
          (hom (FC := TypeCat.Fun)
            (↾fun (v : x_1.pt) ↦
              Subtype.mk (p := fun (x : (j : J) → F.obj j) ↦ x ∈ F.sections)
                (fun (j : J) ↦
                  (hom (FC := TypeCat.Fun) (x_1.π.app j) :
                      (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const J).obj x_1.pt).obj j)) →
                        (fun (X : Type (max u v)) ↦ X) (F.obj j))
                    v)
                ⋯))
          x) :
      (j : J) → F.obj j)

Tactic:
funext j
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : J ⥤ Type (max v u)
x_1 : Cone F
x_2 : x_1.pt ⟶ (limitCone.{v, u, w} F).pt
w : ∀ (j : J), x_2 ≫ (limitCone.{v, u, w} F).π.app j = x_1.π.app j
x : x_1.pt
j : J
⊢ (↑((hom (FC := TypeCat.Fun) x_2).toFun x) : (j : J) → F.obj j) j =
    (↑(TypeCat.Fun.toFun
            (hom (FC := TypeCat.Fun)
              (↾fun (v : x_1.pt) ↦
                Subtype.mk (p := fun (x : (j : J) → F.obj j) ↦ x ∈ F.sections)
                  (fun (j : J) ↦
                    (hom (FC := TypeCat.Fun) (x_1.π.app j) :
                        (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const J).obj x_1.pt).obj j)) →
                          (fun (X : Type (max u v)) ↦ X) (F.obj j))
                      v)
                  ⋯))
            x) :
        (j : J) → F.obj j)
      j

Tactic:
congr_hom (w j) x

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : J ⥤ Type (max v u)
x_1 : Cone F
x_2 : x_1.pt ⟶ (limitCone.{v, u, w} F).pt
w : ∀ (j : J), x_2 ≫ (limitCone.{v, u, w} F).π.app j = x_1.π.app j
x : x_1.pt
j : J
⊢ (↑((hom (FC := TypeCat.Fun) x_2).toFun x) : (j : J) → F.obj j) j =
    (↑(TypeCat.Fun.toFun
            (hom (FC := TypeCat.Fun)
              (↾fun (v : x_1.pt) ↦
                Subtype.mk (p := fun (x : (j : J) → F.obj j) ↦ x ∈ F.sections)
                  (fun (j : J) ↦
                    (hom (FC := TypeCat.Fun) (x_1.π.app j) :
                        (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const J).obj x_1.pt).obj j)) →
                          (fun (X : Type (max u v)) ↦ X) (F.obj j))
                      v)
                  ⋯))
            x) :
        (j : J) → F.obj j)
      j

Tactic:
exact congr_hom (w j) x

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
inst_1 : Small.{u, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
⊢ HasLimit F

Tactic:
(hasLimit_iff_small_sections F).mpr inferInstance

Premises used: Iff.mpr, inferInstance, CategoryTheory.Limits.Types.hasLimit_iff_small_sections
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasLimit F
x : limit F
j : J
⊢ Eq.{u + 1} (α := F.obj j)
    ((↑((limitEquivSections F : (a : limit F) → (↑F.sections : Type (max u v))) x) : (j : J) → F.obj j) j : F.obj j)
    ((hom (FC := TypeCat.Fun) (limit.π F j) : (a : limit F) → F.obj j) x : F.obj j)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasLimit F
x : (↑F.sections : Type (max u v))
j : J
⊢ (hom (FC := TypeCat.Fun) (limit.π F j) : (a : (fun (X : Type u) ↦ X) (limit F)) → (fun (X : Type u) ↦ X) (F.obj j))
      ((Equiv.symm (limitEquivSections F) : (a : (↑F.sections : Type (max u v))) → limit F) x : limit F) =
    (↑x : (j : J) → F.obj j) j

Tactic:
isLimitEquivSections_symm_apply _ _ _

Premises used: CategoryTheory.Limits.Types.isLimitEquivSections_symm_apply
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasLimit F
X Y : J ⥤ Type (max u v)
f : X ⟶ Y
h :
  ∀ (x : Functor.obj lim X),
    Eq (α := Functor.obj (Functor.sectionsFunctor J) Y)
      (TypeCat.Fun.toFun
        (hom (FC := TypeCat.Fun)
          (Functor.map lim f ≫
            Iso.hom
              ((fun (F : J ⥤ Type (max u v)) ↦
                  (Equiv.toIso (limitEquivSections F) : limit F ≅ (↑F.sections : Type (max u v))))
                Y)))
        x)
      (TypeCat.Fun.toFun
        (hom (FC := TypeCat.Fun)
          (Iso.hom
              ((fun (F : J ⥤ Type (max u v)) ↦
                  (Equiv.toIso (limitEquivSections F) : limit F ≅ (↑F.sections : Type (max u v))))
                X) ≫
            Functor.map (Functor.sectionsFunctor J) f))
        x)
⊢ Eq (α := Functor.obj lim X ⟶ Functor.obj (Functor.sectionsFunctor J) Y)
    (Functor.map lim f ≫
      Iso.hom
        ((fun (F : J ⥤ Type (max u v)) ↦
            (Equiv.toIso (limitEquivSections F) : limit F ≅ (↑F.sections : Type (max u v))))
          Y))
    (Iso.hom
        ((fun (F : J ⥤ Type (max u v)) ↦
            (Equiv.toIso (limitEquivSections F) : limit F ≅ (↑F.sections : Type (max u v))))
          X) ≫
      Functor.map (Functor.sectionsFunctor J) f)

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasLimit F
X Y : J ⥤ Type (max u v)
f : X ⟶ Y
x : Functor.obj lim X
⊢ Eq (α := Functor.obj (Functor.sectionsFunctor J) Y)
    (TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (Functor.map lim f ≫
          Iso.hom
            ((fun (F : J ⥤ Type (max u v)) ↦
                (Equiv.toIso (limitEquivSections F) : limit F ≅ (↑F.sections : Type (max u v))))
              Y)))
      x)
    (TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (F : J ⥤ Type (max u v)) ↦
                (Equiv.toIso (limitEquivSections F) : limit F ≅ (↑F.sections : Type (max u v))))
              X) ≫
          Functor.map (Functor.sectionsFunctor J) f))
      x)

Tactic:
Subtype.ext (funext fun j ↦ congr_hom (limMap_π f j) x)

Premises used: funext, Subtype.ext
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasLimit F
X Y : J ⥤ Type (max u v)
f : X ⟶ Y
x : Functor.obj lim X
⊢ Eq (α := Functor.obj (Functor.sectionsFunctor J) Y)
    (TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (Functor.map lim f ≫
          Iso.hom
            ((fun (F : J ⥤ Type (max u v)) ↦
                (Equiv.toIso (limitEquivSections F) : limit F ≅ (↑F.sections : Type (max u v))))
              Y)))
      x)
    (TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (F : J ⥤ Type (max u v)) ↦
                (Equiv.toIso (limitEquivSections F) : limit F ≅ (↑F.sections : Type (max u v))))
              X) ≫
          Functor.map (Functor.sectionsFunctor J) f))
      x)

Tactic:
exact Subtype.ext (funext fun j ↦ congr_hom (limMap_π f j) x)

Premises used: funext, Subtype.ext
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasLimit F
x : (j : J) → F.obj j
h :
  ∀ (j j' : J) (f : j ⟶ j'),
    (hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj j'))
        (x j) =
      x j'
j : J
⊢ (hom (FC := TypeCat.Fun) (limit.π F j) : (a : limit F) → F.obj j)
      ((Equiv.symm (limitEquivSections F) : (a : (↑F.sections : Type (max u v))) → limit F)
          (Subtype.mk (p := fun (x : (j : J) → F.obj j) ↦ x ∈ F.sections) x ⋯) :
        limit F) =
    x j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasLimit F
x y : limit F
w :
  ∀ (j : J),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj j))
      ((hom (FC := TypeCat.Fun) (limit.π F j) :
            (a : (fun (X : Type u) ↦ X) (limit F)) → (fun (X : Type u) ↦ X) (F.obj j))
          x :
        (fun (X : Type u) ↦ X) (F.obj j))
      ((hom (FC := TypeCat.Fun) (limit.π F j) :
            (a : (fun (X : Type u) ↦ X) (limit F)) → (fun (X : Type u) ↦ X) (F.obj j))
          y :
        (fun (X : Type u) ↦ X) (F.obj j))
a :
  Eq (α := (↑F.sections : Type (max u v)))
    ((limitEquivSections F : (a : limit F) → (↑F.sections : Type (max u v))) x : (↑F.sections : Type (max u v)))
    ((limitEquivSections F : (a : limit F) → (↑F.sections : Type (max u v))) y : (↑F.sections : Type (max u v)))
⊢ x = y

Tactic:
apply (limitEquivSections F).injective

Premises used: CategoryTheory.Limits.Types.limitEquivSections, Equiv.injective
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasLimit F
x y : limit F
w :
  ∀ (j : J),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj j))
      ((hom (FC := TypeCat.Fun) (limit.π F j) :
            (a : (fun (X : Type u) ↦ X) (limit F)) → (fun (X : Type u) ↦ X) (F.obj j))
          x :
        (fun (X : Type u) ↦ X) (F.obj j))
      ((hom (FC := TypeCat.Fun) (limit.π F j) :
            (a : (fun (X : Type u) ↦ X) (limit F)) → (fun (X : Type u) ↦ X) (F.obj j))
          y :
        (fun (X : Type u) ↦ X) (F.obj j))
a :
  ∀ (j : J),
    Eq.{u + 1} (α := F.obj j)
      ((↑((limitEquivSections F : (a : limit F) → (↑F.sections : Type (max u v))) x) : (j : J) → F.obj j) j)
      ((↑((limitEquivSections F : (a : limit F) → (↑F.sections : Type (max u v))) y) : (j : J) → F.obj j) j)
⊢ Eq (α := (↑F.sections : Type (max u v)))
    ((limitEquivSections F : (a : limit F) → (↑F.sections : Type (max u v))) x : (↑F.sections : Type (max u v)))
    ((limitEquivSections F : (a : limit F) → (↑F.sections : Type (max u v))) y : (↑F.sections : Type (max u v)))

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasLimit F
x y : limit F
w :
  ∀ (j : J),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj j))
      ((hom (FC := TypeCat.Fun) (limit.π F j) :
            (a : (fun (X : Type u) ↦ X) (limit F)) → (fun (X : Type u) ↦ X) (F.obj j))
          x :
        (fun (X : Type u) ↦ X) (F.obj j))
      ((hom (FC := TypeCat.Fun) (limit.π F j) :
            (a : (fun (X : Type u) ↦ X) (limit F)) → (fun (X : Type u) ↦ X) (F.obj j))
          y :
        (fun (X : Type u) ↦ X) (F.obj j))
j : J
⊢ Eq.{u + 1} (α := F.obj j)
    ((↑((limitEquivSections F : (a : limit F) → (↑F.sections : Type (max u v))) x) : (j : J) → F.obj j) j)
    ((↑((limitEquivSections F : (a : limit F) → (↑F.sections : Type (max u v))) y) : (j : J) → F.obj j) j)

Tactic:
simp [w j]
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F' : Functor.{w, v, v, v + 1} J (Type v)
x y : limit F'
w :
  ∀ (j : J),
    Eq (α := (fun (X : Type v) ↦ X) (F'.obj j))
      ((hom (FC := TypeCat.Fun) (limit.π F' j) :
            (a : (fun (X : Type v) ↦ X) (limit F')) → (fun (X : Type v) ↦ X) (F'.obj j))
          x :
        (fun (X : Type v) ↦ X) (F'.obj j))
      ((hom (FC := TypeCat.Fun) (limit.π F' j) :
            (a : (fun (X : Type v) ↦ X) (limit F')) → (fun (X : Type v) ↦ X) (F'.obj j))
          y :
        (fun (X : Type v) ↦ X) (F'.obj j))
⊢ x = y

Tactic:
limit_ext F' x y w

Premises used: CategoryTheory.Limits.Types.limit_ext
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F' : Functor.{w, v, v, v + 1} J (Type v)
x y : limit F'
⊢ x = y ↔
    ∀ (j : J),
      Eq (α := (fun (X : Type v) ↦ X) (F'.obj j))
        ((hom (FC := TypeCat.Fun) (limit.π F' j) :
              (a : (fun (X : Type v) ↦ X) (limit F')) → (fun (X : Type v) ↦ X) (F'.obj j))
            x :
          (fun (X : Type v) ↦ X) (F'.obj j))
        ((hom (FC := TypeCat.Fun) (limit.π F' j) :
              (a : (fun (X : Type v) ↦ X) (limit F')) → (fun (X : Type v) ↦ X) (F'.obj j))
            y :
          (fun (X : Type v) ↦ X) (F'.obj j))

Tactic:
⟨fun t _ => t ▸ rfl, limit_ext' _ _ _⟩

Premises used: Eq.rec, Iff.intro, CategoryTheory.Limits.Types.limit_ext', rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasLimit F
j j' : J
x : limit F
f : j ⟶ j'
⊢ Eq (α := (fun (X : Type u) ↦ X) (F.obj j'))
    ((hom (FC := TypeCat.Fun) (F.map f) : (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj j'))
        ((hom (FC := TypeCat.Fun) (limit.π F j) :
              (a : (fun (X : Type u) ↦ X) (limit F)) → (fun (X : Type u) ↦ X) (F.obj j))
            x :
          (fun (X : Type u) ↦ X) (F.obj j)) :
      (fun (X : Type u) ↦ X) (F.obj j'))
    ((hom (FC := TypeCat.Fun) (limit.π F j') :
          (a : (fun (X : Type u) ↦ X) (limit F)) → (fun (X : Type u) ↦ X) (F.obj j'))
        x :
      (fun (X : Type u) ↦ X) (F.obj j'))

Tactic:
limit.w_apply _ _ _

Premises used: CategoryTheory.Limits.limit.w_apply
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasLimit F
s : Cone F
j : J
x : s.pt
⊢ Eq (α := (fun (X : Type u) ↦ X) (F.obj j))
    ((hom (FC := TypeCat.Fun) (limit.π F j) : (a : (fun (X : Type u) ↦ X) (limit F)) → (fun (X : Type u) ↦ X) (F.obj j))
        ((hom (FC := TypeCat.Fun) (limit.lift F s) :
              (a : (fun (X : Type u) ↦ X) s.pt) → (fun (X : Type u) ↦ X) (limit F))
            x :
          (fun (X : Type u) ↦ X) (limit F)) :
      (fun (X : Type u) ↦ X) (F.obj j))
    ((hom (FC := TypeCat.Fun) (s.π.app j) :
          (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj s.pt).obj j)) → (fun (X : Type u) ↦ X) (F.obj j))
        x :
      (fun (X : Type u) ↦ X) (F.obj j))

Tactic:
limit.lift_π_apply _ _ _

Premises used: CategoryTheory.Limits.limit.lift_π_apply
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F G : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasLimit F
inst_2 : HasLimit G
α : F ⟶ G
j : J
x : limit F
⊢ Eq (α := (fun (X : Type u) ↦ X) (G.obj j))
    ((hom (FC := TypeCat.Fun) (limit.π G j) : (a : (fun (X : Type u) ↦ X) (limit G)) → (fun (X : Type u) ↦ X) (G.obj j))
        ((hom (FC := TypeCat.Fun) (limMap α) :
              (a : (fun (X : Type u) ↦ X) (limit F)) → (fun (X : Type u) ↦ X) (limit G))
            x :
          (fun (X : Type u) ↦ X) (limit G)) :
      (fun (X : Type u) ↦ X) (G.obj j))
    ((hom (FC := TypeCat.Fun) (α.app j) : (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (G.obj j))
        ((hom (FC := TypeCat.Fun) (limit.π F j) :
              (a : (fun (X : Type u) ↦ X) (limit F)) → (fun (X : Type u) ↦ X) (F.obj j))
            x :
          (fun (X : Type u) ↦ X) (F.obj j)) :
      (fun (X : Type u) ↦ X) (G.obj j))

Tactic:
limMap_π_apply _ _ _

Premises used: CategoryTheory.Limits.limMap_π_apply
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F' : Functor.{w, v, v, v + 1} J (Type v)
j j' : J
x : limit F'
f : j ⟶ j'
⊢ Eq (α := (fun (X : Type v) ↦ X) (F'.obj j'))
    ((hom (FC := TypeCat.Fun) (F'.map f) : (a : (fun (X : Type v) ↦ X) (F'.obj j)) → (fun (X : Type v) ↦ X) (F'.obj j'))
        ((hom (FC := TypeCat.Fun) (limit.π F' j) :
            (a : (fun (X : Type v) ↦ X) (limit F')) → (fun (X : Type v) ↦ X) (F'.obj j))
          x) :
      (fun (X : Type v) ↦ X) (F'.obj j'))
    ((hom (FC := TypeCat.Fun) (limit.π F' j') :
          (a : (fun (X : Type v) ↦ X) (limit F')) → (fun (X : Type v) ↦ X) (F'.obj j'))
        x :
      (fun (X : Type v) ↦ X) (F'.obj j'))

Tactic:
limit.w_apply _ _ _

Premises used: CategoryTheory.Limits.limit.w_apply
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F' : Functor.{w, v, v, v + 1} J (Type v)
s : Cone F'
j : J
x : s.pt
⊢ Eq (α := (fun (X : Type v) ↦ X) (F'.obj j))
    ((hom (FC := TypeCat.Fun) (limit.π F' j) :
          (a : (fun (X : Type v) ↦ X) (limit F')) → (fun (X : Type v) ↦ X) (F'.obj j))
        ((hom (FC := TypeCat.Fun) (limit.lift F' s) :
            (a : (fun (X : Type v) ↦ X) s.pt) → (fun (X : Type v) ↦ X) (limit F'))
          x) :
      (fun (X : Type v) ↦ X) (F'.obj j))
    ((hom (FC := TypeCat.Fun) (s.π.app j) :
          (a : (fun (X : Type v) ↦ X) (((Functor.const J).obj s.pt).obj j)) → (fun (X : Type v) ↦ X) (F'.obj j))
        x :
      (fun (X : Type v) ↦ X) (F'.obj j))

Tactic:
limit.lift_π_apply _ _ _

Premises used: CategoryTheory.Limits.limit.lift_π_apply
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F' G' : Functor.{w, v, v, v + 1} J (Type v)
α : F' ⟶ G'
j : J
x : limit F'
⊢ Eq (α := (fun (X : Type v) ↦ X) (G'.obj j))
    ((hom (FC := TypeCat.Fun) (limit.π G' j) :
          (a : (fun (X : Type v) ↦ X) (limit G')) → (fun (X : Type v) ↦ X) (G'.obj j))
        ((hom (FC := TypeCat.Fun) (limMap α) :
            (a : (fun (X : Type v) ↦ X) (limit F')) → (fun (X : Type v) ↦ X) (limit G'))
          x) :
      (fun (X : Type v) ↦ X) (G'.obj j))
    ((hom (FC := TypeCat.Fun) (α.app j) : (a : (fun (X : Type v) ↦ X) (F'.obj j)) → (fun (X : Type v) ↦ X) (G'.obj j))
        ((hom (FC := TypeCat.Fun) (limit.π F' j) :
            (a : (fun (X : Type v) ↦ X) (limit F')) → (fun (X : Type v) ↦ X) (F'.obj j))
          x) :
      (fun (X : Type v) ↦ X) (G'.obj j))

Tactic:
limMap_π_apply _ _ _

Premises used: CategoryTheory.Limits.limMap_π_apply
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
⊢ HasLimitsOfSize.{w, w, max v w, max (v + 1) (w + 1)} (Type (max w v))

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
⊢ HasLimitsOfSize.{w, w, max v w, max (v + 1) (w + 1)} (Type (max v w))

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
⊢ HasLimitsOfSize.{0, 0, v, v + 1} (Type v)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
⊢ HasLimitsOfSize.{v, v, v, v + 1} (Type v)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Types.Limits
Goal:
J : Type v
inst : Category.{w, v} J
inst_1 : UnivLE.{v, u}
⊢ HasLimitsOfSize.{v, v, u, u + 1} (Type u)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
Goal:
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
x : d.multispan.ColimitType
left :
  ∀ (l : J.L) (z : d.multispan.obj (WalkingMultispan.left l)),
    ∃ (i : J.R) (a : d.right i),
      d.multispan.ιColimitType (WalkingMultispan.right i) a = d.multispan.ιColimitType (WalkingMultispan.left l) z
right :
  ∀ (r : J.R) (z : d.multispan.obj (WalkingMultispan.right r)),
    ∃ (i : J.R) (a : d.right i),
      d.multispan.ιColimitType (WalkingMultispan.right i) a = d.multispan.ιColimitType (WalkingMultispan.right r) z
⊢ ∃ (i : J.R) (a : d.right i), d.multispan.ιColimitType (WalkingMultispan.right i) a = x

Tactic:
obtain ⟨(l | r), z, rfl⟩ := d.multispan.ιColimitType_jointly_surjective x

Premises used: CategoryTheory.Functor.ιColimitType_jointly_surjective, CategoryTheory.Limits.MultispanIndex.multispan, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
Goal:
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
l : J.L
z : d.multispan.obj (WalkingMultispan.left l)
rw rw₁ : d.multispan.ιColimitType (WalkingMultispan.left l) z = d.multispan.ιColimitType (WalkingMultispan.left l) z
⊢ d.multispan.ιColimitType (WalkingMultispan.right (J.fst l))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (d.multispan.map (WalkingMultispan.Hom.fst l)) :
          (a : (fun (X : Type u) ↦ X) (d.multispan.obj (WalkingMultispan.left l))) →
            (fun (X : Type u) ↦ X) (d.multispan.obj (WalkingMultispan.right (J.fst l))))
        z) =
    d.multispan.ιColimitType (WalkingMultispan.left l) z

Tactic:
rw [ιColimitType_map]

Premises used: CategoryTheory.Functor.ιColimitType_map
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
Goal:
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
l : J.L
z : d.multispan.obj (WalkingMultispan.left l)
⊢ ∃ (i : J.R) (a : d.right i),
    d.multispan.ιColimitType (WalkingMultispan.right i) a = d.multispan.ιColimitType (WalkingMultispan.left l) z

Tactic:
exact ⟨J.fst l, d.multispan.map (WalkingMultispan.Hom.fst l) z, by rw [ιColimitType_map]⟩