-- 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_1 :
  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 : ι
this_2 : PreservesLimit (cospan (f i) (f j)) F
this : HasPullback (F.map (f i)) (F.map (f 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))))) ↔
    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)))))
have a : Eq (α := P.obj (Opposite.op (F.obj (pullback (f i) (f j)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))
              (P.map (Quiver.Hom.op (pullback.fst (F.map (f i)) (F.map (f j)))))
              (P.map (Quiver.Hom.op (pullbackComparison F (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)
            (CategoryStruct.comp (Y := P.obj (Opposite.op (pullback (F.map (f i)) (F.map (f j)))))
              (P.map (Quiver.Hom.op (pullback.snd (F.map (f i)) (F.map (f j)))))
              (P.map (Quiver.Hom.op (pullbackComparison F (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))))) ↔
  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)))))
Tactic: rw [← pullbackComparison_comp_fst, op_comp, Functor.map_comp,
    ← pullbackComparison_comp_snd, op_comp, Functor.map_comp]