-- Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
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 : FirstObj P X
refine_1 :
  ∀
    (t :
      Arrows.PullbackCompatible P π
        ((Equiv.symm (equivShrink ((i : I) → P.obj (op (X i)))) :
            (a : Shrink.{w, max t w} ((i : I) → P.obj (op (X i)))) → (i : I) → P.obj (op (X i)))
          (((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (Iso.hom (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i)))) :
                  TypeCat.Fun (∏ᶜ fun (i : I) ↦ P.obj (op (X i))) (Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))) :
                (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (i : I) ↦ P.obj (op (X i)))) →
                  (fun (X : Type w) ↦ X) (Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))))
              x :
            (fun (X : Type w) ↦ X) (Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))))),
    Eq (α := (fun (X : Type w) ↦ X) (SecondObj P X π))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P X π) :
            (a : (fun (X : Type w) ↦ X) (FirstObj P X)) → (fun (X : Type w) ↦ X) (SecondObj P X π))
          x :
        (fun (X : Type w) ↦ X) (SecondObj P X π))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P X π) :
            (a : (fun (X : Type w) ↦ X) (FirstObj P X)) → (fun (X : Type w) ↦ X) (SecondObj P X π))
          x :
        (fun (X : Type w) ↦ X) (SecondObj P X π))
refine_2 :
  ∀
    (t :
      Eq (α := (fun (X : Type w) ↦ X) (SecondObj P X π))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P X π) :
              (a : (fun (X : Type w) ↦ X) (FirstObj P X)) → (fun (X : Type w) ↦ X) (SecondObj P X π))
            x :
          (fun (X : Type w) ↦ X) (SecondObj P X π))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P X π) :
              (a : (fun (X : Type w) ↦ X) (FirstObj P X)) → (fun (X : Type w) ↦ X) (SecondObj P X π))
            x :
          (fun (X : Type w) ↦ X) (SecondObj P X π)))
    (i j : I),
    Eq (α := (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π i) (π j)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.fst (π i) (π j)))) :
            (a : (fun (X : Type w) ↦ X) (P.obj (op (X i)))) →
              (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π i) (π j)))))
          ((Equiv.symm (equivShrink ((i : I) → P.obj (op (X i)))) :
                (a : Shrink.{w, max t w} ((i : I) → P.obj (op (X i)))) → (i : I) → P.obj (op (X i)))
              (((ConcreteCategory.hom (FC := TypeCat.Fun)
                        (Iso.hom (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i)))) :
                      TypeCat.Fun (∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
                        (Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))) :
                    (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (i : I) ↦ P.obj (op (X i)))) →
                      (fun (X : Type w) ↦ X) (Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))))
                  x :
                (fun (X : Type w) ↦ X) (Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))))
              i :
            P.obj (op (X i))) :
        (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π i) (π j)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.snd (π i) (π j)))) :
            (a : (fun (X : Type w) ↦ X) (P.obj (op (X j)))) →
              (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π i) (π j)))))
          ((Equiv.symm (equivShrink ((i : I) → P.obj (op (X i)))) :
                (a : Shrink.{w, max t w} ((i : I) → P.obj (op (X i)))) → (i : I) → P.obj (op (X i)))
              (((ConcreteCategory.hom (FC := TypeCat.Fun)
                        (Iso.hom (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i)))) :
                      TypeCat.Fun (∏ᶜ fun (i : I) ↦ P.obj (op (X i)))
                        (Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))) :
                    (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (i : I) ↦ P.obj (op (X i)))) →
                      (fun (X : Type w) ↦ X) (Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))))
                  x :
                (fun (X : Type w) ↦ X) (Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))))
              j :
            P.obj (op (X j))) :
        (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback (π i) (π j)))))
⊢ Arrows.PullbackCompatible P π
      ((Equiv.symm (equivShrink ((i : I) → P.obj (op (X i)))) :
          (a : Shrink.{w, max t w} ((i : I) → P.obj (op (X i)))) → (i : I) → P.obj (op (X i)))
        (((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (Types.Small.productIso fun (i : I) ↦ P.obj (op (X i)))) :
                TypeCat.Fun (∏ᶜ fun (i : I) ↦ P.obj (op (X i))) (Shrink.{w, max w t} ((j : I) → P.obj (op (X j))))) :
              (a : (fun (X : Type w) ↦ X) (∏ᶜ fun (i : I) ↦ P.obj (op (X i)))) →
                (fun (X : Type w) ↦ X) (Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))))
            x :
          (fun (X : Type w) ↦ X) (Shrink.{w, max w t} ((j : I) → P.obj (op (X j)))))) ↔
    Eq (α := (fun (X : Type w) ↦ X) (SecondObj P X π))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (firstMap P X π) :
            (a : (fun (X : Type w) ↦ X) (FirstObj P X)) → (fun (X : Type w) ↦ X) (SecondObj P X π))
          x :
        (fun (X : Type w) ↦ X) (SecondObj P X π))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (secondMap P X π) :
            (a : (fun (X : Type w) ↦ X) (FirstObj P X)) → (fun (X : Type w) ↦ X) (SecondObj P X π))
          x :
        (fun (X : Type w) ↦ X) (SecondObj P X π))

Tactic:
refine ⟨fun t ↦ ?_, fun t i j ↦ ?_⟩