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.Initial
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 : CreatesLimit G H
c : Cone ((F ⋙ G) ⋙ H)
hc : IsLimit c
refine :
  H.mapCone
      (Cone.whisker F
        (liftLimit.{v₂, u₂, v₃, v₄, u₃, u₄} (D := B) (F := H) (c := obj extendCone c)
          (((Equiv.symm (isLimitExtendConeEquiv F c) : IsLimit c ≃ IsLimit (obj extendCone c)) :
              (a : IsLimit c) → IsLimit (extendCone.obj c))
            hc))) ≅
    c
⊢ LiftableCone (F ⋙ G) H c

Tactic:
refine ⟨(liftLimit ((isLimitExtendConeEquiv 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.Initial
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 : CreatesLimit G H
c : Cone ((F ⋙ G) ⋙ H)
hc : IsLimit c
i : H.mapCone
    (liftLimit.{v₂, u₂, v₃, v₄, u₃, u₄} (D := B) (F := H) (c := obj extendCone c)
      (((Equiv.symm (isLimitExtendConeEquiv F c) : IsLimit c ≃ IsLimit (obj extendCone c)) :
          (a : IsLimit c) → IsLimit (extendCone.obj c))
        hc)) ≅
  obj extendCone c :=
  liftedLimitMapsToOriginal
    (((Equiv.symm (isLimitExtendConeEquiv F c) : IsLimit c ≃ IsLimit (obj extendCone c)) :
        (a : IsLimit c) → IsLimit (extendCone.obj c))
      hc)
⊢ H.mapCone
      (Cone.whisker F
        (liftLimit.{v₂, u₂, v₃, v₄, u₃, u₄} (D := B) (F := H) (c := obj extendCone c)
          (((Equiv.symm (isLimitExtendConeEquiv F c) : IsLimit c ≃ IsLimit (obj extendCone c)) :
              (a : IsLimit c) → IsLimit (extendCone.obj c))
            hc))) ≅
    c

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

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Functor.comp, CategoryTheory.Functor.Initial.conesEquiv, CategoryTheory.Iso.symm, CategoryTheory.Iso.app, CategoryTheory.Functor.mapIso, CategoryTheory.Limits.Cone.whiskering
-- 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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_4 : HasLimit G
rw :
  IsIso (X := limit G) (Y := limit (F ⋙ G))
    (Iso.hom (limit.isoLimitCone (getLimitCone G)) ≫
      (limitConeComp F (getLimitCone G)).isLimit.lift (Cone.whisker F (getLimitCone G).cone) ≫
        Iso.inv (limit.isoLimitCone (limitConeComp F (getLimitCone G))))
⊢ IsIso (X := limit G) (Y := limit (F ⋙ G)) (limit.pre G F)

Tactic:
rw [limit.pre_eq (limitConeComp F (getLimitCone G)) (getLimitCone G)]

Premises used: CategoryTheory.Functor.Initial.limitConeComp, CategoryTheory.Limits.getLimitCone, CategoryTheory.Limits.limit.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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_4 : HasLimit G
simp : IsIso (Y := limit (F ⋙ G)) (Iso.inv (limit.isoLimitCone (limitConeComp F (getLimitCone G))))
⊢ IsIso (X := limit G) (Y := limit (F ⋙ G))
    (Iso.hom (limit.isoLimitCone (getLimitCone G)) ≫
      (limitConeComp F (getLimitCone G)).isLimit.lift (Cone.whisker F (getLimitCone G).cone) ≫
        Iso.inv (limit.isoLimitCone (limitConeComp F (getLimitCone G))))

Tactic:
simp only [limitConeComp_cone, Cone.whisker_pt, limitConeComp_isLimit, IsLimit.lift_self,
    Category.id_comp, isIso_comp_left_iff]

Premises used: CategoryTheory.Functor.Initial.limitConeComp_isLimit, CategoryTheory.isIso_comp_left_iff, CategoryTheory.Functor.Initial.limitConeComp_cone, CategoryTheory.Limits.Cone.whisker_pt, CategoryTheory.Limits.IsLimit.lift_self, CategoryTheory.Category.id_comp
-- 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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_4 : HasLimit G
⊢ IsIso (Y := limit (F ⋙ G)) (Iso.inv (limit.isoLimitCone (limitConeComp F (getLimitCone 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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_4 : HasLimitsOfShape.{v₂, u₂, v₃, u₃} D E
inst_5 : HasLimitsOfShape.{v₁, u₁, v₃, u₃} C E
X Y : Functor.{v₂, v₃, u₂, u₃} D E
f : X ⟶ Y
simp :
  Eq (α := limit X ⟶ limit (F ⋙ Y)) (CategoryStruct.comp (Y := limit Y) (limMap f) (limit.pre Y F))
    (CategoryStruct.comp (Y := limit (F ⋙ X)) (limit.pre X F) (limMap (F.whiskerLeft f)))
⊢ Eq (α := obj lim X ⟶ obj (obj (whiskeringLeft C D E) F ⋙ lim) Y)
    (map lim f ≫
      Iso.hom ((fun (G : Functor.{v₂, v₃, u₂, u₃} D E) ↦ (Iso.symm (limitIso F G) : limit G ≅ limit (F ⋙ G))) Y))
    (Iso.hom ((fun (G : Functor.{v₂, v₃, u₂, u₃} D E) ↦ (Iso.symm (limitIso F G) : limit G ≅ limit (F ⋙ G))) X) ≫
      map (obj (whiskeringLeft C D E) F ⋙ lim) f)

Tactic:
simp only [comp_obj, whiskeringLeft_obj_obj, lim_obj, comp_map, whiskeringLeft_obj_map, lim_map,
      Iso.symm_hom, limitIso_inv]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Limits.lim_map, CategoryTheory.Functor.Initial.limitIso_inv, CategoryTheory.Iso.symm_hom, CategoryTheory.Limits.lim_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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_4 : HasLimitsOfShape.{v₂, u₂, v₃, u₃} D E
inst_5 : HasLimitsOfShape.{v₁, u₁, v₃, u₃} C E
X Y : Functor.{v₂, v₃, u₂, u₃} D E
f : X ⟶ Y
w :
  ∀ (j : C),
    Eq (α := limit X ⟶ (F ⋙ Y).obj j)
      (CategoryStruct.comp (Y := limit (F ⋙ Y)) (CategoryStruct.comp (Y := limit Y) (limMap f) (limit.pre Y F))
        (limit.π (F ⋙ Y) j))
      (CategoryStruct.comp (Y := limit (F ⋙ Y))
        (CategoryStruct.comp (Y := limit (F ⋙ X)) (limit.pre X F) (limMap (F.whiskerLeft f))) (limit.π (F ⋙ Y) j))
⊢ Eq (α := limit X ⟶ limit (F ⋙ Y)) (CategoryStruct.comp (Y := limit Y) (limMap f) (limit.pre Y F))
    (CategoryStruct.comp (Y := limit (F ⋙ X)) (limit.pre X F) (limMap (F.whiskerLeft 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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_4 : HasLimitsOfShape.{v₂, u₂, v₃, u₃} D E
inst_5 : HasLimitsOfShape.{v₁, u₁, v₃, u₃} C E
X Y : Functor.{v₂, v₃, u₂, u₃} D E
f : X ⟶ Y
j : C
⊢ Eq (α := limit X ⟶ (F ⋙ Y).obj j)
    (CategoryStruct.comp (Y := limit (F ⋙ Y)) (CategoryStruct.comp (Y := limit Y) (limMap f) (limit.pre Y F))
      (limit.π (F ⋙ Y) j))
    (CategoryStruct.comp (Y := limit (F ⋙ Y))
      (CategoryStruct.comp (Y := limit (F ⋙ X)) (limit.pre X F) (limMap (F.whiskerLeft f))) (limit.π (F ⋙ Y) 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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_4 : HasLimit (F ⋙ G)
⊢ HasLimit G

Tactic:
HasLimit.mk (limitConeOfComp F (getLimitCone (F ⋙ G)))

Premises used: CategoryTheory.Functor.Initial.limitConeOfComp, CategoryTheory.Functor.comp, CategoryTheory.Limits.getLimitCone, CategoryTheory.Limits.HasLimit.mk
-- 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.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
⊢ HasLimit (F ⋙ G) ↔ HasLimit G

Tactic:
⟨fun _ ↦ Functor.Initial.hasLimit_of_comp F, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro, CategoryTheory.Functor.Initial.hasLimit_of_comp
-- 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.Initial
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 : PreservesLimit (F ⋙ G) H
c : Cone G
hc : IsLimit c
⊢ Nonempty (IsLimit (H.mapCone c))

Tactic:
⟨isLimitWhiskerEquiv F _ ?_⟩

Premises used: CategoryTheory.Functor.Initial.isLimitWhiskerEquiv, 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.Initial
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 : PreservesLimit (F ⋙ G) H
c : Cone G
hc : IsLimit c
refine : IsLimit (Cone.whisker F (H.mapCone c))
⊢ Nonempty (IsLimit (H.mapCone c))

Tactic:
refine ⟨isLimitWhiskerEquiv 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.Initial
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 : PreservesLimit (F ⋙ G) H
c : Cone G
hc : IsLimit c
hc' : IsLimit (H.mapCone (Cone.whisker F c)) :=
  isLimitOfPreserves H (((isLimitWhiskerEquiv F c).symm : (a : IsLimit c) → IsLimit (Cone.whisker F c)) hc)
⊢ ∀ (j : C),
    (H.mapCone (Cone.whisker F c)).π.app j =
      Iso.hom (Iso.refl (H.mapCone (Cone.whisker F c)).pt) ≫ (Cone.whisker F (H.mapCone 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.Initial
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 : PreservesLimit (F ⋙ G) H
c : Cone G
hc : IsLimit c
hc' : IsLimit (H.mapCone (Cone.whisker F c)) :=
  isLimitOfPreserves H (((isLimitWhiskerEquiv F c).symm : (a : IsLimit c) → IsLimit (Cone.whisker F c)) hc)
⊢ IsLimit (Cone.whisker F (H.mapCone c))

Tactic:
exact IsLimit.ofIsoLimit hc' (Cone.ext (Iso.refl _) (by simp))

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.IsLimit.ofIsoLimit, CategoryTheory.Limits.Cone.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.Initial
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 : ReflectsLimit (F ⋙ G) H
c : Cone G
hc : IsLimit (H.mapCone c)
⊢ Nonempty (IsLimit c)

Tactic:
⟨isLimitWhiskerEquiv F _ (isLimitOfReflects H ?_)⟩

Premises used: CategoryTheory.Functor.Initial.isLimitWhiskerEquiv, CategoryTheory.Limits.isLimitOfReflects, 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.Initial
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 : ReflectsLimit (F ⋙ G) H
c : Cone G
hc : IsLimit (H.mapCone c)
refine : IsLimit (H.mapCone (Cone.whisker F c))
⊢ Nonempty (IsLimit c)

Tactic:
refine ⟨isLimitWhiskerEquiv F _ (isLimitOfReflects 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.Initial
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 : ReflectsLimit (F ⋙ G) H
c : Cone G
hc : IsLimit (H.mapCone c)
hc' : IsLimit (Cone.whisker F (H.mapCone c)) :=
  ((isLimitWhiskerEquiv F (H.mapCone c)).symm : (a : IsLimit (H.mapCone c)) → IsLimit (Cone.whisker F (H.mapCone c))) hc
⊢ ∀ (j : C),
    (Cone.whisker F (H.mapCone c)).π.app j =
      Iso.hom (Iso.refl (Cone.whisker F (H.mapCone c)).pt) ≫ (H.mapCone (Cone.whisker F 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.Initial
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 : ReflectsLimit (F ⋙ G) H
c : Cone G
hc : IsLimit (H.mapCone c)
hc' : IsLimit (Cone.whisker F (H.mapCone c)) :=
  ((isLimitWhiskerEquiv F (H.mapCone c)).symm : (a : IsLimit (H.mapCone c)) → IsLimit (Cone.whisker F (H.mapCone c))) hc
⊢ IsLimit (H.mapCone (Cone.whisker F c))

Tactic:
exact IsLimit.ofIsoLimit hc' (Cone.ext (Iso.refl _) (by simp))

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.IsLimit.ofIsoLimit, CategoryTheory.Limits.Cone.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.Initial
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 : CreatesLimit (F ⋙ G) H
c : Cone (G ⋙ H)
hc : IsLimit c
refine :
  H.mapCone
      (obj (C := Cone (F ⋙ G)) extendCone
        (liftLimit.{v₁, u₁, v₃, v₄, u₃, u₄} (D := B) (F := H) (c := Cone.whisker F c)
          (((isLimitWhiskerEquiv F c).symm : (a : IsLimit c) → IsLimit (Cone.whisker F c)) hc))) ≅
    c
⊢ LiftableCone G H c

Tactic:
refine ⟨(extendCone (F := F)).obj (liftLimit ((isLimitWhiskerEquiv F _).symm hc)), ?_⟩
-- 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.Initial
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 : CreatesLimit (F ⋙ G) H
c : Cone (G ⋙ H)
hc : IsLimit c
i : H.mapCone
    (liftLimit.{v₁, u₁, v₃, v₄, u₃, u₄} (D := B) (F := H) (c := Cone.whisker F c)
      (((isLimitWhiskerEquiv F c).symm : (a : IsLimit c) → IsLimit (Cone.whisker F c)) hc)) ≅
  Cone.whisker F c :=
  liftedLimitMapsToOriginal (((isLimitWhiskerEquiv F c).symm : (a : IsLimit c) → IsLimit (Cone.whisker F c)) hc)
refine :
  H.mapCone
      (obj (C := Cone (F ⋙ G)) extendCone
        (liftLimit.{v₁, u₁, v₃, v₄, u₃, u₄} (D := B) (F := H) (c := Cone.whisker F c)
          (((isLimitWhiskerEquiv F c).symm : (a : IsLimit c) → IsLimit (Cone.whisker F c)) hc))) ≅
    obj (C := Cone (F ⋙ G ⋙ H)) extendCone
      (H.mapCone
        (liftLimit.{v₁, u₁, v₃, v₄, u₃, u₄} (D := B) (F := H) (c := Cone.whisker F c)
          (((isLimitWhiskerEquiv F c).symm : (a : IsLimit c) → IsLimit (Cone.whisker F c)) hc)))
⊢ H.mapCone
      (obj (C := Cone (F ⋙ G)) extendCone
        (liftLimit.{v₁, u₁, v₃, v₄, u₃, u₄} (D := B) (F := H) (c := Cone.whisker F c)
          (((isLimitWhiskerEquiv F c).symm : (a : IsLimit c) → IsLimit (Cone.whisker F c)) hc))) ≅
    c

Tactic:
refine ?_ ≪≫ ((extendCone (F := F)).mapIso i) ≪≫ ((conesEquiv F (G ⋙ H)).counitIso.app _)

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.Initial.conesEquiv, CategoryTheory.Functor.Initial.extendCone, CategoryTheory.Iso.app, CategoryTheory.Functor.mapIso, CategoryTheory.Equivalence.counitIso
-- 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.Initial
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 : CreatesLimit (F ⋙ G) H
c : Cone (G ⋙ H)
hc : IsLimit c
i : H.mapCone
    (liftLimit.{v₁, u₁, v₃, v₄, u₃, u₄} (D := B) (F := H) (c := Cone.whisker F c)
      (((isLimitWhiskerEquiv F c).symm : (a : IsLimit c) → IsLimit (Cone.whisker F c)) hc)) ≅
  Cone.whisker F c :=
  liftedLimitMapsToOriginal (((isLimitWhiskerEquiv F c).symm : (a : IsLimit c) → IsLimit (Cone.whisker F c)) hc)
⊢ H.mapCone
      (obj (C := Cone (F ⋙ G)) extendCone
        (liftLimit.{v₁, u₁, v₃, v₄, u₃, u₄} (D := B) (F := H) (c := Cone.whisker F c)
          (((isLimitWhiskerEquiv F c).symm : (a : IsLimit c) → IsLimit (Cone.whisker F c)) hc))) ≅
    obj (C := Cone (F ⋙ G ⋙ H)) extendCone
      (H.mapCone
        (liftLimit.{v₁, u₁, v₃, v₄, u₃, u₄} (D := B) (F := H) (c := Cone.whisker F c)
          (((isLimitWhiskerEquiv F c).symm : (a : IsLimit c) → IsLimit (Cone.whisker F c)) hc)))

Tactic:
exact Cone.ext (Iso.refl _)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.Cone.ext
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F.Final
inst_4 : G.IsEquivalence
⊢ (F ⋙ G).Final

Tactic:
let i : F ≅ (F ⋙ G) ⋙ G.inv := isoWhiskerLeft F G.asEquivalence.unitIso
  have : Final ((F ⋙ G) ⋙ G.inv) := final_of_natIso i
  final_of_comp_full_faithful (F ⋙ G) G.inv

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Functor.final_of_natIso, CategoryTheory.Functor.comp, CategoryTheory.Functor.asEquivalence, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Functor.inv, CategoryTheory.Functor.final_of_comp_full_faithful
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F.Initial
inst_4 : G.IsEquivalence
⊢ (F ⋙ G).Initial

Tactic:
let i : F ≅ (F ⋙ G) ⋙ G.inv := isoWhiskerLeft F G.asEquivalence.unitIso
  have : Initial ((F ⋙ G) ⋙ G.inv) := initial_of_natIso i
  initial_of_comp_full_faithful (F ⋙ G) G.inv

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Functor.comp, CategoryTheory.Functor.asEquivalence, CategoryTheory.Functor.isoWhiskerLeft, CategoryTheory.Functor.inv, CategoryTheory.Functor.initial_of_natIso, CategoryTheory.Functor.initial_of_comp_full_faithful
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : G.IsEquivalence
⊢ F.Final ↔ (F ⋙ G).Final

Tactic:
⟨fun _ => final_comp_equivalence _ _, fun _ => final_of_comp_full_faithful _ G⟩

Premises used: CategoryTheory.Functor.final_comp_equivalence, Iff.intro, CategoryTheory.Functor.final_of_comp_full_faithful
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F.IsEquivalence
⊢ G.Final ↔ (F ⋙ G).Final

Tactic:
⟨fun _ => final_equivalence_comp _ _, fun _ => final_of_equivalence_comp F _⟩

Premises used: Iff.intro, CategoryTheory.Functor.final_of_equivalence_comp, CategoryTheory.Functor.final_equivalence_comp
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : G.IsEquivalence
⊢ F.Initial ↔ (F ⋙ G).Initial

Tactic:
⟨fun _ => initial_comp_equivalence _ _, fun _ => initial_of_comp_full_faithful _ G⟩

Premises used: CategoryTheory.Functor.initial_comp_equivalence, Iff.intro, CategoryTheory.Functor.initial_of_comp_full_faithful
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F.IsEquivalence
⊢ G.Initial ↔ (F ⋙ G).Initial

Tactic:
⟨fun _ => initial_equivalence_comp _ _, fun _ => initial_of_equivalence_comp F _⟩

Premises used: Iff.intro, CategoryTheory.Functor.initial_equivalence_comp, CategoryTheory.Functor.initial_of_equivalence_comp
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
hF : F.Final
hG : G.Final
s₁ : C ≌ AsSmall C := AsSmall.equiv
s₂ : D ≌ AsSmall D := AsSmall.equiv
s₃ : E ≌ AsSmall E := AsSmall.equiv
i : s₁.inverse ⋙ (F ⋙ G) ⋙ s₃.functor ≅ (s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor :=
  (s₁.inverse ⋙ F).isoWhiskerLeft (isoWhiskerRight s₂.unitIso (G ⋙ s₃.functor))
rw :
  ∀ (G_1 : AsSmall E ⥤ Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)),
    IsIso (X := colimit (((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor) ⋙ G_1)) (Y := colimit G_1)
      (colimit.pre G_1 ((s₁.inverse ⋙ F ⋙ s₂.functor) ⋙ s₂.inverse ⋙ G ⋙ s₃.functor))
⊢ (F ⋙ G).Final

Tactic:
rw [final_iff_comp_equivalence (F ⋙ G) s₃.functor, final_iff_equivalence_comp s₁.inverse,
    final_natIso_iff i, final_iff_isIso_colimit_pre]

Premises used: CategoryTheory.Functor.final_iff_comp_equivalence, CategoryTheory.Functor.comp, CategoryTheory.Equivalence.functor, CategoryTheory.Functor.final_iff_isIso_colimit_pre, CategoryTheory.Functor.final_natIso_iff, CategoryTheory.Functor.final_iff_equivalence_comp, CategoryTheory.Equivalence.inverse