awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasColimit F
G : Functor.{v, v', u, u'} C D
inst_4 : HasColimit (F ⋙ G)
E : Type u''
inst_5 : Category.{v'', u''} E
H : Functor.{v', v'', u', u''} D E
h : HasColimit ((F ⋙ G) ⋙ H)
j : J
w :
  Eq (α := ((F ⋙ G) ⋙ H).obj j ⟶ H.obj (G.obj (colimit F))) (H.map (G.map (ι F j)))
    (CategoryStruct.comp (Y := colimit ((F ⋙ G) ⋙ H)) (ι ((F ⋙ G) ⋙ H) j) (post F (G ⋙ H)))
⊢ Eq (α := ((F ⋙ G) ⋙ H).obj j ⟶ H.obj (G.obj (colimit F)))
    (CategoryStruct.comp (Y := colimit ((F ⋙ G) ⋙ H)) (ι ((F ⋙ G) ⋙ H) j)
      (CategoryStruct.comp (Y := H.obj (colimit (F ⋙ G))) (post (F ⋙ G) H) (H.map (post F G))))
    (CategoryStruct.comp (Y := colimit ((F ⋙ G) ⋙ H)) (ι ((F ⋙ G) ⋙ H) j) (post F (G ⋙ H)))

Tactic:
rw [← assoc, colimit.ι_post, ← H.map_comp, colimit.ι_post]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.colimit.ι_post, CategoryTheory.Functor.map_comp
-- 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 : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasColimit F
G : Functor.{v, v', u, u'} C D
inst_4 : HasColimit (F ⋙ G)
E : Type u''
inst_5 : Category.{v'', u''} E
H : Functor.{v', v'', u', u''} D E
h : HasColimit ((F ⋙ G) ⋙ H)
j : J
⊢ HasColimit (F ⋙ G ⋙ H)

Tactic:
haveI : HasColimit (F ⋙ G ⋙ H) := h
-- 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 : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasColimit F
G : Functor.{v, v', u, u'} C D
inst_4 : HasColimit (F ⋙ G)
E : Type u''
inst_5 : Category.{v'', u''} E
H : Functor.{v', v'', u', u''} D E
h : HasColimit ((F ⋙ G) ⋙ H)
j : J
this : HasColimit (F ⋙ G ⋙ H)
⊢ Eq (α := ((F ⋙ G) ⋙ H).obj j ⟶ H.obj (G.obj (colimit F))) (H.map (G.map (ι F j)))
    (CategoryStruct.comp (Y := colimit ((F ⋙ G) ⋙ H)) (ι ((F ⋙ G) ⋙ H) j) (post F (G ⋙ H)))

Tactic:
(colimit.ι_post F (G ⋙ H) j).symm

Premises used: CategoryTheory.Limits.colimit.ι_post, CategoryTheory.Functor.comp, Eq.symm
-- 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 : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasColimit F
G : Functor.{v, v', u, u'} C D
inst_4 : HasColimit (F ⋙ G)
E : Type u''
inst_5 : Category.{v'', u''} E
H : Functor.{v', v'', u', u''} D E
h : HasColimit ((F ⋙ G) ⋙ H)
j : J
this : HasColimit (F ⋙ G ⋙ H)
⊢ Eq (α := ((F ⋙ G) ⋙ H).obj j ⟶ H.obj (G.obj (colimit F))) (H.map (G.map (ι F j)))
    (CategoryStruct.comp (Y := colimit ((F ⋙ G) ⋙ H)) (ι ((F ⋙ G) ⋙ H) j) (post F (G ⋙ H)))

Tactic:
exact (colimit.ι_post F (G ⋙ H) j).symm

Premises used: CategoryTheory.Limits.colimit.ι_post, CategoryTheory.Functor.comp, Eq.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
D : Type u'
inst_3 : Category.{v', u'} D
E : Functor.{v₂, v₁, u₂, u₁} K J
F : Functor.{v₁, v, u₁, u} J C
G : Functor.{v, v', u, u'} C D
inst_4 : HasColimit F
inst_5 : HasColimit (E ⋙ F)
inst_6 : HasColimit (F ⋙ G)
h : HasColimit ((E ⋙ F) ⋙ G)
w :
  ∀ (j : K),
    Eq (α := ((E ⋙ F) ⋙ G).obj j ⟶ G.obj (colimit F))
      (CategoryStruct.comp (Y := colimit ((E ⋙ F) ⋙ G)) (ι ((E ⋙ F) ⋙ G) j)
        (CategoryStruct.comp (Y := G.obj (colimit (E ⋙ F))) (post (E ⋙ F) G) (G.map (pre F E))))
      (CategoryStruct.comp (Y := colimit ((E ⋙ F) ⋙ G)) (ι ((E ⋙ F) ⋙ G) j)
        (CategoryStruct.comp (Y := colimit (F ⋙ G)) (pre (F ⋙ G) E) (post F G)))
⊢ Eq (α := colimit ((E ⋙ F) ⋙ G) ⟶ G.obj (colimit F))
    (CategoryStruct.comp (Y := G.obj (colimit (E ⋙ F))) (post (E ⋙ F) G) (G.map (pre F E)))
    (CategoryStruct.comp (Y := colimit (F ⋙ G)) (pre (F ⋙ G) E) (post F G))

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
D : Type u'
inst_3 : Category.{v', u'} D
E : Functor.{v₂, v₁, u₂, u₁} K J
F : Functor.{v₁, v, u₁, u} J C
G : Functor.{v, v', u, u'} C D
inst_4 : HasColimit F
inst_5 : HasColimit (E ⋙ F)
inst_6 : HasColimit (F ⋙ G)
h : HasColimit ((E ⋙ F) ⋙ G)
j : K
w :
  Eq (α := ((E ⋙ F) ⋙ G).obj j ⟶ G.obj (colimit F)) (G.map (ι F (E.obj j)))
    (CategoryStruct.comp (Y := colimit (F ⋙ G))
      (CategoryStruct.comp (Y := colimit ((E ⋙ F) ⋙ G)) (ι ((E ⋙ F) ⋙ G) j) (pre (F ⋙ G) E)) (post F G))
⊢ Eq (α := ((E ⋙ F) ⋙ G).obj j ⟶ G.obj (colimit F))
    (CategoryStruct.comp (Y := colimit ((E ⋙ F) ⋙ G)) (ι ((E ⋙ F) ⋙ G) j)
      (CategoryStruct.comp (Y := G.obj (colimit (E ⋙ F))) (post (E ⋙ F) G) (G.map (pre F E))))
    (CategoryStruct.comp (Y := colimit ((E ⋙ F) ⋙ G)) (ι ((E ⋙ F) ⋙ G) j)
      (CategoryStruct.comp (Y := colimit (F ⋙ G)) (pre (F ⋙ G) E) (post F G)))

Tactic:
rw [← assoc, colimit.ι_post, ← G.map_comp, colimit.ι_pre, ← assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.colimit.ι_post, CategoryTheory.Limits.colimit.ι_pre, 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
D : Type u'
inst_3 : Category.{v', u'} D
E : Functor.{v₂, v₁, u₂, u₁} K J
F : Functor.{v₁, v, u₁, u} J C
G : Functor.{v, v', u, u'} C D
inst_4 : HasColimit F
inst_5 : HasColimit (E ⋙ F)
inst_6 : HasColimit (F ⋙ G)
h : HasColimit ((E ⋙ F) ⋙ G)
j : K
⊢ HasColimit (E ⋙ F ⋙ G)

Tactic:
haveI : HasColimit (E ⋙ F ⋙ G) := h
-- 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
D : Type u'
inst_3 : Category.{v', u'} D
E : Functor.{v₂, v₁, u₂, u₁} K J
F : Functor.{v₁, v, u₁, u} J C
G : Functor.{v, v', u, u'} C D
inst_4 : HasColimit F
inst_5 : HasColimit (E ⋙ F)
inst_6 : HasColimit (F ⋙ G)
h : HasColimit ((E ⋙ F) ⋙ G)
j : K
this : HasColimit (E ⋙ F ⋙ G)
w :
  Eq (α := ((E ⋙ F) ⋙ G).obj j ⟶ G.obj (colimit F)) (G.map (ι F (E.obj j)))
    (CategoryStruct.comp (Y := colimit (F ⋙ G)) (ι (F ⋙ G) (E.obj j)) (post F G))
w₁ w₂ : Eq (α := ((E ⋙ F) ⋙ G).obj j ⟶ G.obj (colimit F)) (G.map (ι F (E.obj j))) (G.map (ι F (E.obj j)))
⊢ Eq (α := ((E ⋙ F) ⋙ G).obj j ⟶ G.obj (colimit F)) (G.map (ι F (E.obj j)))
    (CategoryStruct.comp (Y := colimit (F ⋙ G))
      (CategoryStruct.comp (Y := colimit ((E ⋙ F) ⋙ G)) (ι ((E ⋙ F) ⋙ G) j) (pre (F ⋙ G) E)) (post F G))

Tactic:
erw [colimit.ι_pre (F ⋙ G) E j, colimit.ι_post]

Premises used: CategoryTheory.Limits.colimit.ι_post, CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.ι_pre
-- 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 : HasColimit F
⊢ HasColimit (e.functor ⋙ F)

Tactic:
HasColimit.mk
    { cocone := Cocone.whisker e.functor (colimit.cocone F)
      isColimit := IsColimit.whiskerEquivalence (colimit.isColimit F) e }

Premises used: CategoryTheory.Limits.IsColimit.whiskerEquivalence, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.Cocone.whisker, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Equivalence.functor, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.colimit.cocone
-- 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 : HasColimit (e.functor ⋙ F)
⊢ HasColimit (e.inverse ⋙ e.functor ⋙ F)

Tactic:
haveI : HasColimit (e.inverse ⋙ e.functor ⋙ F) := Limits.hasColimit_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 : HasColimit (e.functor ⋙ F)
this : HasColimit (e.inverse ⋙ e.functor ⋙ F)
⊢ HasColimit F

Tactic:
apply hasColimit_of_iso (e.invFunIdAssoc F).symm

Premises used: CategoryTheory.Limits.hasColimit_of_iso, CategoryTheory.Iso.symm, 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
⊢ HasColimit (e.functor ⋙ F) ↔ HasColimit F

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

Premises used: CategoryTheory.Limits.hasColimit_of_equivalence_comp, inferInstance, Iff.intro
-- 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
⊢ HasColimit (e.inverse ⋙ F) ↔ HasColimit F

Tactic:
hasColimit_equivalence_comp_iff e.symm

Premises used: CategoryTheory.Limits.hasColimit_equivalence_comp_iff, CategoryTheory.Equivalence.symm
-- 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 : HasColimitsOfShape.{v₁, u₁, v, u} J C
G : Functor.{v₁, v, u₁, u} J C
α : F ⟶ G
⊢ Eq (α := colimit F ⟶ colimit G) (colimMap α) (map colim α)

Tactic:
rfl

Premises used: CategoryTheory.Limits.colimMap, CategoryTheory.Limits.IsColimit.map, 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 : HasColimitsOfShape.{v₁, u₁, v, u} J C
G : Functor.{v₁, v, u₁, u} J C
α : F ⟶ G
j : J
⊢ Eq (α := F.obj j ⟶ obj colim G) (CategoryStruct.comp (Y := colimit F) (ι F j) (map colim α)) (α.app j ≫ ι G 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 : HasColimitsOfShape.{v₁, u₁, v, u} J C
G : Functor.{v₁, v, u₁, u} J C
α : F ⟶ G
c : Cocone G
w :
  ∀ (j : J),
    CategoryStruct.comp (Y := colimit F) (ι F j) (CategoryStruct.comp (Y := colimit G) (colimMap α) (desc G c)) =
      CategoryStruct.comp (Y := colimit F) (ι F j) (desc F ((Cocone.precompose α).obj c))
⊢ Eq (α := colimit F ⟶ c.pt) (CategoryStruct.comp (Y := colimit G) (colimMap α) (desc G c))
    (desc F ((Cocone.precompose α).obj c))

Tactic:
ext j
-- 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 : HasColimitsOfShape.{v₁, u₁, v, u} J C
G : Functor.{v₁, v, u₁, u} J C
α : F ⟶ G
c : Cocone G
j : J
⊢ CategoryStruct.comp (Y := colimit F) (ι F j) (CategoryStruct.comp (Y := colimit G) (colimMap α) (desc G c)) =
    CategoryStruct.comp (Y := colimit F) (ι F j) (desc F ((Cocone.precompose α).obj c))

Tactic:
simp [colimit.ι_desc, colimit.ι_desc]

Premises used: CategoryTheory.Limits.colimit.ι_desc
-- 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 : HasColimitsOfShape.{v₁, u₁, v, u} J C
G : Functor.{v₁, v, u₁, u} J C
α : F ⟶ G
inst_4 : HasColimitsOfShape.{v₂, u₂, v, u} K C
E : Functor.{v₂, v₁, u₂, u₁} K J
w :
  ∀ (j : K),
    Eq (α := (E ⋙ F).obj j ⟶ obj colim G)
      (CategoryStruct.comp (Y := colimit (E ⋙ F)) (ι (E ⋙ F) j)
        (CategoryStruct.comp (Y := colimit F) (pre F E) (map colim α)))
      (CategoryStruct.comp (Y := colimit (E ⋙ F)) (ι (E ⋙ F) j) (map colim (E.whiskerLeft α) ≫ pre G E))
⊢ Eq (α := colimit (E ⋙ F) ⟶ obj colim G) (CategoryStruct.comp (Y := colimit F) (pre F E) (map colim α))
    (map colim (E.whiskerLeft α) ≫ pre G E)

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 : HasColimitsOfShape.{v₁, u₁, v, u} J C
G : Functor.{v₁, v, u₁, u} J C
α : F ⟶ G
inst_4 : HasColimitsOfShape.{v₂, u₂, v, u} K C
E : Functor.{v₂, v₁, u₂, u₁} K J
j : K
w : Eq (α := (E ⋙ F).obj j ⟶ obj colim G) (α.app (E.obj j) ≫ ι G (E.obj j)) ((E.whiskerLeft α).app j ≫ ι G (E.obj j))
⊢ Eq (α := (E ⋙ F).obj j ⟶ obj colim G)
    (CategoryStruct.comp (Y := colimit (E ⋙ F)) (ι (E ⋙ F) j)
      (CategoryStruct.comp (Y := colimit F) (pre F E) (map colim α)))
    (CategoryStruct.comp (Y := colimit (E ⋙ F)) (ι (E ⋙ F) j) (map colim (E.whiskerLeft α) ≫ pre G E))

Tactic:
rw [← assoc, colimit.ι_pre, colimit.ι_map, ← assoc, colimit.ι_map, assoc, colimit.ι_pre]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.colimit.ι_map, CategoryTheory.Limits.colimit.ι_pre
-- 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 : HasColimitsOfShape.{v₁, u₁, v, u} J C
G : Functor.{v₁, v, u₁, u} J C
α : F ⟶ G
inst_4 : HasColimitsOfShape.{v₂, u₂, v, u} K C
E : Functor.{v₂, v₁, u₂, u₁} K J
j : K
⊢ Eq (α := (E ⋙ F).obj j ⟶ obj colim G) (α.app (E.obj j) ≫ ι G (E.obj j)) ((E.whiskerLeft α).app j ≫ ι G (E.obj j))

Tactic:
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
inst_3 : HasColimitsOfShape.{v₁, u₁, v, u} J C
inst_4 : HasColimitsOfShape.{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 (α := (E₁ ⋙ F).obj j ⟶ colimit F) (CategoryStruct.comp (Y := colimit (E₁ ⋙ F)) (ι (E₁ ⋙ F) j) (pre F E₁))
      (CategoryStruct.comp (Y := colimit (E₁ ⋙ F)) (ι (E₁ ⋙ F) j) (map colim (whiskerRight α F) ≫ pre F E₂))
⊢ Eq (α := colimit (E₁ ⋙ F) ⟶ colimit F) (pre F E₁) (map colim (whiskerRight α F) ≫ pre F E₂)

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 : HasColimitsOfShape.{v₁, u₁, v, u} J C
inst_4 : HasColimitsOfShape.{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 (α := (E₁ ⋙ F).obj j ⟶ colimit F) (CategoryStruct.comp (Y := colimit (E₁ ⋙ F)) (ι (E₁ ⋙ F) j) (pre F E₁))
    (CategoryStruct.comp (Y := colimit (E₁ ⋙ F)) (ι (E₁ ⋙ F) j) (map colim (whiskerRight α F) ≫ pre F E₂))

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 : HasColimitsOfShape.{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 : HasColimitsOfShape.{v₁, u₁, v', u'} J D
H : Functor.{v, v', u, u'} C D
w :
  ∀ (j : J),
    Eq (α := (F ⋙ H).obj j ⟶ H.obj (obj colim G))
      (CategoryStruct.comp (Y := colimit (F ⋙ H)) (ι (F ⋙ H) j)
        (CategoryStruct.comp (Y := H.obj (colimit F)) (post F H) (H.map (map colim α))))
      (CategoryStruct.comp (Y := colimit (F ⋙ H)) (ι (F ⋙ H) j) (map colim (whiskerRight α H) ≫ post G H))
⊢ Eq (α := colimit (F ⋙ H) ⟶ H.obj (obj colim G))
    (CategoryStruct.comp (Y := H.obj (colimit F)) (post F H) (H.map (map colim α)))
    (map colim (whiskerRight α H) ≫ post G 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 : HasColimitsOfShape.{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 : HasColimitsOfShape.{v₁, u₁, v', u'} J D
H : Functor.{v, v', u, u'} C D
j : J
w :
  Eq (α := (F ⋙ H).obj j ⟶ H.obj (obj colim G)) (H.map (α.app j) ≫ H.map (ι G j))
    (CategoryStruct.comp (Y := colimit (F ⋙ H)) (ι (F ⋙ H) j) (map colim (whiskerRight α H) ≫ post G H))
⊢ Eq (α := (F ⋙ H).obj j ⟶ H.obj (obj colim G))
    (CategoryStruct.comp (Y := colimit (F ⋙ H)) (ι (F ⋙ H) j)
      (CategoryStruct.comp (Y := H.obj (colimit F)) (post F H) (H.map (map colim α))))
    (CategoryStruct.comp (Y := colimit (F ⋙ H)) (ι (F ⋙ H) j) (map colim (whiskerRight α H) ≫ post G H))

Tactic:
rw [← assoc, colimit.ι_post, ← H.map_comp, colimit.ι_map, H.map_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.colimit.ι_map, CategoryTheory.Limits.colimit.ι_post, CategoryTheory.Functor.map_comp
-- 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 : HasColimitsOfShape.{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 : HasColimitsOfShape.{v₁, u₁, v', u'} J D
H : Functor.{v, v', u, u'} C D
j : J
w :
  Eq (α := (F ⋙ H).obj j ⟶ H.obj (obj colim G)) (H.map (α.app j) ≫ H.map (ι G j))
    ((whiskerRight α H).app j ≫ H.map (ι G j))
⊢ Eq (α := (F ⋙ H).obj j ⟶ H.obj (obj colim G)) (H.map (α.app j) ≫ H.map (ι G j))
    (CategoryStruct.comp (Y := colimit (F ⋙ H)) (ι (F ⋙ H) j) (map colim (whiskerRight α H) ≫ post G H))

Tactic:
rw [← assoc, colimit.ι_map, assoc, colimit.ι_post]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.colimit.ι_map, CategoryTheory.Limits.colimit.ι_post
-- 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 : HasColimitsOfShape.{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 : HasColimitsOfShape.{v₁, u₁, v', u'} J D
H : Functor.{v, v', u, u'} C D
j : J
⊢ Eq (α := (F ⋙ H).obj j ⟶ H.obj (obj colim G)) (H.map (α.app j) ≫ H.map (ι G j))
    ((whiskerRight α H).app j ≫ H.map (ι G j))

Tactic:
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 : HasColimitsOfShape.{v₁, u₁, v, u} J C
G : Functor.{v₁, v, u₁, u} J C
α : F ⟶ G
⊢ IsLeftAdjoint (C := Functor.{v₁, v, u₁, u} J C) colim

Tactic:
⟨_, ⟨colimConstAdj⟩⟩

Premises used: Nonempty.intro, Exists.intro, CategoryTheory.Functor.IsLeftAdjoint.mk, CategoryTheory.Limits.colimConstAdj
-- 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 : HasColimitsOfShape.{v₁, u₁, v, u} J C
α : F ⟶ G
inst_4 : Epi α
⊢ Epi (X := colimit F) (Y := colimit G) (colimMap α)

Tactic:
(colim : (J ⥤ C) ⥤ C).map_epi α

Premises used: CategoryTheory.Limits.colim, CategoryTheory.Functor.map_epi, CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimMap, CategoryTheory.Limits.IsColimit.map
-- 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 : HasColimit F
inst_4 : HasColimit G
α : F ⟶ G
inst_5 : ∀ (j : J), Epi (α.app j)
Z : C
u v : colimit G ⟶ Z
h : Eq (α := colimit F ⟶ Z) (colimMap α ≫ u) (colimMap α ≫ v)
j : J
⊢ α.app j ≫ colimit.ι G j ≫ u = α.app j ≫ colimit.ι G j ≫ v

Tactic:
simpa using colimit.ι _ j ≫= h

Premises used: CategoryTheory.Limits.colimit.ι
-- 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 : HasColimitsOfShape.{v₁, u₁, v, u} J C
has_colimit : autoParam (∀ (F : Functor.{v₂, v, u₂, u} J' C), HasColimit F) HasColimitsOfShape.has_colimit._autoParam
⊢ HasColimitsOfShape.{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 : HasColimitsOfShape.{v₁, u₁, v, u} J C
F : Functor.{v₂, v, u₂, u} J' C
⊢ HasColimit F

Tactic:
apply hasColimit_of_equivalence_comp e

Premises used: CategoryTheory.Limits.hasColimit_of_equivalence_comp
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimitsOfSize.{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
⊢ HasColimitsOfShape.{v₁, u₁, v, u} (ShrinkHoms.{u₁} (Shrink.{u₁, u₂} J)) C

Tactic:
have := HasColimitsOfSize.has_colimits_of_shape (C := C) (ShrinkHoms (Shrink.{u₁} J))
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimitsOfSize.{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 : HasColimitsOfShape.{v₁, u₁, v, u} (ShrinkHoms.{u₁} (Shrink.{u₁, u₂} J)) C
⊢ HasColimitsOfShape.{v₂, u₂, v, u} J C

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

Premises used: CategoryTheory.Limits.hasColimitsOfShape_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 : HasColimitsOfSize.{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 : HasColimitsOfShape.{v₁, u₁, v, u} (ShrinkHoms.{u₁} (Shrink.{u₁, u₂} J)) C
⊢ HasColimitsOfShape.{v₂, u₂, v, u} J C

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

Premises used: CategoryTheory.Limits.hasColimitsOfShape_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 : HasColimitsOfSize.{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
⊢ HasColimitsOfShape.{u₁, u₁, v, u} (SmallModel.{u₁, v₂, u₂} J) C

Tactic:
have := HasColimitsOfShape.of_small.{v₁, u₁} C (SmallModel.{u₁} J)
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimitsOfSize.{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 : HasColimitsOfShape.{u₁, u₁, v, u} (SmallModel.{u₁, v₂, u₂} J) C
⊢ HasColimitsOfShape.{v₂, u₂, v, u} J C

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

Premises used: CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, CategoryTheory.Equivalence.symm, CategoryTheory.equivSmallModel
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimitsOfSize.{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 : HasColimitsOfShape.{u₁, u₁, v, u} (SmallModel.{u₁, v₂, u₂} J) C
⊢ HasColimitsOfShape.{v₂, u₂, v, u} J C

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