awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : F.CoconeTypes
hc :
  Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
    ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)
x y : F.ColimitType
h : F.descColimitType c x = F.descColimitType c y
f : (z : F.ColimitType) → ULift.{u, 0} Bool := fun (z : F.ColimitType) ↦ { down := decide (x = z) }
z : F.ColimitType
mpr :
  ∀ (j : J) (z : F.obj j),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            (hc.desc
              ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F)
                (F.coconeTypes.postcomp (T := ULift.{u, 0} Bool) f))) :
          (a : (fun (X : Type u) ↦ X) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c).pt) →
            (fun (X : Type u) ↦ X)
              ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) (F.coconeTypes.postcomp f)).pt)
        (F.descColimitType c (F.ιColimitType j z)) =
      f (F.ιColimitType j z)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (hc.desc
            ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F)
              (F.coconeTypes.postcomp (T := ULift.{u, 0} Bool) f))) :
        (a : (fun (X : Type u) ↦ X) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c).pt) →
          (fun (X : Type u) ↦ X) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) (F.coconeTypes.postcomp f)).pt)
      (F.descColimitType c z) =
    f z

Tactic:
obtain ⟨j, z, rfl⟩ := F.ιColimitType_jointly_surjective z

Premises used: CategoryTheory.Functor.ιColimitType_jointly_surjective, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : F.CoconeTypes
hc :
  Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
    ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)
x y : F.ColimitType
h : F.descColimitType c x = F.descColimitType c y
f : (z : F.ColimitType) → ULift.{u, 0} Bool := fun (z : F.ColimitType) ↦ { down := decide (x = z) }
j : J
z : F.obj j
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (hc.desc
            ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F)
              (F.coconeTypes.postcomp (T := ULift.{u, 0} Bool) f))) :
        (a : (fun (X : Type u) ↦ X) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c).pt) →
          (fun (X : Type u) ↦ X) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) (F.coconeTypes.postcomp f)).pt)
      (F.descColimitType c (F.ιColimitType j z)) =
    f (F.ιColimitType j z)

Tactic:
ConcreteCategory.congr_hom (hc.fac _ j) z

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Functor.descColimitType, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Functor.ιColimitType
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : F.CoconeTypes
hc :
  Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
    ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)
x y : F.ColimitType
h : F.descColimitType c x = F.descColimitType c y
f : (z : F.ColimitType) → ULift.{u, 0} Bool := fun (z : F.ColimitType) ↦ { down := decide (x = z) }
j : J
z : F.obj j
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (hc.desc
            ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F)
              (F.coconeTypes.postcomp (T := ULift.{u, 0} Bool) f))) :
        (a : (fun (X : Type u) ↦ X) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c).pt) →
          (fun (X : Type u) ↦ X) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) (F.coconeTypes.postcomp f)).pt)
      (F.descColimitType c (F.ιColimitType j z)) =
    f (F.ιColimitType j z)

Tactic:
exact ConcreteCategory.congr_hom (hc.fac _ j) z

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : F.CoconeTypes
hc :
  Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
    ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)
x : c.pt
f₁ : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c) ⟶
  ULift.{u, 0} Bool :=
  ↾fun (x : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) ↦
    { down := true }
f₂ : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c) ⟶
  ULift.{u, 0} Bool :=
  ↾fun (x : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) ↦
    { down := decide (∃ (a : F.ColimitType), F.descColimitType c a = x) }
this : f₁ = f₂
⊢ Eq (α := ULift.{u, 0} Bool)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f₁ :
          (a : ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c).pt) → ULift.{u, 0} Bool)
        x :
      ULift.{u, 0} Bool)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f₂ :
          (a : ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c).pt) → ULift.{u, 0} Bool)
        x :
      ULift.{u, 0} Bool)

Tactic:
have := ConcreteCategory.congr_hom this x
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : F.CoconeTypes
hc :
  Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
    ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)
x : c.pt
f₁ : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c) ⟶
  ULift.{u, 0} Bool :=
  ↾fun (x : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) ↦
    { down := true }
f₂ : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c) ⟶
  ULift.{u, 0} Bool :=
  ↾fun (x : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) ↦
    { down := decide (∃ (a : F.ColimitType), F.descColimitType c a = x) }
this_1 : f₁ = f₂
this :
  Eq (α := ULift.{u, 0} Bool)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f₁ :
          (a : ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c).pt) → ULift.{u, 0} Bool)
        x :
      ULift.{u, 0} Bool)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f₂ :
          (a : ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c).pt) → ULift.{u, 0} Bool)
        x :
      ULift.{u, 0} Bool)
⊢ ∃ (a : F.ColimitType), F.descColimitType c a = x

Tactic:
simpa [f₁, f₂] using this
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : F.CoconeTypes
hc :
  Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
    ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)
x : c.pt
f₁ : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c) ⟶
  ULift.{u, 0} Bool :=
  ↾fun (x : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) ↦
    { down := true }
f₂ : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c) ⟶
  ULift.{u, 0} Bool :=
  ↾fun (x : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) ↦
    { down := decide (∃ (a : F.ColimitType), F.descColimitType c a = x) }
mpr : f₁ = f₂
⊢ ∃ (a : F.ColimitType), F.descColimitType c a = x

Tactic:
suffices f₁ = f₂ by
        have := ConcreteCategory.congr_hom this x
        simpa [f₁, f₂] using this
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : F.CoconeTypes
hc :
  Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
    ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)
x : c.pt
f₁ : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c) ⟶
  ULift.{u, 0} Bool :=
  ↾fun (x : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) ↦
    { down := true }
f₂ : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c) ⟶
  ULift.{u, 0} Bool :=
  ↾fun (x : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) ↦
    { down := decide (∃ (a : F.ColimitType), F.descColimitType c a = x) }
⊢ f₁ = f₂

Tactic:
hc.hom_ext fun j => ?_

Premises used: CategoryTheory.Limits.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : F.CoconeTypes
hc :
  Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
    ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)
x : c.pt
f₁ : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c) ⟶
  ULift.{u, 0} Bool :=
  ↾fun (x : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) ↦
    { down := true }
f₂ : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c) ⟶
  ULift.{u, 0} Bool :=
  ↾fun (x : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) ↦
    { down := decide (∃ (a : F.ColimitType), F.descColimitType c a = x) }
mpr :
  ∀ (j : J),
    Eq.{u + 1} (α := F.obj j ⟶ ULift.{u, 0} Bool)
      (NatTrans.app (Cocone.ι ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) j ≫ f₁)
      (NatTrans.app (Cocone.ι ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) j ≫ f₂)
⊢ f₁ = f₂

Tactic:
refine hc.hom_ext fun j => ?_

Premises used: CategoryTheory.Limits.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : F.CoconeTypes
hc :
  Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
    ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)
x : c.pt
f₁ : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c) ⟶
  ULift.{u, 0} Bool :=
  ↾fun (x : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) ↦
    { down := true }
f₂ : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c) ⟶
  ULift.{u, 0} Bool :=
  ↾fun (x : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) ↦
    { down := decide (∃ (a : F.ColimitType), F.descColimitType c a = x) }
j : J
mpr :
  ∀ (x : F.obj j),
    Eq (α := Bool)
      (ULift.down.{u, 0}
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) j ≫ f₁))
          x))
      (ULift.down.{u, 0}
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app (Cocone.ι ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) j ≫ f₂))
          x))
⊢ Eq.{u + 1} (α := F.obj j ⟶ ULift.{u, 0} Bool)
    (NatTrans.app (Cocone.ι ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) j ≫ f₁)
    (NatTrans.app (Cocone.ι ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) j ≫ f₂)

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : F.CoconeTypes
hc :
  Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
    ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)
x_1 : c.pt
f₁ : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c) ⟶
  ULift.{u, 0} Bool :=
  ↾fun (x : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) ↦
    { down := true }
f₂ : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c) ⟶
  ULift.{u, 0} Bool :=
  ↾fun (x : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) ↦
    { down := decide (∃ (a : F.ColimitType), F.descColimitType c a = x) }
j : J
x : F.obj j
⊢ F.descColimitType c (F.ιColimitType j x) = c.ι j x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : F.CoconeTypes
hc :
  Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
    ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)
x_1 : c.pt
f₁ : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c) ⟶
  ULift.{u, 0} Bool :=
  ↾fun (x : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) ↦
    { down := true }
f₂ : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c) ⟶
  ULift.{u, 0} Bool :=
  ↾fun (x : Cocone.pt.{w, u, v, u + 1} (J := J) (F := F) ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) ↦
    { down := decide (∃ (a : F.ColimitType), F.descColimitType c a = x) }
j : J
x : F.obj j
⊢ Eq (α := Bool)
    (ULift.down.{u, 0}
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app (Cocone.ι ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) j ≫ f₁))
        x))
    (ULift.down.{u, 0}
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app (Cocone.ι ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)) j ≫ f₂))
        x))

Tactic:
simpa [f₁, f₂] using ⟨F.ιColimitType j x, by simp⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : F.CoconeTypes
hc :
  Limits.IsColimit.{w, u, v, u + 1} (J := J) (C := Type u) (F := F)
    ((F.coconeTypesEquiv : (a : F.CoconeTypes) → Cocone F) c)
mpr : ∀ (x y : F.ColimitType) (h : F.descColimitType c x = F.descColimitType c y), x = y
mpr₁ mpr₂ : ∀ (x : c.pt), ∃ (a : F.ColimitType), F.descColimitType c a = x
⊢ c.IsColimit

Tactic:
classical
    refine ⟨⟨fun x y h ↦ ?_, fun x ↦ ?_⟩⟩
    · let f (z : F.ColimitType) : ULift.{u} Bool := ULift.up (x = z)
      suffices f x = f y by simpa [f] using this
      suffices ∀ z, hc.desc (F.coconeTypesEquiv (F.coconeTypes.postcomp f))
          (F.descColimitType c z) = f z by rw [← this x, h, ← this y]
      intro z
      obtain ⟨j, z, rfl⟩ := F.ιColimitType_jointly_surjective z
      exact ConcreteCategory.congr_hom (hc.fac _ j) z
    · let f₁ : (F.coconeTypesEquiv c).pt ⟶ (ULift.{u} Bool) :=
        ↾fun _ => ULift.up true
      let f₂ : (F.coconeTypesEquiv c).pt ⟶ (ULift.{u} Bool) :=
        ↾fun x => ULift.up (∃ a, F.descColimitType c a = x)
      suffices f₁ = f₂ by
        have := ConcreteCategory.congr_hom this x
        simpa [f₁, f₂] using this
      refine hc.hom_ext fun j => ?_
      ext x
      simpa [f₁, f₂] using ⟨F.ιColimitType j x, by simp⟩

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
c : Cocone F
⊢ Nonempty (IsColimit c) ↔
    Functor.CoconeTypes.IsColimit.{u, u, w, v} (J := J) (F := F)
      ((F.coconeTypesEquiv.symm : (a : Cocone F) → F.CoconeTypes) c)

Tactic:
simp only [Functor.CoconeTypes.isColimit_iff, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, CategoryTheory.Functor.CoconeTypes.isColimit_iff
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : Small.{u, max u v} F.ColimitType
⊢ ∀ (j : J) (x : F.obj j),
    Eq (α :=
      Functor.CoconeTypes.pt.{u, u, w, v} (J := J) (F := F)
        ((F.coconeTypesEquiv.symm : (a : Cocone F) → F.CoconeTypes) (colimitCocone F)))
      (Functor.CoconeTypes.ι ((F.coconeTypesEquiv.symm : (a : Cocone F) → F.CoconeTypes) (colimitCocone F)) j x)
      ((equivShrink F.ColimitType :
          (a : F.coconeTypes.pt) → ((F.coconeTypesEquiv.symm : (a : Cocone F) → F.CoconeTypes) (colimitCocone F)).pt)
        (F.coconeTypes.ι j x))

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
⊢ HasColimit F ↔ Small.{u, max u v} F.ColimitType

Tactic:
⟨fun _ ↦ small_of_injective
      ((isColimit_iff_coconeTypesIsColimit _).1 ⟨colimit.isColimit F⟩).bijective.1,
    fun _ ↦ ⟨_, colimitCoconeIsColimit F⟩⟩

Premises used: CategoryTheory.Limits.Types.isColimit_iff_coconeTypesIsColimit, CategoryTheory.Functor.CoconeTypes.IsColimit.bijective, CategoryTheory.Limits.colimit.isColimit, small_of_injective, Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk, And.left, CategoryTheory.Limits.Types.colimitCoconeIsColimit, Iff.intro, Iff.mp, CategoryTheory.Limits.colimit.cocone, CategoryTheory.Limits.Types.colimitCocone
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasColimit F
⊢ Small.{u, max u v} F.ColimitType

Tactic:
(hasColimit_iff_small_colimitType F).mp inferInstance

Premises used: inferInstance, CategoryTheory.Limits.Types.hasColimit_iff_small_colimitType, Iff.mp
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
inst_1 : Small.{u, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
⊢ HasColimit F

Tactic:
(hasColimit_iff_small_colimitType F).mpr inferInstance

Premises used: Iff.mpr, inferInstance, CategoryTheory.Limits.Types.hasColimit_iff_small_colimitType
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
⊢ HasColimitsOfSize.{w, w, max v w, max (v + 1) (w + 1)} (Type (max w v))

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
⊢ HasColimitsOfSize.{w, w, max v w, max (v + 1) (w + 1)} (Type (max v w))

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
⊢ HasColimitsOfSize.{0, 0, v, v + 1} (Type v)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
⊢ HasColimitsOfSize.{v, v, v, v + 1} (Type v)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
inst_1 : UnivLE.{v, u}
⊢ HasColimitsOfSize.{v, v, u, u + 1} (Type u)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasColimit F
j : J
x : F.obj j
⊢ Eq.{u + 1} (α := colimit F)
    ((Equiv.symm (colimitEquivColimitType F) : (a : F.ColimitType) → colimit F)
        (Quot.mk F.ColimitTypeRel (Sigma.mk (β := fun (j : J) ↦ F.obj j) j x)) :
      colimit F)
    ((hom (FC := TypeCat.Fun) (colimit.ι F j) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (colimit F))
        x :
      (fun (X : Type u) ↦ X) (colimit F))

Tactic:
congr_hom (IsColimit.comp_coconePointUniqueUpToIso_inv (colimit.isColimit F) _ _) x

Premises used: CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.colimit, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Functor.ιColimitType
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasColimit F
j : J
x : F.obj j
a :
  Eq.{u + 1} (α := colimit F)
    ((Equiv.symm (colimitEquivColimitType F) : (a : F.ColimitType) → colimit F)
        ((colimitEquivColimitType F : (a : colimit F) → F.ColimitType)
          ((hom (FC := TypeCat.Fun) (colimit.ι F j) :
              (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (colimit F))
            x)) :
      colimit F)
    ((Equiv.symm (colimitEquivColimitType F) : (a : F.ColimitType) → colimit F)
        (Quot.mk F.ColimitTypeRel (Sigma.mk (β := fun (j : J) ↦ F.obj j) j x)) :
      colimit F)
⊢ (colimitEquivColimitType F : (a : colimit F) → F.ColimitType)
      ((hom (FC := TypeCat.Fun) (colimit.ι F j) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (colimit F))
        x) =
    Quot.mk F.ColimitTypeRel (Sigma.mk (β := fun (j : J) ↦ F.obj j) j x)

Tactic:
apply (colimitEquivColimitType F).symm.injective

Premises used: CategoryTheory.Limits.Types.colimitEquivColimitType, Equiv.injective, Equiv.symm
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasColimit F
j : J
x : F.obj j
⊢ Eq.{u + 1} (α := colimit F)
    ((Equiv.symm (colimitEquivColimitType F) : (a : F.ColimitType) → colimit F)
        ((colimitEquivColimitType F : (a : colimit F) → F.ColimitType)
          ((hom (FC := TypeCat.Fun) (colimit.ι F j) :
              (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (colimit F))
            x)) :
      colimit F)
    ((Equiv.symm (colimitEquivColimitType F) : (a : F.ColimitType) → colimit F)
        (Quot.mk F.ColimitTypeRel (Sigma.mk (β := fun (j : J) ↦ F.obj j) j x)) :
      colimit F)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasColimit F
j j' : J
x : F.obj j
f : j ⟶ j'
rw :
  Eq (α := (fun (X : Type u) ↦ X) (colimit F))
    ((hom (FC := TypeCat.Fun) (F.map f ≫ colimit.ι F j') : (a : (fun (X : Type u) ↦ X) (F.obj j)) → colimit F) x :
      colimit F)
    ((hom (FC := TypeCat.Fun) (colimit.ι F j) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (colimit F))
        x :
      (fun (X : Type u) ↦ X) (colimit F))
⊢ Eq (α := (fun (X : Type u) ↦ X) (colimit F))
    ((hom (FC := TypeCat.Fun) (colimit.ι F j') :
          (a : (fun (X : Type u) ↦ X) (F.obj j')) → (fun (X : Type u) ↦ X) (colimit F))
        ((hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj j'))
            x :
          (fun (X : Type u) ↦ X) (F.obj j')) :
      (fun (X : Type u) ↦ X) (colimit F))
    ((hom (FC := TypeCat.Fun) (colimit.ι F j) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (colimit F))
        x :
      (fun (X : Type u) ↦ X) (colimit F))

Tactic:
rw [← comp_apply]

Premises used: CategoryTheory.comp_apply
-- Module: Mathlib.CategoryTheory.Limits.Types.Colimits
Goal:
J : Type v
inst : Category.{w, v} J
F : Functor.{w, u, v, u + 1} J (Type u)
inst_1 : HasColimit F
j j' : J
x : F.obj j
f : j ⟶ j'
⊢ Eq (α := (fun (X : Type u) ↦ X) (colimit F))
    ((hom (FC := TypeCat.Fun) (F.map f ≫ colimit.ι F j') : (a : (fun (X : Type u) ↦ X) (F.obj j)) → colimit F) x :
      colimit F)
    ((hom (FC := TypeCat.Fun) (colimit.ι F j) :
          (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (colimit F))
        x :
      (fun (X : Type u) ↦ X) (colimit F))

Tactic:
congr_hom (colimit.w F f) x

Premises used: CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Limits.colimit.w