-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
s : Presieve.{v₁, u₁} X
inst_1 : HasPullbacks.{v₁, u₁} C
B : C
b : B ⟶ X
Z : C
v : Z ⟶ B
Y : C
u : Y ⟶ X
hu : Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u ∈ s.uncurry
h :
  Sigma.fst (β := fun (Y : C) ↦ Y ⟶ B)
        ((fun (f : (Y : C) × (Y ⟶ X)) ↦
            (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) (pullback (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b)
                (pullback.snd (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b) :
              (Y : C) × (Y ⟶ B)))
          (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u)) =
      Sigma.fst (β := fun (Y : C) ↦ Y ⟶ B) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) Z v) ∧
    HEq.{v₁ + 1} (α :=
      Sigma.fst (β := fun (Y : C) ↦ Y ⟶ B)
          ((fun (f : (Y : C) × (Y ⟶ X)) ↦
              (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) (pullback (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b)
                  (pullback.snd (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b) :
                (Y : C) × (Y ⟶ B)))
            (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u)) ⟶
        B)
      (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ B)
          ((fun (f : (Y : C) × (Y ⟶ X)) ↦
              (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) (pullback (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b)
                  (pullback.snd (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b) :
                (Y : C) × (Y ⟶ B)))
            (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u)) :
        Sigma.fst (β := fun (Y : C) ↦ Y ⟶ B)
            ((fun (f : (Y : C) × (Y ⟶ X)) ↦
                (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) (pullback (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b)
                    (pullback.snd (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b) :
                  (Y : C) × (Y ⟶ B)))
              (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u)) ⟶
          B)
      (β := Sigma.fst (β := fun (Y : C) ↦ Y ⟶ B) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) Z v) ⟶ B)
      (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ B) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) Z v) :
        Sigma.fst (β := fun (Y : C) ↦ Y ⟶ B) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) Z v) ⟶ B)
h₁ :
  ∀
    (v :
      Sigma.fst (β := fun (Y : C) ↦ Y ⟶ B)
          ((fun (f : (Y : C) × (Y ⟶ X)) ↦
              (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) (pullback (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b)
                  (pullback.snd (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b) :
                (Y : C) × (Y ⟶ B)))
            (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u)) ⟶
        B)
    (h :
      HEq (α :=
        Sigma.fst (β := fun (Y : C) ↦ Y ⟶ B)
            ((fun (f : (Y : C) × (Y ⟶ X)) ↦
                (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) (pullback (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b)
                    (pullback.snd (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b) :
                  (Y : C) × (Y ⟶ B)))
              (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u)) ⟶
          B)
        (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ B)
            ((fun (f : (Y : C) × (Y ⟶ X)) ↦
                (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) (pullback (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b)
                    (pullback.snd (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b) :
                  (Y : C) × (Y ⟶ B)))
              (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u)) :
          Sigma.fst (β := fun (Y : C) ↦ Y ⟶ B)
              ((fun (f : (Y : C) × (Y ⟶ X)) ↦
                  (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) (pullback (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b)
                      (pullback.snd (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b) :
                    (Y : C) × (Y ⟶ B)))
                (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u)) ⟶
            B)
        (β :=
        (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B)
                (Sigma.fst (β := fun (Y : C) ↦ Y ⟶ B)
                  ((fun (f : (Y : C) × (Y ⟶ X)) ↦
                      (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) (pullback (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b)
                          (pullback.snd (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b) :
                        (Y : C) × (Y ⟶ B)))
                    (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u)))
                v).fst
            (β := fun (Y : C) ↦ Y ⟶ B) ⟶
          B)
        ((Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B)
                (Sigma.fst (β := fun (Y : C) ↦ Y ⟶ B)
                  ((fun (f : (Y : C) × (Y ⟶ X)) ↦
                      (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) (pullback (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b)
                          (pullback.snd (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b) :
                        (Y : C) × (Y ⟶ B)))
                    (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u)))
                v).snd
            (β := fun (Y : C) ↦ Y ⟶ B) :
          (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B)
                  (Sigma.fst (β := fun (Y : C) ↦ Y ⟶ B)
                    ((fun (f : (Y : C) × (Y ⟶ X)) ↦
                        (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) (pullback (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b)
                            (pullback.snd (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b) :
                          (Y : C) × (Y ⟶ B)))
                      (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u)))
                  v).fst
              (β := fun (Y : C) ↦ Y ⟶ B) ⟶
            B)),
    Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B)
        (Sigma.fst (β := fun (Y : C) ↦ Y ⟶ B)
          ((fun (f : (Y : C) × (Y ⟶ X)) ↦
              (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) (pullback (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b)
                  (pullback.snd (f.snd (β := fun (Y : C) ↦ Y ⟶ X)) b) :
                (Y : C) × (Y ⟶ B)))
            (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u)))
        v ∈
      (pullbackArrows b s).uncurry
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) Z v ∈ (pullbackArrows b s).uncurry

Tactic:
obtain ⟨rfl, h⟩ := h

Premises used: rfl