-- Mathlib/CategoryTheory/Limits/Constructions/BinaryProducts.lean
/-- A functor that preserves terminal objects and pullbacks preserves binary products. -/
lemma preservesBinaryProducts_of_preservesTerminal_and_pullbacks [HasTerminal C]
    [HasPullbacks C] [PreservesLimitsOfShape (Discrete.{0} PEmpty) F]
    [PreservesLimitsOfShape WalkingCospan F] : PreservesLimitsOfShape (Discrete WalkingPair) F :=
  ⟨fun {K} =>
    preservesLimit_of_preserves_limit_cone (limitConeOfTerminalAndPullbacks K).2
      (by
        apply
          isBinaryProductOfIsTerminalIsPullback _ _ (isLimitOfHasTerminalOfPreservesLimit F)
        apply isLimitOfHasPullbackOfPreservesLimit)⟩

Proof state:
case hc
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : PreservesLimitsOfShape WalkingCospan F
K : Discrete WalkingPair ⥤ C
⊢ IsLimit
    (PullbackCone.mk ((F.mapCone (limitConeOfTerminalAndPullbacks K).cone).π.app { as := WalkingPair.left })
      ((F.mapCone (limitConeOfTerminalAndPullbacks K).cone).π.app { as := WalkingPair.right }) ⋯)

case f
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : PreservesLimitsOfShape WalkingCospan F
K : Discrete WalkingPair ⥤ C
⊢ (K ⋙ F).obj { as := WalkingPair.left } ⟶ F.obj (⊤_ C)

case g
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : PreservesLimitsOfShape WalkingCospan F
K : Discrete WalkingPair ⥤ C
⊢ (K ⋙ F).obj { as := WalkingPair.right } ⟶ F.obj (⊤_ C)

Tactic:
apply isLimitOfHasPullbackOfPreservesLimit

Result:
no goals

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : PreservesLimitsOfShape WalkingCospan F
K : Discrete WalkingPair ⥤ C
⊢ IsLimit (F.mapCone (limitConeOfTerminalAndPullbacks K).cone)

Tactic:
apply
  isBinaryProductOfIsTerminalIsPullback _ _ (isLimitOfHasTerminalOfPreservesLimit F)

Result:
case hc
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : PreservesLimitsOfShape WalkingCospan F
K : Discrete WalkingPair ⥤ C
⊢ IsLimit
    (PullbackCone.mk ((F.mapCone (limitConeOfTerminalAndPullbacks K).cone).π.app { as := WalkingPair.left })
      ((F.mapCone (limitConeOfTerminalAndPullbacks K).cone).π.app { as := WalkingPair.right }) ⋯)

case f
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : PreservesLimitsOfShape WalkingCospan F
K : Discrete WalkingPair ⥤ C
⊢ (K ⋙ F).obj { as := WalkingPair.left } ⟶ F.obj (⊤_ C)

case g
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
inst✝³ : HasTerminal C
inst✝² : HasPullbacks C
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : PreservesLimitsOfShape WalkingCospan F
K : Discrete WalkingPair ⥤ C
⊢ (K ⋙ F).obj { as := WalkingPair.right } ⟶ F.obj (⊤_ C)