-- 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 :
  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)
h₁ :
  ∀
    (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)) ⟶
        X)
    (h :
      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)
              (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)))
              v) ⟶
          X)
        (Sigma.snd (β := fun (Y : C) ↦ Y ⟶ X)
            (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X)
              (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)))
              v) :
          Sigma.fst (β := fun (Y : C) ↦ Y ⟶ X)
              (Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X)
                (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)))
                v) ⟶
            X)),
    Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X)
        (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)))
        v ∈
      (s.bind t).uncurry
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (s.bind t).uncurry

Tactic:
obtain ⟨rfl, h⟩ := h

Premises used: rfl