-- Lean 4 proof step from Mathlib.CategoryTheory.Presentable.OrthogonalReflection (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasPushouts.{v, u} C
inst_2 : ∀ (Z : C), HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_3 : ∀ (Z : C), HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_4 : ∀ (Z : C), HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
κ : Cardinal.{w}
inst_5 : OrderBot κ.ord.ToType
inst_6 : HasIterationOfShape.{w, v, u} κ.ord.ToType C
inst_7 : Fact κ.IsRegular
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
H : MorphismProperty.TransfiniteCompositionOfShape.{w, v, u} W.isLocal.isLocal κ.ord.ToType (Y := reflectionObj W Z κ)
  (reflection W Z κ) :=
  transfiniteCompositionOfShapeReflection W Z κ
X Y : C
f : X ⟶ Y
hf : W f
left : IsCardinalPresentable.{w, v, u} X κ
right : IsCardinalPresentable.{w, v, u} Y κ
j : κ.ord.ToType
g₁ g₂ : Y ⟶ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj j
h :
  f ≫ g₁ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j =
    f ≫ g₂ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j
k : κ.ord.ToType
u : j ⟶ k
hk :
  (f ≫ g₁) ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map u =
    (f ≫ g₂) ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map u
hg :
  Eq (α := Y ⟶ (iteration W Z κ).obj (Order.succ k))
    (g₁ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map u ≫ (iteration W Z κ).map (homOfLE ⋯))
    (g₂ ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map u ≫ (iteration W Z κ).map (homOfLE ⋯))
this :
  CategoryStruct.comp (Y := H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj (Order.succ k))
      (H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map (u ≫ homOfLE ⋯))
      (H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app (Order.succ k)) =
    H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j
⊢ Eq (α := Y ⟶ reflectionObj W Z κ)
    (g₁ ≫
        H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map u ≫
          CategoryStruct.comp (Y := H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj (Order.succ k))
            (H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map (homOfLE ⋯))
            (H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app (Order.succ k)) :
      Y ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const κ.ord.ToType) (reflectionObj W Z κ)) j)
    (g₂ ≫
        H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map u ≫
          CategoryStruct.comp (Y := H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj (Order.succ k))
            (H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map (homOfLE ⋯))
            (H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app (Order.succ k)) :
      Y ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const κ.ord.ToType) (reflectionObj W Z κ)) j)
have refine_1 : Eq (α := Y ⟶ reflectionObj W Z κ)
  (g₂ ≫
      H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map u ≫
        CategoryStruct.comp (Y := (iteration W Z κ).obj (Order.succ k)) ((iteration W Z κ).map (homOfLE sorry))
          (H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app (Order.succ k)) :
    Y ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const κ.ord.ToType) (reflectionObj W Z κ)) j)
  (g₂ ≫
      H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map u ≫
        CategoryStruct.comp (Y := H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj (Order.succ k))
          (H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.map (homOfLE sorry))
          (H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app (Order.succ k)) :
    Y ⟶ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const κ.ord.ToType) (reflectionObj W Z κ)) j)
Tactic: rw [reassoc_of% hg]