awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type u_1
I_1 : J_1 → Type u_2
inst_1 : Category.{v_1, u_1} J_1
inst_2 : (j : J_1) → Category.{?u.30679, u_2} (I_1 j)
D_1 : Functor.{v_1, v, u_1, u} J_1 C
P_1 : (j : J_1) → ColimitPresentation.{?u.30679, u_2, v, u} (I_1 j) (D_1.obj j)
J : Type w
I : J → Type w
inst_3 : SmallCategory J
inst_4 : (j : J) → SmallCategory (I j)
D : Functor.{w, v, w, u} J C
P : (j : J) → ColimitPresentation.{w, w, v, u} (I j) (D.obj j)
inst_5 : IsFiltered J
inst_6 : ∀ (j : J), IsFiltered.{w, w} (I j)
inst_7 : ∀ (j : J) (i : I j), IsFinitelyPresentable.{w, v, u} ((P j).diag.obj i)
k l : Total (I := I) P
f g : k ⟶ l
a : J := IsFiltered.coeq (f.base (I := I)) (g.base (I := I))
a' : I (IsFiltered.coeq (f.base (I := I)) (g.base (I := I)))
u :
  Total.mk (I := I) P (l.fst (β := fun (j : J) ↦ I j)) (l.snd (β := fun (j : J) ↦ I j)) ⟶
    Total.mk (I := I) P (IsFiltered.coeq (f.base (I := I)) (g.base (I := I))) a'
hu : u.base (I := I) = IsFiltered.coeqHom (f.base (I := I)) (g.base (I := I))
this :
  (f.hom (I := I) ≫ u.hom (I := I)) ≫
      NatTrans.app
        (ι
          (P
            ((Total.mk (I := I) P (IsFiltered.coeq (f.base (I := I)) (g.base (I := I))) a').fst (β := fun (j : J) ↦
              I j))))
        ((Total.mk (I := I) P (IsFiltered.coeq (f.base (I := I)) (g.base (I := I))) a').snd (β := fun (j : J) ↦ I j)) =
    (g.hom (I := I) ≫ u.hom (I := I)) ≫
      NatTrans.app
        (ι
          (P
            ((Total.mk (I := I) P (IsFiltered.coeq (f.base (I := I)) (g.base (I := I))) a').fst (β := fun (j : J) ↦
              I j))))
        ((Total.mk (I := I) P (IsFiltered.coeq (f.base (I := I)) (g.base (I := I))) a').snd (β := fun (j : J) ↦ I j))
j : I ((Total.mk (I := I) P (IsFiltered.coeq (f.base (I := I)) (g.base (I := I))) a').fst (β := fun (j : J) ↦ I j))
p q : a' ⟶ j
hpq :
  f.hom (I := I) ≫
      u.hom (I := I) ≫
        Functor.map
          (diag
            (P
              ((Total.mk (I := I) P (IsFiltered.coeq (f.base (I := I)) (g.base (I := I))) a').fst (β := fun (j : J) ↦
                I j))))
          p =
    (g.hom (I := I) ≫ u.hom (I := I)) ≫
      Functor.map
        (diag
          (P
            ((Total.mk (I := I) P (IsFiltered.coeq (f.base (I := I)) (g.base (I := I))) a').fst (β := fun (j : J) ↦
              I j))))
        q
⊢ Eq (α :=
    Functor.obj (diag (P (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)) ⟶
      (P a).diag.obj (IsFiltered.coeq p q))
    (g.hom (I := I) ≫
      u.hom (I := I) ≫
        Functor.map (diag (P (IsFiltered.coeq (f.base (I := I)) (g.base (I := I))))) q ≫
          Functor.map (diag (P (IsFiltered.coeq (f.base (I := I)) (g.base (I := I))))) (IsFiltered.coeqHom p q))
    (g.hom (I := I) ≫
      u.hom (I := I) ≫
        Functor.map (diag (P (IsFiltered.coeq (f.base (I := I)) (g.base (I := I))))) p ≫
          Functor.map (diag (P (IsFiltered.coeq (f.base (I := I)) (g.base (I := I))))) (IsFiltered.coeqHom p q))

Tactic:
simp [← Functor.map_comp, ← IsFiltered.coeq_condition]

Premises used: CategoryTheory.IsFiltered.coeq_condition, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type u_1
I_1 : J_1 → Type u_2
inst_1 : Category.{v_1, u_1} J_1
inst_2 : (j : J_1) → Category.{?u.52389, u_2} (I_1 j)
D_1 : Functor.{v_1, v, u_1, u} J_1 C
P_1 : (j : J_1) → ColimitPresentation.{?u.52389, u_2, v, u} (I_1 j) (D_1.obj j)
J : Type w
I : J → Type w
inst_3 : SmallCategory J
inst_4 : (j : J) → SmallCategory (I j)
D : Functor.{w, v, w, u} J C
P_2 : (j : J) → ColimitPresentation.{w, w, v, u} (I j) (D.obj j)
X : C
P : ColimitPresentation.{w, w, v, u} J X
Q : (j : J) → ColimitPresentation.{w, w, v, u} (I j) (P.diag.obj j)
inst_5 : ∀ (j : J), IsFiltered.{w, w} (I j)
inst_6 : ∀ (j : J) (i : I j), IsFinitelyPresentable.{w, v, u} ((Q j).diag.obj i)
k l : Total (I := I) Q
u : k ⟶ l
⊢ {
            obj := fun (k : Total (I := I) Q) ↦
              Functor.obj (diag (Q (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)),
            map := fun {k l : Total (I := I) Q} (f : k ⟶ l) ↦ f.hom (I := I), map_id := ⋯, map_comp := ⋯ :
            Total (I := I) Q ⥤ C }.map
        u ≫
      NatTrans.app (ι (Q (l.fst (β := fun (j : J) ↦ I j)))) (l.snd (β := fun (j : J) ↦ I j)) ≫
        P.ι.app (l.fst (β := fun (j : J) ↦ I j)) =
    (NatTrans.app (ι (Q (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)) ≫
        P.ι.app (k.fst (β := fun (j : J) ↦ I j))) ≫
      Functor.map (Functor.obj (Functor.const (Total (I := I) Q)) X) u

Tactic:
simp [← u.w_assoc]

Premises used: CategoryTheory.Limits.ColimitPresentation.Total.Hom.w_assoc
-- Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type u_1
I_1 : J_1 → Type u_2
inst_1 : Category.{v_1, u_1} J_1
inst_2 : (j : J_1) → Category.{?u.52389, u_2} (I_1 j)
D_1 : Functor.{v_1, v, u_1, u} J_1 C
P_1 : (j : J_1) → ColimitPresentation.{?u.52389, u_2, v, u} (I_1 j) (D_1.obj j)
J : Type w
I : J → Type w
inst_3 : SmallCategory J
inst_4 : (j : J) → SmallCategory (I j)
D : Functor.{w, v, w, u} J C
P_2 : (j : J) → ColimitPresentation.{w, w, v, u} (I j) (D.obj j)
X : C
P : ColimitPresentation.{w, w, v, u} J X
Q : (j : J) → ColimitPresentation.{w, w, v, u} (I j) (P.diag.obj j)
inst_5 : ∀ (j : J), IsFiltered.{w, w} (I j)
inst_6 : ∀ (j : J) (i : I j), IsFinitelyPresentable.{w, v, u} ((Q j).diag.obj i)
c :
  Cocone
    {
      obj := fun (k : Total (I := I) Q) ↦
        Functor.obj (diag (Q (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)),
      map := fun {k l : Total (I := I) Q} (f : k ⟶ l) ↦ f.hom (I := I), map_id := ⋯, map_comp := ⋯ :
      Total (I := I) Q ⥤ C }
j : J
i i' : I j
u : i ⟶ i'
v : Total.mk (I := I) Q j i ⟶ Total.mk (I := I) Q j i' :=
  Total.Hom.mk (I := I) (𝟙 ((Total.mk (I := I) Q j i).fst (β := fun (j : J) ↦ I j)))
    (Functor.map (diag (Q ((Total.mk (I := I) Q j i).fst (β := fun (j : J) ↦ I j)))) u) ⋯
⊢ Eq (α := (Q j).diag.obj i ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (I j)) c.pt) i')
    ((Q j).diag.map u ≫ c.ι.app (Sigma.mk (β := fun (j : J) ↦ I j) j i'))
    (c.ι.app (Sigma.mk (β := fun (j : J) ↦ I j) j i) ≫ Functor.map (Functor.obj (Functor.const (I j)) c.pt) u)

Tactic:
simpa using c.ι.naturality v

Premises used: CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type u_1
I_1 : J_1 → Type u_2
inst_1 : Category.{v_1, u_1} J_1
inst_2 : (j : J_1) → Category.{?u.52389, u_2} (I_1 j)
D_1 : Functor.{v_1, v, u_1, u} J_1 C
P_1 : (j : J_1) → ColimitPresentation.{?u.52389, u_2, v, u} (I_1 j) (D_1.obj j)
J : Type w
I : J → Type w
inst_3 : SmallCategory J
inst_4 : (j : J) → SmallCategory (I j)
D : Functor.{w, v, w, u} J C
P_2 : (j : J) → ColimitPresentation.{w, w, v, u} (I j) (D.obj j)
X : C
P : ColimitPresentation.{w, w, v, u} J X
Q : (j : J) → ColimitPresentation.{w, w, v, u} (I j) (P.diag.obj j)
inst_5 : ∀ (j : J), IsFiltered.{w, w} (I j)
inst_6 : ∀ (j : J) (i : I j), IsFinitelyPresentable.{w, v, u} ((Q j).diag.obj i)
c :
  Cocone
    {
      obj := fun (k : Total (I := I) Q) ↦
        Functor.obj (diag (Q (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)),
      map := fun {k l : Total (I := I) Q} (f : k ⟶ l) ↦ f.hom (I := I), map_id := ⋯, map_comp := ⋯ :
      Total (I := I) Q ⥤ C }
j j' : J
u : j ⟶ j'
⊢ Eq (α := P.diag.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const J) c.pt) j')
    (P.diag.map u ≫
        (Q j').isColimit.desc
          { pt := c.pt,
            ι := { app := fun (i : I j') ↦ c.ι.app (Sigma.mk (β := fun (j : J) ↦ I j) j' i), naturality := ⋯ } } :
      P.diag.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const J) c.pt) j')
    (CategoryStruct.comp (Y := Functor.obj.{w, v, w, u} (Functor.obj (Functor.const J) c.pt) j)
        ((Q j).isColimit.desc
            { pt := c.pt,
              ι := { app := fun (i : I j) ↦ c.ι.app (Sigma.mk (β := fun (j : J) ↦ I j) j i), naturality := ⋯ } } :
          { pt := P.diag.obj j, ι := (Q j).ι : Cocone (Q j).diag }.pt ⟶
            Cocone.pt.{w, v, w, u} (J := I j) (F := (Q j).diag)
              { pt := c.pt,
                ι := { app := fun (i : I j) ↦ c.ι.app (Sigma.mk (β := fun (j : J) ↦ I j) j i), naturality := ⋯ } })
        (Functor.map (Functor.obj (Functor.const J) c.pt) u) :
      P.diag.obj j ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const J) c.pt) j')

Tactic:
(Q j).isColimit.hom_ext fun i ↦ ?_

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.Limits.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type u_1
I_1 : J_1 → Type u_2
inst_1 : Category.{v_1, u_1} J_1
inst_2 : (j : J_1) → Category.{?u.52389, u_2} (I_1 j)
D_1 : Functor.{v_1, v, u_1, u} J_1 C
P_1 : (j : J_1) → ColimitPresentation.{?u.52389, u_2, v, u} (I_1 j) (D_1.obj j)
J : Type w
I : J → Type w
inst_3 : SmallCategory J
inst_4 : (j : J) → SmallCategory (I j)
D : Functor.{w, v, w, u} J C
P_2 : (j : J) → ColimitPresentation.{w, w, v, u} (I j) (D.obj j)
X : C
P : ColimitPresentation.{w, w, v, u} J X
Q : (j : J) → ColimitPresentation.{w, w, v, u} (I j) (P.diag.obj j)
inst_5 : ∀ (j : J), IsFiltered.{w, w} (I j)
inst_6 : ∀ (j : J) (i : I j), IsFinitelyPresentable.{w, v, u} ((Q j).diag.obj i)
c :
  Cocone
    {
      obj := fun (k : Total (I := I) Q) ↦
        Functor.obj (diag (Q (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)),
      map := fun {k l : Total (I := I) Q} (f : k ⟶ l) ↦ f.hom (I := I), map_id := ⋯, map_comp := ⋯ :
      Total (I := I) Q ⥤ C }
j j' : J
u : j ⟶ j'
i : I j
obtain :
  ∀ (i' : I j') (hom : Total.mk (I := I) Q j i ⟶ Total.mk (I := I) Q j' i'),
    Eq (α := (Q j).diag.obj i ⟶ c.pt)
      ((Q j).ι.app i ≫
          P.diag.map (hom.base (I := I)) ≫
            (Q j').isColimit.desc
              { pt := c.pt,
                ι := { app := fun (i : I j') ↦ c.ι.app (Sigma.mk (β := fun (j : J) ↦ I j) j' i), naturality := ⋯ } } :
        (Q j).diag.obj i ⟶ c.pt)
      (c.ι.app (Sigma.mk (β := fun (j : J) ↦ I j) j i) :
        {
                obj := fun (k : Total (I := I) Q) ↦
                  Functor.obj (diag (Q (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)),
                map := fun {k l : Total (I := I) Q} (f : k ⟶ l) ↦ f.hom (I := I), map_id := ⋯, map_comp := ⋯ :
                Total (I := I) Q ⥤ C }.obj
            (Sigma.mk (β := fun (j : J) ↦ I j) j i) ⟶
          Functor.obj (Functor.obj (Functor.const (Total (I := I) Q)) c.pt) (Sigma.mk (β := fun (j : J) ↦ I j) j i))
⊢ Eq (α := (Q j).diag.obj i ⟶ c.pt)
    ((Q j).ι.app i ≫
        P.diag.map u ≫
          (Q j').isColimit.desc
            { pt := c.pt,
              ι := { app := fun (i : I j') ↦ c.ι.app (Sigma.mk (β := fun (j : J) ↦ I j) j' i), naturality := ⋯ } } :
      (Q j).diag.obj i ⟶ c.pt)
    (c.ι.app (Sigma.mk (β := fun (j : J) ↦ I j) j i) :
      {
              obj := fun (k : Total (I := I) Q) ↦
                Functor.obj (diag (Q (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)),
              map := fun {k l : Total (I := I) Q} (f : k ⟶ l) ↦ f.hom (I := I), map_id := ⋯, map_comp := ⋯ :
              Total (I := I) Q ⥤ C }.obj
          (Sigma.mk (β := fun (j : J) ↦ I j) j i) ⟶
        Functor.obj (Functor.obj (Functor.const (Total (I := I) Q)) c.pt) (Sigma.mk (β := fun (j : J) ↦ I j) j i))

Tactic:
obtain ⟨i', hom, rfl⟩ := Total.exists_hom_of_hom (P := Q) i u

Premises used: CategoryTheory.Limits.ColimitPresentation.Total.exists_hom_of_hom, rfl
-- Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type u_1
I_1 : J_1 → Type u_2
inst_1 : Category.{v_1, u_1} J_1
inst_2 : (j : J_1) → Category.{?u.52389, u_2} (I_1 j)
D_1 : Functor.{v_1, v, u_1, u} J_1 C
P_1 : (j : J_1) → ColimitPresentation.{?u.52389, u_2, v, u} (I_1 j) (D_1.obj j)
J : Type w
I : J → Type w
inst_3 : SmallCategory J
inst_4 : (j : J) → SmallCategory (I j)
D : Functor.{w, v, w, u} J C
P_2 : (j : J) → ColimitPresentation.{w, w, v, u} (I j) (D.obj j)
X : C
P : ColimitPresentation.{w, w, v, u} J X
Q : (j : J) → ColimitPresentation.{w, w, v, u} (I j) (P.diag.obj j)
inst_5 : ∀ (j : J), IsFiltered.{w, w} (I j)
inst_6 : ∀ (j : J) (i : I j), IsFinitelyPresentable.{w, v, u} ((Q j).diag.obj i)
c :
  Cocone
    {
      obj := fun (k : Total (I := I) Q) ↦
        Functor.obj (diag (Q (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)),
      map := fun {k l : Total (I := I) Q} (f : k ⟶ l) ↦ f.hom (I := I), map_id := ⋯, map_comp := ⋯ :
      Total (I := I) Q ⥤ C }
j j' : J
i : I j
i' : I j'
hom : Total.mk (I := I) Q j i ⟶ Total.mk (I := I) Q j' i'
rw :
  Eq (α := (Q j).diag.obj i ⟶ c.pt)
    (hom.hom (I := I) ≫
        NatTrans.app
          (Cocone.ι
            { pt := c.pt,
              ι := { app := fun (i : I j') ↦ c.ι.app (Sigma.mk (β := fun (j : J) ↦ I j) j' i), naturality := ⋯ } })
          i' :
      (Q j).diag.obj i ⟶ c.pt)
    (c.ι.app (Sigma.mk (β := fun (j : J) ↦ I j) j i) :
      {
              obj := fun (k : Total (I := I) Q) ↦
                Functor.obj (diag (Q (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)),
              map := fun {k l : Total (I := I) Q} (f : k ⟶ l) ↦ f.hom (I := I), map_id := ⋯, map_comp := ⋯ :
              Total (I := I) Q ⥤ C }.obj
          (Sigma.mk (β := fun (j : J) ↦ I j) j i) ⟶
        Functor.obj (Functor.obj (Functor.const (Total (I := I) Q)) c.pt) (Sigma.mk (β := fun (j : J) ↦ I j) j i))
⊢ Eq (α := (Q j).diag.obj i ⟶ c.pt)
    ((Q j).ι.app i ≫
        P.diag.map (hom.base (I := I)) ≫
          (Q j').isColimit.desc
            { pt := c.pt,
              ι := { app := fun (i : I j') ↦ c.ι.app (Sigma.mk (β := fun (j : J) ↦ I j) j' i), naturality := ⋯ } } :
      (Q j).diag.obj i ⟶ c.pt)
    (c.ι.app (Sigma.mk (β := fun (j : J) ↦ I j) j i) :
      {
              obj := fun (k : Total (I := I) Q) ↦
                Functor.obj (diag (Q (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)),
              map := fun {k l : Total (I := I) Q} (f : k ⟶ l) ↦ f.hom (I := I), map_id := ⋯, map_comp := ⋯ :
              Total (I := I) Q ⥤ C }.obj
          (Sigma.mk (β := fun (j : J) ↦ I j) j i) ⟶
        Functor.obj (Functor.obj (Functor.const (Total (I := I) Q)) c.pt) (Sigma.mk (β := fun (j : J) ↦ I j) j i))

Tactic:
rw [reassoc_of% hom.w, (Q j').isColimit.fac]

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.ColimitPresentation.Total.Hom.w
-- Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type u_1
I_1 : J_1 → Type u_2
inst_1 : Category.{v_1, u_1} J_1
inst_2 : (j : J_1) → Category.{?u.52389, u_2} (I_1 j)
D_1 : Functor.{v_1, v, u_1, u} J_1 C
P_1 : (j : J_1) → ColimitPresentation.{?u.52389, u_2, v, u} (I_1 j) (D_1.obj j)
J : Type w
I : J → Type w
inst_3 : SmallCategory J
inst_4 : (j : J) → SmallCategory (I j)
D : Functor.{w, v, w, u} J C
P_2 : (j : J) → ColimitPresentation.{w, w, v, u} (I j) (D.obj j)
X : C
P : ColimitPresentation.{w, w, v, u} J X
Q : (j : J) → ColimitPresentation.{w, w, v, u} (I j) (P.diag.obj j)
inst_5 : ∀ (j : J), IsFiltered.{w, w} (I j)
inst_6 : ∀ (j : J) (i : I j), IsFinitelyPresentable.{w, v, u} ((Q j).diag.obj i)
c :
  Cocone
    {
      obj := fun (k : Total (I := I) Q) ↦
        Functor.obj (diag (Q (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)),
      map := fun {k l : Total (I := I) Q} (f : k ⟶ l) ↦ f.hom (I := I), map_id := ⋯, map_comp := ⋯ :
      Total (I := I) Q ⥤ C }
j j' : J
i : I j
i' : I j'
hom : Total.mk (I := I) Q j i ⟶ Total.mk (I := I) Q j' i'
⊢ Eq (α := (Q j).diag.obj i ⟶ c.pt)
    (hom.hom (I := I) ≫
        NatTrans.app
          (Cocone.ι
            { pt := c.pt,
              ι := { app := fun (i : I j') ↦ c.ι.app (Sigma.mk (β := fun (j : J) ↦ I j) j' i), naturality := ⋯ } })
          i' :
      (Q j).diag.obj i ⟶ c.pt)
    (c.ι.app (Sigma.mk (β := fun (j : J) ↦ I j) j i) :
      {
              obj := fun (k : Total (I := I) Q) ↦
                Functor.obj (diag (Q (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)),
              map := fun {k l : Total (I := I) Q} (f : k ⟶ l) ↦ f.hom (I := I), map_id := ⋯, map_comp := ⋯ :
              Total (I := I) Q ⥤ C }.obj
          (Sigma.mk (β := fun (j : J) ↦ I j) j i) ⟶
        Functor.obj (Functor.obj (Functor.const (Total (I := I) Q)) c.pt) (Sigma.mk (β := fun (j : J) ↦ I j) j i))

Tactic:
simpa using c.ι.naturality hom

Premises used: CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type u_1
I_1 : J_1 → Type u_2
inst_1 : Category.{v_1, u_1} J_1
inst_2 : (j : J_1) → Category.{?u.52389, u_2} (I_1 j)
D_1 : Functor.{v_1, v, u_1, u} J_1 C
P_1 : (j : J_1) → ColimitPresentation.{?u.52389, u_2, v, u} (I_1 j) (D_1.obj j)
J : Type w
I : J → Type w
inst_3 : SmallCategory J
inst_4 : (j : J) → SmallCategory (I j)
D : Functor.{w, v, w, u} J C
P_2 : (j : J) → ColimitPresentation.{w, w, v, u} (I j) (D.obj j)
X : C
P : ColimitPresentation.{w, w, v, u} J X
Q : (j : J) → ColimitPresentation.{w, w, v, u} (I j) (P.diag.obj j)
inst_5 : ∀ (j : J), IsFiltered.{w, w} (I j)
inst_6 : ∀ (j : J) (i : I j), IsFinitelyPresentable.{w, v, u} ((Q j).diag.obj i)
c :
  Cocone
    {
      obj := fun (k : Total (I := I) Q) ↦
        Functor.obj (diag (Q (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)),
      map := fun {k l : Total (I := I) Q} (f : k ⟶ l) ↦ f.hom (I := I), map_id := ⋯, map_comp := ⋯ :
      Total (I := I) Q ⥤ C }
m :
  Cocone.pt (J := Total (I := I) Q) (F :=
      {
        obj := fun (k : Total (I := I) Q) ↦
          Functor.obj (diag (Q (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)),
        map := fun {k l : Total (I := I) Q} (f : k ⟶ l) ↦ f.hom (I := I), map_id := ⋯, map_comp := ⋯ :
        Total (I := I) Q ⥤ C })
      { pt := X,
        ι :=
          {
            app := fun (k : Total (I := I) Q) ↦
              NatTrans.app (ι (Q (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)) ≫
                P.ι.app (k.fst (β := fun (j : J) ↦ I j)),
            naturality := ⋯ :
            NatTrans
              {
                obj := fun (k : Total (I := I) Q) ↦
                  Functor.obj (diag (Q (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)),
                map := fun {k l : Total (I := I) Q} (f : k ⟶ l) ↦ f.hom (I := I), map_id := ⋯, map_comp := ⋯ :
                Total (I := I) Q ⥤ C }
              (Functor.obj (Functor.const (Total (I := I) Q)) X) } :
        Cocone
          {
            obj := fun (k : Total (I := I) Q) ↦
              Functor.obj (diag (Q (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)),
            map := fun {k l : Total (I := I) Q} (f : k ⟶ l) ↦ f.hom (I := I), map_id := ⋯, map_comp := ⋯ :
            Total (I := I) Q ⥤ C } } ⟶
    c.pt
hm :
  ∀ (j : Total (I := I) Q),
    NatTrans.app
          (Cocone.ι
            { pt := X,
              ι :=
                {
                  app := fun (k : Total (I := I) Q) ↦
                    NatTrans.app (ι (Q (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)) ≫
                      P.ι.app (k.fst (β := fun (j : J) ↦ I j)),
                  naturality := ⋯ } })
          j ≫
        m =
      c.ι.app j
j : J
⊢ P.ι.app j ≫ m =
    (Q j).isColimit.desc
      { pt := c.pt, ι := { app := fun (i : I j) ↦ c.ι.app (Sigma.mk (β := fun (j : J) ↦ I j) j i), naturality := ⋯ } }

Tactic:
(Q j).isColimit.hom_ext fun i ↦ ?_

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.Limits.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Presentable.Dense
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalAccessibleCategory.{w, v, u} C κ
obtain :
  ∀ (P : ObjectProperty.{v, u} C),
    ObjectProperty.EssentiallySmall.{w, v, u} P →
      ∀ (hP : P.IsCardinalFilteredGenerator κ),
        ObjectProperty.IsCardinalFilteredGenerator.{w, v, u} (isCardinalPresentable C κ) κ
⊢ ObjectProperty.IsCardinalFilteredGenerator.{w, v, u} (isCardinalPresentable C κ) κ

Tactic:
obtain ⟨P, _, hP⟩ := HasCardinalFilteredGenerator.exists_generator C κ

Premises used: CategoryTheory.HasCardinalFilteredGenerator.exists_generator
-- Module: Mathlib.CategoryTheory.Presentable.Dense
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalAccessibleCategory.{w, v, u} C κ
P : ObjectProperty.{v, u} C
w : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
⊢ ObjectProperty.IsCardinalFilteredGenerator.{w, v, u} (isCardinalPresentable C κ) κ

Tactic:
hP.of_le_isoClosure ?_ le_rfl

Premises used: le_rfl, CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.of_le_isoClosure
-- Module: Mathlib.CategoryTheory.Presentable.Dense
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalAccessibleCategory.{w, v, u} C κ
P : ObjectProperty.{v, u} C
w : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
refine : P ≤ ObjectProperty.isoClosure (isCardinalPresentable C κ)
⊢ ObjectProperty.IsCardinalFilteredGenerator.{w, v, u} (isCardinalPresentable C κ) κ

Tactic:
refine hP.of_le_isoClosure ?_ le_rfl

Premises used: le_rfl, CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.of_le_isoClosure
-- Module: Mathlib.CategoryTheory.Presentable.Dense
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalAccessibleCategory.{w, v, u} C κ
P : ObjectProperty.{v, u} C
w : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
rw : P ≤ isCardinalPresentable C κ
⊢ P ≤ ObjectProperty.isoClosure (isCardinalPresentable C κ)

Tactic:
rw [ObjectProperty.isoClosure_eq_self]

Premises used: CategoryTheory.ObjectProperty.isoClosure_eq_self
-- Module: Mathlib.CategoryTheory.Presentable.Dense
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalAccessibleCategory.{w, v, u} C κ
P : ObjectProperty.{v, u} C
w : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
⊢ P ≤ isCardinalPresentable C κ

Tactic:
hP.le_isCardinalPresentable

Premises used: CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.le_isCardinalPresentable
-- Module: Mathlib.CategoryTheory.Presentable.Dense
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalAccessibleCategory.{w, v, u} C κ
P : ObjectProperty.{v, u} C
w : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
⊢ P ≤ isCardinalPresentable C κ

Tactic:
exact hP.le_isCardinalPresentable

Premises used: CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.le_isCardinalPresentable
-- Module: Mathlib.CategoryTheory.Presentable.Dense
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
J : Type u'
inst_2 : Category.{v', u'} J
inst_3 : EssentiallySmall.{w, v', u'} J
inst_4 : IsCardinalFiltered.{w, v', u'} J κ
X : C
p : ObjectProperty.ColimitOfShape.{v', u', v, u} (isCardinalPresentable C κ) J X
⊢ IsFiltered.{v', u'} J

Tactic:
have := isFiltered_of_isCardinalFiltered J κ