awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t : Cocone F
h : IsColimit t
W : C
f f' : t.pt ⟶ W
w : ∀ (j : J), t.ι.app j ≫ f = t.ι.app j ≫ f'
rw :
  Eq (α := t.pt ⟶ W)
    (h.desc { pt := W, ι := { app := fun (b : J) ↦ t.ι.app b ≫ f, naturality := ⋯ : NatTrans F (obj (const J) W) } } :
      t.pt ⟶
        { pt := W, ι := { app := fun (b : J) ↦ t.ι.app b ≫ f, naturality := ⋯ : NatTrans F (obj (const J) W) } :
            Cocone F }.pt)
    (h.desc { pt := W, ι := { app := fun (b : J) ↦ t.ι.app b ≫ f', naturality := ⋯ : NatTrans F (obj (const J) W) } })
⊢ f = f'

Tactic:
rw [h.hom_desc f, h.hom_desc f']

Premises used: CategoryTheory.Limits.IsColimit.hom_desc
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t : Cocone F
h : IsColimit t
W : C
f f' : t.pt ⟶ W
w : ∀ (j : J), t.ι.app j ≫ f = t.ι.app j ≫ f'
h₁ :
  Eq (α := (X : J) → F.obj X ⟶ obj.{v₁, v₃, u₁, u₃} (obj (const J) W) X) (fun (b : J) ↦ t.ι.app b ≫ f) fun (b : J) ↦
    t.ι.app b ≫ f'
⊢ Eq (α := t.pt ⟶ W)
    (h.desc { pt := W, ι := { app := fun (b : J) ↦ t.ι.app b ≫ f, naturality := ⋯ : NatTrans F (obj (const J) W) } } :
      t.pt ⟶
        { pt := W, ι := { app := fun (b : J) ↦ t.ι.app b ≫ f, naturality := ⋯ : NatTrans F (obj (const J) W) } :
            Cocone F }.pt)
    (h.desc { pt := W, ι := { app := fun (b : J) ↦ t.ι.app b ≫ f', naturality := ⋯ : NatTrans F (obj (const J) W) } })

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t : Cocone F
h : IsColimit t
W : C
f f' : t.pt ⟶ W
w : ∀ (j : J), t.ι.app j ≫ f = t.ι.app j ≫ f'
⊢ Eq (α := (X : J) → F.obj X ⟶ obj.{v₁, v₃, u₁, u₃} (obj (const J) W) X) (fun (b : J) ↦ t.ι.app b ≫ f) fun (b : J) ↦
    t.ι.app b ≫ f'

Tactic:
funext w

Premises used: funext
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t : Cocone F
h : IsColimit t
W : C
f f' : t.pt ⟶ W
w : ∀ (j : J), t.ι.app j ≫ f = t.ι.app j ≫ f'
⊢ Eq (α := (X : J) → F.obj X ⟶ obj.{v₁, v₃, u₁, u₃} (obj (const J) W) X) (fun (b : J) ↦ t.ι.app b ≫ f) fun (b : J) ↦
    t.ι.app b ≫ f'

Tactic:
exact funext w

Premises used: funext
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
s t : Cocone F
hs : IsColimit s
h : Nonempty (IsColimit t)
ht : IsColimit t
⊢ ∀ (j : J), s.ι.app j ≫ hs.desc t ≫ ht.desc s = s.ι.app j ≫ 𝟙 s.pt

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
s t : Cocone F
hs : IsColimit s
h : Nonempty (IsColimit t)
ht : IsColimit t
⊢ ∀ (j : J), t.ι.app j ≫ ht.desc s ≫ hs.desc t = t.ι.app j ≫ 𝟙 t.pt

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₂, v₄, u₂, u₄} K D
h : Cocone G ≌ Cocone F
c : Cocone G
P : IsColimit (h.functor.obj c)
s : Cocone G
⊢ desc ((ofCoconeEquiv h : (a : IsColimit (h.functor.obj c)) → IsColimit c) P) s =
    (h.unit.app c).hom ≫
      CoconeMorphism.hom (h.inverse.map (P.descCoconeMorphism (h.functor.obj s))) ≫ (h.unitInv.app s).hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₂, v₄, u₂, u₄} K D
h : Cocone G ≌ Cocone F
c : Cocone G
P : IsColimit c
s : Cocone F
⊢ desc ((Equiv.symm (ofCoconeEquiv h) : (a : IsColimit c) → IsColimit (h.functor.obj c)) P) s =
    CoconeMorphism.hom (h.functor.map (P.descCoconeMorphism (h.inverse.obj s))) ≫ (h.counit.app s).hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t_1 : Cocone F_1
F G : Functor.{v₁, v₃, u₁, u₃} J C
s : Cocone F
t : Cocone G
P : IsColimit s
Q : IsColimit t
w : F ≅ G
⊢ ∀ (j : J), s.ι.app j ≫ P.map t w.hom ≫ Q.map s w.inv = s.ι.app j ≫ 𝟙 s.pt

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t_1 : Cocone F_1
F G : Functor.{v₁, v₃, u₁, u₃} J C
s : Cocone F
t : Cocone G
P : IsColimit s
Q : IsColimit t
w : F ≅ G
⊢ ∀ (j : J), t.ι.app j ≫ Q.map s w.inv ≫ P.map t w.hom = t.ι.app j ≫ 𝟙 t.pt

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
s : Cocone F
t : Cocone G
P : IsColimit s
Q : IsColimit t
w : F ≅ G
j : J
⊢ s.ι.app j ≫ (P.coconePointsIsoOfNatIso Q w).hom = w.hom.app j ≫ t.ι.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
s : Cocone F
t : Cocone G
P : IsColimit s
Q : IsColimit t
w : F ≅ G
j : J
⊢ t.ι.app j ≫ (P.coconePointsIsoOfNatIso Q w).inv = w.inv.app j ≫ s.ι.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
s : Cocone F
r t : Cocone G
P : IsColimit s
Q : IsColimit t
w : F ≅ G
⊢ ∀ (j : J), s.ι.app j ≫ (P.coconePointsIsoOfNatIso Q w).hom ≫ Q.desc r = s.ι.app j ≫ P.map r w.hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
s : Cocone G
r t : Cocone F
P : IsColimit t
Q : IsColimit s
w : F ≅ G
⊢ ∀ (j : J), s.ι.app j ≫ (P.coconePointsIsoOfNatIso Q w).inv ≫ P.desc r = s.ι.app j ≫ Q.map r w.inv

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t_1 : Cocone F_1
F : Functor.{v₁, v₃, u₁, u₃} J C
s : Cocone F
G : Functor.{v₂, v₃, u₂, u₃} K C
t : Cocone G
P : IsColimit s
Q : IsColimit t
e : Equivalence.{v₁, v₂, u₁, u₂} J K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
apply :
  ∀ (j : J),
    s.ι.app j ≫
        CategoryStruct.comp (Y := t.pt)
          (P.desc ((Cocone.equivalenceOfReindexing e w).functor.obj t) :
            s.pt ⟶ ((Cocone.equivalenceOfReindexing e w).functor.obj t).pt)
          (Q.desc ((Cocone.equivalenceOfReindexing e.symm w').functor.obj s)) =
      s.ι.app j ≫ 𝟙 s.pt
⊢ CategoryStruct.comp (Y := t.pt)
      (P.desc ((Cocone.equivalenceOfReindexing e w).functor.obj t) :
        s.pt ⟶ ((Cocone.equivalenceOfReindexing e w).functor.obj t).pt)
      (Q.desc ((Cocone.equivalenceOfReindexing e.symm w').functor.obj s)) =
    𝟙 s.pt

Tactic:
apply hom_ext P

Premises used: CategoryTheory.Limits.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t_1 : Cocone F_1
F : Functor.{v₁, v₃, u₁, u₃} J C
s : Cocone F
G : Functor.{v₂, v₃, u₂, u₃} K C
t : Cocone G
P : IsColimit s
Q : IsColimit t
e : Equivalence.{v₁, v₂, u₁, u₂} J K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
j : J
dsimp :
  s.ι.app j ≫
      CategoryStruct.comp (Y := t.pt)
        (P.desc ((Cocone.precompose w.inv).obj (Cocone.whisker e.functor t)) :
          s.pt ⟶ ((Cocone.precompose w.inv).obj (Cocone.whisker e.functor t)).pt)
        (Q.desc
          ((Cocone.precompose ((e.invFunIdAssoc G).inv ≫ e.inverse.whiskerLeft w.hom)).obj
            (Cocone.whisker e.inverse s))) =
    s.ι.app j ≫ 𝟙 s.pt
⊢ s.ι.app j ≫
      CategoryStruct.comp (Y := t.pt)
        (P.desc ((Cocone.equivalenceOfReindexing e w).functor.obj t) :
          s.pt ⟶ ((Cocone.equivalenceOfReindexing e w).functor.obj t).pt)
        (Q.desc ((Cocone.equivalenceOfReindexing e.symm w').functor.obj s)) =
    s.ι.app j ≫ 𝟙 s.pt

Tactic:
dsimp [w']
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t_1 : Cocone F_1
F : Functor.{v₁, v₃, u₁, u₃} J C
s : Cocone F
G : Functor.{v₂, v₃, u₂, u₃} K C
t : Cocone G
P : IsColimit s
Q : IsColimit t
e : Equivalence.{v₁, v₂, u₁, u₂} J K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
j : J
simp :
  w.inv.app j ≫
      G.map (e.counitInv.app (e.functor.obj j)) ≫
        w.hom.app (e.inverse.obj (e.functor.obj j)) ≫ s.ι.app (e.inverse.obj (e.functor.obj j)) =
    s.ι.app j
⊢ s.ι.app j ≫
      CategoryStruct.comp (Y := t.pt)
        (P.desc ((Cocone.precompose w.inv).obj (Cocone.whisker e.functor t)) :
          s.pt ⟶ ((Cocone.precompose w.inv).obj (Cocone.whisker e.functor t)).pt)
        (Q.desc
          ((Cocone.precompose ((e.invFunIdAssoc G).inv ≫ e.inverse.whiskerLeft w.hom)).obj
            (Cocone.whisker e.inverse s))) =
    s.ι.app j ≫ 𝟙 s.pt

Tactic:
simp only [Limits.Cocone.whisker_ι, fac, invFunIdAssoc_inv_app, whiskerLeft_app, assoc,
        comp_id, Limits.Cocone.precompose_obj_ι, fac_assoc, NatTrans.comp_app]

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Category.assoc, CategoryTheory.Limits.Cocone.whisker_ι, CategoryTheory.Functor.whiskerLeft_app, CategoryTheory.Category.comp_id, CategoryTheory.Equivalence.invFunIdAssoc_inv_app, CategoryTheory.Limits.Cocone.precompose_obj_ι, CategoryTheory.NatTrans.comp_app, CategoryTheory.Limits.IsColimit.fac_assoc
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t_1 : Cocone F_1
F : Functor.{v₁, v₃, u₁, u₃} J C
s : Cocone F
G : Functor.{v₂, v₃, u₂, u₃} K C
t : Cocone G
P : IsColimit s
Q : IsColimit t
e : Equivalence.{v₁, v₂, u₁, u₂} J K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
j : J
rw :
  F.map (e.unit.app j) ≫
      w.inv.app ((e.functor ⋙ e.inverse).obj j) ≫
        w.hom.app (e.inverse.obj (e.functor.obj j)) ≫ s.ι.app (e.inverse.obj (e.functor.obj j)) =
    s.ι.app j
⊢ w.inv.app j ≫
      G.map (e.counitInv.app (e.functor.obj j)) ≫
        w.hom.app (e.inverse.obj (e.functor.obj j)) ≫ s.ι.app (e.inverse.obj (e.functor.obj j)) =
    s.ι.app j

Tactic:
rw [counitInv_app_functor, ← Functor.comp_map, ← w.inv.naturality_assoc]

Premises used: CategoryTheory.Equivalence.counitInv_app_functor, CategoryTheory.Iso.inv, CategoryTheory.Functor.comp_map, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t_1 : Cocone F_1
F : Functor.{v₁, v₃, u₁, u₃} J C
s : Cocone F
G : Functor.{v₂, v₃, u₂, u₃} K C
t : Cocone G
P : IsColimit s
Q : IsColimit t
e : Equivalence.{v₁, v₂, u₁, u₂} J K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
j : J
⊢ F.map (e.unit.app j) ≫
      w.inv.app ((e.functor ⋙ e.inverse).obj j) ≫
        w.hom.app (e.inverse.obj (e.functor.obj j)) ≫ s.ι.app (e.inverse.obj (e.functor.obj j)) =
    s.ι.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t_1 : Cocone F_1
F : Functor.{v₁, v₃, u₁, u₃} J C
s : Cocone F
G : Functor.{v₂, v₃, u₂, u₃} K C
t : Cocone G
P : IsColimit s
Q : IsColimit t
e : Equivalence.{v₁, v₂, u₁, u₂} J K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
apply :
  ∀ (j : K),
    t.ι.app j ≫
        CategoryStruct.comp (Y := s.pt)
          (Q.desc ((Cocone.equivalenceOfReindexing e.symm w').functor.obj s) :
            t.pt ⟶ ((Cocone.equivalenceOfReindexing e.symm w').functor.obj s).pt)
          (P.desc ((Cocone.equivalenceOfReindexing e w).functor.obj t)) =
      t.ι.app j ≫ 𝟙 t.pt
⊢ CategoryStruct.comp (Y := s.pt)
      (Q.desc ((Cocone.equivalenceOfReindexing e.symm w').functor.obj s) :
        t.pt ⟶ ((Cocone.equivalenceOfReindexing e.symm w').functor.obj s).pt)
      (P.desc ((Cocone.equivalenceOfReindexing e w).functor.obj t)) =
    𝟙 t.pt

Tactic:
apply hom_ext Q

Premises used: CategoryTheory.Limits.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t : Cocone F
h : IsColimit t
W : C
f : t.pt ⟶ W
⊢ ∀ (j : J),
    t.ι.app j ≫
        (fun (ι : F ⟶ obj (const J) W) ↦ (h.desc { pt := W, ι := ι } : t.pt ⟶ { pt := W, ι := ι : Cocone F }.pt))
          ((fun (f : t.pt ⟶ W) ↦ (t.extend f).ι) f) =
      t.ι.app j ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t : Cocone F
h : IsColimit t
W : C
f : t.pt ⟶ W
⊢ (h.homEquiv : (a : t.pt ⟶ W) → F ⟶ (const J).obj W) f = (t.extend f).ι

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, rfl
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t : Cocone F
h : IsColimit t
W : C
f : F ⟶ obj (const J) W
j : J
⊢ t.ι.app j ≫ (Equiv.symm h.homEquiv : (a : F ⟶ (const J).obj W) → t.pt ⟶ W) f = f.app j

Tactic:
simp [homEquiv]

Premises used: CategoryTheory.Limits.IsColimit.homEquiv
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t : Cocone F
h : IsColimit t
W W' : C
f : F ⟶ obj (const J) W
g : W ⟶ W'
⊢ Eq (α := F ⟶ obj (const J) W')
    ((h.homEquiv : (a : t.pt ⟶ W') → F ⟶ (const J).obj W')
        ((Equiv.symm h.homEquiv : (a : F ⟶ (const J).obj W') → t.pt ⟶ W') (f ≫ Functor.map (const J) g)) :
      F ⟶ obj (const J) W')
    ((h.homEquiv : (a : t.pt ⟶ W') → F ⟶ (const J).obj W')
        ((Equiv.symm h.homEquiv : (a : F ⟶ (const J).obj W) → t.pt ⟶ W) f ≫ g) :
      F ⟶ obj (const J) W')

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t : Cocone F
h : IsColimit t
W : C
⊢ (h.homIso W).hom = ↾fun (f : ULift.{u₁, v₃} (t.pt ⟶ W)) ↦ (t.extend f.down).ι

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, rfl
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t : Cocone F
h : IsColimit t
W : C
ι : F ⟶ obj (const J) W
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ ι.app j' = ι.app j ≫ Functor.map (obj (const J) W) f

Tactic:
ι.naturality f

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t : Cocone F
h : IsColimit t
W : C
ι : F ⟶ obj (const J) W
j j' : J
f : j ⟶ j'
h₁ :
  (F.obj j ⟶ obj.{v₁, v₃, u₁, u₃} (obj (const J) W) j') = (F.obj j ⟶ W) →
    ι.app j ≫ Functor.map (obj (const J) W) f = (fun (j : J) ↦ ι.app j) j
⊢ Eq (α := F.obj j ⟶ W) (F.map f ≫ (fun (j : J) ↦ ι.app j) j') ((fun (j : J) ↦ ι.app j) j)

Tactic:
convert! ← ι.naturality f

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t : Cocone F
h : IsColimit t
W : C
ι : F ⟶ obj (const J) W
j j' : J
f : j ⟶ j'
e_1 : (F.obj j ⟶ obj.{v₁, v₃, u₁, u₃} (obj (const J) W) j') = (F.obj j ⟶ W)
⊢ ι.app j ≫ Functor.map (obj (const J) W) f = (fun (j : J) ↦ ι.app j) j

Tactic:
apply comp_id

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t : Cocone F
h : IsColimit t
W : C
p : { p : (j : J) → F.obj j ⟶ W // ∀ {j j' : J} (f : j ⟶ j'), F.map f ≫ p j' = p j }
j j' : J
f : j ⟶ j'
dsimp : F.map f ≫ (↑p : (j : J) → F.obj j ⟶ W) j' = (↑p : (j : J) → F.obj j ⟶ W) j ≫ 𝟙 W
⊢ F.map f ≫ (↑p : (j : J) → F.obj j ⟶ W) j' = (↑p : (j : J) → F.obj j ⟶ W) j ≫ Functor.map (obj (const J) W) f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t : Cocone F
h : IsColimit t
W : C
p : { p : (j : J) → F.obj j ⟶ W // ∀ {j j' : J} (f : j ⟶ j'), F.map f ≫ p j' = p j }
j j' : J
f : j ⟶ j'
rw : F.map f ≫ (↑p : (j : J) → F.obj j ⟶ W) j' = (↑p : (j : J) → F.obj j ⟶ W) j
⊢ F.map f ≫ (↑p : (j : J) → F.obj j ⟶ W) j' = (↑p : (j : J) → F.obj j ⟶ W) j ≫ 𝟙 W

Tactic:
rw [comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t : Cocone F
h : IsColimit t
W : C
p : { p : (j : J) → F.obj j ⟶ W // ∀ {j j' : J} (f : j ⟶ j'), F.map f ≫ p j' = p j }
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ (↑p : (j : J) → F.obj j ⟶ W) j' = (↑p : (j : J) → F.obj j ⟶ W) j

Tactic:
p.2 f

Premises used: Subtype.property
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t : Cocone F
h : IsColimit t
W : C
p : { p : (j : J) → F.obj j ⟶ W // ∀ {j j' : J} (f : j ⟶ j'), F.map f ≫ p j' = p j }
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ (↑p : (j : J) → F.obj j ⟶ W) j' = (↑p : (j : J) → F.obj j ⟶ W) j

Tactic:
exact p.2 f

Premises used: Subtype.property
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t_1 t : Cocone F
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₃, v₄, u₃, u₄} C D
inst_4 : G.Faithful
ht : IsColimit (G.mapCocone t)
desc : (s : Cocone F) → t.pt ⟶ s.pt
h : ∀ (s : Cocone F), G.map (desc s) = ht.desc (G.mapCocone s)
s : Cocone F
j : J
a : G.map (t.ι.app j ≫ desc s) = G.map (s.ι.app j)
⊢ t.ι.app j ≫ desc s = s.ι.app j

Tactic:
apply G.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t_1 t : Cocone F
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₃, v₄, u₃, u₄} C D
inst_4 : G.Faithful
ht : IsColimit (G.mapCocone t)
desc : (s : Cocone F) → t.pt ⟶ s.pt
h : ∀ (s : Cocone F), G.map (desc s) = ht.desc (G.mapCocone s)
s : Cocone F
j : J
a : G.map (t.ι.app j) ≫ ht.desc (G.mapCocone s) = G.map (s.ι.app j)
⊢ G.map (t.ι.app j ≫ desc s) = G.map (s.ι.app j)

Tactic:
rw [G.map_comp, h]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t_1 t : Cocone F
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₃, v₄, u₃, u₄} C D
inst_4 : G.Faithful
ht : IsColimit (G.mapCocone t)
desc : (s : Cocone F) → t.pt ⟶ s.pt
h : ∀ (s : Cocone F), G.map (desc s) = ht.desc (G.mapCocone s)
s : Cocone F
j : J
⊢ G.map (t.ι.app j) ≫ ht.desc (G.mapCocone s) = G.map (s.ι.app j)

Tactic:
apply ht.fac

Premises used: CategoryTheory.Limits.IsColimit.fac
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t_1 t : Cocone F
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₃, v₄, u₃, u₄} C D
inst_4 : G.Faithful
ht : IsColimit (G.mapCocone t)
desc : (s : Cocone F) → t.pt ⟶ s.pt
h : ∀ (s : Cocone F), G.map (desc s) = ht.desc (G.mapCocone s)
s : Cocone F
m : t.pt ⟶ s.pt
w : ∀ (j : J), t.ι.app j ≫ m = s.ι.app j
a : G.map m = G.map (desc s)
⊢ m = desc s

Tactic:
apply G.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t_1 t : Cocone F
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₃, v₄, u₃, u₄} C D
inst_4 : G.Faithful
ht : IsColimit (G.mapCocone t)
desc : (s : Cocone F) → t.pt ⟶ s.pt
h : ∀ (s : Cocone F), G.map (desc s) = ht.desc (G.mapCocone s)
s : Cocone F
m : t.pt ⟶ s.pt
w : ∀ (j : J), t.ι.app j ≫ m = s.ι.app j
a : G.map m = ht.desc (G.mapCocone s)
⊢ G.map m = G.map (desc s)

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t_1 t : Cocone F
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₃, v₄, u₃, u₄} C D
inst_4 : G.Faithful
ht : IsColimit (G.mapCocone t)
desc : (s : Cocone F) → t.pt ⟶ s.pt
h : ∀ (s : Cocone F), G.map (desc s) = ht.desc (G.mapCocone s)
s : Cocone F
m : t.pt ⟶ s.pt
w : ∀ (j : J), t.ι.app j ≫ m = s.ι.app j
⊢ G.map m = ht.desc (G.mapCocone s)

Tactic:
ht.uniq (mapCocone G s) _ fun j => ?_

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.Limits.IsColimit.uniq
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
t_1 t : Cocone F
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₃, v₄, u₃, u₄} C D
inst_4 : G.Faithful
ht : IsColimit (G.mapCocone t)
desc : (s : Cocone F) → t.pt ⟶ s.pt
h : ∀ (s : Cocone F), G.map (desc s) = ht.desc (G.mapCocone s)
s : Cocone F
m : t.pt ⟶ s.pt
w : ∀ (j : J), t.ι.app j ≫ m = s.ι.app j
a : ∀ (j : J), (G.mapCocone t).ι.app j ≫ G.map m = (G.mapCocone s).ι.app j
⊢ G.map m = ht.desc (G.mapCocone s)

Tactic:
refine ht.uniq (mapCocone G s) _ fun j => ?_

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.Limits.IsColimit.uniq