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 : HasLimit F
X : C
f f' : X ⟶ limit F
w : ∀ (j : J), f ≫ π F j = f' ≫ π F j
⊢ f = f'

Tactic:
(limit.isLimit F).hom_ext w

Premises used: CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.limit, CategoryTheory.Limits.IsLimit.hom_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 G : Functor.{v₁, v, u₁, u} J C
inst_2 : HasLimit F
inst_3 : HasLimit G
c : Cone F
α : F ⟶ G
w :
  ∀ (j : J),
    CategoryStruct.comp (Y := limit G) (CategoryStruct.comp (Y := limit F) (lift F c) (limMap α)) (π G j) =
      CategoryStruct.comp (Y := limit G) (lift G ((Cone.postcompose α).obj c)) (π G j)
⊢ Eq (α := c.pt ⟶ limit G) (CategoryStruct.comp (Y := limit F) (lift F c) (limMap α))
    (lift G ((Cone.postcompose α).obj 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 G : Functor.{v₁, v, u₁, u} J C
inst_2 : HasLimit F
inst_3 : HasLimit G
c : Cone F
α : F ⟶ G
j : J
w : c.π.app j ≫ α.app j = ((Cone.postcompose α).obj c).π.app j
⊢ CategoryStruct.comp (Y := limit G) (CategoryStruct.comp (Y := limit F) (lift F c) (limMap α)) (π G j) =
    CategoryStruct.comp (Y := limit G) (lift G ((Cone.postcompose α).obj c)) (π G j)

Tactic:
rw [assoc, limMap_π, limit.lift_π_assoc, limit.lift_π]

Premises used: CategoryTheory.Limits.limMap_π, CategoryTheory.Category.assoc, CategoryTheory.Limits.limit.lift_π_assoc, CategoryTheory.Limits.limit.lift_π
-- 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 : HasLimit F
inst_3 : HasLimit G
c : Cone F
α : F ⟶ G
j : J
⊢ c.π.app j ≫ α.app j = ((Cone.postcompose α).obj 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
inst_2 : HasLimit F
⊢ lift F (cone F) = 𝟙 (limit F)

Tactic:
(limit.isLimit _).lift_self

Premises used: CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.limit, CategoryTheory.Limits.limit.lift, CategoryTheory.Limits.IsLimit.lift_self
-- 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 : HasLimit F
W : C
⊢ Eq (α := ULift.{u₁, v} (W ⟶ limit F) ⟶ F.cones.obj (op W)) (Iso.hom (homIso F W))
    (↾fun (f : ULift.{u₁, v} (W ⟶ limit F)) ↦ map (const J) f.down ≫ (cone F).π)

Tactic:
(limit.isLimit F).homIso_hom

Premises used: CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.limit, CategoryTheory.Limits.IsLimit.homIso_hom
-- 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 : HasLimit F
α : F ≅ G
⊢ HasLimit G

Tactic:
HasLimit.mk
    { cone := (Cone.postcompose α.hom).obj (limit.cone F)
      isLimit := (IsLimit.postcomposeHomEquiv _ _).symm (limit.isLimit F) }

Premises used: CategoryTheory.Limits.IsLimit.postcomposeHomEquiv, CategoryTheory.Limits.limit.cone, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.LimitCone.mk, Equiv.symm, CategoryTheory.Iso.hom, DFunLike.coe, CategoryTheory.Functor.obj, CategoryTheory.Limits.Cone.postcompose
-- 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
⊢ HasLimit F ↔ HasLimit G

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

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

Tactic:
HasLimit.mk ⟨_, IsLimit.ofRepresentableBy ((limit.isLimit F).representableBy.ofIso h)⟩

Premises used: CategoryTheory.Limits.IsLimit.ofRepresentableBy, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.IsLimit.representableBy, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Functor.RepresentableBy.ofIso, CategoryTheory.Limits.LimitCone.mk
-- 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 : HasLimit F
inst_3 : HasLimit G
w : F ≅ G
j : J
⊢ Eq (α := limit F ⟶ G.obj j) (CategoryStruct.comp (Y := limit G) (Iso.hom (isoOfNatIso w)) (limit.π G j))
    (limit.π F j ≫ w.hom.app j)

Tactic:
IsLimit.conePointsIsoOfNatIso_hom_comp _ _ _ _

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

Tactic:
IsLimit.conePointsIsoOfNatIso_inv_comp _ _ _ _

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso_inv_comp, CategoryTheory.Limits.limit
-- 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 : HasLimit F
inst_3 : HasLimit G
t : Cone F
w : F ≅ G
⊢ Eq (α := t.pt ⟶ limit G) (CategoryStruct.comp (Y := limit F) (limit.lift F t) (Iso.hom (isoOfNatIso w)))
    (limit.lift G ((Cone.postcompose w.hom).obj t))

Tactic:
IsLimit.lift_comp_conePointsIsoOfNatIso_hom _ _ _

Premises used: CategoryTheory.Limits.IsLimit.lift_comp_conePointsIsoOfNatIso_hom, CategoryTheory.Limits.limit, CategoryTheory.Limits.IsLimit.map, CategoryTheory.Limits.limit.lift
-- 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 : HasLimit F
inst_3 : HasLimit G
t : Cone G
w : F ≅ G
⊢ Eq (α := t.pt ⟶ limit F) (CategoryStruct.comp (Y := limit G) (limit.lift G t) (Iso.inv (isoOfNatIso w)))
    (limit.lift F ((Cone.postcompose w.inv).obj t))

Tactic:
IsLimit.lift_comp_conePointsIsoOfNatIso_inv _ _ _

Premises used: CategoryTheory.Limits.IsLimit.lift_comp_conePointsIsoOfNatIso_inv, CategoryTheory.Limits.limit, CategoryTheory.Limits.IsLimit.map, CategoryTheory.Limits.limit.lift
-- 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 : HasLimit F
G : Functor.{v₂, v, u₂, u} K C
inst_4 : HasLimit G
e : Equivalence.{v₁, v₂, u₁, u₂} J K
w : e.functor ⋙ G ≅ F
k : K
simp :
  Eq (α := limit F ⟶ G.obj k)
    (CategoryStruct.comp (Y := limit G)
        (IsLimit.lift (limit.isLimit G)
          ((Cone.equivalenceOfReindexing e.symm ((e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G)).functor.obj
            (limit.cone F)))
        (limit.π G k) :
      limit F ⟶ G.obj k)
    (limit.π F (e.inverse.obj k) ≫ w.inv.app (e.inverse.obj k) ≫ G.map (e.counit.app k) :
      limit F ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 K) k))
⊢ Eq (α := limit F ⟶ G.obj k) (CategoryStruct.comp (Y := limit G) (Iso.hom (isoOfEquivalence e w)) (limit.π G k))
    (limit.π F (e.inverse.obj k) ≫ w.inv.app (e.inverse.obj k) ≫ G.map (e.counit.app k))

Tactic:
simp only [HasLimit.isoOfEquivalence, IsLimit.conePointsIsoOfEquivalence_hom]

Premises used: CategoryTheory.Limits.HasLimit.isoOfEquivalence, CategoryTheory.Limits.IsLimit.conePointsIsoOfEquivalence_hom
-- 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 : HasLimit F
G : Functor.{v₂, v, u₂, u} K C
inst_4 : HasLimit G
e : Equivalence.{v₁, v₂, u₁, u₂} J K
w : e.functor ⋙ G ≅ F
k : K
⊢ Eq (α := limit F ⟶ G.obj k)
    (CategoryStruct.comp (Y := limit G)
        (IsLimit.lift (limit.isLimit G)
          ((Cone.equivalenceOfReindexing e.symm ((e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G)).functor.obj
            (limit.cone F)))
        (limit.π G k) :
      limit F ⟶ G.obj k)
    (limit.π F (e.inverse.obj k) ≫ w.inv.app (e.inverse.obj k) ≫ G.map (e.counit.app k) :
      limit F ⟶ G.obj (obj.{v₂, v₂, u₂, u₂} (𝟭 K) k))

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 : HasLimit F
G : Functor.{v₂, v, u₂, u} K C
inst_4 : HasLimit G
e : Equivalence.{v₁, v₂, u₁, u₂} J K
w : e.functor ⋙ G ≅ F
j : J
simp :
  Eq (α := limit G ⟶ F.obj j)
    (CategoryStruct.comp (Y := limit F)
      (Iso.inv (IsLimit.conePointsIsoOfEquivalence (limit.isLimit F) (limit.isLimit G) e w)) (limit.π F j))
    (limit.π G (e.functor.obj j) ≫ w.hom.app j)
⊢ Eq (α := limit G ⟶ F.obj j) (CategoryStruct.comp (Y := limit F) (Iso.inv (isoOfEquivalence e w)) (limit.π F j))
    (limit.π G (e.functor.obj j) ≫ w.hom.app j)

Tactic:
simp only [HasLimit.isoOfEquivalence]

Premises used: CategoryTheory.Limits.HasLimit.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 : HasLimit F
G : Functor.{v₂, v, u₂, u} K C
inst_4 : HasLimit G
e : Equivalence.{v₁, v₂, u₁, u₂} J K
w : e.functor ⋙ G ≅ F
j : J
⊢ Eq (α := limit G ⟶ F.obj j)
    (CategoryStruct.comp (Y := limit F)
      (Iso.inv (IsLimit.conePointsIsoOfEquivalence (limit.isLimit F) (limit.isLimit G) e w)) (limit.π F j))
    (limit.π G (e.functor.obj j) ≫ w.hom.app j)

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 : HasLimit F
E : Functor.{v₂, v₁, u₂, u₁} K J
inst_4 : HasLimit (E ⋙ F)
k : K
⊢ Eq (α := limit F ⟶ (E ⋙ F).obj k) (CategoryStruct.comp (Y := limit (E ⋙ F)) (pre F E) (π (E ⋙ F) k)) (π F (E.obj k))

Tactic:
simp [limit.pre]

Premises used: CategoryTheory.Limits.limit.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 : HasLimit F
E : Functor.{v₂, v₁, u₂, u₁} K J
inst_4 : HasLimit (E ⋙ F)
c : Cone F
w :
  ∀ (j : K),
    CategoryStruct.comp (Y := limit (E ⋙ F)) (CategoryStruct.comp (Y := limit F) (lift F c) (pre F E)) (π (E ⋙ F) j) =
      CategoryStruct.comp (Y := limit (E ⋙ F)) (lift (E ⋙ F) (Cone.whisker E c)) (π (E ⋙ F) j)
⊢ Eq (α := c.pt ⟶ limit (E ⋙ F)) (CategoryStruct.comp (Y := limit F) (lift F c) (pre F E))
    (lift (E ⋙ F) (Cone.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 : HasLimit F
E : Functor.{v₂, v₁, u₂, u₁} K J
inst_4 : HasLimit (E ⋙ F)
c : Cone F
j : K
⊢ CategoryStruct.comp (Y := limit (E ⋙ F)) (CategoryStruct.comp (Y := limit F) (lift F c) (pre F E)) (π (E ⋙ F) j) =
    CategoryStruct.comp (Y := limit (E ⋙ F)) (lift (E ⋙ F) (Cone.whisker E c)) (π (E ⋙ F) j)

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

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

Tactic:
erw [assoc, limit.pre_π, limit.pre_π, limit.pre_π]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.limit.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 : HasLimit F
E : Functor.{v₂, v₁, u₂, u₁} K J
inst_4 : HasLimit (E ⋙ F)
L : Type u₃
inst_5 : Category.{v₃, u₃} L
D : Functor.{v₃, v₂, u₃, u₂} L K
h : HasLimit (D ⋙ E ⋙ F)
this : HasLimit ((D ⋙ E) ⋙ F)
j : L
⊢ Eq (α := limit F ⟶ (D ⋙ E ⋙ F).obj j) (π F (E.obj (D.obj j))) (π F ((D ⋙ E).obj 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
D : Type u'
inst_2 : Category.{v', u'} D
F : Functor.{v₁, v, u₁, u} J C
inst_3 : HasLimit F
G : Functor.{v, v', u, u'} C D
inst_4 : HasLimit (F ⋙ G)
j : J
⊢ Eq (α := G.obj (limit F) ⟶ (F ⋙ G).obj j) (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (π (F ⋙ G) j))
    (G.map (π F j))

Tactic:
simp [limit.post]

Premises used: CategoryTheory.Limits.limit.post
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
F : Functor.{v₁, v, u₁, u} J C
inst_3 : HasLimit F
G : Functor.{v, v', u, u'} C D
inst_4 : HasLimit (F ⋙ G)
c : Cone F
w :
  ∀ (j : J),
    CategoryStruct.comp (Y := limit (F ⋙ G)) (CategoryStruct.comp (Y := G.obj (limit F)) (G.map (lift F c)) (post F G))
        (π (F ⋙ G) j) =
      CategoryStruct.comp (Y := limit (F ⋙ G)) (lift (F ⋙ G) (G.mapCone c)) (π (F ⋙ G) j)
⊢ Eq (α := G.obj c.pt ⟶ limit (F ⋙ G)) (CategoryStruct.comp (Y := G.obj (limit F)) (G.map (lift F c)) (post F G))
    (lift (F ⋙ G) (G.mapCone 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
D : Type u'
inst_2 : Category.{v', u'} D
F : Functor.{v₁, v, u₁, u} J C
inst_3 : HasLimit F
G : Functor.{v, v', u, u'} C D
inst_4 : HasLimit (F ⋙ G)
c : Cone F
j : J
w : G.map (c.π.app j) = (G.mapCone c).π.app j
⊢ CategoryStruct.comp (Y := limit (F ⋙ G)) (CategoryStruct.comp (Y := G.obj (limit F)) (G.map (lift F c)) (post F G))
      (π (F ⋙ G) j) =
    CategoryStruct.comp (Y := limit (F ⋙ G)) (lift (F ⋙ G) (G.mapCone c)) (π (F ⋙ G) j)

Tactic:
rw [assoc, limit.post_π, ← G.map_comp, limit.lift_π, limit.lift_π]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.limit.post_π, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.limit.lift_π
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
F : Functor.{v₁, v, u₁, u} J C
inst_3 : HasLimit F
G : Functor.{v, v', u, u'} C D
inst_4 : HasLimit (F ⋙ G)
c : Cone F
j : J
⊢ G.map (c.π.app j) = (G.mapCone 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
D : Type u'
inst_2 : Category.{v', u'} D
F : Functor.{v₁, v, u₁, u} J C
inst_3 : HasLimit F
G : Functor.{v, v', u, u'} C D
inst_4 : HasLimit (F ⋙ G)
E : Type u''
inst_5 : Category.{v'', u''} E
H : Functor.{v', v'', u', u''} D E
h : HasLimit ((F ⋙ G) ⋙ H)
⊢ HasLimit (F ⋙ G ⋙ H)

Tactic:
haveI : HasLimit (F ⋙ G ⋙ H) := h
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
F : Functor.{v₁, v, u₁, u} J C
inst_3 : HasLimit F
G : Functor.{v, v', u, u'} C D
inst_4 : HasLimit (F ⋙ G)
E : Type u''
inst_5 : Category.{v'', u''} E
H : Functor.{v', v'', u', u''} D E
h : HasLimit ((F ⋙ G) ⋙ H)
this : HasLimit (F ⋙ G ⋙ H)
w :
  ∀ (j : J),
    Eq (α := H.obj (G.obj (limit F)) ⟶ ((F ⋙ G) ⋙ H).obj j)
      (CategoryStruct.comp (Y := limit ((F ⋙ G) ⋙ H))
        (CategoryStruct.comp (Y := H.obj (limit (F ⋙ G))) (H.map (post F G)) (post (F ⋙ G) H)) (π ((F ⋙ G) ⋙ H) j))
      (CategoryStruct.comp (Y := limit ((F ⋙ G) ⋙ H)) (post F (G ⋙ H)) (π ((F ⋙ G) ⋙ H) j))
⊢ Eq (α := H.obj (G.obj (limit F)) ⟶ limit ((F ⋙ G) ⋙ H))
    (CategoryStruct.comp (Y := H.obj (limit (F ⋙ G))) (H.map (post F G)) (post (F ⋙ G) H)) (post F (G ⋙ H))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
F : Functor.{v₁, v, u₁, u} J C
inst_3 : HasLimit F
G : Functor.{v, v', u, u'} C D
inst_4 : HasLimit (F ⋙ G)
E : Type u''
inst_5 : Category.{v'', u''} E
H : Functor.{v', v'', u', u''} D E
h : HasLimit ((F ⋙ G) ⋙ H)
this : HasLimit (F ⋙ G ⋙ H)
j : J
w : Eq (α := H.obj (G.obj (limit F)) ⟶ ((F ⋙ G) ⋙ H).obj j) (H.map (G.map (π F j))) ((G ⋙ H).map (π F j))
⊢ Eq (α := H.obj (G.obj (limit F)) ⟶ ((F ⋙ G) ⋙ H).obj j)
    (CategoryStruct.comp (Y := limit ((F ⋙ G) ⋙ H))
      (CategoryStruct.comp (Y := H.obj (limit (F ⋙ G))) (H.map (post F G)) (post (F ⋙ G) H)) (π ((F ⋙ G) ⋙ H) j))
    (CategoryStruct.comp (Y := limit ((F ⋙ G) ⋙ H)) (post F (G ⋙ H)) (π ((F ⋙ G) ⋙ H) j))

Tactic:
erw [assoc, limit.post_π, ← H.map_comp, limit.post_π, limit.post_π]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.limit.post_π, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
F : Functor.{v₁, v, u₁, u} J C
inst_3 : HasLimit F
G : Functor.{v, v', u, u'} C D
inst_4 : HasLimit (F ⋙ G)
E : Type u''
inst_5 : Category.{v'', u''} E
H : Functor.{v', v'', u', u''} D E
h : HasLimit ((F ⋙ G) ⋙ H)
this : HasLimit (F ⋙ G ⋙ H)
j : J
⊢ Eq (α := H.obj (G.obj (limit F)) ⟶ ((F ⋙ G) ⋙ H).obj j) (H.map (G.map (π F j))) ((G ⋙ H).map (π F j))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
D : Type u'
inst_3 : Category.{v', u'} D
E : Functor.{v₂, v₁, u₂, u₁} K J
F : Functor.{v₁, v, u₁, u} J C
G : Functor.{v, v', u, u'} C D
inst_4 : HasLimit F
inst_5 : HasLimit (E ⋙ F)
inst_6 : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
⊢ HasLimit (E ⋙ F ⋙ G)

Tactic:
haveI : HasLimit (E ⋙ F ⋙ G) := h
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
D : Type u'
inst_3 : Category.{v', u'} D
E : Functor.{v₂, v₁, u₂, u₁} K J
F : Functor.{v₁, v, u₁, u} J C
G : Functor.{v, v', u, u'} C D
inst_4 : HasLimit F
inst_5 : HasLimit (E ⋙ F)
inst_6 : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
this : HasLimit (E ⋙ F ⋙ G)
w :
  ∀ (j : K),
    Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j)
      (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
        (CategoryStruct.comp (Y := G.obj (limit (E ⋙ F))) (G.map (pre F E)) (post (E ⋙ F) G)) (π ((E ⋙ F) ⋙ G) j))
      (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
        (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))
⊢ Eq (α := G.obj (limit F) ⟶ limit ((E ⋙ F) ⋙ G))
    (CategoryStruct.comp (Y := G.obj (limit (E ⋙ F))) (G.map (pre F E)) (post (E ⋙ F) G))
    (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.HasLimits
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u
inst_2 : Category.{v, u} C
D : Type u'
inst_3 : Category.{v', u'} D
E : Functor.{v₂, v₁, u₂, u₁} K J
F : Functor.{v₁, v, u₁, u} J C
G : Functor.{v, v', u, u'} C D
inst_4 : HasLimit F
inst_5 : HasLimit (E ⋙ F)
inst_6 : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
this : HasLimit (E ⋙ F ⋙ G)
j : K
w :
  Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j)
    (CategoryStruct.comp (Y := G.obj (limit (E ⋙ F))) (G.map (pre F E))
      (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G)) (post (E ⋙ F) G) (π ((E ⋙ F) ⋙ G) j)))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))
w₁ :
  Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j)
    (CategoryStruct.comp (Y := G.obj (limit (E ⋙ F))) (G.map (pre F E)) (G.map (π (E ⋙ F) j)))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))
w₂ :
  Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j)
    (G.map (CategoryStruct.comp (Y := limit (E ⋙ F)) (pre F E) (π (E ⋙ F) j)))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))
w₃ :
  Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j) (G.map (π F (E.obj j)))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))
w₄ :
  Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j) (G.map (π F (E.obj j)))
    (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G)
      (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G)) (pre (F ⋙ G) E) (π ((E ⋙ F) ⋙ G) j)))
w₅ :
  Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j) (G.map (π F (E.obj j)))
    (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (π (F ⋙ G) (E.obj j)))
w₆ w₇ : Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j) (G.map (π F (E.obj j))) (G.map (π F (E.obj j)))
⊢ Eq (α := G.obj (limit F) ⟶ ((E ⋙ F) ⋙ G).obj j)
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := G.obj (limit (E ⋙ F))) (G.map (pre F E)) (post (E ⋙ F) G)) (π ((E ⋙ F) ⋙ G) j))
    (CategoryStruct.comp (Y := limit ((E ⋙ F) ⋙ G))
      (CategoryStruct.comp (Y := limit (F ⋙ G)) (post F G) (pre (F ⋙ G) E)) (π ((E ⋙ F) ⋙ G) j))

Tactic:
erw [assoc, limit.post_π, ← G.map_comp, limit.pre_π, assoc, limit.pre_π, limit.post_π]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.limit.post_π, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.limit.pre_π