-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : LocallySmall.{w, v₁, u₁} C
inst_3 : WellPowered.{w, v₁, u₁} C
inst_4 : HasWidePullbacks.{w, v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
Z_1 : C
u v : Z_1 ⟶ widePullback.{w, v₁, u₁} s
h : u ≫ widePullbackι s = v ≫ widePullbackι s
val :
  (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) : Type w)
some :
  Eq (α := Z_1 ⟶ A)
    (u ≫
      CategoryStruct.comp (Y :=
        Functor.obj (C := Subobject.{v₁, u₁} A) underlying
          ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) : (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
            (↑val : Shrink.{w, max u₁ v₁} (Subobject A))))
        (limit.π (wideCospan s) (Option.some val) :
          limit.{w, w, v₁, u₁} (J :=
              WidePullbackShape
                (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                      s) :
                  Type w))
              (wideCospan s :
                Functor.{w, v₁, w, u₁}
                  (WidePullbackShape
                    (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                            (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                          s) :
                      Type w))
                  C) ⟶
            Functor.obj
              (wideCospan s :
                Functor.{w, v₁, w, u₁}
                  (WidePullbackShape
                    (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                            (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                          s) :
                      Type w))
                  C)
              (Option.some val))
        (arrow
            ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) : (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
              (↑val : Shrink.{w, max u₁ v₁} (Subobject A))) :
          Functor.obj (C := Subobject.{v₁, u₁} A) underlying
              ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                  (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                (↑val : Shrink.{w, max u₁ v₁} (Subobject A))) ⟶
            A))
    (v ≫
      CategoryStruct.comp (Y :=
        Functor.obj (C := Subobject.{v₁, u₁} A) underlying
          ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) : (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
            (↑val : Shrink.{w, max u₁ v₁} (Subobject A))))
        (limit.π (wideCospan s) (Option.some val) :
          limit.{w, w, v₁, u₁} (J :=
              WidePullbackShape
                (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                      s) :
                  Type w))
              (wideCospan s :
                Functor.{w, v₁, w, u₁}
                  (WidePullbackShape
                    (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                            (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                          s) :
                      Type w))
                  C) ⟶
            Functor.obj
              (wideCospan s :
                Functor.{w, v₁, w, u₁}
                  (WidePullbackShape
                    (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                            (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                          s) :
                      Type w))
                  C)
              (Option.some val))
        (arrow
            ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) : (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
              (↑val : Shrink.{w, max u₁ v₁} (Subobject A))) :
          Functor.obj (C := Subobject.{v₁, u₁} A) underlying
              ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) :
                  (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
                (↑val : Shrink.{w, max u₁ v₁} (Subobject A))) ⟶
            A))
⊢ Eq (α := Z_1 ⟶ A)
    (CategoryStruct.comp (Y :=
      Functor.obj (C := Subobject.{v₁, u₁} A) underlying
        ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) : (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
          (↑val : Shrink.{w, max u₁ v₁} (Subobject A))))
      (u ≫ limit.π (wideCospan s) (Option.some val) :
        Z_1 ⟶
          Functor.obj
            (wideCospan s :
              Functor.{w, v₁, w, u₁}
                (WidePullbackShape
                  (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                          (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                        s) :
                    Type w))
                C)
            (Option.some val))
      (arrow
          ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) : (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
            (↑val : Shrink.{w, max u₁ v₁} (Subobject A))) :
        Functor.obj (C := Subobject.{v₁, u₁} A) underlying
            ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) : (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
              (↑val : Shrink.{w, max u₁ v₁} (Subobject A))) ⟶
          A))
    (CategoryStruct.comp (Y :=
      Functor.obj (C := Subobject.{v₁, u₁} A) underlying
        ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) : (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
          (↑val : Shrink.{w, max u₁ v₁} (Subobject A))))
      (v ≫ limit.π (wideCospan s) (Option.some val) :
        Z_1 ⟶
          Functor.obj
            (wideCospan s :
              Functor.{w, v₁, w, u₁}
                (WidePullbackShape
                  (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                          (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                        s) :
                    Type w))
                C)
            (Option.some val))
      (arrow
          ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) : (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
            (↑val : Shrink.{w, max u₁ v₁} (Subobject A))) :
        Functor.obj (C := Subobject.{v₁, u₁} A) underlying
            ((Equiv.symm (equivShrink (Subobject.{v₁, u₁} A)) : (a : Shrink.{w, max u₁ v₁} (Subobject A)) → Subobject A)
              (↑val : Shrink.{w, max u₁ v₁} (Subobject A))) ⟶
          A))

Tactic:
rw [assoc, assoc]

Premises used: CategoryTheory.Category.assoc