-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.EqualizerSheafCondition (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
B : C
I : Type t
inst_1 : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst_2 : (Presieve.ofArrows X π).HasPairwisePullbacks
⊢ (∀ (x : (i : I) → P.obj (op (X i))),
      Arrows.Compatible P π x →
        ∃! t : P.obj (op B),
          ∀ (i : I),
            (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) : (a : P.obj (op B)) → P.obj (op (X i))) t =
              x i) ↔
    ∀ (y : ∏ᶜ fun (i : I) ↦ P.obj (op (X i))),
      Eq (α := SecondObj P X π)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P X π) :
                (a : ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) → SecondObj P X π)
              y :
            SecondObj P X π)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P X π) :
                (a : ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) → SecondObj P X π)
              y :
            SecondObj P X π) →
        ∃! x : P.obj (op B),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P X π) :
                (a : P.obj (op B)) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
              x =
            y
have rw : (∀ (x : (i : I) → P.obj (op (X i))),
    Arrows.Compatible P π x →
      ∃! t : P.obj (op B),
        ∀ (i : I),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (π i).op) : (a : P.obj (op B)) → P.obj (op (X i))) t = x i) ↔
  ∀ (a : (j : I) → P.obj (op (X j))),
    Eq (α := SecondObj P X π)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P X π) :
              (a : ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) → SecondObj P X π)
            (((Equiv.trans (β := Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
                      (equivShrink ((j : I) → P.obj (op (X j))) :
                        ((j : I) → P.obj (op (X j))) ≃ Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
                      (Equiv.symm (Iso.toEquiv (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i)))) :
                        Shrink.{w, max w t} ((j : I) → P.obj (op (X j))) ≃ ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
                    ((j : I) → P.obj (op (X j))) ≃ ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
                  (a : (j : I) → P.obj (op (X j))) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
                a :
              ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
          SecondObj P X π)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P X π) :
              (a : ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) → SecondObj P X π)
            (((Equiv.trans (β := Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
                      (equivShrink ((j : I) → P.obj (op (X j))) :
                        ((j : I) → P.obj (op (X j))) ≃ Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
                      (Equiv.symm (Iso.toEquiv (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i)))) :
                        Shrink.{w, max w t} ((j : I) → P.obj (op (X j))) ≃ ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
                    ((j : I) → P.obj (op (X j))) ≃ ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
                  (a : (j : I) → P.obj (op (X j))) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
                a :
              ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
          SecondObj P X π) →
      ∃! x : P.obj (op B),
        Eq (α := ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (forkMap P X π) :
                (a : P.obj (op B)) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
              x :
            ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
          (((Equiv.trans (β := Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
                    (equivShrink ((j : I) → P.obj (op (X j))) :
                      ((j : I) → P.obj (op (X j))) ≃ Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
                    (Equiv.symm (Iso.toEquiv (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i)))) :
                      Shrink.{w, max w t} ((j : I) → P.obj (op (X j))) ≃ ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
                  ((j : I) → P.obj (op (X j))) ≃ ∏ᶜ fun (i : I) ↦ P.obj (op (X i))) :
                (a : (j : I) → P.obj (op (X j))) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
              a :
            ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
Tactic: rw [← Equiv.forall_congr_right ((equivShrink _).trans (Types.Small.productIso _).toEquiv.symm)]