-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Sites.Representability (goal)
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
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 = γ ≫ β
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)))
⊢ γ ≫ α = γ ≫ β
have rw : ∀
  (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)))
          (a ≫ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) i) :
        (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)))
          (b ≫ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) j) :
        (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op V)))),
  a ≫ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) i =
    b ≫ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) j
Tactic: rw [← fac₁, ← fac₂] at h ⊢
Cleared hypotheses: h