awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X ⟶ Y
⊢ IsIso f ↔
    Function.Bijective (α := (fun (X : Type u) ↦ X) X) (β := (fun (X : Type u) ↦ X) Y)
      (⇑(ConcreteCategory.hom (FC := Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)

Tactic:
Iff.intro (fun _ => (asIso f : X ≅ Y).toEquiv.bijective) fun b =>
    (Equiv.ofBijective f b).toIso.isIso_hom

Premises used: Equiv.bijective, CategoryTheory.Iso.toEquiv, CategoryTheory.ConcreteCategory.hom, Equiv.toIso, CategoryTheory.Iso.isIso_hom, Equiv.ofBijective, Iff.intro, DFunLike.coe, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X → Y
⊢ Function.Bijective f ↔ IsIso (↾f)

Tactic:
Iff.intro (fun b => (Equiv.ofBijective f b).toIso.isIso_hom)
    fun _ => (asIso (ofHom f) : X ≅ Y).toEquiv.bijective

Premises used: Equiv.bijective, CategoryTheory.Iso.toEquiv, TypeCat.ofHom, Equiv.toIso, CategoryTheory.Iso.isIso_hom, Equiv.ofBijective, Iff.intro, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X ⟶ Y
hf : Epi f
h :
  ∀ (x : Y),
    (ConcreteCategory.hom (FC := Fun) (↾Function.surjInv ⋯ ≫ f)).toFun x =
      (ConcreteCategory.hom (FC := Fun) (𝟙 Y)).toFun x
⊢ ↾Function.surjInv ⋯ ≫ f = 𝟙 Y

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X ⟶ Y
hf : Epi f
x : Y
⊢ (ConcreteCategory.hom (FC := Fun) (↾Function.surjInv ⋯ ≫ f)).toFun x =
    (ConcreteCategory.hom (FC := Fun) (𝟙 Y)).toFun x

Tactic:
(Function.rightInverse_surjInv <| (epi_iff_surjective f).1 hf) x

Premises used: CategoryTheory.epi_iff_surjective, Function.surjInv, Iff.mp, Function.rightInverse_surjInv, Classical.choose
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X ⟶ Y
hf : Epi f
x : Y
⊢ (ConcreteCategory.hom (FC := Fun) (↾Function.surjInv ⋯ ≫ f)).toFun x =
    (ConcreteCategory.hom (FC := Fun) (𝟙 Y)).toFun x

Tactic:
exact (Function.rightInverse_surjInv <| (epi_iff_surjective f).1 hf) x

Premises used: CategoryTheory.epi_iff_surjective, Iff.mp, Function.rightInverse_surjInv
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
f : X ⟶ Y
hf :
  Function.Surjective (α := (fun (X : Type u) ↦ X) X) (β := (fun (X : Type u) ↦ X) Y)
    (⇑(ConcreteCategory.hom (FC := Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
⊢ IsSplitEpi f

Tactic:
simp only [(epi_iff_surjective f).mpr hf, isSplitEpi_of_epi]

Premises used: Iff.mpr, CategoryTheory.epi_iff_surjective, CategoryTheory.isSplitEpi_of_epi
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
e : X ≃ Y
⊢ (equivEquivIso : (a : X ≃ Y) → X ≅ Y) e = e.toIso

Tactic:
rfl

Premises used: Equiv.toIso, rfl
-- Module: Mathlib.CategoryTheory.Types.Basic
Goal:
X Y : Type u
e : X ≅ Y
⊢ (Equiv.symm equivEquivIso : (a : X ≅ Y) → X ≃ Y) e = e.toEquiv

Tactic:
rfl

Premises used: CategoryTheory.Iso.toEquiv, rfl
-- Module: Mathlib.CategoryTheory.Types.Epimorphisms
Goal:
x x_1 x_2 x_3 : Type u
b : x ⟶ x_3
r : x_1 ⟶ x_3
t : x_2 ⟶ x_1
l : x_2 ⟶ x
sq : IsPullback t l r b
hr : epimorphisms (Type u) r
simp :
  ∀ (hr : Function.Surjective (α := x_1) (β := x_3) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) r) : (a : x_1) → x_3)),
    Function.Surjective (α := x_2) (β := x) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) : (a : x_2) → x)
⊢ epimorphisms (Type u) l

Tactic:
simp only [epimorphisms.iff, epi_iff_surjective] at hr ⊢

Premises used: CategoryTheory.epi_iff_surjective, CategoryTheory.MorphismProperty.epimorphisms.iff
-- Module: Mathlib.CategoryTheory.Types.Epimorphisms
Goal:
x_1 x_2 x_3 x_4 : Type u
b : x_1 ⟶ x_4
r : x_2 ⟶ x_4
t : x_3 ⟶ x_2
l : x_3 ⟶ x_1
sq : IsPullback t l r b
hr : Function.Surjective (α := x_2) (β := x_4) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) r) : (a : x_2) → x_4)
x : x_1
obtain :
  ∀ (y : x_2)
    (hy :
      Eq (α := x_4) ((ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : x_2) → x_4) y : x_4)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) x_1) → (fun (X : Type u) ↦ X) x_4)
            x :
          (fun (X : Type u) ↦ X) x_4)),
    ∃ (a : x_3), (ConcreteCategory.hom (FC := TypeCat.Fun) l : (a : x_3) → x_1) a = x
⊢ ∃ (a : x_3), (ConcreteCategory.hom (FC := TypeCat.Fun) l : (a : x_3) → x_1) a = x

Tactic:
obtain ⟨y, hy⟩ := hr (b x)

Premises used: CategoryTheory.ConcreteCategory.hom, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Types.Epimorphisms
Goal:
x_1 x_2 x_3 x_4 : Type u
b : x_1 ⟶ x_4
r : x_2 ⟶ x_4
t : x_3 ⟶ x_2
l : x_3 ⟶ x_1
sq : IsPullback t l r b
hr : Function.Surjective (α := x_2) (β := x_4) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) r) : (a : x_2) → x_4)
x : x_1
y : x_2
hy :
  Eq (α := x_4) ((ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : x_2) → x_4) y : x_4)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) x_1) → (fun (X : Type u) ↦ X) x_4) x :
      (fun (X : Type u) ↦ X) x_4)
obtain :
  ∀ (z : x_3),
    (ConcreteCategory.hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) x_3) → (fun (X : Type u) ↦ X) x_2) z = y →
      ∀
        (hz :
          (ConcreteCategory.hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) x_3) → (fun (X : Type u) ↦ X) x_1)
              z =
            x),
        ∃ (a : x_3), (ConcreteCategory.hom (FC := TypeCat.Fun) l : (a : x_3) → x_1) a = x
⊢ ∃ (a : x_3), (ConcreteCategory.hom (FC := TypeCat.Fun) l : (a : x_3) → x_1) a = x

Tactic:
obtain ⟨z, _, hz⟩ := Types.exists_of_isPullback sq _ _ hy

Premises used: CategoryTheory.Limits.Types.exists_of_isPullback
-- Module: Mathlib.CategoryTheory.Types.Epimorphisms
Goal:
x_1 x_2 x_3 x_4 : Type u
b : x_1 ⟶ x_4
r : x_2 ⟶ x_4
t : x_3 ⟶ x_2
l : x_3 ⟶ x_1
sq : IsPullback t l r b
hr : Function.Surjective (α := x_2) (β := x_4) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) r) : (a : x_2) → x_4)
x : x_1
y : x_2
hy :
  Eq (α := x_4) ((ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : x_2) → x_4) y : x_4)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) x_1) → (fun (X : Type u) ↦ X) x_4) x :
      (fun (X : Type u) ↦ X) x_4)
z : x_3
left :
  (ConcreteCategory.hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) x_3) → (fun (X : Type u) ↦ X) x_2) z = y
hz : (ConcreteCategory.hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) x_3) → (fun (X : Type u) ↦ X) x_1) z = x
⊢ ∃ (a : x_3), (ConcreteCategory.hom (FC := TypeCat.Fun) l : (a : x_3) → x_1) a = x

Tactic:
⟨z, hz⟩

Premises used: Exists.intro
-- Module: Mathlib.CategoryTheory.Types.Epimorphisms
Goal:
x_1 x_2 x_3 x_4 : Type u
b : x_1 ⟶ x_4
r : x_2 ⟶ x_4
t : x_3 ⟶ x_2
l : x_3 ⟶ x_1
sq : IsPullback t l r b
hr : Function.Surjective (α := x_2) (β := x_4) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) r) : (a : x_2) → x_4)
x : x_1
y : x_2
hy :
  Eq (α := x_4) ((ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : x_2) → x_4) y : x_4)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) x_1) → (fun (X : Type u) ↦ X) x_4) x :
      (fun (X : Type u) ↦ X) x_4)
z : x_3
left :
  (ConcreteCategory.hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) x_3) → (fun (X : Type u) ↦ X) x_2) z = y
hz : (ConcreteCategory.hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) x_3) → (fun (X : Type u) ↦ X) x_1) z = x
⊢ ∃ (a : x_3), (ConcreteCategory.hom (FC := TypeCat.Fun) l : (a : x_3) → x_1) a = x

Tactic:
exact ⟨z, hz⟩
-- Module: Mathlib.CategoryTheory.Types.Monomorphisms
Goal:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₃ ⟶ X₄
b : X₂ ⟶ X₄
sq : IsPushout l t r b
ht : monomorphisms (Type u) t
⊢ Mono t

Tactic:
simp only [monomorphisms.iff] at ht ⊢

Premises used: CategoryTheory.MorphismProperty.monomorphisms.iff
-- Module: Mathlib.CategoryTheory.Types.Monomorphisms
Goal:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₃ ⟶ X₄
b : X₂ ⟶ X₄
sq : IsPushout l t r b
ht : Mono t
⊢ Mono r

Tactic:
Limits.Types.pushoutCocone_inr_mono_of_isColimit sq.flip.isColimit

Premises used: CategoryTheory.IsPushout.flip, CategoryTheory.Limits.Types.pushoutCocone_inr_mono_of_isColimit, CategoryTheory.IsPushout.isColimit
-- Module: Mathlib.CategoryTheory.Types.Monomorphisms
Goal:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₃ ⟶ X₄
b : X₂ ⟶ X₄
sq : IsPushout l t r b
ht : Mono t
⊢ Mono r

Tactic:
exact Limits.Types.pushoutCocone_inr_mono_of_isColimit sq.flip.isColimit

Premises used: CategoryTheory.IsPushout.flip, CategoryTheory.Limits.Types.pushoutCocone_inr_mono_of_isColimit, CategoryTheory.IsPushout.isColimit
-- Module: Mathlib.CategoryTheory.Types.Monomorphisms
Goal:
J : Type u'
x : Category.{v', u'} J
h : IsFiltered.{v', u'} J
F₁ F₂ : Functor.{v', u, u', u + 1} J (Type u)
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
hf : functorCategory (monomorphisms (Type u)) J f
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j
simp :
  ∀
    (hf :
      ∀ (j : J),
        Function.Injective (α := F₁.obj j) (β := F₂.obj j)
          (⇑(hom (FC := TypeCat.Fun) (f.app j)) : (a : F₁.obj j) → F₂.obj j)),
    Function.Injective (α := c₁.pt) (β := c₂.pt) (⇑(hom (FC := TypeCat.Fun) φ) : (a : c₁.pt) → c₂.pt)
⊢ monomorphisms (Type u) φ

Tactic:
simp only [functorCategory, monomorphisms.iff, mono_iff_injective] at hf ⊢

Premises used: CategoryTheory.mono_iff_injective, CategoryTheory.MorphismProperty.monomorphisms.iff, CategoryTheory.MorphismProperty.functorCategory
-- Module: Mathlib.CategoryTheory.Types.Monomorphisms
Goal:
J : Type u'
x : Category.{v', u'} J
h : IsFiltered.{v', u'} J
F₁ F₂ : Functor.{v', u, u', u + 1} J (Type u)
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
φ : c₁.pt ⟶ c₂.pt
hφ : ∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j
hf :
  ∀ (j : J),
    Function.Injective (α := F₁.obj j) (β := F₂.obj j)
      (⇑(hom (FC := TypeCat.Fun) (f.app j)) : (a : F₁.obj j) → F₂.obj j)
⊢ ∀ (j : J) (x_1 : ToType (FC := TypeCat.Fun) (F₁.obj j)),
    Eq (α := c₂.pt) ((hom (FC := TypeCat.Fun) (c₁.ι.app j ≫ φ) : (a : F₁.obj j) → c₂.pt) x_1 : c₂.pt)
      ((hom (FC := TypeCat.Fun) (f.app j ≫ c₂.ι.app j) : (a : F₁.obj j) → c₂.pt) x_1 : c₂.pt)

Tactic:
replace hφ (j : J) := congr_hom (hφ j)
-- Module: Mathlib.CategoryTheory.Types.Monomorphisms
Goal:
J : Type u'
x : Category.{v', u'} J
h : IsFiltered.{v', u'} J
F₁ F₂ : Functor.{v', u, u', u + 1} J (Type u)
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
φ : c₁.pt ⟶ c₂.pt
hf :
  ∀ (j : J),
    Function.Injective (α := F₁.obj j) (β := F₂.obj j)
      (⇑(hom (FC := TypeCat.Fun) (f.app j)) : (a : F₁.obj j) → F₂.obj j)
hφ :
  ∀ (j : J) (x_1 : ToType (FC := TypeCat.Fun) (F₁.obj j)),
    Eq (α := c₂.pt) ((hom (FC := TypeCat.Fun) (c₁.ι.app j ≫ φ) : (a : F₁.obj j) → c₂.pt) x_1 : c₂.pt)
      ((hom (FC := TypeCat.Fun) (f.app j ≫ c₂.ι.app j) : (a : F₁.obj j) → c₂.pt) x_1 : c₂.pt)
⊢ ∀ (j : J) (x_1 : ToType (FC := TypeCat.Fun) (F₁.obj j)),
    Eq (α := c₂.pt)
      ((hom (FC := TypeCat.Fun) φ : (a : c₁.pt) → c₂.pt)
          ((hom (FC := TypeCat.Fun) (c₁.ι.app j) : (a : F₁.obj j) → c₁.pt) x_1 : c₁.pt) :
        c₂.pt)
      ((hom (FC := TypeCat.Fun) (c₂.ι.app j) : (a : F₂.obj j) → c₂.pt)
          ((hom (FC := TypeCat.Fun) (f.app j) : (a : F₁.obj j) → F₂.obj j) x_1 : F₂.obj j) :
        c₂.pt)

Tactic:
simp only [Functor.const_obj_obj, comp_apply] at hφ

Premises used: CategoryTheory.comp_apply, CategoryTheory.Functor.const_obj_obj
-- Module: Mathlib.CategoryTheory.Types.Monomorphisms
Goal:
J : Type u'
x : Category.{v', u'} J
h_1 : IsFiltered.{v', u'} J
F₁ F₂ : Functor.{v', u, u', u + 1} J (Type u)
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
φ : c₁.pt ⟶ c₂.pt
hf :
  ∀ (j : J),
    Function.Injective (α := F₁.obj j) (β := F₂.obj j)
      (⇑(hom (FC := TypeCat.Fun) (f.app j)) : (a : F₁.obj j) → F₂.obj j)
hφ :
  ∀ (j : J) (x_1 : ToType (FC := TypeCat.Fun) (F₁.obj j)),
    Eq (α := c₂.pt)
      ((hom (FC := TypeCat.Fun) φ : (a : c₁.pt) → c₂.pt)
          ((hom (FC := TypeCat.Fun) (c₁.ι.app j) : (a : F₁.obj j) → c₁.pt) x_1 : c₁.pt) :
        c₂.pt)
      ((hom (FC := TypeCat.Fun) (c₂.ι.app j) : (a : F₂.obj j) → c₂.pt)
          ((hom (FC := TypeCat.Fun) (f.app j) : (a : F₁.obj j) → F₂.obj j) x_1 : F₂.obj j) :
        c₂.pt)
x₁ y₁ : c₁.pt
h :
  Eq (α := c₂.pt) ((hom (FC := TypeCat.Fun) φ : (a : c₁.pt) → c₂.pt) x₁ : c₂.pt)
    ((hom (FC := TypeCat.Fun) φ : (a : c₁.pt) → c₂.pt) y₁ : c₂.pt)
obtain :
  ∀ (j : J) (x₁ : F₁.obj j)
    (h :
      Eq (α := c₂.pt)
        ((hom (FC := TypeCat.Fun) φ : (a : c₁.pt) → c₂.pt)
            ((hom (FC := TypeCat.Fun) (c₁.ι.app j) :
                  (a : (fun (X : Type u) ↦ X) (F₁.obj j)) →
                    (fun (X : Type u) ↦ X) (((Functor.const J).obj c₁.pt).obj j))
                x₁ :
              (fun (X : Type u) ↦ X) (Functor.obj.{v', u, u', u + 1} (Functor.obj (Functor.const J) c₁.pt) j)) :
          c₂.pt)
        ((hom (FC := TypeCat.Fun) φ : (a : c₁.pt) → c₂.pt) y₁ : c₂.pt)),
    ∃ (j_1 : J) (x₁' : F₁.obj j_1) (y₁' : F₁.obj j_1),
      Eq (α := c₁.pt)
          ((hom (FC := TypeCat.Fun) (c₁.ι.app j) :
                (a : (fun (X : Type u) ↦ X) (F₁.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj c₁.pt).obj j))
              x₁ :
            (fun (X : Type u) ↦ X) (Functor.obj.{v', u, u', u + 1} (Functor.obj (Functor.const J) c₁.pt) j))
          ((hom (FC := TypeCat.Fun) (c₁.ι.app j_1) :
                (a : (fun (X : Type u) ↦ X) (F₁.obj j_1)) →
                  (fun (X : Type u) ↦ X) (((Functor.const J).obj c₁.pt).obj j_1))
              x₁' :
            (fun (X : Type u) ↦ X) (Functor.obj.{v', u, u', u + 1} (Functor.obj (Functor.const J) c₁.pt) j_1)) ∧
        y₁ =
          (hom (FC := TypeCat.Fun) (c₁.ι.app j_1) :
              (a : (fun (X : Type u) ↦ X) (F₁.obj j_1)) →
                (fun (X : Type u) ↦ X) (((Functor.const J).obj c₁.pt).obj j_1))
            y₁'
⊢ ∃ (j : J) (x₁' : F₁.obj j) (y₁' : F₁.obj j),
    x₁ =
        (hom (FC := TypeCat.Fun) (c₁.ι.app j) :
            (a : (fun (X : Type u) ↦ X) (F₁.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj c₁.pt).obj j))
          x₁' ∧
      y₁ =
        (hom (FC := TypeCat.Fun) (c₁.ι.app j) :
            (a : (fun (X : Type u) ↦ X) (F₁.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj c₁.pt).obj j))
          y₁'

Tactic:
obtain ⟨j, x₁, rfl⟩ := Types.jointly_surjective_of_isColimit hc₁ x₁

Premises used: CategoryTheory.Limits.Types.jointly_surjective_of_isColimit, rfl
-- Module: Mathlib.CategoryTheory.Types.Monomorphisms
Goal:
J : Type u'
x : Category.{v', u'} J
h_1 : IsFiltered.{v', u'} J
F₁ F₂ : Functor.{v', u, u', u + 1} J (Type u)
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
φ : c₁.pt ⟶ c₂.pt
hf :
  ∀ (j : J),
    Function.Injective (α := F₁.obj j) (β := F₂.obj j)
      (⇑(hom (FC := TypeCat.Fun) (f.app j)) : (a : F₁.obj j) → F₂.obj j)
hφ :
  ∀ (j : J) (x_1 : ToType (FC := TypeCat.Fun) (F₁.obj j)),
    Eq (α := c₂.pt)
      ((hom (FC := TypeCat.Fun) φ : (a : c₁.pt) → c₂.pt)
          ((hom (FC := TypeCat.Fun) (c₁.ι.app j) : (a : F₁.obj j) → c₁.pt) x_1 : c₁.pt) :
        c₂.pt)
      ((hom (FC := TypeCat.Fun) (c₂.ι.app j) : (a : F₂.obj j) → c₂.pt)
          ((hom (FC := TypeCat.Fun) (f.app j) : (a : F₁.obj j) → F₂.obj j) x_1 : F₂.obj j) :
        c₂.pt)
j : J
x₁ : F₁.obj j
l : J
y₁ : F₁.obj l
h :
  Eq (α := c₂.pt)
    ((hom (FC := TypeCat.Fun) φ : (a : c₁.pt) → c₂.pt)
        ((hom (FC := TypeCat.Fun) (c₁.ι.app j) :
              (a : (fun (X : Type u) ↦ X) (F₁.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj c₁.pt).obj j))
            x₁ :
          (fun (X : Type u) ↦ X) (Functor.obj.{v', u, u', u + 1} (Functor.obj (Functor.const J) c₁.pt) j)) :
      c₂.pt)
    ((hom (FC := TypeCat.Fun) φ : (a : c₁.pt) → c₂.pt)
        ((hom (FC := TypeCat.Fun) (c₁.ι.app l) :
              (a : (fun (X : Type u) ↦ X) (F₁.obj l)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj c₁.pt).obj l))
            y₁ :
          (fun (X : Type u) ↦ X) (Functor.obj.{v', u, u', u + 1} (Functor.obj (Functor.const J) c₁.pt) l)) :
      c₂.pt)
⊢ ∃ (j_1 : J) (x₁' : F₁.obj j_1) (y₁' : F₁.obj j_1),
    Eq (α := c₁.pt)
        ((hom (FC := TypeCat.Fun) (c₁.ι.app j) :
              (a : (fun (X : Type u) ↦ X) (F₁.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj c₁.pt).obj j))
            x₁ :
          (fun (X : Type u) ↦ X) (Functor.obj.{v', u, u', u + 1} (Functor.obj (Functor.const J) c₁.pt) j))
        ((hom (FC := TypeCat.Fun) (c₁.ι.app j_1) :
              (a : (fun (X : Type u) ↦ X) (F₁.obj j_1)) →
                (fun (X : Type u) ↦ X) (((Functor.const J).obj c₁.pt).obj j_1))
            x₁' :
          (fun (X : Type u) ↦ X) (Functor.obj.{v', u, u', u + 1} (Functor.obj (Functor.const J) c₁.pt) j_1)) ∧
      Eq (α := c₁.pt)
        ((hom (FC := TypeCat.Fun) (c₁.ι.app l) :
              (a : (fun (X : Type u) ↦ X) (F₁.obj l)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj c₁.pt).obj l))
            y₁ :
          (fun (X : Type u) ↦ X) (Functor.obj.{v', u, u', u + 1} (Functor.obj (Functor.const J) c₁.pt) l))
        ((hom (FC := TypeCat.Fun) (c₁.ι.app j_1) :
              (a : (fun (X : Type u) ↦ X) (F₁.obj j_1)) →
                (fun (X : Type u) ↦ X) (((Functor.const J).obj c₁.pt).obj j_1))
            y₁' :
          (fun (X : Type u) ↦ X) (Functor.obj.{v', u, u', u + 1} (Functor.obj (Functor.const J) c₁.pt) j_1))

Tactic:
exact ⟨_,  _, _, congr_hom (c₁.w (IsFiltered.leftToMax j l)).symm _,
        congr_hom (c₁.w (IsFiltered.rightToMax j l)).symm _⟩
-- Module: Mathlib.CategoryTheory.Types.Monomorphisms
Goal:
J : Type u'
x : Category.{v', u'} J
h_1 : IsFiltered.{v', u'} J
F₁ F₂ : Functor.{v', u, u', u + 1} J (Type u)
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
φ : c₁.pt ⟶ c₂.pt
hf :
  ∀ (j : J),
    Function.Injective (α := F₁.obj j) (β := F₂.obj j)
      (⇑(hom (FC := TypeCat.Fun) (f.app j)) : (a : F₁.obj j) → F₂.obj j)
hφ :
  ∀ (j : J) (x_1 : ToType (FC := TypeCat.Fun) (F₁.obj j)),
    Eq (α := c₂.pt)
      ((hom (FC := TypeCat.Fun) φ : (a : c₁.pt) → c₂.pt)
          ((hom (FC := TypeCat.Fun) (c₁.ι.app j) : (a : F₁.obj j) → c₁.pt) x_1 : c₁.pt) :
        c₂.pt)
      ((hom (FC := TypeCat.Fun) (c₂.ι.app j) : (a : F₂.obj j) → c₂.pt)
          ((hom (FC := TypeCat.Fun) (f.app j) : (a : F₁.obj j) → F₂.obj j) x_1 : F₂.obj j) :
        c₂.pt)
x₁ y₁ : c₁.pt
h :
  Eq (α := c₂.pt) ((hom (FC := TypeCat.Fun) φ : (a : c₁.pt) → c₂.pt) x₁ : c₂.pt)
    ((hom (FC := TypeCat.Fun) φ : (a : c₁.pt) → c₂.pt) y₁ : c₂.pt)
obtain :
  ∀ (j : J) (x₁ y₁ : F₁.obj j)
    (h :
      Eq (α := c₂.pt)
        ((hom (FC := TypeCat.Fun) φ : (a : c₁.pt) → c₂.pt)
            ((hom (FC := TypeCat.Fun) (c₁.ι.app j) :
                  (a : (fun (X : Type u) ↦ X) (F₁.obj j)) →
                    (fun (X : Type u) ↦ X) (((Functor.const J).obj c₁.pt).obj j))
                x₁ :
              (fun (X : Type u) ↦ X) (Functor.obj.{v', u, u', u + 1} (Functor.obj (Functor.const J) c₁.pt) j)) :
          c₂.pt)
        ((hom (FC := TypeCat.Fun) φ : (a : c₁.pt) → c₂.pt)
            ((hom (FC := TypeCat.Fun) (c₁.ι.app j) :
                  (a : (fun (X : Type u) ↦ X) (F₁.obj j)) →
                    (fun (X : Type u) ↦ X) (((Functor.const J).obj c₁.pt).obj j))
                y₁ :
              (fun (X : Type u) ↦ X) (Functor.obj.{v', u, u', u + 1} (Functor.obj (Functor.const J) c₁.pt) j)) :
          c₂.pt)),
    Eq (α := c₁.pt)
      ((hom (FC := TypeCat.Fun) (c₁.ι.app j) :
            (a : (fun (X : Type u) ↦ X) (F₁.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj c₁.pt).obj j))
          x₁ :
        (fun (X : Type u) ↦ X) (Functor.obj.{v', u, u', u + 1} (Functor.obj (Functor.const J) c₁.pt) j))
      ((hom (FC := TypeCat.Fun) (c₁.ι.app j) :
            (a : (fun (X : Type u) ↦ X) (F₁.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj c₁.pt).obj j))
          y₁ :
        (fun (X : Type u) ↦ X) (Functor.obj.{v', u, u', u + 1} (Functor.obj (Functor.const J) c₁.pt) j))
⊢ x₁ = y₁

Tactic:
obtain ⟨j, x₁, y₁, rfl, rfl⟩ : ∃ (j : J) (x₁' y₁' : F₁.obj j),
        x₁ = c₁.ι.app j x₁' ∧ y₁ = c₁.ι.app j y₁' := by
      obtain ⟨j, x₁, rfl⟩ := Types.jointly_surjective_of_isColimit hc₁ x₁
      obtain ⟨l, y₁, rfl⟩ := Types.jointly_surjective_of_isColimit hc₁ y₁
      exact ⟨_,  _, _, congr_hom (c₁.w (IsFiltered.leftToMax j l)).symm _,
        congr_hom (c₁.w (IsFiltered.rightToMax j l)).symm _⟩

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Types.Monomorphisms
Goal:
J : Type u'
x : Category.{v', u'} J
h_1 : IsFiltered.{v', u'} J
F₁ F₂ : Functor.{v', u, u', u + 1} J (Type u)
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
φ : c₁.pt ⟶ c₂.pt
hf :
  ∀ (j : J),
    Function.Injective (α := F₁.obj j) (β := F₂.obj j)
      (⇑(hom (FC := TypeCat.Fun) (f.app j)) : (a : F₁.obj j) → F₂.obj j)
hφ :
  ∀ (j : J) (x_1 : ToType (FC := TypeCat.Fun) (F₁.obj j)),
    Eq (α := c₂.pt)
      ((hom (FC := TypeCat.Fun) φ : (a : c₁.pt) → c₂.pt)
          ((hom (FC := TypeCat.Fun) (c₁.ι.app j) : (a : F₁.obj j) → c₁.pt) x_1 : c₁.pt) :
        c₂.pt)
      ((hom (FC := TypeCat.Fun) (c₂.ι.app j) : (a : F₂.obj j) → c₂.pt)
          ((hom (FC := TypeCat.Fun) (f.app j) : (a : F₁.obj j) → F₂.obj j) x_1 : F₂.obj j) :
        c₂.pt)
j : J
x₁ y₁ : F₁.obj j
h :
  Eq (α := c₂.pt)
    ((hom (FC := TypeCat.Fun) φ : (a : c₁.pt) → c₂.pt)
        ((hom (FC := TypeCat.Fun) (c₁.ι.app j) :
              (a : (fun (X : Type u) ↦ X) (F₁.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj c₁.pt).obj j))
            x₁ :
          (fun (X : Type u) ↦ X) (Functor.obj.{v', u, u', u + 1} (Functor.obj (Functor.const J) c₁.pt) j)) :
      c₂.pt)
    ((hom (FC := TypeCat.Fun) φ : (a : c₁.pt) → c₂.pt)
        ((hom (FC := TypeCat.Fun) (c₁.ι.app j) :
              (a : (fun (X : Type u) ↦ X) (F₁.obj j)) → (fun (X : Type u) ↦ X) (((Functor.const J).obj c₁.pt).obj j))
            y₁ :
          (fun (X : Type u) ↦ X) (Functor.obj.{v', u, u', u + 1} (Functor.obj (Functor.const J) c₁.pt) j)) :
      c₂.pt)
⊢ Eq (α := c₂.pt)
    ((hom (FC := TypeCat.Fun) (c₂.ι.app j) : (a : F₂.obj j) → c₂.pt)
        ((hom (FC := TypeCat.Fun) (f.app j) : (a : F₁.obj j) → F₂.obj j) x₁ : F₂.obj j) :
      c₂.pt)
    ((hom (FC := TypeCat.Fun) (c₂.ι.app j) : (a : F₂.obj j) → c₂.pt)
        ((hom (FC := TypeCat.Fun) (f.app j) : (a : F₁.obj j) → F₂.obj j) y₁ : F₂.obj j) :
      c₂.pt)

Tactic:
simp only [Functor.const_obj_obj, hφ] at h

Premises used: CategoryTheory.Functor.const_obj_obj