-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
U : X.Opens
f g : (↑Γ(X, U) : Type u)
𝒰 : OpenCover.{u_1, u} X
h :
  ∀ (i : 𝒰.I₀),
    Eq (α := (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          f :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.app (𝒰.f i) U) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
          g :
        (↑Γ(𝒰.X i, 𝒰.f i ⁻¹ᵁ U) : Type u))
hcover : U ≤ ⨆ (i : ↥X), Hom.opensRange (X := 𝒰.X (Cover.idx 𝒰 i)) (𝒰.f (Cover.idx 𝒰 i)) ⊓ U
h₁ :
  ∀ (i : ↥X),
    Eq (α :=
      (↑(X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj
            (op (Hom.opensRange (X := 𝒰.X (Cover.idx 𝒰 i)) (𝒰.f (Cover.idx 𝒰 i)) ⊓ U))) :
        Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj (op U))
              (Y :=
              X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj
                (op (Hom.opensRange (X := 𝒰.X (Cover.idx 𝒰 i)) (𝒰.f (Cover.idx 𝒰 i)) ⊓ U)))
              (X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).map (Quiver.Hom.op (homOfLE ⋯))) :
            (a : (↑(X.sheaf.obj.obj (op U)) : Type u)) →
              (↑(X.sheaf.obj.obj (op (Hom.opensRange (𝒰.f (Cover.idx 𝒰 i)) ⊓ U))) : Type u))
          f :
        (↑(X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj
              (op (Hom.opensRange (X := 𝒰.X (Cover.idx 𝒰 i)) (𝒰.f (Cover.idx 𝒰 i)) ⊓ U))) :
          Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj (op U))
              (Y :=
              X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj
                (op (Hom.opensRange (X := 𝒰.X (Cover.idx 𝒰 i)) (𝒰.f (Cover.idx 𝒰 i)) ⊓ U)))
              (X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).map (Quiver.Hom.op (homOfLE ⋯))) :
            (a : (↑(X.sheaf.obj.obj (op U)) : Type u)) →
              (↑(X.sheaf.obj.obj (op (Hom.opensRange (𝒰.f (Cover.idx 𝒰 i)) ⊓ U))) : Type u))
          g :
        (↑(X.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj
              (op (Hom.opensRange (X := 𝒰.X (Cover.idx 𝒰 i)) (𝒰.f (Cover.idx 𝒰 i)) ⊓ U))) :
          Type u))
⊢ f = g

Tactic:
fapply TopCat.Sheaf.eq_of_locally_eq' X.sheaf
    (fun i ↦ (𝒰.f (𝒰.idx i)).opensRange ⊓ U) _ (fun _ ↦ homOfLE inf_le_right)

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Hom.opensRange, inf_le_right, AlgebraicGeometry.Scheme.sheaf, TopCat.Sheaf.eq_of_locally_eq', CategoryTheory.homOfLE, AlgebraicGeometry.Scheme.Cover.idx, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, Min.min