-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
Z : C
inst_1 : HasCoproduct (β := D₁ W Z) (D₁.obj₁ (W := W))
inst_2 : HasCoproduct (β := D₁ W Z) (D₁.obj₂ (W := W))
inst_3 : HasPushouts.{v, u} C
inst_4 : HasMulticoequalizer (J := D₂.multispanShape W Z) (D₂.multispanIndex W Z)
T : C
hT : W.isLocal T
g : Z ⟶ T
f : (d : D₁ W Z) → (↑(d.fst (β := fun (f : (↑W.toSet : Type (max u v))) ↦ (↑f : Arrow C).left ⟶ Z)) : Arrow C).right ⟶ T
hf :
  ∀ (d : D₁ W Z),
    (fun (g : (↑(d.fst (β := fun (f : (↑W.toSet : Type (max u v))) ↦ (↑f : Arrow C).left ⟶ Z)) : Arrow C).right ⟶ T) ↦
          (↑(d.fst (β := fun (f : (↑W.toSet : Type (max u v))) ↦ (↑f : Arrow C).left ⟶ Z)) : Arrow C).hom ≫ g)
        (f d) =
      d.snd (β := fun (f : (↑W.toSet : Type (max u v))) ↦ (↑f : Arrow C).left ⟶ Z) ≫ g
d : (D₂.multispanShape W Z).L
⊢ Eq.{v + 1} (α :=
    (↑(d.fst (β := fun (f : (↑W.toSet : Type (max u v))) ↦
              { pq : ((↑f : Arrow C).right ⟶ step W Z) × ((↑f : Arrow C).right ⟶ step W Z) //
                (↑f : Arrow C).hom ≫ pq.1 = (↑f : Arrow C).hom ≫ pq.2 })) :
          Arrow C).left ⟶
      T)
    ((fun
          (g :
            (↑(d.fst (β := fun (f : (↑W.toSet : Type (max u v))) ↦
                      { pq : ((↑f : Arrow C).right ⟶ step W Z) × ((↑f : Arrow C).right ⟶ step W Z) //
                        (↑f : Arrow C).hom ≫ pq.1 = (↑f : Arrow C).hom ≫ pq.2 })) :
                  Arrow C).right ⟶
              T) ↦
        (↑(d.fst (β := fun (f : (↑W.toSet : Type (max u v))) ↦
                  { pq : ((↑f : Arrow C).right ⟶ step W Z) × ((↑f : Arrow C).right ⟶ step W Z) //
                    (↑f : Arrow C).hom ≫ pq.1 = (↑f : Arrow C).hom ≫ pq.2 })) :
              Arrow C).hom ≫
          g)
      (MultispanIndex.fst (D₂.multispanIndex W Z) d ≫
        (fun (x : (D₂.multispanShape W Z).R) ↦
            (match (motive := (x : (D₂.multispanShape W Z).R) → MultispanIndex.right (D₂.multispanIndex W Z) x ⟶ T)
                x with
              | PUnit.unit => pushout.desc (Sigma.desc f) g ⋯ :
              MultispanIndex.right (D₂.multispanIndex W Z) x ⟶ T))
          ((D₂.multispanShape W Z).fst d)))
    ((fun
          (g :
            (↑(d.fst (β := fun (f : (↑W.toSet : Type (max u v))) ↦
                      { pq : ((↑f : Arrow C).right ⟶ step W Z) × ((↑f : Arrow C).right ⟶ step W Z) //
                        (↑f : Arrow C).hom ≫ pq.1 = (↑f : Arrow C).hom ≫ pq.2 })) :
                  Arrow C).right ⟶
              T) ↦
        (↑(d.fst (β := fun (f : (↑W.toSet : Type (max u v))) ↦
                  { pq : ((↑f : Arrow C).right ⟶ step W Z) × ((↑f : Arrow C).right ⟶ step W Z) //
                    (↑f : Arrow C).hom ≫ pq.1 = (↑f : Arrow C).hom ≫ pq.2 })) :
              Arrow C).hom ≫
          g)
      (MultispanIndex.snd (D₂.multispanIndex W Z) d ≫
        (fun (x : (D₂.multispanShape W Z).R) ↦
            (match (motive := (x : (D₂.multispanShape W Z).R) → MultispanIndex.right (D₂.multispanIndex W Z) x ⟶ T)
                x with
              | PUnit.unit => pushout.desc (Sigma.desc f) g ⋯ :
              MultispanIndex.right (D₂.multispanIndex W Z) x ⟶ T))
          ((D₂.multispanShape W Z).snd d)))

Tactic:
simp [reassoc_of% d.2.2]

Premises used: Sigma.snd, Subtype.property