awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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.cones.RepresentableBy X
Y : C
f : Y ⟶ X
⊢ Eq (α := obj (const J) Y ⟶ F) ((h.homEquiv : (a : Y ⟶ X) → (const J).obj Y ⟶ F) (f ≫ 𝟙 X) : obj (const J) Y ⟶ F)
    (Functor.map (const J) f ≫ (h.homEquiv : (a : X ⟶ X) → (const J).obj X ⟶ F) (𝟙 X) : obj (const J) Y ⟶ F)

Tactic:
exact h.homEquiv_comp f (𝟙 X)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.RepresentableBy.homEquiv_comp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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.cones.RepresentableBy X
s : Cone F
rw :
  (limitCone h).extend (X := (coneOfHom h (homOfCone h s)).pt) (homOfCone h (coneOfHom h (homOfCone h s))) =
    coneOfHom h (homOfCone h s)
⊢ (limitCone h).extend (X := s.pt) (homOfCone h s) = s

Tactic:
rw [← coneOfHom_homOfCone h s]

Premises used: CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom_homOfCone
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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.cones.RepresentableBy X
s : Cone F
simp : (limitCone h).extend (X := (coneOfHom h (homOfCone h s)).pt) (homOfCone h s)
| (limitCone h).extend (X := (coneOfHom h (homOfCone h s)).pt) (homOfCone h (coneOfHom h (homOfCone h s)))

Tactic:
simp only [homOfCone_coneOfHom]

Premises used: CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone_coneOfHom
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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.cones.RepresentableBy X
s : Cone F
conv_lhs : (limitCone h).extend (X := (coneOfHom h (homOfCone h s)).pt) (homOfCone h s) = coneOfHom h (homOfCone h s)
⊢ (limitCone h).extend (X := (coneOfHom h (homOfCone h s)).pt) (homOfCone h (coneOfHom h (homOfCone h s))) =
    coneOfHom h (homOfCone h s)

Tactic:
conv_lhs => simp only [homOfCone_coneOfHom]

Premises used: CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone_coneOfHom
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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.cones.RepresentableBy X
s : Cone F
⊢ (limitCone h).extend (X := (coneOfHom h (homOfCone h s)).pt) (homOfCone h s) = coneOfHom h (homOfCone h s)

Tactic:
apply (coneOfHom_fac _ _).symm

Premises used: CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom_fac, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
j : J
⊢ (limitCone h).extend (X := s.pt) (homOfCone h s) = s

Tactic:
have h := cone_fac h s
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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_1 : F.cones.RepresentableBy X
s : Cone F
j : J
h : (limitCone h_1).extend (X := s.pt) (homOfCone h_1 s) = s
mk :
  ∀ (pt : C) (π : obj (const J) pt ⟶ F)
    (h :
      (limitCone h_1).extend (X := { pt := pt, π := π : Cone F }.pt) (homOfCone h_1 { pt := pt, π := π : Cone F }) =
        { pt := pt, π := π }),
    homOfCone h_1 { pt := pt, π := π } ≫ (limitCone h_1).π.app j = { pt := pt, π := π : Cone F }.π.app j
⊢ homOfCone h_1 s ≫ (limitCone h_1).π.app j = s.π.app j

Tactic:
cases s
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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_1 : F.cones.RepresentableBy X
j : J
pt : C
π : obj (const J) pt ⟶ F
h :
  (limitCone h_1).extend (X := { pt := pt, π := π : Cone F }.pt) (homOfCone h_1 { pt := pt, π := π : Cone F }) =
    { pt := pt, π := π }
⊢ { pt := pt, π := π : Cone F }.pt = pt

Tactic:
injection h with h₁ h₂
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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_1 : F.cones.RepresentableBy X
j : J
pt : C
π : obj (const J) pt ⟶ F
h :
  (limitCone h_1).extend (X := { pt := pt, π := π : Cone F }.pt) (homOfCone h_1 { pt := pt, π := π : Cone F }) =
    { pt := pt, π := π }
h₁ : { pt := pt, π := π : Cone F }.pt = pt
⊢ Functor.map (const J) (homOfCone h_1 { pt := pt, π := π }) ≫ (limitCone h_1).π = π

Tactic:
injection h with h₁ h₂
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
j : J
pt : C
π : obj (const J) pt ⟶ F
h₁ : { pt := pt, π := π : Cone F }.pt = pt
h₂ : Functor.map (const J) (homOfCone h { pt := pt, π := π }) ≫ (limitCone h).π = π
rw :
  NatTrans.app
    (Cone.π
      { pt := pt,
        π := (Functor.map (const J) (homOfCone h { pt := pt, π := π }) ≫ (limitCone h).π : obj (const J) pt ⟶ F) })
    j
| { pt := pt, π := π : Cone F }.π.app j

Tactic:
rw [← h₂]
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
j : J
pt : C
π : obj (const J) pt ⟶ F
h₁ : { pt := pt, π := π : Cone F }.pt = pt
h₂ : Functor.map (const J) (homOfCone h { pt := pt, π := π }) ≫ (limitCone h).π = π
mk :
  Eq (α := { pt := pt, π := π : Cone F }.pt ⟶ F.obj j) (homOfCone h { pt := pt, π := π } ≫ (limitCone h).π.app j)
    (NatTrans.app
      (Cone.π
        { pt := pt,
          π := (Functor.map (const J) (homOfCone h { pt := pt, π := π }) ≫ (limitCone h).π : obj (const J) pt ⟶ F) })
      j)
⊢ homOfCone h { pt := pt, π := π } ≫ (limitCone h).π.app j = { pt := pt, π := π : Cone F }.π.app j

Tactic:
conv_rhs => rw [← h₂]
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
j : J
pt : C
π : obj (const J) pt ⟶ F
h₁ : { pt := pt, π := π : Cone F }.pt = pt
h₂ : Functor.map (const J) (homOfCone h { pt := pt, π := π }) ≫ (limitCone h).π = π
⊢ Eq (α := { pt := pt, π := π : Cone F }.pt ⟶ F.obj j) (homOfCone h { pt := pt, π := π } ≫ (limitCone h).π.app j)
    (NatTrans.app
      (Cone.π
        { pt := pt,
          π := (Functor.map (const J) (homOfCone h { pt := pt, π := π }) ≫ (limitCone h).π : obj (const J) pt ⟶ F) })
      j)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
rw : homOfCone h (coneOfHom h m) = homOfCone h s
⊢ m = homOfCone h s

Tactic:
rw [← homOfCone_coneOfHom h m]

Premises used: CategoryTheory.Limits.IsLimit.OfNatIso.homOfCone_coneOfHom
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
h₁ : coneOfHom h m = s
⊢ homOfCone h (coneOfHom h m) = homOfCone h s

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
h₁ : (limitCone h).extend m = s
⊢ coneOfHom h m = s

Tactic:
rw [coneOfHom_fac]

Premises used: CategoryTheory.Limits.IsLimit.OfNatIso.coneOfHom_fac
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
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, π := π }
⊢ { pt := s.pt, π := Functor.map (const J) m ≫ (limitCone h).π : Cone F } = s

Tactic:
cases s
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
h₁ : ∀ (j : J), (Functor.map (const J) m ≫ (limitCone h).π).app j = π.app j
⊢ { pt := { pt := pt, π := π : Cone F }.pt, π := Functor.map (const J) m ≫ (limitCone h).π : Cone F } =
    { pt := pt, π := π }

Tactic:
congr with j
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
j : J
⊢ (Functor.map (const J) m ≫ (limitCone h).π).app j = π.app j

Tactic:
w j
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
j : J
⊢ (Functor.map (const J) m ≫ (limitCone h).π).app j = π.app j

Tactic:
exact w j
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
hc : IsLimit t
X X' : C
f : X ⟶ X'
g : X' ⟶ t.pt
j : J
⊢ Eq.{v₃ + 1} (α := obj.{v₁, v₃, u₁, u₃} (unop (obj (Functor.op (const J)) (op X))) j ⟶ F.obj j)
    (NatTrans.app ((hc.homEquiv : (a : X ⟶ t.pt) → F.cones.obj (op X)) (f ≫ g)) j)
    (NatTrans.app
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.cones.map f.op) :
          (a : (fun (X : Type (max u₁ v₃)) ↦ X) (F.cones.obj (op X'))) →
            (fun (X : Type (max u₁ v₃)) ↦ X) (F.cones.obj (op X)))
        ((hc.homEquiv : (a : X' ⟶ t.pt) → F.cones.obj (op X')) g))
      j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
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
⊢ P = Q

Tactic:
cases P
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
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 }
⊢ { desc := desc, fac := fac, uniq := uniq : IsColimit t } = Q

Tactic:
cases Q
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
mk : desc = desc_1
⊢ { desc := desc, fac := fac, uniq := uniq : IsColimit t } = { desc := desc_1, fac := fac_1, uniq := uniq_1 }

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
c : Cocone F
hc : IsColimit c
d : Cocone G
α : F ⟶ G
j : J
⊢ c.ι.app j ≫ hc.map d α = α.app j ≫ d.ι.app j

Tactic:
fac _ _ _

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.IsColimit.map
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
⊢ h.desc t = 𝟙 t.pt

Tactic:
(h.uniq _ _ fun _ => comp_id _).symm

Premises used: CategoryTheory.Limits.IsColimit.uniq, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
w : g.hom = (h.descCoconeMorphism s).hom
⊢ g = h.descCoconeMorphism s

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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.hom = (h.descCoconeMorphism s).hom

Tactic:
h.uniq _ _ g.w

Premises used: CategoryTheory.Limits.CoconeMorphism.w, CategoryTheory.Limits.IsColimit.uniq
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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.hom = (h.descCoconeMorphism s).hom

Tactic:
exact h.uniq _ _ g.w

Premises used: CategoryTheory.Limits.CoconeMorphism.w, CategoryTheory.Limits.IsColimit.uniq
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
s : Cocone F
⊢ ∃! d : t.pt ⟶ s.pt, ∀ (j : J), t.ι.app j ≫ d = s.ι.app j

Tactic:
⟨h.desc s, h.fac s, h.uniq s⟩

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.IsColimit.uniq, CategoryTheory.Limits.IsColimit.desc, ExistsUnique, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
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
⊢ IsColimit t

Tactic:
choose s hs hs' using ht
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
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:
exact ⟨s, hs, hs'⟩
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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 ⟶ s
uniq' : ∀ (s : Cocone F) (m : t ⟶ s), m = desc s
s : Cocone F
m : t.pt ⟶ s.pt
w : ∀ (j : J), t.ι.app j ≫ m = s.ι.app j
⊢ { hom := m, w := w : CoconeMorphism t s } = desc s

Tactic:
apply uniq'
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
P : IsColimit s
Q : IsColimit t
f : s ⟶ t
⊢ IsIso f

Tactic:
⟨⟨Q.descCoconeMorphism s, ⟨P.uniq_cocone_morphism, Q.uniq_cocone_morphism⟩⟩⟩

Premises used: CategoryTheory.Limits.IsColimit.uniq_cocone_morphism, And.intro, Exists.intro, CategoryTheory.IsIso.mk, CategoryTheory.Limits.IsColimit.descCoconeMorphism
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
P : IsColimit s
Q : IsColimit t
j : J
⊢ s.ι.app j ≫ (P.coconePointUniqueUpToIso Q).hom = t.ι.app j

Tactic:
(uniqueUpToIso P Q).hom.w _

Premises used: CategoryTheory.Limits.CoconeMorphism.w, CategoryTheory.Limits.IsColimit.uniqueUpToIso, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
P : IsColimit s
Q : IsColimit t
j : J
⊢ t.ι.app j ≫ (P.coconePointUniqueUpToIso Q).inv = s.ι.app j

Tactic:
(uniqueUpToIso P Q).inv.w _

Premises used: CategoryTheory.Limits.CoconeMorphism.w, CategoryTheory.Limits.IsColimit.uniqueUpToIso, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
r s t : Cocone F
P : IsColimit s
Q : IsColimit t
⊢ ∀ (j : J), s.ι.app j ≫ (P.coconePointUniqueUpToIso Q).hom ≫ Q.desc r = r.ι.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
r s t : Cocone F
P : IsColimit s
Q : IsColimit t
⊢ ∀ (j : J), t.ι.app j ≫ (P.coconePointUniqueUpToIso Q).inv ≫ P.desc r = r.ι.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
rw : i.hom ≫ m = P.descCoconeMorphism s
⊢ m = (fun (s : Cocone F) ↦ i.inv ≫ P.descCoconeMorphism s) s

Tactic:
rw [i.eq_inv_comp]

Premises used: CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
⊢ i.hom ≫ m = P.descCoconeMorphism s

Tactic:
apply P.uniq_cocone_morphism

Premises used: CategoryTheory.Limits.IsColimit.uniq_cocone_morphism
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
r t : Cocone F
P : IsColimit r
i : r ≅ t
s : Cocone F
⊢ (P.ofIsoColimit i).desc s = i.inv.hom ≫ P.desc s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
r t : Cocone F
i : r ≅ t
P : IsColimit r
⊢ (equivIsoColimit i : (a : IsColimit r) → IsColimit t) P = P.ofIsoColimit i

Tactic:
rfl

Premises used: CategoryTheory.Limits.IsColimit.mkCoconeMorphism, CategoryTheory.Limits.IsColimit.ofIsoColimit, rfl
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
r t : Cocone F
i : r ≅ t
P : IsColimit t
⊢ ((equivIsoColimit i).symm : (a : IsColimit t) → IsColimit r) P = P.ofIsoColimit i.symm

Tactic:
rfl

Premises used: CategoryTheory.Limits.IsColimit.mkCoconeMorphism, CategoryTheory.Limits.IsColimit.ofIsoColimit, rfl
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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)
⊢ IsIso (P.descCoconeMorphism t).hom

Tactic:
haveI : IsIso (P.descCoconeMorphism t).hom := i
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
⊢ IsIso (P.descCoconeMorphism t)

Tactic:
haveI : IsIso (P.descCoconeMorphism t) := Cocone.cocone_iso_of_hom_iso _
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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_1 : IsIso (P.descCoconeMorphism t).hom
this : IsIso (P.descCoconeMorphism t)
⊢ r ≅ t

Tactic:
apply asIso (P.descCoconeMorphism t)

Premises used: CategoryTheory.asIso, CategoryTheory.Limits.IsColimit.descCoconeMorphism
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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
m : t.pt ⟶ W
⊢ m = h.desc { pt := W, ι := { app := fun (b : J) ↦ t.ι.app b ≫ m, naturality := ⋯ : NatTrans F (obj (const J) W) } }

Tactic:
h.uniq
    { pt := W
      ι := { app := fun b => t.ι.app b ≫ m } }
    m fun _ => rfl

Premises used: CategoryTheory.Limits.Cocone.mk, CategoryTheory.NatTrans.mk, CategoryTheory.Limits.IsColimit.uniq, CategoryTheory.Limits.Cocone.ι, CategoryTheory.CategoryStruct.comp, CategoryTheory.NatTrans.app, rfl