awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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
⊢ Eq.{v₄ + 1} (α := G.obj (F.obj j) ⟶ G.obj s.pt) ((fun (f : F.obj j ⟶ s.pt) ↦ G.map f) (t.ι.app j ≫ m))
    ((fun (f : F.obj j ⟶ s.pt) ↦ G.map f) (s.ι.app j))

Tactic:
congrArg (fun f => G.map f) (w j)

Premises used: congrArg, CategoryTheory.Functor.map
-- 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_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
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
⊢ (G.mapCocone t).ι.app j ≫ G.map m = (G.mapCocone s).ι.app j

Tactic:
convert! ← congrArg (fun f => G.map f) (w j)

Premises used: congrArg, CategoryTheory.Functor.map
-- 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_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
e_1 : (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:
apply G.map_comp

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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)
apply : IsColimit ((Cocone.precompose (K.whiskerLeft h.inv)).obj (F.mapCocone c))
⊢ IsColimit (G.mapCocone c)

Tactic:
apply IsColimit.ofIsoColimit _ (precomposeWhiskerLeftMapCocone h c)

Premises used: CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.Functor.precomposeWhiskerLeftMapCocone
-- Module: Mathlib.CategoryTheory.Limits.IsLimit
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 ((Cocone.precompose (K.whiskerLeft h.inv)).obj (F.mapCocone c))

Tactic:
apply (precomposeInvEquiv (isoWhiskerLeft K h :) _).symm t

Premises used: CategoryTheory.Functor.isoWhiskerLeft, Equiv.symm, DFunLike.coe, CategoryTheory.Limits.IsColimit.precomposeInvEquiv
-- 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.cocones.CorepresentableBy X
s : Cocone F
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
⊢ coconeOfHom h (homOfCocone h s) = s

Tactic:
dsimp [coconeOfHom, homOfCocone]

Premises used: CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom, CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone
-- 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.cocones.CorepresentableBy X
s : Cocone F
s_pt : C
s_ι : F ⟶ obj (const J) s_pt
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_ι
⊢ { 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 }

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 : 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
⊢ (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:
h.homEquiv.apply_symm_apply s_ι

Premises used: Equiv.apply_symm_apply, CategoryTheory.Functor.CorepresentableBy.homEquiv
-- 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.cocones.CorepresentableBy X
s : Cocone F
s_pt : C
s_ι : F ⟶ obj (const J) s_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_ι }.ι) =
    s_ι

Tactic:
exact h.homEquiv.apply_symm_apply s_ι

Premises used: Equiv.apply_symm_apply, CategoryTheory.Functor.CorepresentableBy.homEquiv
-- 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.cocones.CorepresentableBy X
s : Cocone F
⊢ { 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:
match s with
  | .mk s_pt s_ι =>
    congr
    exact h.homEquiv.apply_symm_apply s_ι
-- 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.cocones.CorepresentableBy X
Y : C
f : X ⟶ Y
⊢ homOfCocone h (coconeOfHom h f) = f

Tactic:
simp [homOfCocone, coconeOfHom]

Premises used: CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom, CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone
-- 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.cocones.CorepresentableBy X
Y : C
f : X ⟶ Y
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 }
⊢ coconeOfHom h f = (colimitCocone h).extend (X := Y) f

Tactic:
dsimp [coconeOfHom, colimitCocone, Cocone.extend]

Premises used: CategoryTheory.Limits.Cocone.extend, CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom, CategoryTheory.Limits.IsColimit.OfNatIso.colimitCocone
-- 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.cocones.CorepresentableBy X
Y : C
f : X ⟶ Y
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)
⊢ 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:
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 : Functor.{v₁, v₃, u₁, u₃} J C
X : C
h : F.cocones.CorepresentableBy X
Y : C
f : X ⟶ Y
rw : ((h.homEquiv : (a : X ⟶ Y) → F ⟶ (const J).obj Y) (𝟙 X ≫ f) : F ⟶ obj (const J) Y)
| ((h.homEquiv : (a : X ⟶ Y) → F ⟶ (const J).obj Y) f : F ⟶ obj (const J) Y)

Tactic:
rw [← Category.id_comp f]

Premises used: CategoryTheory.Category.id_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.cocones.CorepresentableBy X
Y : C
f : X ⟶ Y
e_ι :
  Eq (α := F ⟶ obj (const J) Y) ((h.homEquiv : (a : X ⟶ Y) → F ⟶ (const J).obj Y) (𝟙 X ≫ 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)
⊢ 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:
conv_lhs => rw [← Category.id_comp f]

Premises used: CategoryTheory.Category.id_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.cocones.CorepresentableBy X
Y : C
f : X ⟶ Y
⊢ Eq (α := F ⟶ obj (const J) Y) ((h.homEquiv : (a : X ⟶ Y) → F ⟶ (const J).obj Y) (𝟙 X ≫ 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:
h.homEquiv_comp f (𝟙 X)

Premises used: CategoryTheory.NatTrans.vcomp, CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.CorepresentableBy.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.cocones.CorepresentableBy X
Y : C
f : X ⟶ Y
⊢ Eq (α := F ⟶ obj (const J) Y) ((h.homEquiv : (a : X ⟶ Y) → F ⟶ (const J).obj Y) (𝟙 X ≫ 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:
exact h.homEquiv_comp f (𝟙 X)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.CorepresentableBy.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.cocones.CorepresentableBy X
s : Cocone F
rw :
  (colimitCocone h).extend (X := (coconeOfHom h (homOfCocone h s)).pt)
      (homOfCocone h (coconeOfHom h (homOfCocone h s))) =
    coconeOfHom h (homOfCocone h s)
⊢ (colimitCocone h).extend (X := s.pt) (homOfCocone h s) = s

Tactic:
rw [← coconeOfHom_homOfCocone h s]

Premises used: CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom_homOfCocone
-- 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.cocones.CorepresentableBy X
s : Cocone F
simp : (colimitCocone h).extend (X := (coconeOfHom h (homOfCocone h s)).pt) (homOfCocone h s)
| (colimitCocone h).extend (X := (coconeOfHom h (homOfCocone h s)).pt) (homOfCocone h (coconeOfHom h (homOfCocone h s)))

Tactic:
simp only [homOfCocone_coconeOfHom]

Premises used: CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone_coconeOfHom
-- 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.cocones.CorepresentableBy X
s : Cocone F
conv_lhs :
  (colimitCocone h).extend (X := (coconeOfHom h (homOfCocone h s)).pt) (homOfCocone h s) =
    coconeOfHom h (homOfCocone h s)
⊢ (colimitCocone h).extend (X := (coconeOfHom h (homOfCocone h s)).pt)
      (homOfCocone h (coconeOfHom h (homOfCocone h s))) =
    coconeOfHom h (homOfCocone h s)

Tactic:
conv_lhs => simp only [homOfCocone_coconeOfHom]

Premises used: CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone_coconeOfHom
-- 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.cocones.CorepresentableBy X
s : Cocone F
⊢ (colimitCocone h).extend (X := (coconeOfHom h (homOfCocone h s)).pt) (homOfCocone h s) =
    coconeOfHom h (homOfCocone h s)

Tactic:
apply (coconeOfHom_fac _ _).symm

Premises used: CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom_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 : Cocone F
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
j : J
⊢ (colimitCocone h).extend (X := s.pt) (homOfCocone h s) = s

Tactic:
have h := cocone_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 : Cocone F
X : C
h_1 : F.cocones.CorepresentableBy X
s : Cocone F
j : J
h : (colimitCocone h_1).extend (X := s.pt) (homOfCocone h_1 s) = s
mk :
  ∀ (pt : C) (ι : F ⟶ obj (const J) pt)
    (h :
      (colimitCocone h_1).extend (X := { pt := pt, ι := ι : Cocone F }.pt)
          (homOfCocone h_1 { pt := pt, ι := ι : Cocone F }) =
        { pt := pt, ι := ι }),
    (colimitCocone h_1).ι.app j ≫ homOfCocone h_1 { pt := pt, ι := ι } = { pt := pt, ι := ι : Cocone F }.ι.app j
⊢ (colimitCocone h_1).ι.app j ≫ homOfCocone h_1 s = 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 : Cocone F
X : C
h_1 : F.cocones.CorepresentableBy X
j : J
pt : C
ι : F ⟶ obj (const J) pt
h :
  (colimitCocone h_1).extend (X := { pt := pt, ι := ι : Cocone F }.pt)
      (homOfCocone h_1 { pt := pt, ι := ι : Cocone F }) =
    { pt := pt, ι := ι }
⊢ { pt := pt, ι := ι : Cocone 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 : Cocone F
X : C
h_1 : F.cocones.CorepresentableBy X
j : J
pt : C
ι : F ⟶ obj (const J) pt
h :
  (colimitCocone h_1).extend (X := { pt := pt, ι := ι : Cocone F }.pt)
      (homOfCocone h_1 { pt := pt, ι := ι : Cocone F }) =
    { pt := pt, ι := ι }
h₁ : { pt := pt, ι := ι : Cocone F }.pt = pt
⊢ (colimitCocone h_1).ι ≫ Functor.map (const J) (homOfCocone h_1 { 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 : Cocone F
X : C
h : F.cocones.CorepresentableBy X
j : J
pt : C
ι : F ⟶ obj (const J) pt
h₁ : { pt := pt, ι := ι : Cocone F }.pt = pt
h₂ : (colimitCocone h).ι ≫ Functor.map (const J) (homOfCocone h { pt := pt, ι := ι }) = ι
rw :
  NatTrans.app
    (Cocone.ι
      { pt := pt,
        ι :=
          ((colimitCocone h).ι ≫ Functor.map (const J) (homOfCocone h { pt := pt, ι := ι }) : F ⟶ obj (const J) pt) })
    j
| { pt := pt, ι := ι : Cocone 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 : Cocone F
X : C
h : F.cocones.CorepresentableBy X
j : J
pt : C
ι : F ⟶ obj (const J) pt
h₁ : { pt := pt, ι := ι : Cocone F }.pt = pt
h₂ : (colimitCocone h).ι ≫ Functor.map (const J) (homOfCocone h { pt := pt, ι := ι }) = ι
mk :
  Eq (α := F.obj j ⟶ { pt := pt, ι := ι : Cocone F }.pt)
    ((colimitCocone h).ι.app j ≫ homOfCocone h { pt := pt, ι := ι })
    (NatTrans.app
      (Cocone.ι
        { pt := pt,
          ι :=
            ((colimitCocone h).ι ≫ Functor.map (const J) (homOfCocone h { pt := pt, ι := ι }) : F ⟶ obj (const J) pt) })
      j)
⊢ (colimitCocone h).ι.app j ≫ homOfCocone h { pt := pt, ι := ι } = { pt := pt, ι := ι : Cocone 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 : Cocone F
X : C
h : F.cocones.CorepresentableBy X
j : J
pt : C
ι : F ⟶ obj (const J) pt
h₁ : { pt := pt, ι := ι : Cocone F }.pt = pt
h₂ : (colimitCocone h).ι ≫ Functor.map (const J) (homOfCocone h { pt := pt, ι := ι }) = ι
⊢ Eq (α := F.obj j ⟶ { pt := pt, ι := ι : Cocone F }.pt)
    ((colimitCocone h).ι.app j ≫ homOfCocone h { pt := pt, ι := ι })
    (NatTrans.app
      (Cocone.ι
        { pt := pt,
          ι :=
            ((colimitCocone h).ι ≫ Functor.map (const J) (homOfCocone h { pt := pt, ι := ι }) : F ⟶ obj (const J) pt) })
      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 : Cocone F
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
m : (colimitCocone h).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = s.ι.app j
rw : homOfCocone h (coconeOfHom h m) = homOfCocone h s
⊢ m = homOfCocone h s

Tactic:
rw [← homOfCocone_coconeOfHom h m]

Premises used: CategoryTheory.Limits.IsColimit.OfNatIso.homOfCocone_coconeOfHom
-- 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
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
m : (colimitCocone h).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = s.ι.app j
h₁ : coconeOfHom h m = s
⊢ homOfCocone h (coconeOfHom h m) = homOfCocone 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 : Cocone F
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
m : (colimitCocone h).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = s.ι.app j
h₁ : (colimitCocone h).extend m = s
⊢ coconeOfHom h m = s

Tactic:
rw [coconeOfHom_fac]

Premises used: CategoryTheory.Limits.IsColimit.OfNatIso.coconeOfHom_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 : Cocone F
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
m : (colimitCocone h).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = s.ι.app j
h₁ :
  ∀ (pt : C) (ι : F ⟶ obj (const J) pt) (m : (colimitCocone h).pt ⟶ { pt := pt, ι := ι : Cocone F }.pt)
    (w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = { pt := pt, ι := ι }.ι.app j),
    { pt := { pt := pt, ι := ι : Cocone F }.pt, ι := (colimitCocone h).ι ≫ Functor.map (const J) m : Cocone F } =
      { pt := pt, ι := ι }
⊢ { pt := s.pt, ι := (colimitCocone h).ι ≫ Functor.map (const J) m : Cocone 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 : Cocone F
X : C
h : F.cocones.CorepresentableBy X
pt : C
ι : F ⟶ obj (const J) pt
m : (colimitCocone h).pt ⟶ { pt := pt, ι := ι : Cocone F }.pt
w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = { pt := pt, ι := ι }.ι.app j
h₁ : ∀ (j : J), ((colimitCocone h).ι ≫ Functor.map (const J) m).app j = ι.app j
⊢ { pt := { pt := pt, ι := ι : Cocone F }.pt, ι := (colimitCocone h).ι ≫ Functor.map (const J) m : Cocone 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 : Cocone F
X : C
h : F.cocones.CorepresentableBy X
pt : C
ι : F ⟶ obj (const J) pt
m : (colimitCocone h).pt ⟶ { pt := pt, ι := ι : Cocone F }.pt
w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = { pt := pt, ι := ι }.ι.app j
j : J
⊢ ((colimitCocone h).ι ≫ Functor.map (const J) m).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 : Cocone F
X : C
h : F.cocones.CorepresentableBy X
pt : C
ι : F ⟶ obj (const J) pt
m : (colimitCocone h).pt ⟶ { pt := pt, ι := ι : Cocone F }.pt
w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = { pt := pt, ι := ι }.ι.app j
j : J
⊢ ((colimitCocone h).ι ≫ Functor.map (const J) m).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 : Cocone F
hc : IsColimit t
X X' : C
f : X ⟶ X'
g : t.pt ⟶ X
j : J
⊢ Eq.{v₃ + 1} (α := (unop (op F)).obj j ⟶ obj.{v₁, v₃, u₁, u₃} (obj (const J) X') j)
    (NatTrans.app ((hc.homEquiv : (a : t.pt ⟶ X') → F.cocones.obj X') (g ≫ f)) j)
    (NatTrans.app
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.cocones.map f) :
          (a : (fun (X : Type (max u₁ v₃)) ↦ X) (F.cocones.obj X)) →
            (fun (X : Type (max u₁ v₃)) ↦ X) (F.cocones.obj X'))
        ((hc.homEquiv : (a : t.pt ⟶ X) → F.cocones.obj X) g))
      j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
J_1 : Type w
inst : SmallCategory J_1
inst_1 : FinCategory J_1
inst_2 : SemilatticeInf α
inst_3 : OrderTop α
J : Type
𝒥₁ : SmallCategory J
𝒥₂ : FinCategory J
⊢ HasLimitsOfShape J α

Tactic:
{ has_limit := fun F => HasLimit.mk (finiteLimitCone F) }

Premises used: CategoryTheory.Limits.HasLimitsOfShape.mk, CategoryTheory.Limits.CompleteLattice.finiteLimitCone, CategoryTheory.Limits.HasLimit.mk
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
J_1 : Type w
inst : SmallCategory J_1
inst_1 : FinCategory J_1
inst_2 : SemilatticeInf α
inst_3 : OrderTop α
J : Type
𝒥₁ : SmallCategory J
𝒥₂ : FinCategory J
⊢ HasLimitsOfShape J α

Tactic:
exact { has_limit := fun F => HasLimit.mk (finiteLimitCone F) }
-- Module: Mathlib.CategoryTheory.Limits.Lattice
Goal:
α : Type u
J_1 : Type w
inst : SmallCategory J_1
inst_1 : FinCategory J_1
inst_2 : SemilatticeSup α
inst_3 : OrderBot α
J : Type
𝒥₁ : SmallCategory J
𝒥₂ : FinCategory J
⊢ HasColimitsOfShape J α

Tactic:
{ has_colimit := fun F => HasColimit.mk (finiteColimitCocone F) }

Premises used: CategoryTheory.Limits.HasColimitsOfShape.mk, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.CompleteLattice.finiteColimitCocone