-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
Goal:
C : Type u₁
D : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} H
F' : Functor.{v₂, v₃, u₂, u₃} D H
F : Functor.{v₁, v₃, u₁, u₃} C H
L : Functor.{v₁, v₂, u₁, u₂} C D
α : L ⋙ F' ⟶ F
W : MorphismProperty.{v₁, u₁} C
G : Functor.{v₂, v₃, u₂, u₃} D H
e : F ≅ L ⋙ G
inst_3 : L.IsLocalization W
Y : C
s : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
j : StructuredArrow (L.obj Y) L
X₁ X₂ : C
w : X₁ ⟶ X₂
hw : W w
φ : L.obj Y ⟶ L.obj X₂
hφ :
  CategoryStruct.comp (Y := Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y)))
      (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y :
        s.pt ⟶ Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y)))
      (NatTrans.app (Cone.π ((RightExtension.mk G e.inv).coneAt (L.obj Y))) (StructuredArrow.mk φ) :
        obj
            (obj (const (StructuredArrow (L.obj Y) L))
              (Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y))))
            (StructuredArrow.mk φ) ⟶
          (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk φ)) =
    s.π.app (StructuredArrow.mk φ)
this : IsIso (F.map w)
eq :
  Eq (α :=
    obj (obj (const (StructuredArrow (L.obj Y) L)) s.pt)
        (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv)) ⟶
      (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk φ))
    (map (obj (const (StructuredArrow (L.obj Y) L)) s.pt) (StructuredArrow.homMk w ⋯) ≫ s.π.app (StructuredArrow.mk φ))
    (s.π.app (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv)) ≫
      (StructuredArrow.proj (L.obj Y) L ⋙ F).map (StructuredArrow.homMk w ⋯))
refine_2 :
  Eq (α := s.pt ⟶ F.obj X₁)
    ((s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫
        G.map (φ ≫ (Localization.isoOfHom L W w hw).inv) ≫ e.inv.app X₁ :
      s.pt ⟶ F.obj X₁)
    (s.π.app (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv)) :
      obj (obj (const (StructuredArrow (L.obj Y) L)) s.pt)
          (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv)) ⟶
        (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv)))
⊢ CategoryStruct.comp (Y := Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y)))
      (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y :
        s.pt ⟶ Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y)))
      (NatTrans.app (Cone.π ((RightExtension.mk G e.inv).coneAt (L.obj Y)))
          (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv)) :
        obj
            (obj (const (StructuredArrow (L.obj Y) L))
              (Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y))))
            (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv)) ⟶
          (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv))) =
    s.π.app (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv))

Tactic:
dsimp at eq hφ ⊢