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

Tactic:
let A := CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit 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✝ : 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

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✝ : 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
⊢ IsLimit ((monadicLeftAdjoint R).mapCone c)

Tactic:
apply isLimitChangeEmptyCone D (limit.isLimit 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✝ : 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
⊢ (limit.cone F).pt ≅ ((monadicLeftAdjoint R).mapCone 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
⊢ (limit.cone F).pt ≅ ((monadicLeftAdjoint R).mapCone c).pt

Tactic:
apply (asIso ((monadicAdjunction R).counit.app _)).symm.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✝ : 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

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)
this : HasLimit F
⊢ Nonempty (IsLimit ((monadicLeftAdjoint R).mapCone 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✝ : 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
⊢ IsLimit ((monadicLeftAdjoint R).mapCone c)