-- Mathlib/CategoryTheory/Adjunction/Lifting/Left.lean
/-- If `R ⋙ U` has a left adjoint, the domain of `R` has reflexive coequalizers and `U` is a monadic
functor, then `R` has a left adjoint.
This is a special case of `isRightAdjoint_triangle_lift` which is often more useful in practice.
-/
lemma isRightAdjoint_triangle_lift_monadic (U : B ⥤ C) [MonadicRightAdjoint U] {R : A ⥤ B}
    [HasReflexiveCoequalizers A] [(R ⋙ U).IsRightAdjoint] : R.IsRightAdjoint

Proof state:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := R ⋙ Monad.comparison (monadicAdjunction U)
this : (R' ⋙ (monadicAdjunction U).toMonad.forget).IsRightAdjoint :=
  Adjunction.isRightAdjoint
    ((Adjunction.ofIsRightAdjoint (R ⋙ U)).ofNatIsoRight
      (isoWhiskerLeft R (Monad.comparisonForget (monadicAdjunction U)).symm))
⊢ (X : (monadicAdjunction U).toMonad.Algebra) → RegularEpi ((monadicAdjunction U).toMonad.adj.counit.app X)

Tactic:
intro X

Result:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := R ⋙ Monad.comparison (monadicAdjunction U)
this : (R' ⋙ (monadicAdjunction U).toMonad.forget).IsRightAdjoint :=
  Adjunction.isRightAdjoint
    ((Adjunction.ofIsRightAdjoint (R ⋙ U)).ofNatIsoRight
      (isoWhiskerLeft R (Monad.comparisonForget (monadicAdjunction U)).symm))
X : (monadicAdjunction U).toMonad.Algebra
⊢ RegularEpi ((monadicAdjunction U).toMonad.adj.counit.app X)

Proof state:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := R ⋙ Monad.comparison (monadicAdjunction U)
this : (R' ⋙ (monadicAdjunction U).toMonad.forget).IsRightAdjoint :=
  Adjunction.isRightAdjoint
    ((Adjunction.ofIsRightAdjoint (R ⋙ U)).ofNatIsoRight
      (isoWhiskerLeft R (Monad.comparisonForget (monadicAdjunction U)).symm))
X : (monadicAdjunction U).toMonad.Algebra
⊢ RegularEpi ((monadicAdjunction U).toMonad.adj.counit.app X)

Tactic:
simp only [Monad.adj_counit]

Result:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := R ⋙ Monad.comparison (monadicAdjunction U)
this : (R' ⋙ (monadicAdjunction U).toMonad.forget).IsRightAdjoint :=
  Adjunction.isRightAdjoint
    ((Adjunction.ofIsRightAdjoint (R ⋙ U)).ofNatIsoRight
      (isoWhiskerLeft R (Monad.comparisonForget (monadicAdjunction U)).symm))
X : (monadicAdjunction U).toMonad.Algebra
⊢ RegularEpi { f := X.a, h := ⋯ }

Proof state:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := R ⋙ Monad.comparison (monadicAdjunction U)
⊢ R'.IsRightAdjoint

Tactic:
let this : (R' ⋙ Monad.forget (monadicAdjunction U).toMonad).IsRightAdjoint := by
  refine ((Adjunction.ofIsRightAdjoint (R ⋙ U)).ofNatIsoRight ?_).isRightAdjoint
  exact isoWhiskerLeft R (Monad.comparisonForget (monadicAdjunction U)).symm

Result:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := R ⋙ Monad.comparison (monadicAdjunction U)
this : (R' ⋙ (monadicAdjunction U).toMonad.forget).IsRightAdjoint :=
  Adjunction.isRightAdjoint
    ((Adjunction.ofIsRightAdjoint (R ⋙ U)).ofNatIsoRight
      (isoWhiskerLeft R (Monad.comparisonForget (monadicAdjunction U)).symm))
⊢ R'.IsRightAdjoint

Proof state:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := R ⋙ Monad.comparison (monadicAdjunction U)
this : (R' ⋙ (monadicAdjunction U).toMonad.forget).IsRightAdjoint :=
  Adjunction.isRightAdjoint
    ((Adjunction.ofIsRightAdjoint (R ⋙ U)).ofNatIsoRight
      (isoWhiskerLeft R (Monad.comparisonForget (monadicAdjunction U)).symm))
X : (monadicAdjunction U).toMonad.Algebra
⊢ RegularEpi { f := X.a, h := ⋯ }

Tactic:
exact ⟨_, _, _, _, Monad.beckAlgebraCoequalizer X⟩

Result:
no goals

Proof state:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := R ⋙ Monad.comparison (monadicAdjunction U)
this✝ : R'.IsRightAdjoint
this : (R' ⋙ (Monad.comparison (monadicAdjunction U)).inv).IsRightAdjoint := inferInstance
⊢ R' ⋙ (Monad.comparison (monadicAdjunction U)).inv ≅ R

Tactic:
exact isoWhiskerLeft R (Monad.comparison _).asEquivalence.unitIso.symm ≪≫ R.rightUnitor

Result:
no goals

Proof state:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := R ⋙ Monad.comparison (monadicAdjunction U)
⊢ (R' ⋙ (monadicAdjunction U).toMonad.forget).IsRightAdjoint

Tactic:
refine ((Adjunction.ofIsRightAdjoint (R ⋙ U)).ofNatIsoRight ?_).isRightAdjoint

Result:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := R ⋙ Monad.comparison (monadicAdjunction U)
⊢ R ⋙ U ≅ R' ⋙ (monadicAdjunction U).toMonad.forget

Proof state:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := R ⋙ Monad.comparison (monadicAdjunction U)
this✝ : R'.IsRightAdjoint
this : (R' ⋙ (Monad.comparison (monadicAdjunction U)).inv).IsRightAdjoint := inferInstance
⊢ R.IsRightAdjoint

Tactic:
refine ((Adjunction.ofIsRightAdjoint
  (R' ⋙ (Monad.comparison (monadicAdjunction U)).inv)).ofNatIsoRight ?_).isRightAdjoint

Result:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
U : B ⥤ C
inst✝² : MonadicRightAdjoint U
R : A ⥤ B
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (R ⋙ U).IsRightAdjoint
R' : A ⥤ (monadicAdjunction U).toMonad.Algebra := R ⋙ Monad.comparison (monadicAdjunction U)
this✝ : R'.IsRightAdjoint
this : (R' ⋙ (Monad.comparison (monadicAdjunction U)).inv).IsRightAdjoint := inferInstance
⊢ R' ⋙ (Monad.comparison (monadicAdjunction U)).inv ≅ R