-- Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean
/-- If a functor preserves coequalizers and the appropriate coproducts, it preserves colimits. -/
lemma preservesColimit_of_preservesCoequalizers_and_coproduct :
    PreservesColimitsOfShape J G where
  preservesColimit {K}

Proof state:
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.1
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.1 }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
f : (p : J × J) × (p.1 ⟶ p.2)
⊢ (Cofan.mk (G.obj Q) fun j => G.map (Sigma.ι (fun j => K.obj j.fst.1) j)).ι.app { as := f } ≫ G.map s =
    (K ⋙ G).map f.snd ≫ (Cofan.mk (G.obj (∐ K.obj)) fun f => G.map (Sigma.ι K.obj f)).ι.app { as := f.fst.2 }

Tactic:
dsimp [P, Q, s, Cofan.mk]

Result:
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.1
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.1 }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
f : (p : J × J) × (p.1 ⟶ p.2)
⊢ G.map (Sigma.ι (fun j => K.obj j.fst.1) f) ≫
      G.map (Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }) =
    G.map (K.map f.snd) ≫ G.map (Sigma.ι K.obj f.fst.2)

Proof state:
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.1
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.1 }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ Cofan (K ⋙ G).obj

Tactic:
exact Cofan.mk _ fun f => G.map (Sigma.ι _ f)

Result:
no goals

Proof state:
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.1
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.1 }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
f : (p : J × J) × (p.1 ⟶ p.2)
⊢ G.map (Sigma.ι (fun j => K.obj j.fst.1) f) ≫
      G.map (Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.1 }) =
    G.map (Sigma.ι K.obj f.fst.1)

Tactic:
simp only [← G.map_comp, colimit.ι_desc]

Result:
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.1
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.1 }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
f : (p : J × J) × (p.1 ⟶ p.2)
⊢ G.map ((Cofan.mk (∐ K.obj) fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.1 }).ι.app { as := f }) =
    G.map (Sigma.ι K.obj f.fst.1)

Proof state:
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f => K.obj f.fst.1
s : Q ⟶ P := Sigma.desc fun f => K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
t : Q ⟶ P := Sigma.desc fun f => colimit.ι (Discrete.functor K.obj) { as := f.fst.1 }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
j : J
⊢ (G.map (Sigma.ι K.obj j) ≫ G.map (coequalizer.π s t)) ≫ 𝟙 (G.obj (coequalizer s t)) =
    G.map (colimit.ι (Discrete.functor K.obj) { as := j } ≫ coequalizer.π s t)

Tactic:
simp

Result:
no goals