C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
J : Type u
inst✝² : Category J
R : D ⥤ C
inst✝¹ : Reflective R
inst✝ : HasColimitsOfShape J C
F : J ⥤ D
c : Cocone ((F ⋙ R) ⋙ leftAdjoint R) := (leftAdjoint R).mapCocone (colimit.cocone (F ⋙ R))
⊢ HasColimit F
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
J : Type u
inst✝² : Category J
R : D ⥤ C
inst✝¹ : Reflective R
inst✝ : HasColimitsOfShape J C
F : J ⥤ D
⊢ HasColimit F
let c := (leftAdjoint R).mapCocone (colimit.cocone (F ⋙ R))
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
J : Type u
inst✝² : Category J
R : D ⥤ C
inst✝¹ : Reflective R
inst✝ : HasColimitsOfShape J C
F : J ⥤ D
c : Cocone ((F ⋙ R) ⋙ leftAdjoint R) := (leftAdjoint R).mapCocone (colimit.cocone (F ⋙ R))
this : PreservesColimitsOfShape J (leftAdjoint R) := PreservesColimitsOfSize.preservesColimitsOfShape
⊢ HasColimit F
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
J : Type u
inst✝² : Category J
R : D ⥤ C
inst✝¹ : Reflective R
inst✝ : HasColimitsOfShape J C
F : J ⥤ D
c : Cocone ((F ⋙ R) ⋙ leftAdjoint R) := (leftAdjoint R).mapCocone (colimit.cocone (F ⋙ R))
⊢ HasColimit F
letI : PreservesColimitsOfShape J _ :=
  (Adjunction.ofRightAdjoint R).leftAdjointPreservesColimits.1
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
J : Type u
inst✝² : Category J
R : D ⥤ C
inst✝¹ : Reflective R
inst✝ : HasColimitsOfShape J C
F : J ⥤ D
c : Cocone ((F ⋙ R) ⋙ leftAdjoint R) := (leftAdjoint R).mapCocone (colimit.cocone (F ⋙ R))
this : PreservesColimitsOfShape J (leftAdjoint R) := PreservesColimitsOfSize.preservesColimitsOfShape
t : IsColimit c := isColimitOfPreserves (leftAdjoint R) (colimit.isColimit (F ⋙ R))
⊢ HasColimit F
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
J : Type u
inst✝² : Category J
R : D ⥤ C
inst✝¹ : Reflective R
inst✝ : HasColimitsOfShape J C
F : J ⥤ D
c : Cocone ((F ⋙ R) ⋙ leftAdjoint R) := (leftAdjoint R).mapCocone (colimit.cocone (F ⋙ R))
this : PreservesColimitsOfShape J (leftAdjoint R) := PreservesColimitsOfSize.preservesColimitsOfShape
⊢ HasColimit F
let t : IsColimit c := isColimitOfPreserves (leftAdjoint R) (colimit.isColimit _)
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
J : Type u
inst✝² : Category J
R : D ⥤ C
inst✝¹ : Reflective R
inst✝ : HasColimitsOfShape J C
F : J ⥤ D
c : Cocone ((F ⋙ R) ⋙ leftAdjoint R) := (leftAdjoint R).mapCocone (colimit.cocone (F ⋙ R))
this : PreservesColimitsOfShape J (leftAdjoint R) := PreservesColimitsOfSize.preservesColimitsOfShape
t : IsColimit c := isColimitOfPreserves (leftAdjoint R) (colimit.isColimit (F ⋙ R))
⊢ (F ⋙ R) ⋙ leftAdjoint R ≅ F
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
J : Type u
inst✝² : Category J
R : D ⥤ C
inst✝¹ : Reflective R
inst✝ : HasColimitsOfShape J C
F : J ⥤ D
c : Cocone ((F ⋙ R) ⋙ leftAdjoint R) := (leftAdjoint R).mapCocone (colimit.cocone (F ⋙ R))
this : PreservesColimitsOfShape J (leftAdjoint R) := PreservesColimitsOfSize.preservesColimitsOfShape
t : IsColimit c := isColimitOfPreserves (leftAdjoint R) (colimit.isColimit (F ⋙ R))
⊢ HasColimit F
apply HasColimit.mk ⟨_, (IsColimit.precomposeInvEquiv _ _).symm t⟩
no goals
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
J : Type u
inst✝² : Category J
R : D ⥤ C
inst✝¹ : Reflective R
inst✝ : HasColimitsOfShape J C
F : J ⥤ D
c : Cocone ((F ⋙ R) ⋙ leftAdjoint R) := (leftAdjoint R).mapCocone (colimit.cocone (F ⋙ R))
this : PreservesColimitsOfShape J (leftAdjoint R) := PreservesColimitsOfSize.preservesColimitsOfShape
t : IsColimit c := isColimitOfPreserves (leftAdjoint R) (colimit.isColimit (F ⋙ R))
⊢ (F ⋙ R) ⋙ leftAdjoint R ≅ F
apply
  (isoWhiskerLeft F (asIso (Adjunction.ofRightAdjoint R).counit) : _) ≪≫ F.rightUnitor