awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) (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 (α := 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

Premises used: CategoryTheory.NatTrans.naturality_apply
-- Module: Mathlib.CategoryTheory.Types.Monomorphisms
Goal:
T : Type u'
X₁ X₂ : T → Type u
_ :
  ∀ [inst : HasCoproduct X₁] [inst_1 : HasCoproduct X₂] (f : (j : T) → X₁ j ⟶ X₂ j),
    (∀ (j : T), monomorphisms (Type u) (f j)) →
      monomorphisms (Type u) (X := ∐ X₁) (Y := ∐ X₂) (Limits.Sigma.map (f := X₁) (g := X₂) f)
⊢ ∀ [inst : HasCoproduct X₁] [inst_1 : HasCoproduct X₂] (f : (j : T) → X₁ j ⟶ X₂ j),
    (∀ (j : T), monomorphisms (Type u) (f j)) →
      monomorphisms (Type u) (X := ∐ X₁) (Y := ∐ X₂) (Limits.Sigma.map (f := X₁) (g := X₂) f)

Tactic:
_
-- Module: Mathlib.CategoryTheory.Types.Monomorphisms
Goal:
T : Type u'
X₁ X₂ : T → Type u
inst : HasCoproduct X₁
_ :
  ∀ [inst_1 : HasCoproduct X₂] (f : (j : T) → X₁ j ⟶ X₂ j),
    (∀ (j : T), monomorphisms (Type u) (f j)) →
      monomorphisms (Type u) (X := ∐ X₁) (Y := ∐ X₂) (Limits.Sigma.map (f := X₁) (g := X₂) f)
⊢ ∀ [inst_1 : HasCoproduct X₂] (f : (j : T) → X₁ j ⟶ X₂ j),
    (∀ (j : T), monomorphisms (Type u) (f j)) →
      monomorphisms (Type u) (X := ∐ X₁) (Y := ∐ X₂) (Limits.Sigma.map (f := X₁) (g := X₂) f)

Tactic:
_
-- Module: Mathlib.CategoryTheory.Types.Monomorphisms
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)
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₂)
⊢ monomorphisms (Type u) (X := ∐ X₁) (Y := ∐ X₂) (Limits.Sigma.map (f := X₁) (g := X₂) f)

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

Premises used: CategoryTheory.mono_iff_injective, CategoryTheory.MorphismProperty.monomorphisms.iff
-- Module: Mathlib.CategoryTheory.Types.Monomorphisms
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), Function.Injective (α := X₁ j) (β := X₂ j) (⇑(hom (FC := TypeCat.Fun) (f j)) : (a : X₁ j) → X₂ j)
x₁ x₂ : ∐ X₁
hx :
  Eq (α := ∐ X₂) ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂) x₁ : ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂) x₂ : ∐ X₂)
obtain :
  ∀ (i₁ : T) (x₁ : X₁ i₁)
    (hx :
      Eq (α := ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
            ((hom (FC := TypeCat.Fun) ((Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).inj (f := X₁) i₁) :
                  (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt)
                x₁ :
              (fun (X : Type u) ↦ X) (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
          ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂) x₂ : ∐ X₂)),
    (hom (FC := TypeCat.Fun) ((Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).inj (f := X₁) i₁) :
          (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt)
        x₁ =
      x₂
⊢ x₁ = x₂

Tactic:
obtain ⟨i₁, x₁, rfl⟩ := Cofan.inj_jointly_surjective_of_isColimit
      (coproductIsCoproduct X₁) x₁

Premises used: CategoryTheory.Limits.coproductIsCoproduct, CategoryTheory.Limits.Cofan.inj_jointly_surjective_of_isColimit, rfl
-- Module: Mathlib.CategoryTheory.Types.Monomorphisms
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), Function.Injective (α := X₁ j) (β := X₂ j) (⇑(hom (FC := TypeCat.Fun) (f j)) : (a : X₁ j) → X₂ j)
x₂ : ∐ X₁
i₁ : T
x₁ : X₁ i₁
hx :
  Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) ((Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).inj (f := X₁) i₁) :
              (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt)
            x₁ :
          (fun (X : Type u) ↦ X) (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂) x₂ : ∐ X₂)
obtain :
  ∀ (i₂ : T) (x₂ : X₁ i₂)
    (hx :
      Eq (α := ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
            ((hom (FC := TypeCat.Fun) ((Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).inj (f := X₁) i₁) :
                  (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt)
                x₁ :
              (fun (X : Type u) ↦ X) (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
          ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
            ((hom (FC := TypeCat.Fun) ((Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).inj (f := X₁) i₂) :
                  (a : (fun (X : Type u) ↦ X) (X₁ i₂)) → (fun (X : Type u) ↦ X) (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt)
                x₂ :
              (fun (X : Type u) ↦ X) (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
          ∐ X₂)),
    Eq (α := ∐ X₁)
      ((hom (FC := TypeCat.Fun) ((Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).inj (f := X₁) i₁) :
            (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt)
          x₁ :
        (fun (X : Type u) ↦ X) (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)
      ((hom (FC := TypeCat.Fun) ((Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).inj (f := X₁) i₂) :
            (a : (fun (X : Type u) ↦ X) (X₁ i₂)) → (fun (X : Type u) ↦ X) (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt)
          x₂ :
        (fun (X : Type u) ↦ X) (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)
⊢ (hom (FC := TypeCat.Fun) ((Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).inj (f := X₁) i₁) :
        (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt)
      x₁ =
    x₂

Tactic:
obtain ⟨i₂, x₂, rfl⟩ := Cofan.inj_jointly_surjective_of_isColimit
      (coproductIsCoproduct X₁) x₂

Premises used: CategoryTheory.Limits.coproductIsCoproduct, CategoryTheory.Limits.Cofan.inj_jointly_surjective_of_isColimit, rfl
-- Module: Mathlib.CategoryTheory.Types.Monomorphisms
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), Function.Injective (α := X₁ j) (β := X₂ j) (⇑(hom (FC := TypeCat.Fun) (f j)) : (a : X₁ j) → X₂ j)
i₁ : T
x₁ : X₁ i₁
i₂ : T
x₂ : X₁ i₂
hx :
  Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) ((Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).inj (f := X₁) i₁) :
              (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt)
            x₁ :
          (fun (X : Type u) ↦ X) (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) ((Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).inj (f := X₁) i₂) :
              (a : (fun (X : Type u) ↦ X) (X₁ i₂)) → (fun (X : Type u) ↦ X) (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt)
            x₂ :
          (fun (X : Type u) ↦ X) (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
      ∐ X₂)
simp :
  Eq (α := ∐ X₁)
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₁ :
      (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₂) : (a : X₁ i₂) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₂ :
      (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)
⊢ Eq (α := ∐ X₁)
    ((hom (FC := TypeCat.Fun) ((Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).inj (f := X₁) i₁) :
          (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt)
        x₁ :
      (fun (X : Type u) ↦ X) (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)
    ((hom (FC := TypeCat.Fun) ((Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).inj (f := X₁) i₂) :
          (a : (fun (X : Type u) ↦ X) (X₁ i₂)) → (fun (X : Type u) ↦ X) (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt)
        x₂ :
      (fun (X : Type u) ↦ X) (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)

Tactic:
simp only [cofan_mk_inj] at hx ⊢

Premises used: CategoryTheory.Limits.cofan_mk_inj
-- Module: Mathlib.CategoryTheory.Types.Monomorphisms
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), Function.Injective (α := X₁ j) (β := X₂ j) (⇑(hom (FC := TypeCat.Fun) (f j)) : (a : X₁ j) → X₂ j)
i₁ : T
x₁ : X₁ i₁
i₂ : T
x₂ : X₁ i₂
hx :
  Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₁ :
          (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₂) : (a : X₁ i₂) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₂ :
          (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
      ∐ X₂)
⊢ Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := ∐ X₁) (Sigma.ι X₁ i₁) (Limits.Sigma.map (f := X₁) (g := X₂) f)) :
          (a : X₁ i₁) → ∐ X₂)
        x₁ :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (f i₁ ≫ Sigma.ι X₂ i₁) : (a : X₁ i₁) → ∐ X₂) x₁ : ∐ X₂)

Tactic:
have h₁ := congr_hom (Sigma.ι_map f i₁) x₁
-- Module: Mathlib.CategoryTheory.Types.Monomorphisms
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), Function.Injective (α := X₁ j) (β := X₂ j) (⇑(hom (FC := TypeCat.Fun) (f j)) : (a : X₁ j) → X₂ j)
i₁ : T
x₁ : X₁ i₁
i₂ : T
x₂ : X₁ i₂
hx :
  Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₁ :
          (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₂) : (a : X₁ i₂) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₂ :
          (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
      ∐ X₂)
h₁ :
  Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := ∐ X₁) (Sigma.ι X₁ i₁) (Limits.Sigma.map (f := X₁) (g := X₂) f)) :
          (a : X₁ i₁) → ∐ X₂)
        x₁ :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (f i₁ ≫ Sigma.ι X₂ i₁) : (a : X₁ i₁) → ∐ X₂) x₁ : ∐ X₂)
⊢ Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := ∐ X₁) (Sigma.ι X₁ i₂) (Limits.Sigma.map (f := X₁) (g := X₂) f)) :
          (a : X₁ i₂) → ∐ X₂)
        x₂ :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (f i₂ ≫ Sigma.ι X₂ i₂) : (a : X₁ i₂) → ∐ X₂) x₂ : ∐ X₂)

Tactic:
have h₂ := congr_hom (Sigma.ι_map f i₂) x₂
-- Module: Mathlib.CategoryTheory.Types.Monomorphisms
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), Function.Injective (α := X₁ j) (β := X₂ j) (⇑(hom (FC := TypeCat.Fun) (f j)) : (a : X₁ j) → X₂ j)
i₁ : T
x₁ : X₁ i₁
i₂ : T
x₂ : X₁ i₂
hx :
  Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₁ :
          (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₂) : (a : X₁ i₂) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₂ :
          (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
      ∐ X₂)
h₁ :
  Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := ∐ X₁) (Sigma.ι X₁ i₁) (Limits.Sigma.map (f := X₁) (g := X₂) f)) :
          (a : X₁ i₁) → ∐ X₂)
        x₁ :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (f i₁ ≫ Sigma.ι X₂ i₁) : (a : X₁ i₁) → ∐ X₂) x₁ : ∐ X₂)
h₂ :
  Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := ∐ X₁) (Sigma.ι X₁ i₂) (Limits.Sigma.map (f := X₁) (g := X₂) f)) :
          (a : X₁ i₂) → ∐ X₂)
        x₂ :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (f i₂ ≫ Sigma.ι X₂ i₂) : (a : X₁ i₂) → ∐ X₂) x₂ : ∐ X₂)
⊢ Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → ∐ X₁) x₁ : ∐ X₁) :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₁) : (a : X₂ i₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (f i₁) : (a : X₁ i₁) → X₂ i₁) x₁ : X₂ i₁) :
      ∐ X₂)

Tactic:
simp only [comp_apply] at h₁ h₂ hx

Premises used: CategoryTheory.comp_apply
-- Module: Mathlib.CategoryTheory.Types.Monomorphisms
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), Function.Injective (α := X₁ j) (β := X₂ j) (⇑(hom (FC := TypeCat.Fun) (f j)) : (a : X₁ j) → X₂ j)
i₁ : T
x₁ : X₁ i₁
i₂ : T
x₂ : X₁ i₂
hx :
  Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₁ :
          (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₂) : (a : X₁ i₂) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₂ :
          (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
      ∐ X₂)
h₁ :
  Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := ∐ X₁) (Sigma.ι X₁ i₁) (Limits.Sigma.map (f := X₁) (g := X₂) f)) :
          (a : X₁ i₁) → ∐ X₂)
        x₁ :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (f i₁ ≫ Sigma.ι X₂ i₁) : (a : X₁ i₁) → ∐ X₂) x₁ : ∐ X₂)
h₂ :
  Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := ∐ X₁) (Sigma.ι X₁ i₂) (Limits.Sigma.map (f := X₁) (g := X₂) f)) :
          (a : X₁ i₂) → ∐ X₂)
        x₂ :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (f i₂ ≫ Sigma.ι X₂ i₂) : (a : X₁ i₂) → ∐ X₂) x₂ : ∐ X₂)
h₃ :
  Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → ∐ X₁) x₁ : ∐ X₁) :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₁) : (a : X₂ i₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (f i₁) : (a : X₁ i₁) → X₂ i₁) x₁ : X₂ i₁) :
      ∐ X₂)
⊢ Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₂) : (a : X₁ i₂) → ∐ X₁) x₂ : ∐ X₁) :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₂) : (a : X₂ i₂) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (f i₂) : (a : X₁ i₂) → X₂ i₂) x₂ : X₂ i₂) :
      ∐ X₂)

Tactic:
simp only [comp_apply] at h₁ h₂ hx

Premises used: CategoryTheory.comp_apply
-- Module: Mathlib.CategoryTheory.Types.Monomorphisms
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), Function.Injective (α := X₁ j) (β := X₂ j) (⇑(hom (FC := TypeCat.Fun) (f j)) : (a : X₁ j) → X₂ j)
i₁ : T
x₁ : X₁ i₁
i₂ : T
x₂ : X₁ i₂
hx :
  Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₁ :
          (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₂) : (a : X₁ i₂) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₂ :
          (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
      ∐ X₂)
h₁ :
  Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → ∐ X₁) x₁ : ∐ X₁) :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₁) : (a : X₂ i₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (f i₁) : (a : X₁ i₁) → X₂ i₁) x₁ : X₂ i₁) :
      ∐ X₂)
h₂ :
  Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₂) : (a : X₁ i₂) → ∐ X₁) x₂ : ∐ X₁) :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₂) : (a : X₂ i₂) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (f i₂) : (a : X₁ i₂) → X₂ i₂) x₂ : X₂ i₂) :
      ∐ X₂)
⊢ Eq (α := (fun (X : Type u) ↦ X) (∐ X₂))
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₁) : (a : (fun (X : Type u) ↦ X) (X₂ i₁)) → (fun (X : Type u) ↦ X) (∐ X₂))
        ((hom (FC := TypeCat.Fun) (f i₁) : (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (X₂ i₁)) x₁ :
          (fun (X : Type u) ↦ X) (X₂ i₁)) :
      (fun (X : Type u) ↦ X) (∐ X₂))
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₂) : (a : (fun (X : Type u) ↦ X) (X₂ i₂)) → (fun (X : Type u) ↦ X) (∐ X₂))
        ((hom (FC := TypeCat.Fun) (f i₂) : (a : (fun (X : Type u) ↦ X) (X₁ i₂)) → (fun (X : Type u) ↦ X) (X₂ i₂)) x₂ :
          (fun (X : Type u) ↦ X) (X₂ i₂)) :
      (fun (X : Type u) ↦ X) (∐ X₂))

Tactic:
simpa [← h₁, ← h₂]
-- Module: Mathlib.CategoryTheory.Types.Monomorphisms
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), Function.Injective (α := X₁ j) (β := X₂ j) (⇑(hom (FC := TypeCat.Fun) (f j)) : (a : X₁ j) → X₂ j)
i₁ : T
x₁ : X₁ i₁
i₂ : T
x₂ : X₁ i₂
hx :
  Eq (α := ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₁ :
          (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
      ∐ X₂)
    ((hom (FC := TypeCat.Fun) (Limits.Sigma.map (f := X₁) (g := X₂) f) : (a : ∐ X₁) → ∐ X₂)
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₂) : (a : X₁ i₂) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₂ :
          (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt) :
      ∐ X₂)
⊢ Eq (α := (fun (X : Type u) ↦ X) (∐ X₂))
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₁) : (a : (fun (X : Type u) ↦ X) (X₂ i₁)) → (fun (X : Type u) ↦ X) (∐ X₂))
        ((hom (FC := TypeCat.Fun) (f i₁) : (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (X₂ i₁)) x₁ :
          (fun (X : Type u) ↦ X) (X₂ i₁)) :
      (fun (X : Type u) ↦ X) (∐ X₂))
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₂) : (a : (fun (X : Type u) ↦ X) (X₂ i₂)) → (fun (X : Type u) ↦ X) (∐ X₂))
        ((hom (FC := TypeCat.Fun) (f i₂) : (a : (fun (X : Type u) ↦ X) (X₁ i₂)) → (fun (X : Type u) ↦ X) (X₂ i₂)) x₂ :
          (fun (X : Type u) ↦ X) (X₂ i₂)) :
      (fun (X : Type u) ↦ X) (∐ X₂))

Tactic:
replace hx : Sigma.ι X₂ i₁ (f i₁ x₁) = Sigma.ι X₂ i₂ (f i₂ x₂) := by
      have h₁ := congr_hom (Sigma.ι_map f i₁) x₁
      have h₂ := congr_hom (Sigma.ι_map f i₂) x₂
      simp only [comp_apply] at h₁ h₂ hx
      simpa [← h₁, ← h₂]
-- Module: Mathlib.CategoryTheory.Types.Monomorphisms
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), Function.Injective (α := X₁ j) (β := X₂ j) (⇑(hom (FC := TypeCat.Fun) (f j)) : (a : X₁ j) → X₂ j)
i₁ : T
x₁ : X₁ i₁
i₂ : T
x₂ : X₁ i₂
hx :
  Eq (α := (fun (X : Type u) ↦ X) (∐ X₂))
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₁) : (a : (fun (X : Type u) ↦ X) (X₂ i₁)) → (fun (X : Type u) ↦ X) (∐ X₂))
        ((hom (FC := TypeCat.Fun) (f i₁) : (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (X₂ i₁)) x₁ :
          (fun (X : Type u) ↦ X) (X₂ i₁)) :
      (fun (X : Type u) ↦ X) (∐ X₂))
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₂) : (a : (fun (X : Type u) ↦ X) (X₂ i₂)) → (fun (X : Type u) ↦ X) (∐ X₂))
        ((hom (FC := TypeCat.Fun) (f i₂) : (a : (fun (X : Type u) ↦ X) (X₁ i₂)) → (fun (X : Type u) ↦ X) (X₂ i₂)) x₂ :
          (fun (X : Type u) ↦ X) (X₂ i₂)) :
      (fun (X : Type u) ↦ X) (∐ X₂))
obtain :
  ∀ (x₂ : X₁ i₁)
    (hx :
      Eq (α := (fun (X : Type u) ↦ X) (∐ X₂))
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₁) :
              (a : (fun (X : Type u) ↦ X) (X₂ i₁)) → (fun (X : Type u) ↦ X) (∐ X₂))
            ((hom (FC := TypeCat.Fun) (f i₁) : (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (X₂ i₁))
                x₁ :
              (fun (X : Type u) ↦ X) (X₂ i₁)) :
          (fun (X : Type u) ↦ X) (∐ X₂))
        ((hom (FC := TypeCat.Fun) (Sigma.ι X₂ i₁) :
              (a : (fun (X : Type u) ↦ X) (X₂ i₁)) → (fun (X : Type u) ↦ X) (∐ X₂))
            ((hom (FC := TypeCat.Fun) (f i₁) : (a : (fun (X : Type u) ↦ X) (X₁ i₁)) → (fun (X : Type u) ↦ X) (X₂ i₁))
                x₂ :
              (fun (X : Type u) ↦ X) (X₂ i₁)) :
          (fun (X : Type u) ↦ X) (∐ X₂))),
    Eq (α := ∐ X₁)
      ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₁ :
        (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)
      ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₂ :
        (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)
⊢ Eq (α := ∐ X₁)
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₁) : (a : X₁ i₁) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₁ :
      (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)
    ((hom (FC := TypeCat.Fun) (Sigma.ι X₁ i₂) : (a : X₁ i₂) → (Cofan.mk (∐ X₁) (Sigma.ι X₁)).pt) x₂ :
      (Cofan.mk (f := X₁) (∐ X₁) (Sigma.ι X₁)).pt)

Tactic:
obtain rfl := Cofan.eq_of_inj_apply_eq_of_isColimit (coproductIsCoproduct X₂) _ _ hx

Premises used: CategoryTheory.Limits.Cofan.eq_of_inj_apply_eq_of_isColimit, CategoryTheory.Limits.coproductIsCoproduct, rfl