-- 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:
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 : WalkingParallelPair
⊢ (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)
        c ≫
      (G.mapCone (equalizerCone K)).π.app j =
    c.π.app j

Tactic:
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]

Result:
case one
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.one

Proof state:
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 }

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

Result:
no goals

Proof state:
case refine_1
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.pt ⟶ G.obj (K.obj WalkingParallelPair.zero)

Tactic:
exact c.π.app WalkingParallelPair.zero

Result:
no goals

Proof state:
case refine_2
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.pt ⟶ G.obj (K.obj WalkingParallelPair.zero)

Tactic:
exact c.π.app WalkingParallelPair.zero

Result:
no goals

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 (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 }

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

Result:
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)