awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
X : I₁ ⊕ I₂ → C
c : Cofan X
c₁ : Cofan.{u_2, v_1, u_1} (X ∘ Sum.inl)
c₂ : Cofan.{u_3, v_1, u_1} (X ∘ Sum.inr)
hc : IsColimit c
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
inst_1 : MonoCoprod.{v_1, u_1} C
inr : c₂.pt ⟶ c.pt
hinr : ∀ (i₂ : I₂), c₂.inj i₂ ≫ inr = c.inj (Sum.inr i₂)
suffices : inr = (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr
⊢ Mono inr

Tactic:
suffices inr = (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr by
    rw [this]
    exact MonoCoprod.binaryCofan_inr _ (isColimitBinaryCofanSum c c₁ c₂ hc hc₁ hc₂)
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
X : I₁ ⊕ I₂ → C
c : Cofan X
c₁ : Cofan.{u_2, v_1, u_1} (X ∘ Sum.inl)
c₂ : Cofan.{u_3, v_1, u_1} (X ∘ Sum.inr)
hc : IsColimit c
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
inst_1 : MonoCoprod.{v_1, u_1} C
inr : c₂.pt ⟶ c.pt
hinr : ∀ (i₂ : I₂), c₂.inj i₂ ≫ inr = c.inj (Sum.inr i₂)
⊢ ∀ (i : I₂), c₂.inj i ≫ inr = c₂.inj i ≫ (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr

Tactic:
simpa using hinr
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
X : I₁ ⊕ I₂ → C
c : Cofan X
c₁ : Cofan.{u_2, v_1, u_1} (X ∘ Sum.inl)
c₂ : Cofan.{u_3, v_1, u_1} (X ∘ Sum.inr)
hc : IsColimit c
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
inst_1 : MonoCoprod.{v_1, u_1} C
inr : c₂.pt ⟶ c.pt
hinr : ∀ (i₂ : I₂), c₂.inj i₂ ≫ inr = c.inj (Sum.inr i₂)
⊢ inr = (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr

Tactic:
exact Cofan.IsColimit.hom_ext hc₂ _ _ (by simpa using hinr)

Premises used: CategoryTheory.Limits.Cofan.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoCoprod.{v_1, u_1} C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
c : Cofan.{u_2, v_1, u_1} X
c₁ : Cofan.{u_3, v_1, u_1} (X ∘ ι)
hc : IsColimit c
hc₁ : IsColimit c₁
c₂ : Cofan.{u_2, v_1, u_1} (C := C) fun (k : (↑(Set.range ι)ᶜ : Type u_2)) ↦ X (↑k : I)
hc₂ : IsColimit c₂
e : Sum.{u_3, u_2} J (↑(Set.range ι)ᶜ : Type u_2) ≃ I :=
  Equiv.trans ((Equiv.ofInjective ι hι).sumCongr (Equiv.refl (↑(Set.range ι)ᶜ : Type u_2)))
    (Equiv.Set.sumCompl (Set.range ι))
⊢ ∀ (i₁ : J),
    Eq (α :=
      ((fun (i' : Sum.{u_3, u_2} J (↑(Set.range ι)ᶜ : Type u_2)) ↦
              X ((e : (a : J ⊕ (↑(Set.range ι)ᶜ : Type u_2)) → I) i')) ∘
            Sum.inl)
          i₁ ⟶
        Cocone.pt (J := Discrete (Sum.{u_3, u_2} J (↑(Set.range ι)ᶜ : Type u_2))) (F :=
          Discrete.functor fun (i' : Sum.{u_3, u_2} J (↑(Set.range ι)ᶜ : Type u_2)) ↦
            X ((e : (a : J ⊕ (↑(Set.range ι)ᶜ : Type u_2)) → I) i'))
          (Cofan.mk c.pt fun (i' : Sum.{u_3, u_2} J (↑(Set.range ι)ᶜ : Type u_2)) ↦
            c.inj ((e : (a : J ⊕ (↑(Set.range ι)ᶜ : Type u_2)) → I) i')))
      (c₁.inj i₁ ≫ Cofan.IsColimit.desc hc₁ fun (i : J) ↦ c.inj (ι i))
      (Cofan.inj
        (Cofan.mk c.pt fun (i' : Sum.{u_3, u_2} J (↑(Set.range ι)ᶜ : Type u_2)) ↦
          c.inj ((e : (a : J ⊕ (↑(Set.range ι)ᶜ : Type u_2)) → I) i'))
        (Sum.inl i₁))

Tactic:
simp [e]
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoCoprod.{v_1, u_1} C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
c : Cofan.{u_2, v_1, u_1} X
c₁ : Cofan.{u_3, v_1, u_1} (X ∘ ι)
hc : IsColimit c
hc₁ : IsColimit c₁
c₂ : Cofan.{u_2, v_1, u_1} (C := C) fun (k : (↑(Set.range ι)ᶜ : Type u_2)) ↦ X (↑k : I)
hc₂ : IsColimit c₂
e : Sum.{u_3, u_2} J (↑(Set.range ι)ᶜ : Type u_2) ≃ I :=
  Equiv.trans ((Equiv.ofInjective ι hι).sumCongr (Equiv.refl (↑(Set.range ι)ᶜ : Type u_2)))
    (Equiv.Set.sumCompl (Set.range ι))
refine :
  IsColimit (J := Discrete (Sum.{u_3, u_2} J (↑(Set.range ι)ᶜ : Type u_2))) (F :=
    Discrete.functor fun (i' : Sum.{u_3, u_2} J (↑(Set.range ι)ᶜ : Type u_2)) ↦
      X ((e : (a : J ⊕ (↑(Set.range ι)ᶜ : Type u_2)) → I) i'))
    (Cofan.mk c.pt fun (i' : Sum.{u_3, u_2} J (↑(Set.range ι)ᶜ : Type u_2)) ↦
      c.inj ((e : (a : J ⊕ (↑(Set.range ι)ᶜ : Type u_2)) → I) i'))
⊢ Mono (Y := c.pt) (Cofan.IsColimit.desc hc₁ fun (i : J) ↦ c.inj (ι i))

Tactic:
refine mono_binaryCofanSum_inl' (Cofan.mk c.pt (fun i' => c.inj (e i'))) _ _ ?_
    hc₁ hc₂ _ (by simp [e])

Premises used: CategoryTheory.Limits.MonoCoprod.mono_binaryCofanSum_inl', CategoryTheory.Limits.Cofan.inj, CategoryTheory.Limits.Cofan.mk, DFunLike.coe, CategoryTheory.Limits.Cocone.pt
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoCoprod.{v_1, u_1} C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
c : Cofan.{u_2, v_1, u_1} X
c₁ : Cofan.{u_3, v_1, u_1} (X ∘ ι)
hc : IsColimit c
hc₁ : IsColimit c₁
c₂ : Cofan.{u_2, v_1, u_1} (C := C) fun (k : (↑(Set.range ι)ᶜ : Type u_2)) ↦ X (↑k : I)
hc₂ : IsColimit c₂
e : Sum.{u_3, u_2} J (↑(Set.range ι)ᶜ : Type u_2) ≃ I :=
  Equiv.trans ((Equiv.ofInjective ι hι).sumCongr (Equiv.refl (↑(Set.range ι)ᶜ : Type u_2)))
    (Equiv.Set.sumCompl (Set.range ι))
⊢ IsColimit (J := Discrete (Sum.{u_3, u_2} J (↑(Set.range ι)ᶜ : Type u_2))) (F :=
    Discrete.functor fun (i' : Sum.{u_3, u_2} J (↑(Set.range ι)ᶜ : Type u_2)) ↦
      X ((e : (a : J ⊕ (↑(Set.range ι)ᶜ : Type u_2)) → I) i'))
    (Cofan.mk c.pt fun (i' : Sum.{u_3, u_2} J (↑(Set.range ι)ᶜ : Type u_2)) ↦
      c.inj ((e : (a : J ⊕ (↑(Set.range ι)ᶜ : Type u_2)) → I) i'))

Tactic:
exact IsColimit.ofIsoColimit ((IsColimit.ofCoconeEquiv (Cocone.equivalenceOfReindexing
    (Discrete.equivalence e) (Iso.refl _))).symm hc) (Cocone.ext (Iso.refl _))

Premises used: CategoryTheory.Limits.IsColimit.ofCoconeEquiv, CategoryTheory.Limits.Cocone.ext, CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.Iso.refl, CategoryTheory.Discrete.equivalence, CategoryTheory.Limits.Cocone.equivalenceOfReindexing, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoCoprod.{v_1, u_1} C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
c : Cofan.{u_2, v_1, u_1} X
c₁ : Cofan.{u_3, v_1, u_1} (X ∘ ι)
hc : IsColimit c
hc₁ : IsColimit c₁
c₂ : Cofan.{u_2, v_1, u_1} (C := C) fun (k : (↑(Set.range ι)ᶜ : Type u_2)) ↦ X (↑k : I)
hc₂ : IsColimit c₂
let let₁ let₂ : Mono (Y := c.pt) (Cofan.IsColimit.desc hc₁ fun (i : J) ↦ c.inj (ι i))
let₃ :
  let e :=
    Equiv.trans ((Equiv.ofInjective ι hι).sumCongr (Equiv.refl (↑(Set.range ι)ᶜ : Type u_2)))
      (Equiv.Set.sumCompl (Set.range ι));
  IsColimit (J := Discrete (Sum.{u_3, u_2} J (↑(Set.range ι)ᶜ : Type u_2))) (F :=
    Discrete.functor fun (i' : Sum.{u_3, u_2} J (↑(Set.range ι)ᶜ : Type u_2)) ↦
      X ((e : (a : J ⊕ (↑(Set.range ι)ᶜ : Type u_2)) → I) i'))
    (Cofan.mk c.pt fun (i' : Sum.{u_3, u_2} J (↑(Set.range ι)ᶜ : Type u_2)) ↦
      c.inj ((e : (a : J ⊕ (↑(Set.range ι)ᶜ : Type u_2)) → I) i'))
⊢ Mono (Y := c.pt) (Cofan.IsColimit.desc hc₁ fun (i : J) ↦ c.inj (ι i))

Tactic:
classical
  let e := ((Equiv.ofInjective ι hι).sumCongr (Equiv.refl _)).trans (Equiv.Set.sumCompl _)
  refine mono_binaryCofanSum_inl' (Cofan.mk c.pt (fun i' => c.inj (e i'))) _ _ ?_
    hc₁ hc₂ _ (by simp [e])
  exact IsColimit.ofIsoColimit ((IsColimit.ofCoconeEquiv (Cocone.equivalenceOfReindexing
    (Discrete.equivalence e) (Iso.refl _))).symm hc) (Cocone.ext (Iso.refl _))
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoCoprod.{v_1, u_1} C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
c : Cofan.{u_2, v_1, u_1} X
c₁ : Cofan.{u_3, v_1, u_1} (X ∘ ι)
hc : IsColimit c
hc₁ : IsColimit c₁
inst_2 : HasCoproduct.{u_2, v_1, u_1} (C := C) fun (k : (↑(Set.range ι)ᶜ : Type u_2)) ↦ X (↑k : I)
⊢ Mono (Y := c.pt) (Cofan.IsColimit.desc hc₁ fun (i : J) ↦ c.inj (ι i))

Tactic:
mono_of_injective_aux X ι hι c c₁ hc hc₁ _ (colimit.isColimit _)

Premises used: CategoryTheory.Limits.MonoCoprod.mono_of_injective_aux, CategoryTheory.Limits.colimit.isColimit
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoCoprod.{v_1, u_1} C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
inst_2 : HasCoproduct.{u_3, v_1, u_1} (X ∘ ι)
inst_3 : HasCoproduct.{u_2, v_1, u_1} X
inst_4 : HasCoproduct.{u_2, v_1, u_1} (C := C) fun (k : (↑(Set.range ι)ᶜ : Type u_2)) ↦ X (↑k : I)
⊢ Mono.{v_1, u_1} (C := C) (X := sigmaObj.{u_3, v_1, u_1} (X ∘ ι)) (Y := sigmaObj.{u_2, v_1, u_1} X)
    (Sigma.desc fun (j : J) ↦ Sigma.ι X (ι j))

Tactic:
mono_of_injective X ι hι _ _ (colimit.isColimit _) (colimit.isColimit _)

Premises used: CategoryTheory.Limits.Cofan.IsColimit.desc, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.MonoCoprod.mono_of_injective, CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimit.desc, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoCoprod.{v_1, u_1} C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
inst_2 : HasCoproduct.{u_3, v_1, u_1} (X ∘ ι)
inst_3 : HasCoproduct.{u_2, v_1, u_1} X
inst_4 : HasCoproduct.{u_2, v_1, u_1} (C := C) fun (k : (↑(Set.range ι)ᶜ : Type u_2)) ↦ X (↑k : I)
⊢ Mono.{v_1, u_1} (C := C) (X := sigmaObj.{u_3, v_1, u_1} (X ∘ ι)) (Y := sigmaObj.{u_2, v_1, u_1} X)
    (Sigma.desc fun (j : J) ↦ Sigma.ι X (ι j))

Tactic:
mono_of_injective' X ι hι

Premises used: CategoryTheory.Limits.MonoCoprod.mono_of_injective'
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoCoprod.{v_1, u_1} C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
inst_2 : HasCoproduct.{u_3, v_1, u_1} (X ∘ ι)
inst_3 : HasCoproduct.{u_2, v_1, u_1} X
inst_4 : HasCoproduct.{u_2, v_1, u_1} (C := C) fun (k : (↑(Set.range ι)ᶜ : Type u_2)) ↦ X (↑k : I)
h :
  Eq.{v_1 + 1} (α := sigmaObj.{u_3, v_1, u_1} (X ∘ ι) ⟶ sigmaObj.{u_2, v_1, u_1} X)
    (Sigma.map' ι fun (j : J) ↦ 𝟙 ((X ∘ ι) j)) (Sigma.desc fun (j : J) ↦ Sigma.ι X (ι j))
⊢ Mono.{v_1, u_1} (C := C) (X := sigmaObj.{u_3, v_1, u_1} (X ∘ ι)) (Y := sigmaObj.{u_2, v_1, u_1} X)
    (Sigma.map' ι fun (j : J) ↦ 𝟙 ((X ∘ ι) j))

Tactic:
convert! mono_of_injective' X ι hι

Premises used: CategoryTheory.Limits.MonoCoprod.mono_of_injective'
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoCoprod.{v_1, u_1} C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
inst_2 : HasCoproduct.{u_3, v_1, u_1} (X ∘ ι)
inst_3 : HasCoproduct.{u_2, v_1, u_1} X
inst_4 : HasCoproduct.{u_2, v_1, u_1} (C := C) fun (k : (↑(Set.range ι)ᶜ : Type u_2)) ↦ X (↑k : I)
h :
  ∀ (b : J),
    Eq.{v_1 + 1} (α := (X ∘ ι) b ⟶ sigmaObj.{u_2, v_1, u_1} X)
      (CategoryStruct.comp (Y := sigmaObj.{u_3, v_1, u_1} (X ∘ ι)) (Sigma.ι (X ∘ ι) b)
        (Sigma.map' ι fun (j : J) ↦ 𝟙 ((X ∘ ι) j)))
      (CategoryStruct.comp (Y := sigmaObj.{u_3, v_1, u_1} (X ∘ ι)) (Sigma.ι (X ∘ ι) b)
        (Sigma.desc fun (j : J) ↦ Sigma.ι X (ι j)))
⊢ Eq.{v_1 + 1} (α := sigmaObj.{u_3, v_1, u_1} (X ∘ ι) ⟶ sigmaObj.{u_2, v_1, u_1} X)
    (Sigma.map' ι fun (j : J) ↦ 𝟙 ((X ∘ ι) j)) (Sigma.desc fun (j : J) ↦ Sigma.ι X (ι j))

Tactic:
apply Sigma.hom_ext

Premises used: CategoryTheory.Limits.Sigma.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoCoprod.{v_1, u_1} C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
inst_2 : HasCoproduct.{u_3, v_1, u_1} (X ∘ ι)
inst_3 : HasCoproduct.{u_2, v_1, u_1} X
inst_4 : HasCoproduct.{u_2, v_1, u_1} (C := C) fun (k : (↑(Set.range ι)ᶜ : Type u_2)) ↦ X (↑k : I)
j : J
h :
  Eq.{v_1 + 1} (α := (X ∘ ι) j ⟶ sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X (ι j))
    (NatTrans.app (Cocone.ι (Cofan.mk (sigmaObj.{u_2, v_1, u_1} X) fun (j : J) ↦ Sigma.ι X (ι j))) { as := j })
⊢ Eq.{v_1 + 1} (α := (X ∘ ι) j ⟶ sigmaObj.{u_2, v_1, u_1} X)
    (CategoryStruct.comp (Y := sigmaObj.{u_3, v_1, u_1} (X ∘ ι)) (Sigma.ι (X ∘ ι) j)
      (Sigma.map' ι fun (j : J) ↦ 𝟙 ((X ∘ ι) j)))
    (CategoryStruct.comp (Y := sigmaObj.{u_3, v_1, u_1} (X ∘ ι)) (Sigma.ι (X ∘ ι) j)
      (Sigma.desc fun (j : J) ↦ Sigma.ι X (ι j)))

Tactic:
rw [Sigma.ι_comp_map', id_comp, colimit.ι_desc]

Premises used: CategoryTheory.Limits.colimit.ι_desc, CategoryTheory.Limits.Sigma.ι_comp_map', CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoCoprod.{v_1, u_1} C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
inst_2 : HasCoproduct.{u_3, v_1, u_1} (X ∘ ι)
inst_3 : HasCoproduct.{u_2, v_1, u_1} X
inst_4 : HasCoproduct.{u_2, v_1, u_1} (C := C) fun (k : (↑(Set.range ι)ᶜ : Type u_2)) ↦ X (↑k : I)
j : J
⊢ Eq.{v_1 + 1} (α := (X ∘ ι) j ⟶ sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X (ι j))
    (NatTrans.app (Cocone.ι (Cofan.mk (sigmaObj.{u_2, v_1, u_1} X) fun (j : J) ↦ Sigma.ι X (ι j))) { as := j })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoCoprod.{v_1, u_1} C
I : Type u_2
X : I → C
c : Cofan.{u_2, v_1, u_1} X
h : IsColimit c
i : I
inst_2 : HasCoproduct.{u_2, v_1, u_1} (C := C) fun (k : (↑(Set.range fun (x : Unit) ↦ i)ᶜ : Type u_2)) ↦ X (↑k : I)
ι : Unit → I := fun (x : Unit) ↦ i
⊢ Function.Injective ι

Tactic:
have hι : Function.Injective ι := fun _ _ _ ↦ rfl
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoCoprod.{v_1, u_1} C
I : Type u_2
X : I → C
c : Cofan.{u_2, v_1, u_1} X
h : IsColimit c
i : I
inst_2 : HasCoproduct.{u_2, v_1, u_1} (C := C) fun (k : (↑(Set.range fun (x : Unit) ↦ i)ᶜ : Type u_2)) ↦ X (↑k : I)
ι : Unit → I := fun (x : Unit) ↦ i
hι : Function.Injective ι
⊢ Mono (c.inj i)

Tactic:
mono_of_injective X ι hι c (Cofan.mk (X i) (fun _ ↦ 𝟙 _)) h
    (Cofan.IsColimit.mk _ (fun s => s.inj ()))

Premises used: CategoryTheory.Limits.Cofan.IsColimit.desc, Unit.unit, CategoryTheory.Limits.Cofan.IsColimit.mk, Function.comp, CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.MonoCoprod.mono_of_injective, CategoryTheory.Limits.Cofan.inj, CategoryTheory.Limits.Cofan.mk
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoCoprod.{v_1, u_1} C
I : Type u_2
X : I → C
c : Cofan.{u_2, v_1, u_1} X
h : IsColimit c
i : I
inst_2 : HasCoproduct.{u_2, v_1, u_1} (C := C) fun (k : (↑(Set.range fun (x : Unit) ↦ i)ᶜ : Type u_2)) ↦ X (↑k : I)
ι : Unit → I := fun (x : Unit) ↦ i
hι : Function.Injective ι
⊢ Mono (c.inj i)

Tactic:
exact mono_of_injective X ι hι c (Cofan.mk (X i) (fun _ ↦ 𝟙 _)) h
    (Cofan.IsColimit.mk _ (fun s => s.inj ()))

Premises used: Unit.unit, CategoryTheory.Limits.Cofan.IsColimit.mk, Function.comp, CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.MonoCoprod.mono_of_injective, CategoryTheory.Limits.Cofan.inj, CategoryTheory.Limits.Cofan.mk
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoCoprod.{v_1, u_1} C
I : Type u_2
X : I → C
inst_2 : HasCoproduct.{u_2, v_1, u_1} X
i : I
inst_3 : HasCoproduct.{u_2, v_1, u_1} (C := C) fun (k : (↑(Set.range fun (x : Unit) ↦ i)ᶜ : Type u_2)) ↦ X (↑k : I)
⊢ Mono.{v_1, u_1} (Y := sigmaObj.{u_2, v_1, u_1} X) (Sigma.ι X i)

Tactic:
mono_inj X _ (colimit.isColimit _) i

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.colimit, CategoryTheory.Limits.MonoCoprod.mono_inj, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : MonoCoprod.{v_2, u_2} D
inst_3 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_4 : F.ReflectsMonomorphisms
A B : C
c : BinaryCofan.{v_1, u_1} A B
h : IsColimit c
c' : BinaryCofan.{v_2, u_2} (F.obj (obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.left : Discrete WalkingPair }))
  (F.obj (obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.right : Discrete WalkingPair })) :=
  BinaryCofan.mk (F.map c.inl) (F.map c.inr)
apply : Mono (F.map c.inl)
⊢ Mono c.inl

Tactic:
apply mono_of_mono_map F

Premises used: CategoryTheory.Functor.mono_of_mono_map
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : MonoCoprod.{v_2, u_2} D
inst_3 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_4 : F.ReflectsMonomorphisms
A B : C
c : BinaryCofan.{v_1, u_1} A B
h : IsColimit c
c' : BinaryCofan.{v_2, u_2} (F.obj (obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.left : Discrete WalkingPair }))
  (F.obj (obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.right : Discrete WalkingPair })) :=
  BinaryCofan.mk (F.map c.inl) (F.map c.inr)
change : Mono c'.inl
⊢ Mono (F.map c.inl)

Tactic:
change Mono c'.inl

Premises used: CategoryTheory.Mono, CategoryTheory.Limits.BinaryCofan.inl
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : MonoCoprod.{v_2, u_2} D
inst_3 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_4 : F.ReflectsMonomorphisms
A B : C
c : BinaryCofan.{v_1, u_1} A B
h : IsColimit c
c' : BinaryCofan.{v_2, u_2} (F.obj (obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.left : Discrete WalkingPair }))
  (F.obj (obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.right : Discrete WalkingPair })) :=
  BinaryCofan.mk (F.map c.inl) (F.map c.inr)
x : IsColimit c'
⊢ Mono c'.inl

Tactic:
apply MonoCoprod.binaryCofan_inl

Premises used: CategoryTheory.Limits.MonoCoprod.binaryCofan_inl
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : MonoCoprod.{v_2, u_2} D
inst_3 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_4 : F.ReflectsMonomorphisms
A B : C
c : BinaryCofan.{v_1, u_1} A B
h : IsColimit c
c' : BinaryCofan.{v_2, u_2} (F.obj (obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.left : Discrete WalkingPair }))
  (F.obj (obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.right : Discrete WalkingPair })) :=
  BinaryCofan.mk (F.map c.inl) (F.map c.inr)
x : IsColimit (BinaryCofan.mk c.inl c.inr)
⊢ IsColimit c'

Tactic:
apply mapIsColimitOfPreservesOfIsColimit F

Premises used: CategoryTheory.Limits.mapIsColimitOfPreservesOfIsColimit
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : MonoCoprod.{v_2, u_2} D
inst_3 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_4 : F.ReflectsMonomorphisms
A B : C
c : BinaryCofan.{v_1, u_1} A B
h : IsColimit c
c' : BinaryCofan.{v_2, u_2} (F.obj (obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.left : Discrete WalkingPair }))
  (F.obj (obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.right : Discrete WalkingPair })) :=
  BinaryCofan.mk (F.map c.inl) (F.map c.inr)
x : c ≅ BinaryCofan.mk c.inl c.inr
⊢ IsColimit (BinaryCofan.mk c.inl c.inr)

Tactic:
apply IsColimit.ofIsoColimit h

Premises used: CategoryTheory.Limits.IsColimit.ofIsoColimit
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : MonoCoprod.{v_2, u_2} D
inst_3 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_4 : F.ReflectsMonomorphisms
A B : C
c : BinaryCofan.{v_1, u_1} A B
h : IsColimit c
c' : BinaryCofan.{v_2, u_2} (F.obj (obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.left : Discrete WalkingPair }))
  (F.obj (obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.right : Discrete WalkingPair })) :=
  BinaryCofan.mk (F.map c.inl) (F.map c.inr)
x : ∀ (j : Discrete WalkingPair), c.ι.app j ≫ Iso.hom (eqToIso ⋯) = (BinaryCofan.mk c.inl c.inr).ι.app j
⊢ c ≅ BinaryCofan.mk c.inl c.inr

Tactic:
refine Cocone.ext (φ := eqToIso rfl) ?_

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.eqToIso, rfl
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : MonoCoprod.{v_2, u_2} D
inst_3 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_4 : F.ReflectsMonomorphisms
A B : C
c : BinaryCofan.{v_1, u_1} A B
h : IsColimit c
c' : BinaryCofan.{v_2, u_2} (F.obj (obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.left : Discrete WalkingPair }))
  (F.obj (obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.right : Discrete WalkingPair })) :=
  BinaryCofan.mk (F.map c.inl) (F.map c.inr)
⊢ Eq (α :=
    obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.left : Discrete WalkingPair } ⟶ (BinaryCofan.mk c.inl c.inr).pt)
    (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ Iso.hom (eqToIso ⋯))
    ((BinaryCofan.mk c.inl c.inr).ι.app { as := WalkingPair.left })

Tactic:
simp only [const_obj_obj, eqToIso_refl, Iso.refl_hom,
      Category.comp_id, BinaryCofan.mk_inl, BinaryCofan.mk_inr]

Premises used: CategoryTheory.Limits.BinaryCofan.mk_inr, CategoryTheory.Limits.BinaryCofan.mk_inl, CategoryTheory.Category.comp_id, CategoryTheory.eqToIso_refl, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Iso.refl_hom
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : MonoCoprod.{v_2, u_2} D
inst_3 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_4 : F.ReflectsMonomorphisms
A B : C
c : BinaryCofan.{v_1, u_1} A B
h : IsColimit c
c' : BinaryCofan.{v_2, u_2} (F.obj (obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.left : Discrete WalkingPair }))
  (F.obj (obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.right : Discrete WalkingPair })) :=
  BinaryCofan.mk (F.map c.inl) (F.map c.inr)
⊢ Eq (α :=
    obj.{0, v_1, 0, u_1} (pair A B) { as := WalkingPair.right : Discrete WalkingPair } ⟶
      (BinaryCofan.mk c.inl c.inr).pt)
    (c.ι.app { as := WalkingPair.right : Discrete WalkingPair } ≫ Iso.hom (eqToIso ⋯))
    ((BinaryCofan.mk c.inl c.inr).ι.app { as := WalkingPair.right })

Tactic:
simp only [const_obj_obj, eqToIso_refl, Iso.refl_hom,
      Category.comp_id, BinaryCofan.mk_inl, BinaryCofan.mk_inr]

Premises used: CategoryTheory.Limits.BinaryCofan.mk_inr, CategoryTheory.Limits.BinaryCofan.mk_inl, CategoryTheory.Category.comp_id, CategoryTheory.eqToIso_refl, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Iso.refl_hom
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst_1 : (X Y : C) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} C FC (CC := CC)
inst_3 : PreservesColimitsOfShape.{0, 0, v_1, u_3, u_1, u_3 + 1} (Discrete WalkingPair) (forget C (FC := FC) (CC := CC))
inst_4 : ReflectsMonomorphisms.{v_1, u_3, u_1, u_3 + 1} (forget C (FC := FC) (CC := CC))
⊢ MonoCoprod.{v_1, u_1} C

Tactic:
monoCoprod_of_preservesCoprod_of_reflectsMono (forget C)

Premises used: CategoryTheory.forget, CategoryTheory.Limits.MonoCoprod.monoCoprod_of_preservesCoprod_of_reflectsMono
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A : C
inst_1 : HasCoproducts.{u, v_1, u_1} C
inst_2 : MonoCoprod.{v_1, u_1} C
J I : Type u
ι : J ⟶ I
hι : Mono ι
⊢ Function.Injective (α := (fun (X : Type u) ↦ X) J) (β := (fun (X : Type u) ↦ X) I)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ι) : (a : (fun (X : Type u) ↦ X) J) → (fun (X : Type u) ↦ X) I)

Tactic:
rw [mono_iff_injective] at hι

Premises used: CategoryTheory.mono_iff_injective