-- 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:
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
this : PreservesColimit (F ⋙ R) (comonadicRightAdjoint R) :=
  {
    preserves := fun {c} h =>
      Nonempty.intro
        (isColimitChangeEmptyCocone D (colimit.isColimit F) ((comonadicRightAdjoint R).mapCocone c)
          (asIso ((comonadicAdjunction R).unit.app (colimit.cocone F).1) ≪≫
            (comonadicRightAdjoint R).mapIso
              (let A := preservesColimit_of_createsColimit_and_hasColimit F R;
              (isColimitOfPreserves R (colimit.isColimit F)).coconePointUniqueUpToIso h))) }
⊢ PreservesColimit K (comonadicRightAdjoint R)

Tactic:
apply preservesColimit_of_iso_diagram _ (Functor.emptyExt (F ⋙ R) _)

Result:
no goals

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
F : Discrete PEmpty.{v + 1} ⥤ D := Functor.empty D
⊢ PreservesColimit (F ⋙ R) (comonadicRightAdjoint R)

Tactic:
constructor

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)}, 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
this✝ : HasColimit (F ⋙ R)
this : HasColimit F
⊢ Nonempty (IsColimit ((comonadicRightAdjoint R).mapCocone c))

Tactic:
constructor

Result:
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)

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
⊢ (colimit.cocone F).pt ≅ ((comonadicRightAdjoint R).mapCocone c).pt

Tactic:
apply (asIso ((comonadicAdjunction R).unit.app _)).trans

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
⊢ (R ⋙ comonadicRightAdjoint R).obj (colimit.cocone F).1 ≅ ((comonadicRightAdjoint R).mapCocone 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
F : Discrete PEmpty.{v + 1} ⥤ D := Functor.empty D
⊢ PreservesColimit K (comonadicRightAdjoint R)

Tactic:
letI : PreservesColimit (F ⋙ R) (comonadicRightAdjoint R) := by
  constructor
  intro c h
  haveI : HasColimit (F ⋙ R) := ⟨⟨⟨c, h⟩⟩⟩
  haveI : HasColimit F := hasColimit_of_coreflective F R
  constructor
  apply isColimitChangeEmptyCocone D (colimit.isColimit F)
  apply (asIso ((comonadicAdjunction R).unit.app _)).trans
  apply (comonadicRightAdjoint R).mapIso
  letI := comonadicCreatesColimits.{v, v} R
  let A := CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit F R
  apply (isColimitOfPreserves _ (colimit.isColimit F)).coconePointUniqueUpToIso h

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
this : PreservesColimit (F ⋙ R) (comonadicRightAdjoint R) :=
  {
    preserves := fun {c} h =>
      Nonempty.intro
        (isColimitChangeEmptyCocone D (colimit.isColimit F) ((comonadicRightAdjoint R).mapCocone c)
          (asIso ((comonadicAdjunction R).unit.app (colimit.cocone F).1) ≪≫
            (comonadicRightAdjoint R).mapIso
              (let A := preservesColimit_of_createsColimit_and_hasColimit F R;
              (isColimitOfPreserves R (colimit.isColimit F)).coconePointUniqueUpToIso h))) }
⊢ PreservesColimit K (comonadicRightAdjoint R)

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 ⋙ comonadicRightAdjoint R).obj (colimit.cocone F).1 ≅ ((comonadicRightAdjoint R).mapCocone c).pt

Tactic:
apply (comonadicRightAdjoint R).mapIso

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
⊢ R.obj (colimit.cocone F).1 ≅ 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
⊢ R.obj (colimit.cocone F).1 ≅ c.pt

Tactic:
let A := CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit F 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
A : PreservesColimit F R := preservesColimit_of_createsColimit_and_hasColimit F R
⊢ R.obj (colimit.cocone F).1 ≅ c.pt

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
this : HasColimit (F ⋙ R)
⊢ Nonempty (IsColimit ((comonadicRightAdjoint R).mapCocone c))

Tactic:
haveI : HasColimit F := hasColimit_of_coreflective F R

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)
this : HasColimit F
⊢ Nonempty (IsColimit ((comonadicRightAdjoint R).mapCocone c))