awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F_1 : CategoryTheory.Functor.{v, v', u, u'} C D
F : CategoryTheory.Functor.{0, v, 0, u} (Discrete WalkingPair) C
c : Cocone F
X : C
hX : IsInitial.{v, u} X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc :
  IsColimit (F := span f g)
    (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair }) (c.ι.app { as := WalkingPair.right })
        ⋯ :
      PushoutCocone f g)
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), c.ι.app j ≫ m = s.ι.app j
c' : PushoutCocone f g :=
  PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
    (c.ι.app { as := WalkingPair.right } ≫ m) ⋯
rw :
  m =
    hc.desc
      (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
        (c.ι.app { as := WalkingPair.right } ≫ m) ⋯)
⊢ m =
    hc.desc
      (PushoutCocone.mk (s.ι.app { as := WalkingPair.left : Discrete WalkingPair })
        (s.ι.app { as := WalkingPair.right }) ⋯)

Tactic:
rw [← J, ← J]
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F_1 : CategoryTheory.Functor.{v, v', u, u'} C D
F : CategoryTheory.Functor.{0, v, 0, u} (Discrete WalkingPair) C
c : Cocone F
X : C
hX : IsInitial.{v, u} X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc :
  IsColimit (F := span f g)
    (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair }) (c.ι.app { as := WalkingPair.right })
        ⋯ :
      PushoutCocone f g)
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), c.ι.app j ≫ m = s.ι.app j
c' : PushoutCocone f g :=
  PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
    (c.ι.app { as := WalkingPair.right } ≫ m) ⋯
apply :
  ∀ (j : WalkingSpan),
    Eq (α := (span f g).obj j ⟶ s.pt)
      (NatTrans.app
            (Cocone.ι
              (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair })
                (c.ι.app { as := WalkingPair.right }) ⋯))
            j ≫
          m :
        (span f g).obj j ⟶ s.pt)
      (CategoryStruct.comp (Y :=
          Functor.obj.{0, v, 0, u}
            (Functor.obj (Functor.const WalkingSpan)
              (Cocone.pt (F := span f g)
                (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair })
                    (c.ι.app { as := WalkingPair.right : Discrete WalkingPair }) ⋯ :
                  PushoutCocone f g)))
            j)
          (NatTrans.app
            (Cocone.ι
              (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair })
                (c.ι.app { as := WalkingPair.right }) ⋯))
            j)
          (hc.desc
            (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
              (c.ι.app { as := WalkingPair.right } ≫ m) ⋯)) :
        (span f g).obj j ⟶ s.pt)
⊢ m =
    hc.desc
      (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
        (c.ι.app { as := WalkingPair.right } ≫ m) ⋯)

Tactic:
apply hc.hom_ext

Premises used: CategoryTheory.Limits.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F_1 : CategoryTheory.Functor.{v, v', u, u'} C D
F : CategoryTheory.Functor.{0, v, 0, u} (Discrete WalkingPair) C
c : Cocone F
X : C
hX : IsInitial.{v, u} X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc :
  IsColimit (F := span f g)
    (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair }) (c.ι.app { as := WalkingPair.right })
        ⋯ :
      PushoutCocone f g)
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), c.ι.app j ≫ m = s.ι.app j
c' : PushoutCocone f g :=
  PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
    (c.ι.app { as := WalkingPair.right } ≫ m) ⋯
none :
  f ≫ c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m =
    f ≫
      c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫
        hc.desc
          (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
            (c.ι.app { as := WalkingPair.right } ≫ m) ⋯)
⊢ Eq (α := (span f g).obj Option.none ⟶ s.pt)
    (NatTrans.app
          (Cocone.ι
            (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair })
              (c.ι.app { as := WalkingPair.right }) ⋯))
          Option.none ≫
        m :
      (span f g).obj Option.none ⟶ s.pt)
    (CategoryStruct.comp (Y :=
        Functor.obj.{0, v, 0, u}
          (Functor.obj (Functor.const WalkingSpan)
            (Cocone.pt (F := span f g)
              (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair })
                  (c.ι.app { as := WalkingPair.right : Discrete WalkingPair }) ⋯ :
                PushoutCocone f g)))
          Option.none)
        (NatTrans.app
          (Cocone.ι
            (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair })
              (c.ι.app { as := WalkingPair.right }) ⋯))
          Option.none)
        (hc.desc
          (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
            (c.ι.app { as := WalkingPair.right } ≫ m) ⋯)) :
      (span f g).obj Option.none ⟶ s.pt)

Tactic:
simp only [PushoutCocone.mk_ι_app, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PushoutCocone.mk_ι_app
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F_1 : CategoryTheory.Functor.{v, v', u, u'} C D
F : CategoryTheory.Functor.{0, v, 0, u} (Discrete WalkingPair) C
c : Cocone F
X : C
hX : IsInitial.{v, u} X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc :
  IsColimit (F := span f g)
    (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair }) (c.ι.app { as := WalkingPair.right })
        ⋯ :
      PushoutCocone f g)
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), c.ι.app j ≫ m = s.ι.app j
c' : PushoutCocone f g :=
  PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
    (c.ι.app { as := WalkingPair.right } ≫ m) ⋯
some :
  Eq (α := (span f g).obj (Option.some WalkingPair.left) ⟶ s.pt) (c.ι.app { as := WalkingPair.left } ≫ m)
    (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫
      hc.desc
        (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
          (c.ι.app { as := WalkingPair.right } ≫ m) ⋯))
⊢ Eq (α := (span f g).obj (Option.some WalkingPair.left) ⟶ s.pt)
    (NatTrans.app
          (Cocone.ι
            (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair })
              (c.ι.app { as := WalkingPair.right }) ⋯))
          (Option.some WalkingPair.left) ≫
        m :
      (span f g).obj (Option.some WalkingPair.left) ⟶ s.pt)
    (CategoryStruct.comp (Y :=
        Functor.obj.{0, v, 0, u}
          (Functor.obj (Functor.const WalkingSpan)
            (Cocone.pt (F := span f g)
              (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair })
                  (c.ι.app { as := WalkingPair.right : Discrete WalkingPair }) ⋯ :
                PushoutCocone f g)))
          (Option.some WalkingPair.left))
        (NatTrans.app
          (Cocone.ι
            (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair })
              (c.ι.app { as := WalkingPair.right }) ⋯))
          (Option.some WalkingPair.left))
        (hc.desc
          (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
            (c.ι.app { as := WalkingPair.right } ≫ m) ⋯)) :
      (span f g).obj (Option.some WalkingPair.left) ⟶ s.pt)

Tactic:
simp only [PushoutCocone.mk_ι_app, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PushoutCocone.mk_ι_app
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F_1 : CategoryTheory.Functor.{v, v', u, u'} C D
F : CategoryTheory.Functor.{0, v, 0, u} (Discrete WalkingPair) C
c : Cocone F
X : C
hX : IsInitial.{v, u} X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc :
  IsColimit (F := span f g)
    (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair }) (c.ι.app { as := WalkingPair.right })
        ⋯ :
      PushoutCocone f g)
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), c.ι.app j ≫ m = s.ι.app j
c' : PushoutCocone f g :=
  PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
    (c.ι.app { as := WalkingPair.right } ≫ m) ⋯
some :
  Eq (α := (span f g).obj (Option.some WalkingPair.right) ⟶ s.pt) (c.ι.app { as := WalkingPair.right } ≫ m)
    (c.ι.app { as := WalkingPair.right : Discrete WalkingPair } ≫
      hc.desc
        (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
          (c.ι.app { as := WalkingPair.right } ≫ m) ⋯))
⊢ Eq (α := (span f g).obj (Option.some WalkingPair.right) ⟶ s.pt)
    (NatTrans.app
          (Cocone.ι
            (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair })
              (c.ι.app { as := WalkingPair.right }) ⋯))
          (Option.some WalkingPair.right) ≫
        m :
      (span f g).obj (Option.some WalkingPair.right) ⟶ s.pt)
    (CategoryStruct.comp (Y :=
        Functor.obj.{0, v, 0, u}
          (Functor.obj (Functor.const WalkingSpan)
            (Cocone.pt (F := span f g)
              (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair })
                  (c.ι.app { as := WalkingPair.right : Discrete WalkingPair }) ⋯ :
                PushoutCocone f g)))
          (Option.some WalkingPair.right))
        (NatTrans.app
          (Cocone.ι
            (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair })
              (c.ι.app { as := WalkingPair.right }) ⋯))
          (Option.some WalkingPair.right))
        (hc.desc
          (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
            (c.ι.app { as := WalkingPair.right } ≫ m) ⋯)) :
      (span f g).obj (Option.some WalkingPair.right) ⟶ s.pt)

Tactic:
simp only [PushoutCocone.mk_ι_app, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PushoutCocone.mk_ι_app
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F_1 : CategoryTheory.Functor.{v, v', u, u'} C D
F : CategoryTheory.Functor.{0, v, 0, u} (Discrete WalkingPair) C
c : Cocone F
X : C
hX : IsInitial.{v, u} X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc :
  IsColimit (F := span f g)
    (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair }) (c.ι.app { as := WalkingPair.right })
        ⋯ :
      PushoutCocone f g)
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), c.ι.app j ≫ m = s.ι.app j
c' : PushoutCocone f g :=
  PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
    (c.ι.app { as := WalkingPair.right } ≫ m) ⋯
none :
  Eq (α := F.obj { as := WalkingPair.left : Discrete WalkingPair } ⟶ s.pt) (c.ι.app { as := WalkingPair.left } ≫ m)
    (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫
      hc.desc
        (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
          (c.ι.app { as := WalkingPair.right } ≫ m) ⋯))
⊢ f ≫ c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m =
    f ≫
      c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫
        hc.desc
          (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
            (c.ι.app { as := WalkingPair.right } ≫ m) ⋯)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F_1 : CategoryTheory.Functor.{v, v', u, u'} C D
F : CategoryTheory.Functor.{0, v, 0, u} (Discrete WalkingPair) C
c : Cocone F
X : C
hX : IsInitial.{v, u} X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc :
  IsColimit (F := span f g)
    (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair }) (c.ι.app { as := WalkingPair.right })
        ⋯ :
      PushoutCocone f g)
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), c.ι.app j ≫ m = s.ι.app j
c' : PushoutCocone f g :=
  PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
    (c.ι.app { as := WalkingPair.right } ≫ m) ⋯
none :
  Eq (α := F.obj { as := WalkingPair.left : Discrete WalkingPair } ⟶ s.pt) (c.ι.app { as := WalkingPair.left } ≫ m)
    (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫
      hc.desc
        (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
          (c.ι.app { as := WalkingPair.right } ≫ m) ⋯))
⊢ f ≫ c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m =
    f ≫
      c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫
        hc.desc
          (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
            (c.ι.app { as := WalkingPair.right } ≫ m) ⋯)

Tactic:
on_goal 1 => congr 1
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F_1 : CategoryTheory.Functor.{v, v', u, u'} C D
F : CategoryTheory.Functor.{0, v, 0, u} (Discrete WalkingPair) C
c : Cocone F
X : C
hX : IsInitial.{v, u} X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc :
  IsColimit (F := span f g)
    (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair }) (c.ι.app { as := WalkingPair.right })
        ⋯ :
      PushoutCocone f g)
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), c.ι.app j ≫ m = s.ι.app j
c' : PushoutCocone f g :=
  PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
    (c.ι.app { as := WalkingPair.right } ≫ m) ⋯
⊢ Eq (α := F.obj { as := WalkingPair.left : Discrete WalkingPair } ⟶ s.pt) (c.ι.app { as := WalkingPair.left } ≫ m)
    (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫
      hc.desc
        (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
          (c.ι.app { as := WalkingPair.right } ≫ m) ⋯))

Tactic:
(hc.fac c' WalkingSpan.left).symm

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.WalkingSpan.left, CategoryTheory.Limits.WidePushoutShape.wideSpan, Eq.symm, CategoryTheory.Limits.span, CategoryTheory.Limits.WidePushoutShape
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F_1 : CategoryTheory.Functor.{v, v', u, u'} C D
F : CategoryTheory.Functor.{0, v, 0, u} (Discrete WalkingPair) C
c : Cocone F
X : C
hX : IsInitial.{v, u} X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc :
  IsColimit (F := span f g)
    (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair }) (c.ι.app { as := WalkingPair.right })
        ⋯ :
      PushoutCocone f g)
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), c.ι.app j ≫ m = s.ι.app j
c' : PushoutCocone f g :=
  PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
    (c.ι.app { as := WalkingPair.right } ≫ m) ⋯
⊢ Eq (α := (span f g).obj (some WalkingPair.left) ⟶ s.pt) (c.ι.app { as := WalkingPair.left } ≫ m)
    (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫
      hc.desc
        (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
          (c.ι.app { as := WalkingPair.right } ≫ m) ⋯))

Tactic:
(hc.fac c' WalkingSpan.left).symm

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.WalkingSpan.left, CategoryTheory.Limits.WidePushoutShape.wideSpan, Eq.symm, CategoryTheory.Limits.span, CategoryTheory.Limits.WidePushoutShape
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F_1 : CategoryTheory.Functor.{v, v', u, u'} C D
F : CategoryTheory.Functor.{0, v, 0, u} (Discrete WalkingPair) C
c : Cocone F
X : C
hX : IsInitial.{v, u} X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc :
  IsColimit (F := span f g)
    (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair }) (c.ι.app { as := WalkingPair.right })
        ⋯ :
      PushoutCocone f g)
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), c.ι.app j ≫ m = s.ι.app j
c' : PushoutCocone f g :=
  PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
    (c.ι.app { as := WalkingPair.right } ≫ m) ⋯
⊢ Eq (α := (span f g).obj (some WalkingPair.right) ⟶ s.pt) (c.ι.app { as := WalkingPair.right } ≫ m)
    (c.ι.app { as := WalkingPair.right : Discrete WalkingPair } ≫
      hc.desc
        (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
          (c.ι.app { as := WalkingPair.right } ≫ m) ⋯))

Tactic:
(hc.fac c' WalkingSpan.right).symm

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.WidePushoutShape.wideSpan, CategoryTheory.Limits.WalkingSpan.right, Eq.symm, CategoryTheory.Limits.span, CategoryTheory.Limits.WidePushoutShape
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F_1 : CategoryTheory.Functor.{v, v', u, u'} C D
F : CategoryTheory.Functor.{0, v, 0, u} (Discrete WalkingPair) C
c : Cocone F
X : C
hX : IsInitial.{v, u} X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc :
  IsColimit (F := span f g)
    (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair }) (c.ι.app { as := WalkingPair.right })
        ⋯ :
      PushoutCocone f g)
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), c.ι.app j ≫ m = s.ι.app j
c' : PushoutCocone f g :=
  PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
    (c.ι.app { as := WalkingPair.right } ≫ m) ⋯
⊢ Eq (α := F.obj { as := WalkingPair.left : Discrete WalkingPair } ⟶ s.pt) (c.ι.app { as := WalkingPair.left } ≫ m)
    (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫
      hc.desc
        (PushoutCocone.mk (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ m)
          (c.ι.app { as := WalkingPair.right } ≫ m) ⋯))

Tactic:
exacts [(hc.fac c' WalkingSpan.left).symm, (hc.fac c' WalkingSpan.left).symm,
      (hc.fac c' WalkingSpan.right).symm]

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.WalkingSpan.left, CategoryTheory.Limits.WalkingSpan.right, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : CategoryTheory.Functor.{v, v', u, u'} C D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial.{v, u} W
H₂ : IsColimit (F := span h k) (PushoutCocone.mk f g ⋯)
hc :
  IsColimit (F := span h k)
    (PushoutCocone.mk ((BinaryCofan.mk f g).ι.app { as := WalkingPair.left : Discrete WalkingPair })
        ((BinaryCofan.mk f g).ι.app { as := WalkingPair.right }) ⋯ :
      PushoutCocone h k)
f₁ : W ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }
g₁ : W ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }
⊢ IsColimit (BinaryCofan.mk f g)

Tactic:
apply isBinaryCoproductOfIsInitialIsPushout _ _ H₁

Premises used: isBinaryCoproductOfIsInitialIsPushout
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : CategoryTheory.Functor.{v, v', u, u'} C D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial.{v, u} W
H₂ : IsColimit (BinaryCofan.mk f g)
create :
  (s : PushoutCocone h k) →
    { l : Cocone.pt (F := span h k) (PushoutCocone.mk f g ⋯) ⟶ s.pt //
      PushoutCocone.inl (PushoutCocone.mk f g ⋯) ≫ l = s.inl ∧
        PushoutCocone.inr (PushoutCocone.mk f g ⋯) ≫ l = s.inr ∧
          ∀ {m : Cocone.pt (F := span h k) (PushoutCocone.mk f g ⋯) ⟶ s.pt},
            PushoutCocone.inl (PushoutCocone.mk f g ⋯) ≫ m = s.inl →
              PushoutCocone.inr (PushoutCocone.mk f g ⋯) ≫ m = s.inr → m = l }
⊢ IsColimit (F := span h k) (PushoutCocone.mk f g ⋯)

Tactic:
apply PushoutCocone.isColimitAux'

Premises used: CategoryTheory.Limits.PushoutCocone.isColimitAux'
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : CategoryTheory.Functor.{v, v', u, u'} C D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial.{v, u} W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
property :
  PushoutCocone.inl (PushoutCocone.mk f g ⋯) ≫ BinaryCofan.IsColimit.desc H₂ s.inl s.inr = s.inl ∧
    PushoutCocone.inr (PushoutCocone.mk f g ⋯) ≫ BinaryCofan.IsColimit.desc H₂ s.inl s.inr = s.inr ∧
      ∀ {m : Cocone.pt (F := span h k) (PushoutCocone.mk f g ⋯) ⟶ s.pt},
        PushoutCocone.inl (PushoutCocone.mk f g ⋯) ≫ m = s.inl →
          PushoutCocone.inr (PushoutCocone.mk f g ⋯) ≫ m = s.inr → m = BinaryCofan.IsColimit.desc H₂ s.inl s.inr
⊢ { l : Cocone.pt (F := span h k) (PushoutCocone.mk f g ⋯) ⟶ s.pt //
    PushoutCocone.inl (PushoutCocone.mk f g ⋯) ≫ l = s.inl ∧
      PushoutCocone.inr (PushoutCocone.mk f g ⋯) ≫ l = s.inr ∧
        ∀ {m : Cocone.pt (F := span h k) (PushoutCocone.mk f g ⋯) ⟶ s.pt},
          PushoutCocone.inl (PushoutCocone.mk f g ⋯) ≫ m = s.inl →
            PushoutCocone.inr (PushoutCocone.mk f g ⋯) ≫ m = s.inr → m = l }

Tactic:
use BinaryCofan.IsColimit.desc H₂ s.inl s.inr

Premises used: CategoryTheory.Limits.BinaryCofan.IsColimit.desc, CategoryTheory.Limits.PushoutCocone.inr, CategoryTheory.Limits.PushoutCocone.inl
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : CategoryTheory.Functor.{v, v', u, u'} C D
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
H₁ : IsInitial.{v, u} W
H₂ : IsColimit (BinaryCofan.mk f g)
s : PushoutCocone h k
right :
  PushoutCocone.inr (PushoutCocone.mk f g ⋯) ≫ BinaryCofan.IsColimit.desc H₂ s.inl s.inr = s.inr ∧
    ∀ {m : Cocone.pt (F := span h k) (PushoutCocone.mk f g ⋯) ⟶ s.pt},
      PushoutCocone.inl (PushoutCocone.mk f g ⋯) ≫ m = s.inl →
        PushoutCocone.inr (PushoutCocone.mk f g ⋯) ≫ m = s.inr → m = BinaryCofan.IsColimit.desc H₂ s.inl s.inr
⊢ PushoutCocone.inl (PushoutCocone.mk f g ⋯) ≫ BinaryCofan.IsColimit.desc H₂ s.inl s.inr = s.inl ∧
    PushoutCocone.inr (PushoutCocone.mk f g ⋯) ≫ BinaryCofan.IsColimit.desc H₂ s.inl s.inr = s.inr ∧
      ∀ {m : Cocone.pt (F := span h k) (PushoutCocone.mk f g ⋯) ⟶ s.pt},
        PushoutCocone.inl (PushoutCocone.mk f g ⋯) ≫ m = s.inl →
          PushoutCocone.inr (PushoutCocone.mk f g ⋯) ≫ m = s.inr → m = BinaryCofan.IsColimit.desc H₂ s.inl s.inr

Tactic:
use BinaryCofan.IsColimit.inl_desc H₂ _ _

Premises used: CategoryTheory.Limits.BinaryCofan.IsColimit.inl_desc