-- Module: Mathlib.CategoryTheory.Sites.Sieves
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
s : Presieve.{v₁, u₁} X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve.{v₁, u₁} Y
Z : C
v : Z ⟶ X
fst : C
f : fst ⟶ X
hf : Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f ∈ s.uncurry
Y : C
g : Y ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)
hg :
  Sigma.mk (β := fun (Z : C) ↦ Z ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) Y
      g ∈
    (t (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) ⋯).uncurry
h :
  Eq (α := (Y : C) × (Y ⟶ X))
    (Sigma.map (β₁ := fun (Z : C) ↦
      Z ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) (β₂ := fun (Y : C) ↦ Y ⟶ X)
      id
      (fun (Z : C) (g : Z ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) ↦
        g ≫ Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f))
      (Sigma.mk (β := fun (Z : C) ↦
        Z ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) Y g))
    (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v)
⊢ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X)
        (Sigma.map (β₁ := fun (Z : C) ↦
          Z ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) (β₂ := fun (Y : C) ↦
          Y ⟶ X) id
          (fun (Z : C) (g : Z ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) ↦
            g ≫ Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f))
          (Sigma.mk (β := fun (Z : C) ↦
            Z ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) Y g)) =
      Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) ∧
    HEq.{v₁ + 1} (α :=
      Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X)
          (Sigma.map (β₁ := fun (Z : C) ↦
            Z ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) (β₂ := fun (Y : C) ↦
            Y ⟶ X) id
            (fun (Z : C) (g : Z ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) ↦
              g ≫ Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f))
            (Sigma.mk (β := fun (Z : C) ↦
              Z ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) Y g)) ⟶
        X)
      (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X)
          (Sigma.map (β₁ := fun (Z : C) ↦
            Z ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) (β₂ := fun (Y : C) ↦
            Y ⟶ X) id
            (fun (Z : C) (g : Z ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) ↦
              g ≫ Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f))
            (Sigma.mk (β := fun (Z : C) ↦
              Z ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) Y g)) :
        Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X)
            (Sigma.map (β₁ := fun (Z : C) ↦
              Z ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) (β₂ := fun (Y : C) ↦
              Y ⟶ X) id
              (fun (Z : C) (g : Z ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) ↦
                g ≫ Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f))
              (Sigma.mk (β := fun (Z : C) ↦
                Z ⟶ Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) fst f)) Y g)) ⟶
          X)
      (β := Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) ⟶ X)
      (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) :
        Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X) (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v) ⟶ X)

Tactic:
rw [Sigma.ext_iff] at h

Premises used: Sigma.ext_iff