-- Module: Mathlib.CategoryTheory.Functor.Derived.Adjunction
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_4 : L₁.IsLocalization W₁
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst_6 : G'.IsLeftDerivedFunctor α W₁
inst_7 : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₂ : C₂
eq₁ : β.app X₂ ≫ η.app (F'.obj (L₂.obj X₂)) = η.app (L₁.obj (F.obj X₂)) ≫ F'.map (G'.map (β.app X₂))
eq₃ : L₁.map (F.map (adj.counit.app X₂)) ≫ β.app X₂ = β.app (G.obj (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂))
eq₂ :
  F'.map (G'.map (β.app X₂)) ≫ F'.map (ε.app (L₂.obj X₂)) =
    F'.map (α.app (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂))
hγ :
  β.app X₂ ≫
      𝟙 (F'.obj (L₂.obj X₂)) ≫
        η.app (F'.obj (L₂.obj X₂)) ≫ 𝟙 (F'.obj (G'.obj (F'.obj (L₂.obj X₂)))) ≫ F'.map (ε.app (L₂.obj X₂)) =
    β.app X₂ ≫ 𝟙 (F'.obj (L₂.obj X₂))
hγ₁ :
  β.app X₂ ≫
      𝟙 (F'.obj (L₂.obj X₂)) ≫
        η.app (F'.obj (L₂.obj X₂)) ≫ 𝟙 (F'.obj (G'.obj (F'.obj (L₂.obj X₂)))) ≫ F'.map (ε.app (L₂.obj X₂)) =
    β.app X₂
hγ₂ :
  β.app X₂ ≫ η.app (F'.obj (L₂.obj X₂)) ≫ 𝟙 (F'.obj (G'.obj (F'.obj (L₂.obj X₂)))) ≫ F'.map (ε.app (L₂.obj X₂)) =
    β.app X₂
hγ₃ : β.app X₂ ≫ η.app (F'.obj (L₂.obj X₂)) ≫ F'.map (ε.app (L₂.obj X₂)) = β.app X₂
hγ₄ : η.app (L₁.obj (F.obj X₂)) ≫ F'.map (G'.map (β.app X₂)) ≫ F'.map (ε.app (L₂.obj X₂)) = β.app X₂
hγ₅ : η.app (L₁.obj (F.obj X₂)) ≫ F'.map (α.app (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂)) = β.app X₂
hγ₆ : L₁.map (adj.unit.app (F.obj X₂)) ≫ β.app (G.obj (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂)) = β.app X₂
hγ₇ : L₁.map (adj.unit.app (F.obj X₂)) ≫ L₁.map (F.map (adj.counit.app X₂)) ≫ β.app X₂ = β.app X₂
hγ₈ : L₁.map (adj.unit.app (F.obj X₂) ≫ F.map (adj.counit.app X₂)) ≫ β.app X₂ = β.app X₂
hγ₉ : L₁.map (𝟙 (F.obj X₂)) ≫ β.app X₂ = β.app X₂
hγ₁₀ : 𝟙 (L₁.obj (F.obj X₂)) ≫ β.app X₂ = β.app X₂
hγ₁₁ hγ₁₂ : β.app X₂ = β.app X₂
⊢ β.app X₂ ≫
      𝟙 (F'.obj (L₂.obj X₂)) ≫
        η.app (F'.obj (L₂.obj X₂)) ≫
          𝟙 (F'.obj (G'.obj (F'.obj (L₂.obj X₂)))) ≫ F'.map (ε.app (L₂.obj X₂)) ≫ 𝟙 (F'.obj (L₂.obj X₂)) =
    β.app X₂ ≫ 𝟙 (F'.obj (L₂.obj X₂))

Tactic:
rw [Category.comp_id, Category.comp_id, Category.id_comp, Category.id_comp,
      reassoc_of% eq₁, eq₂, reassoc_of% (hη (F.obj X₂)), ← eq₃, ← L₁.map_comp_assoc,
      adj.right_triangle_components, Functor.map_id, Category.id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Adjunction.right_triangle_components, CategoryTheory.Functor.obj, CategoryTheory.Category.id_comp