awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x : SmallCategory J
h : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
f : X ⟶ c.pt
j : (x : X) → J
g : (x_1 : X) → (fun (X : Type u) ↦ X) (F.obj (j x_1))
hg :
  ∀ (x_1 : X),
    Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) (j x_1)))
      ((hom (FC := TypeCat.Fun) (c.ι.app (j x_1)) :
            (a : (fun (X : Type u) ↦ X) (F.obj (j x_1))) →
              (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj (j x_1)))
          (g x_1) :
        (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) (j x_1)))
      ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) c.pt) x_1 :
        (fun (X : Type u) ↦ X) c.pt)
refine_1 :
  f =
    (hom (FC := TypeCat.Fun)
          (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (op X)) c)) (IsCardinalFiltered.max j hX)) :
        (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj (IsCardinalFiltered.max j hX))) →
          (fun (X : Type u) ↦ X)
            (((Functor.const J).obj ((coyoneda.obj (op X)).mapCocone c).pt).obj (IsCardinalFiltered.max j hX)))
      (↾fun (x_1 : unop (op X)) ↦
        (hom (FC := TypeCat.Fun) (F.map (IsCardinalFiltered.toMax j hX x_1)) :
            (a : (fun (X : Type u) ↦ X) (F.obj (j x_1))) → (fun (X : Type u) ↦ X) (F.obj (IsCardinalFiltered.max j hX)))
          (g x_1))
⊢ ∃ (i : J) (xi : (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (op X)).obj i)),
    f =
      (hom (FC := TypeCat.Fun) (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (op X)) c)) i) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj i)) →
            (fun (X : Type u) ↦ X) (((Functor.const J).obj ((coyoneda.obj (op X)).mapCocone c).pt).obj i))
        xi

Tactic:
refine ⟨IsCardinalFiltered.max j hX,
          ↾fun x ↦ F.map (IsCardinalFiltered.toMax j hX x) (g x), ?_⟩
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x : SmallCategory J
h : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
f : X ⟶ c.pt
j : (x : X) → J
g : (x_1 : X) → (fun (X : Type u) ↦ X) (F.obj (j x_1))
hg :
  ∀ (x_1 : X),
    Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) (j x_1)))
      ((hom (FC := TypeCat.Fun) (c.ι.app (j x_1)) :
            (a : (fun (X : Type u) ↦ X) (F.obj (j x_1))) →
              (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj (j x_1)))
          (g x_1) :
        (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) (j x_1)))
      ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) c.pt) x_1 :
        (fun (X : Type u) ↦ X) c.pt)
refine_1 :
  f =
    CategoryStruct.comp (Y := F.obj (IsCardinalFiltered.max j hX))
      (↾fun (x_1 : X) ↦
        (hom (FC := TypeCat.Fun) (F.map (IsCardinalFiltered.toMax j hX x_1)) :
            (a : F.obj (j x_1)) → F.obj (IsCardinalFiltered.max j hX))
          (g x_1))
      (c.ι.app (IsCardinalFiltered.max j hX))
⊢ f =
    (hom (FC := TypeCat.Fun)
          (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (op X)) c)) (IsCardinalFiltered.max j hX)) :
        (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj (IsCardinalFiltered.max j hX))) →
          (fun (X : Type u) ↦ X)
            (((Functor.const J).obj ((coyoneda.obj (op X)).mapCocone c).pt).obj (IsCardinalFiltered.max j hX)))
      (↾fun (x_1 : unop (op X)) ↦
        (hom (FC := TypeCat.Fun) (F.map (IsCardinalFiltered.toMax j hX x_1)) :
            (a : (fun (X : Type u) ↦ X) (F.obj (j x_1))) → (fun (X : Type u) ↦ X) (F.obj (IsCardinalFiltered.max j hX)))
          (g x_1))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x : SmallCategory J
h : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
f : X ⟶ c.pt
j : (x : X) → J
g : (x_1 : X) → (fun (X : Type u) ↦ X) (F.obj (j x_1))
hg :
  ∀ (x_1 : X),
    Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) (j x_1)))
      ((hom (FC := TypeCat.Fun) (c.ι.app (j x_1)) :
            (a : (fun (X : Type u) ↦ X) (F.obj (j x_1))) →
              (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj (j x_1)))
          (g x_1) :
        (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) (j x_1)))
      ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) c.pt) x_1 :
        (fun (X : Type u) ↦ X) c.pt)
refine_1 :
  ∀ (x_1 : X),
    (hom (FC := TypeCat.Fun) f).toFun x_1 =
      TypeCat.Fun.toFun
        (hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := F.obj (IsCardinalFiltered.max j hX))
            (↾fun (x_2 : X) ↦
              (hom (FC := TypeCat.Fun) (F.map (IsCardinalFiltered.toMax j hX x_2)) :
                  (a : F.obj (j x_2)) → F.obj (IsCardinalFiltered.max j hX))
                (g x_2))
            (c.ι.app (IsCardinalFiltered.max j hX))))
        x_1
⊢ f =
    CategoryStruct.comp (Y := F.obj (IsCardinalFiltered.max j hX))
      (↾fun (x_1 : X) ↦
        (hom (FC := TypeCat.Fun) (F.map (IsCardinalFiltered.toMax j hX x_1)) :
            (a : F.obj (j x_1)) → F.obj (IsCardinalFiltered.max j hX))
          (g x_1))
      (c.ι.app (IsCardinalFiltered.max j hX))

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x_1 : SmallCategory J
h : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
f : X ⟶ c.pt
j : (x : X) → J
g : (x : X) → (fun (X : Type u) ↦ X) (F.obj (j x))
hg :
  ∀ (x : X),
    Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) (j x)))
      ((hom (FC := TypeCat.Fun) (c.ι.app (j x)) :
            (a : (fun (X : Type u) ↦ X) (F.obj (j x))) →
              (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj (j x)))
          (g x) :
        (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) (j x)))
      ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) c.pt) x :
        (fun (X : Type u) ↦ X) c.pt)
x : X
refine_1 :
  Eq (α := c.pt) ((hom (FC := TypeCat.Fun) f : (a : X) → c.pt) x : c.pt)
    ((hom (FC := TypeCat.Fun) (c.ι.app (IsCardinalFiltered.max j hX)) :
          (a : F.obj (IsCardinalFiltered.max j hX)) → c.pt)
        ((hom (FC := TypeCat.Fun) (F.map (IsCardinalFiltered.toMax j hX x)) :
              (a : F.obj (j x)) → F.obj (IsCardinalFiltered.max j hX))
            (g x) :
          F.obj (IsCardinalFiltered.max j hX)) :
      c.pt)
⊢ (hom (FC := TypeCat.Fun) f).toFun x =
    TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := F.obj (IsCardinalFiltered.max j hX))
          (↾fun (x : X) ↦
            (hom (FC := TypeCat.Fun) (F.map (IsCardinalFiltered.toMax j hX x)) :
                (a : F.obj (j x)) → F.obj (IsCardinalFiltered.max j hX))
              (g x))
          (c.ι.app (IsCardinalFiltered.max j hX))))
      x

Tactic:
dsimp at j g hg x ⊢
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x_1 : SmallCategory J
h : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
f : X ⟶ c.pt
j : (x : X) → J
g : (x : X) → F.obj (j x)
hg :
  ∀ (x : X),
    Eq (α := c.pt) ((hom (FC := TypeCat.Fun) (c.ι.app (j x)) : (a : F.obj (j x)) → c.pt) (g x) : c.pt)
      ((hom (FC := TypeCat.Fun) f : (a : X) → c.pt) x : c.pt)
x : X
refine_1 :
  Eq (α := c.pt) ((hom (FC := TypeCat.Fun) (c.ι.app (j x)) : (a : F.obj (j x)) → c.pt) (g x) : c.pt)
    ((hom (FC := TypeCat.Fun) (c.ι.app (IsCardinalFiltered.max j hX)) :
          (a : F.obj (IsCardinalFiltered.max j hX)) → c.pt)
        ((hom (FC := TypeCat.Fun) (F.map (IsCardinalFiltered.toMax j hX x)) :
              (a : F.obj (j x)) → F.obj (IsCardinalFiltered.max j hX))
            (g x) :
          F.obj (IsCardinalFiltered.max j hX)) :
      c.pt)
⊢ Eq (α := c.pt) ((hom (FC := TypeCat.Fun) f : (a : X) → c.pt) x : c.pt)
    ((hom (FC := TypeCat.Fun) (c.ι.app (IsCardinalFiltered.max j hX)) :
          (a : F.obj (IsCardinalFiltered.max j hX)) → c.pt)
        ((hom (FC := TypeCat.Fun) (F.map (IsCardinalFiltered.toMax j hX x)) :
              (a : F.obj (j x)) → F.obj (IsCardinalFiltered.max j hX))
            (g x) :
          F.obj (IsCardinalFiltered.max j hX)) :
      c.pt)

Tactic:
rw [← hg]
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x_1 : SmallCategory J
h : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
f : X ⟶ c.pt
j : (x : X) → J
g : (x : X) → F.obj (j x)
hg :
  ∀ (x : X),
    Eq (α := c.pt) ((hom (FC := TypeCat.Fun) (c.ι.app (j x)) : (a : F.obj (j x)) → c.pt) (g x) : c.pt)
      ((hom (FC := TypeCat.Fun) f : (a : X) → c.pt) x : c.pt)
x : X
⊢ Eq (α := c.pt) ((hom (FC := TypeCat.Fun) (c.ι.app (j x)) : (a : F.obj (j x)) → c.pt) (g x) : c.pt)
    ((hom (FC := TypeCat.Fun) (c.ι.app (IsCardinalFiltered.max j hX)) :
          (a : F.obj (IsCardinalFiltered.max j hX)) → c.pt)
        ((hom (FC := TypeCat.Fun) (F.map (IsCardinalFiltered.toMax j hX x)) :
              (a : F.obj (j x)) → F.obj (IsCardinalFiltered.max j hX))
            (g x) :
          F.obj (IsCardinalFiltered.max j hX)) :
      c.pt)

Tactic:
congr_hom (c.w (IsCardinalFiltered.toMax j hX x)).symm (g x)

Premises used: CategoryTheory.IsCardinalFiltered.toMax, CategoryTheory.Limits.Cocone.w, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x_1 : SmallCategory J
h : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
f : X ⟶ c.pt
j : (x : X) → J
g : (x : X) → F.obj (j x)
hg :
  ∀ (x : X),
    Eq (α := c.pt) ((hom (FC := TypeCat.Fun) (c.ι.app (j x)) : (a : F.obj (j x)) → c.pt) (g x) : c.pt)
      ((hom (FC := TypeCat.Fun) f : (a : X) → c.pt) x : c.pt)
x : X
⊢ Eq (α := c.pt) ((hom (FC := TypeCat.Fun) (c.ι.app (j x)) : (a : F.obj (j x)) → c.pt) (g x) : c.pt)
    ((hom (FC := TypeCat.Fun) (c.ι.app (IsCardinalFiltered.max j hX)) :
          (a : F.obj (IsCardinalFiltered.max j hX)) → c.pt)
        ((hom (FC := TypeCat.Fun) (F.map (IsCardinalFiltered.toMax j hX x)) :
              (a : F.obj (j x)) → F.obj (IsCardinalFiltered.max j hX))
            (g x) :
          F.obj (IsCardinalFiltered.max j hX)) :
      c.pt)

Tactic:
exact congr_hom (c.w (IsCardinalFiltered.toMax j hX x)).symm (g x)

Premises used: CategoryTheory.IsCardinalFiltered.toMax, CategoryTheory.Limits.Cocone.w, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
j : J
f g : (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (op X)).obj j)
h :
  Eq (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj
        (Functor.obj (Functor.const J)
          (Cocone.pt (F := F ⋙ Functor.obj coyoneda (op X)) (Functor.mapCocone (Functor.obj coyoneda (op X)) c)))
        j))
    ((hom (FC := TypeCat.Fun) (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (op X)) c)) j) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj j)) →
            (fun (X : Type u) ↦ X) (((Functor.const J).obj ((coyoneda.obj (op X)).mapCocone c).pt).obj j))
        f :
      (fun (X : Type u) ↦ X)
        (Functor.obj
          (Functor.obj (Functor.const J)
            (Cocone.pt (F := F ⋙ Functor.obj coyoneda (op X)) (Functor.mapCocone (Functor.obj coyoneda (op X)) c)))
          j))
    ((hom (FC := TypeCat.Fun) (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (op X)) c)) j) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj j)) →
            (fun (X : Type u) ↦ X) (((Functor.const J).obj ((coyoneda.obj (op X)).mapCocone c).pt).obj j))
        g :
      (fun (X : Type u) ↦ X)
        (Functor.obj
          (Functor.obj (Functor.const J)
            (Cocone.pt (F := F ⋙ Functor.obj coyoneda (op X)) (Functor.mapCocone (Functor.obj coyoneda (op X)) c)))
          j))
k : (x : ToType (FC := TypeCat.Fun) (unop (op X))) → J
a : (x_1 : ToType (FC := TypeCat.Fun) (unop (op X))) → j ⟶ k x_1
hk :
  ∀ (x_1 : ToType (FC := TypeCat.Fun) (unop (op X))),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj (k x_1)))
      ((hom (FC := TypeCat.Fun) (F.map (a x_1)) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj (k x_1)))
          (f.hom'.toFun x_1) :
        (fun (X : Type u) ↦ X) (F.obj (k x_1)))
      ((hom (FC := TypeCat.Fun) (F.map (a x_1)) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj (k x_1)))
          (g.hom'.toFun x_1) :
        (fun (X : Type u) ↦ X) (F.obj (k x_1)))
refine_2 : ∃ (k : J) (f_1 : j ⟶ k), f ≫ F.map f_1 = g ≫ F.map f_1
⊢ ∃ (k : J) (f_1 : j ⟶ k),
    Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (op X)).obj k))
      ((hom (FC := TypeCat.Fun) ((F ⋙ Functor.obj coyoneda (op X)).map f_1) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj j)) →
              (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj k))
          f :
        (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (op X)).obj k))
      ((hom (FC := TypeCat.Fun) ((F ⋙ Functor.obj coyoneda (op X)).map f_1) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj j)) →
              (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj k))
          g :
        (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (op X)).obj k))

Tactic:
dsimp at f g h k a hk ⊢
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
j : J
f g : X ⟶ F.obj j
h : f ≫ c.ι.app j = g ≫ c.ι.app j
k : (x : ToType (FC := TypeCat.Fun) X) → J
a : (x_1 : ToType (FC := TypeCat.Fun) X) → j ⟶ k x_1
hk :
  ∀ (x_1 : ToType (FC := TypeCat.Fun) X),
    Eq (α := F.obj (k x_1))
      ((hom (FC := TypeCat.Fun) (F.map (a x_1)) : (a : F.obj j) → F.obj (k x_1)) ((f.hom' : (a : X) → F.obj j) x_1) :
        F.obj (k x_1))
      ((hom (FC := TypeCat.Fun) (F.map (a x_1)) : (a : F.obj j) → F.obj (k x_1)) ((g.hom' : (a : X) → F.obj j) x_1) :
        F.obj (k x_1))
⊢ ∀ (x_1 : ToType (FC := TypeCat.Fun) X),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj (k x_1)))
      ((hom (FC := TypeCat.Fun) (F.map (a x_1)) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj (k x_1)))
          ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (F.obj j)) x_1) :
        (fun (X : Type u) ↦ X) (F.obj (k x_1)))
      ((hom (FC := TypeCat.Fun) (F.map (a x_1)) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj (k x_1)))
          ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (F.obj j)) x_1) :
        (fun (X : Type u) ↦ X) (F.obj (k x_1)))

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
j : J
f g : X ⟶ F.obj j
h : f ≫ c.ι.app j = g ≫ c.ι.app j
k : (x : ToType (FC := TypeCat.Fun) X) → J
a : (x_1 : ToType (FC := TypeCat.Fun) X) → j ⟶ k x_1
hk :
  ∀ (x_1 : ToType (FC := TypeCat.Fun) X),
    Eq (α := F.obj (k x_1))
      ((hom (FC := TypeCat.Fun) (F.map (a x_1)) : (a : F.obj j) → F.obj (k x_1)) ((f.hom' : (a : X) → F.obj j) x_1) :
        F.obj (k x_1))
      ((hom (FC := TypeCat.Fun) (F.map (a x_1)) : (a : F.obj j) → F.obj (k x_1)) ((g.hom' : (a : X) → F.obj j) x_1) :
        F.obj (k x_1))
⊢ ∀ (x_1 : ToType (FC := TypeCat.Fun) X),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj (k x_1)))
      ((hom (FC := TypeCat.Fun) (F.map (a x_1)) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj (k x_1)))
          ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (F.obj j)) x_1) :
        (fun (X : Type u) ↦ X) (F.obj (k x_1)))
      ((hom (FC := TypeCat.Fun) (F.map (a x_1)) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj (k x_1)))
          ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (F.obj j)) x_1) :
        (fun (X : Type u) ↦ X) (F.obj (k x_1)))

Tactic:
replace hk : ∀ x, F.map (a x) (f x) = F.map (a x) (g x) := by assumption
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x_1 : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
j : J
f g : X ⟶ F.obj j
h : f ≫ c.ι.app j = g ≫ c.ι.app j
k : (x : ToType (FC := TypeCat.Fun) X) → J
a : (x : ToType (FC := TypeCat.Fun) X) → j ⟶ k x
hk :
  ∀ (x : ToType (FC := TypeCat.Fun) X),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj (k x)))
      ((hom (FC := TypeCat.Fun) (F.map (a x)) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj (k x)))
          ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (F.obj j)) x) :
        (fun (X : Type u) ↦ X) (F.obj (k x)))
      ((hom (FC := TypeCat.Fun) (F.map (a x)) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj (k x)))
          ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (F.obj j)) x) :
        (fun (X : Type u) ↦ X) (F.obj (k x)))
φ : (x : X) → j ⟶ IsCardinalFiltered.max k hX := fun (x : X) ↦ a x ≫ IsCardinalFiltered.toMax k hX x
x : ToType (FC := TypeCat.Fun) X
⊢ Eq (α := j ⟶ IsCardinalFiltered.coeq φ hX)
    (a x ≫
      (fun (x : ToType (FC := TypeCat.Fun) X) ↦
          (IsCardinalFiltered.toMax k hX x ≫ IsCardinalFiltered.coeqHom φ hX : k x ⟶ IsCardinalFiltered.coeq φ hX))
        x)
    (IsCardinalFiltered.toCoeq φ hX)

Tactic:
simpa [φ] using IsCardinalFiltered.coeq_condition φ hX x

Premises used: CategoryTheory.IsCardinalFiltered.coeq_condition
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
j : J
f g : X ⟶ F.obj j
h : f ≫ c.ι.app j = g ≫ c.ι.app j
k : (x : ToType (FC := TypeCat.Fun) X) → J
a : (x_1 : ToType (FC := TypeCat.Fun) X) → j ⟶ k x_1
hk :
  ∀ (x_1 : ToType (FC := TypeCat.Fun) X),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj (k x_1)))
      ((hom (FC := TypeCat.Fun) (F.map (a x_1)) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj (k x_1)))
          ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (F.obj j)) x_1) :
        (fun (X : Type u) ↦ X) (F.obj (k x_1)))
      ((hom (FC := TypeCat.Fun) (F.map (a x_1)) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj (k x_1)))
          ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (F.obj j)) x_1) :
        (fun (X : Type u) ↦ X) (F.obj (k x_1)))
φ : (x_1 : X) → j ⟶ IsCardinalFiltered.max k hX := fun (x_1 : X) ↦ a x_1 ≫ IsCardinalFiltered.toMax k hX x_1
⊢ ∃ (l : J) (c : j ⟶ l) (b : (x_1 : ToType (FC := TypeCat.Fun) X) → k x_1 ⟶ l),
    ∀ (x_1 : ToType (FC := TypeCat.Fun) X), a x_1 ≫ b x_1 = c

Tactic:
exact ⟨IsCardinalFiltered.coeq φ hX,
            IsCardinalFiltered.toCoeq φ hX,
            fun x ↦ IsCardinalFiltered.toMax k hX x ≫ IsCardinalFiltered.coeqHom φ hX,
            fun x ↦ by simpa [φ] using IsCardinalFiltered.coeq_condition φ hX x⟩
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
j : J
f g : X ⟶ F.obj j
h : f ≫ c.ι.app j = g ≫ c.ι.app j
k : (x : ToType (FC := TypeCat.Fun) X) → J
a : (x_1 : ToType (FC := TypeCat.Fun) X) → j ⟶ k x_1
hk :
  ∀ (x_1 : ToType (FC := TypeCat.Fun) X),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj (k x_1)))
      ((hom (FC := TypeCat.Fun) (F.map (a x_1)) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj (k x_1)))
          ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (F.obj j)) x_1) :
        (fun (X : Type u) ↦ X) (F.obj (k x_1)))
      ((hom (FC := TypeCat.Fun) (F.map (a x_1)) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj (k x_1)))
          ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (F.obj j)) x_1) :
        (fun (X : Type u) ↦ X) (F.obj (k x_1)))
refine_2 :
  ∀ (l : J) (b : j ⟶ l) (c : (x_1 : ToType (FC := TypeCat.Fun) X) → k x_1 ⟶ l)
    (hl : ∀ (x_1 : ToType (FC := TypeCat.Fun) X), a x_1 ≫ c x_1 = b),
    ∃ (k : J) (f_1 : j ⟶ k), f ≫ F.map f_1 = g ≫ F.map f_1
⊢ ∃ (k : J) (f_1 : j ⟶ k), f ≫ F.map f_1 = g ≫ F.map f_1

Tactic:
obtain ⟨l, b, c, hl⟩ : ∃ (l : J) (c : j ⟶ l) (b : ∀ x, k x ⟶ l),
            ∀ x, a x ≫ b x = c := by
          let φ (x : X) : j ⟶ IsCardinalFiltered.max k hX :=
            a x ≫ IsCardinalFiltered.toMax k hX x
          exact ⟨IsCardinalFiltered.coeq φ hX,
            IsCardinalFiltered.toCoeq φ hX,
            fun x ↦ IsCardinalFiltered.toMax k hX x ≫ IsCardinalFiltered.coeqHom φ hX,
            fun x ↦ by simpa [φ] using IsCardinalFiltered.coeq_condition φ hX x⟩
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : J ⥤ Type u
c_1 : Cocone F
hc : IsColimit c_1
this : IsFiltered J
j : J
f g : X ⟶ F.obj j
h : f ≫ c_1.ι.app j = g ≫ c_1.ι.app j
k : (x : ToType (FC := TypeCat.Fun) X) → J
a : (x_1 : ToType (FC := TypeCat.Fun) X) → j ⟶ k x_1
hk :
  ∀ (x_1 : ToType (FC := TypeCat.Fun) X),
    Eq (α := (fun (X : Type u) ↦ X) (F.obj (k x_1)))
      ((hom (FC := TypeCat.Fun) (F.map (a x_1)) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj (k x_1)))
          ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (F.obj j)) x_1) :
        (fun (X : Type u) ↦ X) (F.obj (k x_1)))
      ((hom (FC := TypeCat.Fun) (F.map (a x_1)) :
            (a : (fun (X : Type u) ↦ X) (F.obj j)) → (fun (X : Type u) ↦ X) (F.obj (k x_1)))
          ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (F.obj j)) x_1) :
        (fun (X : Type u) ↦ X) (F.obj (k x_1)))
l : J
b : j ⟶ l
c : (x_1 : ToType (FC := TypeCat.Fun) X) → k x_1 ⟶ l
hl : ∀ (x_1 : ToType (FC := TypeCat.Fun) X), a x_1 ≫ c x_1 = b
h₁ : ∀ (x_1 : X), (hom (FC := TypeCat.Fun) (f ≫ F.map b)).toFun x_1 = (hom (FC := TypeCat.Fun) (g ≫ F.map b)).toFun x_1
⊢ f ≫ F.map b = g ≫ F.map b

Tactic:
ext x