awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
G : Functor.{v, v', u, u'} C D
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : HasPushouts.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
conv_rhs :
  Eq (α := F.obj WalkingParallelPair.zero ⟶ constructCoequalizer F) (F.map WalkingParallelPairHom.left ≫ pushoutInl F)
    (F.map WalkingParallelPairHom.right ≫
      pushout.inr (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
        (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)))
⊢ Eq (α := F.obj WalkingParallelPair.zero ⟶ constructCoequalizer F) (F.map WalkingParallelPairHom.left ≫ pushoutInl F)
    (F.map WalkingParallelPairHom.right ≫ pushoutInl F)

Tactic:
conv_rhs => rw [pushoutInl_eq_pushout_inr]

Premises used: CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.pushoutInl_eq_pushout_inr
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
G : Functor.{v, v', u, u'} C D
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : HasPushouts.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
⊢ Eq (α := F.obj WalkingParallelPair.zero ⟶ constructCoequalizer F)
    (CategoryStruct.comp (Y := coprod.{v, u} (F.obj WalkingParallelPair.one) (F.obj WalkingParallelPair.zero))
      coprod.inr
      (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left) ≫
        pushout.inl (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right))))
    (CategoryStruct.comp (Y := coprod.{v, u} (F.obj WalkingParallelPair.one) (F.obj WalkingParallelPair.zero))
      coprod.inr
      (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right) ≫
        pushout.inr (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right))))

Tactic:
(whisker_eq Limits.coprod.inr pushout.condition :
            (_ : F.obj _ ⟶ constructCoequalizer _) = _)

Premises used: CategoryTheory.Limits.pushout.condition, CategoryTheory.Limits.coprod.inr, CategoryTheory.whisker_eq
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
G : Functor.{v, v', u, u'} C D
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : HasPushouts.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
h :
  Eq (α := F.obj WalkingParallelPair.zero ⟶ constructCoequalizer F) (F.map WalkingParallelPairHom.left ≫ pushoutInl F)
    (CategoryStruct.comp (Y := coprod.{v, u} (F.obj WalkingParallelPair.one) (F.obj WalkingParallelPair.zero))
      coprod.inr
      (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left) ≫
        pushout.inl (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right))))
h₁ :
  Eq (α := F.obj WalkingParallelPair.zero ⟶ constructCoequalizer F)
    (F.map WalkingParallelPairHom.right ≫
      pushout.inr (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
        (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)))
    (CategoryStruct.comp (Y := coprod.{v, u} (F.obj WalkingParallelPair.one) (F.obj WalkingParallelPair.zero))
      coprod.inr
      (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right) ≫
        pushout.inr (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right))))
⊢ Eq (α := F.obj WalkingParallelPair.zero ⟶ constructCoequalizer F) (F.map WalkingParallelPairHom.left ≫ pushoutInl F)
    (F.map WalkingParallelPairHom.right ≫
      pushout.inr (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
        (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)))

Tactic:
convert!
          (whisker_eq Limits.coprod.inr pushout.condition :
            (_ : F.obj _ ⟶ constructCoequalizer _) = _) using
          1

Premises used: CategoryTheory.Limits.pushout.condition, CategoryTheory.Limits.coprod.inr, CategoryTheory.whisker_eq
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
G : Functor.{v, v', u, u'} C D
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : HasPushouts.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
⊢ Eq (α := F.obj WalkingParallelPair.zero ⟶ constructCoequalizer F) (F.map WalkingParallelPairHom.left ≫ pushoutInl F)
    (CategoryStruct.comp (Y := coprod.{v, u} (F.obj WalkingParallelPair.one) (F.obj WalkingParallelPair.zero))
      coprod.inr
      (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left) ≫
        pushout.inl (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
G : Functor.{v, v', u, u'} C D
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : HasPushouts.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
⊢ Eq (α := F.obj WalkingParallelPair.zero ⟶ constructCoequalizer F)
    (F.map WalkingParallelPairHom.right ≫
      pushout.inr (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
        (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)))
    (CategoryStruct.comp (Y := coprod.{v, u} (F.obj WalkingParallelPair.one) (F.obj WalkingParallelPair.zero))
      coprod.inr
      (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right) ≫
        pushout.inr (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
G : Functor.{v, v', u, u'} C D
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : HasPushouts.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cocone F
⊢ (coequalizerCocone F).ι.app WalkingParallelPair.zero ≫
      pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯ =
    c.ι.app WalkingParallelPair.zero

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
G : Functor.{v, v', u, u'} C D
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : HasPushouts.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cocone F
⊢ (coequalizerCocone F).ι.app WalkingParallelPair.one ≫
      pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯ =
    c.ι.app WalkingParallelPair.one

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
G : Functor.{v, v', u, u'} C D
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : HasPushouts.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cocone F
m : (coequalizerCocone F).pt ⟶ c.pt
J : ∀ (j : WalkingParallelPair), (coequalizerCocone F).ι.app j ≫ m = c.ι.app j
⊢ pushoutInl F ≫ m = c.ι.app WalkingParallelPair.one

Tactic:
simpa using J WalkingParallelPair.one

Premises used: CategoryTheory.Limits.WalkingParallelPair.one
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
G : Functor.{v, v', u, u'} C D
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : HasPushouts.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cocone F
m : (coequalizerCocone F).pt ⟶ c.pt
J : ∀ (j : WalkingParallelPair), (coequalizerCocone F).ι.app j ≫ m = c.ι.app j
⊢ pushoutInl F ≫ m = c.ι.app WalkingParallelPair.one

Tactic:
have J1 : pushoutInl F ≫ m = c.ι.app WalkingParallelPair.one := by
      simpa using J WalkingParallelPair.one
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
G : Functor.{v, v', u, u'} C D
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : HasPushouts.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cocone F
m : (coequalizerCocone F).pt ⟶ c.pt
J : ∀ (j : WalkingParallelPair), (coequalizerCocone F).ι.app j ≫ m = c.ι.app j
J1 : pushoutInl F ≫ m = c.ι.app WalkingParallelPair.one
h₀ :
  pushout.inl (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
        (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)) ≫
      m =
    NatTrans.app (Cocone.ι (PushoutCocone.mk (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯))
      WalkingSpan.left
⊢ pushout.inl (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
        (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)) ≫
      m =
    CategoryStruct.comp (Y :=
      pushout (X := coprod.{v, u} (F.obj WalkingParallelPair.one) (F.obj WalkingParallelPair.zero))
        (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
        (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)))
      (pushout.inl (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)) :
        F.obj WalkingParallelPair.one ⟶
          pushout (X := coprod.{v, u} (F.obj WalkingParallelPair.one) (F.obj WalkingParallelPair.zero))
            (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
            (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)))
      (pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯ :
        pushout (X := coprod.{v, u} (F.obj WalkingParallelPair.one) (F.obj WalkingParallelPair.zero))
            (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
            (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)) ⟶
          c.pt)

Tactic:
rw [colimit.ι_desc]

Premises used: CategoryTheory.Limits.colimit.ι_desc
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
G : Functor.{v, v', u, u'} C D
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : HasPushouts.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cocone F
m : (coequalizerCocone F).pt ⟶ c.pt
J : ∀ (j : WalkingParallelPair), (coequalizerCocone F).ι.app j ≫ m = c.ι.app j
J1 : pushoutInl F ≫ m = c.ι.app WalkingParallelPair.one
⊢ pushout.inl (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
        (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)) ≫
      m =
    NatTrans.app (Cocone.ι (PushoutCocone.mk (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯))
      WalkingSpan.left

Tactic:
J1
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
G : Functor.{v, v', u, u'} C D
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : HasPushouts.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cocone F
m : (coequalizerCocone F).pt ⟶ c.pt
J : ∀ (j : WalkingParallelPair), (coequalizerCocone F).ι.app j ≫ m = c.ι.app j
J1 : pushoutInl F ≫ m = c.ι.app WalkingParallelPair.one
⊢ pushout.inl (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
        (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)) ≫
      m =
    NatTrans.app (Cocone.ι (PushoutCocone.mk (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯))
      WalkingSpan.left

Tactic:
exact J1
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
G : Functor.{v, v', u, u'} C D
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : HasPushouts.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cocone F
m : (coequalizerCocone F).pt ⟶ c.pt
J : ∀ (j : WalkingParallelPair), (coequalizerCocone F).ι.app j ≫ m = c.ι.app j
J1 : pushoutInl F ≫ m = c.ι.app WalkingParallelPair.one
h₁ :
  pushoutInl F ≫ m =
    NatTrans.app (Cocone.ι (PushoutCocone.mk (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯))
      WalkingSpan.right
⊢ pushout.inr (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
        (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)) ≫
      m =
    CategoryStruct.comp (Y :=
      pushout (X := coprod.{v, u} (F.obj WalkingParallelPair.one) (F.obj WalkingParallelPair.zero))
        (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
        (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)))
      (pushout.inr (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)) :
        F.obj WalkingParallelPair.one ⟶
          pushout (X := coprod.{v, u} (F.obj WalkingParallelPair.one) (F.obj WalkingParallelPair.zero))
            (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
            (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)))
      (pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯ :
        pushout (X := coprod.{v, u} (F.obj WalkingParallelPair.one) (F.obj WalkingParallelPair.zero))
            (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.left))
            (coprod.desc (𝟙 (F.obj WalkingParallelPair.one)) (F.map WalkingParallelPairHom.right)) ⟶
          c.pt)

Tactic:
rw [colimit.ι_desc, ← pushoutInl_eq_pushout_inr]

Premises used: CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.pushoutInl_eq_pushout_inr, CategoryTheory.Limits.colimit.ι_desc
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
G : Functor.{v, v', u, u'} C D
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : HasPushouts.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cocone F
m : (coequalizerCocone F).pt ⟶ c.pt
J : ∀ (j : WalkingParallelPair), (coequalizerCocone F).ι.app j ≫ m = c.ι.app j
J1 : pushoutInl F ≫ m = c.ι.app WalkingParallelPair.one
⊢ pushoutInl F ≫ m =
    NatTrans.app (Cocone.ι (PushoutCocone.mk (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯))
      WalkingSpan.right

Tactic:
J1
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
G : Functor.{v, v', u, u'} C D
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : HasPushouts.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cocone F
m : (coequalizerCocone F).pt ⟶ c.pt
J : ∀ (j : WalkingParallelPair), (coequalizerCocone F).ι.app j ≫ m = c.ι.app j
J1 : pushoutInl F ≫ m = c.ι.app WalkingParallelPair.one
⊢ pushoutInl F ≫ m =
    NatTrans.app (Cocone.ι (PushoutCocone.mk (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯))
      WalkingSpan.right

Tactic:
exact J1
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryCoproducts.{v, u} C
inst_2 : HasPushouts.{v, u} C
⊢ HasCoequalizers.{v, u} C

Tactic:
{
    has_colimit := fun F =>
      HasColimit.mk
        { cocone := coequalizerCocone F
          isColimit := coequalizerCoconeIsColimit F } }

Premises used: CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.coequalizerCoconeIsColimit, CategoryTheory.Limits.HasColimitsOfShape.mk, CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.coequalizerCocone, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.ColimitCocone.mk
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
G : Functor.{v, v', u, u'} C D
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : HasPushouts.{v, u} C
inst_4 : PreservesColimitsOfShape (Discrete WalkingPair) G
inst_5 : PreservesColimitsOfShape WalkingSpan G
K : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cocone (K ⋙ G)
refine_1 refine_2 : G.obj (K.obj WalkingParallelPair.one) ⟶ c.pt
refine_3 :
  Eq (α := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)) ⟶ c.pt)
    (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)) ≫
      c.ι.app WalkingParallelPair.one)
    (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right)) ≫
      c.ι.app WalkingParallelPair.one)
⊢ (G.mapCocone (coequalizerCocone K)).pt ⟶ c.pt

Tactic:
refine (PreservesPushout.iso _ _ _).inv ≫ pushout.desc ?_ ?_ ?_

Premises used: CategoryTheory.Limits.PreservesPushout.iso, CategoryTheory.Limits.pushout.desc, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
G : Functor.{v, v', u, u'} C D
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : HasPushouts.{v, u} C
inst_4 : PreservesColimitsOfShape (Discrete WalkingPair) G
inst_5 : PreservesColimitsOfShape WalkingSpan G
K : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cocone (K ⋙ G)
⊢ G.obj (K.obj WalkingParallelPair.one) ⟶ c.pt

Tactic:
exact c.ι.app WalkingParallelPair.one

Premises used: CategoryTheory.Limits.WalkingParallelPair.one, CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
G : Functor.{v, v', u, u'} C D
inst_2 : HasBinaryCoproducts.{v, u} C
inst_3 : HasPushouts.{v, u} C
inst_4 : PreservesColimitsOfShape (Discrete WalkingPair) G
inst_5 : PreservesColimitsOfShape WalkingSpan G
K : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cocone (K ⋙ G)
refine_3 :
  ∀ (j : Discrete WalkingPair),
    Eq (α :=
      Functor.obj.{0, v', 0, u'} (pair (G.obj (K.obj WalkingParallelPair.one)) (G.obj (K.obj WalkingParallelPair.zero)))
          j ⟶
        c.pt)
      (CategoryStruct.comp (Y :=
        Functor.obj.{0, v', 0, u'}
          (Functor.obj (Functor.const (Discrete WalkingPair))
            (Cocone.pt (F := pair (G.obj (K.obj WalkingParallelPair.one)) (G.obj (K.obj WalkingParallelPair.zero)))
              (BinaryCofan.mk (P :=
                G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
                (G.map coprod.inl) (G.map coprod.inr))))
          j)
        (NatTrans.app
          (Cocone.ι
            (BinaryCofan.mk (P :=
              G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero))) (G.map coprod.inl)
              (G.map coprod.inr)))
          j)
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)) ≫
          c.ι.app WalkingParallelPair.one))
      (CategoryStruct.comp (Y :=
        Functor.obj.{0, v', 0, u'}
          (Functor.obj (Functor.const (Discrete WalkingPair))
            (Cocone.pt (F := pair (G.obj (K.obj WalkingParallelPair.one)) (G.obj (K.obj WalkingParallelPair.zero)))
              (BinaryCofan.mk (P :=
                G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
                (G.map coprod.inl) (G.map coprod.inr))))
          j)
        (NatTrans.app
          (Cocone.ι
            (BinaryCofan.mk (P :=
              G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero))) (G.map coprod.inl)
              (G.map coprod.inr)))
          j)
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right)) ≫
          c.ι.app WalkingParallelPair.one))
⊢ Eq (α := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)) ⟶ c.pt)
    (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)) ≫
      c.ι.app WalkingParallelPair.one)
    (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right)) ≫
      c.ι.app WalkingParallelPair.one)

Tactic:
apply (mapIsColimitOfPreservesOfIsColimit G _ _ (coprodIsCoprod _ _)).hom_ext

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Limits.coprodIsCoprod, CategoryTheory.Limits.mapIsColimitOfPreservesOfIsColimit