-- Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean
/-- If G preserves initial objects and pushouts, it preserves all finite colimits. -/
lemma preservesFiniteColimits_of_preservesInitial_and_pushouts [HasInitial C]
    [HasPushouts C] (G : C ⥤ D) [PreservesColimitsOfShape (Discrete.{0} PEmpty) G]
    [PreservesColimitsOfShape WalkingSpan G] : PreservesFiniteColimits G

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasInitial C
inst✝² : HasPushouts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
this✝ : HasFiniteColimits C
this : PreservesColimitsOfShape (Discrete WalkingPair) G
⊢ PreservesFiniteColimits G

Tactic:
haveI : PreservesColimitsOfShape (WalkingParallelPair) G :=
    (preservesCoequalizers_of_preservesPushouts_and_binaryCoproducts G)

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasInitial C
inst✝² : HasPushouts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
this✝¹ : HasFiniteColimits C
this✝ : PreservesColimitsOfShape (Discrete WalkingPair) G
this : PreservesColimitsOfShape WalkingParallelPair G
⊢ PreservesFiniteColimits G

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasInitial C
inst✝² : HasPushouts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
this✝¹ : HasFiniteColimits C
this✝ : PreservesColimitsOfShape (Discrete WalkingPair) G
this : PreservesColimitsOfShape WalkingParallelPair G
⊢ PreservesFiniteColimits G

Tactic:
refine
  @preservesFiniteColimits_of_preservesCoequalizers_and_finiteCoproducts _ _ _ _ _ _ G _ ?_

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasInitial C
inst✝² : HasPushouts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
this✝¹ : HasFiniteColimits C
this✝ : PreservesColimitsOfShape (Discrete WalkingPair) G
this : PreservesColimitsOfShape WalkingParallelPair G
⊢ PreservesFiniteCoproducts G

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasInitial C
inst✝² : HasPushouts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
this : HasFiniteColimits C
⊢ PreservesFiniteColimits G

Tactic:
haveI : PreservesColimitsOfShape (Discrete WalkingPair) G :=
  preservesBinaryCoproducts_of_preservesInitial_and_pushouts G

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasInitial C
inst✝² : HasPushouts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
this✝ : HasFiniteColimits C
this : PreservesColimitsOfShape (Discrete WalkingPair) G
⊢ PreservesFiniteColimits G

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasInitial C
inst✝² : HasPushouts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
⊢ PreservesFiniteColimits G

Tactic:
haveI : HasFiniteColimits C := hasFiniteColimits_of_hasInitial_and_pushouts

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasInitial C
inst✝² : HasPushouts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
this : HasFiniteColimits C
⊢ PreservesFiniteColimits G

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasInitial C
inst✝² : HasPushouts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
this✝¹ : HasFiniteColimits C
this✝ : PreservesColimitsOfShape (Discrete WalkingPair) G
this : PreservesColimitsOfShape WalkingParallelPair G
x✝ : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x✝)) G

Tactic:
apply preservesFiniteCoproductsOfPreservesBinaryAndInitial G

Result:
no goals

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasInitial C
inst✝² : HasPushouts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
this✝¹ : HasFiniteColimits C
this✝ : PreservesColimitsOfShape (Discrete WalkingPair) G
this : PreservesColimitsOfShape WalkingParallelPair G
⊢ PreservesFiniteCoproducts G

Tactic:
refine ⟨fun _ ↦ ?_⟩

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasInitial C
inst✝² : HasPushouts C
G : C ⥤ D
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) G
inst✝ : PreservesColimitsOfShape WalkingSpan G
this✝¹ : HasFiniteColimits C
this✝ : PreservesColimitsOfShape (Discrete WalkingPair) G
this : PreservesColimitsOfShape WalkingParallelPair G
x✝ : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x✝)) G