-- Mathlib/CategoryTheory/Limits/Constructions/Equalizers.lean
/-- A functor that preserves pushouts and binary coproducts also presrves coequalizers. -/
lemma preservesCoequalizers_of_preservesPushouts_and_binaryCoproducts [HasBinaryCoproducts C]
    [HasPushouts C] [PreservesColimitsOfShape (Discrete WalkingPair) G]
    [PreservesColimitsOfShape WalkingSpan G] : PreservesColimitsOfShape WalkingParallelPair G :=
  ⟨fun {K} =>
    preservesColimit_of_preserves_colimit_cocone (coequalizerCoconeIsColimit K) <|
      { desc := fun c => by
          refine (PreservesPushout.iso _ _ _).inv ≫ pushout.desc ?_ ?_ ?_
          · exact c.ι.app WalkingParallelPair.one
          · exact c.ι.app WalkingParallelPair.one
          apply (mapIsColimitOfPreservesOfIsColimit G _ _ (coprodIsCoprod _ _)).hom_ext
          rintro (_ | _)
          · simp only [BinaryCofan.ι_app_left, BinaryCofan.mk_inl, Category.assoc, ←
              G.map_comp_assoc, coprod.inl_desc]
          · simp only [BinaryCofan.ι_app_right, BinaryCofan.mk_inr, Category.assoc, ←
              G.map_comp_assoc, coprod.inr_desc]
            exact
              (c.ι.naturality WalkingParallelPairHom.left).trans
                (c.ι.naturality WalkingParallelPairHom.right).symm
        fac := fun c j => by
          rcases j with (_ | _) <;>
            simp only [Functor.mapCocone_ι_app, Cocone.ofCofork_ι, Category.id_comp,
              eqToHom_refl, Category.assoc, Functor.map_comp, Cofork.ofπ_ι_app, pushout.inl_desc,
              PreservesPushout.inl_iso_inv_assoc]
          exact (c.ι.naturality WalkingParallelPairHom.left).trans (Category.comp_id _)
        uniq := fun s m h => by
          rw [Iso.eq_inv_comp]
          have := h WalkingParallelPair.one
          dsimp [coequalizerCocone] at this
          ext <;>
            simp only [PreservesPushout.inl_iso_hom_assoc, Category.id_comp, pushout.inl_desc,
              pushout.inr_desc, PreservesPushout.inr_iso_hom_assoc, ← pushoutInl_eq_pushout_inr, ←
              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✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
⊢ G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)) ≫
      c.ι.app WalkingParallelPair.one =
    G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right)) ≫
      c.ι.app WalkingParallelPair.one

Tactic:
apply (mapIsColimitOfPreservesOfIsColimit G _ _ (coprodIsCoprod _ _)).hom_ext

Result:
case refine_3
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
⊢ ∀ (j : Discrete WalkingPair),
    (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr)).ι.app j ≫
        G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)) ≫
          c.ι.app WalkingParallelPair.one =
      (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr)).ι.app j ≫
        G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right)) ≫
          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✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
⊢ (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr)).ι.app { as := WalkingPair.left } ≫
      G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left)) ≫
        c.ι.app WalkingParallelPair.one =
    (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr)).ι.app { as := WalkingPair.left } ≫
      G.map (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right)) ≫
        c.ι.app WalkingParallelPair.one

Tactic:
simp only [BinaryCofan.ι_app_left, BinaryCofan.mk_inl, Category.assoc, ←
  G.map_comp_assoc, coprod.inl_desc]

Result:
no goals

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
j : WalkingParallelPair
⊢ (G.mapCocone (coequalizerCocone K)).ι.app j ≫
      (fun c =>
          (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
                (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))).inv ≫
            pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯)
        c =
    c.ι.app j

Tactic:
rcases j with (_ | _) <;>
  simp only [Functor.mapCocone_ι_app, Cocone.ofCofork_ι, Category.id_comp,
    eqToHom_refl, Category.assoc, Functor.map_comp, Cofork.ofπ_ι_app, pushout.inl_desc,
    PreservesPushout.inl_iso_inv_assoc]

Result:
case zero
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
c : Cocone (K ⋙ G)
⊢ G.map (K.map WalkingParallelPairHom.left) ≫ c.ι.app WalkingParallelPair.one = c.ι.app WalkingParallelPair.zero

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
s : Cocone (K ⋙ G)
m : (G.mapCocone (coequalizerCocone K)).pt ⟶ s.pt
h : ∀ (j : WalkingParallelPair), (G.mapCocone (coequalizerCocone K)).ι.app j ≫ m = s.ι.app j
⊢ m =
    (fun c =>
        (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
              (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))).inv ≫
          pushout.desc (c.ι.app WalkingParallelPair.one) (c.ι.app WalkingParallelPair.one) ⋯)
      s

Tactic:
rw [Iso.eq_inv_comp]

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
G : C ⥤ D
inst✝³ : HasBinaryCoproducts C
inst✝² : HasPushouts C
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
K : WalkingParallelPair ⥤ C
s : Cocone (K ⋙ G)
m : (G.mapCocone (coequalizerCocone K)).pt ⟶ s.pt
h : ∀ (j : WalkingParallelPair), (G.mapCocone (coequalizerCocone K)).ι.app j ≫ m = s.ι.app j
⊢ (PreservesPushout.iso G (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.left))
          (coprod.desc (𝟙 (K.obj WalkingParallelPair.one)) (K.map WalkingParallelPairHom.right))).hom ≫
      m =
    pushout.desc (s.ι.app WalkingParallelPair.one) (s.ι.app WalkingParallelPair.one) ⋯