awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
t : Cone F
X : C
h : F.cones.RepresentableBy X
s : Cone F
m : s.pt ⟶ (limitCone h).pt
w : ∀ (j : J), m ≫ (limitCone h).π.app j = s.π.app j
⊢ homOfCone h (coneOfHom h m) = homOfCone h s
have h₁ : coneOfHom h m = s
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
t : Cone F
X : C
h : F.cones.RepresentableBy X
s : Cone F
m : s.pt ⟶ (limitCone h).pt
w : ∀ (j : J), m ≫ (limitCone h).π.app j = s.π.app j
⊢ coneOfHom h m = s
have h₁ : (limitCone h).extend m = s
Tactic: rw [coneOfHom_fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
t : Cone F
X : C
h : F.cones.RepresentableBy X
s : Cone F
m : s.pt ⟶ (limitCone h).pt
w : ∀ (j : J), m ≫ (limitCone h).π.app j = s.π.app j
⊢ { pt := s.pt, π := Functor.map (const J) m ≫ (limitCone h).π : Cone F } = s
have h₁ : ∀ (pt : C) (π : obj (const J) pt ⟶ F) (m : { pt := pt, π := π : Cone F }.pt ⟶ (limitCone h).pt)
  (w : ∀ (j : J), m ≫ (limitCone h).π.app j = { pt := pt, π := π }.π.app j),
  { pt := { pt := pt, π := π : Cone F }.pt, π := Functor.map (const J) m ≫ (limitCone h).π : Cone F } =
    { pt := pt, π := π }
Tactic: cases s
Cleared hypotheses: s, m, w
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
t : Cone F
X : C
h : F.cones.RepresentableBy X
pt : C
π : obj (const J) pt ⟶ F
m : { pt := pt, π := π : Cone F }.pt ⟶ (limitCone h).pt
w : ∀ (j : J), m ≫ (limitCone h).π.app j = { pt := pt, π := π }.π.app j
⊢ { pt := { pt := pt, π := π : Cone F }.pt, π := Functor.map (const J) m ≫ (limitCone h).π : Cone F } =
    { pt := pt, π := π }
have h₁ : ∀ (j : J), (Functor.map (const J) m ≫ (limitCone h).π).app j = π.app j
Tactic: congr with j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
t : Cocone F
P Q : IsColimit t
⊢ P = Q
have mk : ∀ (desc : (s : Cocone F) → t.pt ⟶ s.pt) (fac : ∀ (s : Cocone F) (j : J), t.ι.app j ≫ desc s = s.ι.app j)
  (uniq : ∀ (s : Cocone F) (m : t.pt ⟶ s.pt), (∀ (j : J), t.ι.app j ≫ m = s.ι.app j) → m = desc s),
  { desc := desc, fac := fac, uniq := uniq : IsColimit t } = Q
Tactic: cases P
Cleared hypotheses: P
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
t : Cocone F
Q : IsColimit t
desc : (s : Cocone F) → t.pt ⟶ s.pt
fac : ∀ (s : Cocone F) (j : J), t.ι.app j ≫ desc s = s.ι.app j
uniq : ∀ (s : Cocone F) (m : t.pt ⟶ s.pt), (∀ (j : J), t.ι.app j ≫ m = s.ι.app j) → m = desc s
⊢ { desc := desc, fac := fac, uniq := uniq : IsColimit t } = Q
have mk : ∀ (desc_1 : (s : Cocone F) → t.pt ⟶ s.pt) (fac_1 : ∀ (s : Cocone F) (j : J), t.ι.app j ≫ desc_1 s = s.ι.app j)
  (uniq_1 : ∀ (s : Cocone F) (m : t.pt ⟶ s.pt), (∀ (j : J), t.ι.app j ≫ m = s.ι.app j) → m = desc_1 s),
  { desc := desc, fac := fac, uniq := uniq : IsColimit t } = { desc := desc_1, fac := fac_1, uniq := uniq_1 }
Tactic: cases Q
Cleared hypotheses: Q
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
t : Cocone F
desc : (s : Cocone F) → t.pt ⟶ s.pt
fac : ∀ (s : Cocone F) (j : J), t.ι.app j ≫ desc s = s.ι.app j
uniq : ∀ (s : Cocone F) (m : t.pt ⟶ s.pt), (∀ (j : J), t.ι.app j ≫ m = s.ι.app j) → m = desc s
desc_1 : (s : Cocone F) → t.pt ⟶ s.pt
fac_1 : ∀ (s : Cocone F) (j : J), t.ι.app j ≫ desc_1 s = s.ι.app j
uniq_1 : ∀ (s : Cocone F) (m : t.pt ⟶ s.pt), (∀ (j : J), t.ι.app j ≫ m = s.ι.app j) → m = desc_1 s
⊢ { desc := desc, fac := fac, uniq := uniq : IsColimit t } = { desc := desc_1, fac := fac_1, uniq := uniq_1 }
have mk : desc = desc_1
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
s t : Cocone F
h : IsColimit t
f f' g : t ⟶ s
⊢ g = h.descCoconeMorphism s
have w : g.hom = (h.descCoconeMorphism s).hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
t : Cocone F
ht : ∀ (s : Cocone F), ∃! d : t.pt ⟶ s.pt, ∀ (j : J), t.ι.app j ≫ d = s.ι.app j
⊢ IsColimit t
have choose : (s : (s : Cocone F) → t.pt ⟶ s.pt) →
  (hs : ∀ (s_1 : Cocone F), (fun (d : t.pt ⟶ s_1.pt) ↦ ∀ (j : J), t.ι.app j ≫ d = s_1.ι.app j) (s s_1)) →
    (hs' :
        ∀ (s_1 : Cocone F) (y : t.pt ⟶ s_1.pt),
          (fun (d : t.pt ⟶ s_1.pt) ↦ ∀ (j : J), t.ι.app j ≫ d = s_1.ι.app j) y → y = s s_1) →
      IsColimit t
Tactic: choose s hs hs' using ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
r t : Cocone F
P : IsColimit r
i : r ≅ t
s : Cocone F
m : t ⟶ s
⊢ m = (fun (s : Cocone F) ↦ i.inv ≫ P.descCoconeMorphism s) s
have rw : i.hom ≫ m = P.descCoconeMorphism s
Tactic: rw [i.eq_inv_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
r t : Cocone F
P : IsColimit r
i : IsIso (P.desc t)
⊢ r ≅ t
have this : IsIso (P.descCoconeMorphism t).hom
Tactic: haveI : IsIso (P.descCoconeMorphism t).hom := i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
r t : Cocone F
P : IsColimit r
i : IsIso (P.desc t)
this : IsIso (P.descCoconeMorphism t).hom
⊢ r ≅ t
have this₁ : IsIso (P.descCoconeMorphism t)
Tactic: haveI : IsIso (P.descCoconeMorphism t) := Cocone.cocone_iso_of_hom_iso _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
t : Cocone F
h : IsColimit t
W : C
f f' : t.pt ⟶ W
w : ∀ (j : J), t.ι.app j ≫ f = t.ι.app j ≫ f'
⊢ f = f'
have rw : Eq (α := t.pt ⟶ W)
  (h.desc { pt := W, ι := { app := fun (b : J) ↦ t.ι.app b ≫ f, naturality := sorry : NatTrans F (obj (const J) W) } } :
    t.pt ⟶
      { pt := W, ι := { app := fun (b : J) ↦ t.ι.app b ≫ f, naturality := sorry : NatTrans F (obj (const J) W) } :
          Cocone F }.pt)
  (h.desc { pt := W, ι := { app := fun (b : J) ↦ t.ι.app b ≫ f', naturality := sorry : NatTrans F (obj (const J) W) } })
Tactic: rw [h.hom_desc f, h.hom_desc f']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
t : Cocone F
h : IsColimit t
W : C
f f' : t.pt ⟶ W
w : ∀ (j : J), t.ι.app j ≫ f = t.ι.app j ≫ f'
⊢ Eq (α := t.pt ⟶ W)
    (h.desc { pt := W, ι := { app := fun (b : J) ↦ t.ι.app b ≫ f, naturality := ⋯ : NatTrans F (obj (const J) W) } } :
      t.pt ⟶
        { pt := W, ι := { app := fun (b : J) ↦ t.ι.app b ≫ f, naturality := ⋯ : NatTrans F (obj (const J) W) } :
            Cocone F }.pt)
    (h.desc { pt := W, ι := { app := fun (b : J) ↦ t.ι.app b ≫ f', naturality := ⋯ : NatTrans F (obj (const J) W) } })
have h₁ : Eq (α := (X : J) → F.obj X ⟶ obj.{v₁, v₃, u₁, u₃} (obj (const J) W) X) (fun (b : J) ↦ t.ι.app b ≫ f) fun (b : J) ↦
  t.ι.app b ≫ f'
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
t_1 : Cocone F_1
F : Functor.{v₁, v₃, u₁, u₃} J C
s : Cocone F
G : Functor.{v₂, v₃, u₂, u₃} K C
t : Cocone G
P : IsColimit s
Q : IsColimit t
e : Equivalence.{v₁, v₂, u₁, u₂} J K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
⊢ CategoryStruct.comp (Y := t.pt)
      (P.desc ((Cocone.equivalenceOfReindexing e w).functor.obj t) :
        s.pt ⟶ ((Cocone.equivalenceOfReindexing e w).functor.obj t).pt)
      (Q.desc ((Cocone.equivalenceOfReindexing e.symm w').functor.obj s)) =
    𝟙 s.pt
have apply : ∀ (j : J),
  s.ι.app j ≫
      CategoryStruct.comp (Y := t.pt)
        (P.desc ((Cocone.equivalenceOfReindexing e w).functor.obj t) :
          s.pt ⟶ ((Cocone.equivalenceOfReindexing e w).functor.obj t).pt)
        (Q.desc ((Cocone.equivalenceOfReindexing e.symm w').functor.obj s)) =
    s.ι.app j ≫ 𝟙 s.pt
Tactic: apply hom_ext P
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
t_1 : Cocone F_1
F : Functor.{v₁, v₃, u₁, u₃} J C
s : Cocone F
G : Functor.{v₂, v₃, u₂, u₃} K C
t : Cocone G
P : IsColimit s
Q : IsColimit t
e : Equivalence.{v₁, v₂, u₁, u₂} J K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
j : J
⊢ s.ι.app j ≫
      CategoryStruct.comp (Y := t.pt)
        (P.desc ((Cocone.equivalenceOfReindexing e w).functor.obj t) :
          s.pt ⟶ ((Cocone.equivalenceOfReindexing e w).functor.obj t).pt)
        (Q.desc ((Cocone.equivalenceOfReindexing e.symm w').functor.obj s)) =
    s.ι.app j ≫ 𝟙 s.pt
have dsimp : s.ι.app j ≫
    CategoryStruct.comp (Y := t.pt)
      (P.desc ((Cocone.precompose w.inv).obj (Cocone.whisker e.functor t)) :
        s.pt ⟶ ((Cocone.precompose w.inv).obj (Cocone.whisker e.functor t)).pt)
      (Q.desc
        ((Cocone.precompose ((e.invFunIdAssoc G).inv ≫ e.inverse.whiskerLeft w.hom)).obj
          (Cocone.whisker e.inverse s))) =
  s.ι.app j ≫ 𝟙 s.pt
Tactic: dsimp [w']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
t_1 : Cocone F_1
F : Functor.{v₁, v₃, u₁, u₃} J C
s : Cocone F
G : Functor.{v₂, v₃, u₂, u₃} K C
t : Cocone G
P : IsColimit s
Q : IsColimit t
e : Equivalence.{v₁, v₂, u₁, u₂} J K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
j : J
⊢ s.ι.app j ≫
      CategoryStruct.comp (Y := t.pt)
        (P.desc ((Cocone.precompose w.inv).obj (Cocone.whisker e.functor t)) :
          s.pt ⟶ ((Cocone.precompose w.inv).obj (Cocone.whisker e.functor t)).pt)
        (Q.desc
          ((Cocone.precompose ((e.invFunIdAssoc G).inv ≫ e.inverse.whiskerLeft w.hom)).obj
            (Cocone.whisker e.inverse s))) =
    s.ι.app j ≫ 𝟙 s.pt
have simp : w.inv.app j ≫
    G.map (e.counitInv.app (e.functor.obj j)) ≫
      w.hom.app (e.inverse.obj (e.functor.obj j)) ≫ s.ι.app (e.inverse.obj (e.functor.obj j)) =
  s.ι.app j
Tactic: simp only [Limits.Cocone.whisker_ι, fac, invFunIdAssoc_inv_app, whiskerLeft_app, assoc,
        comp_id, Limits.Cocone.precompose_obj_ι, fac_assoc, NatTrans.comp_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
t_1 : Cocone F_1
F : Functor.{v₁, v₃, u₁, u₃} J C
s : Cocone F
G : Functor.{v₂, v₃, u₂, u₃} K C
t : Cocone G
P : IsColimit s
Q : IsColimit t
e : Equivalence.{v₁, v₂, u₁, u₂} J K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
j : J
⊢ w.inv.app j ≫
      G.map (e.counitInv.app (e.functor.obj j)) ≫
        w.hom.app (e.inverse.obj (e.functor.obj j)) ≫ s.ι.app (e.inverse.obj (e.functor.obj j)) =
    s.ι.app j
have rw : F.map (e.unit.app j) ≫
    w.inv.app ((e.functor ⋙ e.inverse).obj j) ≫
      w.hom.app (e.inverse.obj (e.functor.obj j)) ≫ s.ι.app (e.inverse.obj (e.functor.obj j)) =
  s.ι.app j
Tactic: rw [counitInv_app_functor, ← Functor.comp_map, ← w.inv.naturality_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
t_1 : Cocone F_1
F : Functor.{v₁, v₃, u₁, u₃} J C
s : Cocone F
G : Functor.{v₂, v₃, u₂, u₃} K C
t : Cocone G
P : IsColimit s
Q : IsColimit t
e : Equivalence.{v₁, v₂, u₁, u₂} J K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
⊢ CategoryStruct.comp (Y := s.pt)
      (Q.desc ((Cocone.equivalenceOfReindexing e.symm w').functor.obj s) :
        t.pt ⟶ ((Cocone.equivalenceOfReindexing e.symm w').functor.obj s).pt)
      (P.desc ((Cocone.equivalenceOfReindexing e w).functor.obj t)) =
    𝟙 t.pt
have apply : ∀ (j : K),
  t.ι.app j ≫
      CategoryStruct.comp (Y := s.pt)
        (Q.desc ((Cocone.equivalenceOfReindexing e.symm w').functor.obj s) :
          t.pt ⟶ ((Cocone.equivalenceOfReindexing e.symm w').functor.obj s).pt)
        (P.desc ((Cocone.equivalenceOfReindexing e w).functor.obj t)) =
    t.ι.app j ≫ 𝟙 t.pt
Tactic: apply hom_ext Q
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
t : Cocone F
h : IsColimit t
W : C
ι : F ⟶ obj (const J) W
j j' : J
f : j ⟶ j'
⊢ Eq (α := F.obj j ⟶ W) (F.map f ≫ (fun (j : J) ↦ ι.app j) j') ((fun (j : J) ↦ ι.app j) j)
have h₁ : (F.obj j ⟶ obj.{v₁, v₃, u₁, u₃} (obj (const J) W) j') = (F.obj j ⟶ W) →
  ι.app j ≫ Functor.map (obj (const J) W) f = (fun (j : J) ↦ ι.app j) j
Tactic: convert! ← ι.naturality f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
t : Cocone F
h : IsColimit t
W : C
p : { p : (j : J) → F.obj j ⟶ W // ∀ {j j' : J} (f : j ⟶ j'), F.map f ≫ p j' = p j }
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ (↑p : (j : J) → F.obj j ⟶ W) j' = (↑p : (j : J) → F.obj j ⟶ W) j ≫ Functor.map (obj (const J) W) f
have dsimp : F.map f ≫ (↑p : (j : J) → F.obj j ⟶ W) j' = (↑p : (j : J) → F.obj j ⟶ W) j ≫ 𝟙 W
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
t : Cocone F
h : IsColimit t
W : C
p : { p : (j : J) → F.obj j ⟶ W // ∀ {j j' : J} (f : j ⟶ j'), F.map f ≫ p j' = p j }
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ (↑p : (j : J) → F.obj j ⟶ W) j' = (↑p : (j : J) → F.obj j ⟶ W) j ≫ 𝟙 W
have rw : F.map f ≫ (↑p : (j : J) → F.obj j ⟶ W) j' = (↑p : (j : J) → F.obj j ⟶ W) j
Tactic: rw [comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
t_1 t : Cocone F
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₃, v₄, u₃, u₄} C D
inst_4 : G.Faithful
ht : IsColimit (G.mapCocone t)
desc : (s : Cocone F) → t.pt ⟶ s.pt
h : ∀ (s : Cocone F), G.map (desc s) = ht.desc (G.mapCocone s)
s : Cocone F
j : J
⊢ t.ι.app j ≫ desc s = s.ι.app j
have a : G.map (t.ι.app j ≫ desc s) = G.map (s.ι.app j)
Tactic: apply G.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
t_1 t : Cocone F
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₃, v₄, u₃, u₄} C D
inst_4 : G.Faithful
ht : IsColimit (G.mapCocone t)
desc : (s : Cocone F) → t.pt ⟶ s.pt
h : ∀ (s : Cocone F), G.map (desc s) = ht.desc (G.mapCocone s)
s : Cocone F
j : J
⊢ G.map (t.ι.app j ≫ desc s) = G.map (s.ι.app j)
have a : G.map (t.ι.app j) ≫ ht.desc (G.mapCocone s) = G.map (s.ι.app j)
Tactic: rw [G.map_comp, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
t_1 t : Cocone F
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₃, v₄, u₃, u₄} C D
inst_4 : G.Faithful
ht : IsColimit (G.mapCocone t)
desc : (s : Cocone F) → t.pt ⟶ s.pt
h : ∀ (s : Cocone F), G.map (desc s) = ht.desc (G.mapCocone s)
s : Cocone F
m : t.pt ⟶ s.pt
w : ∀ (j : J), t.ι.app j ≫ m = s.ι.app j
⊢ m = desc s
have a : G.map m = G.map (desc s)
Tactic: apply G.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
t_1 t : Cocone F
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₃, v₄, u₃, u₄} C D
inst_4 : G.Faithful
ht : IsColimit (G.mapCocone t)
desc : (s : Cocone F) → t.pt ⟶ s.pt
h : ∀ (s : Cocone F), G.map (desc s) = ht.desc (G.mapCocone s)
s : Cocone F
m : t.pt ⟶ s.pt
w : ∀ (j : J), t.ι.app j ≫ m = s.ι.app j
⊢ G.map m = G.map (desc s)
have a : G.map m = ht.desc (G.mapCocone s)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
t_1 t : Cocone F
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₃, v₄, u₃, u₄} C D
inst_4 : G.Faithful
ht : IsColimit (G.mapCocone t)
desc : (s : Cocone F) → t.pt ⟶ s.pt
h : ∀ (s : Cocone F), G.map (desc s) = ht.desc (G.mapCocone s)
s : Cocone F
m : t.pt ⟶ s.pt
w : ∀ (j : J), t.ι.app j ≫ m = s.ι.app j
⊢ G.map m = ht.desc (G.mapCocone s)
have a : ∀ (j : J), (G.mapCocone t).ι.app j ≫ G.map m = (G.mapCocone s).ι.app j
Tactic: refine ht.uniq (mapCocone G s) _ fun j => ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
t_1 t : Cocone F
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₃, v₄, u₃, u₄} C D
inst_4 : G.Faithful
ht : IsColimit (G.mapCocone t)
desc : (s : Cocone F) → t.pt ⟶ s.pt
h : ∀ (s : Cocone F), G.map (desc s) = ht.desc (G.mapCocone s)
s : Cocone F
m : t.pt ⟶ s.pt
w : ∀ (j : J), t.ι.app j ≫ m = s.ι.app j
j : J
⊢ (G.mapCocone t).ι.app j ≫ G.map m = (G.mapCocone s).ι.app j
have h₁ : (G.obj (F.obj j) ⟶ G.obj s.pt) = ((F ⋙ G).obj j ⟶ (G.mapCocone s).pt) →
  G.map (t.ι.app j ≫ m) = (G.mapCocone t).ι.app j ≫ G.map m
Tactic: convert! ← congrArg (fun f => G.map f) (w j)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K_1 : Type u₂
inst_1 : Category.{v₂, u₂} K_1
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F_1 : Functor.{v₁, v₃, u₁, u₃} J C
t_1 : Cocone F_1
D : Type u₄
inst_3 : Category.{v₄, u₄} D
K : Functor.{v₁, v₃, u₁, u₃} J C
F G : Functor.{v₃, v₄, u₃, u₄} C D
h : F ≅ G
c : Cocone K
t : IsColimit (F.mapCocone c)
⊢ IsColimit (G.mapCocone c)
have apply : IsColimit ((Cocone.precompose (K.whiskerLeft h.inv)).obj (F.mapCocone c))
Tactic: apply IsColimit.ofIsoColimit _ (precomposeWhiskerLeftMapCocone h c)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
⊢ coconeOfHom h (homOfCocone h s) = s
have dsimp : { pt := s.pt,
    ι :=
      (h.homEquiv : (a : X ⟶ s.pt) → F ⟶ (const J).obj s.pt)
        ((Equiv.symm h.homEquiv : (a : F ⟶ (const J).obj s.pt) → X ⟶ s.pt) s.ι) } =
  s
Tactic: dsimp [coconeOfHom, homOfCocone]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
s_pt : C
s_ι : F ⟶ obj (const J) s_pt
⊢ { pt := { pt := s_pt, ι := s_ι : Cocone F }.pt,
      ι :=
        (h.homEquiv : (a : X ⟶ { pt := s_pt, ι := s_ι }.pt) → F ⟶ (const J).obj { pt := s_pt, ι := s_ι }.pt)
          ((Equiv.symm h.homEquiv :
              (a : F ⟶ (const J).obj { pt := s_pt, ι := s_ι }.pt) → X ⟶ { pt := s_pt, ι := s_ι }.pt)
            { pt := s_pt, ι := s_ι }.ι) } =
    { pt := s_pt, ι := s_ι : Cocone F }
have e_ι : (h.homEquiv : (a : X ⟶ { pt := s_pt, ι := s_ι }.pt) → F ⟶ (const J).obj { pt := s_pt, ι := s_ι }.pt)
    ((Equiv.symm h.homEquiv : (a : F ⟶ (const J).obj { pt := s_pt, ι := s_ι }.pt) → X ⟶ { pt := s_pt, ι := s_ι }.pt)
      { pt := s_pt, ι := s_ι }.ι) =
  s_ι
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
X : C
h : F.cocones.CorepresentableBy X
Y : C
f : X ⟶ Y
⊢ coconeOfHom h f = (colimitCocone h).extend (X := Y) f
have dsimp : Eq (α := Cocone F) { pt := Y, ι := (h.homEquiv : (a : X ⟶ Y) → F ⟶ (const J).obj Y) f }
  { pt := Y, ι := (h.homEquiv : (a : X ⟶ X) → F ⟶ (const J).obj X) (𝟙 X) ≫ Functor.map (const J) f }
Tactic: dsimp [coconeOfHom, colimitCocone, Cocone.extend]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
X : C
h : F.cocones.CorepresentableBy X
Y : C
f : X ⟶ Y
⊢ Eq (α := Cocone F) { pt := Y, ι := (h.homEquiv : (a : X ⟶ Y) → F ⟶ (const J).obj Y) f }
    { pt := Y, ι := (h.homEquiv : (a : X ⟶ X) → F ⟶ (const J).obj X) (𝟙 X) ≫ Functor.map (const J) f }
have e_ι : Eq (α := F ⟶ obj (const J) Y) ((h.homEquiv : (a : X ⟶ Y) → F ⟶ (const J).obj Y) f : F ⟶ obj (const J) Y)
  ((h.homEquiv : (a : X ⟶ X) → F ⟶ (const J).obj X) (𝟙 X) ≫ Functor.map (const J) f : F ⟶ obj (const J) Y)
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (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
X : C
h : F.cocones.CorepresentableBy X
Y : C
f : X ⟶ Y
| ((h.homEquiv : (a : X ⟶ Y) → F ⟶ (const J).obj Y) f : F ⟶ obj (const J) Y)
have rw : ((h.homEquiv : (a : X ⟶ Y) → F ⟶ (const J).obj Y) (𝟙 X ≫ f) : F ⟶ obj (const J) Y)
Tactic: rw [← Category.id_comp f]