-- Mathlib/CategoryTheory/Monad/Limits.lean
/-- The reflector always preserves terminal objects. Note this in general doesn't apply to any other
limit.
-/
lemma leftAdjoint_preservesTerminal_of_reflective (R : D ⥤ C) [Reflective R] :
    PreservesLimitsOfShape (Discrete.{v} PEmpty) (monadicLeftAdjoint R) where
  preservesLimit {K}

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := Functor.empty D
⊢ PreservesLimit K (monadicLeftAdjoint R)

Tactic:
letI : PreservesLimit (F ⋙ R) (monadicLeftAdjoint R) := by
  constructor
  intro c h
  haveI : HasLimit (F ⋙ R) := ⟨⟨⟨c, h⟩⟩⟩
  haveI : HasLimit F := hasLimit_of_reflective F R
  constructor
  apply isLimitChangeEmptyCone D (limit.isLimit F)
  apply (asIso ((monadicAdjunction R).counit.app _)).symm.trans
  apply (monadicLeftAdjoint R).mapIso
  letI := monadicCreatesLimits.{v, v} R
  let A := CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit F R
  apply (isLimitOfPreserves _ (limit.isLimit F)).conePointUniqueUpToIso h

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := Functor.empty D
this : PreservesLimit (F ⋙ R) (monadicLeftAdjoint R) :=
  {
    preserves := fun {c} h =>
      Nonempty.intro
        (isLimitChangeEmptyCone D (limit.isLimit F) ((monadicLeftAdjoint R).mapCone c)
          ((asIso ((monadicAdjunction R).counit.app (limit.cone F).1)).symm ≪≫
            (monadicLeftAdjoint R).mapIso
              (let A := preservesLimit_of_createsLimit_and_hasLimit F R;
              (isLimitOfPreserves R (limit.isLimit F)).conePointUniqueUpToIso h))) }
⊢ PreservesLimit K (monadicLeftAdjoint 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✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := Functor.empty D
c : Cone (F ⋙ R)
h : IsLimit c
this✝ : HasLimit (F ⋙ R)
this : HasLimit F
⊢ R.obj (limit.cone F).1 ≅ c.pt

Tactic:
letI := monadicCreatesLimits.{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✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := Functor.empty D
c : Cone (F ⋙ R)
h : IsLimit c
this✝¹ : HasLimit (F ⋙ R)
this✝ : HasLimit F
this : CreatesLimitsOfSize.{v, v, v₂, v₁, u₂, u₁} R := monadicCreatesLimits R
⊢ R.obj (limit.cone 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✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := Functor.empty D
this : PreservesLimit (F ⋙ R) (monadicLeftAdjoint R) :=
  {
    preserves := fun {c} h =>
      Nonempty.intro
        (isLimitChangeEmptyCone D (limit.isLimit F) ((monadicLeftAdjoint R).mapCone c)
          ((asIso ((monadicAdjunction R).counit.app (limit.cone F).1)).symm ≪≫
            (monadicLeftAdjoint R).mapIso
              (let A := preservesLimit_of_createsLimit_and_hasLimit F R;
              (isLimitOfPreserves R (limit.isLimit F)).conePointUniqueUpToIso h))) }
⊢ PreservesLimit K (monadicLeftAdjoint R)

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

Result:
no goals

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✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := Functor.empty D
c : Cone (F ⋙ R)
h : IsLimit c
this✝ : HasLimit (F ⋙ R)
this : HasLimit F
⊢ (R ⋙ monadicLeftAdjoint R).obj (limit.cone F).1 ≅ ((monadicLeftAdjoint R).mapCone c).pt

Tactic:
apply (monadicLeftAdjoint 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✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := Functor.empty D
c : Cone (F ⋙ R)
h : IsLimit c
this✝ : HasLimit (F ⋙ R)
this : HasLimit F
⊢ R.obj (limit.cone 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✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := Functor.empty D
c : Cone (F ⋙ R)
h : IsLimit c
this✝¹ : HasLimit (F ⋙ R)
this✝ : HasLimit F
this : CreatesLimitsOfSize.{v, v, v₂, v₁, u₂, u₁} R := monadicCreatesLimits R
A : PreservesLimit F R := preservesLimit_of_createsLimit_and_hasLimit F R
⊢ R.obj (limit.cone F).1 ≅ c.pt

Tactic:
apply (isLimitOfPreserves _ (limit.isLimit F)).conePointUniqueUpToIso h

Result:
no goals

Proof state:
case preserves
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := Functor.empty D
⊢ ∀ {c : Cone (F ⋙ R)}, IsLimit c → Nonempty (IsLimit ((monadicLeftAdjoint R).mapCone 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✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := Functor.empty D
c : Cone (F ⋙ R)
h : IsLimit c
⊢ Nonempty (IsLimit ((monadicLeftAdjoint R).mapCone c))

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
⊢ PreservesLimit K (monadicLeftAdjoint 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✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := Functor.empty D
⊢ PreservesLimit K (monadicLeftAdjoint R)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := Functor.empty D
⊢ PreservesLimit (F ⋙ R) (monadicLeftAdjoint 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✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := Functor.empty D
⊢ ∀ {c : Cone (F ⋙ R)}, IsLimit c → Nonempty (IsLimit ((monadicLeftAdjoint R).mapCone 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✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := Functor.empty D
c : Cone (F ⋙ R)
h : IsLimit c
⊢ Nonempty (IsLimit ((monadicLeftAdjoint R).mapCone c))

Tactic:
haveI : HasLimit (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✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := Functor.empty D
c : Cone (F ⋙ R)
h : IsLimit c
this : HasLimit (F ⋙ R)
⊢ Nonempty (IsLimit ((monadicLeftAdjoint R).mapCone 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✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := Functor.empty D
c : Cone (F ⋙ R)
h : IsLimit c
this : HasLimit (F ⋙ R)
⊢ Nonempty (IsLimit ((monadicLeftAdjoint R).mapCone c))

Tactic:
haveI : HasLimit F := hasLimit_of_reflective 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✝ : Reflective R
K : Discrete PEmpty.{v + 1} ⥤ C
F : Discrete PEmpty.{v + 1} ⥤ D := Functor.empty D
c : Cone (F ⋙ R)
h : IsLimit c
this✝ : HasLimit (F ⋙ R)
this : HasLimit F
⊢ Nonempty (IsLimit ((monadicLeftAdjoint R).mapCone c))