-- 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 : ι) → (F.op ⋙ P).obj (Opposite.op (Y i))),
      Arrows.PullbackCompatible (F.op ⋙ P) f x →
        ∃! t : (F.op ⋙ P).obj (Opposite.op X),
          ∀ (i : ι),
            (ConcreteCategory.hom (FC := TypeCat.Fun) ((F.op ⋙ P).map (f i).op) :
                  (a : (F.op ⋙ P).obj (Opposite.op X)) → (F.op ⋙ P).obj (Opposite.op (Y i)))
                t =
              x i) ↔
    ∀ (x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))),
      Arrows.PullbackCompatible P (B := F.obj X) (fun (i : ι) ↦ F.map (f i)) x →
        ∃! 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 dsimp : (∀ (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) ↔
  ∀ (x : (i : ι) → P.obj (Opposite.op (F.obj (Y 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
Tactic: dsimp [Arrows.PullbackCompatible]