-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (hypothesis)
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.mk (β := fun (Y : C) ↦ Y ⟶ X) Z v ∈ (s.bind t).uncurry
have 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)
Tactic: rw [Sigma.ext_iff] at h
Cleared hypotheses: h