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 : HasBinaryProducts.{v, u} C
inst_3 : HasPullbacks.{v, u} C
inst_4 : PreservesLimitsOfShape (Discrete WalkingPair) G
inst_5 : PreservesLimitsOfShape WalkingCospan G
K : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cone (K ⋙ G)
⊢ c.π.app WalkingParallelPair.zero ≫ G.map (K.map WalkingParallelPairHom.left) =
    c.π.app WalkingParallelPair.zero ≫ G.map (K.map WalkingParallelPairHom.right)

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

Premises used: CategoryTheory.Limits.Cone.π, 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 : HasBinaryProducts.{v, u} C
inst_3 : HasPullbacks.{v, u} C
inst_4 : PreservesLimitsOfShape (Discrete WalkingPair) G
inst_5 : PreservesLimitsOfShape WalkingCospan G
K : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cone (K ⋙ G)
⊢ c.π.app WalkingParallelPair.zero ≫ G.map (K.map WalkingParallelPairHom.left) =
    c.π.app WalkingParallelPair.zero ≫ G.map (K.map WalkingParallelPairHom.right)

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

Premises used: CategoryTheory.Limits.Cone.π, 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 : HasBinaryProducts.{v, u} C
inst_3 : HasPullbacks.{v, u} C
inst_4 : PreservesLimitsOfShape (Discrete WalkingPair) G
inst_5 : PreservesLimitsOfShape WalkingCospan G
K : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cone (K ⋙ G)
j : WalkingParallelPair
zero :
  CategoryStruct.comp (Y :=
        pullback (Z := G.obj (prod.{v, u} (K.obj WalkingParallelPair.zero) (K.obj WalkingParallelPair.one)))
          (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)))
          (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))))
        (pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯)
        (Iso.inv
          (PreservesPullback.iso G (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
            (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right)))) ≫
      (G.mapCone (equalizerCone K)).π.app WalkingParallelPair.zero =
    c.π.app WalkingParallelPair.zero
one :
  CategoryStruct.comp (Y :=
        pullback (Z := G.obj (prod.{v, u} (K.obj WalkingParallelPair.zero) (K.obj WalkingParallelPair.one)))
          (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)))
          (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))))
        (pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯)
        (Iso.inv
          (PreservesPullback.iso G (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
            (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right)))) ≫
      (G.mapCone (equalizerCone K)).π.app WalkingParallelPair.one =
    c.π.app WalkingParallelPair.one
⊢ CategoryStruct.comp (Y :=
        pullback (Z := G.obj (prod.{v, u} (K.obj WalkingParallelPair.zero) (K.obj WalkingParallelPair.one)))
          (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)))
          (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))))
        (pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯)
        (Iso.inv
          (PreservesPullback.iso G (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
            (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right)))) ≫
      (G.mapCone (equalizerCone K)).π.app j =
    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 : HasBinaryProducts.{v, u} C
inst_3 : HasPullbacks.{v, u} C
inst_4 : PreservesLimitsOfShape (Discrete WalkingPair) G
inst_5 : PreservesLimitsOfShape WalkingCospan G
K : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cone (K ⋙ G)
⊢ CategoryStruct.comp (Y :=
        pullback (Z := G.obj (prod.{v, u} (K.obj WalkingParallelPair.zero) (K.obj WalkingParallelPair.one)))
          (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)))
          (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))))
        (pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯)
        (Iso.inv
          (PreservesPullback.iso G (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
            (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right)))) ≫
      (G.mapCone (equalizerCone K)).π.app WalkingParallelPair.zero =
    c.π.app WalkingParallelPair.zero

Tactic:
simp only [Category.comp_id, PreservesPullback.iso_inv_fst, Cone.ofFork_π, G.map_comp,
              PreservesPullback.iso_inv_fst_assoc, Functor.mapCone_π_app, eqToHom_refl,
              Category.assoc, Fork.ofι_π_app, pullback.lift_fst, pullback.lift_fst_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.lift_fst_assoc, CategoryTheory.Limits.PreservesPullback.iso_inv_fst_assoc, CategoryTheory.Limits.PreservesPullback.iso_inv_fst, CategoryTheory.Limits.Fork.ofι_π_app, CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, CategoryTheory.Functor.mapCone_π_app, CategoryTheory.Limits.Cone.ofFork_π, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.pullback.lift_fst
-- 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 : HasBinaryProducts.{v, u} C
inst_3 : HasPullbacks.{v, u} C
inst_4 : PreservesLimitsOfShape (Discrete WalkingPair) G
inst_5 : PreservesLimitsOfShape WalkingCospan G
K : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cone (K ⋙ G)
one : c.π.app WalkingParallelPair.zero ≫ G.map (K.map WalkingParallelPairHom.left) = c.π.app WalkingParallelPair.one
⊢ CategoryStruct.comp (Y :=
        pullback (Z := G.obj (prod.{v, u} (K.obj WalkingParallelPair.zero) (K.obj WalkingParallelPair.one)))
          (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)))
          (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))))
        (pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯)
        (Iso.inv
          (PreservesPullback.iso G (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
            (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right)))) ≫
      (G.mapCone (equalizerCone K)).π.app WalkingParallelPair.one =
    c.π.app WalkingParallelPair.one

Tactic:
simp only [Category.comp_id, PreservesPullback.iso_inv_fst, Cone.ofFork_π, G.map_comp,
              PreservesPullback.iso_inv_fst_assoc, Functor.mapCone_π_app, eqToHom_refl,
              Category.assoc, Fork.ofι_π_app, pullback.lift_fst, pullback.lift_fst_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.lift_fst_assoc, CategoryTheory.Limits.PreservesPullback.iso_inv_fst_assoc, CategoryTheory.Limits.PreservesPullback.iso_inv_fst, CategoryTheory.Limits.Fork.ofι_π_app, CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, CategoryTheory.Functor.mapCone_π_app, CategoryTheory.Limits.Cone.ofFork_π, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.pullback.lift_fst
-- 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 : HasBinaryProducts.{v, u} C
inst_3 : HasPullbacks.{v, u} C
inst_4 : PreservesLimitsOfShape (Discrete WalkingPair) G
inst_5 : PreservesLimitsOfShape WalkingCospan G
K : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cone (K ⋙ G)
⊢ c.π.app WalkingParallelPair.zero ≫ G.map (K.map WalkingParallelPairHom.left) = c.π.app WalkingParallelPair.one

Tactic:
(c.π.naturality WalkingParallelPairHom.left).symm.trans (Category.id_comp _)

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.NatTrans.naturality, Eq.symm, CategoryTheory.Limits.WalkingParallelPairHom.left, Eq.trans, 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 : HasBinaryProducts.{v, u} C
inst_3 : HasPullbacks.{v, u} C
inst_4 : PreservesLimitsOfShape (Discrete WalkingPair) G
inst_5 : PreservesLimitsOfShape WalkingCospan G
K : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cone (K ⋙ G)
⊢ c.π.app WalkingParallelPair.zero ≫ G.map (K.map WalkingParallelPairHom.left) = c.π.app WalkingParallelPair.one

Tactic:
exact (c.π.naturality WalkingParallelPairHom.left).symm.trans (Category.id_comp _)

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.NatTrans.naturality, Eq.symm, CategoryTheory.Limits.WalkingParallelPairHom.left, Eq.trans, 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 : HasBinaryProducts.{v, u} C
inst_3 : HasPullbacks.{v, u} C
inst_4 : PreservesLimitsOfShape (Discrete WalkingPair) G
inst_5 : PreservesLimitsOfShape WalkingCospan G
K : Functor.{0, v, 0, u} WalkingParallelPair C
s : Cone (K ⋙ G)
m : s.pt ⟶ (G.mapCone (equalizerCone K)).pt
h : ∀ (j : WalkingParallelPair), m ≫ (G.mapCone (equalizerCone K)).π.app j = s.π.app j
rw :
  Eq (α :=
    s.pt ⟶
      pullback (Z := G.obj (prod.{v, u} (K.obj WalkingParallelPair.zero) (K.obj WalkingParallelPair.one)))
        (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)))
        (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))))
    (m ≫
      Iso.hom
        (PreservesPullback.iso G (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))))
    (pullback.lift (s.π.app WalkingParallelPair.zero) (s.π.app WalkingParallelPair.zero) ⋯)
⊢ m =
    CategoryStruct.comp (Y :=
      pullback (Z := G.obj (prod.{v, u} (K.obj WalkingParallelPair.zero) (K.obj WalkingParallelPair.one)))
        (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)))
        (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))))
      (pullback.lift (s.π.app WalkingParallelPair.zero) (s.π.app WalkingParallelPair.zero) ⋯)
      (Iso.inv
        (PreservesPullback.iso G (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))))

Tactic:
rw [Iso.eq_comp_inv]

Premises used: CategoryTheory.Iso.eq_comp_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 : HasBinaryProducts.{v, u} C
inst_3 : HasPullbacks.{v, u} C
inst_4 : PreservesLimitsOfShape (Discrete WalkingPair) G
inst_5 : PreservesLimitsOfShape WalkingCospan G
K : Functor.{0, v, 0, u} WalkingParallelPair C
s : Cone (K ⋙ G)
m : s.pt ⟶ (G.mapCone (equalizerCone K)).pt
h : ∀ (j : WalkingParallelPair), m ≫ (G.mapCone (equalizerCone K)).π.app j = s.π.app j
⊢ m ≫ (G.mapCone (equalizerCone K)).π.app WalkingParallelPair.zero = s.π.app WalkingParallelPair.zero

Tactic:
have := h WalkingParallelPair.zero
-- 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 : HasBinaryProducts.{v, u} C
inst_3 : HasPullbacks.{v, u} C
inst_4 : PreservesLimitsOfShape (Discrete WalkingPair) G
inst_5 : PreservesLimitsOfShape WalkingCospan G
K : Functor.{0, v, 0, u} WalkingParallelPair C
s : Cone (K ⋙ G)
m : s.pt ⟶ (G.mapCone (equalizerCone K)).pt
h : ∀ (j : WalkingParallelPair), m ≫ (G.mapCone (equalizerCone K)).π.app j = s.π.app j
this : m ≫ G.map (pullbackFst K ≫ 𝟙 (K.obj WalkingParallelPair.zero)) = s.π.app WalkingParallelPair.zero
⊢ CategoryStruct.comp (Y :=
      pullback (Z := G.obj (prod.{v, u} (K.obj WalkingParallelPair.zero) (K.obj WalkingParallelPair.one)))
        (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)))
        (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))))
      (m ≫
        Iso.hom
          (PreservesPullback.iso G (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
            (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))))
      (pullback.fst (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)))
        (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right)))) =
    CategoryStruct.comp (Y :=
      pullback (Z := G.obj (prod.{v, u} (K.obj WalkingParallelPair.zero) (K.obj WalkingParallelPair.one)))
        (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)))
        (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))))
      (pullback.lift (s.π.app WalkingParallelPair.zero) (s.π.app WalkingParallelPair.zero) ⋯)
      (pullback.fst (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)))
        (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))))

Tactic:
simp only [PreservesPullback.iso_hom_snd, Category.assoc,
              PreservesPullback.iso_hom_fst, pullback.lift_fst, pullback.lift_snd,
              Category.comp_id, ← pullbackFst_eq_pullback_snd, ← this]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.lift_snd, CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.pullbackFst_eq_pullback_snd, CategoryTheory.Limits.PreservesPullback.iso_hom_fst, CategoryTheory.Category.comp_id, CategoryTheory.Limits.PreservesPullback.iso_hom_snd, CategoryTheory.Limits.pullback.lift_fst
-- 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 : HasBinaryProducts.{v, u} C
inst_3 : HasPullbacks.{v, u} C
inst_4 : PreservesLimitsOfShape (Discrete WalkingPair) G
inst_5 : PreservesLimitsOfShape WalkingCospan G
K : Functor.{0, v, 0, u} WalkingParallelPair C
s : Cone (K ⋙ G)
m : s.pt ⟶ (G.mapCone (equalizerCone K)).pt
h : ∀ (j : WalkingParallelPair), m ≫ (G.mapCone (equalizerCone K)).π.app j = s.π.app j
this : m ≫ G.map (pullbackFst K ≫ 𝟙 (K.obj WalkingParallelPair.zero)) = s.π.app WalkingParallelPair.zero
⊢ CategoryStruct.comp (Y :=
      pullback (Z := G.obj (prod.{v, u} (K.obj WalkingParallelPair.zero) (K.obj WalkingParallelPair.one)))
        (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)))
        (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))))
      (m ≫
        Iso.hom
          (PreservesPullback.iso G (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
            (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))))
      (pullback.snd (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)))
        (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right)))) =
    CategoryStruct.comp (Y :=
      pullback (Z := G.obj (prod.{v, u} (K.obj WalkingParallelPair.zero) (K.obj WalkingParallelPair.one)))
        (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)))
        (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))))
      (pullback.lift (s.π.app WalkingParallelPair.zero) (s.π.app WalkingParallelPair.zero) ⋯)
      (pullback.snd (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)))
        (G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))))

Tactic:
simp only [PreservesPullback.iso_hom_snd, Category.assoc,
              PreservesPullback.iso_hom_fst, pullback.lift_fst, pullback.lift_snd,
              Category.comp_id, ← pullbackFst_eq_pullback_snd, ← this]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.lift_snd, CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.pullbackFst_eq_pullback_snd, CategoryTheory.Limits.PreservesPullback.iso_hom_fst, CategoryTheory.Category.comp_id, CategoryTheory.Limits.PreservesPullback.iso_hom_snd, CategoryTheory.Limits.pullback.lift_fst
-- 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
F : Functor.{0, v, 0, u} WalkingParallelPair C
⊢ Eq (α := F.obj WalkingParallelPair.one ⟶ constructCoequalizer F)
    (CategoryStruct.comp (Y := coprod.{v, u} (F.obj WalkingParallelPair.one) (F.obj WalkingParallelPair.zero))
      coprod.inl
      (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.inl
      (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.inl pushout.condition : (_ : F.obj _ ⟶ constructCoequalizer _) = _)

Premises used: CategoryTheory.Limits.pushout.condition, CategoryTheory.Limits.coprod.inl, CategoryTheory.whisker_eq
-- 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
F : Functor.{0, v, 0, u} WalkingParallelPair C
h :
  Eq (α := F.obj WalkingParallelPair.one ⟶ constructCoequalizer F) (pushoutInl F)
    (CategoryStruct.comp (Y := coprod.{v, u} (F.obj WalkingParallelPair.one) (F.obj WalkingParallelPair.zero))
      coprod.inl
      (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.one ⟶ constructCoequalizer F)
    (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.inl
      (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.one ⟶ constructCoequalizer F) (pushoutInl F)
    (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.inl pushout.condition : (_ : F.obj _ ⟶ constructCoequalizer _) = _)

Premises used: CategoryTheory.Limits.pushout.condition, CategoryTheory.Limits.coprod.inl, CategoryTheory.whisker_eq
-- 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
F : Functor.{0, v, 0, u} WalkingParallelPair C
⊢ Eq (α := F.obj WalkingParallelPair.one ⟶ constructCoequalizer F) (pushoutInl F)
    (CategoryStruct.comp (Y := coprod.{v, u} (F.obj WalkingParallelPair.one) (F.obj WalkingParallelPair.zero))
      coprod.inl
      (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
inst_1 : HasBinaryCoproducts.{v, u} C
inst_2 : HasPushouts.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
⊢ Eq (α := F.obj WalkingParallelPair.one ⟶ constructCoequalizer F)
    (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.inl
      (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
rw :
  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.map WalkingParallelPairHom.right ≫ pushoutInl F

Tactic:
rw [pushoutInl_eq_pushout_inr]

Premises used: CategoryTheory.Limits.HasCoequalizersOfHasPushoutsAndBinaryCoproducts.pushoutInl_eq_pushout_inr