-- 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) ↔
    ∀ (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)))
have simp_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))),
    Arrows.Compatible P π a →
      ∃! 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.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))) :
                (a : Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) → ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
              ((equivShrink ((j : I) → P.obj (op (X j))) :
                    (a : (j : I) → P.obj (op (X j))) → Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))
                  a :
                Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))) :
            ∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
Tactic: simp_rw [← compatible_iff_of_small, ← Iso.toEquiv_apply, Equiv.trans_apply,
    Equiv.apply_symm_apply, Equiv.symm_apply_apply]