awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
x_1 : Cocone.{u_1, u, u_1, u + 1} (Functor.empty (Type u))
x_2 :
  Cocone.pt.{u_1, u, u_1, u + 1}
      { pt := PEmpty.{u + 1},
        ι :=
          Iso.inv (Functor.uniqueFromEmpty (Functor.obj (Functor.const (Discrete PEmpty.{u_1 + 1})) PEmpty.{u + 1})) :
        Cocone.{u_1, u, u_1, u + 1} (Functor.empty (Type u)) } ⟶
    x_1.pt
h :
  ∀ (j : Discrete PEmpty.{u_1 + 1}),
    NatTrans.app
          (Cocone.ι
            { pt := PEmpty.{u + 1},
              ι :=
                Iso.inv
                  (Functor.uniqueFromEmpty (Functor.obj (Functor.const (Discrete PEmpty.{u_1 + 1})) PEmpty.{u + 1})) })
          j ≫
        x_2 =
      x_1.ι.app j
x :
  Cocone.pt.{u_1, u, u_1, u + 1}
    { pt := PEmpty.{u + 1},
      ι := Iso.inv (Functor.uniqueFromEmpty (Functor.obj (Functor.const (Discrete PEmpty.{u_1 + 1})) PEmpty.{u + 1})) }
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) x_2).toFun x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾fun
            (x :
              Cocone.pt.{u_1, u, u_1, u + 1}
                { pt := PEmpty.{u + 1},
                  ι :=
                    Iso.inv
                      (Functor.uniqueFromEmpty
                        (Functor.obj (Functor.const (Discrete PEmpty.{u_1 + 1})) PEmpty.{u + 1})) :
                  Cocone.{u_1, u, u_1, u + 1} (Functor.empty (Type u)) }) ↦
          PEmpty.elim x))
      x

Tactic:
cases x
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
X : Type u
mp : Nonempty.{u + 2} (IsInitial X) → IsEmpty X
mpr : IsEmpty X → Nonempty.{u + 2} (IsInitial X)
⊢ Nonempty.{u + 2} (IsInitial X) ↔ IsEmpty X

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
X : Type u
h : IsInitial X
⊢ IsEmpty X

Tactic:
Function.isEmpty (IsInitial.to h PEmpty)

Premises used: Function.isEmpty, CategoryTheory.ConcreteCategory.hom, PEmpty, CategoryTheory.Limits.IsInitial.to, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
X : Type u
h : IsInitial X
⊢ IsEmpty X

Tactic:
exact Function.isEmpty (IsInitial.to h PEmpty)

Premises used: Function.isEmpty, CategoryTheory.ConcreteCategory.hom, PEmpty, CategoryTheory.Limits.IsInitial.to, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
X : Type u
h : IsEmpty X
⊢ Nonempty.{u + 2} (IsInitial X)

Tactic:
⟨IsInitial.ofIso Types.isInitialPEmpty <| Equiv.toIso <| Equiv.equivOfIsEmpty PEmpty X⟩

Premises used: Equiv.equivOfIsEmpty, CategoryTheory.Limits.Types.isInitialPEmpty, PEmpty, Equiv.toIso, Nonempty.intro, CategoryTheory.Limits.IsInitial.ofIso
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
X : Type u
h : IsEmpty X
⊢ Nonempty.{u + 2} (IsInitial X)

Tactic:
exact ⟨IsInitial.ofIso Types.isInitialPEmpty <| Equiv.toIso <| Equiv.equivOfIsEmpty PEmpty X⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
X Y : Type u
x : Cocone (pair X Y)
x_1 : (binaryCoproductCocone X Y).pt ⟶ x.pt
w : ∀ (j : Discrete WalkingPair), (binaryCoproductCocone X Y).ι.app j ≫ x_1 = x.ι.app j
h :
  ∀ (val : X),
    (ConcreteCategory.hom (FC := TypeCat.Fun) x_1).toFun (Sum.inl val) =
      TypeCat.Fun.toFun (X := (binaryCoproductCocone X Y).pt)
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾Sum.elim
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryCofan.inl x)) :
                (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
                  (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x.pt).obj { as := left }))
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryCofan.inr x)) :
                (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right })) →
                  (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x.pt).obj { as := right }))))
        (Sum.inl val)
h₁ :
  ∀ (val : Y),
    (ConcreteCategory.hom (FC := TypeCat.Fun) x_1).toFun (Sum.inr val) =
      TypeCat.Fun.toFun (X := (binaryCoproductCocone X Y).pt)
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾Sum.elim
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryCofan.inl x)) :
                (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
                  (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x.pt).obj { as := left }))
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryCofan.inr x)) :
                (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right })) →
                  (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x.pt).obj { as := right }))))
        (Sum.inr val)
⊢ x_1 =
    ↾Sum.elim
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryCofan.inl x)) :
          (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
            (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x.pt).obj { as := left }))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryCofan.inr x)) :
          (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right })) →
            (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x.pt).obj { as := right }))

Tactic:
ext ⟨⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
X Y : Type u
x : Cocone (pair X Y)
x_1 : (binaryCoproductCocone X Y).pt ⟶ x.pt
w : ∀ (j : Discrete WalkingPair), (binaryCoproductCocone X Y).ι.app j ≫ x_1 = x.ι.app j
val : X
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) x_1).toFun (Sum.inl val) =
    TypeCat.Fun.toFun (X := (binaryCoproductCocone X Y).pt)
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾Sum.elim
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryCofan.inl x)) :
              (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
                (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x.pt).obj { as := left }))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryCofan.inr x)) :
              (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right })) →
                (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x.pt).obj { as := right }))))
      (Sum.inl val)

Tactic:
ConcreteCategory.congr_hom (w ⟨left⟩) _

Premises used: CategoryTheory.Discrete.mk, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Limits.WalkingPair.left, Sum.elim
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
X Y : Type u
x : Cocone (pair X Y)
x_1 : (binaryCoproductCocone X Y).pt ⟶ x.pt
w : ∀ (j : Discrete WalkingPair), (binaryCoproductCocone X Y).ι.app j ≫ x_1 = x.ι.app j
val : Y
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) x_1).toFun (Sum.inr val) =
    TypeCat.Fun.toFun (X := (binaryCoproductCocone X Y).pt)
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾Sum.elim
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryCofan.inl x)) :
              (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
                (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x.pt).obj { as := left }))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryCofan.inr x)) :
              (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right })) →
                (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x.pt).obj { as := right }))))
      (Sum.inr val)

Tactic:
ConcreteCategory.congr_hom (w ⟨right⟩) _

Premises used: CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Discrete.mk, CategoryTheory.ConcreteCategory.congr_hom, Sum.elim
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
X Y : Type u
x : Cocone (pair X Y)
x_1 : (binaryCoproductCocone X Y).pt ⟶ x.pt
w : ∀ (j : Discrete WalkingPair), (binaryCoproductCocone X Y).ι.app j ≫ x_1 = x.ι.app j
val : X
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) x_1).toFun (Sum.inl val) =
    TypeCat.Fun.toFun (X := (binaryCoproductCocone X Y).pt)
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾Sum.elim
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryCofan.inl x)) :
              (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
                (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x.pt).obj { as := left }))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (BinaryCofan.inr x)) :
              (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right })) →
                (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj x.pt).obj { as := right }))))
      (Sum.inl val)

Tactic:
exacts [ConcreteCategory.congr_hom (w ⟨left⟩) _, ConcreteCategory.congr_hom (w ⟨right⟩) _]

Premises used: CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Discrete.mk, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
X Y : Type u
⊢ coprod.inl ≫ (binaryCoproductIso X Y).hom = ↾Sum.inl

Tactic:
colimit.isoColimitCocone_ι_hom (binaryCoproductColimitCocone X Y) ⟨WalkingPair.left⟩

Premises used: CategoryTheory.Discrete.mk, CategoryTheory.Limits.Types.binaryCoproductColimitCocone, CategoryTheory.Limits.WalkingPair.left, CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
X Y : Type u
⊢ coprod.inr ≫ (binaryCoproductIso X Y).hom = ↾Sum.inr

Tactic:
colimit.isoColimitCocone_ι_hom (binaryCoproductColimitCocone X Y) ⟨WalkingPair.right⟩

Premises used: CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Discrete.mk, CategoryTheory.Limits.Types.binaryCoproductColimitCocone, CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
X Y : Type u
⊢ ↾Sum.inl ≫ (binaryCoproductIso X Y).inv = coprod.inl

Tactic:
colimit.isoColimitCocone_ι_inv (binaryCoproductColimitCocone X Y) ⟨WalkingPair.left⟩

Premises used: CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv, CategoryTheory.Discrete.mk, CategoryTheory.Limits.Types.binaryCoproductColimitCocone, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
X Y : Type u
⊢ ↾Sum.inr ≫ (binaryCoproductIso X Y).inv = coprod.inr

Tactic:
colimit.isoColimitCocone_ι_inv (binaryCoproductColimitCocone X Y) ⟨WalkingPair.right⟩

Premises used: CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv, CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Discrete.mk, CategoryTheory.Limits.Types.binaryCoproductColimitCocone
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ Injective (α := X) (β := c.pt)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾Sum.inl ≫ (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) :
        (a : X) → c.pt) ∧
    Injective (α := Y) (β := c.pt)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾Sum.inr ≫ (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) :
          (a : Y) → c.pt) ∧
      IsCompl (α := Set c.pt)
        (Set.range (ι := X)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                (↾Sum.inl ≫ (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) :
            (a : X) → c.pt))
        (Set.range (ι := Y)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                (↾Sum.inr ≫ (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) :
            (a : Y) → c.pt))

Tactic:
⟨(h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).symm.toEquiv.injective.comp
            Sum.inl_injective,
          (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).symm.toEquiv.injective.comp
            Sum.inr_injective, ?_⟩

Premises used: Sum.inr_injective, CategoryTheory.Iso.toEquiv, Sum.inl_injective, Function.Injective.comp, And.intro, CategoryTheory.Iso.symm, Equiv.injective, CategoryTheory.Limits.Types.binaryCoproductColimit, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
mp :
  IsCompl (α := Set c.pt)
    (Set.range (ι := X)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾Sum.inl ≫ (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) :
        (a : X) → c.pt))
    (Set.range (ι := Y)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾Sum.inr ≫ (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) :
        (a : Y) → c.pt))
⊢ Injective (α := X) (β := c.pt)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾Sum.inl ≫ (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) :
        (a : X) → c.pt) ∧
    Injective (α := Y) (β := c.pt)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾Sum.inr ≫ (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) :
          (a : Y) → c.pt) ∧
      IsCompl (α := Set c.pt)
        (Set.range (ι := X)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                (↾Sum.inl ≫ (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) :
            (a : X) → c.pt))
        (Set.range (ι := Y)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
                (↾Sum.inr ≫ (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) :
            (a : Y) → c.pt))

Tactic:
refine
        ⟨(h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).symm.toEquiv.injective.comp
            Sum.inl_injective,
          (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).symm.toEquiv.injective.comp
            Sum.inr_injective, ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
mp :
  Eq (α := Set c.pt)
    (Set.image (α := (fun (X : Type u) ↦ X) (X ⊕ Y))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) :
        (a : (fun (X : Type u) ↦ X) (X ⊕ Y)) → (fun (X : Type u) ↦ X) c.pt)
      (Set.range (ι := X)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (↾Sum.inl)) :
          (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (X ⊕ Y))))
    (Set.range (ι := Y)
        (Function.comp (β := (fun (X : Type u) ↦ X) (X ⊕ Y))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) :
            (a : (fun (X : Type u) ↦ X) (X ⊕ Y)) → (fun (X : Type u) ↦ X) c.pt)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (↾Sum.inr)) :
            (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) (X ⊕ Y))))ᶜ
⊢ IsCompl (α := Set c.pt)
    (Set.range (ι := X)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾Sum.inl ≫ (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) :
        (a : X) → c.pt))
    (Set.range (ι := Y)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾Sum.inr ≫ (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)) :
        (a : Y) → c.pt))

Tactic:
rw [types_comp, Set.range_comp, ← eq_compl_iff_isCompl, types_comp]

Premises used: Set.range_comp, CategoryTheory.types_comp, eq_compl_iff_isCompl
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
mp :
  Eq (α := Set c.pt)
    (Set.image (α := X ⊕ Y)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) :
        (a : X ⊕ Y) → c.pt)
      (Set.range Sum.inl))
    (Set.range (ι := Y)
        (Function.comp (β := X ⊕ Y)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) :
            (a : X ⊕ Y) → c.pt)
          Sum.inr))ᶜ
⊢ Eq (α := Set c.pt)
    (Set.image (α := (fun (X : Type u) ↦ X) (X ⊕ Y))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) :
        (a : (fun (X : Type u) ↦ X) (X ⊕ Y)) → (fun (X : Type u) ↦ X) c.pt)
      (Set.range (ι := X)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (↾Sum.inl)) :
          (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) (X ⊕ Y))))
    (Set.range (ι := Y)
        (Function.comp (β := (fun (X : Type u) ↦ X) (X ⊕ Y))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) :
            (a : (fun (X : Type u) ↦ X) (X ⊕ Y)) → (fun (X : Type u) ↦ X) c.pt)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (↾Sum.inr)) :
            (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) (X ⊕ Y))))ᶜ

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
mp :
  Eq (α := Set c.pt)
    (Set.image (α := X ⊕ Y)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) :
        (a : X ⊕ Y) → c.pt)
      (Set.range Sum.inl))
    (Set.image (α := X ⊕ Y)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) :
        (a : X ⊕ Y) → c.pt)
      (Set.range Sum.inr)ᶜ)
⊢ Eq (α := Set c.pt)
    (Set.image (α := X ⊕ Y)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) :
        (a : X ⊕ Y) → c.pt)
      (Set.range Sum.inl))
    (Set.range (ι := Y)
        (Function.comp (β := X ⊕ Y)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) :
            (a : X ⊕ Y) → c.pt)
          Sum.inr))ᶜ

Tactic:
rw [Set.range_comp _ Sum.inr, ← dsimp% [Iso.toEquiv] Set.image_compl_eq
          (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).symm.toEquiv.bijective]

Premises used: Set.range_comp, Equiv.bijective, CategoryTheory.Iso.toEquiv, Set.image_compl_eq, Sum.inr, CategoryTheory.Iso.symm, CategoryTheory.Limits.Types.binaryCoproductColimit, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ Eq (α := Set c.pt)
    (Set.image (α := X ⊕ Y)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) :
        (a : X ⊕ Y) → c.pt)
      (Set.range Sum.inl))
    (Set.image (α := X ⊕ Y)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) :
        (a : X ⊕ Y) → c.pt)
      (Set.range Sum.inr)ᶜ)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F : C → Type v
X Y : Type u
f : X ⟶ Y
inst : Mono f
h :
  Nonempty.{u + 2}
    (IsColimit (F :=
      pair X
        { x : (fun (X : Type u) ↦ X) Y //
          Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
            (Set.range (ι := (fun (X : Type u) ↦ X) X)
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                  (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
            x })
      (BinaryCofan.mk f
        (↾Subtype.val (p := fun (x : (fun (X : Type u) ↦ X) Y) ↦
            Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
              (Set.range (ι := (fun (X : Type u) ↦ X) X)
                  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                    (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
              x))))
⊢ IsColimit (F :=
    pair X
      { x : (fun (X : Type u) ↦ X) Y //
        Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
          (Set.range (ι := (fun (X : Type u) ↦ X) X)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
          x })
    (BinaryCofan.mk f
      (↾Subtype.val (p := fun (x : (fun (X : Type u) ↦ X) Y) ↦
          Membership.mem (γ := Set ((fun (X : Type u) ↦ X) Y))
            (Set.range (ι := (fun (X : Type u) ↦ X) X)
                (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                  (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))ᶜ
            x)))

Tactic:
apply Nonempty.some

Premises used: Nonempty.some
-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F_1 : C → Type v
J : Type v
F : J → Type (max v u)
s : Cocone (Discrete.functor F)
m :
  Cocone.pt (J := Discrete J) (F := Discrete.functor F)
      { pt := (j : J) × F j,
        ι :=
          Discrete.natTrans fun (x : Discrete J) ↦
            match (motive :=
              (x : Discrete J) →
                Functor.obj (Discrete.functor F) x ⟶
                  Functor.obj (Functor.obj (Functor.const (Discrete J)) ((j : J) × F j)) x)
              x with
            | { as := j } =>
              ↾fun (x : Functor.obj (Discrete.functor F) { as := j : Discrete J }) ↦
                Sigma.mk (β := fun (j : J) ↦ F j) j x :
        Cocone (Discrete.functor F) } ⟶
    s.pt
w :
  ∀ (j : Discrete J),
    NatTrans.app
          (Cocone.ι
            { pt := (j : J) × F j,
              ι :=
                Discrete.natTrans fun (x : Discrete J) ↦
                  match (motive :=
                    (x : Discrete J) →
                      Functor.obj (Discrete.functor F) x ⟶
                        Functor.obj (Functor.obj (Functor.const (Discrete J)) ((j : J) × F j)) x)
                    x with
                  | { as := j } =>
                    ↾fun (x : Functor.obj (Discrete.functor F) { as := j : Discrete J }) ↦
                      Sigma.mk (β := fun (j : J) ↦ F j) j x })
          j ≫
        m =
      s.ι.app j
j : J
x : F j
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun (Sigma.mk (β := fun (j : J) ↦ F j) j x) =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾fun
            (x :
              Cocone.pt (J := Discrete J) (F := Discrete.functor F)
                { pt := (j : J) × F j,
                  ι :=
                    Discrete.natTrans fun (x : Discrete J) ↦
                      match (motive :=
                        (x : Discrete J) →
                          Functor.obj (Discrete.functor F) x ⟶
                            Functor.obj (Functor.obj (Functor.const (Discrete J)) ((j : J) × F j)) x)
                        x with
                      | { as := j } =>
                        ↾fun (x : Functor.obj (Discrete.functor F) { as := j : Discrete J }) ↦
                          Sigma.mk (β := fun (j : J) ↦ F j) j x :
                  Cocone (Discrete.functor F) }) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app { as := x.fst (β := fun (j : J) ↦ F j) : Discrete J }) :
              (a : (fun (X : Type (max u v)) ↦ X) ((Discrete.functor F).obj { as := x.fst })) →
                (fun (X : Type (max u v)) ↦ X) (((Functor.const (Discrete J)).obj s.pt).obj { as := x.fst }))
            (x.snd (β := fun (j : J) ↦ F j))))
      (Sigma.mk (β := fun (j : J) ↦ F j) j x)

Tactic:
ConcreteCategory.congr_hom (w ⟨j⟩) x

Premises used: CategoryTheory.Discrete.mk, CategoryTheory.ConcreteCategory.congr_hom