-- 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
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)
⊢ Sigma.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (s.bind t).uncurry
have 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
Tactic: obtain ⟨rfl, h⟩ := h
Cleared hypotheses: Z, v, h