awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
e : Equivalence.{v₂, v₁, u₂, u₁} K J
inst_3 : HasLimit F
⊢ HasLimit (e.functor ⋙ F)

Tactic:
HasLimit.mk
    { cone := Cone.whisker e.functor (limit.cone F)
      isLimit := IsLimit.whiskerEquivalence (limit.isLimit F) e }

Premises used: CategoryTheory.Limits.limit.cone, CategoryTheory.Equivalence.functor, CategoryTheory.Limits.IsLimit.whiskerEquivalence, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.Cone.whisker, CategoryTheory.Limits.LimitCone.mk
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
e : Equivalence.{v₂, v₁, u₂, u₁} K J
inst_3 : HasLimit (e.functor ⋙ F)
⊢ HasLimit (e.inverse ⋙ e.functor ⋙ F)

Tactic:
haveI : HasLimit (e.inverse ⋙ e.functor ⋙ F) := Limits.hasLimit_equivalence_comp e.symm
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
e : Equivalence.{v₂, v₁, u₂, u₁} K J
inst_3 : HasLimit (e.functor ⋙ F)
this : HasLimit (e.inverse ⋙ e.functor ⋙ F)
⊢ HasLimit F

Tactic:
apply hasLimit_of_iso (e.invFunIdAssoc F)

Premises used: CategoryTheory.Limits.hasLimit_of_iso, CategoryTheory.Equivalence.invFunIdAssoc
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
e : Equivalence.{v₂, v₁, u₂, u₁} K J
⊢ HasLimit (e.functor ⋙ F) ↔ HasLimit F

Tactic:
⟨fun _ ↦ hasLimit_of_equivalence_comp e, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro, CategoryTheory.Limits.hasLimit_of_equivalence_comp
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
e : Equivalence.{v₁, v₂, u₁, u₂} J K
⊢ HasLimit (e.inverse ⋙ F) ↔ HasLimit F

Tactic:
hasLimit_equivalence_comp_iff e.symm

Premises used: CategoryTheory.Limits.hasLimit_equivalence_comp_iff, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F_1 : Functor.{v₁, v, u₁, u} J C
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
F : Functor.{v₁, v, u₁, u} J C
w : ∀ (j : J), CategoryStruct.comp (Y := limit F) (limMap (𝟙 F)) (limit.π F j) = 𝟙 (limit F) ≫ limit.π F j
⊢ limMap (𝟙 F) = 𝟙 (limit F)

Tactic:
apply Limits.limit.hom_ext

Premises used: CategoryTheory.Limits.limit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F_1 : Functor.{v₁, v, u₁, u} J C
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
F : Functor.{v₁, v, u₁, u} J C
j : J
⊢ CategoryStruct.comp (Y := limit F) (limMap (𝟙 F)) (limit.π F j) = 𝟙 (limit F) ≫ limit.π F j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
X Y Z : Functor.{v₁, v, u₁, u} J C
α : X ⟶ Y
β : Y ⟶ Z
w :
  ∀ (j : J),
    Eq (α := limit X ⟶ Z.obj j) (CategoryStruct.comp (Y := limit Z) (limMap (α ≫ β)) (limit.π Z j))
      (CategoryStruct.comp (Y := limit Z) (CategoryStruct.comp (Y := limit Y) (limMap α) (limMap β)) (limit.π Z j))
⊢ Eq (α := limit X ⟶ limit Z) (limMap (α ≫ β)) (CategoryStruct.comp (Y := limit Y) (limMap α) (limMap β))

Tactic:
apply Limits.limit.hom_ext

Premises used: CategoryTheory.Limits.limit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
X Y Z : Functor.{v₁, v, u₁, u} J C
α : X ⟶ Y
β : Y ⟶ Z
j : J
⊢ Eq (α := limit X ⟶ Z.obj j) (CategoryStruct.comp (Y := limit Z) (limMap (α ≫ β)) (limit.π Z j))
    (CategoryStruct.comp (Y := limit Z) (CategoryStruct.comp (Y := limit Y) (limMap α) (limMap β)) (limit.π Z j))

Tactic:
simp [assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_2 : HasLimitsOfShape.{v₁, u₁, v, u} J C
G : Functor.{v₁, v, u₁, u} J C
α : F ⟶ G
⊢ Eq (α := limit F ⟶ limit G) (limMap α) (map lim α)

Tactic:
rfl

Premises used: CategoryTheory.Limits.IsLimit.map, CategoryTheory.Limits.limMap, rfl
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
G : Functor.{v₁, v, u₁, u} J C
α : F ⟶ G
inst_4 : HasLimitsOfShape.{v₂, u₂, v, u} K C
E : Functor.{v₂, v₁, u₂, u₁} K J
w :
  ∀ (j : K),
    Eq (α := obj lim F ⟶ (E ⋙ G).obj j) (CategoryStruct.comp (Y := limit (E ⋙ G)) (map lim α ≫ pre G E) (π (E ⋙ G) j))
      (CategoryStruct.comp (Y := limit (E ⋙ G))
        (CategoryStruct.comp (Y := limit (E ⋙ F)) (pre F E) (map lim (E.whiskerLeft α))) (π (E ⋙ G) j))
⊢ Eq (α := obj lim F ⟶ limit (E ⋙ G)) (map lim α ≫ pre G E)
    (CategoryStruct.comp (Y := limit (E ⋙ F)) (pre F E) (map lim (E.whiskerLeft α)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
G : Functor.{v₁, v, u₁, u} J C
α : F ⟶ G
inst_4 : HasLimitsOfShape.{v₂, u₂, v, u} K C
E : Functor.{v₂, v₁, u₂, u₁} K J
j : K
⊢ Eq (α := obj lim F ⟶ (E ⋙ G).obj j) (CategoryStruct.comp (Y := limit (E ⋙ G)) (map lim α ≫ pre G E) (π (E ⋙ G) j))
    (CategoryStruct.comp (Y := limit (E ⋙ G))
      (CategoryStruct.comp (Y := limit (E ⋙ F)) (pre F E) (map lim (E.whiskerLeft α))) (π (E ⋙ G) j))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
inst_4 : HasLimitsOfShape.{v₂, u₂, v, u} K C
F : Functor.{v₁, v, u₁, u} J C
E₁ E₂ : Functor.{v₂, v₁, u₂, u₁} K J
α : E₁ ⟶ E₂
w :
  ∀ (j : K),
    Eq (α := limit F ⟶ (E₂ ⋙ F).obj j) (CategoryStruct.comp (Y := limit (E₂ ⋙ F)) (pre F E₂) (π (E₂ ⋙ F) j))
      (CategoryStruct.comp (Y := limit (E₂ ⋙ F))
        (CategoryStruct.comp (Y := limit (E₁ ⋙ F)) (pre F E₁) (map lim (whiskerRight α F))) (π (E₂ ⋙ F) j))
⊢ Eq (α := limit F ⟶ limit (E₂ ⋙ F)) (pre F E₂)
    (CategoryStruct.comp (Y := limit (E₁ ⋙ F)) (pre F E₁) (map lim (whiskerRight α F)))

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
inst_4 : HasLimitsOfShape.{v₂, u₂, v, u} K C
F : Functor.{v₁, v, u₁, u} J C
E₁ E₂ : Functor.{v₂, v₁, u₂, u₁} K J
α : E₁ ⟶ E₂
j : K
⊢ Eq (α := limit F ⟶ (E₂ ⋙ F).obj j) (CategoryStruct.comp (Y := limit (E₂ ⋙ F)) (pre F E₂) (π (E₂ ⋙ F) j))
    (CategoryStruct.comp (Y := limit (E₂ ⋙ F))
      (CategoryStruct.comp (Y := limit (E₁ ⋙ F)) (pre F E₁) (map lim (whiskerRight α F))) (π (E₂ ⋙ F) j))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_2 : HasLimitsOfShape.{v₁, u₁, v, u} J C
G : Functor.{v₁, v, u₁, u} J C
α : F ⟶ G
D : Type u'
inst_3 : Category.{v', u'} D
inst_4 : HasLimitsOfShape.{v₁, u₁, v', u'} J D
H : Functor.{v, v', u, u'} C D
w :
  ∀ (j : J),
    Eq (α := H.obj (limit F) ⟶ (G ⋙ H).obj j)
      (CategoryStruct.comp (Y := limit (G ⋙ H))
        (CategoryStruct.comp (Y := H.obj (limit G)) (H.map (limMap α)) (post G H)) (π (G ⋙ H) j))
      (CategoryStruct.comp (Y := limit (G ⋙ H))
        (CategoryStruct.comp (Y := limit (F ⋙ H)) (post F H) (limMap (whiskerRight α H))) (π (G ⋙ H) j))
⊢ Eq (α := H.obj (limit F) ⟶ limit (G ⋙ H)) (CategoryStruct.comp (Y := H.obj (limit G)) (H.map (limMap α)) (post G H))
    (CategoryStruct.comp (Y := limit (F ⋙ H)) (post F H) (limMap (whiskerRight α H)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_2 : HasLimitsOfShape.{v₁, u₁, v, u} J C
G : Functor.{v₁, v, u₁, u} J C
α : F ⟶ G
D : Type u'
inst_3 : Category.{v', u'} D
inst_4 : HasLimitsOfShape.{v₁, u₁, v', u'} J D
H : Functor.{v, v', u, u'} C D
j : J
⊢ Eq (α := H.obj (limit F) ⟶ (G ⋙ H).obj j)
    (CategoryStruct.comp (Y := limit (G ⋙ H)) (CategoryStruct.comp (Y := H.obj (limit G)) (H.map (limMap α)) (post G H))
      (π (G ⋙ H) j))
    (CategoryStruct.comp (Y := limit (G ⋙ H))
      (CategoryStruct.comp (Y := limit (F ⋙ H)) (post F H) (limMap (whiskerRight α H))) (π (G ⋙ H) j))

Tactic:
simp only [whiskerRight_app, limMap_π, assoc, limit.post_π_assoc, limit.post_π, ← H.map_comp]

Premises used: CategoryTheory.Limits.limMap_π, CategoryTheory.Category.assoc, CategoryTheory.Limits.limit.post_π, CategoryTheory.Limits.limit.post_π_assoc, CategoryTheory.Functor.whiskerRight_app, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
G : Functor.{v₁, v, u₁, u} J C
α : F ⟶ G
⊢ IsRightAdjoint (C := C) (D := Functor.{v₁, v, u₁, u} J C) lim

Tactic:
⟨_, ⟨constLimAdj⟩⟩

Premises used: Nonempty.intro, Exists.intro, CategoryTheory.Limits.constLimAdj, CategoryTheory.Functor.IsRightAdjoint.mk
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F_1 F G : Functor.{v₁, v, u₁, u} J C
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
α : F ⟶ G
inst_4 : Mono α
⊢ Mono (X := limit F) (Y := limit G) (limMap α)

Tactic:
(lim : (J ⥤ C) ⥤ C).map_mono α

Premises used: CategoryTheory.Limits.lim, CategoryTheory.Functor.map_mono, CategoryTheory.Limits.limit, CategoryTheory.Limits.IsLimit.map, CategoryTheory.Limits.limMap
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F_1 F G : Functor.{v₁, v, u₁, u} J C
inst_3 : HasLimit F
inst_4 : HasLimit G
α : F ⟶ G
inst_5 : ∀ (j : J), Mono (α.app j)
Z : C
u v : Z ⟶ limit F
h : Eq (α := Z ⟶ limit G) (u ≫ limMap α) (v ≫ limMap α)
j : J
⊢ (u ≫ limit.π F j) ≫ α.app j = (v ≫ limit.π F j) ≫ α.app j

Tactic:
simpa using h =≫ limit.π _ j

Premises used: CategoryTheory.Limits.limit.π
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F_1 : Functor.{v₁, v, u₁, u} J C
L : Functor.{v₁, v, u₁, u} J C ⥤ C
adj : const J ⊣ L
F : Functor.{v₁, v, u₁, u} J C
s : Cone F
j : J
⊢ (map (L ⋙ const J) s.π ≫ adj.counit.app F).app j =
    (adj.counit.app (obj (const J) s.pt) ≫ map (𝟭 (Functor.{v₁, v, u₁, u} J C)) s.π).app j

Tactic:
have eq := NatTrans.congr_app (adj.counit.naturality s.π) j
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F_1 : Functor.{v₁, v, u₁, u} J C
L : Functor.{v₁, v, u₁, u} J C ⥤ C
adj : const J ⊣ L
F : Functor.{v₁, v, u₁, u} J C
s : Cone F
j : J
eq :
  (map (L ⋙ const J) s.π ≫ adj.counit.app F).app j =
    (adj.counit.app (obj (const J) s.pt) ≫ map (𝟭 (Functor.{v₁, v, u₁, u} J C)) s.π).app j
⊢ Eq (α := obj.{v₁, v, u₁, u} (obj (const J) s.pt) j ⟶ obj.{v₁, v, u₁, u} (obj (const J) s.pt) j)
    (NatTrans.app (map (const J) (adj.unit.app s.pt) ≫ adj.counit.app (obj (const J) s.pt)) j)
    (NatTrans.app (𝟙 (obj (const J) s.pt)) j)

Tactic:
have eq' := NatTrans.congr_app (adj.left_triangle_components s.pt) j
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F_1 : Functor.{v₁, v, u₁, u} J C
L : Functor.{v₁, v, u₁, u} J C ⥤ C
adj : const J ⊣ L
F : Functor.{v₁, v, u₁, u} J C
s : Cone F
j : J
eq :
  (map (L ⋙ const J) s.π ≫ adj.counit.app F).app j =
    (adj.counit.app (obj (const J) s.pt) ≫ map (𝟭 (Functor.{v₁, v, u₁, u} J C)) s.π).app j
eq' :
  Eq (α := obj.{v₁, v, u₁, u} (obj (const J) s.pt) j ⟶ obj.{v₁, v, u₁, u} (obj (const J) s.pt) j)
    (NatTrans.app (map (const J) (adj.unit.app s.pt) ≫ adj.counit.app (obj (const J) s.pt)) j)
    (NatTrans.app (𝟙 (obj (const J) s.pt)) j)
dsimp : (adj.homEquiv s.pt F : (a : (const J).obj s.pt ⟶ F) → s.pt ⟶ L.obj F) s.π ≫ (adj.counit.app F).app j = s.π.app j
⊢ (adj.homEquiv s.pt F : (a : (const J).obj s.pt ⟶ F) → s.pt ⟶ L.obj F) s.π ≫ (coneOfAdj adj F).π.app j = s.π.app j

Tactic:
dsimp at eq eq' ⊢
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F_1 : Functor.{v₁, v, u₁, u} J C
L : Functor.{v₁, v, u₁, u} J C ⥤ C
adj : const J ⊣ L
F : Functor.{v₁, v, u₁, u} J C
s : Cone F
j : J
eq : L.map s.π ≫ (adj.counit.app F).app j = NatTrans.app (adj.counit.app (obj (const J) s.pt)) j ≫ s.π.app j
eq' : adj.unit.app s.pt ≫ NatTrans.app (adj.counit.app (obj (const J) s.pt)) j = 𝟙 s.pt
rw : (adj.unit.app s.pt ≫ L.map s.π) ≫ (adj.counit.app F).app j = s.π.app j
rw₁ : adj.unit.app s.pt ≫ L.map s.π ≫ (adj.counit.app F).app j = s.π.app j
rw₂ : adj.unit.app s.pt ≫ NatTrans.app (adj.counit.app (obj (const J) s.pt)) j ≫ s.π.app j = s.π.app j
rw₃ rw₄ : s.π.app j = s.π.app j
⊢ (adj.homEquiv s.pt F : (a : (const J).obj s.pt ⟶ F) → s.pt ⟶ L.obj F) s.π ≫ (adj.counit.app F).app j = s.π.app j

Tactic:
rw [adj.homEquiv_unit, assoc, eq, reassoc_of% eq']

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Adjunction.homEquiv_unit
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F_1 : Functor.{v₁, v, u₁, u} J C
L : Functor.{v₁, v, u₁, u} J C ⥤ C
adj : const J ⊣ L
F : Functor.{v₁, v, u₁, u} J C
s : Cone F
m : s.pt ⟶ (coneOfAdj adj F).pt
hm : ∀ (j : J), m ≫ (coneOfAdj adj F).π.app j = s.π.app j
w :
  ∀ (j : J),
    Eq.{v + 1} (α := obj.{v₁, v, u₁, u} (obj (const J) s.pt) j ⟶ F.obj j)
      (NatTrans.app ((Equiv.symm (adj.homEquiv s.pt F) : (a : s.pt ⟶ L.obj F) → (const J).obj s.pt ⟶ F) m) j)
      (NatTrans.app
        ((Equiv.symm (adj.homEquiv s.pt F) : (a : s.pt ⟶ L.obj F) → (const J).obj s.pt ⟶ F)
          ((adj.homEquiv s.pt F : (a : (const J).obj s.pt ⟶ F) → s.pt ⟶ L.obj F) s.π))
        j)
⊢ Eq (α := obj (const J) s.pt ⟶ F)
    ((Equiv.symm (adj.homEquiv s.pt F) : (a : s.pt ⟶ L.obj F) → (const J).obj s.pt ⟶ F) m : obj (const J) s.pt ⟶ F)
    ((Equiv.symm (adj.homEquiv s.pt F) : (a : s.pt ⟶ L.obj F) → (const J).obj s.pt ⟶ F)
        ((adj.homEquiv s.pt F : (a : (const J).obj s.pt ⟶ F) → s.pt ⟶ L.obj F) s.π) :
      obj (const J) s.pt ⟶ F)

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F_1 : Functor.{v₁, v, u₁, u} J C
L : Functor.{v₁, v, u₁, u} J C ⥤ C
adj : const J ⊣ L
F : Functor.{v₁, v, u₁, u} J C
s : Cone F
m : s.pt ⟶ (coneOfAdj adj F).pt
hm : ∀ (j : J), m ≫ (coneOfAdj adj F).π.app j = s.π.app j
j : J
⊢ Eq.{v + 1} (α := obj.{v₁, v, u₁, u} (obj (const J) s.pt) j ⟶ F.obj j)
    (NatTrans.app ((Equiv.symm (adj.homEquiv s.pt F) : (a : s.pt ⟶ L.obj F) → (const J).obj s.pt ⟶ F) m) j)
    (NatTrans.app
      ((Equiv.symm (adj.homEquiv s.pt F) : (a : s.pt ⟶ L.obj F) → (const J).obj s.pt ⟶ F)
        ((adj.homEquiv s.pt F : (a : (const J).obj s.pt ⟶ F) → s.pt ⟶ L.obj F) s.π))
      j)

Tactic:
simpa using hm j
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
J' : Type u₂
inst_2 : Category.{v₂, u₂} J'
e : Equivalence.{v₁, v₂, u₁, u₂} J J'
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
has_limit : autoParam (∀ (F : Functor.{v₂, v, u₂, u} J' C), HasLimit F) HasLimitsOfShape.has_limit._autoParam
⊢ HasLimitsOfShape.{v₂, u₂, v, u} J' C

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
J' : Type u₂
inst_2 : Category.{v₂, u₂} J'
e : Equivalence.{v₁, v₂, u₁, u₂} J J'
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
F : Functor.{v₂, v, u₂, u} J' C
⊢ HasLimit F

Tactic:
apply hasLimit_of_equivalence_comp e

Premises used: CategoryTheory.Limits.hasLimit_of_equivalence_comp
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimitsOfSize.{v₁, u₁, v, u} C
J : Type u₂
inst_2 : Category.{v₂, u₂} J
inst_3 : Small.{u₁, u₂} J
inst_4 : LocallySmall.{v₁, v₂, u₂} J
⊢ HasLimitsOfShape.{v₁, u₁, v, u} (ShrinkHoms.{u₁} (Shrink.{u₁, u₂} J)) C

Tactic:
have := HasLimitsOfSize.has_limits_of_shape (C := C) (ShrinkHoms (Shrink.{u₁} J))
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimitsOfSize.{v₁, u₁, v, u} C
J : Type u₂
inst_2 : Category.{v₂, u₂} J
inst_3 : Small.{u₁, u₂} J
inst_4 : LocallySmall.{v₁, v₂, u₂} J
this : HasLimitsOfShape.{v₁, u₁, v, u} (ShrinkHoms.{u₁} (Shrink.{u₁, u₂} J)) C
⊢ HasLimitsOfShape.{v₂, u₂, v, u} J C

Tactic:
hasLimitsOfShape_of_equivalence
    ((ShrinkHoms.equivalence _).symm.trans (Shrink.equivalence _).symm)

Premises used: CategoryTheory.Limits.hasLimitsOfShape_of_equivalence, CategoryTheory.ShrinkHoms.equivalence, CategoryTheory.Shrink.equivalence, CategoryTheory.Equivalence.trans, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimitsOfSize.{v₁, u₁, v, u} C
J : Type u₂
inst_2 : Category.{v₂, u₂} J
inst_3 : Small.{u₁, u₂} J
inst_4 : LocallySmall.{v₁, v₂, u₂} J
this : HasLimitsOfShape.{v₁, u₁, v, u} (ShrinkHoms.{u₁} (Shrink.{u₁, u₂} J)) C
⊢ HasLimitsOfShape.{v₂, u₂, v, u} J C

Tactic:
exact hasLimitsOfShape_of_equivalence
    ((ShrinkHoms.equivalence _).symm.trans (Shrink.equivalence _).symm)

Premises used: CategoryTheory.Limits.hasLimitsOfShape_of_equivalence, CategoryTheory.ShrinkHoms.equivalence, CategoryTheory.Shrink.equivalence, CategoryTheory.Equivalence.trans, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimitsOfSize.{v₁, u₁, v, u} C
J : Type u₂
inst_2 : Category.{v₂, u₂} J
inst_3 : EssentiallySmall.{u₁, v₂, u₂} J
inst_4 : LocallySmall.{v₁, v₂, u₂} J
⊢ HasLimitsOfShape.{u₁, u₁, v, u} (SmallModel.{u₁, v₂, u₂} J) C

Tactic:
have := HasLimitsOfShape.of_small.{v₁, u₁} C (SmallModel.{u₁} J)
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimitsOfSize.{v₁, u₁, v, u} C
J : Type u₂
inst_2 : Category.{v₂, u₂} J
inst_3 : EssentiallySmall.{u₁, v₂, u₂} J
inst_4 : LocallySmall.{v₁, v₂, u₂} J
this : HasLimitsOfShape.{u₁, u₁, v, u} (SmallModel.{u₁, v₂, u₂} J) C
⊢ HasLimitsOfShape.{v₂, u₂, v, u} J C

Tactic:
hasLimitsOfShape_of_equivalence (equivSmallModel.{u₁} J).symm

Premises used: CategoryTheory.Limits.hasLimitsOfShape_of_equivalence, CategoryTheory.Equivalence.symm, CategoryTheory.equivSmallModel
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimitsOfSize.{v₁, u₁, v, u} C
J : Type u₂
inst_2 : Category.{v₂, u₂} J
inst_3 : EssentiallySmall.{u₁, v₂, u₂} J
inst_4 : LocallySmall.{v₁, v₂, u₂} J
this : HasLimitsOfShape.{u₁, u₁, v, u} (SmallModel.{u₁, v₂, u₂} J) C
⊢ HasLimitsOfShape.{v₂, u₂, v, u} J C

Tactic:
exact hasLimitsOfShape_of_equivalence (equivSmallModel.{u₁} J).symm
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimitsOfSize.{max v₁ v₂, max u₁ u₂, v, u} C
⊢ HasLimitsOfSize.{v₁, u₁, v, u} C

Tactic:
hasLimitsOfSizeOfUnivLE.{max v₁ v₂, max u₁ u₂} C

Premises used: CategoryTheory.Limits.hasLimitsOfSizeOfUnivLE
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_3 : HasLimits.{v, u} C
⊢ HasLimitsOfSize.{0, 0, v, u} C

Tactic:
hasLimitsOfSizeShrink.{0, 0} C

Premises used: CategoryTheory.Limits.hasLimitsOfSizeShrink
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
d : ColimitCocone F
⊢ HasColimit F

Tactic:
⟨Nonempty.intro d⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.HasColimit.mk'
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimits.{v, u} C
J : Type v
inst_2 : Category.{v, v} J
⊢ HasColimitsOfShape J C

Tactic:
HasColimitsOfSize.has_colimits_of_shape J

Premises used: CategoryTheory.Limits.HasColimitsOfSize.has_colimits_of_shape
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J_1 : Type u₁
inst : Category.{v₁, u₁} J_1
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F_1 : Functor.{v₁, v, u₁, u} J_1 C
J : Type u₁
inst_3 : Category.{v₁, u₁} J
inst_4 : HasColimitsOfShape.{v₁, u₁, v, u} J C
F : Functor.{v₁, v, u₁, u} J C
⊢ HasColimit F

Tactic:
HasColimitsOfShape.has_colimit F

Premises used: CategoryTheory.Limits.HasColimitsOfShape.has_colimit
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J_1 : Type u₁
inst : Category.{v₁, u₁} J_1
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J_1 C
J : Type u₁
inst_3 : Category.{v₁, u₁} J
inst_4 : HasColimitsOfSize.{v₁, u₁, v, u} C
⊢ HasColimitsOfShape.{v₁, u₁, v, u} J C

Tactic:
HasColimitsOfSize.has_colimits_of_shape J

Premises used: CategoryTheory.Limits.HasColimitsOfSize.has_colimits_of_shape
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F_1 F : Functor.{v₁, v, u₁, u} J C
inst_3 : HasColimit F
j j' : J
hj : j = j'
subst : F.obj j = F.obj j
⊢ F.obj j' = F.obj j

Tactic:
subst hj
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
F_1 F : Functor.{v₁, v, u₁, u} J C
inst_3 : HasColimit F
j : J
⊢ F.obj j = F.obj j

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_2 : HasColimit F
j j' : J
hj : j = j'
subst : Eq (α := F.obj j ⟶ colimit F) (eqToHom ⋯ ≫ ι F j) (ι F j)
⊢ Eq (α := F.obj j' ⟶ colimit F) (eqToHom ⋯ ≫ ι F j) (ι F j')

Tactic:
subst hj
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
F : Functor.{v₁, v, u₁, u} J C
inst_2 : HasColimit F
j : J
⊢ Eq (α := F.obj j ⟶ colimit F) (eqToHom ⋯ ≫ ι F j) (ι F j)

Tactic:
simp