-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
Φ : LocalizerMorphism W₁ W₂
inst_2 : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution (W₁ := W₁) (W₂ := W₂) X₂)
inst_3 : Φ.arrow (W₁ := W₁) (W₂ := W₂).HasRightResolutions (W₁ := W₁.arrow) (W₂ := W₂.arrow)
inst_4 : W₂.ContainsIdentities
D : Type u_3
inst_5 : Category.{v_3, u_3} D
L : Functor.{v_2, v_3, u_2, u_3} C₂ D
inst_6 : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
w : TwoSquare (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D) :=
  TwoSquare.mk (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D)
    (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L).rightUnitor.inv
this_1 : Nonempty (w.CostructuredArrowDownwards y)
c : C₁
g : X₂ ⟶ Φ.functor (W₁ := W₁) (W₂ := W₂).obj c
x : L.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c) ⟶ X₃
fac_1 : L.map g ≫ 𝟙 (L.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c)) ≫ x = y
fac : L.map g ≫ x = y
ρ : Φ.arrow (W₁ := W₁) (W₂ := W₂).RightResolution (W₁ := W₁.arrow) (W₂ := W₂.arrow) (Arrow.mk g) :=
  Classical.arbitrary (Φ.arrow (W₁ := W₁) (W₂ := W₂).RightResolution (W₁ := W₁.arrow) (W₂ := W₂.arrow) (Arrow.mk g))
this :
  Zigzag
    ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (𝟙 (Φ.functor (W₁ := W₁) (W₂ := W₂).obj c)) ⋯))
    ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.right (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow))) ⋯))
⊢ ((TwoSquare.mk (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D)
                (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L).rightUnitor.inv).structuredArrowDownwards
            X₂).map
        (StructuredArrow.homMk ρ.X₁ (W₁ := W₁.arrow) (W₂ := W₂.arrow).hom ⋯) ≫
      CostructuredArrow.hom
        ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
          (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.right (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow))) ⋯)) =
    CostructuredArrow.hom
      ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L y).obj
        (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.left (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow))) ⋯))
have refine_2 : StructuredArrow.Hom.right
    (((TwoSquare.mk (Φ.functor (W₁ := W₁) (W₂ := W₂)) (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L) L (𝟭 D)
                (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L).rightUnitor.inv).structuredArrowDownwards
            X₂).map
        (StructuredArrow.homMk ρ.X₁ (W₁ := W₁.arrow) (W₂ := W₂.arrow).hom sorry) ≫
      CostructuredArrow.hom
        ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
          (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.right (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow))) sorry))) =
  StructuredArrow.Hom.right
    (CostructuredArrow.hom
      ((fromRightResolution (W₁ := W₁) (W₂ := W₂) Φ L y).obj
        (RightResolution.mk (W₁ := W₁) (W₂ := W₂) (Arrow.Hom.left (ρ.w (W₁ := W₁.arrow) (W₂ := W₂.arrow))) sorry)))
Tactic: ext