-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
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 κ
g₂ : Y ⟶ reflectionObj W Z κ
j₁ : κ.ord.ToType
g₁ : Y ⟶ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj j₁
h :
  Eq.{v + 1} (α := X ⟶ reflectionObj W Z κ)
    ((fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g)
      (g₁ ≫
        { pt := reflectionObj W Z κ, ι := H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl }.ι.app j₁))
    ((fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g) g₂)
obtain :
  ∀ (j₂ : κ.ord.ToType) (g₂ : Y ⟶ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj j₂)
    (h :
      Eq.{v + 1} (α := X ⟶ reflectionObj W Z κ)
        ((fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g)
          (g₁ ≫
            { pt := reflectionObj W Z κ, ι := H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl }.ι.app
              j₁))
        ((fun (g : Y ⟶ reflectionObj W Z κ) ↦ f ≫ g)
          (g₂ ≫
            { pt := reflectionObj W Z κ, ι := H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl }.ι.app
              j₂))),
    ∃ (j : κ.ord.ToType) (g₁' : Y ⟶ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj j) (g₂' :
      Y ⟶ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj j),
      g₁' ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j =
          g₁ ≫
            { pt := reflectionObj W Z κ, ι := H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl }.ι.app
              j₁ ∧
        g₂' ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j =
          g₂ ≫
            { pt := reflectionObj W Z κ, ι := H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl }.ι.app j₂
⊢ ∃ (j : κ.ord.ToType) (g₁' : Y ⟶ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj j) (g₂' :
    Y ⟶ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).F.obj j),
    g₁' ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j =
        g₁ ≫
          { pt := reflectionObj W Z κ, ι := H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl }.ι.app j₁ ∧
      g₂' ≫ H.toTransfiniteCompositionOfShape (W := W.isLocal.isLocal).incl.app j = g₂

Tactic:
obtain ⟨j₂, g₂, rfl⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ H.isColimit g₂

Premises used: CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape, CategoryTheory.IsCardinalPresentable.exists_hom_of_isColimit, CategoryTheory.TransfiniteCompositionOfShape.isColimit, rfl