-- 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
Y : C
u : Y ⟶ X
hu : Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Y u ∈ s.uncurry
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)
⊢ Eq (α :=
    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).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)

Tactic:
rw [heq_iff_eq] at h

Premises used: heq_iff_eq