awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Epimorphisms (goal)
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
⊢ ∃ (a : x_3), (ConcreteCategory.hom (FC := TypeCat.Fun) l : (a : x_3) → x_1) a = x
have 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
Tactic: obtain ⟨y, hy⟩ := hr (b x)
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Epimorphisms (goal)
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)
⊢ ∃ (a : x_3), (ConcreteCategory.hom (FC := TypeCat.Fun) l : (a : x_3) → x_1) a = x
have 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
Tactic: obtain ⟨z, _, hz⟩ := Types.exists_of_isPullback sq _ _ hy
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Monomorphisms (hypothesis)
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
⊢ monomorphisms (Type u) r
have ht₁ : Mono t
Tactic: simp only [monomorphisms.iff] at ht ⊢
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Monomorphisms (goal)
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
⊢ monomorphisms (Type u) φ
have 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)
Tactic: simp only [functorCategory, monomorphisms.iff, mono_iff_injective] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Monomorphisms (hypothesis)
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)
⊢ Function.Injective (α := c₁.pt) (β := c₂.pt) (⇑(hom (FC := TypeCat.Fun) φ) : (a : c₁.pt) → c₂.pt)
have 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)
Tactic: replace hφ (j : J) := congr_hom (hφ j)
Cleared hypotheses: hφ
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Monomorphisms (hypothesis)
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)
⊢ Function.Injective (α := c₁.pt) (β := c₂.pt) (⇑(hom (FC := TypeCat.Fun) φ) : (a : c₁.pt) → c₂.pt)
have 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)
Tactic: simp only [Functor.const_obj_obj, comp_apply] at hφ
Cleared hypotheses: hφ
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Monomorphisms (goal)
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)
⊢ ∃ (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₁'
have 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₁'
Tactic: obtain ⟨j, x₁, rfl⟩ := Types.jointly_surjective_of_isColimit hc₁ x₁
Cleared hypotheses: x₁, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Monomorphisms (goal)
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)
⊢ x₁ = y₁
have 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))
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 _⟩
Cleared hypotheses: x₁, y₁, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Monomorphisms (hypothesis)
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 : (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))
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Monomorphisms (goal)
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) (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)
⊢ 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))
have obtain : ∀ (k : J) (α : j ⟶ k)
  (hk :
    Eq (α := (fun (X : Type u) ↦ X) (F₂.obj k))
      ((hom (FC := TypeCat.Fun) (F₂.map α) :
            (a : (fun (X : Type u) ↦ X) (F₂.obj j)) → (fun (X : Type u) ↦ X) (F₂.obj k))
          ((hom (FC := TypeCat.Fun) (f.app j) : (a : F₁.obj j) → F₂.obj j) x₁ : F₂.obj j) :
        (fun (X : Type u) ↦ X) (F₂.obj k))
      ((hom (FC := TypeCat.Fun) (F₂.map α) :
            (a : (fun (X : Type u) ↦ X) (F₂.obj j)) → (fun (X : Type u) ↦ X) (F₂.obj k))
          ((hom (FC := TypeCat.Fun) (f.app j) : (a : F₁.obj j) → F₂.obj j) y₁ : F₂.obj j) :
        (fun (X : Type u) ↦ X) (F₂.obj k))),
  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))
Tactic: obtain ⟨k, α, hk⟩ := (Types.FilteredColimit.isColimit_eq_iff' hc₂ _ _).1 h
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Monomorphisms (hypothesis)
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) (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)
k : J
α : j ⟶ k
hk :
  Eq (α := (fun (X : Type u) ↦ X) (F₂.obj k))
    ((hom (FC := TypeCat.Fun) (F₂.map α) : (a : (fun (X : Type u) ↦ X) (F₂.obj j)) → (fun (X : Type u) ↦ X) (F₂.obj k))
        ((hom (FC := TypeCat.Fun) (f.app j) : (a : F₁.obj j) → F₂.obj j) x₁ : F₂.obj j) :
      (fun (X : Type u) ↦ X) (F₂.obj k))
    ((hom (FC := TypeCat.Fun) (F₂.map α) : (a : (fun (X : Type u) ↦ X) (F₂.obj j)) → (fun (X : Type u) ↦ X) (F₂.obj k))
        ((hom (FC := TypeCat.Fun) (f.app j) : (a : F₁.obj j) → F₂.obj j) y₁ : F₂.obj j) :
      (fun (X : Type u) ↦ X) (F₂.obj k))
⊢ 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))
have hk₁ : Eq (α := F₂.obj k)
  ((hom (FC := TypeCat.Fun) (f.app k) : (a : F₁.obj k) → F₂.obj k)
      ((hom (FC := TypeCat.Fun) (F₁.map α) : (a : F₁.obj j) → F₁.obj k) x₁ : F₁.obj k) :
    F₂.obj k)
  ((hom (FC := TypeCat.Fun) (f.app k) : (a : F₁.obj k) → F₂.obj k)
      ((hom (FC := TypeCat.Fun) (F₁.map α) : (a : F₁.obj j) → F₁.obj k) y₁ : F₁.obj k) :
    F₂.obj k)
Tactic: simp only [← NatTrans.naturality_apply] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Monomorphisms (goal)
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) (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)
k : J
α : j ⟶ k
hk :
  Eq (α := F₂.obj k)
    ((hom (FC := TypeCat.Fun) (f.app k) : (a : F₁.obj k) → F₂.obj k)
        ((hom (FC := TypeCat.Fun) (F₁.map α) : (a : F₁.obj j) → F₁.obj k) x₁ : F₁.obj k) :
      F₂.obj k)
    ((hom (FC := TypeCat.Fun) (f.app k) : (a : F₁.obj k) → F₂.obj k)
        ((hom (FC := TypeCat.Fun) (F₁.map α) : (a : F₁.obj j) → F₁.obj k) y₁ : F₁.obj k) :
      F₂.obj k)
⊢ 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))
have rw : Eq (α := c₁.pt)
  ((hom (FC := TypeCat.Fun) (F₁.map α ≫ c₁.ι.app k) :
        (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) (F₁.map α ≫ c₁.ι.app k) :
        (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))
Tactic: rw [← c₁.w α, comp_apply, comp_apply, hf _ hk]
-- Lean 4 proof step from Mathlib.CategoryTheory.Types.Monomorphisms (goal)
Goal:
T : Type u'
X₁ X₂ : T → Type u
inst : HasCoproduct X₁
inst_1 : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), monomorphisms (Type u) (f j)
⊢ monomorphisms (Type u) (X := ∐ X₁) (Y := ∐ X₂) (Limits.Sigma.map (f := X₁) (g := X₂) f)
have simp : ∀ (h : ∀ (j : T), Function.Injective (α := X₁ j) (β := X₂ j) (⇑(hom (FC := TypeCat.Fun) (f j)) : (a : X₁ j) → X₂ j)),
  Function.Injective (α := ∐ X₁) (β := ∐ X₂)
    (⇑(hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f)) : (a : ∐ X₁) → ∐ X₂)
Tactic: simp only [monomorphisms.iff, mono_iff_injective] at h ⊢
Cleared hypotheses: h