[GOAL]
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
X : B
s : Cofork (F.map (U.map (NatTrans.app adj₁.counit X))) (NatTrans.app adj₁.counit (F.obj (U.obj X)))
⊢ { l //
    Cofork.π
            (Cofork.ofπ (NatTrans.app adj₁.counit X)
              (_ :
                F.map (U.map (NatTrans.app adj₁.counit X)) ≫ NatTrans.app adj₁.counit X =
                  NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ NatTrans.app adj₁.counit X)) ≫
          l =
        Cofork.π s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj
                  (Cofork.ofπ (NatTrans.app adj₁.counit X)
                      (_ :
                        F.map (U.map (NatTrans.app adj₁.counit X)) ≫ NatTrans.app adj₁.counit X =
                          NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ NatTrans.app adj₁.counit X)).pt).obj
              WalkingParallelPair.one ⟶
            ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one},
        Cofork.π
                (Cofork.ofπ (NatTrans.app adj₁.counit X)
                  (_ :
                    F.map (U.map (NatTrans.app adj₁.counit X)) ≫ NatTrans.app adj₁.counit X =
                      NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ NatTrans.app adj₁.counit X)) ≫
              m =
            Cofork.π s →
          m = l }
[PROOFSTEP]
refine' ⟨(RegularEpi.desc' (adj₁.counit.app X) s.π _).1, _, _⟩
[GOAL]
case refine'_1
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
X : B
s : Cofork (F.map (U.map (NatTrans.app adj₁.counit X))) (NatTrans.app adj₁.counit (F.obj (U.obj X)))
⊢ RegularEpi.left ≫ Cofork.π s = RegularEpi.right ≫ Cofork.π s
[PROOFSTEP]
rw [← cancel_epi (adj₁.counit.app (RegularEpi.W (adj₁.counit.app X)))]
[GOAL]
case refine'_1
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
X : B
s : Cofork (F.map (U.map (NatTrans.app adj₁.counit X))) (NatTrans.app adj₁.counit (F.obj (U.obj X)))
⊢ NatTrans.app adj₁.counit (RegularEpi.W (NatTrans.app adj₁.counit X)) ≫ RegularEpi.left ≫ Cofork.π s =
    NatTrans.app adj₁.counit (RegularEpi.W (NatTrans.app adj₁.counit X)) ≫ RegularEpi.right ≫ Cofork.π s
[PROOFSTEP]
rw [← adj₁.counit_naturality_assoc RegularEpi.left]
[GOAL]
case refine'_1
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
X : B
s : Cofork (F.map (U.map (NatTrans.app adj₁.counit X))) (NatTrans.app adj₁.counit (F.obj (U.obj X)))
⊢ F.map (U.map RegularEpi.left) ≫ NatTrans.app adj₁.counit ((U ⋙ F).obj X) ≫ Cofork.π s =
    NatTrans.app adj₁.counit (RegularEpi.W (NatTrans.app adj₁.counit X)) ≫ RegularEpi.right ≫ Cofork.π s
[PROOFSTEP]
dsimp only [Functor.comp_obj]
[GOAL]
case refine'_1
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
X : B
s : Cofork (F.map (U.map (NatTrans.app adj₁.counit X))) (NatTrans.app adj₁.counit (F.obj (U.obj X)))
⊢ F.map (U.map RegularEpi.left) ≫ NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ Cofork.π s =
    NatTrans.app adj₁.counit (RegularEpi.W (NatTrans.app adj₁.counit X)) ≫ RegularEpi.right ≫ Cofork.π s
[PROOFSTEP]
rw [← s.condition, ← F.map_comp_assoc, ← U.map_comp, RegularEpi.w, U.map_comp, F.map_comp_assoc, s.condition, ←
  adj₁.counit_naturality_assoc RegularEpi.right]
[GOAL]
case refine'_2
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
X : B
s : Cofork (F.map (U.map (NatTrans.app adj₁.counit X))) (NatTrans.app adj₁.counit (F.obj (U.obj X)))
⊢ Cofork.π
        (Cofork.ofπ (NatTrans.app adj₁.counit X)
          (_ :
            F.map (U.map (NatTrans.app adj₁.counit X)) ≫ NatTrans.app adj₁.counit X =
              NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ NatTrans.app adj₁.counit X)) ≫
      ↑(RegularEpi.desc' (NatTrans.app adj₁.counit X) (Cofork.π s)
          (_ : RegularEpi.left ≫ Cofork.π s = RegularEpi.right ≫ Cofork.π s)) =
    Cofork.π s
[PROOFSTEP]
apply (RegularEpi.desc' (adj₁.counit.app X) s.π _).2
[GOAL]
case refine'_3
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
X : B
s : Cofork (F.map (U.map (NatTrans.app adj₁.counit X))) (NatTrans.app adj₁.counit (F.obj (U.obj X)))
⊢ ∀
    {m :
      ((Functor.const WalkingParallelPair).obj
              (Cofork.ofπ (NatTrans.app adj₁.counit X)
                  (_ :
                    F.map (U.map (NatTrans.app adj₁.counit X)) ≫ NatTrans.app adj₁.counit X =
                      NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ NatTrans.app adj₁.counit X)).pt).obj
          WalkingParallelPair.one ⟶
        ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one},
    Cofork.π
            (Cofork.ofπ (NatTrans.app adj₁.counit X)
              (_ :
                F.map (U.map (NatTrans.app adj₁.counit X)) ≫ NatTrans.app adj₁.counit X =
                  NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ NatTrans.app adj₁.counit X)) ≫
          m =
        Cofork.π s →
      m =
        ↑(RegularEpi.desc' (NatTrans.app adj₁.counit X) (Cofork.π s)
            (_ : RegularEpi.left ≫ Cofork.π s = RegularEpi.right ≫ Cofork.π s))
[PROOFSTEP]
intro m hm
[GOAL]
case refine'_3
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
X : B
s : Cofork (F.map (U.map (NatTrans.app adj₁.counit X))) (NatTrans.app adj₁.counit (F.obj (U.obj X)))
m :
  ((Functor.const WalkingParallelPair).obj
          (Cofork.ofπ (NatTrans.app adj₁.counit X)
              (_ :
                F.map (U.map (NatTrans.app adj₁.counit X)) ≫ NatTrans.app adj₁.counit X =
                  NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ NatTrans.app adj₁.counit X)).pt).obj
      WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hm :
  Cofork.π
        (Cofork.ofπ (NatTrans.app adj₁.counit X)
          (_ :
            F.map (U.map (NatTrans.app adj₁.counit X)) ≫ NatTrans.app adj₁.counit X =
              NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ NatTrans.app adj₁.counit X)) ≫
      m =
    Cofork.π s
⊢ m =
    ↑(RegularEpi.desc' (NatTrans.app adj₁.counit X) (Cofork.π s)
        (_ : RegularEpi.left ≫ Cofork.π s = RegularEpi.right ≫ Cofork.π s))
[PROOFSTEP]
rw [← cancel_epi (adj₁.counit.app X)]
[GOAL]
case refine'_3
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
X : B
s : Cofork (F.map (U.map (NatTrans.app adj₁.counit X))) (NatTrans.app adj₁.counit (F.obj (U.obj X)))
m :
  ((Functor.const WalkingParallelPair).obj
          (Cofork.ofπ (NatTrans.app adj₁.counit X)
              (_ :
                F.map (U.map (NatTrans.app adj₁.counit X)) ≫ NatTrans.app adj₁.counit X =
                  NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ NatTrans.app adj₁.counit X)).pt).obj
      WalkingParallelPair.one ⟶
    ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one
hm :
  Cofork.π
        (Cofork.ofπ (NatTrans.app adj₁.counit X)
          (_ :
            F.map (U.map (NatTrans.app adj₁.counit X)) ≫ NatTrans.app adj₁.counit X =
              NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ NatTrans.app adj₁.counit X)) ≫
      m =
    Cofork.π s
⊢ NatTrans.app adj₁.counit X ≫ m =
    NatTrans.app adj₁.counit X ≫
      ↑(RegularEpi.desc' (NatTrans.app adj₁.counit X) (Cofork.π s)
          (_ : RegularEpi.left ≫ Cofork.π s = RegularEpi.right ≫ Cofork.π s))
[PROOFSTEP]
apply hm.trans (RegularEpi.desc' (adj₁.counit.app X) s.π _).2.symm
[GOAL]
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
X : B
⊢ F'.map (NatTrans.app adj₁.unit (U.obj X)) ≫ F'.map (U.map (NatTrans.app adj₁.counit X)) =
    𝟙 (F'.obj (U.obj ((𝟭 B).obj X)))
[PROOFSTEP]
rw [← F'.map_comp, adj₁.right_triangle_components]
[GOAL]
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
X : B
⊢ F'.map (𝟙 (U.obj X)) = 𝟙 (F'.obj (U.obj ((𝟭 B).obj X)))
[PROOFSTEP]
apply F'.map_id
[GOAL]
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
X : B
⊢ F'.map (NatTrans.app adj₁.unit (U.obj X)) ≫ otherMap R F' adj₁ adj₂ X = 𝟙 (F'.obj (U.obj ((𝟭 B).obj X)))
[PROOFSTEP]
dsimp [otherMap]
[GOAL]
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
X : B
⊢ F'.map (NatTrans.app adj₁.unit (U.obj X)) ≫
      F'.map
          (U.map
            (F.map (NatTrans.app adj₂.unit (U.toPrefunctor.1 X)) ≫
              NatTrans.app adj₁.counit (R.obj (F'.obj (U.toPrefunctor.1 X))))) ≫
        NatTrans.app adj₂.counit (F'.obj (U.toPrefunctor.1 X)) =
    𝟙 (F'.obj (U.obj X))
[PROOFSTEP]
rw [← F'.map_comp_assoc, U.map_comp, adj₁.unit_naturality_assoc, adj₁.right_triangle_components, comp_id,
  adj₂.left_triangle_components]
[GOAL]
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
Y : A
X : B
⊢ { f // F'.map (U.map (NatTrans.app adj₁.counit X)) ≫ f = otherMap R F' adj₁ adj₂ X ≫ f } ≃
    { g // U.map (F.map g ≫ NatTrans.app adj₁.counit (R.obj Y)) = U.map (NatTrans.app adj₁.counit X) ≫ g }
[PROOFSTEP]
apply (adj₂.homEquiv _ _).subtypeEquiv _
[GOAL]
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
Y : A
X : B
⊢ ∀ (a : F'.obj (U.obj X) ⟶ Y),
    F'.map (U.map (NatTrans.app adj₁.counit X)) ≫ a = otherMap R F' adj₁ adj₂ X ≫ a ↔
      U.map (F.map (↑(Adjunction.homEquiv adj₂ (U.obj X) Y) a) ≫ NatTrans.app adj₁.counit (R.obj Y)) =
        U.map (NatTrans.app adj₁.counit X) ≫ ↑(Adjunction.homEquiv adj₂ (U.obj X) Y) a
[PROOFSTEP]
intro f
[GOAL]
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
Y : A
X : B
f : F'.obj (U.obj X) ⟶ Y
⊢ F'.map (U.map (NatTrans.app adj₁.counit X)) ≫ f = otherMap R F' adj₁ adj₂ X ≫ f ↔
    U.map (F.map (↑(Adjunction.homEquiv adj₂ (U.obj X) Y) f) ≫ NatTrans.app adj₁.counit (R.obj Y)) =
      U.map (NatTrans.app adj₁.counit X) ≫ ↑(Adjunction.homEquiv adj₂ (U.obj X) Y) f
[PROOFSTEP]
rw [← (adj₂.homEquiv _ _).injective.eq_iff, eq_comm, adj₂.homEquiv_naturality_left, otherMap, assoc,
  adj₂.homEquiv_naturality_left, ← adj₂.counit_naturality, adj₂.homEquiv_naturality_left, adj₂.homEquiv_unit,
  adj₂.right_triangle_components, comp_id, Functor.comp_map, ← U.map_comp, assoc, ← adj₁.counit_naturality,
  adj₂.homEquiv_unit, adj₂.homEquiv_unit, F.map_comp, assoc]
[GOAL]
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
Y : A
X : B
f : F'.obj (U.obj X) ⟶ Y
⊢ U.map
        (F.map (NatTrans.app adj₂.unit (U.toPrefunctor.1 X)) ≫
          F.map (U.map (R.map f)) ≫ NatTrans.app adj₁.counit (R.obj Y)) =
      U.map (NatTrans.app adj₁.counit X) ≫ NatTrans.app adj₂.unit (U.obj ((𝟭 B).obj X)) ≫ (R ⋙ U).map f ↔
    U.map (F.map (NatTrans.app adj₂.unit (U.obj X)) ≫ F.map ((R ⋙ U).map f) ≫ NatTrans.app adj₁.counit (R.obj Y)) =
      U.map (NatTrans.app adj₁.counit X) ≫ NatTrans.app adj₂.unit (U.obj X) ≫ (R ⋙ U).map f
[PROOFSTEP]
rfl
[GOAL]
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
Y : A
X : B
⊢ { g // U.map (F.map g ≫ NatTrans.app adj₁.counit (R.obj Y)) = U.map (NatTrans.app adj₁.counit X) ≫ g } ≃
    { z // F.map (U.map (NatTrans.app adj₁.counit X)) ≫ z = NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ z }
[PROOFSTEP]
apply (adj₁.homEquiv _ _).symm.subtypeEquiv
[GOAL]
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
Y : A
X : B
⊢ ∀ (a : U.obj X ⟶ U.obj (R.obj Y)),
    U.map (F.map a ≫ NatTrans.app adj₁.counit (R.obj Y)) = U.map (NatTrans.app adj₁.counit X) ≫ a ↔
      F.map (U.map (NatTrans.app adj₁.counit X)) ≫ ↑(Adjunction.homEquiv adj₁ (U.obj X) (R.obj Y)).symm a =
        NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ ↑(Adjunction.homEquiv adj₁ (U.obj X) (R.obj Y)).symm a
[PROOFSTEP]
intro g
[GOAL]
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
Y : A
X : B
g : U.obj X ⟶ U.obj (R.obj Y)
⊢ U.map (F.map g ≫ NatTrans.app adj₁.counit (R.obj Y)) = U.map (NatTrans.app adj₁.counit X) ≫ g ↔
    F.map (U.map (NatTrans.app adj₁.counit X)) ≫ ↑(Adjunction.homEquiv adj₁ (U.obj X) (R.obj Y)).symm g =
      NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ ↑(Adjunction.homEquiv adj₁ (U.obj X) (R.obj Y)).symm g
[PROOFSTEP]
rw [← (adj₁.homEquiv _ _).symm.injective.eq_iff, adj₁.homEquiv_counit, adj₁.homEquiv_counit, adj₁.homEquiv_counit,
  F.map_comp, assoc, U.map_comp, F.map_comp, assoc, adj₁.counit_naturality, adj₁.counit_naturality_assoc]
[GOAL]
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
Y : A
X : B
g : U.obj X ⟶ U.obj (R.obj Y)
⊢ NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ F.map g ≫ NatTrans.app adj₁.counit (R.obj Y) =
      F.map (U.map (NatTrans.app adj₁.counit X)) ≫ F.map g ≫ NatTrans.app adj₁.counit ((𝟭 B).obj (R.obj Y)) ↔
    F.map (U.map (NatTrans.app adj₁.counit X)) ≫ F.map g ≫ NatTrans.app adj₁.counit (R.obj Y) =
      NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ F.map g ≫ NatTrans.app adj₁.counit (R.obj Y)
[PROOFSTEP]
apply eq_comm
[GOAL]
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
⊢ B ⥤ A
[PROOFSTEP]
refine' Adjunction.leftAdjointOfEquiv (fun X Y => constructLeftAdjointEquiv R _ adj₁ adj₂ Y X) _
[GOAL]
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
⊢ ∀ (X : B) (Y Y' : A) (g : Y ⟶ Y') (h : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y),
    ↑((fun X Y => constructLeftAdjointEquiv R F' adj₁ adj₂ Y X) X Y') (h ≫ g) =
      ↑((fun X Y => constructLeftAdjointEquiv R F' adj₁ adj₂ Y X) X Y) h ≫ R.map g
[PROOFSTEP]
intro X Y Y' g h
[GOAL]
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
X : B
Y Y' : A
g : Y ⟶ Y'
h : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y
⊢ ↑((fun X Y => constructLeftAdjointEquiv R F' adj₁ adj₂ Y X) X Y') (h ≫ g) =
    ↑((fun X Y => constructLeftAdjointEquiv R F' adj₁ adj₂ Y X) X Y) h ≫ R.map g
[PROOFSTEP]
rw [constructLeftAdjointEquiv_apply, constructLeftAdjointEquiv_apply, Equiv.symm_apply_eq, Subtype.ext_iff]
[GOAL]
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
X : B
Y Y' : A
g : Y ⟶ Y'
h : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y
⊢ ↑{
        val :=
          F.map
              (↑(Adjunction.homEquiv adj₂ (U.obj X) Y')
                ↑(↑(Cofork.IsColimit.homIso
                        (colimit.isColimit
                          (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X))) (otherMap R F' adj₁ adj₂ X)))
                        Y')
                    (h ≫ g))) ≫
            NatTrans.app adj₁.counit (R.obj Y'),
        property :=
          (_ :
            (fun b => F.map (U.map (NatTrans.app adj₁.counit X)) ≫ b = NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ b)
              (F.map
                  (↑(Adjunction.homEquiv adj₂ (U.obj X) Y')
                    ↑(↑(Cofork.IsColimit.homIso
                            (colimit.isColimit
                              (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X))) (otherMap R F' adj₁ adj₂ X)))
                            Y')
                        (h ≫ g))) ≫
                NatTrans.app adj₁.counit (R.obj Y'))) } =
    ↑(↑(Cofork.IsColimit.homIso (counitCoequalises adj₁ X) (R.obj Y'))
        (↑(Cofork.IsColimit.homIso (counitCoequalises adj₁ X) (R.obj Y)).symm
            {
              val :=
                F.map
                    (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
                      ↑(↑(Cofork.IsColimit.homIso
                              (colimit.isColimit
                                (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X)))
                                  (otherMap R F' adj₁ adj₂ X)))
                              Y)
                          h)) ≫
                  NatTrans.app adj₁.counit (R.obj Y),
              property :=
                (_ :
                  (fun b =>
                      F.map (U.map (NatTrans.app adj₁.counit X)) ≫ b = NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫ b)
                    (F.map
                        (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
                          ↑(↑(Cofork.IsColimit.homIso
                                  (colimit.isColimit
                                    (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X)))
                                      (otherMap R F' adj₁ adj₂ X)))
                                  Y)
                              h)) ≫
                      NatTrans.app adj₁.counit (R.obj Y))) } ≫
          R.map g))
[PROOFSTEP]
dsimp
[GOAL]
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
X : B
Y Y' : A
g : Y ⟶ Y'
h : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y
⊢ F.map
        (↑(Adjunction.homEquiv adj₂ (U.obj X) Y')
          ↑(↑(Cofork.IsColimit.homIso
                  (colimit.isColimit
                    (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X))) (otherMap R F' adj₁ adj₂ X)))
                  Y')
              (h ≫ g))) ≫
      NatTrans.app adj₁.counit (R.obj Y') =
    ↑(↑(Cofork.IsColimit.homIso (counitCoequalises adj₁ X) (R.obj Y'))
        (↑(Cofork.IsColimit.homIso (counitCoequalises adj₁ X) (R.obj Y)).symm
            {
              val :=
                F.map
                    (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
                      ↑(↑(Cofork.IsColimit.homIso
                              (colimit.isColimit
                                (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X)))
                                  (otherMap R F' adj₁ adj₂ X)))
                              Y)
                          h)) ≫
                  NatTrans.app adj₁.counit (R.obj Y),
              property :=
                (_ :
                  F.map (U.map (NatTrans.app adj₁.counit X)) ≫
                      F.map
                          (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
                            ↑(↑(Cofork.IsColimit.homIso
                                    (colimit.isColimit
                                      (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X)))
                                        (otherMap R F' adj₁ adj₂ X)))
                                    Y)
                                h)) ≫
                        NatTrans.app adj₁.counit (R.obj Y) =
                    NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫
                      F.map
                          (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
                            ↑(↑(Cofork.IsColimit.homIso
                                    (colimit.isColimit
                                      (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X)))
                                        (otherMap R F' adj₁ adj₂ X)))
                                    Y)
                                h)) ≫
                        NatTrans.app adj₁.counit (R.obj Y)) } ≫
          R.map g))
[PROOFSTEP]
rw [Cofork.IsColimit.homIso_natural, Cofork.IsColimit.homIso_natural]
[GOAL]
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
X : B
Y Y' : A
g : Y ⟶ Y'
h : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y
⊢ F.map
        (↑(Adjunction.homEquiv adj₂ (U.obj X) Y')
          (↑(↑(Cofork.IsColimit.homIso
                    (colimit.isColimit
                      (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X))) (otherMap R F' adj₁ adj₂ X)))
                    Y)
                h) ≫
            g)) ≫
      NatTrans.app adj₁.counit (R.obj Y') =
    ↑(↑(Cofork.IsColimit.homIso (counitCoequalises adj₁ X) (R.obj Y))
          (↑(Cofork.IsColimit.homIso (counitCoequalises adj₁ X) (R.obj Y)).symm
            {
              val :=
                F.map
                    (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
                      ↑(↑(Cofork.IsColimit.homIso
                              (colimit.isColimit
                                (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X)))
                                  (otherMap R F' adj₁ adj₂ X)))
                              Y)
                          h)) ≫
                  NatTrans.app adj₁.counit (R.obj Y),
              property :=
                (_ :
                  F.map (U.map (NatTrans.app adj₁.counit X)) ≫
                      F.map
                          (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
                            ↑(↑(Cofork.IsColimit.homIso
                                    (colimit.isColimit
                                      (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X)))
                                        (otherMap R F' adj₁ adj₂ X)))
                                    Y)
                                h)) ≫
                        NatTrans.app adj₁.counit (R.obj Y) =
                    NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫
                      F.map
                          (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
                            ↑(↑(Cofork.IsColimit.homIso
                                    (colimit.isColimit
                                      (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X)))
                                        (otherMap R F' adj₁ adj₂ X)))
                                    Y)
                                h)) ≫
                        NatTrans.app adj₁.counit (R.obj Y)) })) ≫
      R.map g
[PROOFSTEP]
erw [adj₂.homEquiv_naturality_right]
[GOAL]
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
X : B
Y Y' : A
g : Y ⟶ Y'
h : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y
⊢ F.map
        (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
            ↑(↑(Cofork.IsColimit.homIso
                    (colimit.isColimit
                      (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X))) (otherMap R F' adj₁ adj₂ X)))
                    Y)
                h) ≫
          (R ⋙ U).map g) ≫
      NatTrans.app adj₁.counit (R.obj Y') =
    ↑(↑(Cofork.IsColimit.homIso (counitCoequalises adj₁ X) (R.obj Y))
          (↑(Cofork.IsColimit.homIso (counitCoequalises adj₁ X) (R.obj Y)).symm
            {
              val :=
                F.map
                    (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
                      ↑(↑(Cofork.IsColimit.homIso
                              (colimit.isColimit
                                (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X)))
                                  (otherMap R F' adj₁ adj₂ X)))
                              Y)
                          h)) ≫
                  NatTrans.app adj₁.counit (R.obj Y),
              property :=
                (_ :
                  F.map (U.map (NatTrans.app adj₁.counit X)) ≫
                      F.map
                          (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
                            ↑(↑(Cofork.IsColimit.homIso
                                    (colimit.isColimit
                                      (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X)))
                                        (otherMap R F' adj₁ adj₂ X)))
                                    Y)
                                h)) ≫
                        NatTrans.app adj₁.counit (R.obj Y) =
                    NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫
                      F.map
                          (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
                            ↑(↑(Cofork.IsColimit.homIso
                                    (colimit.isColimit
                                      (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X)))
                                        (otherMap R F' adj₁ adj₂ X)))
                                    Y)
                                h)) ≫
                        NatTrans.app adj₁.counit (R.obj Y)) })) ≫
      R.map g
[PROOFSTEP]
simp_rw [Functor.comp_map]
[GOAL]
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
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝¹ : HasReflexiveCoequalizers A
inst✝ : (X : B) → RegularEpi (NatTrans.app adj₁.counit X)
X : B
Y Y' : A
g : Y ⟶ Y'
h : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y
⊢ F.map
        (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
            ↑(↑(Cofork.IsColimit.homIso
                    (colimit.isColimit
                      (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X))) (otherMap R F' adj₁ adj₂ X)))
                    Y)
                h) ≫
          U.map (R.map g)) ≫
      NatTrans.app adj₁.counit (R.obj Y') =
    ↑(↑(Cofork.IsColimit.homIso (counitCoequalises adj₁ X) (R.obj Y))
          (↑(Cofork.IsColimit.homIso (counitCoequalises adj₁ X) (R.obj Y)).symm
            {
              val :=
                F.map
                    (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
                      ↑(↑(Cofork.IsColimit.homIso
                              (colimit.isColimit
                                (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X)))
                                  (otherMap R F' adj₁ adj₂ X)))
                              Y)
                          h)) ≫
                  NatTrans.app adj₁.counit (R.obj Y),
              property :=
                (_ :
                  F.map (U.map (NatTrans.app adj₁.counit X)) ≫
                      F.map
                          (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
                            ↑(↑(Cofork.IsColimit.homIso
                                    (colimit.isColimit
                                      (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X)))
                                        (otherMap R F' adj₁ adj₂ X)))
                                    Y)
                                h)) ≫
                        NatTrans.app adj₁.counit (R.obj Y) =
                    NatTrans.app adj₁.counit (F.obj (U.obj X)) ≫
                      F.map
                          (↑(Adjunction.homEquiv adj₂ (U.obj X) Y)
                            ↑(↑(Cofork.IsColimit.homIso
                                    (colimit.isColimit
                                      (parallelPair (F'.map (U.map (NatTrans.app adj₁.counit X)))
                                        (otherMap R F' adj₁ adj₂ X)))
                                    Y)
                                h)) ≫
                        NatTrans.app adj₁.counit (R.obj Y)) })) ≫
      R.map g
[PROOFSTEP]
simp
[GOAL]
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✝ : IsRightAdjoint (R ⋙ U)
⊢ IsRightAdjoint R
[PROOFSTEP]
let R' : A ⥤ _ := R ⋙ Monad.comparison (Adjunction.ofRightAdjoint U)
[GOAL]
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✝ : IsRightAdjoint (R ⋙ U)
R' : A ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint U)) :=
  R ⋙ Monad.comparison (Adjunction.ofRightAdjoint U)
⊢ IsRightAdjoint R
[PROOFSTEP]
rsuffices : IsRightAdjoint R'
[GOAL]
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✝ : IsRightAdjoint (R ⋙ U)
R' : A ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint U)) :=
  R ⋙ Monad.comparison (Adjunction.ofRightAdjoint U)
this✝ : IsRightAdjoint R'
⊢ IsRightAdjoint R
[PROOFSTEP]
let this : IsRightAdjoint (R' ⋙ (Monad.comparison (Adjunction.ofRightAdjoint U)).inv) := by infer_instance
[GOAL]
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✝ : IsRightAdjoint (R ⋙ U)
R' : A ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint U)) :=
  R ⋙ Monad.comparison (Adjunction.ofRightAdjoint U)
this✝ : IsRightAdjoint R'
⊢ IsRightAdjoint (R' ⋙ Functor.inv (Monad.comparison (Adjunction.ofRightAdjoint U)))
[PROOFSTEP]
infer_instance
[GOAL]
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✝ : IsRightAdjoint (R ⋙ U)
R' : A ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint U)) :=
  R ⋙ Monad.comparison (Adjunction.ofRightAdjoint U)
this✝ : IsRightAdjoint R'
this : IsRightAdjoint (R' ⋙ Functor.inv (Monad.comparison (Adjunction.ofRightAdjoint U))) := inferInstance
⊢ IsRightAdjoint R
[PROOFSTEP]
let this : R' ⋙ (Monad.comparison (Adjunction.ofRightAdjoint U)).inv ≅ R :=
  (isoWhiskerLeft R (Monad.comparison _).asEquivalence.unitIso.symm : _) ≪≫ R.rightUnitor
[GOAL]
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✝ : IsRightAdjoint (R ⋙ U)
R' : A ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint U)) :=
  R ⋙ Monad.comparison (Adjunction.ofRightAdjoint U)
this✝¹ : IsRightAdjoint R'
this✝ : IsRightAdjoint (R' ⋙ Functor.inv (Monad.comparison (Adjunction.ofRightAdjoint U))) := inferInstance
this : R' ⋙ Functor.inv (Monad.comparison (Adjunction.ofRightAdjoint U)) ≅ R :=
  isoWhiskerLeft R (Functor.asEquivalence (Monad.comparison (Adjunction.ofRightAdjoint U))).unitIso.symm ≪≫
    Functor.rightUnitor R
⊢ IsRightAdjoint R
[PROOFSTEP]
exact Adjunction.rightAdjointOfNatIso this
[GOAL]
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✝ : IsRightAdjoint (R ⋙ U)
R' : A ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint U)) :=
  R ⋙ Monad.comparison (Adjunction.ofRightAdjoint U)
⊢ IsRightAdjoint R'
[PROOFSTEP]
let this : IsRightAdjoint (R' ⋙ Monad.forget (Adjunction.ofRightAdjoint U).toMonad) :=
  Adjunction.rightAdjointOfNatIso (isoWhiskerLeft R (Monad.comparisonForget (Adjunction.ofRightAdjoint U)).symm : _)
[GOAL]
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✝ : IsRightAdjoint (R ⋙ U)
R' : A ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint U)) :=
  R ⋙ Monad.comparison (Adjunction.ofRightAdjoint U)
this : IsRightAdjoint (R' ⋙ Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint U))) :=
  Adjunction.rightAdjointOfNatIso (isoWhiskerLeft R (Monad.comparisonForget (Adjunction.ofRightAdjoint U)).symm)
⊢ IsRightAdjoint R'
[PROOFSTEP]
let this : ∀ X, RegularEpi ((Monad.adj (Adjunction.ofRightAdjoint U).toMonad).counit.app X) :=
  by
  intro X
  simp only [Monad.adj_counit]
  exact ⟨_, _, _, _, Monad.beckAlgebraCoequalizer X⟩
[GOAL]
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✝ : IsRightAdjoint (R ⋙ U)
R' : A ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint U)) :=
  R ⋙ Monad.comparison (Adjunction.ofRightAdjoint U)
this : IsRightAdjoint (R' ⋙ Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint U))) :=
  Adjunction.rightAdjointOfNatIso (isoWhiskerLeft R (Monad.comparisonForget (Adjunction.ofRightAdjoint U)).symm)
⊢ (X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint U))) →
    RegularEpi (NatTrans.app (Monad.adj (Adjunction.toMonad (Adjunction.ofRightAdjoint U))).counit X)
[PROOFSTEP]
intro X
[GOAL]
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✝ : IsRightAdjoint (R ⋙ U)
R' : A ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint U)) :=
  R ⋙ Monad.comparison (Adjunction.ofRightAdjoint U)
this : IsRightAdjoint (R' ⋙ Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint U))) :=
  Adjunction.rightAdjointOfNatIso (isoWhiskerLeft R (Monad.comparisonForget (Adjunction.ofRightAdjoint U)).symm)
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint U))
⊢ RegularEpi (NatTrans.app (Monad.adj (Adjunction.toMonad (Adjunction.ofRightAdjoint U))).counit X)
[PROOFSTEP]
simp only [Monad.adj_counit]
[GOAL]
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✝ : IsRightAdjoint (R ⋙ U)
R' : A ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint U)) :=
  R ⋙ Monad.comparison (Adjunction.ofRightAdjoint U)
this : IsRightAdjoint (R' ⋙ Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint U))) :=
  Adjunction.rightAdjointOfNatIso (isoWhiskerLeft R (Monad.comparisonForget (Adjunction.ofRightAdjoint U)).symm)
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint U))
⊢ RegularEpi (Monad.Algebra.Hom.mk X.a)
[PROOFSTEP]
exact ⟨_, _, _, _, Monad.beckAlgebraCoequalizer X⟩
[GOAL]
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✝ : IsRightAdjoint (R ⋙ U)
R' : A ⥤ Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint U)) :=
  R ⋙ Monad.comparison (Adjunction.ofRightAdjoint U)
this✝ : IsRightAdjoint (R' ⋙ Monad.forget (Adjunction.toMonad (Adjunction.ofRightAdjoint U))) :=
  Adjunction.rightAdjointOfNatIso (isoWhiskerLeft R (Monad.comparisonForget (Adjunction.ofRightAdjoint U)).symm)
this : (X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint U))) →
  RegularEpi (NatTrans.app (Monad.adj (Adjunction.toMonad (Adjunction.ofRightAdjoint U))).counit X) :=
  fun X =>
    Eq.mpr
      (_ :
        RegularEpi (NatTrans.app (Monad.adj (Adjunction.toMonad (Adjunction.ofRightAdjoint U))).counit X) =
          RegularEpi (Monad.Algebra.Hom.mk X.a))
      (RegularEpi.mk
        ((Monad.free (Adjunction.toMonad (Adjunction.ofRightAdjoint U))).obj
          ((Adjunction.toMonad (Adjunction.ofRightAdjoint U)).toFunctor.obj X.A))
        (Monad.FreeCoequalizer.topMap X) (Monad.FreeCoequalizer.bottomMap X) (Monad.beckAlgebraCoequalizer X))
⊢ IsRightAdjoint R'
[PROOFSTEP]
exact adjointTriangleLift R' (Monad.adj _)
