-- Mathlib/CategoryTheory/Monad/Limits.lean
/-- The coreflector always preserves initial objects. Note this in general doesn't apply to any
other colimit.
-/
lemma rightAdjoint_preservesInitial_of_coreflective (R : D ⥤ C) [Coreflective R] :
    PreservesColimitsOfShape (Discrete.{v} PEmpty) (comonadicRightAdjoint R) where
  preservesColimit {K}

Proof state:
case preserves
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := Functor.empty D
⊢ ∀ {c : Cocone (F ⋙ R)}, IsColimit c → Nonempty (IsColimit ((comonadicRightAdjoint R).mapCocone c))

Tactic:
intro c h

Result:
case preserves
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := Functor.empty D
c : Cocone (F ⋙ R)
h : IsColimit c
⊢ Nonempty (IsColimit ((comonadicRightAdjoint R).mapCocone c))

Proof state:
case preserves
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := Functor.empty D
c : Cocone (F ⋙ R)
h : IsColimit c
⊢ Nonempty (IsColimit ((comonadicRightAdjoint R).mapCocone c))

Tactic:
haveI : HasColimit (F ⋙ R) := ⟨⟨⟨c, h⟩⟩⟩

Result:
case preserves
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := Functor.empty D
c : Cocone (F ⋙ R)
h : IsColimit c
this : HasColimit (F ⋙ R)
⊢ Nonempty (IsColimit ((comonadicRightAdjoint R).mapCocone c))

Proof state:
case preserves.val.hi
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := Functor.empty D
c : Cocone (F ⋙ R)
h : IsColimit c
this✝ : HasColimit (F ⋙ R)
this : HasColimit F
⊢ R.obj (colimit.cocone F).1 ≅ c.pt

Tactic:
letI := comonadicCreatesColimits.{v, v} R

Result:
case preserves.val.hi
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := Functor.empty D
c : Cocone (F ⋙ R)
h : IsColimit c
this✝¹ : HasColimit (F ⋙ R)
this✝ : HasColimit F
this : CreatesColimitsOfSize.{v, v, v₂, v₁, u₂, u₁} R := comonadicCreatesColimits R
⊢ R.obj (colimit.cocone F).1 ≅ c.pt

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
⊢ PreservesColimit K (comonadicRightAdjoint R)

Tactic:
let F := Functor.empty.{v} D

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := Functor.empty D
⊢ PreservesColimit K (comonadicRightAdjoint R)

Proof state:
case preserves.val
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := Functor.empty D
c : Cocone (F ⋙ R)
h : IsColimit c
this✝ : HasColimit (F ⋙ R)
this : HasColimit F
⊢ IsColimit ((comonadicRightAdjoint R).mapCocone c)

Tactic:
apply isColimitChangeEmptyCocone D (colimit.isColimit F)

Result:
case preserves.val.hi
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := Functor.empty D
c : Cocone (F ⋙ R)
h : IsColimit c
this✝ : HasColimit (F ⋙ R)
this : HasColimit F
⊢ (colimit.cocone F).pt ≅ ((comonadicRightAdjoint R).mapCocone c).pt

Proof state:
case preserves.val.hi
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := Functor.empty D
c : Cocone (F ⋙ R)
h : IsColimit c
this✝¹ : HasColimit (F ⋙ R)
this✝ : HasColimit F
this : CreatesColimitsOfSize.{v, v, v₂, v₁, u₂, u₁} R := comonadicCreatesColimits R
A : PreservesColimit F R := preservesColimit_of_createsColimit_and_hasColimit F R
⊢ R.obj (colimit.cocone F).1 ≅ c.pt

Tactic:
apply (isColimitOfPreserves _ (colimit.isColimit F)).coconePointUniqueUpToIso h

Result:
no goals