awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Functor.{v₁, v, u₁, u} J C
L : Functor.{v₁, v, u₁, u} J C ⥤ C
adj : const J ⊣ L
F : Functor.{v₁, v, u₁, u} J C
s : Cone F
j : J
eq : L.map s.π ≫ (adj.counit.app F).app j = NatTrans.app (adj.counit.app (obj (const J) s.pt)) j ≫ s.π.app j
eq' : adj.unit.app s.pt ≫ NatTrans.app (adj.counit.app (obj (const J) s.pt)) j = 𝟙 s.pt
rw : (adj.unit.app s.pt ≫ L.map s.π) ≫ (adj.counit.app F).app j = s.π.app j
rw₁ : adj.unit.app s.pt ≫ L.map s.π ≫ (adj.counit.app F).app j = s.π.app j
rw₂ : adj.unit.app s.pt ≫ NatTrans.app (adj.counit.app (obj (const J) s.pt)) j ≫ s.π.app j = s.π.app j
⊢ (adj.homEquiv s.pt F : (a : (const J).obj s.pt ⟶ F) → s.pt ⟶ L.obj F) s.π ≫ (adj.counit.app F).app j = s.π.app j
have rw₃ : s.π.app j = s.π.app j
Tactic: rw [adj.homEquiv_unit, assoc, eq, reassoc_of% eq']
-- 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 : Functor.{v₁, v, u₁, u} J C
L : Functor.{v₁, v, u₁, u} J C ⥤ C
adj : const J ⊣ L
F : Functor.{v₁, v, u₁, u} J C
s : Cone F
m : s.pt ⟶ (coneOfAdj adj F).pt
hm : ∀ (j : J), m ≫ (coneOfAdj adj F).π.app j = s.π.app j
⊢ Eq (α := obj (const J) s.pt ⟶ F)
    ((Equiv.symm (adj.homEquiv s.pt F) : (a : s.pt ⟶ L.obj F) → (const J).obj s.pt ⟶ F) m : obj (const J) s.pt ⟶ F)
    ((Equiv.symm (adj.homEquiv s.pt F) : (a : s.pt ⟶ L.obj F) → (const J).obj s.pt ⟶ F)
        ((adj.homEquiv s.pt F : (a : (const J).obj s.pt ⟶ F) → s.pt ⟶ L.obj F) s.π) :
      obj (const J) s.pt ⟶ F)
have w : ∀ (j : J),
  Eq.{v + 1} (α := obj.{v₁, v, u₁, u} (obj (const J) s.pt) j ⟶ F.obj j)
    (NatTrans.app ((Equiv.symm (adj.homEquiv s.pt F) : (a : s.pt ⟶ L.obj F) → (const J).obj s.pt ⟶ F) m) j)
    (NatTrans.app
      ((Equiv.symm (adj.homEquiv s.pt F) : (a : s.pt ⟶ L.obj F) → (const J).obj s.pt ⟶ F)
        ((adj.homEquiv s.pt F : (a : (const J).obj s.pt ⟶ F) → s.pt ⟶ L.obj F) s.π))
      j)
Tactic: ext j
-- 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
J' : Type u₂
inst_2 : Category.{v₂, u₂} J'
e : Equivalence.{v₁, v₂, u₁, u₂} J J'
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} J C
⊢ HasLimitsOfShape.{v₂, u₂, v, u} J' C
have has_limit : autoParam (∀ (F : Functor.{v₂, v, u₂, u} J' C), HasLimit F) HasLimitsOfShape.has_limit._autoParam
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimitsOfSize.{v₁, u₁, v, u} C
J : Type u₂
inst_2 : Category.{v₂, u₂} J
inst_3 : Small.{u₁, u₂} J
inst_4 : LocallySmall.{v₁, v₂, u₂} J
⊢ HasLimitsOfShape.{v₂, u₂, v, u} J C
have this : HasLimitsOfShape.{v₁, u₁, v, u} (ShrinkHoms.{u₁} (Shrink.{u₁, u₂} J)) C
Tactic: have := HasLimitsOfSize.has_limits_of_shape (C := C) (ShrinkHoms (Shrink.{u₁} J))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.HasLimits (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimitsOfSize.{v₁, u₁, v, u} C
J : Type u₂
inst_2 : Category.{v₂, u₂} J
inst_3 : EssentiallySmall.{u₁, v₂, u₂} J
inst_4 : LocallySmall.{v₁, v₂, u₂} J
⊢ HasLimitsOfShape.{v₂, u₂, v, u} J C
have this : HasLimitsOfShape.{u₁, u₁, v, u} (SmallModel.{u₁, v₂, u₂} J) C
Tactic: have := HasLimitsOfShape.of_small.{v₁, u₁} C (SmallModel.{u₁} 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_1 F : Functor.{v₁, v, u₁, u} J C
inst_3 : HasColimit 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 : HasColimit F
j j' : J
hj : j = j'
⊢ Eq (α := F.obj j' ⟶ colimit F) (eqToHom ⋯ ≫ ι F j) (ι F j')
have subst : Eq (α := F.obj j ⟶ colimit F) (eqToHom sorry ≫ ι F j) (ι 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 : HasColimit F
t : ColimitCocone F
j : J
⊢ CategoryStruct.comp (Y := colimit F) (ι F j) (Iso.hom (isoColimitCocone t)) = t.cocone.ι.app j
have dsimp : CategoryStruct.comp (Y := colimit F) (ι F j) (desc F t.cocone) = t.cocone.ι.app j
Tactic: dsimp [colimit.isoColimitCocone, IsColimit.coconePointUniqueUpToIso]
-- 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 : HasColimit F
t : ColimitCocone F
j : J
⊢ Eq (α := F.obj j ⟶ colimit F) (t.cocone.ι.app j ≫ Iso.inv (isoColimitCocone t)) (ι F j)
have dsimp : Eq (α := F.obj j ⟶ colimit F) (t.cocone.ι.app j ≫ t.isColimit.desc (cocone F)) (ι F j)
Tactic: dsimp [colimit.isoColimitCocone, IsColimit.coconePointUniqueUpToIso]
-- 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 : HasColimit F
c : Cocone F
X : C
f : c.pt ⟶ X
⊢ Eq (α := colimit F ⟶ (c.extend f).pt) (desc F (c.extend f)) (desc F c ≫ f)
have w : ∀ (j : J),
  CategoryStruct.comp (Y := colimit F) (ι F j) (desc F (c.extend f)) =
    CategoryStruct.comp (Y := colimit F) (ι F j) (desc F c ≫ f)
Tactic: ext
-- 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 : HasColimit F
E : Functor.{v₂, v₁, u₂, u₁} K J
inst_4 : HasColimit (E ⋙ F)
c : Cocone F
⊢ Eq (α := colimit (E ⋙ F) ⟶ c.pt) (CategoryStruct.comp (Y := colimit F) (pre F E) (desc F c))
    (desc (E ⋙ F) (Cocone.whisker E c))
have w : ∀ (j : K),
  CategoryStruct.comp (Y := colimit (E ⋙ F)) (ι (E ⋙ F) j) (CategoryStruct.comp (Y := colimit F) (pre F E) (desc F c)) =
    CategoryStruct.comp (Y := colimit (E ⋙ F)) (ι (E ⋙ F) j) (desc (E ⋙ F) (Cocone.whisker E c))
Tactic: ext
-- 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 : HasColimit F
E : Functor.{v₂, v₁, u₂, u₁} K J
inst_4 : HasColimit (E ⋙ F)
L : Type u₃
inst_5 : Category.{v₃, u₃} L
D : Functor.{v₃, v₂, u₃, u₂} L K
h : HasColimit (D ⋙ E ⋙ F)
⊢ Eq (α := colimit (D ⋙ E ⋙ F) ⟶ colimit F) (CategoryStruct.comp (Y := colimit (E ⋙ F)) (pre (E ⋙ F) D) (pre F E))
    (pre F (D ⋙ E))
have w : ∀ (j : L),
  Eq (α := (D ⋙ E ⋙ F).obj j ⟶ colimit F)
    (CategoryStruct.comp (Y := colimit (D ⋙ E ⋙ F)) (ι (D ⋙ E ⋙ F) j)
      (CategoryStruct.comp (Y := colimit (E ⋙ F)) (pre (E ⋙ F) D) (pre F E)))
    (CategoryStruct.comp (Y := colimit (D ⋙ E ⋙ F)) (ι (D ⋙ E ⋙ F) j) (pre F (D ⋙ E)))
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 : HasColimit F
E : Functor.{v₂, v₁, u₂, u₁} K J
inst_4 : HasColimit (E ⋙ F)
L : Type u₃
inst_5 : Category.{v₃, u₃} L
D : Functor.{v₃, v₂, u₃, u₂} L K
h : HasColimit (D ⋙ E ⋙ F)
j : L
⊢ Eq (α := (D ⋙ E ⋙ F).obj j ⟶ colimit F)
    (CategoryStruct.comp (Y := colimit (D ⋙ E ⋙ F)) (ι (D ⋙ E ⋙ F) j)
      (CategoryStruct.comp (Y := colimit (E ⋙ F)) (pre (E ⋙ F) D) (pre F E)))
    (CategoryStruct.comp (Y := colimit (D ⋙ E ⋙ F)) (ι (D ⋙ E ⋙ F) j) (pre F (D ⋙ E)))
have w : Eq (α := (D ⋙ E ⋙ F).obj j ⟶ colimit F) (ι F (E.obj (D.obj j)))
  (CategoryStruct.comp (Y := colimit (D ⋙ E ⋙ F)) (ι (D ⋙ E ⋙ F) j) (pre F (D ⋙ E)))
Tactic: rw [← assoc, colimit.ι_pre, colimit.ι_pre]
-- 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 : HasColimit F
E : Functor.{v₂, v₁, u₂, u₁} K J
inst_4 : HasColimit (E ⋙ F)
L : Type u₃
inst_5 : Category.{v₃, u₃} L
D : Functor.{v₃, v₂, u₃, u₂} L K
h : HasColimit (D ⋙ E ⋙ F)
j : L
⊢ Eq (α := (D ⋙ E ⋙ F).obj j ⟶ colimit F) (ι F (E.obj (D.obj j)))
    (CategoryStruct.comp (Y := colimit (D ⋙ E ⋙ F)) (ι (D ⋙ E ⋙ F) j) (pre F (D ⋙ E)))
have this : HasColimit ((D ⋙ E) ⋙ F)
Tactic: haveI : HasColimit ((D ⋙ E) ⋙ F) := 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
F : Functor.{v₁, v, u₁, u} J C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasColimit F
G : Functor.{v, v', u, u'} C D
inst_4 : HasColimit (F ⋙ G)
c : Cocone F
⊢ Eq (α := colimit (F ⋙ G) ⟶ G.obj c.pt) (CategoryStruct.comp (Y := G.obj (colimit F)) (post F G) (G.map (desc F c)))
    (desc (F ⋙ G) (G.mapCocone c))
have w : ∀ (j : J),
  CategoryStruct.comp (Y := colimit (F ⋙ G)) (ι (F ⋙ G) j)
      (CategoryStruct.comp (Y := G.obj (colimit F)) (post F G) (G.map (desc F c))) =
    CategoryStruct.comp (Y := colimit (F ⋙ G)) (ι (F ⋙ G) j) (desc (F ⋙ G) (G.mapCocone c))
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 : Functor.{v₁, v, u₁, u} J C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasColimit F
G : Functor.{v, v', u, u'} C D
inst_4 : HasColimit (F ⋙ G)
c : Cocone F
j : J
⊢ CategoryStruct.comp (Y := colimit (F ⋙ G)) (ι (F ⋙ G) j)
      (CategoryStruct.comp (Y := G.obj (colimit F)) (post F G) (G.map (desc F c))) =
    CategoryStruct.comp (Y := colimit (F ⋙ G)) (ι (F ⋙ G) j) (desc (F ⋙ G) (G.mapCocone c))
have w : G.map (c.ι.app j) = (G.mapCocone c).ι.app j
Tactic: rw [← assoc, colimit.ι_post, ← G.map_comp, colimit.ι_desc, colimit.ι_desc]
-- 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
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasColimit F
G : Functor.{v, v', u, u'} C D
inst_4 : HasColimit (F ⋙ G)
E : Type u''
inst_5 : Category.{v'', u''} E
H : Functor.{v', v'', u', u''} D E
h : HasColimit ((F ⋙ G) ⋙ H)
⊢ Eq (α := colimit ((F ⋙ G) ⋙ H) ⟶ H.obj (G.obj (colimit F)))
    (CategoryStruct.comp (Y := H.obj (colimit (F ⋙ G))) (post (F ⋙ G) H) (H.map (post F G))) (post F (G ⋙ H))
have w : ∀ (j : J),
  Eq (α := ((F ⋙ G) ⋙ H).obj j ⟶ H.obj (G.obj (colimit F)))
    (CategoryStruct.comp (Y := colimit ((F ⋙ G) ⋙ H)) (ι ((F ⋙ G) ⋙ H) j)
      (CategoryStruct.comp (Y := H.obj (colimit (F ⋙ G))) (post (F ⋙ G) H) (H.map (post F G))))
    (CategoryStruct.comp (Y := colimit ((F ⋙ G) ⋙ H)) (ι ((F ⋙ G) ⋙ H) j) (post F (G ⋙ H)))
Tactic: ext j
-- 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
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasColimit F
G : Functor.{v, v', u, u'} C D
inst_4 : HasColimit (F ⋙ G)
E : Type u''
inst_5 : Category.{v'', u''} E
H : Functor.{v', v'', u', u''} D E
h : HasColimit ((F ⋙ G) ⋙ H)
j : J
⊢ Eq (α := ((F ⋙ G) ⋙ H).obj j ⟶ H.obj (G.obj (colimit F)))
    (CategoryStruct.comp (Y := colimit ((F ⋙ G) ⋙ H)) (ι ((F ⋙ G) ⋙ H) j)
      (CategoryStruct.comp (Y := H.obj (colimit (F ⋙ G))) (post (F ⋙ G) H) (H.map (post F G))))
    (CategoryStruct.comp (Y := colimit ((F ⋙ G) ⋙ H)) (ι ((F ⋙ G) ⋙ H) j) (post F (G ⋙ H)))
have w : Eq (α := ((F ⋙ G) ⋙ H).obj j ⟶ H.obj (G.obj (colimit F))) (H.map (G.map (ι F j)))
  (CategoryStruct.comp (Y := colimit ((F ⋙ G) ⋙ H)) (ι ((F ⋙ G) ⋙ H) j) (post F (G ⋙ H)))
Tactic: rw [← assoc, colimit.ι_post, ← H.map_comp, colimit.ι_post]
-- 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
F : Functor.{v₁, v, u₁, u} J C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasColimit F
G : Functor.{v, v', u, u'} C D
inst_4 : HasColimit (F ⋙ G)
E : Type u''
inst_5 : Category.{v'', u''} E
H : Functor.{v', v'', u', u''} D E
h : HasColimit ((F ⋙ G) ⋙ H)
j : J
⊢ Eq (α := ((F ⋙ G) ⋙ H).obj j ⟶ H.obj (G.obj (colimit F))) (H.map (G.map (ι F j)))
    (CategoryStruct.comp (Y := colimit ((F ⋙ G) ⋙ H)) (ι ((F ⋙ G) ⋙ H) j) (post F (G ⋙ H)))
have this : HasColimit (F ⋙ G ⋙ H)
Tactic: haveI : HasColimit (F ⋙ G ⋙ H) := 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 : HasColimit F
inst_5 : HasColimit (E ⋙ F)
inst_6 : HasColimit (F ⋙ G)
h : HasColimit ((E ⋙ F) ⋙ G)
⊢ Eq (α := colimit ((E ⋙ F) ⋙ G) ⟶ G.obj (colimit F))
    (CategoryStruct.comp (Y := G.obj (colimit (E ⋙ F))) (post (E ⋙ F) G) (G.map (pre F E)))
    (CategoryStruct.comp (Y := colimit (F ⋙ G)) (pre (F ⋙ G) E) (post F G))
have w : ∀ (j : K),
  Eq (α := ((E ⋙ F) ⋙ G).obj j ⟶ G.obj (colimit F))
    (CategoryStruct.comp (Y := colimit ((E ⋙ F) ⋙ G)) (ι ((E ⋙ F) ⋙ G) j)
      (CategoryStruct.comp (Y := G.obj (colimit (E ⋙ F))) (post (E ⋙ F) G) (G.map (pre F E))))
    (CategoryStruct.comp (Y := colimit ((E ⋙ F) ⋙ G)) (ι ((E ⋙ F) ⋙ G) j)
      (CategoryStruct.comp (Y := colimit (F ⋙ G)) (pre (F ⋙ G) E) (post F G)))
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
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 : HasColimit F
inst_5 : HasColimit (E ⋙ F)
inst_6 : HasColimit (F ⋙ G)
h : HasColimit ((E ⋙ F) ⋙ G)
j : K
⊢ Eq (α := ((E ⋙ F) ⋙ G).obj j ⟶ G.obj (colimit F))
    (CategoryStruct.comp (Y := colimit ((E ⋙ F) ⋙ G)) (ι ((E ⋙ F) ⋙ G) j)
      (CategoryStruct.comp (Y := G.obj (colimit (E ⋙ F))) (post (E ⋙ F) G) (G.map (pre F E))))
    (CategoryStruct.comp (Y := colimit ((E ⋙ F) ⋙ G)) (ι ((E ⋙ F) ⋙ G) j)
      (CategoryStruct.comp (Y := colimit (F ⋙ G)) (pre (F ⋙ G) E) (post F G)))
have w : Eq (α := ((E ⋙ F) ⋙ G).obj j ⟶ G.obj (colimit F)) (G.map (ι F (E.obj j)))
  (CategoryStruct.comp (Y := colimit (F ⋙ G))
    (CategoryStruct.comp (Y := colimit ((E ⋙ F) ⋙ G)) (ι ((E ⋙ F) ⋙ G) j) (pre (F ⋙ G) E)) (post F G))
Tactic: rw [← assoc, colimit.ι_post, ← G.map_comp, colimit.ι_pre, ← assoc]
-- 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 : HasColimit F
inst_5 : HasColimit (E ⋙ F)
inst_6 : HasColimit (F ⋙ G)
h : HasColimit ((E ⋙ F) ⋙ G)
j : K
⊢ Eq (α := ((E ⋙ F) ⋙ G).obj j ⟶ G.obj (colimit F)) (G.map (ι F (E.obj j)))
    (CategoryStruct.comp (Y := colimit (F ⋙ G))
      (CategoryStruct.comp (Y := colimit ((E ⋙ F) ⋙ G)) (ι ((E ⋙ F) ⋙ G) j) (pre (F ⋙ G) E)) (post F G))
have this : HasColimit (E ⋙ F ⋙ G)
Tactic: haveI : HasColimit (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 : HasColimit F
inst_5 : HasColimit (E ⋙ F)
inst_6 : HasColimit (F ⋙ G)
h : HasColimit ((E ⋙ F) ⋙ G)
j : K
this : HasColimit (E ⋙ F ⋙ G)
⊢ Eq (α := ((E ⋙ F) ⋙ G).obj j ⟶ G.obj (colimit F)) (G.map (ι F (E.obj j)))
    (CategoryStruct.comp (Y := colimit (F ⋙ G))
      (CategoryStruct.comp (Y := colimit ((E ⋙ F) ⋙ G)) (ι ((E ⋙ F) ⋙ G) j) (pre (F ⋙ G) E)) (post F G))
have w : Eq (α := ((E ⋙ F) ⋙ G).obj j ⟶ G.obj (colimit F)) (G.map (ι F (E.obj j)))
  (CategoryStruct.comp (Y := colimit (F ⋙ G)) (ι (F ⋙ G) (E.obj j)) (post F G))
Tactic: erw [colimit.ι_pre (F ⋙ G) E j, colimit.ι_post]
-- 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 : HasColimit F
inst_5 : HasColimit (E ⋙ F)
inst_6 : HasColimit (F ⋙ G)
h : HasColimit ((E ⋙ F) ⋙ G)
j : K
this : HasColimit (E ⋙ F ⋙ G)
w :
  Eq (α := ((E ⋙ F) ⋙ G).obj j ⟶ G.obj (colimit F)) (G.map (ι F (E.obj j)))
    (CategoryStruct.comp (Y := colimit (F ⋙ G)) (ι (F ⋙ G) (E.obj j)) (post F G))
⊢ Eq (α := ((E ⋙ F) ⋙ G).obj j ⟶ G.obj (colimit F)) (G.map (ι F (E.obj j)))
    (CategoryStruct.comp (Y := colimit (F ⋙ G))
      (CategoryStruct.comp (Y := colimit ((E ⋙ F) ⋙ G)) (ι ((E ⋙ F) ⋙ G) j) (pre (F ⋙ G) E)) (post F G))
have w₁ : Eq (α := ((E ⋙ F) ⋙ G).obj j ⟶ G.obj (colimit F)) (G.map (ι F (E.obj j))) (G.map (ι F (E.obj j)))
Tactic: erw [colimit.ι_pre (F ⋙ G) E j, colimit.ι_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
F : Functor.{v₁, v, u₁, u} J C
e : Equivalence.{v₂, v₁, u₂, u₁} K J
inst_3 : HasColimit (e.functor ⋙ F)
⊢ HasColimit F
have this : HasColimit (e.inverse ⋙ e.functor ⋙ F)
Tactic: haveI : HasColimit (e.inverse ⋙ e.functor ⋙ F) := Limits.hasColimit_equivalence_comp e.symm
-- 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 : HasColimitsOfShape.{v₁, u₁, v, u} J C
G : Functor.{v₁, v, u₁, u} J C
α : F ⟶ G
c : Cocone G
⊢ Eq (α := colimit F ⟶ c.pt) (CategoryStruct.comp (Y := colimit G) (colimMap α) (desc G c))
    (desc F ((Cocone.precompose α).obj c))
have w : ∀ (j : J),
  CategoryStruct.comp (Y := colimit F) (ι F j) (CategoryStruct.comp (Y := colimit G) (colimMap α) (desc G c)) =
    CategoryStruct.comp (Y := colimit F) (ι F j) (desc F ((Cocone.precompose α).obj c))
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 : HasColimitsOfShape.{v₁, u₁, v, u} J C
G : Functor.{v₁, v, u₁, u} J C
α : F ⟶ G
inst_4 : HasColimitsOfShape.{v₂, u₂, v, u} K C
E : Functor.{v₂, v₁, u₂, u₁} K J
⊢ Eq (α := colimit (E ⋙ F) ⟶ obj colim G) (CategoryStruct.comp (Y := colimit F) (pre F E) (map colim α))
    (map colim (E.whiskerLeft α) ≫ pre G E)
have w : ∀ (j : K),
  Eq (α := (E ⋙ F).obj j ⟶ obj colim G)
    (CategoryStruct.comp (Y := colimit (E ⋙ F)) (ι (E ⋙ F) j)
      (CategoryStruct.comp (Y := colimit F) (pre F E) (map colim α)))
    (CategoryStruct.comp (Y := colimit (E ⋙ F)) (ι (E ⋙ F) j) (map colim (E.whiskerLeft α) ≫ pre G E))
Tactic: ext
-- 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 : HasColimitsOfShape.{v₁, u₁, v, u} J C
G : Functor.{v₁, v, u₁, u} J C
α : F ⟶ G
inst_4 : HasColimitsOfShape.{v₂, u₂, v, u} K C
E : Functor.{v₂, v₁, u₂, u₁} K J
j : K
⊢ Eq (α := (E ⋙ F).obj j ⟶ obj colim G)
    (CategoryStruct.comp (Y := colimit (E ⋙ F)) (ι (E ⋙ F) j)
      (CategoryStruct.comp (Y := colimit F) (pre F E) (map colim α)))
    (CategoryStruct.comp (Y := colimit (E ⋙ F)) (ι (E ⋙ F) j) (map colim (E.whiskerLeft α) ≫ pre G E))
have w : Eq (α := (E ⋙ F).obj j ⟶ obj colim G) (α.app (E.obj j) ≫ ι G (E.obj j)) ((E.whiskerLeft α).app j ≫ ι G (E.obj j))
Tactic: rw [← assoc, colimit.ι_pre, colimit.ι_map, ← assoc, colimit.ι_map, assoc, colimit.ι_pre]
-- 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
inst_3 : HasColimitsOfShape.{v₁, u₁, v, u} J C
inst_4 : HasColimitsOfShape.{v₂, u₂, v, u} K C
F : Functor.{v₁, v, u₁, u} J C
E₁ E₂ : Functor.{v₂, v₁, u₂, u₁} K J
α : E₁ ⟶ E₂
⊢ Eq (α := colimit (E₁ ⋙ F) ⟶ colimit F) (pre F E₁) (map colim (whiskerRight α F) ≫ pre F E₂)
have w : ∀ (j : K),
  Eq (α := (E₁ ⋙ F).obj j ⟶ colimit F) (CategoryStruct.comp (Y := colimit (E₁ ⋙ F)) (ι (E₁ ⋙ F) j) (pre F E₁))
    (CategoryStruct.comp (Y := colimit (E₁ ⋙ F)) (ι (E₁ ⋙ F) j) (map colim (whiskerRight α F) ≫ pre F E₂))
Tactic: ext1
-- 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 : HasColimitsOfShape.{v₁, u₁, v, u} J C
G : Functor.{v₁, v, u₁, u} J C
α : F ⟶ G
D : Type u'
inst_3 : Category.{v', u'} D
inst_4 : HasColimitsOfShape.{v₁, u₁, v', u'} J D
H : Functor.{v, v', u, u'} C D
⊢ Eq (α := colimit (F ⋙ H) ⟶ H.obj (obj colim G))
    (CategoryStruct.comp (Y := H.obj (colimit F)) (post F H) (H.map (map colim α)))
    (map colim (whiskerRight α H) ≫ post G H)
have w : ∀ (j : J),
  Eq (α := (F ⋙ H).obj j ⟶ H.obj (obj colim G))
    (CategoryStruct.comp (Y := colimit (F ⋙ H)) (ι (F ⋙ H) j)
      (CategoryStruct.comp (Y := H.obj (colimit F)) (post F H) (H.map (map colim α))))
    (CategoryStruct.comp (Y := colimit (F ⋙ H)) (ι (F ⋙ H) j) (map colim (whiskerRight α H) ≫ post G H))
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 : Functor.{v₁, v, u₁, u} J C
inst_2 : HasColimitsOfShape.{v₁, u₁, v, u} J C
G : Functor.{v₁, v, u₁, u} J C
α : F ⟶ G
D : Type u'
inst_3 : Category.{v', u'} D
inst_4 : HasColimitsOfShape.{v₁, u₁, v', u'} J D
H : Functor.{v, v', u, u'} C D
j : J
⊢ Eq (α := (F ⋙ H).obj j ⟶ H.obj (obj colim G))
    (CategoryStruct.comp (Y := colimit (F ⋙ H)) (ι (F ⋙ H) j)
      (CategoryStruct.comp (Y := H.obj (colimit F)) (post F H) (H.map (map colim α))))
    (CategoryStruct.comp (Y := colimit (F ⋙ H)) (ι (F ⋙ H) j) (map colim (whiskerRight α H) ≫ post G H))
have w : Eq (α := (F ⋙ H).obj j ⟶ H.obj (obj colim G)) (H.map (α.app j) ≫ H.map (ι G j))
  (CategoryStruct.comp (Y := colimit (F ⋙ H)) (ι (F ⋙ H) j) (map colim (whiskerRight α H) ≫ post G H))
Tactic: rw [← assoc, colimit.ι_post, ← H.map_comp, colimit.ι_map, H.map_comp]
-- 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 : HasColimitsOfShape.{v₁, u₁, v, u} J C
G : Functor.{v₁, v, u₁, u} J C
α : F ⟶ G
D : Type u'
inst_3 : Category.{v', u'} D
inst_4 : HasColimitsOfShape.{v₁, u₁, v', u'} J D
H : Functor.{v, v', u, u'} C D
j : J
⊢ Eq (α := (F ⋙ H).obj j ⟶ H.obj (obj colim G)) (H.map (α.app j) ≫ H.map (ι G j))
    (CategoryStruct.comp (Y := colimit (F ⋙ H)) (ι (F ⋙ H) j) (map colim (whiskerRight α H) ≫ post G H))
have w : Eq (α := (F ⋙ H).obj j ⟶ H.obj (obj colim G)) (H.map (α.app j) ≫ H.map (ι G j))
  ((whiskerRight α H).app j ≫ H.map (ι G j))
Tactic: rw [← assoc, colimit.ι_map, assoc, colimit.ι_post]