awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cocone (F ⋙ G)
X : D
Y : C
f : X ⟶ F.obj Y
X₁ X₂ : C
k₁ : X ⟶ F.obj X₁
k₂ : X ⟶ F.obj X₂
f_1 : X₁ ⟶ X₂
h₁ : k₁ ≫ F.map f_1 = k₂
h₂ : G.map k₂ ≫ c.ι.app X₂ = G.map f ≫ c.ι.app Y
⊢ G.map k₁ ≫ c.ι.app X₁ = G.map f ≫ c.ι.app Y

Tactic:
simp [← h₂, ← h₁, ← Functor.comp_map, c.ι.naturality]

Premises used: CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
s : Cocone (F ⋙ G)
j : C
h₁ :
  ∀ (X₁ X₂ : C) (k₁ : F.obj j ⟶ F.obj X₁) (k₂ : F.obj j ⟶ F.obj X₂) (f : X₁ ⟶ X₂),
    k₁ ≫ F.map f = k₂ → G.map k₁ ≫ s.ι.app X₁ = s.ι.app j → G.map k₂ ≫ s.ι.app X₂ = s.ι.app j
h₂ :
  ∀ (X₁ X₂ : C) (k₁ : F.obj j ⟶ F.obj X₁) (k₂ : F.obj j ⟶ F.obj X₂) (f : X₁ ⟶ X₂),
    k₁ ≫ F.map f = k₂ → G.map k₂ ≫ s.ι.app X₂ = s.ι.app j → G.map k₁ ≫ s.ι.app X₁ = s.ι.app j
z : G.map (F.map (𝟙 j)) ≫ s.ι.app j = s.ι.app j
X₀ : C
k₀ : F.obj j ⟶ F.obj j
⊢ G.map (homToLift F (F.obj j)) ≫ s.ι.app (lift F (F.obj j)) = s.ι.app j

Tactic:
apply induction F fun X k => G.map k ≫ s.ι.app X = (s.ι.app j :)

Premises used: CategoryTheory.Functor.Final.induction, CategoryTheory.Functor.map, CategoryTheory.Limits.Cocone.ι, CategoryTheory.CategoryStruct.comp, Eq, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
s : Cocone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j ⟶ F.obj j₁
k₂ : F.obj j ⟶ F.obj j₂
f : j₁ ⟶ j₂
w : k₁ ≫ F.map f = k₂
h : G.map k₁ ≫ s.ι.app j₁ = s.ι.app j
h₁ : G.map (k₁ ≫ F.map f) ≫ s.ι.app j₂ = s.ι.app j
⊢ G.map k₂ ≫ s.ι.app j₂ = s.ι.app j

Tactic:
rw [← w]
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
s : Cocone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j ⟶ F.obj j₁
k₂ : F.obj j ⟶ F.obj j₂
f : j₁ ⟶ j₂
w : k₁ ≫ F.map f = k₂
h : G.map k₁ ≫ s.ι.app j₁ = s.ι.app j
⊢ G.map k₁ ≫ (F ⋙ G).map f ≫ s.ι.app j₂ = s.ι.app j

Tactic:
rw [← s.w f] at h

Premises used: CategoryTheory.Limits.Cocone.w
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
s : Cocone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j ⟶ F.obj j₁
k₂ : F.obj j ⟶ F.obj j₂
f : j₁ ⟶ j₂
w : k₁ ≫ F.map f = k₂
h : G.map k₁ ≫ (F ⋙ G).map f ≫ s.ι.app j₂ = s.ι.app j
⊢ G.map (k₁ ≫ F.map f) ≫ s.ι.app j₂ = s.ι.app j

Tactic:
simpa using h
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
s : Cocone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j ⟶ F.obj j₁
k₂ : F.obj j ⟶ F.obj j₂
f : j₁ ⟶ j₂
w : k₁ ≫ F.map f = k₂
h : G.map k₂ ≫ s.ι.app j₂ = s.ι.app j
⊢ G.map (k₁ ≫ F.map f) ≫ s.ι.app j₂ = s.ι.app j

Tactic:
rw [← w] at h
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
s : Cocone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j ⟶ F.obj j₁
k₂ : F.obj j ⟶ F.obj j₂
f : j₁ ⟶ j₂
w : k₁ ≫ F.map f = k₂
h : G.map (k₁ ≫ F.map f) ≫ s.ι.app j₂ = s.ι.app j
h₂ : G.map k₁ ≫ (F ⋙ G).map f ≫ s.ι.app j₂ = s.ι.app j
⊢ G.map k₁ ≫ s.ι.app j₁ = s.ι.app j

Tactic:
rw [← s.w f]

Premises used: CategoryTheory.Limits.Cocone.w
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
s : Cocone (F ⋙ G)
j j₁ j₂ : C
k₁ : F.obj j ⟶ F.obj j₁
k₂ : F.obj j ⟶ F.obj j₂
f : j₁ ⟶ j₂
w : k₁ ≫ F.map f = k₂
h : G.map (k₁ ≫ F.map f) ≫ s.ι.app j₂ = s.ι.app j
⊢ G.map k₁ ≫ (F ⋙ G).map f ≫ s.ι.app j₂ = s.ι.app j

Tactic:
simpa using h
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
s : Cocone (F ⋙ G)
j : C
⊢ G.map (F.map (𝟙 j)) ≫ s.ι.app j = s.ι.app j

Tactic:
s.w (𝟙 _)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.Cocone.w
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
s : Cocone (F ⋙ G)
j : C
⊢ G.map (F.map (𝟙 j)) ≫ s.ι.app j = s.ι.app j

Tactic:
exact s.w (𝟙 _)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.Cocone.w
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_4 : HasColimit G
⊢ HasColimit (F ⋙ G)

Tactic:
HasColimit.mk (colimitCoconeComp F (getColimitCocone G))

Premises used: CategoryTheory.Functor.Final.colimitCoconeComp, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.getColimitCocone
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
B : Type u₄
inst_4 : Category.{v₄, u₄} B
H : Functor.{v₃, v₄, u₃, u₄} E B
inst_5 : PreservesColimit G H
c : Cocone (F ⋙ G)
hc : IsColimit c
⊢ Nonempty (IsColimit (H.mapCocone c))

Tactic:
⟨isColimitExtendCoconeEquiv (G := G ⋙ H) F (H.mapCocone c) ?_⟩

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.Functor.Final.isColimitExtendCoconeEquiv, Nonempty.intro, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
B : Type u₄
inst_4 : Category.{v₄, u₄} B
H : Functor.{v₃, v₄, u₃, u₄} E B
inst_5 : PreservesColimit G H
c : Cocone (F ⋙ G)
hc : IsColimit c
refine : IsColimit (obj extendCocone (H.mapCocone c))
⊢ Nonempty (IsColimit (H.mapCocone c))

Tactic:
refine ⟨isColimitExtendCoconeEquiv (G := G ⋙ H) F (H.mapCocone c) ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
B : Type u₄
inst_4 : Category.{v₄, u₄} B
H : Functor.{v₃, v₄, u₃, u₄} E B
inst_5 : PreservesColimit G H
c : Cocone (F ⋙ G)
hc : IsColimit c
hc' : IsColimit (H.mapCocone (obj extendCocone c)) :=
  isColimitOfPreserves H
    ((Equiv.symm (isColimitExtendCoconeEquiv F c) : (a : IsColimit c) → IsColimit (extendCocone.obj c)) hc)
⊢ ∀ (j : D),
    (H.mapCocone (obj extendCocone c)).ι.app j ≫ Iso.hom (Iso.refl (H.mapCocone (obj extendCocone c)).pt) =
      NatTrans.app (obj extendCocone (H.mapCocone c)).ι j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
B : Type u₄
inst_4 : Category.{v₄, u₄} B
H : Functor.{v₃, v₄, u₃, u₄} E B
inst_5 : PreservesColimit G H
c : Cocone (F ⋙ G)
hc : IsColimit c
hc' : IsColimit (H.mapCocone (obj extendCocone c)) :=
  isColimitOfPreserves H
    ((Equiv.symm (isColimitExtendCoconeEquiv F c) : (a : IsColimit c) → IsColimit (extendCocone.obj c)) hc)
⊢ IsColimit (obj extendCocone (H.mapCocone c))

Tactic:
exact IsColimit.ofIsoColimit hc' (Cocone.ext (Iso.refl _) (by simp))

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.Iso.refl
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
B : Type u₄
inst_4 : Category.{v₄, u₄} B
H : Functor.{v₃, v₄, u₃, u₄} E B
inst_5 : ReflectsColimit G H
c : Cocone (F ⋙ G)
hc : IsColimit (H.mapCocone c)
⊢ Nonempty (IsColimit c)

Tactic:
⟨isColimitExtendCoconeEquiv F _ (isColimitOfReflects H ?_)⟩

Premises used: CategoryTheory.Functor.Final.isColimitExtendCoconeEquiv, Nonempty.intro, CategoryTheory.Limits.isColimitOfReflects, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
B : Type u₄
inst_4 : Category.{v₄, u₄} B
H : Functor.{v₃, v₄, u₃, u₄} E B
inst_5 : ReflectsColimit G H
c : Cocone (F ⋙ G)
hc : IsColimit (H.mapCocone c)
refine : IsColimit (H.mapCocone (obj extendCocone c))
⊢ Nonempty (IsColimit c)

Tactic:
refine ⟨isColimitExtendCoconeEquiv F _ (isColimitOfReflects H ?_)⟩
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
B : Type u₄
inst_4 : Category.{v₄, u₄} B
H : Functor.{v₃, v₄, u₃, u₄} E B
inst_5 : ReflectsColimit G H
c : Cocone (F ⋙ G)
hc : IsColimit (H.mapCocone c)
hc' : IsColimit (obj extendCocone (H.mapCocone c)) :=
  ((Equiv.symm (isColimitExtendCoconeEquiv F (H.mapCocone c)) :
        IsColimit (H.mapCocone c) ≃ IsColimit (obj extendCocone (H.mapCocone c))) :
      (a : IsColimit (H.mapCocone c)) → IsColimit (extendCocone.obj (H.mapCocone c)))
    hc
⊢ ∀ (j : D),
    CategoryStruct.comp (Y := (obj extendCocone (H.mapCocone c)).pt)
        (NatTrans.app (obj extendCocone (H.mapCocone c)).ι j :
          (G ⋙ H).obj j ⟶ obj.{v₂, v₄, u₂, u₄} (obj (const D) (obj extendCocone (H.mapCocone c)).pt) j)
        (Iso.hom (Iso.refl (obj extendCocone (H.mapCocone c)).pt) :
          (obj extendCocone (H.mapCocone c)).pt ⟶ (H.mapCocone (obj extendCocone c)).pt) =
      (H.mapCocone (obj extendCocone c)).ι.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
B : Type u₄
inst_4 : Category.{v₄, u₄} B
H : Functor.{v₃, v₄, u₃, u₄} E B
inst_5 : ReflectsColimit G H
c : Cocone (F ⋙ G)
hc : IsColimit (H.mapCocone c)
hc' : IsColimit (obj extendCocone (H.mapCocone c)) :=
  ((Equiv.symm (isColimitExtendCoconeEquiv F (H.mapCocone c)) :
        IsColimit (H.mapCocone c) ≃ IsColimit (obj extendCocone (H.mapCocone c))) :
      (a : IsColimit (H.mapCocone c)) → IsColimit (extendCocone.obj (H.mapCocone c)))
    hc
⊢ IsColimit (H.mapCocone (obj extendCocone c))

Tactic:
exact IsColimit.ofIsoColimit hc' (Cocone.ext (Iso.refl _) (by simp))

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.Iso.refl
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
B : Type u₄
inst_4 : Category.{v₄, u₄} B
H : Functor.{v₃, v₄, u₃, u₄} E B
inst_5 : CreatesColimit G H
c : Cocone ((F ⋙ G) ⋙ H)
hc : IsColimit c
refine :
  H.mapCocone
      (Cocone.whisker F
        (liftColimit.{v₂, u₂, v₃, v₄, u₃, u₄} (D := B) (F := H) (c := obj extendCocone c)
          (((Equiv.symm (isColimitExtendCoconeEquiv F c) : IsColimit c ≃ IsColimit (obj extendCocone c)) :
              (a : IsColimit c) → IsColimit (extendCocone.obj c))
            hc))) ≅
    c
⊢ LiftableCocone (F ⋙ G) H c

Tactic:
refine ⟨(liftColimit ((isColimitExtendCoconeEquiv F (G := G ⋙ H) _).symm hc)).whisker F, ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
B : Type u₄
inst_4 : Category.{v₄, u₄} B
H : Functor.{v₃, v₄, u₃, u₄} E B
inst_5 : CreatesColimit G H
c : Cocone ((F ⋙ G) ⋙ H)
hc : IsColimit c
i : H.mapCocone
    (liftColimit.{v₂, u₂, v₃, v₄, u₃, u₄} (D := B) (F := H) (c := obj extendCocone c)
      (((Equiv.symm (isColimitExtendCoconeEquiv F c) : IsColimit c ≃ IsColimit (obj extendCocone c)) :
          (a : IsColimit c) → IsColimit (extendCocone.obj c))
        hc)) ≅
  obj extendCocone c :=
  liftedColimitMapsToOriginal
    (((Equiv.symm (isColimitExtendCoconeEquiv F c) : IsColimit c ≃ IsColimit (obj extendCocone c)) :
        (a : IsColimit c) → IsColimit (extendCocone.obj c))
      hc)
⊢ H.mapCocone
      (Cocone.whisker F
        (liftColimit.{v₂, u₂, v₃, v₄, u₃, u₄} (D := B) (F := H) (c := obj extendCocone c)
          (((Equiv.symm (isColimitExtendCoconeEquiv F c) : IsColimit c ≃ IsColimit (obj extendCocone c)) :
              (a : IsColimit c) → IsColimit (extendCocone.obj c))
            hc))) ≅
    c

Tactic:
exact (Cocone.whiskering F).mapIso i ≪≫ ((coconesEquiv F (G ⋙ H)).unitIso.app _).symm

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Functor.comp, CategoryTheory.Iso.symm, CategoryTheory.Iso.app, CategoryTheory.Functor.mapIso, CategoryTheory.Limits.Cocone.whiskering, CategoryTheory.Functor.Final.coconesEquiv
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_4 : HasColimit G
simp :
  IsIso (X := colimit (F ⋙ G)) (Y := colimit G)
    (Iso.hom (colimit.isoColimitCocone (colimitCoconeComp F (getColimitCocone G))) ≫
      𝟙 (Cocone.whisker F (getColimitCocone G).cocone).pt ≫ Iso.inv (colimit.isoColimitCocone (getColimitCocone G)))
⊢ IsIso (X := colimit (F ⋙ G)) (Y := colimit G) (colimit.pre G F)

Tactic:
simp only [colimit.pre_eq (colimitCoconeComp F (getColimitCocone G)) (getColimitCocone G),
    colimitCoconeComp_cocone, IsColimit.desc_self]

Premises used: CategoryTheory.Functor.Final.colimitCoconeComp_cocone, CategoryTheory.Limits.IsColimit.desc_self, CategoryTheory.Functor.Final.colimitCoconeComp, CategoryTheory.Limits.getColimitCocone, CategoryTheory.Limits.colimit.pre_eq
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_4 : HasColimit G
⊢ IsIso (X := colimit (F ⋙ G)) (Y := colimit G)
    (Iso.hom (colimit.isoColimitCocone (colimitCoconeComp F (getColimitCocone G))) ≫
      𝟙 (Cocone.whisker F (getColimitCocone G).cocone).pt ≫ Iso.inv (colimit.isoColimitCocone (getColimitCocone G)))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_4 : HasColimit G
X : C
⊢ Eq (α := (F ⋙ G).obj X ⟶ colimit G)
    (CategoryStruct.comp (Y := colimit (F ⋙ G)) (colimit.ι (F ⋙ G) X : (F ⋙ G).obj X ⟶ colimit (F ⋙ G))
      (Iso.hom (colimitIso F G) : colimit (F ⋙ G) ⟶ colimit G))
    (colimit.ι G (F.obj X))

Tactic:
simp [colimitIso]

Premises used: CategoryTheory.Functor.Final.colimitIso
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_4 : HasColimit G
X : C
⊢ Eq (α := G.obj (F.obj X) ⟶ colimit (F ⋙ G))
    (CategoryStruct.comp (Y := colimit G) (colimit.ι G (F.obj X)) (Iso.inv (colimitIso F G)) :
      G.obj (F.obj X) ⟶ colimit (F ⋙ G))
    (colimit.ι (F ⋙ G) X : (F ⋙ G).obj X ⟶ colimit (F ⋙ G))

Tactic:
simp [colimitIso]

Premises used: CategoryTheory.Functor.Final.colimitIso
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_4 : HasColimitsOfShape.{v₂, u₂, v₃, u₃} D E
inst_5 : HasColimitsOfShape.{v₁, u₁, v₃, u₃} C E
X Y : Functor.{v₂, v₃, u₂, u₃} D E
f : X ⟶ Y
simp :
  Eq (α := colimit (F ⋙ X) ⟶ colimit Y)
    (CategoryStruct.comp (Y := colimit (F ⋙ Y)) (colimMap (F.whiskerLeft f)) (colimit.pre Y F))
    (CategoryStruct.comp (Y := colimit X) (colimit.pre X F) (colimMap f))
⊢ Eq (α := obj (obj (whiskeringLeft C D E) F ⋙ colim) X ⟶ obj colim Y)
    (map (obj (whiskeringLeft C D E) F ⋙ colim) f ≫
      Iso.hom ((fun (G : Functor.{v₂, v₃, u₂, u₃} D E) ↦ (colimitIso F G : colimit (F ⋙ G) ≅ colimit G)) Y))
    (Iso.hom ((fun (G : Functor.{v₂, v₃, u₂, u₃} D E) ↦ (colimitIso F G : colimit (F ⋙ G) ≅ colimit G)) X) ≫
      map colim f)

Tactic:
simp only [comp_obj, whiskeringLeft_obj_obj, colim_obj, comp_map, whiskeringLeft_obj_map,
      colim_map, colimitIso_hom]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.Final.colimitIso_hom, CategoryTheory.Limits.colim_map, CategoryTheory.Limits.colim_obj, CategoryTheory.Functor.whiskeringLeft_obj_map, CategoryTheory.Functor.whiskeringLeft_obj_obj, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_4 : HasColimitsOfShape.{v₂, u₂, v₃, u₃} D E
inst_5 : HasColimitsOfShape.{v₁, u₁, v₃, u₃} C E
X Y : Functor.{v₂, v₃, u₂, u₃} D E
f : X ⟶ Y
w :
  ∀ (j : C),
    Eq (α := (F ⋙ X).obj j ⟶ colimit Y)
      (CategoryStruct.comp (Y := colimit (F ⋙ X)) (colimit.ι (F ⋙ X) j)
        (CategoryStruct.comp (Y := colimit (F ⋙ Y)) (colimMap (F.whiskerLeft f)) (colimit.pre Y F)))
      (CategoryStruct.comp (Y := colimit (F ⋙ X)) (colimit.ι (F ⋙ X) j)
        (CategoryStruct.comp (Y := colimit X) (colimit.pre X F) (colimMap f)))
⊢ Eq (α := colimit (F ⋙ X) ⟶ colimit Y)
    (CategoryStruct.comp (Y := colimit (F ⋙ Y)) (colimMap (F.whiskerLeft f)) (colimit.pre Y F))
    (CategoryStruct.comp (Y := colimit X) (colimit.pre X F) (colimMap f))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_4 : HasColimitsOfShape.{v₂, u₂, v₃, u₃} D E
inst_5 : HasColimitsOfShape.{v₁, u₁, v₃, u₃} C E
X Y : Functor.{v₂, v₃, u₂, u₃} D E
f : X ⟶ Y
j : C
⊢ Eq (α := (F ⋙ X).obj j ⟶ colimit Y)
    (CategoryStruct.comp (Y := colimit (F ⋙ X)) (colimit.ι (F ⋙ X) j)
      (CategoryStruct.comp (Y := colimit (F ⋙ Y)) (colimMap (F.whiskerLeft f)) (colimit.pre Y F)))
    (CategoryStruct.comp (Y := colimit (F ⋙ X)) (colimit.ι (F ⋙ X) j)
      (CategoryStruct.comp (Y := colimit X) (colimit.pre X F) (colimMap f)))

Tactic:
simp only [comp_obj, ι_colimMap_assoc, whiskerLeft_app, colimit.ι_pre, colimit.ι_pre_assoc,
      ι_colimMap]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Limits.colimit.ι_pre_assoc, CategoryTheory.Limits.ι_colimMap, CategoryTheory.Limits.ι_colimMap_assoc, CategoryTheory.Limits.colimit.ι_pre, CategoryTheory.Functor.whiskerLeft_app
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_4 : HasColimit (F ⋙ G)
⊢ HasColimit G

Tactic:
HasColimit.mk (colimitCoconeOfComp F (getColimitCocone (F ⋙ G)))

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Functor.Final.colimitCoconeOfComp, CategoryTheory.Limits.getColimitCocone
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
⊢ HasColimit (F ⋙ G) ↔ HasColimit G

Tactic:
⟨fun _ ↦ Functor.Final.hasColimit_of_comp F, fun _ ↦ inferInstance⟩

Premises used: CategoryTheory.Functor.Final.hasColimit_of_comp, inferInstance, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
B : Type u₄
inst_4 : Category.{v₄, u₄} B
H : Functor.{v₃, v₄, u₃, u₄} E B
inst_5 : PreservesColimit (F ⋙ G) H
c : Cocone G
hc : IsColimit c
⊢ Nonempty (IsColimit (H.mapCocone c))

Tactic:
⟨isColimitWhiskerEquiv F _ ?_⟩

Premises used: Nonempty.intro, CategoryTheory.Functor.Final.isColimitWhiskerEquiv, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
B : Type u₄
inst_4 : Category.{v₄, u₄} B
H : Functor.{v₃, v₄, u₃, u₄} E B
inst_5 : PreservesColimit (F ⋙ G) H
c : Cocone G
hc : IsColimit c
refine : IsColimit (Cocone.whisker F (H.mapCocone c))
⊢ Nonempty (IsColimit (H.mapCocone c))

Tactic:
refine ⟨isColimitWhiskerEquiv F _ ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
B : Type u₄
inst_4 : Category.{v₄, u₄} B
H : Functor.{v₃, v₄, u₃, u₄} E B
inst_5 : PreservesColimit (F ⋙ G) H
c : Cocone G
hc : IsColimit c
hc' : IsColimit (H.mapCocone (Cocone.whisker F c)) :=
  isColimitOfPreserves H (((isColimitWhiskerEquiv F c).symm : (a : IsColimit c) → IsColimit (Cocone.whisker F c)) hc)
⊢ ∀ (j : C),
    (H.mapCocone (Cocone.whisker F c)).ι.app j ≫ Iso.hom (Iso.refl (H.mapCocone (Cocone.whisker F c)).pt) =
      (Cocone.whisker F (H.mapCocone c)).ι.app j

Tactic:
simp