-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived (goal)
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
refine_1 :
  ∀ (X₁ X₂ : C) (f : X₁ ⟶ X₂) (φ : 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 φ)),
    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 (φ ≫ L.map f)) :
          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 (φ ≫ L.map f)) ⟶
            (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk (φ ≫ L.map f))) =
      s.π.app (StructuredArrow.mk (φ ≫ L.map f))
⊢ 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))) j :
        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))))
            j ⟶
          (StructuredArrow.proj (L.obj Y) L ⋙ F).obj j) =
    s.π.app j
have refine_2 : ∀ (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 φ)),
  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: refine Localization.induction_structuredArrow L W _ (by simp)
      (fun X₁ X₂ f φ hφ ↦ ?_) (fun X₁ X₂ w hw φ hφ ↦ ?_) j