-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Representability (hypothesis)
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i_1 j_1 k : ι
U : Scheme
α β : U ⟶ (glueData hf).glued
h :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op U)) :
          (a : (fun (X : Type u) ↦ X) ((zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) (F.obj.obj (op U)))
        α :
      (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op U)) :
          (a : (fun (X : Type u) ↦ X) ((zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) (F.obj.obj (op U)))
        β :
      (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U)))
mem :
  Membership.mem (γ := Set (Sieve (glueData hf).glued))
    ((grothendieckTopology IsOpenImmersion : (a : Scheme) → Set (Sieve a)) (glueData hf).glued)
    (Sieve.ofArrows (I :=
      PreZeroHypercover.I₀ (S := (glueData hf).glued)
        (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover))
      (PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover))
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover)))
V : Scheme
γ : V ⟶ U
Y_1 : Scheme
i :
  PreZeroHypercover.I₀ (S := (glueData hf).glued)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover)
a : V ⟶ PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) i
fac₁ : a ≫ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) i = γ ≫ α
Y : Scheme
j :
  PreZeroHypercover.I₀ (S := (glueData hf).glued)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover)
b : V ⟶ PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) j
fac₂ : b ≫ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) j = γ ≫ β
⊢ γ ≫ α = γ ≫ β
have h₁ : Eq (α := (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op V)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op V)) :
        (a : (fun (X : Type u) ↦ X) ((zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj (op V))) →
          (fun (X : Type u) ↦ X) (F.obj.obj (op V)))
      (γ ≫ α) :
    (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op V)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op V)) :
        (a : (fun (X : Type u) ↦ X) ((zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj (op V))) →
          (fun (X : Type u) ↦ X) (F.obj.obj (op V)))
      (γ ≫ β) :
    (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op V)))
Tactic: replace h : (yonedaGluedToSheaf hf).hom.app _ (γ ≫ α) =
        (yonedaGluedToSheaf hf).hom.app _ (γ ≫ β) := by dsimp at h; simp [h]
Cleared hypotheses: h