-- Module: Mathlib.CategoryTheory.Subobject.Lattice
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasWidePullbacks.{w, v₁, u₁} C
A : C
s : Set (Subobject.{v₁, u₁} A)
f : Subobject.{v₁, u₁} A
hf : f ∈ s
w :
  Eq (α := widePullback.{w, v₁, u₁} s ⟶ A)
    (CategoryStruct.comp (Y :=
        Functor.obj.{w, v₁, w, u₁} (C :=
          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)
          (some
              (Subtype.mk (p := fun (x : Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)) ↦
                Membership.mem (γ := Set (Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)))
                  ((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                    s)
                  x)
                ((equivShrink (Subobject.{v₁, u₁} A) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) f) ⋯) :
            Option
              (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                    s) :
                Type w)))
        (limit.π (wideCospan s)
            (some
              (Subtype.mk (p := fun (x : Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)) ↦
                Membership.mem (γ := Set (Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)))
                  ((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                    s)
                  x)
                ((equivShrink (Subobject.{v₁, u₁} A) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) f) ⋯)) :
          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.{w, v₁, w, u₁} (C :=
              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)
              (some
                  (Subtype.mk (p := fun (x : Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)) ↦
                    Membership.mem (γ := Set (Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)))
                      ((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                          (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                        s)
                      x)
                    ((equivShrink (Subobject.{v₁, u₁} A) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) f)
                    ⋯) :
                Option
                  (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                          (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                        s) :
                    Type w)))
        (eqToHom ⋯ ≫ f.arrow :
          Functor.obj.{w, v₁, w, u₁} (C :=
              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)
              (some
                  (Subtype.mk (p := fun (x : Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)) ↦
                    Membership.mem (γ := Set (Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)))
                      ((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                          (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                        s)
                      x)
                    ((equivShrink (Subobject.{v₁, u₁} A) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) f)
                    ⋯) :
                Option
                  (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                          (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                        s) :
                    Type w)) ⟶
            A) :
      widePullback.{w, v₁, u₁} s ⟶ A)
    (widePullbackι s : widePullback.{w, v₁, u₁} s ⟶ A)
⊢ (Iso.hom (underlyingIso (widePullbackι s)) ≫
        CategoryStruct.comp (Y :=
          Functor.obj.{w, v₁, w, u₁} (C :=
            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)
            (some
                (Subtype.mk (p := fun (x : Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)) ↦
                  Membership.mem (γ := Set (Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)))
                    ((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                        (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                      s)
                    x)
                  ((equivShrink (Subobject.{v₁, u₁} A) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) f)
                  ⋯) :
              Option
                (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                      s) :
                  Type w)))
          (limit.π (wideCospan s)
              (some
                (Subtype.mk (p := fun (x : Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)) ↦
                  Membership.mem (γ := Set (Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)))
                    ((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                        (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                      s)
                    x)
                  ((equivShrink (Subobject.{v₁, u₁} A) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) f)
                  ⋯)) :
            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.{w, v₁, w, u₁} (C :=
                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)
                (some
                    (Subtype.mk (p := fun (x : Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)) ↦
                      Membership.mem (γ := Set (Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)))
                        ((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                            (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                          s)
                        x)
                      ((equivShrink (Subobject.{v₁, u₁} A) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) f)
                      ⋯) :
                  Option
                    (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                            (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                          s) :
                      Type w)))
          (eqToHom ⋯ :
            Functor.obj.{w, v₁, w, u₁} (C :=
                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)
                (some
                    (Subtype.mk (p := fun (x : Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)) ↦
                      Membership.mem (γ := Set (Shrink.{w, max u₁ v₁} (Subobject.{v₁, u₁} A)))
                        ((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                            (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                          s)
                        x)
                      ((equivShrink (Subobject.{v₁, u₁} A) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) f)
                      ⋯) :
                  Option
                    (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) :
                            (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                          s) :
                      Type w)) ⟶
              Functor.obj underlying f)) ≫
      f.arrow =
    (mk (A := widePullback.{w, v₁, u₁} s) (widePullbackι s)).arrow

Tactic:
simp only [Category.assoc, ← underlyingIso_hom_comp_eq_mk,
      Iso.cancel_iso_hom_left]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.cancel_iso_hom_left, CategoryTheory.Subobject.underlyingIso_hom_comp_eq_mk