[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : G ⋙ L₂ ⟶ L₁ ⋙ H
X Y : D
f : X ⟶ Y
⊢ (R₁ ⋙ G).map f ≫
      (fun X =>
          NatTrans.app adj₂.unit (G.obj (R₁.obj X)) ≫
            R₂.map (NatTrans.app h (R₁.obj X) ≫ H.map (NatTrans.app adj₁.counit X)))
        Y =
    (fun X =>
          NatTrans.app adj₂.unit (G.obj (R₁.obj X)) ≫
            R₂.map (NatTrans.app h (R₁.obj X) ≫ H.map (NatTrans.app adj₁.counit X)))
        X ≫
      (H ⋙ R₂).map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : G ⋙ L₂ ⟶ L₁ ⋙ H
X Y : D
f : X ⟶ Y
⊢ G.map (R₁.map f) ≫
      NatTrans.app adj₂.unit (G.obj (R₁.obj Y)) ≫
        R₂.map (NatTrans.app h (R₁.obj Y) ≫ H.map (NatTrans.app adj₁.counit Y)) =
    (NatTrans.app adj₂.unit (G.obj (R₁.obj X)) ≫
        R₂.map (NatTrans.app h (R₁.obj X) ≫ H.map (NatTrans.app adj₁.counit X))) ≫
      R₂.map (H.map f)
[PROOFSTEP]
rw [assoc, ← R₂.map_comp, assoc, ← H.map_comp, ← adj₁.counit_naturality, H.map_comp, ← Functor.comp_map L₁, ←
  h.naturality_assoc]
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : G ⋙ L₂ ⟶ L₁ ⋙ H
X Y : D
f : X ⟶ Y
⊢ G.map (R₁.map f) ≫
      NatTrans.app adj₂.unit (G.obj (R₁.obj Y)) ≫
        R₂.map (NatTrans.app h (R₁.obj Y) ≫ H.map (NatTrans.app adj₁.counit Y)) =
    NatTrans.app adj₂.unit (G.obj (R₁.obj X)) ≫
      R₂.map ((G ⋙ L₂).map (R₁.map f) ≫ NatTrans.app h (R₁.obj Y) ≫ H.map (NatTrans.app adj₁.counit Y))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : R₁ ⋙ G ⟶ H ⋙ R₂
X Y : C
f : X ⟶ Y
⊢ (G ⋙ L₂).map f ≫
      (fun X =>
          L₂.map (G.map (NatTrans.app adj₁.unit X) ≫ NatTrans.app h (L₁.obj X)) ≫
            NatTrans.app adj₂.counit (H.obj (L₁.obj X)))
        Y =
    (fun X =>
          L₂.map (G.map (NatTrans.app adj₁.unit X) ≫ NatTrans.app h (L₁.obj X)) ≫
            NatTrans.app adj₂.counit (H.obj (L₁.obj X)))
        X ≫
      (L₁ ⋙ H).map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : R₁ ⋙ G ⟶ H ⋙ R₂
X Y : C
f : X ⟶ Y
⊢ L₂.map (G.map f) ≫
      L₂.map (G.map (NatTrans.app adj₁.unit Y) ≫ NatTrans.app h (L₁.obj Y)) ≫
        NatTrans.app adj₂.counit (H.obj (L₁.obj Y)) =
    (L₂.map (G.map (NatTrans.app adj₁.unit X) ≫ NatTrans.app h (L₁.obj X)) ≫
        NatTrans.app adj₂.counit (H.obj (L₁.obj X))) ≫
      H.map (L₁.map f)
[PROOFSTEP]
rw [← L₂.map_comp_assoc, ← G.map_comp_assoc, ← adj₁.unit_naturality, G.map_comp_assoc, ← Functor.comp_map, h.naturality]
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : R₁ ⋙ G ⟶ H ⋙ R₂
X Y : C
f : X ⟶ Y
⊢ L₂.map (G.map (NatTrans.app adj₁.unit X) ≫ NatTrans.app h (L₁.obj X) ≫ (H ⋙ R₂).map (L₁.map f)) ≫
      NatTrans.app adj₂.counit (H.obj (L₁.obj Y)) =
    (L₂.map (G.map (NatTrans.app adj₁.unit X) ≫ NatTrans.app h (L₁.obj X)) ≫
        NatTrans.app adj₂.counit (H.obj (L₁.obj X))) ≫
      H.map (L₁.map f)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : G ⋙ L₂ ⟶ L₁ ⋙ H
⊢ (fun h =>
        NatTrans.mk fun X =>
          L₂.map (G.map (NatTrans.app adj₁.unit X) ≫ NatTrans.app h (L₁.obj X)) ≫
            NatTrans.app adj₂.counit (H.obj (L₁.obj X)))
      ((fun h =>
          NatTrans.mk fun X =>
            NatTrans.app adj₂.unit (G.obj (R₁.obj X)) ≫
              R₂.map (NatTrans.app h (R₁.obj X) ≫ H.map (NatTrans.app adj₁.counit X)))
        h) =
    h
[PROOFSTEP]
ext X
[GOAL]
case w.h
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : G ⋙ L₂ ⟶ L₁ ⋙ H
X : C
⊢ NatTrans.app
      ((fun h =>
          NatTrans.mk fun X =>
            L₂.map (G.map (NatTrans.app adj₁.unit X) ≫ NatTrans.app h (L₁.obj X)) ≫
              NatTrans.app adj₂.counit (H.obj (L₁.obj X)))
        ((fun h =>
            NatTrans.mk fun X =>
              NatTrans.app adj₂.unit (G.obj (R₁.obj X)) ≫
                R₂.map (NatTrans.app h (R₁.obj X) ≫ H.map (NatTrans.app adj₁.counit X)))
          h))
      X =
    NatTrans.app h X
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : G ⋙ L₂ ⟶ L₁ ⋙ H
X : C
⊢ L₂.map
        (G.map (NatTrans.app adj₁.unit X) ≫
          NatTrans.app adj₂.unit (G.obj (R₁.obj (L₁.obj X))) ≫
            R₂.map (NatTrans.app h (R₁.obj (L₁.obj X)) ≫ H.map (NatTrans.app adj₁.counit (L₁.obj X)))) ≫
      NatTrans.app adj₂.counit (H.obj (L₁.obj X)) =
    NatTrans.app h X
[PROOFSTEP]
simp only [L₂.map_comp, assoc, adj₂.counit_naturality, adj₂.left_triangle_components_assoc, ← Functor.comp_map G L₂,
  h.naturality_assoc, Functor.comp_map L₁, ← H.map_comp, adj₁.left_triangle_components]
[GOAL]
case w.h
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : G ⋙ L₂ ⟶ L₁ ⋙ H
X : C
⊢ NatTrans.app h X ≫ H.map (𝟙 (L₁.obj X)) = NatTrans.app h X
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : G ⋙ L₂ ⟶ L₁ ⋙ H
X : C
⊢ NatTrans.app h X ≫ H.map (𝟙 (L₁.obj X)) = NatTrans.app h X
[PROOFSTEP]
simp only [id_comp, ← Functor.comp_map, ← Functor.comp_obj, NatTrans.naturality_assoc]
[GOAL]
case w.h
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : G ⋙ L₂ ⟶ L₁ ⋙ H
X : C
⊢ NatTrans.app h X ≫ H.map (𝟙 (L₁.obj X)) = NatTrans.app h X
[PROOFSTEP]
simp only [Functor.comp_obj, Functor.comp_map, ← Functor.map_comp]
[GOAL]
case w.h
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : G ⋙ L₂ ⟶ L₁ ⋙ H
X : C
⊢ NatTrans.app h X ≫ H.map (𝟙 (L₁.obj X)) = NatTrans.app h X
[PROOFSTEP]
have :
  Prefunctor.map L₁.toPrefunctor (NatTrans.app adj₁.unit X) ≫
      NatTrans.app adj₁.counit (Prefunctor.obj L₁.toPrefunctor X) =
    𝟙 _ :=
  by simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : G ⋙ L₂ ⟶ L₁ ⋙ H
X : C
⊢ L₁.map (NatTrans.app adj₁.unit X) ≫ NatTrans.app adj₁.counit (L₁.obj X) = 𝟙 (L₁.obj ((𝟭 C).obj X))
[PROOFSTEP]
simp
[GOAL]
case w.h
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : G ⋙ L₂ ⟶ L₁ ⋙ H
X : C
this : L₁.map (NatTrans.app adj₁.unit X) ≫ NatTrans.app adj₁.counit (L₁.obj X) = 𝟙 (L₁.obj ((𝟭 C).obj X))
⊢ NatTrans.app h X ≫ H.map (𝟙 (L₁.obj X)) = NatTrans.app h X
[PROOFSTEP]
simp [this]
  -- See library note [dsimp, simp].
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : R₁ ⋙ G ⟶ H ⋙ R₂
⊢ (fun h =>
        NatTrans.mk fun X =>
          NatTrans.app adj₂.unit (G.obj (R₁.obj X)) ≫
            R₂.map (NatTrans.app h (R₁.obj X) ≫ H.map (NatTrans.app adj₁.counit X)))
      ((fun h =>
          NatTrans.mk fun X =>
            L₂.map (G.map (NatTrans.app adj₁.unit X) ≫ NatTrans.app h (L₁.obj X)) ≫
              NatTrans.app adj₂.counit (H.obj (L₁.obj X)))
        h) =
    h
[PROOFSTEP]
ext X
[GOAL]
case w.h
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : R₁ ⋙ G ⟶ H ⋙ R₂
X : D
⊢ NatTrans.app
      ((fun h =>
          NatTrans.mk fun X =>
            NatTrans.app adj₂.unit (G.obj (R₁.obj X)) ≫
              R₂.map (NatTrans.app h (R₁.obj X) ≫ H.map (NatTrans.app adj₁.counit X)))
        ((fun h =>
            NatTrans.mk fun X =>
              L₂.map (G.map (NatTrans.app adj₁.unit X) ≫ NatTrans.app h (L₁.obj X)) ≫
                NatTrans.app adj₂.counit (H.obj (L₁.obj X)))
          h))
      X =
    NatTrans.app h X
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
h : R₁ ⋙ G ⟶ H ⋙ R₂
X : D
⊢ NatTrans.app adj₂.unit (G.obj (R₁.obj X)) ≫
      R₂.map
        ((L₂.map (G.map (NatTrans.app adj₁.unit (R₁.obj X)) ≫ NatTrans.app h (L₁.obj (R₁.obj X))) ≫
            NatTrans.app adj₂.counit (H.obj (L₁.obj (R₁.obj X)))) ≫
          H.map (NatTrans.app adj₁.counit X)) =
    NatTrans.app h X
[PROOFSTEP]
simp [-Functor.comp_map, ← Functor.comp_map H, Functor.comp_map R₁, -NatTrans.naturality, ← h.naturality,
  -Functor.map_comp, ← Functor.map_comp_assoc G, R₂.map_comp]
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : G ⋙ L₂ ⟶ L₁ ⋙ H
Y : D
⊢ L₂.map (NatTrans.app (↑(transferNatTrans adj₁ adj₂) f) Y) ≫ NatTrans.app adj₂.counit (H.obj Y) =
    NatTrans.app f (R₁.obj Y) ≫ H.map (NatTrans.app adj₁.counit Y)
[PROOFSTEP]
erw [Functor.map_comp]
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : G ⋙ L₂ ⟶ L₁ ⋙ H
Y : D
⊢ (L₂.map (NatTrans.app adj₂.unit (G.obj (R₁.obj Y))) ≫
        L₂.map (R₂.map (NatTrans.app f (R₁.obj Y) ≫ H.map (NatTrans.app adj₁.counit Y)))) ≫
      NatTrans.app adj₂.counit (H.obj Y) =
    NatTrans.app f (R₁.obj Y) ≫ H.map (NatTrans.app adj₁.counit Y)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : G ⋙ L₂ ⟶ L₁ ⋙ H
X : C
⊢ G.map (NatTrans.app adj₁.unit X) ≫ NatTrans.app (↑(transferNatTrans adj₁ adj₂) f) (L₁.obj X) =
    NatTrans.app adj₂.unit (G.obj ((𝟭 C).obj X)) ≫ R₂.map (NatTrans.app f ((𝟭 C).obj X))
[PROOFSTEP]
dsimp [transferNatTrans]
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : G ⋙ L₂ ⟶ L₁ ⋙ H
X : C
⊢ G.map (NatTrans.app adj₁.unit X) ≫
      NatTrans.app adj₂.unit (G.obj (R₁.obj (L₁.obj X))) ≫
        R₂.map (NatTrans.app f (R₁.obj (L₁.obj X)) ≫ H.map (NatTrans.app adj₁.counit (L₁.obj X))) =
    NatTrans.app adj₂.unit (G.obj X) ≫ R₂.map (NatTrans.app f X)
[PROOFSTEP]
rw [← adj₂.unit_naturality_assoc, ← R₂.map_comp, ← Functor.comp_map G L₂, f.naturality_assoc, Functor.comp_map, ←
  H.map_comp]
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : G ⋙ L₂ ⟶ L₁ ⋙ H
X : C
⊢ NatTrans.app adj₂.unit (G.obj X) ≫
      R₂.map (NatTrans.app f X ≫ H.map (L₁.map (NatTrans.app adj₁.unit X) ≫ NatTrans.app adj₁.counit (L₁.obj X))) =
    NatTrans.app adj₂.unit (G.obj X) ≫ R₂.map (NatTrans.app f X)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
E : Type u₃
F : Type u₄
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : G ⋙ L₂ ⟶ L₁ ⋙ H
X : C
⊢ NatTrans.app adj₂.unit (G.obj X) ≫
      R₂.map (NatTrans.app f X ≫ H.map (L₁.map (NatTrans.app adj₁.unit X) ≫ NatTrans.app adj₁.counit (L₁.obj X))) =
    NatTrans.app adj₂.unit (G.obj X) ≫ R₂.map (NatTrans.app f X)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : D
⊢ L₂.map (NatTrans.app (↑(transferNatTransSelf adj₁ adj₂) f) X) ≫ NatTrans.app adj₂.counit X =
    NatTrans.app f (R₁.obj X) ≫ NatTrans.app adj₁.counit X
[PROOFSTEP]
dsimp [transferNatTransSelf]
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : D
⊢ L₂.map
        (𝟙 (R₁.obj X) ≫
          NatTrans.app (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv))
              X ≫
            𝟙 (R₂.obj X)) ≫
      NatTrans.app adj₂.counit X =
    NatTrans.app f (R₁.obj X) ≫ NatTrans.app adj₁.counit X
[PROOFSTEP]
rw [id_comp, comp_id]
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : D
⊢ L₂.map
        (NatTrans.app (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv))
          X) ≫
      NatTrans.app adj₂.counit X =
    NatTrans.app f (R₁.obj X) ≫ NatTrans.app adj₁.counit X
[PROOFSTEP]
have := transferNatTrans_counit adj₁ adj₂ (L₂.leftUnitor.hom ≫ f ≫ L₁.rightUnitor.inv) X
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : D
this :
  L₂.map
        (NatTrans.app (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv))
          X) ≫
      NatTrans.app adj₂.counit ((𝟭 D).obj X) =
    NatTrans.app ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv) (R₁.obj X) ≫
      (𝟭 D).map (NatTrans.app adj₁.counit X)
⊢ L₂.map
        (NatTrans.app (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv))
          X) ≫
      NatTrans.app adj₂.counit X =
    NatTrans.app f (R₁.obj X) ≫ NatTrans.app adj₁.counit X
[PROOFSTEP]
dsimp at this 
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : D
this :
  L₂.map
        (NatTrans.app (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv))
          X) ≫
      NatTrans.app adj₂.counit X =
    (𝟙 (L₂.obj (R₁.obj X)) ≫ NatTrans.app f (R₁.obj X) ≫ 𝟙 (L₁.obj (R₁.obj X))) ≫ NatTrans.app adj₁.counit X
⊢ L₂.map
        (NatTrans.app (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv))
          X) ≫
      NatTrans.app adj₂.counit X =
    NatTrans.app f (R₁.obj X) ≫ NatTrans.app adj₁.counit X
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : D
this :
  L₂.map
        (NatTrans.app (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv))
          X) ≫
      NatTrans.app adj₂.counit X =
    (𝟙 (L₂.obj (R₁.obj X)) ≫ NatTrans.app f (R₁.obj X) ≫ 𝟙 (L₁.obj (R₁.obj X))) ≫ NatTrans.app adj₁.counit X
⊢ (𝟙 (L₂.obj (R₁.obj X)) ≫ NatTrans.app f (R₁.obj X) ≫ 𝟙 (L₁.obj (R₁.obj X))) ≫ NatTrans.app adj₁.counit X =
    NatTrans.app f (R₁.obj X) ≫ NatTrans.app adj₁.counit X
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : C
⊢ NatTrans.app adj₁.unit X ≫ NatTrans.app (↑(transferNatTransSelf adj₁ adj₂) f) (L₁.obj X) =
    NatTrans.app adj₂.unit X ≫ R₂.map (NatTrans.app f X)
[PROOFSTEP]
dsimp [transferNatTransSelf]
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : C
⊢ NatTrans.app adj₁.unit X ≫
      𝟙 (R₁.obj (L₁.obj X)) ≫
        NatTrans.app (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv))
            (L₁.obj X) ≫
          𝟙 (R₂.obj (L₁.obj X)) =
    NatTrans.app adj₂.unit X ≫ R₂.map (NatTrans.app f X)
[PROOFSTEP]
rw [id_comp, comp_id]
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : C
⊢ NatTrans.app adj₁.unit X ≫
      NatTrans.app (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv))
        (L₁.obj X) =
    NatTrans.app adj₂.unit X ≫ R₂.map (NatTrans.app f X)
[PROOFSTEP]
have := unit_transferNatTrans adj₁ adj₂ (L₂.leftUnitor.hom ≫ f ≫ L₁.rightUnitor.inv) X
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : C
this :
  (𝟭 C).map (NatTrans.app adj₁.unit X) ≫
      NatTrans.app (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv))
        (L₁.obj X) =
    NatTrans.app adj₂.unit ((𝟭 C).obj ((𝟭 C).obj X)) ≫
      R₂.map (NatTrans.app ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv) ((𝟭 C).obj X))
⊢ NatTrans.app adj₁.unit X ≫
      NatTrans.app (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv))
        (L₁.obj X) =
    NatTrans.app adj₂.unit X ≫ R₂.map (NatTrans.app f X)
[PROOFSTEP]
dsimp at this 
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : C
this :
  NatTrans.app adj₁.unit X ≫
      NatTrans.app (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv))
        (L₁.obj X) =
    NatTrans.app adj₂.unit X ≫ R₂.map (𝟙 (L₂.obj X) ≫ NatTrans.app f X ≫ 𝟙 (L₁.obj X))
⊢ NatTrans.app adj₁.unit X ≫
      NatTrans.app (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv))
        (L₁.obj X) =
    NatTrans.app adj₂.unit X ≫ R₂.map (NatTrans.app f X)
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
X : C
this :
  NatTrans.app adj₁.unit X ≫
      NatTrans.app (↑(transferNatTrans adj₁ adj₂) ((Functor.leftUnitor L₂).hom ≫ f ≫ (Functor.rightUnitor L₁).inv))
        (L₁.obj X) =
    NatTrans.app adj₂.unit X ≫ R₂.map (𝟙 (L₂.obj X) ≫ NatTrans.app f X ≫ 𝟙 (L₁.obj X))
⊢ NatTrans.app adj₂.unit X ≫ R₂.map (𝟙 (L₂.obj X) ≫ NatTrans.app f X ≫ 𝟙 (L₁.obj X)) =
    NatTrans.app adj₂.unit X ≫ R₂.map (NatTrans.app f X)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
⊢ ↑(transferNatTransSelf adj₁ adj₁) (𝟙 L₁) = 𝟙 R₁
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
x✝ : D
⊢ NatTrans.app (↑(transferNatTransSelf adj₁ adj₁) (𝟙 L₁)) x✝ = NatTrans.app (𝟙 R₁) x✝
[PROOFSTEP]
dsimp [transferNatTransSelf, transferNatTrans]
[GOAL]
case w.h
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
x✝ : D
⊢ 𝟙 (R₁.obj x✝) ≫
      (NatTrans.app adj₁.unit (R₁.obj x✝) ≫
          R₁.map
            ((𝟙 (L₁.obj (R₁.obj x✝)) ≫ 𝟙 (L₁.obj (R₁.obj x✝)) ≫ 𝟙 (L₁.obj (R₁.obj x✝))) ≫
              NatTrans.app adj₁.counit x✝)) ≫
        𝟙 (R₁.obj x✝) =
    𝟙 (R₁.obj x✝)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
⊢ ↑(transferNatTransSelf adj₁ adj₁).symm (𝟙 R₁) = 𝟙 L₁
[PROOFSTEP]
rw [Equiv.symm_apply_eq]
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
⊢ 𝟙 R₁ = ↑(transferNatTransSelf adj₁ adj₁) (𝟙 L₁)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
g : L₃ ⟶ L₂
⊢ ↑(transferNatTransSelf adj₁ adj₂) f ≫ ↑(transferNatTransSelf adj₂ adj₃) g = ↑(transferNatTransSelf adj₁ adj₃) (g ≫ f)
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
g : L₃ ⟶ L₂
x✝ : D
⊢ NatTrans.app (↑(transferNatTransSelf adj₁ adj₂) f ≫ ↑(transferNatTransSelf adj₂ adj₃) g) x✝ =
    NatTrans.app (↑(transferNatTransSelf adj₁ adj₃) (g ≫ f)) x✝
[PROOFSTEP]
dsimp [transferNatTransSelf, transferNatTrans]
[GOAL]
case w.h
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
g : L₃ ⟶ L₂
x✝ : D
⊢ (𝟙 (R₁.obj x✝) ≫
        (NatTrans.app adj₂.unit (R₁.obj x✝) ≫
            R₂.map
              ((𝟙 (L₂.obj (R₁.obj x✝)) ≫ NatTrans.app f (R₁.obj x✝) ≫ 𝟙 (L₁.obj (R₁.obj x✝))) ≫
                NatTrans.app adj₁.counit x✝)) ≫
          𝟙 (R₂.obj x✝)) ≫
      𝟙 (R₂.obj x✝) ≫
        (NatTrans.app adj₃.unit (R₂.obj x✝) ≫
            R₃.map
              ((𝟙 (L₃.obj (R₂.obj x✝)) ≫ NatTrans.app g (R₂.obj x✝) ≫ 𝟙 (L₂.obj (R₂.obj x✝))) ≫
                NatTrans.app adj₂.counit x✝)) ≫
          𝟙 (R₃.obj x✝) =
    𝟙 (R₁.obj x✝) ≫
      (NatTrans.app adj₃.unit (R₁.obj x✝) ≫
          R₃.map
            ((𝟙 (L₃.obj (R₁.obj x✝)) ≫
                (NatTrans.app g (R₁.obj x✝) ≫ NatTrans.app f (R₁.obj x✝)) ≫ 𝟙 (L₁.obj (R₁.obj x✝))) ≫
              NatTrans.app adj₁.counit x✝)) ≫
        𝟙 (R₃.obj x✝)
[PROOFSTEP]
simp only [id_comp, comp_id]
[GOAL]
case w.h
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
g : L₃ ⟶ L₂
x✝ : D
⊢ (NatTrans.app adj₂.unit (R₁.obj x✝) ≫ R₂.map (NatTrans.app f (R₁.obj x✝) ≫ NatTrans.app adj₁.counit x✝)) ≫
      NatTrans.app adj₃.unit (R₂.obj x✝) ≫ R₃.map (NatTrans.app g (R₂.obj x✝) ≫ NatTrans.app adj₂.counit x✝) =
    NatTrans.app adj₃.unit (R₁.obj x✝) ≫
      R₃.map ((NatTrans.app g (R₁.obj x✝) ≫ NatTrans.app f (R₁.obj x✝)) ≫ NatTrans.app adj₁.counit x✝)
[PROOFSTEP]
rw [← adj₃.unit_naturality_assoc, ← R₃.map_comp, g.naturality_assoc, L₂.map_comp, assoc, adj₂.counit_naturality,
  adj₂.left_triangle_components_assoc, assoc]
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
L R : C ⥤ C
adj : L ⊣ R
f : 𝟭 C ⟶ L
X : C
⊢ NatTrans.app (↑(transferNatTransSelf adj Adjunction.id) f) X = NatTrans.app f (R.obj X) ≫ NatTrans.app adj.counit X
[PROOFSTEP]
dsimp [transferNatTransSelf, transferNatTrans, Adjunction.id]
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
L R : C ⥤ C
adj : L ⊣ R
f : 𝟭 C ⟶ L
X : C
⊢ 𝟙 (R.obj X) ≫
      (𝟙 (R.obj X) ≫ (𝟙 (R.obj X) ≫ NatTrans.app f (R.obj X) ≫ 𝟙 (L.obj (R.obj X))) ≫ NatTrans.app adj.counit X) ≫ 𝟙 X =
    NatTrans.app f (R.obj X) ≫ NatTrans.app adj.counit X
[PROOFSTEP]
simp only [comp_id, id_comp]
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
L R : C ⥤ C
adj : L ⊣ R
g : R ⟶ 𝟭 C
X : C
⊢ NatTrans.app (↑(transferNatTransSelf adj Adjunction.id).symm g) X = NatTrans.app adj.unit X ≫ NatTrans.app g (L.obj X)
[PROOFSTEP]
dsimp [transferNatTransSelf, transferNatTrans, Adjunction.id]
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
L R : C ⥤ C
adj : L ⊣ R
g : R ⟶ 𝟭 C
X : C
⊢ 𝟙 X ≫
      ((NatTrans.app adj.unit X ≫ 𝟙 (R.obj (L.obj X)) ≫ NatTrans.app g (L.obj X) ≫ 𝟙 (L.obj X)) ≫ 𝟙 (L.obj X)) ≫
        𝟙 (L.obj X) =
    NatTrans.app adj.unit X ≫ NatTrans.app g (L.obj X)
[PROOFSTEP]
simp only [comp_id, id_comp]
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : R₂ ⟶ R₁
g : R₃ ⟶ R₂
⊢ ↑(transferNatTransSelf adj₂ adj₁).symm f ≫ ↑(transferNatTransSelf adj₃ adj₂).symm g =
    ↑(transferNatTransSelf adj₃ adj₁).symm (g ≫ f)
[PROOFSTEP]
rw [Equiv.eq_symm_apply, ← transferNatTransSelf_comp _ adj₂]
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : R₂ ⟶ R₁
g : R₃ ⟶ R₂
⊢ ↑(transferNatTransSelf adj₃ adj₂) (↑(transferNatTransSelf adj₃ adj₂).symm g) ≫
      ↑(transferNatTransSelf adj₂ adj₁) (↑(transferNatTransSelf adj₂ adj₁).symm f) =
    g ≫ f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
g : L₁ ⟶ L₂
gf : g ≫ f = 𝟙 L₁
⊢ ↑(transferNatTransSelf adj₁ adj₂) f ≫ ↑(transferNatTransSelf adj₂ adj₁) g = 𝟙 R₁
[PROOFSTEP]
rw [transferNatTransSelf_comp, gf, transferNatTransSelf_id]
[GOAL]
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : R₁ ⟶ R₂
g : R₂ ⟶ R₁
gf : g ≫ f = 𝟙 R₂
⊢ ↑(transferNatTransSelf adj₁ adj₂).symm f ≫ ↑(transferNatTransSelf adj₂ adj₁).symm g = 𝟙 L₂
[PROOFSTEP]
rw [transferNatTransSelf_symm_comp, gf, transferNatTransSelf_symm_id]
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
inst✝ : IsIso f
⊢ inv f ≫ f = 𝟙 L₁
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
inst✝ : IsIso f
⊢ f ≫ inv f = 𝟙 L₂
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : R₁ ⟶ R₂
inst✝ : IsIso f
⊢ inv f ≫ f = 𝟙 R₂
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : R₁ ⟶ R₂
inst✝ : IsIso f
⊢ f ≫ inv f = 𝟙 R₁
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
inst✝ : IsIso (↑(transferNatTransSelf adj₁ adj₂) f)
⊢ IsIso f
[PROOFSTEP]
suffices IsIso ((transferNatTransSelf adj₁ adj₂).symm (transferNatTransSelf adj₁ adj₂ f)) by simpa using this
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
inst✝ : IsIso (↑(transferNatTransSelf adj₁ adj₂) f)
this : IsIso (↑(transferNatTransSelf adj₁ adj₂).symm (↑(transferNatTransSelf adj₁ adj₂) f))
⊢ IsIso f
[PROOFSTEP]
simpa using this
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : L₂ ⟶ L₁
inst✝ : IsIso (↑(transferNatTransSelf adj₁ adj₂) f)
⊢ IsIso (↑(transferNatTransSelf adj₁ adj₂).symm (↑(transferNatTransSelf adj₁ adj₂) f))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : R₁ ⟶ R₂
inst✝ : IsIso (↑(transferNatTransSelf adj₁ adj₂).symm f)
⊢ IsIso f
[PROOFSTEP]
suffices IsIso ((transferNatTransSelf adj₁ adj₂) ((transferNatTransSelf adj₁ adj₂).symm f)) by simpa using this
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : R₁ ⟶ R₂
inst✝ : IsIso (↑(transferNatTransSelf adj₁ adj₂).symm f)
this : IsIso (↑(transferNatTransSelf adj₁ adj₂) (↑(transferNatTransSelf adj₁ adj₂).symm f))
⊢ IsIso f
[PROOFSTEP]
simpa using this
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ L₃ : C ⥤ D
R₁ R₂ R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
f : R₁ ⟶ R₂
inst✝ : IsIso (↑(transferNatTransSelf adj₁ adj₂).symm f)
⊢ IsIso (↑(transferNatTransSelf adj₁ adj₂) (↑(transferNatTransSelf adj₁ adj₂).symm f))
[PROOFSTEP]
infer_instance
