-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Lattice (goal)
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
j :
  WidePullbackShape
    (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) : Type w)
none :
  Eq (α :=
    Z_1 ⟶
      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)
        (Option.none :
          Option
            (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) :
              Type w)))
    (u ≫ limit.π (wideCospan s) Option.none :
      Z_1 ⟶
        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)
          (Option.none :
            Option
              (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                    s) :
                Type w)))
    (v ≫ limit.π (wideCospan s) Option.none :
      Z_1 ⟶
        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)
          (Option.none :
            Option
              (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                    s) :
                Type w)))
⊢ Eq (α :=
    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)
        j)
    (u ≫ limit.π (wideCospan s) j :
      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)
          j)
    (v ≫ limit.π (wideCospan s) j :
      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)
          j)
have some : ∀
  (val :
    (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) '' s) :
      Type w)),
  Eq (α :=
    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)
        (some val))
    (u ≫ limit.π (wideCospan s) (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)
          (some val))
    (v ≫ limit.π (wideCospan s) (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)
          (some val))
Tactic: cases j
Cleared hypotheses: j