[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ (L ⋙ R).map (NatTrans.app (whiskerRight (whiskerLeft L h.counit) R) X) ≫
      NatTrans.app (whiskerRight (whiskerLeft L h.counit) R) X =
    NatTrans.app (whiskerRight (whiskerLeft L h.counit) R) ((L ⋙ R).obj X) ≫
      NatTrans.app (whiskerRight (whiskerLeft L h.counit) R) X
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ R.map (L.map (R.map (NatTrans.app h.counit (L.obj X)))) ≫ R.map (NatTrans.app h.counit (L.obj X)) =
    R.map (NatTrans.app h.counit (L.obj (R.obj (L.obj X)))) ≫ R.map (NatTrans.app h.counit (L.obj X))
[PROOFSTEP]
rw [← R.map_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ R.map (L.map (R.map (NatTrans.app h.counit (L.obj X))) ≫ NatTrans.app h.counit (L.obj X)) =
    R.map (NatTrans.app h.counit (L.obj (R.obj (L.obj X)))) ≫ R.map (NatTrans.app h.counit (L.obj X))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ (L ⋙ R).map (NatTrans.app h.unit X) ≫ NatTrans.app (whiskerRight (whiskerLeft L h.counit) R) X =
    𝟙 ((L ⋙ R).obj ((𝟭 C).obj X))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ R.map (L.map (NatTrans.app h.unit X)) ≫ R.map (NatTrans.app h.counit (L.obj X)) = 𝟙 (R.obj (L.obj X))
[PROOFSTEP]
rw [← R.map_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ R.map (L.map (NatTrans.app h.unit X) ≫ NatTrans.app h.counit (L.obj X)) = 𝟙 (R.obj (L.obj X))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : D
⊢ NatTrans.app (whiskerRight (whiskerLeft R h.unit) L) X ≫
      (R ⋙ L).map (NatTrans.app (whiskerRight (whiskerLeft R h.unit) L) X) =
    NatTrans.app (whiskerRight (whiskerLeft R h.unit) L) X ≫
      NatTrans.app (whiskerRight (whiskerLeft R h.unit) L) ((R ⋙ L).obj X)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : D
⊢ L.map (NatTrans.app h.unit (R.obj X)) ≫ L.map (R.map (L.map (NatTrans.app h.unit (R.obj X)))) =
    L.map (NatTrans.app h.unit (R.obj X)) ≫ L.map (NatTrans.app h.unit (R.obj (L.obj (R.obj X))))
[PROOFSTEP]
rw [← L.map_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : D
⊢ L.map (NatTrans.app h.unit (R.obj X) ≫ R.map (L.map (NatTrans.app h.unit (R.obj X)))) =
    L.map (NatTrans.app h.unit (R.obj X)) ≫ L.map (NatTrans.app h.unit (R.obj (L.obj (R.obj X))))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : D
⊢ NatTrans.app (whiskerRight (whiskerLeft R h.unit) L) X ≫ (R ⋙ L).map (NatTrans.app h.counit X) = 𝟙 ((R ⋙ L).obj X)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : D
⊢ L.map (NatTrans.app h.unit (R.obj X)) ≫ L.map (R.map (NatTrans.app h.counit X)) = 𝟙 (L.obj (R.obj X))
[PROOFSTEP]
rw [← L.map_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : D
⊢ L.map (NatTrans.app h.unit (R.obj X) ≫ R.map (NatTrans.app h.counit X)) = 𝟙 (L.obj (R.obj X))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : D
⊢ NatTrans.app (μ (Adjunction.toMonad h)) (R.obj X) ≫ R.map (NatTrans.app h.counit X) =
    (Adjunction.toMonad h).toFunctor.map (R.map (NatTrans.app h.counit X)) ≫ R.map (NatTrans.app h.counit X)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : D
⊢ R.map (NatTrans.app h.counit (L.obj (R.obj X))) ≫ R.map (NatTrans.app h.counit X) =
    R.map (L.map (R.map (NatTrans.app h.counit X))) ≫ R.map (NatTrans.app h.counit X)
[PROOFSTEP]
rw [← R.map_comp, ← Adjunction.counit_naturality, R.map_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ (Adjunction.toMonad h).toFunctor.map (R.map f) ≫
      ((fun X => Algebra.mk (R.obj X) (R.map (NatTrans.app h.counit X))) Y✝).a =
    ((fun X => Algebra.mk (R.obj X) (R.map (NatTrans.app h.counit X))) X✝).a ≫ R.map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ R.map (L.map (R.map f)) ≫ R.map (NatTrans.app h.counit Y✝) = R.map (NatTrans.app h.counit X✝) ≫ R.map f
[PROOFSTEP]
rw [← R.map_comp, Adjunction.counit_naturality, R.map_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
T : Monad C
x✝¹ x✝ : Monad.Algebra T
f : (Monad.comparison (Monad.adj T)).obj x✝¹ ⟶ (Monad.comparison (Monad.adj T)).obj x✝
⊢ T.map f.f ≫ x✝.a = x✝¹.a ≫ f.f
[PROOFSTEP]
simpa using f.h
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
T : Monad C
X : Monad.Algebra (Adjunction.toMonad (Monad.adj T))
⊢ NatTrans.app (Monad.η T) X.A ≫ X.a = 𝟙 X.A
[PROOFSTEP]
simpa using X.unit
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
T : Monad C
X : Monad.Algebra (Adjunction.toMonad (Monad.adj T))
⊢ NatTrans.app (Monad.μ T) X.A ≫ X.a = T.map X.a ≫ X.a
[PROOFSTEP]
simpa using X.assoc
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ L.map (NatTrans.app h.unit X) ≫ NatTrans.app (δ (Adjunction.toComonad h)) (L.obj X) =
    L.map (NatTrans.app h.unit X) ≫ (Adjunction.toComonad h).toFunctor.map (L.map (NatTrans.app h.unit X))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ L.map (NatTrans.app h.unit X) ≫ L.map (NatTrans.app h.unit (R.obj (L.obj X))) =
    L.map (NatTrans.app h.unit X) ≫ L.map (R.map (L.map (NatTrans.app h.unit X)))
[PROOFSTEP]
rw [← L.map_comp, ← Adjunction.unit_naturality, L.map_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ ((fun X => Coalgebra.mk (L.obj X) (L.map (NatTrans.app h.unit X))) X✝).a ≫
      (Adjunction.toComonad h).toFunctor.map (L.map f) =
    L.map f ≫ ((fun X => Coalgebra.mk (L.obj X) (L.map (NatTrans.app h.unit X))) Y✝).a
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ L.map (NatTrans.app h.unit X✝) ≫ L.map (R.map (L.map f)) = L.map f ≫ L.map (NatTrans.app h.unit Y✝)
[PROOFSTEP]
rw [← L.map_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ L.map (NatTrans.app h.unit X✝ ≫ R.map (L.map f)) = L.map f ≫ L.map (NatTrans.app h.unit Y✝)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
G : Comonad C
X✝ Y✝ : Comonad.Coalgebra G
f : (Comonad.comparison (Comonad.adj G)).obj X✝ ⟶ (Comonad.comparison (Comonad.adj G)).obj Y✝
⊢ X✝.a ≫ G.map f.f = f.f ≫ Y✝.a
[PROOFSTEP]
simpa using f.h
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
G : Comonad C
X : Comonad.Coalgebra (Adjunction.toComonad (Comonad.adj G))
⊢ X.a ≫ NatTrans.app (Comonad.ε G) X.A = 𝟙 X.A
[PROOFSTEP]
simpa using X.counit
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
G : Comonad C
X : Comonad.Coalgebra (Adjunction.toComonad (Comonad.adj G))
⊢ X.a ≫ NatTrans.app (Comonad.δ G) X.A = X.a ≫ G.map X.a
[PROOFSTEP]
simpa using X.coassoc
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
⊢ IsIso (Monad.μ (Adjunction.toMonad (Adjunction.ofRightAdjoint R)))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
⊢ IsIso (whiskerRight (whiskerLeft (leftAdjoint R) (Adjunction.ofRightAdjoint R).counit) R)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
⊢ X.a ≫ NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A = 𝟙 ((leftAdjoint R ⋙ R).obj X.A)
[PROOFSTEP]
dsimp only [Functor.id_obj]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
⊢ X.a ≫ NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A = 𝟙 ((leftAdjoint R ⋙ R).obj X.A)
[PROOFSTEP]
rw [← (Adjunction.ofRightAdjoint R).unit_naturality]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
⊢ NatTrans.app (Adjunction.ofRightAdjoint R).unit ((leftAdjoint R ⋙ R).obj X.A) ≫ R.map ((leftAdjoint R).map X.a) =
    𝟙 ((leftAdjoint R ⋙ R).obj X.A)
[PROOFSTEP]
dsimp only [Functor.comp_obj, Adjunction.toMonad_coe]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
⊢ NatTrans.app (Adjunction.ofRightAdjoint R).unit (R.obj ((leftAdjoint R).obj X.A)) ≫ R.map ((leftAdjoint R).map X.a) =
    𝟙 (R.obj ((leftAdjoint R).obj X.A))
[PROOFSTEP]
rw [unit_obj_eq_map_unit, ← Functor.map_comp, ← Functor.map_comp]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
⊢ R.map ((leftAdjoint R).map (NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A ≫ X.a)) =
    𝟙 (R.obj ((leftAdjoint R).obj X.A))
[PROOFSTEP]
erw [X.unit]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
⊢ R.map ((leftAdjoint R).map (𝟙 X.A)) = 𝟙 (R.obj ((leftAdjoint R).obj X.A))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
⊢ EssSurj (Monad.comparison (Adjunction.ofRightAdjoint R))
[PROOFSTEP]
refine' ⟨fun X => ⟨(leftAdjoint R).obj X.A, ⟨_⟩⟩⟩
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
⊢ (Monad.comparison (Adjunction.ofRightAdjoint R)).obj ((leftAdjoint R).obj X.A) ≅ X
[PROOFSTEP]
symm
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
⊢ X ≅ (Monad.comparison (Adjunction.ofRightAdjoint R)).obj ((leftAdjoint R).obj X.A)
[PROOFSTEP]
refine' Monad.Algebra.isoMk _ _
[GOAL]
case refine'_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
⊢ X.A ≅ ((Monad.comparison (Adjunction.ofRightAdjoint R)).obj ((leftAdjoint R).obj X.A)).A
[PROOFSTEP]
exact asIso ((Adjunction.ofRightAdjoint R).unit.app X.A)
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
⊢ (Adjunction.toMonad (Adjunction.ofRightAdjoint R)).toFunctor.map
        (asIso (NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A)).hom ≫
      ((Monad.comparison (Adjunction.ofRightAdjoint R)).obj ((leftAdjoint R).obj X.A)).a =
    X.a ≫ (asIso (NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A)).hom
[PROOFSTEP]
dsimp only [Functor.comp_map, Monad.comparison_obj_a, asIso_hom, Functor.comp_obj, Monad.comparison_obj_A,
  Adjunction.toMonad_coe]
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
⊢ R.map ((leftAdjoint R).map (NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A)) ≫
      R.map (NatTrans.app (Adjunction.ofRightAdjoint R).counit ((leftAdjoint R).obj X.A)) =
    X.a ≫ NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A
[PROOFSTEP]
rw [← cancel_epi ((Adjunction.ofRightAdjoint R).unit.app X.A)]
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
⊢ NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A ≫
      R.map ((leftAdjoint R).map (NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A)) ≫
        R.map (NatTrans.app (Adjunction.ofRightAdjoint R).counit ((leftAdjoint R).obj X.A)) =
    NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A ≫ X.a ≫ NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A
[PROOFSTEP]
dsimp only [Functor.id_obj, Functor.comp_obj]
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
⊢ NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A ≫
      R.map ((leftAdjoint R).map (NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A)) ≫
        R.map (NatTrans.app (Adjunction.ofRightAdjoint R).counit ((leftAdjoint R).obj X.A)) =
    NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A ≫ X.a ≫ NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A
[PROOFSTEP]
rw [Adjunction.unit_naturality_assoc, Adjunction.right_triangle_components, comp_id]
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
⊢ NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A =
    NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A ≫ X.a ≫ NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A
[PROOFSTEP]
apply (X.unit_assoc _).symm
