-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
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)
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ B) Z v ∈ (pullbackArrows b s).uncurry
have 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
Tactic: obtain ⟨rfl, h⟩ := h
Cleared hypotheses: Z, v, h