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
inst_2 : HasColimit F
j : J
⊢ (cocone F).ι.app j = ι F j

Tactic:
rfl

Premises used: rfl, 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
F : Functor.{v₁, v, u₁, u} J C
inst_2 : HasColimit F
⊢ (cocone F).pt = colimit F

Tactic:
rfl

Premises used: CategoryTheory.Limits.colimit, 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
f : j ⟶ j'
⊢ Eq (α := F.obj j ⟶ colimit F) (F.map f ≫ ι F j') (ι F j)

Tactic:
(colimit.cocone F).w f

Premises used: CategoryTheory.Limits.colimit, CategoryTheory.Limits.Cocone.w, CategoryTheory.Limits.colimit.cocone, 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
F : Functor.{v₁, v, u₁, u} J C
inst_2 : HasColimit F
c : Cocone F
⊢ Eq (α := (cocone F).pt ⟶ c.pt) (IsColimit.desc (isColimit F) c) (desc F c)

Tactic:
rfl

Premises used: CategoryTheory.Limits.colimit.desc, 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
c : Cocone F
j : J
⊢ CategoryStruct.comp (Y := colimit F) (ι F j) (desc F c) = c.ι.app j

Tactic:
IsColimit.fac _ c j

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimit.desc, 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
F G : Functor.{v₁, v, u₁, u} J C
inst_2 : HasColimit F
inst_3 : HasColimit G
α : F ⟶ G
j : J
⊢ Eq (α := F.obj j ⟶ colimit G) (CategoryStruct.comp (Y := colimit F) (colimit.ι F j) (colimMap α))
    (α.app j ≫ colimit.ι G j)

Tactic:
colimit.ι_desc _ j

Premises used: CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimit.ι_desc, CategoryTheory.Limits.colimit.desc, CategoryTheory.Limits.colimMap, CategoryTheory.Limits.IsColimit.map, 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
F : Functor.{v₁, v, u₁, u} J C
inst_2 : HasColimit F
c : Cocone F
⊢ Eq (α := (cocone F).pt ⟶ c.pt) (CoconeMorphism.hom (coconeMorphism c)) (desc F c)

Tactic:
rfl

Premises used: CategoryTheory.Limits.colimit.desc, 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
c : Cocone F
j : J
⊢ CategoryStruct.comp (Y := colimit F) (ι F j) (CoconeMorphism.hom (coconeMorphism c)) = c.ι.app 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 : HasColimit F
c : Cocone F
hc : IsColimit c
j : J
⊢ CategoryStruct.comp (Y := colimit F) (ι F j) (Iso.hom (IsColimit.coconePointUniqueUpToIso (isColimit F) hc)) =
    c.ι.app j

Tactic:
IsColimit.comp_coconePointUniqueUpToIso_hom _ _ _

Premises used: CategoryTheory.Limits.colimit, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, 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
F : Functor.{v₁, v, u₁, u} J C
inst_2 : HasColimit F
c : Cocone F
hc : IsColimit c
j : J
⊢ CategoryStruct.comp (Y := colimit F) (ι F j) (Iso.inv (hc.coconePointUniqueUpToIso (isColimit F))) = c.ι.app j

Tactic:
IsColimit.comp_coconePointUniqueUpToIso_inv _ _ _

Premises used: CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv, CategoryTheory.Limits.colimit, 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
F : Functor.{v₁, v, u₁, u} J C
inst_2 : HasColimit F
t : Cocone F
⊢ ∃! d : colimit F ⟶ t.pt, ∀ (j : J), ι F j ≫ d = t.ι.app j

Tactic:
(colimit.isColimit F).existsUnique _

Premises used: CategoryTheory.Limits.IsColimit.existsUnique, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.colimit, 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
F : Functor.{v₁, v, u₁, u} J C
inst_2 : HasColimit F
t : ColimitCocone F
j : J
dsimp : CategoryStruct.comp (Y := colimit F) (ι F j) (desc F t.cocone) = t.cocone.ι.app j
⊢ CategoryStruct.comp (Y := colimit F) (ι F j) (Iso.hom (isoColimitCocone t)) = t.cocone.ι.app j

Tactic:
dsimp [colimit.isoColimitCocone, IsColimit.coconePointUniqueUpToIso]

Premises used: CategoryTheory.Limits.colimit.isoColimitCocone, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- 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
t : ColimitCocone F
j : J
⊢ CategoryStruct.comp (Y := colimit F) (ι F j) (desc F t.cocone) = t.cocone.ι.app 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 : HasColimit F
t : ColimitCocone F
j : J
dsimp : Eq (α := F.obj j ⟶ colimit F) (t.cocone.ι.app j ≫ t.isColimit.desc (cocone F)) (ι F j)
⊢ Eq (α := F.obj j ⟶ colimit F) (t.cocone.ι.app j ≫ Iso.inv (isoColimitCocone t)) (ι F j)

Tactic:
dsimp [colimit.isoColimitCocone, IsColimit.coconePointUniqueUpToIso]

Premises used: CategoryTheory.Limits.colimit.isoColimitCocone, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- 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
t : ColimitCocone F
j : J
⊢ Eq (α := F.obj j ⟶ colimit F) (t.cocone.ι.app j ≫ t.isColimit.desc (cocone F)) (ι 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 : HasColimit F
X : C
f f' : colimit F ⟶ X
w : ∀ (j : J), ι F j ≫ f = ι F j ≫ f'
⊢ f = f'

Tactic:
(colimit.isColimit F).hom_ext w

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Limits.colimit.isColimit, 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
F : Functor.{v₁, v, u₁, u} J C
inst_2 : HasColimit F
⊢ desc F (cocone F) = 𝟙 (colimit F)

Tactic:
(colimit.isColimit _).desc_self

Premises used: CategoryTheory.Limits.IsColimit.desc_self, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimit.desc
-- 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
W : C
⊢ Eq (α := ULift.{u₁, v} (colimit F ⟶ W) ⟶ F.cocones.obj W) (Iso.hom (homIso F W))
    (↾fun (f : ULift.{u₁, v} (colimit F ⟶ W)) ↦ (cocone F).ι ≫ map (const J) f.down)

Tactic:
(colimit.isColimit F).homIso_hom

Premises used: CategoryTheory.Limits.IsColimit.homIso_hom, CategoryTheory.Limits.colimit.isColimit, 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
F : Functor.{v₁, v, u₁, u} J C
inst_2 : HasColimit F
c : Cocone F
X : C
f : c.pt ⟶ X
w :
  ∀ (j : J),
    CategoryStruct.comp (Y := colimit F) (ι F j) (desc F (c.extend f)) =
      CategoryStruct.comp (Y := colimit F) (ι F j) (desc F c ≫ f)
⊢ Eq (α := colimit F ⟶ (c.extend f).pt) (desc F (c.extend f)) (desc F c ≫ f)

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 : HasColimit F
c : Cocone F
X : C
f : c.pt ⟶ X
j : J
⊢ CategoryStruct.comp (Y := colimit F) (ι F j) (desc F (c.extend f)) =
    CategoryStruct.comp (Y := colimit F) (ι F j) (desc F c ≫ f)

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 G : Functor.{v₁, v, u₁, u} J C
inst_2 : HasColimit F
α : G ≅ F
⊢ HasColimit G

Tactic:
HasColimit.mk
    { cocone := (Cocone.precompose α.hom).obj (colimit.cocone F)
      isColimit := (IsColimit.precomposeHomEquiv _ _).symm (colimit.isColimit F) }

Premises used: CategoryTheory.Limits.Cocone.precompose, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.colimit.cocone, Equiv.symm, CategoryTheory.Iso.hom, DFunLike.coe, CategoryTheory.Limits.IsColimit.precomposeHomEquiv, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
F G : Functor.{v₁, v, u₁, u} J C
α : F ≅ G
⊢ HasColimit F ↔ HasColimit G

Tactic:
⟨fun _ ↦ hasColimit_of_iso α.symm, fun _ ↦ hasColimit_of_iso α⟩

Premises used: CategoryTheory.Limits.hasColimit_of_iso, Iff.intro, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
K : Type u₁
inst_2 : Category.{v₂, u₁} K
F : Functor.{v₁, v, u₁, u} J C
G : Functor.{v₂, v, u₁, u} K C
h : F.cocones ≅ G.cocones
inst_3 : HasColimit F
⊢ HasColimit G

Tactic:
HasColimit.mk ⟨_, IsColimit.ofCorepresentableBy ((colimit.isColimit F).corepresentableBy.ofIso h)⟩

Premises used: CategoryTheory.Limits.IsColimit.ofCorepresentableBy, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.IsColimit.corepresentableBy, CategoryTheory.Functor.CorepresentableBy.ofIso
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
F G : Functor.{v₁, v, u₁, u} J C
inst_2 : HasColimit F
inst_3 : HasColimit G
w : F ≅ G
j : J
⊢ Eq (α := F.obj j ⟶ colimit G) (CategoryStruct.comp (Y := colimit F) (colimit.ι F j) (Iso.hom (isoOfNatIso w)))
    (w.hom.app j ≫ colimit.ι G j)

Tactic:
IsColimit.comp_coconePointsIsoOfNatIso_hom _ _ _ _

Premises used: CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_hom, CategoryTheory.Limits.colimit, 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
F G : Functor.{v₁, v, u₁, u} J C
inst_2 : HasColimit F
inst_3 : HasColimit G
w : F ≅ G
j : J
⊢ Eq (α := G.obj j ⟶ colimit F) (CategoryStruct.comp (Y := colimit G) (colimit.ι G j) (Iso.inv (isoOfNatIso w)))
    (w.inv.app j ≫ colimit.ι F j)

Tactic:
IsColimit.comp_coconePointsIsoOfNatIso_inv _ _ _ _

Premises used: CategoryTheory.Limits.colimit, CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_inv, 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
F G : Functor.{v₁, v, u₁, u} J C
inst_2 : HasColimit F
inst_3 : HasColimit G
t : Cocone G
w : F ≅ G
⊢ Eq (α := colimit F ⟶ t.pt) (CategoryStruct.comp (Y := colimit G) (Iso.hom (isoOfNatIso w)) (colimit.desc G t))
    (colimit.desc F ((Cocone.precompose w.hom).obj t))

Tactic:
IsColimit.coconePointsIsoOfNatIso_hom_desc _ _ _

Premises used: CategoryTheory.Limits.colimit, CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_hom_desc, CategoryTheory.Limits.colimit.desc, CategoryTheory.Limits.IsColimit.map
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
F G : Functor.{v₁, v, u₁, u} J C
inst_2 : HasColimit F
inst_3 : HasColimit G
t : Cocone F
w : F ≅ G
⊢ Eq (α := colimit G ⟶ t.pt) (CategoryStruct.comp (Y := colimit F) (Iso.inv (isoOfNatIso w)) (colimit.desc F t))
    (colimit.desc G ((Cocone.precompose w.inv).obj t))

Tactic:
IsColimit.coconePointsIsoOfNatIso_inv_desc _ _ _

Premises used: CategoryTheory.Limits.colimit, CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_inv_desc, CategoryTheory.Limits.colimit.desc, 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 : Functor.{v₁, v, u₁, u} J C
inst_3 : HasColimit F
G : Functor.{v₂, v, u₂, u} K C
inst_4 : HasColimit G
e : Equivalence.{v₁, v₂, u₁, u₂} J K
w : e.functor ⋙ G ≅ F
j : J
⊢ Eq (α := F.obj j ⟶ colimit G) (CategoryStruct.comp (Y := colimit F) (colimit.ι F j) (Iso.hom (isoOfEquivalence e w)))
    (F.map (e.unit.app j) ≫
      w.inv.app ((e.functor ⋙ e.inverse).obj j) ≫ colimit.ι G (e.functor.obj ((e.functor ⋙ e.inverse).obj j)))

Tactic:
simp [HasColimit.isoOfEquivalence]

Premises used: CategoryTheory.Limits.HasColimit.isoOfEquivalence
-- 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 : HasColimit F
G : Functor.{v₂, v, u₂, u} K C
inst_4 : HasColimit G
e : Equivalence.{v₁, v₂, u₁, u₂} J K
w : e.functor ⋙ G ≅ F
k : K
⊢ Eq (α := G.obj k ⟶ colimit F) (CategoryStruct.comp (Y := colimit G) (colimit.ι G k) (Iso.inv (isoOfEquivalence e w)))
    (G.map (e.counitInv.app k) ≫ w.hom.app (e.inverse.obj k) ≫ colimit.ι F (e.inverse.obj k))

Tactic:
simp [HasColimit.isoOfEquivalence, IsColimit.coconePointsIsoOfEquivalence_inv]

Premises used: CategoryTheory.Limits.HasColimit.isoOfEquivalence, CategoryTheory.Limits.IsColimit.coconePointsIsoOfEquivalence_inv
-- 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 : HasColimit F
E : Functor.{v₂, v₁, u₂, u₁} K J
inst_4 : HasColimit (E ⋙ F)
k : K
⊢ Eq (α := (E ⋙ F).obj k ⟶ colimit F) (CategoryStruct.comp (Y := colimit (E ⋙ F)) (ι (E ⋙ F) k) (pre F E))
    (ι F (E.obj k))

Tactic:
simp [colimit.pre]

Premises used: 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 : HasColimit F
E : Functor.{v₂, v₁, u₂, u₁} K J
inst_4 : HasColimit (E ⋙ F)
inst_5 : IsIso (X := colimit (E ⋙ F)) (Y := colimit F) (pre F E)
k : K
⊢ Eq (α := F.obj (E.obj k) ⟶ colimit (E ⋙ F)) (CategoryStruct.comp (Y := colimit F) (ι F (E.obj k)) (inv (pre F E)))
    (ι (E ⋙ F) k)

Tactic:
simp [IsIso.comp_inv_eq]

Premises used: CategoryTheory.IsIso.comp_inv_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 : Functor.{v₁, v, u₁, u} J C
inst_3 : HasColimit F
E : Functor.{v₂, v₁, u₂, u₁} K J
inst_4 : HasColimit (E ⋙ F)
c : Cocone F
w :
  ∀ (j : K),
    CategoryStruct.comp (Y := colimit (E ⋙ F)) (ι (E ⋙ F) j)
        (CategoryStruct.comp (Y := colimit F) (pre F E) (desc F c)) =
      CategoryStruct.comp (Y := colimit (E ⋙ F)) (ι (E ⋙ F) j) (desc (E ⋙ F) (Cocone.whisker E c))
⊢ Eq (α := colimit (E ⋙ F) ⟶ c.pt) (CategoryStruct.comp (Y := colimit F) (pre F E) (desc F c))
    (desc (E ⋙ F) (Cocone.whisker E c))

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 : HasColimit F
E : Functor.{v₂, v₁, u₂, u₁} K J
inst_4 : HasColimit (E ⋙ F)
c : Cocone F
j : K
⊢ CategoryStruct.comp (Y := colimit (E ⋙ F)) (ι (E ⋙ F) j) (CategoryStruct.comp (Y := colimit F) (pre F E) (desc F c)) =
    CategoryStruct.comp (Y := colimit (E ⋙ F)) (ι (E ⋙ F) j) (desc (E ⋙ F) (Cocone.whisker E c))

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

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

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

Premises used: CategoryTheory.Category.assoc, 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 : HasColimit F
E : Functor.{v₂, v₁, u₂, u₁} K J
inst_4 : HasColimit (E ⋙ F)
L : Type u₃
inst_5 : Category.{v₃, u₃} L
D : Functor.{v₃, v₂, u₃, u₂} L K
h : HasColimit (D ⋙ E ⋙ F)
j : L
⊢ HasColimit ((D ⋙ E) ⋙ F)

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

Tactic:
(colimit.ι_pre F (D ⋙ E) j).symm

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

Tactic:
exact (colimit.ι_pre F (D ⋙ E) j).symm

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.ι_pre, 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)
j : J
⊢ Eq (α := (F ⋙ G).obj j ⟶ G.obj (colimit F)) (CategoryStruct.comp (Y := colimit (F ⋙ G)) (ι (F ⋙ G) j) (post F G))
    (G.map (ι F j))

Tactic:
simp [colimit.post]

Premises used: 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
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)
c : Cocone F
w :
  ∀ (j : J),
    CategoryStruct.comp (Y := colimit (F ⋙ G)) (ι (F ⋙ G) j)
        (CategoryStruct.comp (Y := G.obj (colimit F)) (post F G) (G.map (desc F c))) =
      CategoryStruct.comp (Y := colimit (F ⋙ G)) (ι (F ⋙ G) j) (desc (F ⋙ G) (G.mapCocone c))
⊢ Eq (α := colimit (F ⋙ G) ⟶ G.obj c.pt) (CategoryStruct.comp (Y := G.obj (colimit F)) (post F G) (G.map (desc F c)))
    (desc (F ⋙ G) (G.mapCocone c))

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
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)
c : Cocone F
j : J
w : G.map (c.ι.app j) = (G.mapCocone c).ι.app j
⊢ CategoryStruct.comp (Y := colimit (F ⋙ G)) (ι (F ⋙ G) j)
      (CategoryStruct.comp (Y := G.obj (colimit F)) (post F G) (G.map (desc F c))) =
    CategoryStruct.comp (Y := colimit (F ⋙ G)) (ι (F ⋙ G) j) (desc (F ⋙ G) (G.mapCocone c))

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.colimit.ι_post, CategoryTheory.Limits.colimit.ι_desc, 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)
c : Cocone F
j : J
⊢ G.map (c.ι.app j) = (G.mapCocone c).ι.app 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
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)
w :
  ∀ (j : J),
    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)))
⊢ Eq (α := colimit ((F ⋙ G) ⋙ H) ⟶ H.obj (G.obj (colimit F)))
    (CategoryStruct.comp (Y := H.obj (colimit (F ⋙ G))) (post (F ⋙ G) H) (H.map (post F G))) (post F (G ⋙ H))

Tactic:
ext j