case w.h
C : Type u₁
D : Type u₂
inst✝¹ : Category C
inst✝ : Category 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
⊢ (↑(transferNatTransSelf adj₁ adj₂) f ≫ ↑(transferNatTransSelf adj₂ adj₃) g).app x✝ =
    (↑(transferNatTransSelf adj₁ adj₃) (g ≫ f)).app x✝
C : Type u₁
D : Type u₂
inst✝¹ : Category C
inst✝ : Category 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)
ext
case w.h
C : Type u₁
D : Type u₂
inst✝¹ : Category C
inst✝ : Category 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✝) ≫
        (adj₂.unit.app (R₁.obj x✝) ≫
            R₂.map ((𝟙 (L₂.obj (R₁.obj x✝)) ≫ f.app (R₁.obj x✝) ≫ 𝟙 (L₁.obj (R₁.obj x✝))) ≫ adj₁.counit.app x✝)) ≫
          𝟙 (R₂.obj x✝)) ≫
      𝟙 (R₂.obj x✝) ≫
        (adj₃.unit.app (R₂.obj x✝) ≫
            R₃.map ((𝟙 (L₃.obj (R₂.obj x✝)) ≫ g.app (R₂.obj x✝) ≫ 𝟙 (L₂.obj (R₂.obj x✝))) ≫ adj₂.counit.app x✝)) ≫
          𝟙 (R₃.obj x✝) =
    𝟙 (R₁.obj x✝) ≫
      (adj₃.unit.app (R₁.obj x✝) ≫
          R₃.map
            ((𝟙 (L₃.obj (R₁.obj x✝)) ≫ (g.app (R₁.obj x✝) ≫ f.app (R₁.obj x✝)) ≫ 𝟙 (L₁.obj (R₁.obj x✝))) ≫
              adj₁.counit.app x✝)) ≫
        𝟙 (R₃.obj x✝)
case w.h
C : Type u₁
D : Type u₂
inst✝¹ : Category C
inst✝ : Category 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
⊢ (↑(transferNatTransSelf adj₁ adj₂) f ≫ ↑(transferNatTransSelf adj₂ adj₃) g).app x✝ =
    (↑(transferNatTransSelf adj₁ adj₃) (g ≫ f)).app x✝
dsimp [transferNatTransSelf, transferNatTrans]
case w.h
C : Type u₁
D : Type u₂
inst✝¹ : Category C
inst✝ : Category 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
⊢ (adj₂.unit.app (R₁.obj x✝) ≫ R₂.map (f.app (R₁.obj x✝) ≫ adj₁.counit.app x✝)) ≫
      adj₃.unit.app (R₂.obj x✝) ≫ R₃.map (g.app (R₂.obj x✝) ≫ adj₂.counit.app x✝) =
    adj₃.unit.app (R₁.obj x✝) ≫ R₃.map ((g.app (R₁.obj x✝) ≫ f.app (R₁.obj x✝)) ≫ adj₁.counit.app x✝)
case w.h
C : Type u₁
D : Type u₂
inst✝¹ : Category C
inst✝ : Category 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✝) ≫
        (adj₂.unit.app (R₁.obj x✝) ≫
            R₂.map ((𝟙 (L₂.obj (R₁.obj x✝)) ≫ f.app (R₁.obj x✝) ≫ 𝟙 (L₁.obj (R₁.obj x✝))) ≫ adj₁.counit.app x✝)) ≫
          𝟙 (R₂.obj x✝)) ≫
      𝟙 (R₂.obj x✝) ≫
        (adj₃.unit.app (R₂.obj x✝) ≫
            R₃.map ((𝟙 (L₃.obj (R₂.obj x✝)) ≫ g.app (R₂.obj x✝) ≫ 𝟙 (L₂.obj (R₂.obj x✝))) ≫ adj₂.counit.app x✝)) ≫
          𝟙 (R₃.obj x✝) =
    𝟙 (R₁.obj x✝) ≫
      (adj₃.unit.app (R₁.obj x✝) ≫
          R₃.map
            ((𝟙 (L₃.obj (R₁.obj x✝)) ≫ (g.app (R₁.obj x✝) ≫ f.app (R₁.obj x✝)) ≫ 𝟙 (L₁.obj (R₁.obj x✝))) ≫
              adj₁.counit.app x✝)) ≫
        𝟙 (R₃.obj x✝)
simp only [id_comp, comp_id]
no goals
case w.h
C : Type u₁
D : Type u₂
inst✝¹ : Category C
inst✝ : Category 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
⊢ (adj₂.unit.app (R₁.obj x✝) ≫ R₂.map (f.app (R₁.obj x✝) ≫ adj₁.counit.app x✝)) ≫
      adj₃.unit.app (R₂.obj x✝) ≫ R₃.map (g.app (R₂.obj x✝) ≫ adj₂.counit.app x✝) =
    adj₃.unit.app (R₁.obj x✝) ≫ R₃.map ((g.app (R₁.obj x✝) ≫ f.app (R₁.obj x✝)) ≫ adj₁.counit.app x✝)
rw [← adj₃.unit_naturality_assoc, ← R₃.map_comp, g.naturality_assoc, L₂.map_comp, assoc,
  adj₂.counit_naturality, adj₂.left_triangle_components_assoc, assoc]