awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : IsColimitCore.{w₂, w₁, w₀, v, u} c
G : Functor.{v, w₀', u, w₀' + 1} J (Type w₀')
e : (j : J) → Equiv.{w₀' + 1, w₀ + 1} (G.obj j) (F.obj j)
naturality :
  ∀ {j j' : J} (f : j ⟶ j'),
    Eq (α := (fun (X : Type w₀') ↦ X) (G.obj j) → F.obj j')
      (Function.comp (β := G.obj j') (⇑(e j') : (a : G.obj j') → F.obj j')
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f)) :
          (a : (fun (X : Type w₀') ↦ X) (G.obj j)) → (fun (X : Type w₀') ↦ X) (G.obj j')))
      (Function.comp (β := (fun (X : Type w₀) ↦ X) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj j'))
        (⇑(e j) : (a : G.obj j) → F.obj j))
c' : CoconeTypes.{w₂, w₀', v, u} G
j : J
rw :
  Function.comp.{w₀' + 1, w₁ + 1, w₂ + 1} (β :=
      pt.{w₁, w₀', v, u} (F := G) (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯))
      (hc.desc (c'.precompose (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) ⋯))
      ((fun (j : J) ↦ (c.ι j ∘ (⇑(e j) : (a : G.obj j) → F.obj j) : G.obj j → c.pt)) j) =
    c'.ι j
rw₁ :
  Function.comp.{w₀' + 1, w₀ + 1, w₂ + 1} (β := F.obj j)
      (hc.desc (c'.precompose (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) ⋯) ∘ c.ι j)
      (⇑(e j) : (a : G.obj j) → F.obj j) =
    c'.ι j
rw₂ :
  ι (c'.precompose (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) ⋯) j ∘
      (⇑(e j) : (a : G.obj j) → F.obj j) =
    c'.ι j
rw₃ :
  Function.comp.{w₀' + 1, w₀ + 1, w₂ + 1} (β := F.obj j)
      ((fun (j : J) ↦ (c'.ι j ∘ (⇑(e j).symm : (a : F.obj j) → G.obj j) : F.obj j → c'.pt)) j)
      (⇑(e j) : (a : G.obj j) → F.obj j) =
    c'.ι j
rw₄ :
  c'.ι j ∘
      Function.comp.{w₀' + 1, w₀ + 1, w₀' + 1} (β := F.obj j) (⇑(e j).symm : (a : F.obj j) → G.obj j)
        (⇑(e j) : (a : G.obj j) → F.obj j) =
    c'.ι j
rw₅ : c'.ι j ∘ id = c'.ι j
rw₆ rw₇ : c'.ι j = c'.ι j
⊢ Function.comp (β :=
      pt.{w₁, w₀', v, u} (F := G) (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯))
      (hc.desc (c'.precompose (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) ⋯))
      (ι (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯) j) =
    c'.ι j

Tactic:
rw [precompose_ι, ← Function.comp_assoc, hc.fac, precompose_ι, Function.comp_assoc,
      Equiv.symm_comp_self, Function.comp_id]

Premises used: Function.comp_id, Equiv.symm_comp_self, CategoryTheory.Functor.CoconeTypes.IsColimitCore.fac, CategoryTheory.Functor.CoconeTypes.precompose_ι, Function.comp_assoc
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : IsColimitCore.{w₂, w₁, w₀, v, u} c
G : Functor.{v, w₀', u, w₀' + 1} J (Type w₀')
e : (j : J) → Equiv.{w₀' + 1, w₀ + 1} (G.obj j) (F.obj j)
naturality :
  ∀ {j j' : J} (f : j ⟶ j'),
    Eq (α := (fun (X : Type w₀') ↦ X) (G.obj j) → F.obj j')
      (Function.comp (β := G.obj j') (⇑(e j') : (a : G.obj j') → F.obj j')
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f)) :
          (a : (fun (X : Type w₀') ↦ X) (G.obj j)) → (fun (X : Type w₀') ↦ X) (G.obj j')))
      (Function.comp (β := (fun (X : Type w₀) ↦ X) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj j'))
        (⇑(e j) : (a : G.obj j) → F.obj j))
T : Type w₂
f g : pt.{w₁, w₀', v, u} (F := G) (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯) → T
h :
  ∀ (j : J),
    f ∘ ι (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯) j =
      g ∘ ι (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯) j
j : J
h₁ : ∀ (x : F.obj j), (f ∘ c.ι j) x = (g ∘ c.ι j) x
⊢ f ∘ c.ι j = g ∘ c.ι j

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : IsColimitCore.{w₂, w₁, w₀, v, u} c
G : Functor.{v, w₀', u, w₀' + 1} J (Type w₀')
e : (j : J) → Equiv.{w₀' + 1, w₀ + 1} (G.obj j) (F.obj j)
naturality :
  ∀ {j j' : J} (f : j ⟶ j'),
    Eq (α := (fun (X : Type w₀') ↦ X) (G.obj j) → F.obj j')
      (Function.comp (β := G.obj j') (⇑(e j') : (a : G.obj j') → F.obj j')
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f)) :
          (a : (fun (X : Type w₀') ↦ X) (G.obj j)) → (fun (X : Type w₀') ↦ X) (G.obj j')))
      (Function.comp (β := (fun (X : Type w₀) ↦ X) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj j'))
        (⇑(e j) : (a : G.obj j) → F.obj j))
T : Type w₂
f g : pt.{w₁, w₀', v, u} (F := G) (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯) → T
h :
  ∀ (j : J),
    f ∘ ι (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯) j =
      g ∘ ι (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯) j
j : J
x : F.obj j
h₁ : ∀ (y : G.obj j), (f ∘ c.ι j) ((e j : (a : G.obj j) → F.obj j) y) = (g ∘ c.ι j) ((e j : (a : G.obj j) → F.obj j) y)
⊢ (f ∘ c.ι j) x = (g ∘ c.ι j) x

Tactic:
obtain ⟨y, rfl⟩ := (e j).surjective x

Premises used: Equiv.surjective, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : IsColimitCore.{w₂, w₁, w₀, v, u} c
G : Functor.{v, w₀', u, w₀' + 1} J (Type w₀')
e : (j : J) → Equiv.{w₀' + 1, w₀ + 1} (G.obj j) (F.obj j)
naturality :
  ∀ {j j' : J} (f : j ⟶ j'),
    Eq (α := (fun (X : Type w₀') ↦ X) (G.obj j) → F.obj j')
      (Function.comp (β := G.obj j') (⇑(e j') : (a : G.obj j') → F.obj j')
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f)) :
          (a : (fun (X : Type w₀') ↦ X) (G.obj j)) → (fun (X : Type w₀') ↦ X) (G.obj j')))
      (Function.comp (β := (fun (X : Type w₀) ↦ X) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj j'))
        (⇑(e j) : (a : G.obj j) → F.obj j))
T : Type w₂
f g : pt.{w₁, w₀', v, u} (F := G) (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯) → T
h :
  ∀ (j : J),
    f ∘ ι (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯) j =
      g ∘ ι (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯) j
j : J
y : G.obj j
⊢ (f ∘ c.ι j) ((e j : (a : G.obj j) → F.obj j) y) = (g ∘ c.ι j) ((e j : (a : G.obj j) → F.obj j) y)

Tactic:
congr_fun (h j) y

Premises used: congr_fun
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : IsColimitCore.{w₂, w₁, w₀, v, u} c
G : Functor.{v, w₀', u, w₀' + 1} J (Type w₀')
e : (j : J) → Equiv.{w₀' + 1, w₀ + 1} (G.obj j) (F.obj j)
naturality :
  ∀ {j j' : J} (f : j ⟶ j'),
    Eq (α := (fun (X : Type w₀') ↦ X) (G.obj j) → F.obj j')
      (Function.comp (β := G.obj j') (⇑(e j') : (a : G.obj j') → F.obj j')
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f)) :
          (a : (fun (X : Type w₀') ↦ X) (G.obj j)) → (fun (X : Type w₀') ↦ X) (G.obj j')))
      (Function.comp (β := (fun (X : Type w₀) ↦ X) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj j'))
        (⇑(e j) : (a : G.obj j) → F.obj j))
T : Type w₂
f g : pt.{w₁, w₀', v, u} (F := G) (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯) → T
h :
  ∀ (j : J),
    f ∘ ι (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯) j =
      g ∘ ι (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯) j
j : J
y : G.obj j
⊢ (f ∘ c.ι j) ((e j : (a : G.obj j) → F.obj j) y) = (g ∘ c.ι j) ((e j : (a : G.obj j) → F.obj j) y)

Tactic:
exact congr_fun (h j) y

Premises used: congr_fun
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimitCore
y : F.ColimitType
obtain :
  ∀ (j : J) (x : F.obj j), hc.down.desc F.coconeTypes (F.descColimitType c (F.ιColimitType j x)) = F.ιColimitType j x
⊢ hc.down.desc F.coconeTypes (F.descColimitType c y) = y

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

Premises used: CategoryTheory.Functor.ιColimitType_jointly_surjective, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimitCore
j : J
x : F.obj j
⊢ hc.down.desc F.coconeTypes (F.descColimitType c (F.ιColimitType j x)) = F.ιColimitType j x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimitCore
j : J
rw : (F.descColimitType c ∘ hc.down.desc F.coconeTypes) ∘ c.ι j = c.ι j
rw₁ : F.descColimitType c ∘ hc.down.desc F.coconeTypes ∘ c.ι j = c.ι j
rw₂ : F.descColimitType c ∘ F.coconeTypes.ι j = c.ι j
rw₃ : F.descColimitType c ∘ (fun (j : J) ↦ F.ιColimitType j) j = c.ι j
rw₄ rw₅ : c.ι j = c.ι j
⊢ (F.descColimitType c ∘ hc.down.desc F.coconeTypes) ∘ c.ι j = id ∘ c.ι j

Tactic:
rw [Function.id_comp, Function.comp_assoc, fac,
                coconeTypes_ι, descColimitType_comp_ι]

Premises used: CategoryTheory.Functor.descColimitType_comp_ι, CategoryTheory.Functor.CoconeTypes.IsColimitCore.fac, CategoryTheory.Functor.coconeTypes_ι, Function.comp_assoc, Function.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimitCore
⊢ F.descColimitType c ∘ hc.down.desc F.coconeTypes = id

Tactic:
have : (F.descColimitType c).comp
              ((down.{max u w₁} hc).desc F.coconeTypes) = id :=
            (down.{max u w₀} hc).funext (fun j ↦ by
              rw [Function.id_comp, Function.comp_assoc, fac,
                coconeTypes_ι, descColimitType_comp_ι])
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimitCore
this : F.descColimitType c ∘ hc.down.desc F.coconeTypes = id
⊢ Function.RightInverse (hc.down.desc F.coconeTypes) (F.descColimitType c)

Tactic:
congr_fun this

Premises used: Function.LeftInverse, Function.RightInverse, congr_fun
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimitCore
this : F.descColimitType c ∘ hc.down.desc F.coconeTypes = id
⊢ Function.RightInverse (hc.down.desc F.coconeTypes) (F.descColimitType c)

Tactic:
exact congr_fun this

Premises used: congr_fun
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimitCore
e : F.ColimitType ≃ c.pt :=
  { toFun := F.descColimitType c, invFun := hc.down.desc F.coconeTypes, left_inv := ⋯, right_inv := ⋯ }
⊢ Function.Bijective (F.descColimitType c)

Tactic:
e.bijective

Premises used: Equiv.bijective, CategoryTheory.Functor.descColimitType
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimitCore
e : F.ColimitType ≃ c.pt :=
  { toFun := F.descColimitType c, invFun := hc.down.desc F.coconeTypes, left_inv := ⋯, right_inv := ⋯ }
⊢ Function.Bijective (F.descColimitType c)

Tactic:
exact e.bijective

Premises used: Equiv.bijective
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
hc : c.IsColimit
G : Functor.{v, w₀', u, w₀' + 1} J (Type w₀')
e : (j : J) → Equiv.{w₀' + 1, w₀ + 1} (G.obj j) (F.obj j)
naturality :
  ∀ {j j' : J} (f : j ⟶ j'),
    Eq (α := (fun (X : Type w₀') ↦ X) (G.obj j) → F.obj j')
      (Function.comp (β := G.obj j') (⇑(e j') : (a : G.obj j') → F.obj j')
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f)) :
          (a : (fun (X : Type w₀') ↦ X) (G.obj j)) → (fun (X : Type w₀') ↦ X) (G.obj j')))
      (Function.comp (β := (fun (X : Type w₀) ↦ X) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj j'))
        (⇑(e j) : (a : G.obj j) → F.obj j))
⊢ IsColimit.{w₁, w₀', v, u} (F := G) (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯)

Tactic:
(hc.isColimitCore.precompose e naturality).isColimit

Premises used: CategoryTheory.Functor.CoconeTypes.IsColimit.isColimitCore, CategoryTheory.Functor.CoconeTypes.IsColimitCore.isColimit, CategoryTheory.Functor.CoconeTypes.IsColimitCore.precompose
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
G : Functor.{v, w₀', u, w₀' + 1} J (Type w₀')
e : (j : J) → Equiv.{w₀' + 1, w₀ + 1} (G.obj j) (F.obj j)
naturality :
  ∀ {j j' : J} (f : j ⟶ j'),
    Eq (α := (fun (X : Type w₀') ↦ X) (G.obj j) → F.obj j')
      (Function.comp (β := G.obj j') (⇑(e j') : (a : G.obj j') → F.obj j')
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f)) :
          (a : (fun (X : Type w₀') ↦ X) (G.obj j)) → (fun (X : Type w₀') ↦ X) (G.obj j')))
      (Function.comp (β := (fun (X : Type w₀) ↦ X) (F.obj j))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f)) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj j'))
        (⇑(e j) : (a : G.obj j) → F.obj j))
hc : IsColimit.{w₁, w₀', v, u} (F := G) (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯)
⊢ ∀ (j : J) (x : F.obj j),
    c.ι j x =
      (Equiv.refl
            (pt.{w₁, w₀, v, u} (F := F)
              (precompose.{w₁, w₀', w₀, v, u} (F := G)
                (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯)
                (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) ⋯)) :
          (a :
              ((c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯).precompose
                  (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) ⋯).pt) →
            c.pt)
        (ι
          (precompose.{w₁, w₀', w₀, v, u} (F := G)
            (c.precompose (fun {j' : J} ↦ (⇑(e j') : (a : G.obj j') → F.obj j')) ⋯)
            (fun {j' : J} ↦ (⇑(e j').symm : (a : F.obj j') → G.obj j')) ⋯)
          j x)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
⊢ Function.Bijective (α := F.ColimitType) id

Tactic:
Function.bijective_id

Premises used: Function.bijective_id
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
h : Eq (α := F.ColimitType → F.coconeTypes.pt) (F.descColimitType F.coconeTypes) id
⊢ Function.Bijective (β := F.coconeTypes.pt) (F.descColimitType F.coconeTypes)

Tactic:
convert! Function.bijective_id

Premises used: Function.bijective_id
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
h : ∀ (y : F.ColimitType), F.descColimitType F.coconeTypes y = id y
⊢ Eq (α := F.ColimitType → F.coconeTypes.pt) (F.descColimitType F.coconeTypes) id

Tactic:
ext y
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
y : F.ColimitType
h : ∀ (j : J) (x : F.obj j), F.descColimitType F.coconeTypes (F.ιColimitType j x) = id (F.ιColimitType j x)
⊢ F.descColimitType F.coconeTypes y = id y

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

Premises used: CategoryTheory.Functor.ιColimitType_jointly_surjective, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitType
Goal:
J : Type u
inst : Category.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
j : J
x : F.obj j
⊢ F.descColimitType F.coconeTypes (F.ιColimitType j x) = id (F.ιColimitType j x)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFiltered.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
x y : (j : J) × F.obj j
mp :
  Relation.EqvGen F.ColimitTypeRel x y →
    ∃ (k : J) (f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ k) (g : y.fst (β := fun (j : J) ↦ F.obj j) ⟶ k),
      Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type w₀) ↦ X) (F.obj x.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
            (x.snd (β := fun (j : J) ↦ F.obj j)) :
          (fun (X : Type w₀) ↦ X) (F.obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
              (a : (fun (X : Type w₀) ↦ X) (F.obj y.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
            (y.snd (β := fun (j : J) ↦ F.obj j)) :
          (fun (X : Type w₀) ↦ X) (F.obj k))
mpr :
  (∃ (k : J) (f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ k) (g : y.fst (β := fun (j : J) ↦ F.obj j) ⟶ k),
      Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type w₀) ↦ X) (F.obj x.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
            (x.snd (β := fun (j : J) ↦ F.obj j)) :
          (fun (X : Type w₀) ↦ X) (F.obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
              (a : (fun (X : Type w₀) ↦ X) (F.obj y.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
            (y.snd (β := fun (j : J) ↦ F.obj j)) :
          (fun (X : Type w₀) ↦ X) (F.obj k))) →
    Relation.EqvGen F.ColimitTypeRel x y
⊢ Relation.EqvGen F.ColimitTypeRel x y ↔
    ∃ (k : J) (f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ k) (g : y.fst (β := fun (j : J) ↦ F.obj j) ⟶ k),
      Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type w₀) ↦ X) (F.obj x.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
            (x.snd (β := fun (j : J) ↦ F.obj j)) :
          (fun (X : Type w₀) ↦ X) (F.obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
              (a : (fun (X : Type w₀) ↦ X) (F.obj y.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
            (y.snd (β := fun (j : J) ↦ F.obj j)) :
          (fun (X : Type w₀) ↦ X) (F.obj k))

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFiltered.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
x_1 y_1 x y : (j : J) × F.obj j
h : F.ColimitTypeRel x y
mp :
  ∀ (f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ y.fst (β := fun (j : J) ↦ F.obj j))
    (h :
      y.snd (β := fun (j : J) ↦ F.obj j) =
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj x.fst)) → (fun (X : Type w₀) ↦ X) (F.obj y.fst))
          (x.snd (β := fun (j : J) ↦ F.obj j))),
    ∃ (k : J) (f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ k) (g : y.fst (β := fun (j : J) ↦ F.obj j) ⟶ k),
      Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type w₀) ↦ X) (F.obj x.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
            (x.snd (β := fun (j : J) ↦ F.obj j)) :
          (fun (X : Type w₀) ↦ X) (F.obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
              (a : (fun (X : Type w₀) ↦ X) (F.obj y.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
            (y.snd (β := fun (j : J) ↦ F.obj j)) :
          (fun (X : Type w₀) ↦ X) (F.obj k))
⊢ ∃ (k : J) (f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ k) (g : y.fst (β := fun (j : J) ↦ F.obj j) ⟶ k),
    Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj x.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          (x.snd (β := fun (j : J) ↦ F.obj j)) :
        (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj y.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          (y.snd (β := fun (j : J) ↦ F.obj j)) :
        (fun (X : Type w₀) ↦ X) (F.obj k))

Tactic:
obtain ⟨f, h⟩ := h
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFiltered.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
x_1 y_1 x y : (j : J) × F.obj j
f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ y.fst (β := fun (j : J) ↦ F.obj j)
h :
  y.snd (β := fun (j : J) ↦ F.obj j) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
        (a : (fun (X : Type w₀) ↦ X) (F.obj x.fst)) → (fun (X : Type w₀) ↦ X) (F.obj y.fst))
      (x.snd (β := fun (j : J) ↦ F.obj j))
⊢ Eq (α := (fun (X : Type w₀) ↦ X) (F.obj (y.fst (β := fun (j : J) ↦ F.obj j))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj x.fst)) → (fun (X : Type w₀) ↦ X) (F.obj y.fst))
        (x.snd (β := fun (j : J) ↦ F.obj j)) :
      (fun (X : Type w₀) ↦ X) (F.obj (y.fst (β := fun (j : J) ↦ F.obj j))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 (y.fst (β := fun (j : J) ↦ F.obj j)))) :
          (a : (fun (X : Type w₀) ↦ X) (F.obj y.fst)) → (fun (X : Type w₀) ↦ X) (F.obj y.fst))
        (y.snd (β := fun (j : J) ↦ F.obj j)) :
      (fun (X : Type w₀) ↦ X) (F.obj (y.fst (β := fun (j : J) ↦ F.obj j))))

Tactic:
simpa using h.symm

Premises used: Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFiltered.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
x_1 y_1 x y : (j : J) × F.obj j
f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ y.fst (β := fun (j : J) ↦ F.obj j)
h :
  y.snd (β := fun (j : J) ↦ F.obj j) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
        (a : (fun (X : Type w₀) ↦ X) (F.obj x.fst)) → (fun (X : Type w₀) ↦ X) (F.obj y.fst))
      (x.snd (β := fun (j : J) ↦ F.obj j))
⊢ ∃ (k : J) (f : x.fst (β := fun (j : J) ↦ F.obj j) ⟶ k) (g : y.fst (β := fun (j : J) ↦ F.obj j) ⟶ k),
    Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj x.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          (x.snd (β := fun (j : J) ↦ F.obj j)) :
        (fun (X : Type w₀) ↦ X) (F.obj k))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
            (a : (fun (X : Type w₀) ↦ X) (F.obj y.fst)) → (fun (X : Type w₀) ↦ X) (F.obj k))
          (y.snd (β := fun (j : J) ↦ F.obj j)) :
        (fun (X : Type w₀) ↦ X) (F.obj k))

Tactic:
exact ⟨y.1, f, 𝟙 _, by simpa using h.symm⟩