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
F : Functor.{0, v, 0, u} WalkingParallelPair C
rw :
  pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
      (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
    F.map WalkingParallelPairHom.right
| pullbackFst F ≫ F.map WalkingParallelPairHom.right

Tactic:
rw [pullbackFst_eq_pullback_snd]

Premises used: CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.pullbackFst_eq_pullback_snd
-- 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
F : Functor.{0, v, 0, u} WalkingParallelPair C
conv_rhs :
  Eq (α := constructEqualizer F ⟶ F.obj WalkingParallelPair.one) (pullbackFst F ≫ F.map WalkingParallelPairHom.left)
    (pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
        (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
      F.map WalkingParallelPairHom.right)
⊢ Eq (α := constructEqualizer F ⟶ F.obj WalkingParallelPair.one) (pullbackFst F ≫ F.map WalkingParallelPairHom.left)
    (pullbackFst F ≫ F.map WalkingParallelPairHom.right)

Tactic:
conv_rhs => rw [pullbackFst_eq_pullback_snd]

Premises used: CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.pullbackFst_eq_pullback_snd
-- 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
F : Functor.{0, v, 0, u} WalkingParallelPair C
⊢ Eq (α :=
    pullback (Z := prod.{v, u} (F.obj WalkingParallelPair.zero) (F.obj WalkingParallelPair.one))
        (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
        (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ⟶
      F.obj WalkingParallelPair.one)
    (CategoryStruct.comp (Y := prod.{v, u} (F.obj WalkingParallelPair.zero) (F.obj WalkingParallelPair.one))
      (pullback.fst (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
        prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
      prod.snd)
    (CategoryStruct.comp (Y := prod.{v, u} (F.obj WalkingParallelPair.zero) (F.obj WalkingParallelPair.one))
      (pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
        prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right))
      prod.snd)

Tactic:
(eq_whisker pullback.condition Limits.prod.snd :
            (_ : constructEqualizer F ⟶ F.obj WalkingParallelPair.one) = _)

Premises used: CategoryTheory.eq_whisker, CategoryTheory.Limits.prod.snd, CategoryTheory.Limits.pullback.condition
-- 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
F : Functor.{0, v, 0, u} WalkingParallelPair C
h :
  Eq (α := constructEqualizer F ⟶ F.obj WalkingParallelPair.one) (pullbackFst F ≫ F.map WalkingParallelPairHom.left)
    (CategoryStruct.comp (Y := prod.{v, u} (F.obj WalkingParallelPair.zero) (F.obj WalkingParallelPair.one))
      (pullback.fst (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
        prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
      prod.snd)
h₁ :
  Eq (α := constructEqualizer F ⟶ F.obj WalkingParallelPair.one)
    (pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
        (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
      F.map WalkingParallelPairHom.right)
    (CategoryStruct.comp (Y := prod.{v, u} (F.obj WalkingParallelPair.zero) (F.obj WalkingParallelPair.one))
      (pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
        prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right))
      prod.snd)
⊢ Eq (α := constructEqualizer F ⟶ F.obj WalkingParallelPair.one) (pullbackFst F ≫ F.map WalkingParallelPairHom.left)
    (pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
        (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
      F.map WalkingParallelPairHom.right)

Tactic:
convert!
          (eq_whisker pullback.condition Limits.prod.snd :
            (_ : constructEqualizer F ⟶ F.obj WalkingParallelPair.one) = _) using
          1

Premises used: CategoryTheory.eq_whisker, CategoryTheory.Limits.prod.snd, CategoryTheory.Limits.pullback.condition
-- 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
F : Functor.{0, v, 0, u} WalkingParallelPair C
⊢ Eq (α := constructEqualizer F ⟶ F.obj WalkingParallelPair.one) (pullbackFst F ≫ F.map WalkingParallelPairHom.left)
    (CategoryStruct.comp (Y := prod.{v, u} (F.obj WalkingParallelPair.zero) (F.obj WalkingParallelPair.one))
      (pullback.fst (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
        prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
      prod.snd)

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 : HasBinaryProducts.{v, u} C
inst_3 : HasPullbacks.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
⊢ Eq (α := constructEqualizer F ⟶ F.obj WalkingParallelPair.one)
    (pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
        (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
      F.map WalkingParallelPairHom.right)
    (CategoryStruct.comp (Y := prod.{v, u} (F.obj WalkingParallelPair.zero) (F.obj WalkingParallelPair.one))
      (pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ≫
        prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right))
      prod.snd)

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 : HasBinaryProducts.{v, u} C
inst_3 : HasPullbacks.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cone F
⊢ pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯ ≫
      (equalizerCone F).π.app WalkingParallelPair.zero =
    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 : HasBinaryProducts.{v, u} C
inst_3 : HasPullbacks.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cone F
⊢ pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯ ≫
      (equalizerCone F).π.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 : HasBinaryProducts.{v, u} C
inst_3 : HasPullbacks.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cone F
_ :
  ∀ (m : c.pt ⟶ (equalizerCone F).pt),
    (∀ (j : WalkingParallelPair), m ≫ (equalizerCone F).π.app j = c.π.app j) →
      m = pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯
⊢ ∀ (m : c.pt ⟶ (equalizerCone F).pt),
    (∀ (j : WalkingParallelPair), m ≫ (equalizerCone F).π.app j = c.π.app j) →
      m = pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯

Tactic:
_
-- 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
F : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cone F
m : c.pt ⟶ (equalizerCone F).pt
J : ∀ (j : WalkingParallelPair), m ≫ (equalizerCone F).π.app j = c.π.app j
⊢ m ≫ (equalizerCone F).π.app WalkingParallelPair.zero = c.π.app WalkingParallelPair.zero

Tactic:
have J0 := J 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
F : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cone F
m : c.pt ⟶ (equalizerCone F).pt
J : ∀ (j : WalkingParallelPair), m ≫ (equalizerCone F).π.app j = c.π.app j
J0 : m ≫ (equalizerCone F).π.app WalkingParallelPair.zero = c.π.app WalkingParallelPair.zero
⊢ m ≫
      pullback.fst (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
        (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) =
    CategoryStruct.comp (Y :=
      pullback (Z := prod.{v, u} (F.obj WalkingParallelPair.zero) (F.obj WalkingParallelPair.one))
        (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
        (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)))
      (pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯ :
        c.pt ⟶
          pullback (Z := prod.{v, u} (F.obj WalkingParallelPair.zero) (F.obj WalkingParallelPair.one))
            (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
            (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)))
      (pullback.fst (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) :
        pullback (Z := prod.{v, u} (F.obj WalkingParallelPair.zero) (F.obj WalkingParallelPair.one))
            (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
            (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ⟶
          F.obj WalkingParallelPair.zero)

Tactic:
simpa [limit.lift_π] using J0

Premises used: CategoryTheory.Limits.limit.lift_π
-- 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
F : Functor.{0, v, 0, u} WalkingParallelPair C
c : Cone F
m : c.pt ⟶ (equalizerCone F).pt
J : ∀ (j : WalkingParallelPair), m ≫ (equalizerCone F).π.app j = c.π.app j
J0 : m ≫ (equalizerCone F).π.app WalkingParallelPair.zero = c.π.app WalkingParallelPair.zero
⊢ m ≫
      pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
        (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) =
    CategoryStruct.comp (Y :=
      pullback (Z := prod.{v, u} (F.obj WalkingParallelPair.zero) (F.obj WalkingParallelPair.one))
        (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
        (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)))
      (pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯ :
        c.pt ⟶
          pullback (Z := prod.{v, u} (F.obj WalkingParallelPair.zero) (F.obj WalkingParallelPair.one))
            (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
            (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)))
      (pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) :
        pullback (Z := prod.{v, u} (F.obj WalkingParallelPair.zero) (F.obj WalkingParallelPair.one))
            (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
            (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)) ⟶
          F.obj WalkingParallelPair.zero)

Tactic:
simp [← J0, pullbackFst_eq_pullback_snd]

Premises used: CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.pullbackFst_eq_pullback_snd
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
⊢ HasEqualizers.{v, u} C

Tactic:
{ has_limit := fun F =>
      HasLimit.mk
        { cone := equalizerCone F
          isLimit := equalizerConeIsLimit F } }

Premises used: CategoryTheory.Limits.HasLimitsOfShape.mk, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.equalizerConeIsLimit, CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.equalizerCone, CategoryTheory.Limits.LimitCone.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 : 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)
refine_1 refine_2 : c.pt ⟶ G.obj (K.obj WalkingParallelPair.zero)
refine_3 :
  Eq (α := c.pt ⟶ G.obj (prod.{v, u} (K.obj WalkingParallelPair.zero) (K.obj WalkingParallelPair.one)))
    (c.π.app WalkingParallelPair.zero ≫
      G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)))
    (c.π.app WalkingParallelPair.zero ≫
      G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right)))
⊢ c.pt ⟶ (G.mapCone (equalizerCone K)).pt

Tactic:
refine pullback.lift ?_ ?_ ?_ ≫ (PreservesPullback.iso _ _ _ ).inv

Premises used: CategoryTheory.Limits.pullback.lift, CategoryTheory.Limits.PreservesPullback.iso, 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 : 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.pt ⟶ G.obj (K.obj WalkingParallelPair.zero)

Tactic:
exact c.π.app WalkingParallelPair.zero

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.NatTrans.app, CategoryTheory.Limits.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
c : Cone (K ⋙ G)
refine_3 :
  ∀ (j : Discrete WalkingPair),
    Eq (α :=
      c.pt ⟶
        Functor.obj.{0, v', 0, u'}
          (pair (G.obj (K.obj WalkingParallelPair.zero)) (G.obj (K.obj WalkingParallelPair.one))) j)
      (CategoryStruct.comp (Y :=
        Cone.pt (F := pair (G.obj (K.obj WalkingParallelPair.zero)) (G.obj (K.obj WalkingParallelPair.one)))
          (BinaryFan.mk (P := G.obj (prod.{v, u} (K.obj WalkingParallelPair.zero) (K.obj WalkingParallelPair.one)))
            (G.map prod.fst) (G.map prod.snd)))
        (c.π.app WalkingParallelPair.zero ≫
          G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)))
        (NatTrans.app
          (Cone.π
            (BinaryFan.mk (P := G.obj (prod.{v, u} (K.obj WalkingParallelPair.zero) (K.obj WalkingParallelPair.one)))
              (G.map prod.fst) (G.map prod.snd)))
          j))
      (CategoryStruct.comp (Y :=
        Cone.pt (F := pair (G.obj (K.obj WalkingParallelPair.zero)) (G.obj (K.obj WalkingParallelPair.one)))
          (BinaryFan.mk (P := G.obj (prod.{v, u} (K.obj WalkingParallelPair.zero) (K.obj WalkingParallelPair.one)))
            (G.map prod.fst) (G.map prod.snd)))
        (c.π.app WalkingParallelPair.zero ≫
          G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right)))
        (NatTrans.app
          (Cone.π
            (BinaryFan.mk (P := G.obj (prod.{v, u} (K.obj WalkingParallelPair.zero) (K.obj WalkingParallelPair.one)))
              (G.map prod.fst) (G.map prod.snd)))
          j))
⊢ Eq (α := c.pt ⟶ G.obj (prod.{v, u} (K.obj WalkingParallelPair.zero) (K.obj WalkingParallelPair.one)))
    (c.π.app WalkingParallelPair.zero ≫
      G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)))
    (c.π.app WalkingParallelPair.zero ≫
      G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right)))

Tactic:
apply (mapIsLimitOfPreservesOfIsLimit G _ _ (prodIsProd _ _)).hom_ext

Premises used: CategoryTheory.Limits.prodIsProd, CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.Limits.mapIsLimitOfPreservesOfIsLimit
-- 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)
⊢ Eq (α :=
    c.pt ⟶
      Functor.obj.{0, v', 0, u'} (pair (G.obj (K.obj WalkingParallelPair.zero)) (G.obj (K.obj WalkingParallelPair.one)))
        { as := WalkingPair.left : Discrete WalkingPair })
    (CategoryStruct.comp (Y :=
      Cone.pt (F := pair (G.obj (K.obj WalkingParallelPair.zero)) (G.obj (K.obj WalkingParallelPair.one)))
        (BinaryFan.mk (P := G.obj (prod.{v, u} (K.obj WalkingParallelPair.zero) (K.obj WalkingParallelPair.one)))
          (G.map prod.fst) (G.map prod.snd)))
      (c.π.app WalkingParallelPair.zero ≫
        G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)))
      (NatTrans.app
        (Cone.π
          (BinaryFan.mk (P := G.obj (prod.{v, u} (K.obj WalkingParallelPair.zero) (K.obj WalkingParallelPair.one)))
            (G.map prod.fst) (G.map prod.snd)))
        { as := WalkingPair.left }))
    (CategoryStruct.comp (Y :=
      Cone.pt (F := pair (G.obj (K.obj WalkingParallelPair.zero)) (G.obj (K.obj WalkingParallelPair.one)))
        (BinaryFan.mk (P := G.obj (prod.{v, u} (K.obj WalkingParallelPair.zero) (K.obj WalkingParallelPair.one)))
          (G.map prod.fst) (G.map prod.snd)))
      (c.π.app WalkingParallelPair.zero ≫
        G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right)))
      (NatTrans.app
        (Cone.π
          (BinaryFan.mk (P := G.obj (prod.{v, u} (K.obj WalkingParallelPair.zero) (K.obj WalkingParallelPair.one)))
            (G.map prod.fst) (G.map prod.snd)))
        { as := WalkingPair.left }))

Tactic:
simp only [Category.assoc, ← G.map_comp, prod.lift_fst, BinaryFan.π_app_left,
              BinaryFan.mk_fst]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.prod.lift_fst, CategoryTheory.Limits.BinaryFan.mk_fst, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.BinaryFan.π_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 : 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)
refine_3 :
  c.π.app WalkingParallelPair.zero ≫ G.map (K.map WalkingParallelPairHom.left) =
    c.π.app WalkingParallelPair.zero ≫ G.map (K.map WalkingParallelPairHom.right)
⊢ Eq (α :=
    c.pt ⟶
      Functor.obj.{0, v', 0, u'} (pair (G.obj (K.obj WalkingParallelPair.zero)) (G.obj (K.obj WalkingParallelPair.one)))
        { as := WalkingPair.right : Discrete WalkingPair })
    (CategoryStruct.comp (Y :=
      Cone.pt (F := pair (G.obj (K.obj WalkingParallelPair.zero)) (G.obj (K.obj WalkingParallelPair.one)))
        (BinaryFan.mk (P := G.obj (prod.{v, u} (K.obj WalkingParallelPair.zero) (K.obj WalkingParallelPair.one)))
          (G.map prod.fst) (G.map prod.snd)))
      (c.π.app WalkingParallelPair.zero ≫
        G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left)))
      (NatTrans.app
        (Cone.π
          (BinaryFan.mk (P := G.obj (prod.{v, u} (K.obj WalkingParallelPair.zero) (K.obj WalkingParallelPair.one)))
            (G.map prod.fst) (G.map prod.snd)))
        { as := WalkingPair.right }))
    (CategoryStruct.comp (Y :=
      Cone.pt (F := pair (G.obj (K.obj WalkingParallelPair.zero)) (G.obj (K.obj WalkingParallelPair.one)))
        (BinaryFan.mk (P := G.obj (prod.{v, u} (K.obj WalkingParallelPair.zero) (K.obj WalkingParallelPair.one)))
          (G.map prod.fst) (G.map prod.snd)))
      (c.π.app WalkingParallelPair.zero ≫
        G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right)))
      (NatTrans.app
        (Cone.π
          (BinaryFan.mk (P := G.obj (prod.{v, u} (K.obj WalkingParallelPair.zero) (K.obj WalkingParallelPair.one)))
            (G.map prod.fst) (G.map prod.snd)))
        { as := WalkingPair.right }))

Tactic:
simp only [BinaryFan.π_app_right, BinaryFan.mk_snd, Category.assoc, ← G.map_comp,
              prod.lift_snd]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.BinaryFan.π_app_right, CategoryTheory.Limits.BinaryFan.mk_snd, CategoryTheory.Limits.prod.lift_snd, CategoryTheory.Functor.map_comp