-- Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean
/-- `F : D ⥤ K ⥤ C` preserves the limit of some `G : J ⥤ D` if it does for each `k : K`. -/
lemma preservesLimit_of_evaluation (F : D ⥤ K ⥤ C) (G : J ⥤ D)
    (H : ∀ k : K, PreservesLimit G (F ⋙ (evaluation K C).obj k : D ⥤ C)) : PreservesLimit G F :=
  ⟨fun {c} hc => ⟨by
    apply evaluationJointlyReflectsLimits
    intro X
    haveI := H X
    change IsLimit ((F ⋙ (evaluation K C).obj X).mapCone c)
    exact isLimitOfPreserves _ hc⟩⟩

Proof state:
case t
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : D ⥤ K ⥤ C
G : J ⥤ D
H : ∀ (k : K), PreservesLimit G (F ⋙ (evaluation K C).obj k)
c : Cone G
hc : IsLimit c
X : K
⊢ IsLimit (((evaluation K C).obj X).mapCone (F.mapCone c))

Tactic:
haveI := H X

Result:
case t
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : D ⥤ K ⥤ C
G : J ⥤ D
H : ∀ (k : K), PreservesLimit G (F ⋙ (evaluation K C).obj k)
c : Cone G
hc : IsLimit c
X : K
this : PreservesLimit G (F ⋙ (evaluation K C).obj X)
⊢ IsLimit (((evaluation K C).obj X).mapCone (F.mapCone c))

Proof state:
case t
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : D ⥤ K ⥤ C
G : J ⥤ D
H : ∀ (k : K), PreservesLimit G (F ⋙ (evaluation K C).obj k)
c : Cone G
hc : IsLimit c
X : K
this : PreservesLimit G (F ⋙ (evaluation K C).obj X)
⊢ IsLimit ((F ⋙ (evaluation K C).obj X).mapCone c)

Tactic:
exact isLimitOfPreserves _ hc

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : D ⥤ K ⥤ C
G : J ⥤ D
H : ∀ (k : K), PreservesLimit G (F ⋙ (evaluation K C).obj k)
c : Cone G
hc : IsLimit c
⊢ IsLimit (F.mapCone c)

Tactic:
apply evaluationJointlyReflectsLimits

Result:
case t
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : D ⥤ K ⥤ C
G : J ⥤ D
H : ∀ (k : K), PreservesLimit G (F ⋙ (evaluation K C).obj k)
c : Cone G
hc : IsLimit c
⊢ (k : K) → IsLimit (((evaluation K C).obj k).mapCone (F.mapCone c))

Proof state:
case t
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : D ⥤ K ⥤ C
G : J ⥤ D
H : ∀ (k : K), PreservesLimit G (F ⋙ (evaluation K C).obj k)
c : Cone G
hc : IsLimit c
X : K
this : PreservesLimit G (F ⋙ (evaluation K C).obj X)
⊢ IsLimit (((evaluation K C).obj X).mapCone (F.mapCone c))

Tactic:
change IsLimit ((F ⋙ (evaluation K C).obj X).mapCone c)

Result:
case t
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : D ⥤ K ⥤ C
G : J ⥤ D
H : ∀ (k : K), PreservesLimit G (F ⋙ (evaluation K C).obj k)
c : Cone G
hc : IsLimit c
X : K
this : PreservesLimit G (F ⋙ (evaluation K C).obj X)
⊢ IsLimit ((F ⋙ (evaluation K C).obj X).mapCone c)

Proof state:
case t
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : D ⥤ K ⥤ C
G : J ⥤ D
H : ∀ (k : K), PreservesLimit G (F ⋙ (evaluation K C).obj k)
c : Cone G
hc : IsLimit c
⊢ (k : K) → IsLimit (((evaluation K C).obj k).mapCone (F.mapCone c))

Tactic:
intro X

Result:
case t
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
F : D ⥤ K ⥤ C
G : J ⥤ D
H : ∀ (k : K), PreservesLimit G (F ⋙ (evaluation K C).obj k)
c : Cone G
hc : IsLimit c
X : K
⊢ IsLimit (((evaluation K C).obj X).mapCone (F.mapCone c))