awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₂, v₁, u₂, u₁} D C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
⊢ Eq (α :=
    { obj := fun (X : D) ↦ (c X).pt,
        map := fun {X Y : D} (h : X ⟶ Y) ↦
          (hc Y).lift { pt := (c X).pt, π := (c X).π ≫ cospanHomMk (H.map h) (F.map h) (G.map h) ⋯ ⋯ },
        map_id := ⋯, map_comp := ⋯ } ⟶
      H)
    ({ app := fun (X : D) ↦ (c X).fst, naturality := ⋯ :
        NatTrans
          { obj := fun (X : D) ↦ (c X).pt,
            map := fun {X Y : D} (h : X ⟶ Y) ↦
              (hc Y).lift
                { pt := (c X).pt, π := (c X).π ≫ cospanHomMk (H.map h) (F.map h) (G.map h) ⋯ ⋯ :
                  Cone (cospan (f.app Y) (g.app Y)) },
            map_id := ⋯, map_comp := ⋯ : Functor.{v₂, v₁, u₂, u₁} D C }
          F } ≫
      f)
    ({ app := fun (X : D) ↦ (c X).snd, naturality := ⋯ :
        NatTrans
          { obj := fun (X : D) ↦ (c X).pt,
            map := fun {X Y : D} (h : X ⟶ Y) ↦
              (hc Y).lift
                { pt := (c X).pt, π := (c X).π ≫ cospanHomMk (H.map h) (F.map h) (G.map h) ⋯ ⋯ :
                  Cone (cospan (f.app Y) (g.app Y)) },
            map_id := ⋯, map_comp := ⋯ : Functor.{v₂, v₁, u₂, u₁} D C }
          G } ≫
      g)
have w : ∀ (x : D),
  Eq (α :=
    Functor.obj.{v₂, v₁, u₂, u₁}
        { obj := fun (X : D) ↦ (c X).pt,
          map := fun {X Y : D} (h : X ⟶ Y) ↦
            (hc Y).lift { pt := (c X).pt, π := (c X).π ≫ cospanHomMk (H.map h) (F.map h) (G.map h) sorry sorry },
          map_id := sorry, map_comp := sorry }
        x ⟶
      H.obj x)
    (NatTrans.app
      ({ app := fun (X : D) ↦ (c X).fst, naturality := sorry :
          NatTrans
            { obj := fun (X : D) ↦ (c X).pt,
              map := fun {X Y : D} (h : X ⟶ Y) ↦
                (hc Y).lift
                  { pt := (c X).pt, π := (c X).π ≫ cospanHomMk (H.map h) (F.map h) (G.map h) sorry sorry :
                    Cone (cospan (f.app Y) (g.app Y)) },
              map_id := sorry, map_comp := sorry : Functor.{v₂, v₁, u₂, u₁} D C }
            F } ≫
        f)
      x)
    (NatTrans.app
      ({ app := fun (X : D) ↦ (c X).snd, naturality := sorry :
          NatTrans
            { obj := fun (X : D) ↦ (c X).pt,
              map := fun {X Y : D} (h : X ⟶ Y) ↦
                (hc Y).lift
                  { pt := (c X).pt, π := (c X).π ≫ cospanHomMk (H.map h) (F.map h) (G.map h) sorry sorry :
                    Cone (cospan (f.app Y) (g.app Y)) },
              map_id := sorry, map_comp := sorry : Functor.{v₂, v₁, u₂, u₁} D C }
            G } ≫
        g)
      x)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₂, v₁, u₂, u₁} D C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
k : D
⊢ IsLimit (F := cospan f g ⋙ Functor.obj (evaluation D C) k)
    (Functor.mapCone (Functor.obj (evaluation D C) k) (combine f g c hc))
have refine_1 : cospan (f.app k) (g.app k) ≅ cospan f g ⋙ Functor.obj (evaluation D C) k
Tactic: refine IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_ (hc k)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₂, v₁, u₂, u₁} D C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
k : D
refine_1 : cospan (f.app k) (g.app k) ≅ cospan f g ⋙ Functor.obj (evaluation D C) k
⊢ IsLimit (F := cospan f g ⋙ Functor.obj (evaluation D C) k)
    (Functor.mapCone (Functor.obj (evaluation D C) k) (combine f g c hc))
have refine_2 : (Cone.postcompose
        (cospanIsoMk (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.one))
            (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.left))
            (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.right)) sorry sorry).hom).obj
    (c k) ≅
  Functor.mapCone (Functor.obj (evaluation D C) k) (combine f g c hc)
Tactic: refine IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_ (hc k)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₂, v₁, u₂, u₁} D C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
k : D
⊢ (Cone.postcompose
          (cospanIsoMk (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.one))
              (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.left))
              (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
      (c k) ≅
    Functor.mapCone (Functor.obj (evaluation D C) k) (combine f g c hc)
have refine_2 : ∀ (j : WalkingCospan),
  NatTrans.app
      ((Cone.postcompose
              (cospanIsoMk (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.one))
                  (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.left))
                  (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.right)) sorry sorry).hom).obj
          (c k)).π
      j =
    Iso.hom
        (Iso.refl
          ((Cone.postcompose
                  (cospanIsoMk (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.one))
                      (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.left))
                      (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.right)) sorry sorry).hom).obj
              (c k)).pt) ≫
      NatTrans.app (Cone.π (Functor.mapCone (Functor.obj (evaluation D C) k) (combine f g c hc))) j
Tactic: refine Cone.ext (Iso.refl _) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Terminal (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
hF : (X : C) → IsTerminal.{v_2, u_2} (F.obj X)
⊢ IsTerminal F
have refine : (X : C) →
  Iso (C :=
    Cone.{0, v_2, 0, u_2}
      (comp (D := Functor.{v_1, v_2, u_1, u_2} C D) (empty (Functor.{v_1, v_2, u_1, u_2} C D))
        (obj (evaluation C D) X)))
    (obj
      (Cone.postcompose
        (Iso.hom
          (emptyExt (empty D)
            (comp (D := Functor.{v_1, v_2, u_1, u_2} C D) (empty (Functor.{v_1, v_2, u_1, u_2} C D))
              (obj (evaluation C D) X)))))
      (asEmptyCone (F.obj X)))
    (mapCone (obj (evaluation C D) X) (asEmptyCone F))
Tactic: refine evaluationJointlyReflectsLimits _
    fun X ↦ IsLimit.equivOfNatIsoOfIso (Functor.emptyExt _ _) _ _ ?_ (hF X)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Terminal (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
hF : (X : C) → IsInitial.{v_2, u_2} (F.obj X)
⊢ IsInitial F
have refine : (X : C) →
  Iso (C :=
    Cocone.{0, v_2, 0, u_2}
      (comp (D := Functor.{v_1, v_2, u_1, u_2} C D) (empty (Functor.{v_1, v_2, u_1, u_2} C D))
        (obj (evaluation C D) X)))
    (obj
      (Cocone.precompose
        (Iso.inv
          (emptyExt (empty D)
            (comp (D := Functor.{v_1, v_2, u_1, u_2} C D) (empty (Functor.{v_1, v_2, u_1, u_2} C D))
              (obj (evaluation C D) X)))))
      (asEmptyCocone (F.obj X)))
    (mapCocone (obj (evaluation C D) X) (asEmptyCocone F))
Tactic: refine evaluationJointlyReflectsColimits _
    fun X ↦ IsColimit.equivOfNatIsoOfIso (Functor.emptyExt _ _) _ _ ?_ (hF X)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorToTypes (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
F : J ⥤ Functor.{v₂, w, u₂, w + 1} K (Type w)
k : K
t : Cocone F
h : IsColimit t
x : t.pt.obj k
inst_2 : ∀ (k : K), HasColimit (F.flip.obj k)
hev : IsColimit (F := F ⋙ Functor.obj (evaluation K (Type w)) k)
  (Functor.mapCocone (Functor.obj (evaluation K (Type w)) k) t) :=
  isColimitOfPreserves (Functor.obj (evaluation K (Type w)) k) h
⊢ ∃ (j : J) (y : (fun (X : Type w) ↦ X) ((F.obj j).obj k)),
    x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((t.ι.app j).app k) :
          (a : (fun (X : Type w) ↦ X) ((F.obj j).obj k)) →
            (fun (X : Type w) ↦ X) ((((Functor.const J).obj t.pt).obj j).obj k))
        y
have obtain : ∀ (j : J) (y : (F ⋙ Functor.obj (evaluation K (Type w)) k).obj j),
  ∃ (j_1 : J) (y_1 : (fun (X : Type w) ↦ X) ((F.obj j_1).obj k)),
    Eq (α := t.pt.obj k)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj (evaluation K (Type w)) k) t)) j) :
            (a : (fun (X : Type w) ↦ X) ((F ⋙ (evaluation K (Type w)).obj k).obj j)) →
              (fun (X : Type w) ↦ X) (((Functor.const J).obj (((evaluation K (Type w)).obj k).mapCocone t).pt).obj j))
          y :
        (fun (X : Type w) ↦ X)
          (Functor.obj.{v₁, w, u₁, w + 1}
            (Functor.obj (Functor.const J)
              (Cocone.pt (F := F ⋙ Functor.obj (evaluation K (Type w)) k)
                (Functor.mapCocone (Functor.obj (evaluation K (Type w)) k) t)))
            j))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((t.ι.app j_1).app k) :
            (a : (fun (X : Type w) ↦ X) ((F.obj j_1).obj k)) →
              (fun (X : Type w) ↦ X) ((((Functor.const J).obj t.pt).obj j_1).obj k))
          y_1 :
        (fun (X : Type w) ↦ X) ((Functor.obj (Functor.obj (Functor.const J) t.pt) j_1).obj k))
Tactic: obtain ⟨j, y, rfl⟩ := Types.jointly_surjective _ hev x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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 F : Functor.{v₁, v, u₁, u} J C
inst_3 : HasLimit F
j j' : J
hj : j = j'
⊢ F.obj j = F.obj j'
have subst : F.obj j = F.obj j
Tactic: subst hj
Cleared hypotheses: j', hj
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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
j j' : J
hj : j = j'
⊢ Eq (α := limit F ⟶ F.obj j') (π F j ≫ eqToHom ⋯) (π F j')
have subst : Eq (α := limit F ⟶ F.obj j) (π F j ≫ eqToHom sorry) (π F j)
Tactic: subst hj
Cleared hypotheses: j', hj
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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
t : LimitCone F
j : J
⊢ Eq (α := limit F ⟶ F.obj j) (Iso.hom (isoLimitCone t) ≫ t.cone.π.app j) (π F j)
have dsimp : Eq (α := limit F ⟶ F.obj j) (t.isLimit.lift (cone F) ≫ t.cone.π.app j) (π F j)
Tactic: dsimp [limit.isoLimitCone, IsLimit.conePointUniqueUpToIso]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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
t : LimitCone F
j : J
⊢ CategoryStruct.comp (Y := limit F) (Iso.inv (isoLimitCone t)) (π F j) = t.cone.π.app j
have dsimp : CategoryStruct.comp (Y := limit F) (lift F t.cone) (π F j) = t.cone.π.app j
Tactic: dsimp [limit.isoLimitCone, IsLimit.conePointUniqueUpToIso]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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
⊢ Eq (α := c.pt ⟶ limit G) (CategoryStruct.comp (Y := limit F) (lift F c) (limMap α))
    (lift G ((Cone.postcompose α).obj c))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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
⊢ 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)
have w : c.π.app j ≫ α.app j = ((Cone.postcompose α).obj c).π.app j
Tactic: rw [assoc, limMap_π, limit.lift_π_assoc, limit.lift_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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) (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))
have 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))
Tactic: simp only [HasLimit.isoOfEquivalence, IsLimit.conePointsIsoOfEquivalence_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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 (isoOfEquivalence e w)) (limit.π F j))
    (limit.π G (e.functor.obj j) ≫ w.hom.app j)
have 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)
Tactic: simp only [HasLimit.isoOfEquivalence]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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
⊢ Eq (α := c.pt ⟶ limit (E ⋙ F)) (CategoryStruct.comp (Y := limit F) (lift F c) (pre F E))
    (lift (E ⋙ F) (Cone.whisker E c))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (hypothesis)
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)
⊢ Eq (α := limit F ⟶ limit (D ⋙ E ⋙ F)) (CategoryStruct.comp (Y := limit (E ⋙ F)) (pre F E) (pre (E ⋙ F) D))
    (pre F (D ⋙ E))
have this : HasLimit ((D ⋙ E) ⋙ F)
Tactic: haveI : HasLimit ((D ⋙ E) ⋙ F) := h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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)
⊢ Eq (α := limit F ⟶ limit (D ⋙ E ⋙ F)) (CategoryStruct.comp (Y := limit (E ⋙ F)) (pre F E) (pre (E ⋙ F) D))
    (pre F (D ⋙ E))
have 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))
Tactic: ext j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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)
    (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))
have w : Eq (α := limit F ⟶ (D ⋙ E ⋙ F).obj j) (π F (E.obj (D.obj j))) (π F ((D ⋙ E).obj j))
Tactic: erw [assoc, limit.pre_π, limit.pre_π, limit.pre_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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
⊢ 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))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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
⊢ 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)
have w : G.map (c.π.app j) = (G.mapCone c).π.app j
Tactic: rw [assoc, limit.post_π, ← G.map_comp, limit.lift_π, limit.lift_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (hypothesis)
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)
⊢ 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))
have this : HasLimit (F ⋙ G ⋙ H)
Tactic: haveI : HasLimit (F ⋙ G ⋙ H) := h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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)
⊢ 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))
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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)
    (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))
have w : Eq (α := H.obj (G.obj (limit F)) ⟶ ((F ⋙ G) ⋙ H).obj j) (H.map (G.map (π F j))) ((G ⋙ H).map (π F j))
Tactic: erw [assoc, limit.post_π, ← H.map_comp, limit.post_π, limit.post_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (hypothesis)
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)
⊢ 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))
have this : HasLimit (E ⋙ F ⋙ G)
Tactic: haveI : HasLimit (E ⋙ F ⋙ G) := h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (goal)
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)
⊢ 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))
have 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))
Tactic: ext