awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasCardinalFilteredGenerator.{w, v, u} C κ
obtain :
  ∀ (P : ObjectProperty.{v, u} C),
    ObjectProperty.EssentiallySmall.{w, v, u} P →
      ∀ (hP : P.IsCardinalFilteredGenerator κ),
        ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P), P.IsCardinalFilteredGenerator κ
⊢ ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P), P.IsCardinalFilteredGenerator κ

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

Premises used: CategoryTheory.HasCardinalFilteredGenerator.exists_generator
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasCardinalFilteredGenerator.{w, v, u} C κ
P : ObjectProperty.{v, u} C
w : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
obtain :
  ∀ (Q : ObjectProperty.{v, u} C),
    ObjectProperty.Small.{w, v, u} Q →
      ∀ (h₁ : Q ≤ P) (h₂ : P ≤ Q.isoClosure),
        ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P), P.IsCardinalFilteredGenerator κ
⊢ ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P), P.IsCardinalFilteredGenerator κ

Tactic:
obtain ⟨Q, _, h₁, h₂⟩ := ObjectProperty.EssentiallySmall.exists_small_le P

Premises used: CategoryTheory.ObjectProperty.EssentiallySmall.exists_small_le
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasCardinalFilteredGenerator.{w, v, u} C κ
P : ObjectProperty.{v, u} C
w : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
Q : ObjectProperty.{v, u} C
w_1 : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
⊢ ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P), P.IsCardinalFilteredGenerator κ

Tactic:
⟨Q, inferInstance, hP.of_le_isoClosure h₂ (h₁.trans hP.le_isCardinalPresentable)⟩

Premises used: CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.of_le_isoClosure, CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.le_isCardinalPresentable, inferInstance, Exists.intro, LE.le.trans
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasCardinalFilteredGenerator.{w, v, u} C κ
P : ObjectProperty.{v, u} C
w : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
Q : ObjectProperty.{v, u} C
w_1 : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
⊢ ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P), P.IsCardinalFilteredGenerator κ

Tactic:
exact ⟨Q, inferInstance, hP.of_le_isoClosure h₂ (h₁.trans hP.le_isCardinalPresentable)⟩
-- Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : HasCardinalFilteredGenerator.{w, v, u} C κ
obtain :
  ∀ (P : ObjectProperty.{v, u} C),
    ObjectProperty.EssentiallySmall.{w, v, u} P →
      ∀ (hP : P.IsCardinalFilteredGenerator κ), ObjectProperty.EssentiallySmall.{w, v, u} (isCardinalPresentable C κ)
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (isCardinalPresentable C κ)

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

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

Tactic:
hP.essentiallySmall_isPresentable

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

Tactic:
exact hP.essentiallySmall_isPresentable

Premises used: CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.essentiallySmall_isPresentable
-- Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
I : J → Type u_2
inst_1 : Category.{v_1, u_1} J
inst_2 : (j : J) → Category.{u_3, u_2} (I j)
D : Functor.{v_1, v, u_1, u} J C
P : (j : J) → ColimitPresentation.{u_3, u_2, v, u} (I j) (D.obj j)
k l m : Total (I := I) P
f : k.Hom (I := I) l
g : l.Hom (I := I) m
simp :
  NatTrans.app (ι (P (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)) ≫
      D.map (f.base (I := I)) ≫ D.map (g.base (I := I)) =
    f.hom (I := I) ≫
      g.hom (I := I) ≫ NatTrans.app (ι (P (m.fst (β := fun (j : J) ↦ I j)))) (m.snd (β := fun (j : J) ↦ I j))
⊢ NatTrans.app (ι (P (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)) ≫
      D.map (f.base (I := I) ≫ g.base (I := I)) =
    (f.hom (I := I) ≫ g.hom (I := I)) ≫
      NatTrans.app (ι (P (m.fst (β := fun (j : J) ↦ I j)))) (m.snd (β := fun (j : J) ↦ I j))

Tactic:
simp only [Functor.const_obj_obj, Functor.map_comp, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.const_obj_obj
-- Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
I : J → Type u_2
inst_1 : Category.{v_1, u_1} J
inst_2 : (j : J) → Category.{u_3, u_2} (I j)
D : Functor.{v_1, v, u_1, u} J C
P : (j : J) → ColimitPresentation.{u_3, u_2, v, u} (I j) (D.obj j)
k l m : Total (I := I) P
f : k.Hom (I := I) l
g : l.Hom (I := I) m
rw :
  f.hom (I := I) ≫
      NatTrans.app (ι (P (l.fst (β := fun (j : J) ↦ I j)))) (l.snd (β := fun (j : J) ↦ I j)) ≫ D.map (g.base (I := I)) =
    f.hom (I := I) ≫
      g.hom (I := I) ≫ NatTrans.app (ι (P (m.fst (β := fun (j : J) ↦ I j)))) (m.snd (β := fun (j : J) ↦ I j))
rw₁ rw₂ :
  f.hom (I := I) ≫
      g.hom (I := I) ≫ NatTrans.app (ι (P (m.fst (β := fun (j : J) ↦ I j)))) (m.snd (β := fun (j : J) ↦ I j)) =
    f.hom (I := I) ≫
      g.hom (I := I) ≫ NatTrans.app (ι (P (m.fst (β := fun (j : J) ↦ I j)))) (m.snd (β := fun (j : J) ↦ I j))
⊢ NatTrans.app (ι (P (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)) ≫
      D.map (f.base (I := I)) ≫ D.map (g.base (I := I)) =
    f.hom (I := I) ≫
      g.hom (I := I) ≫ NatTrans.app (ι (P (m.fst (β := fun (j : J) ↦ I j)))) (m.snd (β := fun (j : J) ↦ I j))

Tactic:
rw [f.w_assoc, g.w]

Premises used: CategoryTheory.Limits.ColimitPresentation.Total.Hom.w, CategoryTheory.Limits.ColimitPresentation.Total.Hom.w_assoc
-- Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u_1
I : J → Type u_2
inst_1 : Category.{v_1, u_1} J
inst_2 : (j : J) → Category.{u_3, u_2} (I j)
D : Functor.{v_1, v, u_1, u} J C
P : (j : J) → ColimitPresentation.{u_3, u_2, v, u} (I j) (D.obj j)
inst_3 : LocallySmall.{w, v, u} C
inst_4 : LocallySmall.{w, v_1, u_1} J
k l : Total (I := I) P
f : (x : k ⟶ l) →
  Prod.{v_1, v} (k.fst (β := fun (j : J) ↦ I j) ⟶ l.fst (β := fun (j : J) ↦ I j))
    (Functor.obj (diag (P (k.fst (β := fun (j : J) ↦ I j)))) (k.snd (β := fun (j : J) ↦ I j)) ⟶
      Functor.obj (diag (P (l.fst (β := fun (j : J) ↦ I j)))) (l.snd (β := fun (j : J) ↦ I j))) :=
  fun (x : k ⟶ l) ↦ (x.base (I := I), x.hom (I := I))
⊢ Function.Injective f

Tactic:
grind [Function.Injective, Total.Hom.ext]

Premises used: Function.Injective, CategoryTheory.Limits.ColimitPresentation.Total.Hom.ext
-- Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
I : J → Type w
inst_1 : SmallCategory J
inst_2 : (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)
j j' : J
i : I j
u : j ⟶ j'
inst_3 : IsFiltered.{w, w} (I j')
inst_4 : IsFinitelyPresentable.{w, v, u} ((P j).diag.obj i)
obtain :
  ∀ (i' : I j') (q : (P j).diag.obj i ⟶ (P j').diag.obj i')
    (hq : q ≫ { pt := D.obj j', ι := (P j').ι : Cocone (P j').diag }.ι.app i' = (P j).ι.app i ≫ D.map u),
    ∃ (i' : I j') (f : mk (I := I) P j i ⟶ mk (I := I) P j' i'), f.base (I := I) = u
⊢ ∃ (i' : I j') (f : mk (I := I) P j i ⟶ mk (I := I) P j' i'), f.base (I := I) = u

Tactic:
obtain ⟨i', q, hq⟩ := IsFinitelyPresentable.exists_hom_of_isColimit (P j').isColimit
    ((P j).ι.app i ≫ D.map u)

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.Limits.ColimitPresentation.ι, CategoryTheory.Functor.map, CategoryTheory.IsFinitelyPresentable.exists_hom_of_isColimit, CategoryTheory.CategoryStruct.comp, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
I : J → Type w
inst_1 : SmallCategory J
inst_2 : (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)
j j' : J
i : I j
u : j ⟶ j'
inst_3 : IsFiltered.{w, w} (I j')
inst_4 : IsFinitelyPresentable.{w, v, u} ((P j).diag.obj i)
i' : I j'
q : (P j).diag.obj i ⟶ (P j').diag.obj i'
hq : q ≫ { pt := D.obj j', ι := (P j').ι : Cocone (P j').diag }.ι.app i' = (P j).ι.app i ≫ D.map u
⊢ NatTrans.app (ι (P ((mk (I := I) P j i).fst (β := fun (j : J) ↦ I j))))
        ((mk (I := I) P j i).snd (β := fun (j : J) ↦ I j)) ≫
      D.map u =
    q ≫
      NatTrans.app (ι (P ((mk (I := I) P j' i').fst (β := fun (j : J) ↦ I j))))
        ((mk (I := I) P j' i').snd (β := fun (j : J) ↦ I j))

Tactic:
simp [← hq]
-- Module: Mathlib.CategoryTheory.Presentable.ColimitPresentation
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
I : J → Type w
inst_1 : SmallCategory J
inst_2 : (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)
j j' : J
i : I j
u : j ⟶ j'
inst_3 : IsFiltered.{w, w} (I j')
inst_4 : IsFinitelyPresentable.{w, v, u} ((P j).diag.obj i)
i' : I j'
q : (P j).diag.obj i ⟶ (P j').diag.obj i'
hq : q ≫ { pt := D.obj j', ι := (P j').ι : Cocone (P j').diag }.ι.app i' = (P j).ι.app i ≫ D.map u
w : I j'
w₁ : mk (I := I) P j i ⟶ mk (I := I) P j' i'
h : Hom.base (I := I) (Hom.mk (I := I) u q ⋯) = u
⊢ ∃ (i' : I j') (f : mk (I := I) P j i ⟶ mk (I := I) P j' i'), f.base (I := I) = u

Tactic:
use i', { base := u, hom := q, w := by simp [← hq] }
-- 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.29355, u_2} (I_1 j)
D_1 : Functor.{v_1, v, u_1, u} J_1 C
P_1 : (j : J_1) → ColimitPresentation.{?u.29355, 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)
⊢ Nonempty J

Tactic:
IsFiltered.nonempty

Premises used: CategoryTheory.IsFiltered.nonempty
-- 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.29355, u_2} (I_1 j)
D_1 : Functor.{v_1, v, u_1, u} J_1 C
P_1 : (j : J_1) → ColimitPresentation.{?u.29355, 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)
obtain : ∀ (j : J), Nonempty.{w + 1} (Total (I := I) P)
⊢ Nonempty.{w + 1} (Total (I := I) P)

Tactic:
obtain ⟨j⟩ : Nonempty J := IsFiltered.nonempty

Premises used: CategoryTheory.IsFiltered.nonempty, Nonempty
-- 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.29355, u_2} (I_1 j)
D_1 : Functor.{v_1, v, u_1, u} J_1 C
P_1 : (j : J_1) → ColimitPresentation.{?u.29355, 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)
j : J
⊢ Nonempty.{w + 1} (I j)

Tactic:
IsFiltered.nonempty

Premises used: CategoryTheory.IsFiltered.nonempty
-- 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.29355, u_2} (I_1 j)
D_1 : Functor.{v_1, v, u_1, u} J_1 C
P_1 : (j : J_1) → ColimitPresentation.{?u.29355, 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)
j : J
obtain : ∀ (i : I j), Nonempty.{w + 1} (Total (I := I) P)
⊢ Nonempty.{w + 1} (Total (I := I) P)

Tactic:
obtain ⟨i⟩ : Nonempty (I j) := IsFiltered.nonempty

Premises used: CategoryTheory.IsFiltered.nonempty, Nonempty
-- 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.29355, u_2} (I_1 j)
D_1 : Functor.{v_1, v, u_1, u} J_1 C
P_1 : (j : J_1) → ColimitPresentation.{?u.29355, 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)
j : J
i : I j
⊢ Nonempty.{w + 1} (Total (I := I) P)

Tactic:
⟨⟨j, i⟩⟩

Premises used: Nonempty.intro, Sigma.mk
-- 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.29355, u_2} (I_1 j)
D_1 : Functor.{v_1, v, u_1, u} J_1 C
P_1 : (j : J_1) → ColimitPresentation.{?u.29355, 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)
j : J
i : I j
⊢ Nonempty.{w + 1} (Total (I := I) P)

Tactic:
exact ⟨⟨j, i⟩⟩
-- 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
a : J := IsFiltered.max (k.fst (β := fun (j : J) ↦ I j)) (l.fst (β := fun (j : J) ↦ I j))
obtain :
  ∀ (a' : I (IsFiltered.max (k.fst (β := fun (j : J) ↦ I j)) (l.fst (β := fun (j : J) ↦ I j))))
    (f :
      Total.mk (I := I) P (k.fst (β := fun (j : J) ↦ I j)) (k.snd (β := fun (j : J) ↦ I j)) ⟶
        Total.mk (I := I) P (IsFiltered.max (k.fst (β := fun (j : J) ↦ I j)) (l.fst (β := fun (j : J) ↦ I j))) a')
    (hf : f.base (I := I) = IsFiltered.leftToMax (k.fst (β := fun (j : J) ↦ I j)) (l.fst (β := fun (j : J) ↦ I j))),
    ∃ (Z : Total (I := I) P) (x : k ⟶ Z) (x : l ⟶ Z), True
⊢ ∃ (Z : Total (I := I) P) (x : k ⟶ Z) (x : l ⟶ Z), True

Tactic:
obtain ⟨a', f, hf⟩ := Total.exists_hom_of_hom (P := P) k.2 (IsFiltered.leftToMax k.1 l.1)

Premises used: CategoryTheory.Limits.ColimitPresentation.Total.exists_hom_of_hom, Sigma.fst, CategoryTheory.IsFiltered.leftToMax, Sigma.snd
-- 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
a : J := IsFiltered.max (k.fst (β := fun (j : J) ↦ I j)) (l.fst (β := fun (j : J) ↦ I j))
a' : I (IsFiltered.max (k.fst (β := fun (j : J) ↦ I j)) (l.fst (β := fun (j : J) ↦ I j)))
f :
  Total.mk (I := I) P (k.fst (β := fun (j : J) ↦ I j)) (k.snd (β := fun (j : J) ↦ I j)) ⟶
    Total.mk (I := I) P (IsFiltered.max (k.fst (β := fun (j : J) ↦ I j)) (l.fst (β := fun (j : J) ↦ I j))) a'
hf : f.base (I := I) = IsFiltered.leftToMax (k.fst (β := fun (j : J) ↦ I j)) (l.fst (β := fun (j : J) ↦ I j))
obtain :
  ∀ (b' : I (IsFiltered.max (k.fst (β := fun (j : J) ↦ I j)) (l.fst (β := fun (j : J) ↦ I j))))
    (g :
      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.max (k.fst (β := fun (j : J) ↦ I j)) (l.fst (β := fun (j : J) ↦ I j))) b')
    (hg : g.base (I := I) = IsFiltered.rightToMax (k.fst (β := fun (j : J) ↦ I j)) (l.fst (β := fun (j : J) ↦ I j))),
    ∃ (Z : Total (I := I) P) (x : k ⟶ Z) (x : l ⟶ Z), True
⊢ ∃ (Z : Total (I := I) P) (x : k ⟶ Z) (x : l ⟶ Z), True

Tactic:
obtain ⟨b', g, hg⟩ := Total.exists_hom_of_hom (P := P) l.2 (IsFiltered.rightToMax k.1 l.1)

Premises used: CategoryTheory.Limits.ColimitPresentation.Total.exists_hom_of_hom, CategoryTheory.IsFiltered.rightToMax, Sigma.fst, Sigma.snd
-- 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
a : J := IsFiltered.max (k.fst (β := fun (j : J) ↦ I j)) (l.fst (β := fun (j : J) ↦ I j))
a' : I (IsFiltered.max (k.fst (β := fun (j : J) ↦ I j)) (l.fst (β := fun (j : J) ↦ I j)))
f :
  Total.mk (I := I) P (k.fst (β := fun (j : J) ↦ I j)) (k.snd (β := fun (j : J) ↦ I j)) ⟶
    Total.mk (I := I) P (IsFiltered.max (k.fst (β := fun (j : J) ↦ I j)) (l.fst (β := fun (j : J) ↦ I j))) a'
hf : f.base (I := I) = IsFiltered.leftToMax (k.fst (β := fun (j : J) ↦ I j)) (l.fst (β := fun (j : J) ↦ I j))
b' : I (IsFiltered.max (k.fst (β := fun (j : J) ↦ I j)) (l.fst (β := fun (j : J) ↦ I j)))
g :
  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.max (k.fst (β := fun (j : J) ↦ I j)) (l.fst (β := fun (j : J) ↦ I j))) b'
hg : g.base (I := I) = IsFiltered.rightToMax (k.fst (β := fun (j : J) ↦ I j)) (l.fst (β := fun (j : J) ↦ I j))
⊢ ∃ (Z : Total (I := I) P) (x : k ⟶ Z) (x : l ⟶ Z), True

Tactic:
⟨⟨a, IsFiltered.max a' b'⟩, ?_, ?_, trivial⟩

Premises used: trivial, CategoryTheory.IsFiltered.max, Exists.intro, Sigma.mk
-- 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
a : J := IsFiltered.max (k.fst (β := fun (j : J) ↦ I j)) (l.fst (β := fun (j : J) ↦ I j))
a' : I (IsFiltered.max (k.fst (β := fun (j : J) ↦ I j)) (l.fst (β := fun (j : J) ↦ I j)))
f :
  Total.mk (I := I) P (k.fst (β := fun (j : J) ↦ I j)) (k.snd (β := fun (j : J) ↦ I j)) ⟶
    Total.mk (I := I) P (IsFiltered.max (k.fst (β := fun (j : J) ↦ I j)) (l.fst (β := fun (j : J) ↦ I j))) a'
hf : f.base (I := I) = IsFiltered.leftToMax (k.fst (β := fun (j : J) ↦ I j)) (l.fst (β := fun (j : J) ↦ I j))
b' : I (IsFiltered.max (k.fst (β := fun (j : J) ↦ I j)) (l.fst (β := fun (j : J) ↦ I j)))
g :
  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.max (k.fst (β := fun (j : J) ↦ I j)) (l.fst (β := fun (j : J) ↦ I j))) b'
hg : g.base (I := I) = IsFiltered.rightToMax (k.fst (β := fun (j : J) ↦ I j)) (l.fst (β := fun (j : J) ↦ I j))
refine_1 : k ⟶ Sigma.mk (β := fun (j : J) ↦ I j) a (IsFiltered.max a' b')
refine_2 : l ⟶ Sigma.mk (β := fun (j : J) ↦ I j) a (IsFiltered.max a' b')
⊢ ∃ (Z : Total (I := I) P) (x : k ⟶ Z) (x : l ⟶ Z), True

Tactic:
refine ⟨⟨a, IsFiltered.max a' b'⟩, ?_, ?_, trivial⟩