-- Mathlib/CategoryTheory/Limits/Constructions/LimitsOfProductsAndEqualizers.lean
/-- If G preserves terminal objects and pullbacks, it preserves all finite limits. -/
lemma preservesFiniteLimits_of_preservesTerminal_and_pullbacks [HasTerminal C]
    [HasPullbacks C] (G : C ⥤ D) [PreservesLimitsOfShape (Discrete.{0} PEmpty) G]
    [PreservesLimitsOfShape WalkingCospan G] : PreservesFiniteLimits G

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
G : C ⥤ D
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
⊢ PreservesFiniteLimits G

Tactic:
haveI : HasFiniteLimits C := hasFiniteLimits_of_hasTerminal_and_pullbacks

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
G : C ⥤ D
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
this : HasFiniteLimits C
⊢ PreservesFiniteLimits G

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
G : C ⥤ D
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
this✝ : HasFiniteLimits C
this : PreservesLimitsOfShape (Discrete WalkingPair) G
⊢ PreservesFiniteLimits G

Tactic:
haveI : PreservesLimitsOfShape WalkingParallelPair G :=
    preservesEqualizers_of_preservesPullbacks_and_binaryProducts G

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
G : C ⥤ D
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
this✝¹ : HasFiniteLimits C
this✝ : PreservesLimitsOfShape (Discrete WalkingPair) G
this : PreservesLimitsOfShape WalkingParallelPair G
⊢ PreservesFiniteLimits G

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
G : C ⥤ D
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
this✝¹ : HasFiniteLimits C
this✝ : PreservesLimitsOfShape (Discrete WalkingPair) G
this : PreservesLimitsOfShape WalkingParallelPair G
⊢ PreservesFiniteProducts G

Tactic:
refine ⟨fun n ↦ ?_⟩

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
G : C ⥤ D
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
this✝¹ : HasFiniteLimits C
this✝ : PreservesLimitsOfShape (Discrete WalkingPair) G
this : PreservesLimitsOfShape WalkingParallelPair G
n : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin n)) G

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
G : C ⥤ D
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
this✝¹ : HasFiniteLimits C
this✝ : PreservesLimitsOfShape (Discrete WalkingPair) G
this : PreservesLimitsOfShape WalkingParallelPair G
n : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin n)) G

Tactic:
apply preservesFiniteProducts_of_preserves_binary_and_terminal G

Result:
no goals

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
G : C ⥤ D
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
this : HasFiniteLimits C
⊢ PreservesFiniteLimits G

Tactic:
haveI : PreservesLimitsOfShape (Discrete WalkingPair) G :=
  preservesBinaryProducts_of_preservesTerminal_and_pullbacks G

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
G : C ⥤ D
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
this✝ : HasFiniteLimits C
this : PreservesLimitsOfShape (Discrete WalkingPair) G
⊢ PreservesFiniteLimits G

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
G : C ⥤ D
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
this✝¹ : HasFiniteLimits C
this✝ : PreservesLimitsOfShape (Discrete WalkingPair) G
this : PreservesLimitsOfShape WalkingParallelPair G
⊢ PreservesFiniteLimits G

Tactic:
apply
  @preservesFiniteLimits_of_preservesEqualizers_and_finiteProducts _ _ _ _ _ _ G _ ?_

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
G : C ⥤ D
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) G
inst✝ : PreservesLimitsOfShape WalkingCospan G
this✝¹ : HasFiniteLimits C
this✝ : PreservesLimitsOfShape (Discrete WalkingPair) G
this : PreservesLimitsOfShape WalkingParallelPair G
⊢ PreservesFiniteProducts G