-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.IsSheafFor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : Functor.{v₁, w, u₁, w + 1} Cᵒᵖ (Type w)
X : C
R : Presieve.{v₁, u₁} X
x : FamilyOfElements P R
inst_1 : R.HasPairwisePullbacks
t : x.PullbackCompatible (R := R)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : R f₁
hf₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
this : HasPullback f₁ f₂
mpr :
  Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (P.map
              (CategoryStruct.comp (Y := Limits.pullback f₁ f₂) (pullback.lift g₁ g₂ comm) (pullback.fst f₁ f₂)).op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op Y₁))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x f₁ hf₁) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op Y₂))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x f₂ hf₂) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
mpr₁ :
  Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (P.map
              (CategoryStruct.comp (Y := op (Limits.pullback f₁ f₂)) (Quiver.Hom.op (pullback.fst f₁ f₂))
                (Quiver.Hom.op (pullback.lift g₁ g₂ comm)))) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op Y₁))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x f₁ hf₁) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op Y₂))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x f₂ hf₂) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
mpr₂ :
  Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := P.obj (op (Limits.pullback f₁ f₂))) (P.map (Quiver.Hom.op (pullback.fst f₁ f₂)))
              (P.map (Quiver.Hom.op (pullback.lift g₁ g₂ comm)))) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op Y₁))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x f₁ hf₁) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op Y₂))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x f₂ hf₂) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
mpr₃ :
  Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.lift g₁ g₂ comm))) :
          (a : P.obj (op (Limits.pullback f₁ f₂))) → P.obj (op Z))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.fst f₁ f₂))) :
              (a : P.obj (op Y₁)) → P.obj (op (Limits.pullback f₁ f₂)))
            (x f₁ hf₁) :
          P.obj (op (Limits.pullback f₁ f₂))) :
      P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op Y₂))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x f₂ hf₂) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
mpr₄ :
  Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.lift g₁ g₂ comm))) :
          (a : P.obj (op (Limits.pullback f₁ f₂))) → P.obj (op Z))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map (Quiver.Hom.op (pullback.snd f₁ f₂))) :
              (a : (fun (X : Type w) ↦ X) (P.obj (op Y₂))) →
                (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback f₁ f₂))))
            (x f₂ hf₂) :
          (fun (X : Type w) ↦ X) (P.obj (op (Limits.pullback f₁ f₂)))) :
      P.obj (op Z))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op Y₂))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x f₂ hf₂) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₁.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op Y₁))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x f₁ hf₁) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op Y₂))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
        (x f₂ hf₂) :
      (fun (X : Type w) ↦ X) (P.obj (op Z)))
have mpr₅ : Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Z)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := P.obj (op (Limits.pullback f₁ f₂))) (P.map (Quiver.Hom.op (pullback.snd f₁ f₂)))
            (P.map (Quiver.Hom.op (pullback.lift g₁ g₂ comm)))) :
        (a : (fun (X : Type w) ↦ X) (P.obj (op Y₂))) → P.obj (op Z))
      (x f₂ hf₂) :
    P.obj (op Z))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g₂.op) :
        (a : (fun (X : Type w) ↦ X) (P.obj (op Y₂))) → (fun (X : Type w) ↦ X) (P.obj (op Z)))
      (x f₂ hf₂) :
    (fun (X : Type w) ↦ X) (P.obj (op Z)))
Tactic: rw [← pullback.lift_fst _ _ comm, op_comp, Functor.map_comp, comp_apply,
      t hf₁ hf₂, ← comp_apply, ← Functor.map_comp, ← op_comp, pullback.lift_snd]