-- Mathlib/CategoryTheory/Monad/Limits.lean
theorem hasLimitsOfShape_of_coreflective (R : D ⥤ C) [Coreflective R] [HasLimitsOfShape J C] :
    HasLimitsOfShape J D where
  has_limit := fun F => by
      let c := (comonadicRightAdjoint R).mapCone (limit.cone (F ⋙ R))
      letI : PreservesLimitsOfShape J _ :=
        (comonadicAdjunction R).rightAdjoint_preservesLimits.1
      let t : IsLimit c := isLimitOfPreserves (comonadicRightAdjoint R) (limit.isLimit _)
      apply HasLimit.mk ⟨_, (IsLimit.postcomposeHomEquiv _ _).symm t⟩
      apply
        (F.rightUnitor ≪≫ (isoWhiskerLeft F ((asIso (comonadicAdjunction R).unit) :) )).symm

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
R : D ⥤ C
inst✝¹ : Coreflective R
inst✝ : HasLimitsOfShape J C
F : J ⥤ D
c : Cone ((F ⋙ R) ⋙ comonadicRightAdjoint R) := (comonadicRightAdjoint R).mapCone (limit.cone (F ⋙ R))
this : PreservesLimitsOfShape J (comonadicRightAdjoint R) := PreservesLimitsOfSize.preservesLimitsOfShape
⊢ HasLimit F

Tactic:
let t : IsLimit c := isLimitOfPreserves (comonadicRightAdjoint R) (limit.isLimit _)

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type u
inst✝² : Category.{v, u} J
R : D ⥤ C
inst✝¹ : Coreflective R
inst✝ : HasLimitsOfShape J C
F : J ⥤ D
c : Cone ((F ⋙ R) ⋙ comonadicRightAdjoint R) := (comonadicRightAdjoint R).mapCone (limit.cone (F ⋙ R))
this : PreservesLimitsOfShape J (comonadicRightAdjoint R) := PreservesLimitsOfSize.preservesLimitsOfShape
t : IsLimit c := isLimitOfPreserves (comonadicRightAdjoint R) (limit.isLimit (F ⋙ R))
⊢ HasLimit F

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
R : D ⥤ C
inst✝¹ : Coreflective R
inst✝ : HasLimitsOfShape J C
F : J ⥤ D
c : Cone ((F ⋙ R) ⋙ comonadicRightAdjoint R) := (comonadicRightAdjoint R).mapCone (limit.cone (F ⋙ R))
this : PreservesLimitsOfShape J (comonadicRightAdjoint R) := PreservesLimitsOfSize.preservesLimitsOfShape
t : IsLimit c := isLimitOfPreserves (comonadicRightAdjoint R) (limit.isLimit (F ⋙ R))
⊢ (F ⋙ R) ⋙ comonadicRightAdjoint R ≅ F

Tactic:
apply
  (F.rightUnitor ≪≫ (isoWhiskerLeft F ((asIso (comonadicAdjunction R).unit) :) )).symm

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
R : D ⥤ C
inst✝¹ : Coreflective R
inst✝ : HasLimitsOfShape J C
F : J ⥤ D
⊢ HasLimit F

Tactic:
let c := (comonadicRightAdjoint R).mapCone (limit.cone (F ⋙ R))

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type u
inst✝² : Category.{v, u} J
R : D ⥤ C
inst✝¹ : Coreflective R
inst✝ : HasLimitsOfShape J C
F : J ⥤ D
c : Cone ((F ⋙ R) ⋙ comonadicRightAdjoint R) := (comonadicRightAdjoint R).mapCone (limit.cone (F ⋙ R))
⊢ HasLimit F

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
R : D ⥤ C
inst✝¹ : Coreflective R
inst✝ : HasLimitsOfShape J C
F : J ⥤ D
c : Cone ((F ⋙ R) ⋙ comonadicRightAdjoint R) := (comonadicRightAdjoint R).mapCone (limit.cone (F ⋙ R))
⊢ HasLimit F

Tactic:
letI : PreservesLimitsOfShape J _ :=
  (comonadicAdjunction R).rightAdjoint_preservesLimits.1

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type u
inst✝² : Category.{v, u} J
R : D ⥤ C
inst✝¹ : Coreflective R
inst✝ : HasLimitsOfShape J C
F : J ⥤ D
c : Cone ((F ⋙ R) ⋙ comonadicRightAdjoint R) := (comonadicRightAdjoint R).mapCone (limit.cone (F ⋙ R))
this : PreservesLimitsOfShape J (comonadicRightAdjoint R) := PreservesLimitsOfSize.preservesLimitsOfShape
⊢ HasLimit F

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
R : D ⥤ C
inst✝¹ : Coreflective R
inst✝ : HasLimitsOfShape J C
F : J ⥤ D
c : Cone ((F ⋙ R) ⋙ comonadicRightAdjoint R) := (comonadicRightAdjoint R).mapCone (limit.cone (F ⋙ R))
this : PreservesLimitsOfShape J (comonadicRightAdjoint R) := PreservesLimitsOfSize.preservesLimitsOfShape
t : IsLimit c := isLimitOfPreserves (comonadicRightAdjoint R) (limit.isLimit (F ⋙ R))
⊢ HasLimit F

Tactic:
apply HasLimit.mk ⟨_, (IsLimit.postcomposeHomEquiv _ _).symm t⟩

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type u
inst✝² : Category.{v, u} J
R : D ⥤ C
inst✝¹ : Coreflective R
inst✝ : HasLimitsOfShape J C
F : J ⥤ D
c : Cone ((F ⋙ R) ⋙ comonadicRightAdjoint R) := (comonadicRightAdjoint R).mapCone (limit.cone (F ⋙ R))
this : PreservesLimitsOfShape J (comonadicRightAdjoint R) := PreservesLimitsOfSize.preservesLimitsOfShape
t : IsLimit c := isLimitOfPreserves (comonadicRightAdjoint R) (limit.isLimit (F ⋙ R))
⊢ (F ⋙ R) ⋙ comonadicRightAdjoint R ≅ F