awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasBinaryProducts.{v, u} C
inst_2 : HasPullbacks.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
h :
  Eq (α := constructEqualizer F ⟶ F.obj WalkingParallelPair.zero) (pullbackFst F)
    (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.fst)
⊢ Eq (α := constructEqualizer F ⟶ F.obj WalkingParallelPair.zero) (pullbackFst F)
    (pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
      (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right)))
have h₁ : Eq (α := constructEqualizer F ⟶ F.obj WalkingParallelPair.zero)
  (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 := 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.fst)
Tactic: convert!
    (eq_whisker pullback.condition Limits.prod.fst :
      (_ : constructEqualizer F ⟶ F.obj WalkingParallelPair.zero) = _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Equalizers (goal)
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
| pullbackFst F ≫ F.map WalkingParallelPairHom.right
have 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
Tactic: rw [pullbackFst_eq_pullback_snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Equalizers (goal)
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)
    (pullbackFst F ≫ F.map WalkingParallelPairHom.right)
have 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)
Tactic: conv_rhs => rw [pullbackFst_eq_pullback_snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Equalizers (goal)
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)
    (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)
have 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)
Tactic: convert!
          (eq_whisker pullback.condition Limits.prod.snd :
            (_ : constructEqualizer F ⟶ F.obj WalkingParallelPair.one) = _) using
          1
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Equalizers (goal)
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)
⊢ 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)
have 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)
Tactic: convert!
          (eq_whisker pullback.condition Limits.prod.snd :
            (_ : constructEqualizer F ⟶ F.obj WalkingParallelPair.one) = _) using
          1
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Equalizers (hypothesis)
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 = pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯
have J0 : m ≫ (equalizerCone F).π.app WalkingParallelPair.zero = c.π.app WalkingParallelPair.zero
Tactic: have J0 := J WalkingParallelPair.zero
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Equalizers (goal)
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.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯
have h₀ : 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) sorry :
      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: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Equalizers (goal)
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.mapCone (equalizerCone K)).pt
have refine_1 : c.pt ⟶ G.obj (K.obj WalkingParallelPair.zero)
Tactic: refine pullback.lift ?_ ?_ ?_ ≫ (PreservesPullback.iso _ _ _ ).inv
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Equalizers (goal)
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)
⊢ c.pt ⟶ (G.mapCone (equalizerCone K)).pt
have 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)))
Tactic: refine pullback.lift ?_ ?_ ?_ ≫ (PreservesPullback.iso _ _ _ ).inv
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Equalizers (goal)
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 ⟶ 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)))
have 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))
Tactic: apply (mapIsLimitOfPreservesOfIsLimit G _ _ (prodIsProd _ _)).hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Equalizers (goal)
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.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 }))
have refine_3 : c.π.app WalkingParallelPair.zero ≫ G.map (K.map WalkingParallelPairHom.left) =
  c.π.app WalkingParallelPair.zero ≫ G.map (K.map WalkingParallelPairHom.right)
Tactic: simp only [BinaryFan.π_app_right, BinaryFan.mk_snd, Category.assoc, ← G.map_comp,
              prod.lift_snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Equalizers (goal)
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
⊢ 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
have 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) sorry)
      (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: rcases j with (_ | _)
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Equalizers (goal)
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
⊢ 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
have 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) sorry)
      (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: rcases j with (_ | _)
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Equalizers (goal)
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.one =
    c.π.app WalkingParallelPair.one
have one : c.π.app WalkingParallelPair.zero ≫ G.map (K.map WalkingParallelPairHom.left) = 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Equalizers (goal)
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 =
    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))))
have 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) sorry)
Tactic: rw [Iso.eq_comp_inv]