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
inst_4 : PreservesColimitsOfShape (Discrete WalkingPair) G
inst_5 : PreservesColimitsOfShape WalkingSpan G
K : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cocone (K ⋙ G)
⊢ Eq (α :=
    Functor.obj.{0, v', 0, u'} (pair (G.obj (K.obj WalkingParallelPair.one)) (G.obj (K.obj WalkingParallelPair.zero)))
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      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))))
        { as := WalkingPair.left : Discrete WalkingPair })
      (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)))
        { as := WalkingPair.left })
      (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))))
        { as := WalkingPair.left : Discrete WalkingPair })
      (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)))
        { as := WalkingPair.left })
      (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right)) ≫
        c.ι.app WalkingParallelPair.one))

Tactic:
simp only [BinaryCofan.ι_app_left, BinaryCofan.mk_inl, ←
              G.map_comp_assoc, coprod.inl_desc]

Premises used: CategoryTheory.Limits.BinaryCofan.mk_inl, CategoryTheory.Limits.coprod.inl_desc, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Limits.BinaryCofan.ι_app_left
-- 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 :
  G.map (K.map WalkingParallelPairHom.left) ≫ c.ι.app WalkingParallelPair.one =
    G.map (K.map WalkingParallelPairHom.right) ≫ c.ι.app WalkingParallelPair.one
⊢ Eq (α :=
    Functor.obj.{0, v', 0, u'} (pair (G.obj (K.obj WalkingParallelPair.one)) (G.obj (K.obj WalkingParallelPair.zero)))
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      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))))
        { as := WalkingPair.right : Discrete WalkingPair })
      (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)))
        { as := WalkingPair.right })
      (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))))
        { as := WalkingPair.right : Discrete WalkingPair })
      (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)))
        { as := WalkingPair.right })
      (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right)) ≫
        c.ι.app WalkingParallelPair.one))

Tactic:
simp only [BinaryCofan.ι_app_right, BinaryCofan.mk_inr, ←
              G.map_comp_assoc, coprod.inr_desc]

Premises used: CategoryTheory.Limits.BinaryCofan.mk_inr, CategoryTheory.Limits.BinaryCofan.ι_app_right, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Limits.coprod.inr_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
inst_4 : PreservesColimitsOfShape (Discrete WalkingPair) G
inst_5 : PreservesColimitsOfShape WalkingSpan G
K : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cocone (K ⋙ G)
⊢ G.map (K.map WalkingParallelPairHom.left) ≫ c.ι.app WalkingParallelPair.one =
    G.map (K.map WalkingParallelPairHom.right) ≫ c.ι.app WalkingParallelPair.one

Tactic:
(c.ι.naturality WalkingParallelPairHom.left).trans
                (c.ι.naturality WalkingParallelPairHom.right).symm

Premises used: CategoryTheory.Limits.Cocone.ι, CategoryTheory.Limits.WalkingParallelPairHom.right, CategoryTheory.NatTrans.naturality, Eq.symm, CategoryTheory.Limits.WalkingParallelPairHom.left, Eq.trans
-- 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.map (K.map WalkingParallelPairHom.left) ≫ c.ι.app WalkingParallelPair.one =
    G.map (K.map WalkingParallelPairHom.right) ≫ c.ι.app WalkingParallelPair.one

Tactic:
exact
              (c.ι.naturality WalkingParallelPairHom.left).trans
                (c.ι.naturality WalkingParallelPairHom.right).symm

Premises used: CategoryTheory.Limits.Cocone.ι, CategoryTheory.Limits.WalkingParallelPairHom.right, CategoryTheory.NatTrans.naturality, Eq.symm, CategoryTheory.Limits.WalkingParallelPairHom.left, Eq.trans
-- 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)
j : WalkingParallelPair
zero :
  (G.mapCocone (coequalizerCocone K)).ι.app WalkingParallelPair.zero ≫
      CategoryStruct.comp (Y :=
        pushout (X := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
          (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
          (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
        (Iso.inv
          (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
            (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
        (pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯) =
    c.ι.app WalkingParallelPair.zero
one :
  (G.mapCocone (coequalizerCocone K)).ι.app WalkingParallelPair.one ≫
      CategoryStruct.comp (Y :=
        pushout (X := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
          (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
          (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
        (Iso.inv
          (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
            (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
        (pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯) =
    c.ι.app WalkingParallelPair.one
⊢ (G.mapCocone (coequalizerCocone K)).ι.app j ≫
      CategoryStruct.comp (Y :=
        pushout (X := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
          (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
          (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
        (Iso.inv
          (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
            (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
        (pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯) =
    c.ι.app j

Tactic:
rcases j with (_ | _)
-- 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)
zero : G.map (K.map WalkingParallelPairHom.left) ≫ c.ι.app WalkingParallelPair.one = c.ι.app WalkingParallelPair.zero
⊢ (G.mapCocone (coequalizerCocone K)).ι.app WalkingParallelPair.zero ≫
      CategoryStruct.comp (Y :=
        pushout (X := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
          (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
          (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
        (Iso.inv
          (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
            (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
        (pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯) =
    c.ι.app WalkingParallelPair.zero

Tactic:
simp only [Functor.mapCocone_ι_app, Cocone.ofCofork_ι, Category.id_comp,
              eqToHom_refl, Category.assoc, Functor.map_comp, Cofork.ofπ_ι_app, pushout.inl_desc,
              PreservesPushout.inl_iso_inv_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.mapCocone_ι_app, CategoryTheory.Limits.PreservesPushout.inl_iso_inv_assoc, CategoryTheory.eqToHom_refl, CategoryTheory.Limits.Cocone.ofCofork_ι, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.pushout.inl_desc, CategoryTheory.Limits.Cofork.ofπ_ι_app, CategoryTheory.Category.id_comp
-- 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.mapCocone (coequalizerCocone K)).ι.app WalkingParallelPair.one ≫
      CategoryStruct.comp (Y :=
        pushout (X := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
          (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
          (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
        (Iso.inv
          (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
            (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
        (pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯) =
    c.ι.app WalkingParallelPair.one

Tactic:
simp only [Functor.mapCocone_ι_app, Cocone.ofCofork_ι, Category.id_comp,
              eqToHom_refl, Category.assoc, Functor.map_comp, Cofork.ofπ_ι_app, pushout.inl_desc,
              PreservesPushout.inl_iso_inv_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.mapCocone_ι_app, CategoryTheory.Limits.PreservesPushout.inl_iso_inv_assoc, CategoryTheory.eqToHom_refl, CategoryTheory.Limits.Cocone.ofCofork_ι, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.pushout.inl_desc, CategoryTheory.Limits.Cofork.ofπ_ι_app, CategoryTheory.Category.id_comp
-- 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.map (K.map WalkingParallelPairHom.left) ≫ c.ι.app WalkingParallelPair.one = c.ι.app WalkingParallelPair.zero

Tactic:
(c.ι.naturality WalkingParallelPairHom.left).trans (Category.comp_id _)

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.naturality, CategoryTheory.Limits.WalkingParallelPairHom.left, Eq.trans
-- 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.map (K.map WalkingParallelPairHom.left) ≫ c.ι.app WalkingParallelPair.one = c.ι.app WalkingParallelPair.zero

Tactic:
exact (c.ι.naturality WalkingParallelPairHom.left).trans (Category.comp_id _)

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.naturality, CategoryTheory.Limits.WalkingParallelPairHom.left, Eq.trans
-- 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
s : Cocone (K ⋙ G)
m : (G.mapCocone (coequalizerCocone K)).pt ⟶ s.pt
h : ∀ (j : WalkingParallelPair), (G.mapCocone (coequalizerCocone K)).ι.app j ≫ m = s.ι.app j
rw :
  Eq (α :=
    pushout (X := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))) ⟶
      s.pt)
    (Iso.hom
        (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))) ≫
      m)
    (pushout.desc (s.ι.app WalkingParallelPair.one) (s.ι.app WalkingParallelPair.one) ⋯)
⊢ m =
    CategoryStruct.comp (Y :=
      pushout (X := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
      (Iso.inv
        (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
      (pushout.desc (s.ι.app WalkingParallelPair.one) (s.ι.app WalkingParallelPair.one) ⋯)

Tactic:
rw [Iso.eq_inv_comp]

Premises used: CategoryTheory.Iso.eq_inv_comp
-- 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
s : Cocone (K ⋙ G)
m : (G.mapCocone (coequalizerCocone K)).pt ⟶ s.pt
h : ∀ (j : WalkingParallelPair), (G.mapCocone (coequalizerCocone K)).ι.app j ≫ m = s.ι.app j
⊢ (G.mapCocone (coequalizerCocone K)).ι.app WalkingParallelPair.one ≫ m = s.ι.app WalkingParallelPair.one

Tactic:
have := h 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
inst_4 : PreservesColimitsOfShape (Discrete WalkingPair) G
inst_5 : PreservesColimitsOfShape WalkingSpan G
K : Functor.{0, v, 0, u} WalkingParallelPair C
s : Cocone (K ⋙ G)
m : (G.mapCocone (coequalizerCocone K)).pt ⟶ s.pt
h : ∀ (j : WalkingParallelPair), (G.mapCocone (coequalizerCocone K)).ι.app j ≫ m = s.ι.app j
this : G.map (𝟙 (K.obj WalkingParallelPair.one) ≫ pushoutInl K) ≫ m = s.ι.app WalkingParallelPair.one
⊢ CategoryStruct.comp (Y :=
      pushout (X := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
      (pushout.inl (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
      (Iso.hom
          (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
            (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))) ≫
        m) =
    CategoryStruct.comp (Y :=
      pushout (X := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
      (pushout.inl (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
      (pushout.desc (s.ι.app WalkingParallelPair.one) (s.ι.app WalkingParallelPair.one) ⋯)

Tactic:
simp only [PreservesPushout.inl_iso_hom_assoc, Category.id_comp, pushout.inl_desc,
              pushout.inr_desc, PreservesPushout.inr_iso_hom_assoc, ← pushoutInl_eq_pushout_inr, ←
              this]

Premises used: CategoryTheory.Limits.pushout.inr_desc, CategoryTheory.Limits.PreservesPushout.inr_iso_hom_assoc, CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.pushoutInl_eq_pushout_inr, CategoryTheory.Limits.PreservesPushout.inl_iso_hom_assoc, CategoryTheory.Limits.pushout.inl_desc, CategoryTheory.Category.id_comp
-- 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
s : Cocone (K ⋙ G)
m : (G.mapCocone (coequalizerCocone K)).pt ⟶ s.pt
h : ∀ (j : WalkingParallelPair), (G.mapCocone (coequalizerCocone K)).ι.app j ≫ m = s.ι.app j
this : G.map (𝟙 (K.obj WalkingParallelPair.one) ≫ pushoutInl K) ≫ m = s.ι.app WalkingParallelPair.one
⊢ CategoryStruct.comp (Y :=
      pushout (X := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
      (pushout.inr (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
      (Iso.hom
          (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
            (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))) ≫
        m) =
    CategoryStruct.comp (Y :=
      pushout (X := G.obj (coprod.{v, u} (K.obj WalkingParallelPair.one) (K.obj WalkingParallelPair.zero)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
      (pushout.inr (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)))
        (G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))))
      (pushout.desc (s.ι.app WalkingParallelPair.one) (s.ι.app WalkingParallelPair.one) ⋯)

Tactic:
simp only [PreservesPushout.inl_iso_hom_assoc, Category.id_comp, pushout.inl_desc,
              pushout.inr_desc, PreservesPushout.inr_iso_hom_assoc, ← pushoutInl_eq_pushout_inr, ←
              this]

Premises used: CategoryTheory.Limits.pushout.inr_desc, CategoryTheory.Limits.PreservesPushout.inr_iso_hom_assoc, CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.pushoutInl_eq_pushout_inr, CategoryTheory.Limits.PreservesPushout.inl_iso_hom_assoc, CategoryTheory.Limits.pushout.inl_desc, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
i₀ : J
h : F.IsEventuallyConstantTo i₀
i j : J
φ : i ⟶ j
π : j ⟶ i₀
⊢ IsIso (F.map π)

Tactic:
have := h π
-- Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
i₀ : J
h : F.IsEventuallyConstantTo i₀
i j : J
φ : i ⟶ j
π : j ⟶ i₀
this : IsIso (F.map π)
⊢ IsIso (F.map (φ ≫ π))

Tactic:
have := h (φ ≫ π)