-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck (goal)
Goal:
C : Type u_4
inst : Category.{u_3, u_4} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
F : Functor.{u_3, v_1, u_4, u_1} C D
P : Functor.{v_1, u_2, u_1, u_2 + 1} Dᵒᵖ (Type u_2)
X : C
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst_2 : (ofArrows Y f).HasPairwisePullbacks
inst_3 : F.PreservesPairwisePullbacks (ofArrows Y f)
this :
  HasPairwisePullbacks.{v_1, u_1} (C := D) (X := F.obj X)
    (ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i))
x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))
⊢ ((∀ (i j : ι),
        Eq (α := P.obj (Opposite.op (F.obj (pullback (f i) (f j)))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (F.map (pullback.fst (f i) (f j))))) :
                (a : P.obj (Opposite.op (F.obj (Y i)))) → P.obj (Opposite.op (F.obj (pullback (f i) (f j)))))
              (x i) :
            P.obj (Opposite.op (F.obj (pullback (f i) (f j)))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (F.map (pullback.snd (f i) (f j))))) :
                (a : P.obj (Opposite.op (F.obj (Y j)))) → P.obj (Opposite.op (F.obj (pullback (f i) (f j)))))
              (x j) :
            P.obj (Opposite.op (F.obj (pullback (f i) (f j)))))) →
      ∃! t : P.obj (Opposite.op (F.obj X)),
        ∀ (i : ι),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (F.map (f i)).op) :
                (a : P.obj (Opposite.op (F.obj X))) → P.obj (Opposite.op (F.obj (Y i))))
              t =
            x i) ↔
    (∀ (i j : ι),
        Eq (α := P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (P.map (Quiver.Hom.op (pullback.fst (F.map (f i)) (F.map (f j))))) :
                (a : P.obj (Opposite.op (F.obj (Y i)))) → P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))
              (x i) :
            P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (P.map (Quiver.Hom.op (pullback.snd (F.map (f i)) (F.map (f j))))) :
                (a : P.obj (Opposite.op (F.obj (Y j)))) → P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))
              (x j) :
            P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))) →
      ∃! t : P.obj (Opposite.op (F.obj X)),
        ∀ (i : ι),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (F.map (f i)).op) :
                (a : P.obj (Opposite.op (F.obj X))) → P.obj (Opposite.op (F.obj (Y i))))
              t =
            x i
have a : ∀ (a b : ι),
  Eq (α := P.obj (Opposite.op (F.obj (pullback (f a) (f b)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (F.map (pullback.fst (f a) (f b))))) :
            (a_1 : P.obj (Opposite.op (F.obj (Y a)))) → P.obj (Opposite.op (F.obj (pullback (f a) (f b)))))
          (x a) :
        P.obj (Opposite.op (F.obj (pullback (f a) (f b)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (F.map (pullback.snd (f a) (f b))))) :
            (a_1 : P.obj (Opposite.op (F.obj (Y b)))) → P.obj (Opposite.op (F.obj (pullback (f a) (f b)))))
          (x b) :
        P.obj (Opposite.op (F.obj (pullback (f a) (f b))))) ↔
    Eq (α := P.obj (Opposite.op (pullback (F.map (f a)) (F.map (f b)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.fst (F.map (f a)) (F.map (f b))))) :
            (a_1 : P.obj (Opposite.op (F.obj (Y a)))) → P.obj (Opposite.op (pullback (F.map (f a)) (F.map (f b)))))
          (x a) :
        P.obj (Opposite.op (pullback (F.map (f a)) (F.map (f b)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.snd (F.map (f a)) (F.map (f b))))) :
            (a_1 : P.obj (Opposite.op (F.obj (Y b)))) → P.obj (Opposite.op (pullback (F.map (f a)) (F.map (f b)))))
          (x b) :
        P.obj (Opposite.op (pullback (F.map (f a)) (F.map (f b)))))
Tactic: rw [forall₂_congr]