awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y X' : C
c : BinaryFan.{v, u} X Y
f : X ⟶ X'
inst_1 : IsIso f
h : IsLimit c
lift :
  (s : BinaryFan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })) →
    s.pt ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := left : Discrete WalkingPair }
fac_left :
  ∀ (s : BinaryFan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })),
    IsLimit.lift h (s.fst ≫ inv f) s.snd ≫ c.fst ≫ f = s.fst
fac_right :
  ∀ (s : BinaryFan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })),
    IsLimit.lift h (s.fst ≫ inv f) s.snd ≫ c.snd = s.snd
uniq :
  ∀ (s : BinaryFan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair }))
    (m :
      s.pt ⟶
        Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
          { as := left : Discrete WalkingPair }),
    m ≫ c.fst ≫ f = s.fst → m ≫ c.snd = s.snd → m = IsLimit.lift h (s.fst ≫ inv f) s.snd
⊢ IsLimit (mk (c.fst ≫ f) c.snd)

Tactic:
fapply BinaryFan.isLimitMk

Premises used: CategoryTheory.Limits.BinaryFan.isLimitMk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y X' : C
c : BinaryFan.{v, u} X Y
f : X ⟶ X'
inst_1 : IsIso f
h : IsLimit c
⊢ (s : BinaryFan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })) →
    s.pt ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := left : Discrete WalkingPair }

Tactic:
exact fun s => IsLimit.lift h (s.fst ≫ inv f) s.snd

Premises used: CategoryTheory.Limits.BinaryFan.IsLimit.lift, CategoryTheory.CategoryStruct.comp, CategoryTheory.inv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y X' : C
c : BinaryFan.{v, u} X Y
f : X ⟶ X'
inst_1 : IsIso f
h : IsLimit c
⊢ ∀ (s : BinaryFan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })),
    IsLimit.lift h (s.fst ≫ inv f) s.snd ≫ c.fst ≫ f = s.fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y X' : C
c : BinaryFan.{v, u} X Y
f : X ⟶ X'
inst_1 : IsIso f
h : IsLimit c
⊢ ∀ (s : BinaryFan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })),
    IsLimit.lift h (s.fst ≫ inv f) s.snd ≫ c.snd = s.snd

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y X' : C
c : BinaryFan.{v, u} X Y
f : X ⟶ X'
inst_1 : IsIso f
h : IsLimit c
s : BinaryFan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })
m :
  s.pt ⟶
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
      { as := left : Discrete WalkingPair }
e₁ : m ≫ c.fst ≫ f = s.fst
e₂ : m ≫ c.snd = s.snd
uniq : m ≫ c.fst = IsLimit.lift h (s.fst ≫ inv f) s.snd ≫ c.fst
uniq₁ : m ≫ c.snd = IsLimit.lift h (s.fst ≫ inv f) s.snd ≫ c.snd
⊢ m = IsLimit.lift h (s.fst ≫ inv f) s.snd

Tactic:
apply BinaryFan.IsLimit.hom_ext h

Premises used: CategoryTheory.Limits.BinaryFan.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y X' : C
c : BinaryFan.{v, u} X Y
f : X ⟶ X'
inst_1 : IsIso f
h : IsLimit c
s : BinaryFan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })
m :
  s.pt ⟶
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
      { as := left : Discrete WalkingPair }
e₁ : m ≫ c.fst ≫ f = s.fst
e₂ : m ≫ c.snd = s.snd
⊢ m ≫ c.fst = IsLimit.lift h (s.fst ≫ inv f) s.snd ≫ c.fst

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y X' : C
c : BinaryFan.{v, u} X Y
f : X ⟶ X'
inst_1 : IsIso f
h : IsLimit c
s : BinaryFan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })
m :
  s.pt ⟶
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
      { as := left : Discrete WalkingPair }
e₁ : m ≫ c.fst ≫ f = s.fst
e₂ : m ≫ c.snd = s.snd
⊢ m ≫ c.snd = IsLimit.lift h (s.fst ≫ inv f) s.snd ≫ c.snd

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsInitial.{v, u} Y
c : BinaryCofan.{v, u} X Y
mp : Nonempty (IsColimit c) → IsIso c.inl
mpr : IsIso c.inl → Nonempty (IsColimit c)
⊢ Nonempty (IsColimit c) ↔ IsIso c.inl

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsInitial.{v, u} Y
c : BinaryCofan.{v, u} X Y
H : IsColimit c
mp : ∀ (l : c.pt ⟶ X) (hl : c.inl ≫ l = 𝟙 X), IsIso c.inl
⊢ IsIso c.inl

Tactic:
obtain ⟨l, hl, -⟩ := BinaryCofan.IsColimit.desc' H (𝟙 X) (h.to X)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.IsInitial.to, CategoryTheory.Limits.BinaryCofan.IsColimit.desc'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsInitial.{v, u} Y
c : BinaryCofan.{v, u} X Y
H : IsColimit c
l : c.pt ⟶ X
hl : c.inl ≫ l = 𝟙 X
⊢ IsIso c.inl

Tactic:
⟨⟨l, hl, BinaryCofan.IsColimit.hom_ext H (?_) (h.hom_ext _ _)⟩⟩

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, CategoryTheory.Limits.BinaryCofan.IsColimit.hom_ext, And.intro, Exists.intro, CategoryTheory.IsIso.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsInitial.{v, u} Y
c : BinaryCofan.{v, u} X Y
H : IsColimit c
l : c.pt ⟶ X
hl : c.inl ≫ l = 𝟙 X
mp :
  c.inl ≫ l ≫ c.inl =
    c.inl ≫
      𝟙
        (Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
          { as := left : Discrete WalkingPair })
⊢ IsIso c.inl

Tactic:
refine ⟨⟨l, hl, BinaryCofan.IsColimit.hom_ext H (?_) (h.hom_ext _ _)⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsInitial.{v, u} Y
c : BinaryCofan.{v, u} X Y
H : IsColimit c
l : c.pt ⟶ X
hl : c.inl ≫ l = 𝟙 X
mp : c.inl ≫ l ≫ c.inl = c.inl
⊢ c.inl ≫ l ≫ c.inl =
    c.inl ≫
      𝟙
        (Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
          { as := left : Discrete WalkingPair })

Tactic:
rw [Category.comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsInitial.{v, u} Y
c : BinaryCofan.{v, u} X Y
H : IsColimit c
l : c.pt ⟶ X
hl : c.inl ≫ l = 𝟙 X
⊢ (c.inl ≫ l) ≫ c.inl = 𝟙 X ≫ c.inl

Tactic:
have e : (inl c ≫ l) ≫ inl c = 𝟙 X ≫ inl c := congrArg (· ≫ inl c) hl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsInitial.{v, u} Y
c : BinaryCofan.{v, u} X Y
H : IsColimit c
l : c.pt ⟶ X
hl : c.inl ≫ l = 𝟙 X
e : (c.inl ≫ l) ≫ c.inl = 𝟙 X ≫ c.inl
mp : ∀ (e : c.inl ≫ l ≫ c.inl = 𝟙 X ≫ c.inl), c.inl ≫ l ≫ c.inl = c.inl
mp₁ mp₂ mp₃ mp₄ : ∀ (e : c.inl ≫ l ≫ c.inl = c.inl), c.inl ≫ l ≫ c.inl = c.inl
⊢ c.inl ≫ l ≫ c.inl = c.inl

Tactic:
rwa [Category.assoc, Category.id_comp] at e

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsInitial.{v, u} Y
c : BinaryCofan.{v, u} X Y
h_1 : IsIso c.inl
⊢ Nonempty (IsColimit c)

Tactic:
⟨BinaryCofan.IsColimit.mk _ (fun f _ => inv c.inl ≫ f)
          (fun _ _ => IsIso.hom_inv_id_assoc _ _) (fun _ _ => h.hom_ext _ _) fun _ _ _ e _ =>
          (IsIso.eq_inv_comp _).mpr e⟩

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, Iff.mpr, CategoryTheory.Limits.BinaryCofan.inr, CategoryTheory.Limits.BinaryCofan.IsColimit.mk, CategoryTheory.IsIso.eq_inv_comp, Nonempty.intro, CategoryTheory.IsIso.hom_inv_id_assoc, CategoryTheory.Limits.BinaryCofan.inl, CategoryTheory.CategoryStruct.comp, CategoryTheory.inv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsInitial.{v, u} Y
c : BinaryCofan.{v, u} X Y
h_1 : IsIso c.inl
⊢ Nonempty (IsColimit c)

Tactic:
exact
      ⟨BinaryCofan.IsColimit.mk _ (fun f _ => inv c.inl ≫ f)
          (fun _ _ => IsIso.hom_inv_id_assoc _ _) (fun _ _ => h.hom_ext _ _) fun _ _ _ e _ =>
          (IsIso.eq_inv_comp _).mpr e⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsInitial.{v, u} X
c : BinaryCofan.{v, u} X Y
⊢ Nonempty (IsColimit c) ↔ IsIso c.inr

Tactic:
Iff.trans ?_ (BinaryCofan.isColimit_iff_isIso_inl h (BinaryCofan.mk c.inr c.inl))

Premises used: CategoryTheory.Limits.BinaryCofan.inr, CategoryTheory.Limits.BinaryCofan.isColimit_iff_isIso_inl, CategoryTheory.Limits.BinaryCofan.mk, CategoryTheory.Limits.BinaryCofan.inl, Iff.trans
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsInitial.{v, u} X
c : BinaryCofan.{v, u} X Y
refine : Nonempty (IsColimit c) ↔ Nonempty (IsColimit (mk c.inr c.inl))
⊢ Nonempty (IsColimit c) ↔ IsIso c.inr

Tactic:
refine Iff.trans ?_ (BinaryCofan.isColimit_iff_isIso_inl h (BinaryCofan.mk c.inr c.inl))

Premises used: CategoryTheory.Limits.BinaryCofan.inr, CategoryTheory.Limits.BinaryCofan.isColimit_iff_isIso_inl, CategoryTheory.Limits.BinaryCofan.mk, CategoryTheory.Limits.BinaryCofan.inl, Iff.trans
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsInitial.{v, u} X
c : BinaryCofan.{v, u} X Y
⊢ Nonempty (IsColimit c) ↔ Nonempty (IsColimit (mk c.inr c.inl))

Tactic:
⟨fun h => ⟨BinaryCofan.isColimitFlip h.some⟩, fun h =>
      ⟨(BinaryCofan.isColimitFlip h.some).ofIsoColimit (isoBinaryCofanMk c).symm⟩⟩

Premises used: CategoryTheory.Limits.IsColimit.ofIsoColimit, Nonempty.some, Nonempty.intro, CategoryTheory.Limits.BinaryCofan.isColimitFlip, CategoryTheory.Limits.isoBinaryCofanMk, Iff.intro, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsInitial.{v, u} X
c : BinaryCofan.{v, u} X Y
⊢ Nonempty (IsColimit c) ↔ Nonempty (IsColimit (mk c.inr c.inl))

Tactic:
exact
    ⟨fun h => ⟨BinaryCofan.isColimitFlip h.some⟩, fun h =>
      ⟨(BinaryCofan.isColimitFlip h.some).ofIsoColimit (isoBinaryCofanMk c).symm⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y X' : C
c : BinaryCofan.{v, u} X Y
f : X' ⟶ X
inst_1 : IsIso f
h : IsColimit c
desc :
  (s : BinaryCofan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })) →
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := left : Discrete WalkingPair } ⟶
      s.pt
fac_left :
  ∀ (s : BinaryCofan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })),
    (f ≫ c.inl) ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr = s.inl
fac_right :
  ∀ (s : BinaryCofan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })),
    c.inr ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr = s.inr
uniq :
  ∀ (s : BinaryCofan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair }))
    (m :
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
          { as := left : Discrete WalkingPair } ⟶
        s.pt),
    (f ≫ c.inl) ≫ m = s.inl → c.inr ≫ m = s.inr → m = IsColimit.desc h (inv f ≫ s.inl) s.inr
⊢ IsColimit (mk (f ≫ c.inl) c.inr)

Tactic:
fapply BinaryCofan.isColimitMk

Premises used: CategoryTheory.Limits.BinaryCofan.isColimitMk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y X' : C
c : BinaryCofan.{v, u} X Y
f : X' ⟶ X
inst_1 : IsIso f
h : IsColimit c
⊢ (s : BinaryCofan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })) →
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := left : Discrete WalkingPair } ⟶
      s.pt

Tactic:
exact fun s => BinaryCofan.IsColimit.desc h (inv f ≫ s.inl) s.inr

Premises used: CategoryTheory.Limits.BinaryCofan.IsColimit.desc, CategoryTheory.CategoryStruct.comp, CategoryTheory.inv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y X' : C
c : BinaryCofan.{v, u} X Y
f : X' ⟶ X
inst_1 : IsIso f
h : IsColimit c
⊢ ∀ (s : BinaryCofan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })),
    (f ≫ c.inl) ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr = s.inl

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y X' : C
c : BinaryCofan.{v, u} X Y
f : X' ⟶ X
inst_1 : IsIso f
h : IsColimit c
⊢ ∀ (s : BinaryCofan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })),
    c.inr ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr = s.inr

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y X' : C
c : BinaryCofan.{v, u} X Y
f : X' ⟶ X
inst_1 : IsIso f
h : IsColimit c
s : BinaryCofan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })
m :
  Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
      { as := left : Discrete WalkingPair } ⟶
    s.pt
e₁ : (f ≫ c.inl) ≫ m = s.inl
e₂ : c.inr ≫ m = s.inr
uniq : c.inl ≫ m = c.inl ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr
uniq₁ : c.inr ≫ m = c.inr ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr
⊢ m = IsColimit.desc h (inv f ≫ s.inl) s.inr

Tactic:
apply BinaryCofan.IsColimit.hom_ext h

Premises used: CategoryTheory.Limits.BinaryCofan.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y X' : C
c : BinaryCofan.{v, u} X Y
f : X' ⟶ X
inst_1 : IsIso f
h : IsColimit c
s : BinaryCofan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })
m :
  Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
      { as := left : Discrete WalkingPair } ⟶
    s.pt
e₁ : (f ≫ c.inl) ≫ m = s.inl
e₂ : c.inr ≫ m = s.inr
uniq : f ≫ c.inl ≫ m = f ≫ c.inl ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr
⊢ c.inl ≫ m = c.inl ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr

Tactic:
rw [← cancel_epi f]

Premises used: CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y X' : C
c : BinaryCofan.{v, u} X Y
f : X' ⟶ X
inst_1 : IsIso f
h : IsColimit c
s : BinaryCofan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })
m :
  Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
      { as := left : Discrete WalkingPair } ⟶
    s.pt
e₁ : (f ≫ c.inl) ≫ m = s.inl
e₂ : c.inr ≫ m = s.inr
⊢ f ≫ c.inl ≫ m = f ≫ c.inl ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr

Tactic:
simpa using e₁
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y X' : C
c : BinaryCofan.{v, u} X Y
f : X' ⟶ X
inst_1 : IsIso f
h : IsColimit c
s : BinaryCofan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })
m :
  Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
      { as := left : Discrete WalkingPair } ⟶
    s.pt
e₁ : (f ≫ c.inl) ≫ m = s.inl
e₂ : c.inr ≫ m = s.inr
⊢ c.inr ≫ m = c.inr ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y : C
inst_1 : HasBinaryProduct.{v, u} X Y
x : Discrete WalkingPair
u : WalkingPair
left :
  Eq (α :=
    Functor.obj.{0, v, 0, u}
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cone.pt.{0, v, 0, u} (F := pair X Y) (limit.cone (pair X Y))))
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (NatTrans.app (Cone.π (limit.cone (pair X Y))) { as := WalkingPair.left })
    (Iso.hom (Iso.refl (Cone.pt.{0, v, 0, u} (F := pair X Y) (limit.cone (pair X Y)))) ≫
      NatTrans.app (Cone.π (BinaryFan.mk (P := prod.{v, u} X Y) prod.fst prod.snd)) { as := WalkingPair.left })
right :
  Eq (α :=
    Functor.obj.{0, v, 0, u}
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cone.pt.{0, v, 0, u} (F := pair X Y) (limit.cone (pair X Y))))
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
    (NatTrans.app (Cone.π (limit.cone (pair X Y))) { as := WalkingPair.right })
    (Iso.hom (Iso.refl (Cone.pt.{0, v, 0, u} (F := pair X Y) (limit.cone (pair X Y)))) ≫
      NatTrans.app (Cone.π (BinaryFan.mk (P := prod.{v, u} X Y) prod.fst prod.snd)) { as := WalkingPair.right })
⊢ Eq (α :=
    Functor.obj.{0, v, 0, u}
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cone.pt.{0, v, 0, u} (F := pair X Y) (limit.cone (pair X Y))))
        { as := u : Discrete WalkingPair } ⟶
      Functor.obj.{0, v, 0, u} (pair X Y) { as := u : Discrete WalkingPair })
    (NatTrans.app (Cone.π (limit.cone (pair X Y))) { as := u })
    (Iso.hom (Iso.refl (Cone.pt.{0, v, 0, u} (F := pair X Y) (limit.cone (pair X Y)))) ≫
      NatTrans.app (Cone.π (BinaryFan.mk (P := prod.{v, u} X Y) prod.fst prod.snd)) { as := u })

Tactic:
cases u
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y : C
inst_1 : HasBinaryProduct.{v, u} X Y
x : Discrete WalkingPair
⊢ Eq (α :=
    Functor.obj.{0, v, 0, u}
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cone.pt.{0, v, 0, u} (F := pair X Y) (limit.cone (pair X Y))))
        { as := left : Discrete WalkingPair } ⟶
      Functor.obj.{0, v, 0, u} (pair X Y) { as := left : Discrete WalkingPair })
    (NatTrans.app (Cone.π (limit.cone (pair X Y))) { as := left })
    (Iso.hom (Iso.refl (Cone.pt.{0, v, 0, u} (F := pair X Y) (limit.cone (pair X Y)))) ≫
      NatTrans.app (Cone.π (BinaryFan.mk (P := prod.{v, u} X Y) prod.fst prod.snd)) { as := left })

Tactic:
simp [Category.id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y : C
inst_1 : HasBinaryProduct.{v, u} X Y
x : Discrete WalkingPair
⊢ Eq (α :=
    Functor.obj.{0, v, 0, u}
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cone.pt.{0, v, 0, u} (F := pair X Y) (limit.cone (pair X Y))))
        { as := right : Discrete WalkingPair } ⟶
      Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })
    (NatTrans.app (Cone.π (limit.cone (pair X Y))) { as := right })
    (Iso.hom (Iso.refl (Cone.pt.{0, v, 0, u} (F := pair X Y) (limit.cone (pair X Y)))) ≫
      NatTrans.app (Cone.π (BinaryFan.mk (P := prod.{v, u} X Y) prod.fst prod.snd)) { as := right })

Tactic:
simp [Category.id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y : C
inst_1 : HasBinaryCoproduct.{v, u} X Y
x : Discrete WalkingPair
u : WalkingPair
left :
  Eq (α :=
    Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair } ⟶
      Cocone.pt.{0, v, 0, u} (F := pair X Y) (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr))
    (NatTrans.app (Cocone.ι (colimit.cocone (pair X Y))) { as := WalkingPair.left } ≫
      Iso.hom (Iso.refl (Cocone.pt.{0, v, 0, u} (F := pair X Y) (colimit.cocone (pair X Y)))))
    (NatTrans.app (Cocone.ι (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr)) { as := WalkingPair.left })
right :
  Eq (α :=
    Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair } ⟶
      Cocone.pt.{0, v, 0, u} (F := pair X Y) (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr))
    (NatTrans.app (Cocone.ι (colimit.cocone (pair X Y))) { as := WalkingPair.right } ≫
      Iso.hom (Iso.refl (Cocone.pt.{0, v, 0, u} (F := pair X Y) (colimit.cocone (pair X Y)))))
    (NatTrans.app (Cocone.ι (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr))
      { as := WalkingPair.right })
⊢ Eq (α :=
    Functor.obj.{0, v, 0, u} (pair X Y) { as := u : Discrete WalkingPair } ⟶
      Cocone.pt.{0, v, 0, u} (F := pair X Y) (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr))
    (NatTrans.app (Cocone.ι (colimit.cocone (pair X Y))) { as := u } ≫
      Iso.hom (Iso.refl (Cocone.pt.{0, v, 0, u} (F := pair X Y) (colimit.cocone (pair X Y)))))
    (NatTrans.app (Cocone.ι (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr)) { as := u })

Tactic:
cases u
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y : C
inst_1 : HasBinaryCoproduct.{v, u} X Y
x : Discrete WalkingPair
left :
  Eq (α := X ⟶ coprod.{v, u} X Y)
    (colimit.ι (pair X Y) { as := WalkingPair.left } ≫ 𝟙 (colimit.{0, 0, v, u} (pair X Y)) : X ⟶ coprod.{v, u} X Y)
    (coprod.inl : X ⟶ coprod.{v, u} X Y)
⊢ Eq (α :=
    Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair } ⟶
      Cocone.pt.{0, v, 0, u} (F := pair X Y) (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr))
    (NatTrans.app (Cocone.ι (colimit.cocone (pair X Y))) { as := WalkingPair.left } ≫
      Iso.hom (Iso.refl (Cocone.pt.{0, v, 0, u} (F := pair X Y) (colimit.cocone (pair X Y)))))
    (NatTrans.app (Cocone.ι (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr)) { as := WalkingPair.left })

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y : C
inst_1 : HasBinaryCoproduct.{v, u} X Y
x : Discrete WalkingPair
⊢ Eq (α := X ⟶ coprod.{v, u} X Y)
    (colimit.ι (pair X Y) { as := left } ≫ 𝟙 (colimit.{0, 0, v, u} (pair X Y)) : X ⟶ coprod.{v, u} X Y)
    (coprod.inl : X ⟶ coprod.{v, u} X Y)

Tactic:
simp only [Category.comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y : C
inst_1 : HasBinaryCoproduct.{v, u} X Y
x : Discrete WalkingPair
right :
  Eq (α := Y ⟶ coprod.{v, u} X Y)
    (colimit.ι (pair X Y) { as := WalkingPair.right } ≫ 𝟙 (colimit.{0, 0, v, u} (pair X Y)) : Y ⟶ coprod.{v, u} X Y)
    (coprod.inr : Y ⟶ coprod.{v, u} X Y)
⊢ Eq (α :=
    Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair } ⟶
      Cocone.pt.{0, v, 0, u} (F := pair X Y) (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr))
    (NatTrans.app (Cocone.ι (colimit.cocone (pair X Y))) { as := WalkingPair.right } ≫
      Iso.hom (Iso.refl (Cocone.pt.{0, v, 0, u} (F := pair X Y) (colimit.cocone (pair X Y)))))
    (NatTrans.app (Cocone.ι (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr))
      { as := WalkingPair.right })

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y : C
inst_1 : HasBinaryCoproduct.{v, u} X Y
x : Discrete WalkingPair
⊢ Eq (α := Y ⟶ coprod.{v, u} X Y)
    (colimit.ι (pair X Y) { as := right } ≫ 𝟙 (colimit.{0, 0, v, u} (pair X Y)) : Y ⟶ coprod.{v, u} X Y)
    (coprod.inr : Y ⟶ coprod.{v, u} X Y)

Tactic:
simp only [Category.comp_id]

Premises used: CategoryTheory.Category.comp_id