-- 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
k : ∀ g ∈ s, f ≤ g
w :
  limit.lift (wideCospan s) (leInfCone s f k) ≫
      Iso.inv (underlyingIso (widePullbackι s)) ≫ (mk (A := widePullback.{w, v₁, u₁} s) (widePullbackι s)).arrow =
    f.arrow
w₁ :
  CategoryStruct.comp (Y :=
      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))
      (limit.lift (wideCospan s) (leInfCone s f k) :
        Cone.pt.{w, v₁, w, u₁} (J :=
            WidePullbackShape
              (↑((⇑(equivShrink (Subobject.{v₁, u₁} A)) : (a : Subobject A) → Shrink.{w, max u₁ v₁} (Subobject A)) ''
                    s) :
                Type w))
            (F :=
            (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))
            (leInfCone s f k) ⟶
          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))
      (widePullbackι s : widePullback.{w, v₁, u₁} s ⟶ A) =
    f.arrow
w₂ :
  CategoryStruct.comp (Y :=
      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))
      (limit.lift (wideCospan s) (leInfCone s f k)) (limit.π (wideCospan s) none) =
    f.arrow
w₃ : NatTrans.app (Cone.π (leInfCone s f k)) none = f.arrow
w₄ w₅ : f.arrow = f.arrow
⊢ (limit.lift (wideCospan s) (leInfCone s f k) ≫ Iso.inv (underlyingIso (widePullbackι s))) ≫
      (mk (A := widePullback.{w, v₁, u₁} s) (widePullbackι s)).arrow =
    f.arrow

Tactic:
rw [assoc, underlyingIso_arrow, widePullbackι, limit.lift_π, leInfCone_π_app_none]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Subobject.underlyingIso_arrow, CategoryTheory.Subobject.leInfCone_π_app_none, CategoryTheory.Subobject.widePullbackι, CategoryTheory.Limits.limit.lift_π