awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B T : Type u
f₁ : A ⟶ T
f₂ : B ⟶ T
⊢ CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))))
        { as := WalkingPair.left : Discrete WalkingPair })
      (BinaryCofan.inl (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)))
      ((fun {T : Type u} (f₁ : A ⟶ T) (f₂ : B ⟶ T) ↦
          (↾fun (x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))) ↦
              Sum.casesOn (motive := fun (x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))) ↦ T) x
                (fun (x : A) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) f₁ :
                      (a : (fun (X : Type u) ↦ X) A) → (fun (X : Type u) ↦ X) T)
                    x)
                fun (x : B) ↦
                (ConcreteCategory.hom (FC := TypeCat.Fun) f₂ :
                    (a : (fun (X : Type u) ↦ X) B) → (fun (X : Type u) ↦ X) T)
                  x :
            Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ⟶ T))
        f₁ f₂) =
    f₁

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B T : Type u
f₁ : A ⟶ T
f₂ : B ⟶ T
⊢ CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))))
        { as := WalkingPair.right : Discrete WalkingPair })
      (BinaryCofan.inr (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)))
      ((fun {T : Type u} (f₁ : A ⟶ T) (f₂ : B ⟶ T) ↦
          (↾fun (x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))) ↦
              Sum.casesOn (motive := fun (x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))) ↦ T) x
                (fun (x : A) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) f₁ :
                      (a : (fun (X : Type u) ↦ X) A) → (fun (X : Type u) ↦ X) T)
                    x)
                fun (x : B) ↦
                (ConcreteCategory.hom (FC := TypeCat.Fun) f₂ :
                    (a : (fun (X : Type u) ↦ X) B) → (fun (X : Type u) ↦ X) T)
                  x :
            Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ⟶ T))
        f₁ f₂) =
    f₂

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B T : Type u
f₁ : A ⟶ T
f₂ : B ⟶ T
m : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ⟶ T
h₁ : BinaryCofan.inl (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ≫ m = f₁
h₂ : BinaryCofan.inr (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ≫ m = f₂
h :
  ∀ (x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))),
    (ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun x =
      TypeCat.Fun.toFun
        (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          ((fun {T : Type u} (f₁ : A ⟶ T) (f₂ : B ⟶ T) ↦
              (↾fun (x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))) ↦
                  Sum.casesOn (motive := fun (x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))) ↦ T)
                    x
                    (fun (x : A) ↦
                      (ConcreteCategory.hom (FC := TypeCat.Fun) f₁ :
                          (a : (fun (X : Type u) ↦ X) A) → (fun (X : Type u) ↦ X) T)
                        x)
                    fun (x : B) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun) f₂ :
                        (a : (fun (X : Type u) ↦ X) B) → (fun (X : Type u) ↦ X) T)
                      x :
                Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ⟶ T))
            f₁ f₂))
        x
⊢ m =
    (fun {T : Type u} (f₁ : A ⟶ T) (f₂ : B ⟶ T) ↦
        (↾fun (x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))) ↦
            Sum.casesOn (motive := fun (x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))) ↦ T) x
              (fun (x : A) ↦
                (ConcreteCategory.hom (FC := TypeCat.Fun) f₁ :
                    (a : (fun (X : Type u) ↦ X) A) → (fun (X : Type u) ↦ X) T)
                  x)
              fun (x : B) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) f₂ : (a : (fun (X : Type u) ↦ X) B) → (fun (X : Type u) ↦ X) T)
                x :
          Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ⟶ T))
      f₁ f₂

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B T : Type u
f₁ : A ⟶ T
f₂ : B ⟶ T
m : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ⟶ T
h₁ : BinaryCofan.inl (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ≫ m = f₁
h₂ : BinaryCofan.inr (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ≫ m = f₂
x : A
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun (Sum.inl x) =
    TypeCat.Fun.toFun (X := Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)))
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        ((fun {T : Type u} (f₁ : A ⟶ T) (f₂ : B ⟶ T) ↦
            (↾fun (x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))) ↦
                Sum.casesOn (motive := fun (x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))) ↦ T) x
                  (fun (x : A) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun) f₁ :
                        (a : (fun (X : Type u) ↦ X) A) → (fun (X : Type u) ↦ X) T)
                      x)
                  fun (x : B) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) f₂ :
                      (a : (fun (X : Type u) ↦ X) B) → (fun (X : Type u) ↦ X) T)
                    x :
              Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ⟶ T))
          f₁ f₂))
      (Sum.inl x)

Tactic:
ConcreteCategory.congr_hom h₁ x

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B T : Type u
f₁ : A ⟶ T
f₂ : B ⟶ T
m : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ⟶ T
h₁ : BinaryCofan.inl (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ≫ m = f₁
h₂ : BinaryCofan.inr (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ≫ m = f₂
x : A
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun (Sum.inl x) =
    TypeCat.Fun.toFun (X := Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)))
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        ((fun {T : Type u} (f₁ : A ⟶ T) (f₂ : B ⟶ T) ↦
            (↾fun (x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))) ↦
                Sum.casesOn (motive := fun (x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))) ↦ T) x
                  (fun (x : A) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun) f₁ :
                        (a : (fun (X : Type u) ↦ X) A) → (fun (X : Type u) ↦ X) T)
                      x)
                  fun (x : B) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) f₂ :
                      (a : (fun (X : Type u) ↦ X) B) → (fun (X : Type u) ↦ X) T)
                    x :
              Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ⟶ T))
          f₁ f₂))
      (Sum.inl x)

Tactic:
exact ConcreteCategory.congr_hom h₁ x

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B T : Type u
f₁ : A ⟶ T
f₂ : B ⟶ T
m : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ⟶ T
h₁ : BinaryCofan.inl (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ≫ m = f₁
h₂ : BinaryCofan.inr (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ≫ m = f₂
x : B
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun (Sum.inr x) =
    TypeCat.Fun.toFun (X := Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)))
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        ((fun {T : Type u} (f₁ : A ⟶ T) (f₂ : B ⟶ T) ↦
            (↾fun (x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))) ↦
                Sum.casesOn (motive := fun (x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))) ↦ T) x
                  (fun (x : A) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun) f₁ :
                        (a : (fun (X : Type u) ↦ X) A) → (fun (X : Type u) ↦ X) T)
                      x)
                  fun (x : B) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) f₂ :
                      (a : (fun (X : Type u) ↦ X) B) → (fun (X : Type u) ↦ X) T)
                    x :
              Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ⟶ T))
          f₁ f₂))
      (Sum.inr x)

Tactic:
ConcreteCategory.congr_hom h₂ x

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B T : Type u
f₁ : A ⟶ T
f₂ : B ⟶ T
m : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ⟶ T
h₁ : BinaryCofan.inl (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ≫ m = f₁
h₂ : BinaryCofan.inr (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ≫ m = f₂
x : B
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun (Sum.inr x) =
    TypeCat.Fun.toFun (X := Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)))
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        ((fun {T : Type u} (f₁ : A ⟶ T) (f₂ : B ⟶ T) ↦
            (↾fun (x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))) ↦
                Sum.casesOn (motive := fun (x : Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))) ↦ T) x
                  (fun (x : A) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun) f₁ :
                        (a : (fun (X : Type u) ↦ X) A) → (fun (X : Type u) ↦ X) T)
                      x)
                  fun (x : B) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) f₂ :
                      (a : (fun (X : Type u) ↦ X) B) → (fun (X : Type u) ↦ X) T)
                    x :
              Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)) ⟶ T))
          f₁ f₂))
      (Sum.inr x)

Tactic:
exact ConcreteCategory.congr_hom h₂ x

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : Type u
⊢ IsColimit (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))

Tactic:
exact BinaryCofan.IsColimit.mk _
        (fun f₁ f₂ => ↾fun x => by
          rcases x with x | x
          exacts [f₁ x, f₂ x])
        (fun f₁ f₂ => by rfl)
        (fun f₁ f₂ => by rfl)
        (fun f₁ f₂ m h₁ h₂ => by
          ext x
          rcases x with x | x
          · exact ConcreteCategory.congr_hom h₁ x
          · exact ConcreteCategory.congr_hom h₂ x)

Premises used: CategoryTheory.Limits.BinaryCofan.IsColimit.mk, TypeCat.ofHom
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : Type u
refine_2 :
  Function.Injective (α :=
    (fun (X : Type u) ↦ X) (Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair })) (β :=
    (fun (X : Type u) ↦ X)
      (Functor.obj
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))))
        { as := WalkingPair.left : Discrete WalkingPair }))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryCofan.inl (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)))) :
      (a : (fun (X : Type u) ↦ X) ((pair A B).obj { as := WalkingPair.left })) →
        (fun (X : Type u) ↦ X)
          (((Functor.const (Discrete WalkingPair)).obj (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)).pt).obj
            { as := WalkingPair.left }))
⊢ Mono.{u, u + 1} (X := Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) (Y :=
    Functor.obj
      (Functor.obj (Functor.const (Discrete WalkingPair))
        (Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))))
      { as := WalkingPair.left : Discrete WalkingPair })
    (BinaryCofan.inl (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)))

Tactic:
rw [mono_iff_injective]

Premises used: CategoryTheory.mono_iff_injective
-- Module: Mathlib.CategoryTheory.Limits.MonoCoprod
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : Type u
a₁ a₂ : Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }
h :
  Eq (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))))
        { as := WalkingPair.left : Discrete WalkingPair }))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryCofan.inl (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))) :
          (a : (fun (X : Type u) ↦ X) ((pair A B).obj { as := WalkingPair.left })) →
            (fun (X : Type u) ↦ X)
              (((Functor.const (Discrete WalkingPair)).obj (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)).pt).obj
                { as := WalkingPair.left }))
        a₁ :
      (fun (X : Type u) ↦ X)
        (Functor.obj
          (Functor.obj (Functor.const (Discrete WalkingPair))
            (Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))))
          { as := WalkingPair.left : Discrete WalkingPair }))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryCofan.inl (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))) :
          (a : (fun (X : Type u) ↦ X) ((pair A B).obj { as := WalkingPair.left })) →
            (fun (X : Type u) ↦ X)
              (((Functor.const (Discrete WalkingPair)).obj (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr)).pt).obj
                { as := WalkingPair.left }))
        a₂ :
      (fun (X : Type u) ↦ X)
        (Functor.obj
          (Functor.obj (Functor.const (Discrete WalkingPair))
            (Cocone.pt (F := pair A B) (BinaryCofan.mk (↾Sum.inl) (↾Sum.inr))))
          { as := WalkingPair.left : Discrete WalkingPair }))
⊢ a₁ = a₂

Tactic:
simpa using h
-- 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₂
T : C
f₁ : c₁.pt ⟶ T
f₂ : c₂.pt ⟶ T
⊢ ∀ (i : I₁),
    c₁.inj i ≫
        (binaryCofanSum c c₁ c₂ hc₁ hc₂).inl ≫
          (fun {T : C} (f₁ : c₁.pt ⟶ T) (f₂ : c₂.pt ⟶ T) ↦
              (Cofan.IsColimit.desc hc fun (i : I₁ ⊕ I₂) ↦
                  match (motive := (i : I₁ ⊕ I₂) → X i ⟶ T) i with
                  | Sum.inl i₁ => c₁.inj i₁ ≫ f₁
                  | Sum.inr i₂ => c₂.inj i₂ ≫ f₂ :
                c.pt ⟶ T))
            f₁ f₂ =
      c₁.inj i ≫ f₁

Tactic:
simp
-- 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₂
T : C
f₁ : c₁.pt ⟶ T
f₂ : c₂.pt ⟶ T
⊢ ∀ (i : I₂),
    c₂.inj i ≫
        (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr ≫
          (fun {T : C} (f₁ : c₁.pt ⟶ T) (f₂ : c₂.pt ⟶ T) ↦
              (Cofan.IsColimit.desc hc fun (i : I₁ ⊕ I₂) ↦
                  match (motive := (i : I₁ ⊕ I₂) → X i ⟶ T) i with
                  | Sum.inl i₁ => c₁.inj i₁ ≫ f₁
                  | Sum.inr i₂ => c₂.inj i₂ ≫ f₂ :
                c.pt ⟶ T))
            f₁ f₂ =
      c₂.inj i ≫ f₂

Tactic:
simp
-- 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₂
T : C
f₁ : c₁.pt ⟶ T
f₂ : c₂.pt ⟶ T
m : (binaryCofanSum c c₁ c₂ hc₁ hc₂).pt ⟶ T
hm₁ : (binaryCofanSum c c₁ c₂ hc₁ hc₂).inl ≫ m = f₁
hm₂ : (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr ≫ m = f₂
h :
  ∀ (i : I₁ ⊕ I₂),
    c.inj i ≫ m =
      c.inj i ≫
        (fun {T : C} (f₁ : c₁.pt ⟶ T) (f₂ : c₂.pt ⟶ T) ↦
            (Cofan.IsColimit.desc hc fun (i : I₁ ⊕ I₂) ↦
                match (motive := (i : I₁ ⊕ I₂) → X i ⟶ T) i with
                | Sum.inl i₁ => c₁.inj i₁ ≫ f₁
                | Sum.inr i₂ => c₂.inj i₂ ≫ f₂ :
              c.pt ⟶ T))
          f₁ f₂
⊢ m =
    (fun {T : C} (f₁ : c₁.pt ⟶ T) (f₂ : c₂.pt ⟶ T) ↦
        (Cofan.IsColimit.desc hc fun (i : I₁ ⊕ I₂) ↦
            match (motive := (i : I₁ ⊕ I₂) → X i ⟶ T) i with
            | Sum.inl i₁ => c₁.inj i₁ ≫ f₁
            | Sum.inr i₂ => c₂.inj i₂ ≫ f₂ :
          c.pt ⟶ T))
      f₁ f₂

Tactic:
apply Cofan.IsColimit.hom_ext hc

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
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
⊢ Mono (binaryCofanSum c c₁ c₂ hc₁ hc₂).inl

Tactic:
MonoCoprod.binaryCofan_inl _ (isColimitBinaryCofanSum c c₁ c₂ hc hc₁ hc₂)

Premises used: CategoryTheory.Limits.MonoCoprod.binaryCofan_inl, CategoryTheory.Limits.MonoCoprod.isColimitBinaryCofanSum
-- 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
⊢ Mono (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr

Tactic:
MonoCoprod.binaryCofan_inr _ (isColimitBinaryCofanSum c c₁ c₂ hc hc₁ hc₂)

Premises used: CategoryTheory.Limits.MonoCoprod.isColimitBinaryCofanSum, CategoryTheory.Limits.MonoCoprod.binaryCofan_inr
-- 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
inl : c₁.pt ⟶ c.pt
hinl : ∀ (i₁ : I₁), c₁.inj i₁ ≫ inl = c.inj (Sum.inl i₁)
this : inl = (binaryCofanSum c c₁ c₂ hc₁ hc₂).inl
rw : Mono (binaryCofanSum c c₁ c₂ hc₁ hc₂).inl
⊢ Mono inl

Tactic:
rw [this]
-- 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
inl : c₁.pt ⟶ c.pt
hinl : ∀ (i₁ : I₁), c₁.inj i₁ ≫ inl = c.inj (Sum.inl i₁)
this : inl = (binaryCofanSum c c₁ c₂ hc₁ hc₂).inl
⊢ Mono (binaryCofanSum c c₁ c₂ hc₁ hc₂).inl

Tactic:
MonoCoprod.binaryCofan_inl _ (isColimitBinaryCofanSum c c₁ c₂ hc hc₁ hc₂)

Premises used: CategoryTheory.Limits.MonoCoprod.binaryCofan_inl, CategoryTheory.Discrete.functor, CategoryTheory.Limits.pair, CategoryTheory.Limits.MonoCoprod.isColimitBinaryCofanSum
-- 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
inl : c₁.pt ⟶ c.pt
hinl : ∀ (i₁ : I₁), c₁.inj i₁ ≫ inl = c.inj (Sum.inl i₁)
this : inl = (binaryCofanSum c c₁ c₂ hc₁ hc₂).inl
⊢ Mono (binaryCofanSum c c₁ c₂ hc₁ hc₂).inl

Tactic:
exact MonoCoprod.binaryCofan_inl _ (isColimitBinaryCofanSum c c₁ c₂ hc hc₁ hc₂)

Premises used: CategoryTheory.Limits.MonoCoprod.binaryCofan_inl, CategoryTheory.Limits.MonoCoprod.isColimitBinaryCofanSum
-- 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
inl : c₁.pt ⟶ c.pt
hinl : ∀ (i₁ : I₁), c₁.inj i₁ ≫ inl = c.inj (Sum.inl i₁)
suffices : inl = (binaryCofanSum c c₁ c₂ hc₁ hc₂).inl
⊢ Mono inl

Tactic:
suffices inl = (binaryCofanSum c c₁ c₂ hc₁ hc₂).inl by
    rw [this]
    exact MonoCoprod.binaryCofan_inl _ (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
inl : c₁.pt ⟶ c.pt
hinl : ∀ (i₁ : I₁), c₁.inj i₁ ≫ inl = c.inj (Sum.inl i₁)
⊢ ∀ (i : I₁), c₁.inj i ≫ inl = c₁.inj i ≫ (binaryCofanSum c c₁ c₂ hc₁ hc₂).inl

Tactic:
simpa using hinl
-- 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
inl : c₁.pt ⟶ c.pt
hinl : ∀ (i₁ : I₁), c₁.inj i₁ ≫ inl = c.inj (Sum.inl i₁)
⊢ inl = (binaryCofanSum c c₁ c₂ hc₁ hc₂).inl

Tactic:
exact Cofan.IsColimit.hom_ext hc₁ _ _ (by simpa using hinl)

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
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₂)
this : inr = (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr
rw : Mono (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr
⊢ Mono inr

Tactic:
rw [this]
-- 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₂)
this : inr = (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr
⊢ Mono (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr

Tactic:
MonoCoprod.binaryCofan_inr _ (isColimitBinaryCofanSum c c₁ c₂ hc hc₁ hc₂)

Premises used: CategoryTheory.Discrete.functor, CategoryTheory.Limits.pair, CategoryTheory.Limits.MonoCoprod.isColimitBinaryCofanSum, CategoryTheory.Limits.MonoCoprod.binaryCofan_inr
-- 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₂)
this : inr = (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr
⊢ Mono (binaryCofanSum c c₁ c₂ hc₁ hc₂).inr

Tactic:
exact MonoCoprod.binaryCofan_inr _ (isColimitBinaryCofanSum c c₁ c₂ hc hc₁ hc₂)

Premises used: CategoryTheory.Limits.MonoCoprod.isColimitBinaryCofanSum, CategoryTheory.Limits.MonoCoprod.binaryCofan_inr