-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear (goal)
Goal:
R : Type t
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Abelian.{v, u} C
inst_3 : Linear.{t, v, u} R C
inst_4 : HasExt.{w, v, u} C
X Y : C
n : ℕ
x : Ext.{w, v, u} X Y n
r : R
this : HasDerivedCategory C := HasDerivedCategory.standard C
h :
  HSMul.hSMul (β :=
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
        (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ))
      r
      ((homEquiv :
            (a : Ext X Y n) →
              ShiftedHom ((DerivedCategory.singleFunctor C 0).obj X) ((DerivedCategory.singleFunctor C 0).obj Y)
                (↑n : ℤ))
          x :
        ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
          (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ)) =
    ShiftedHom.comp x.hom (hom (mk₀ (HSMul.hSMul (β := Y ⟶ Y) r (𝟙 Y)))) ⋯
h₁ :
  HSMul.hSMul (β :=
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
        (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ))
      r
      ((homEquiv :
            (a : Ext X Y n) →
              ShiftedHom ((DerivedCategory.singleFunctor C 0).obj X) ((DerivedCategory.singleFunctor C 0).obj Y)
                (↑n : ℤ))
          x :
        ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
          (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ)) =
    ShiftedHom.comp x.hom
      (ShiftedHom.mk₀ (↑0 : ℤ) mk₀._proof_1
        (Functor.map (DerivedCategory.singleFunctor C 0) (HSMul.hSMul (β := Y ⟶ Y) r (𝟙 Y))))
      ⋯
h₂ :
  HSMul.hSMul (β :=
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
        (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ))
      r
      ((homEquiv :
            (a : Ext X Y n) →
              ShiftedHom ((DerivedCategory.singleFunctor C 0).obj X) ((DerivedCategory.singleFunctor C 0).obj Y)
                (↑n : ℤ))
          x :
        ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
          (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ)) =
    ShiftedHom.comp x.hom
      (ShiftedHom.mk₀ (↑0 : ℤ) mk₀._proof_1
        (HSMul.hSMul (β :=
          Quiver.Hom (V := DerivedCategory C) (Functor.obj (DerivedCategory.singleFunctor C 0) Y)
            (Functor.obj (DerivedCategory.singleFunctor C 0) Y))
          r (Functor.map (DerivedCategory.singleFunctor C 0) (𝟙 Y))))
      ⋯
h₃ :
  HSMul.hSMul (β :=
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
        (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ))
      r
      ((homEquiv :
            (a : Ext X Y n) →
              ShiftedHom ((DerivedCategory.singleFunctor C 0).obj X) ((DerivedCategory.singleFunctor C 0).obj Y)
                (↑n : ℤ))
          x :
        ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
          (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ)) =
    ShiftedHom.comp x.hom
      (ShiftedHom.mk₀ (↑0 : ℤ) mk₀._proof_1
        (HSMul.hSMul (β :=
          Quiver.Hom (V := DerivedCategory C) (Functor.obj (DerivedCategory.singleFunctor C 0) Y)
            (Functor.obj (DerivedCategory.singleFunctor C 0) Y))
          r (𝟙 (Functor.obj (DerivedCategory.singleFunctor C 0) Y))))
      ⋯
⊢ HSMul.hSMul (β :=
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
        (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ))
      r
      ((homEquiv :
            (a : Ext X Y n) →
              ShiftedHom ((DerivedCategory.singleFunctor C 0).obj X) ((DerivedCategory.singleFunctor C 0).obj Y)
                (↑n : ℤ))
          x :
        ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
          (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ)) =
    (x.comp (mk₀ (HSMul.hSMul (β := Y ⟶ Y) r (𝟙 Y))) ⋯).hom
have h₄ : HSMul.hSMul (β :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
      (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ))
    r
    ((homEquiv :
          (a : Ext X Y n) →
            ShiftedHom ((DerivedCategory.singleFunctor C 0).obj X) ((DerivedCategory.singleFunctor C 0).obj Y) (↑n : ℤ))
        x :
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) X)
        (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑n : ℤ)) =
  ShiftedHom.comp x.hom
    (HSMul.hSMul (β :=
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (DerivedCategory.singleFunctor C 0) Y)
        (Functor.obj (DerivedCategory.singleFunctor C 0) Y) (↑0 : ℤ))
      r (ShiftedHom.mk₀ (↑0 : ℤ) mk₀._proof_1 (𝟙 (Functor.obj (DerivedCategory.singleFunctor C 0) Y))))
    sorry
Tactic: rw [comp_hom, mk₀_hom, Functor.map_smul, Functor.map_id, ShiftedHom.mk₀_smul,
    ShiftedHom.comp_smul, ShiftedHom.comp_mk₀_id]