-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived (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
α : F ⟶ L ⋙ 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 : Cocone (J := CostructuredArrow L (L.obj Y)) (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
refine_1 :
  ∀ (X₁ X₂ : C) (f : X₁ ⟶ X₂) (φ : L.obj X₂ ⟶ L.obj Y)
    (hφ :
      CategoryStruct.comp (Y :=
          obj
            (obj (const (CostructuredArrow L (L.obj Y)))
              (Cocone.pt (J := CostructuredArrow L (L.obj Y)) ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))))
            (CostructuredArrow.mk φ))
          (NatTrans.app (Cocone.ι ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))) (CostructuredArrow.mk φ))
          (e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))) =
        s.ι.app (CostructuredArrow.mk φ)),
    CategoryStruct.comp (Y :=
        obj
          (obj (const (CostructuredArrow L (L.obj Y)))
            (Cocone.pt (J := CostructuredArrow L (L.obj Y)) ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))))
          (CostructuredArrow.mk (L.map f ≫ φ)))
        (NatTrans.app (Cocone.ι ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))) (CostructuredArrow.mk (L.map f ≫ φ)))
        (e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))) =
      s.ι.app (CostructuredArrow.mk (L.map f ≫ φ))
⊢ CategoryStruct.comp (Y :=
      obj
        (obj (const (CostructuredArrow L (L.obj Y)))
          (Cocone.pt (J := CostructuredArrow L (L.obj Y)) ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))))
        j)
      (NatTrans.app (Cocone.ι ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))) j)
      (e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))) =
    s.ι.app j
have refine_2 : ∀ (X₁ X₂ : C) (w : X₁ ⟶ X₂) (hw : W w) (φ : L.obj X₁ ⟶ L.obj Y)
  (hφ :
    CategoryStruct.comp (Y :=
        obj
          (obj (const (CostructuredArrow L (L.obj Y)))
            (Cocone.pt (J := CostructuredArrow L (L.obj Y)) ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))))
          (CostructuredArrow.mk φ))
        (NatTrans.app (Cocone.ι ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))) (CostructuredArrow.mk φ))
        (e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))) =
      s.ι.app (CostructuredArrow.mk φ)),
  CategoryStruct.comp (Y :=
      obj
        (obj (const (CostructuredArrow L (L.obj Y)))
          (Cocone.pt (J := CostructuredArrow L (L.obj Y)) ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))))
        (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ)))
      (NatTrans.app (Cocone.ι ((LeftExtension.mk G e.hom).coconeAt (L.obj Y)))
        (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ)))
      (e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))) =
    s.ι.app (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ))
Tactic: refine Localization.induction_costructuredArrow L W _ (by simp)
      (fun X₁ X₂ f φ hφ ↦ ?_) (fun X₁ X₂ w hw φ hφ ↦ ?_) j