-- Mathlib/CategoryTheory/Limits/Constructions/Equalizers.lean
/-- A functor that preserves pullbacks and binary products also presrves equalizers. -/
lemma preservesEqualizers_of_preservesPullbacks_and_binaryProducts
    [HasBinaryProducts C] [HasPullbacks C]
    [PreservesLimitsOfShape (Discrete WalkingPair) G] [PreservesLimitsOfShape WalkingCospan G] :
    PreservesLimitsOfShape WalkingParallelPair G :=
  ⟨fun {K} =>
    preservesLimit_of_preserves_limit_cone (equalizerConeIsLimit K) <|
      { lift := fun c => by
          refine pullback.lift ?_ ?_ ?_ ≫ (PreservesPullback.iso _ _ _ ).inv
          · exact c.π.app WalkingParallelPair.zero
          · exact c.π.app WalkingParallelPair.zero
          apply (mapIsLimitOfPreservesOfIsLimit G _ _ (prodIsProd _ _)).hom_ext
          rintro (_ | _)
          · simp only [Category.assoc, ← G.map_comp, prod.lift_fst, BinaryFan.π_app_left,
              BinaryFan.mk_fst]
          · simp only [BinaryFan.π_app_right, BinaryFan.mk_snd, Category.assoc, ← G.map_comp,
              prod.lift_snd]
            exact
              (c.π.naturality WalkingParallelPairHom.left).symm.trans
                (c.π.naturality WalkingParallelPairHom.right)
        fac := fun c j => by
          rcases j with (_ | _) <;>
            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]
          exact (c.π.naturality WalkingParallelPairHom.left).symm.trans (Category.id_comp _)
        uniq := fun s m h => by
          rw [Iso.eq_comp_inv]
          have := h WalkingParallelPair.zero
          dsimp [equalizerCone] at this
          ext <;>
            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] }⟩

Proof state:
case refine_3
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ ∀ (j : Discrete WalkingPair),
    (c.π.app WalkingParallelPair.zero ≫
          G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))) ≫
        (BinaryFan.mk (G.map prod.fst) (G.map prod.snd)).π.app j =
      (c.π.app WalkingParallelPair.zero ≫
          G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))) ≫
        (BinaryFan.mk (G.map prod.fst) (G.map prod.snd)).π.app j

Tactic:
rintro (_ | _)

Result:
case refine_3.mk.left
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ (c.π.app WalkingParallelPair.zero ≫
        G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))) ≫
      (BinaryFan.mk (G.map prod.fst) (G.map prod.snd)).π.app { as := WalkingPair.left } =
    (c.π.app WalkingParallelPair.zero ≫
        G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))) ≫
      (BinaryFan.mk (G.map prod.fst) (G.map prod.snd)).π.app { as := WalkingPair.left }

case refine_3.mk.right
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : WalkingParallelPair ⥤ C
c : Cone (K ⋙ G)
⊢ (c.π.app WalkingParallelPair.zero ≫
        G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))) ≫
      (BinaryFan.mk (G.map prod.fst) (G.map prod.snd)).π.app { as := WalkingPair.right } =
    (c.π.app WalkingParallelPair.zero ≫
        G.map (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))) ≫
      (BinaryFan.mk (G.map prod.fst) (G.map prod.snd)).π.app { as := WalkingPair.right }

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : 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 =
    (fun c =>
        pullback.lift (c.π.app WalkingParallelPair.zero) (c.π.app WalkingParallelPair.zero) ⋯ ≫
          (PreservesPullback.iso G (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
              (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))).inv)
      s

Tactic:
rw [Iso.eq_comp_inv]

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : 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 ≫
      (PreservesPullback.iso G (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.left))
          (prod.lift (𝟙 (K.obj WalkingParallelPair.zero)) (K.map WalkingParallelPairHom.right))).hom =
    pullback.lift (s.π.app WalkingParallelPair.zero) (s.π.app WalkingParallelPair.zero) ⋯

Proof state:
case refine_3.mk.right
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryProducts C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
K : 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)

Result:
no goals