-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
hU : IsCompact (↑U : Set (↑(PrimeSpectrum.Top R) : Type u))
s :
  Functor.obj
    (ObjectProperty.FullSubcategory.obj (P :=
      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
      (structureSheafInType R M))
    (op U)
g : (x : ↥U) → R
hxg :
  ∀ (x : ↥U), Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen (g x)) (↑x : (↑(PrimeSpectrum.Top R) : Type u))
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : (x : ↥U) → M
H :
  ∀ (x : ↥U),
    Eq (α :=
      Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheafInType R M))
        (op (basicOpen (g x))))
      (const (f x) (g x) (basicOpen (g x)) ⋯)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                (structureSheafInType R M))
              ⋯.hom.op) :
          (a : (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) ((structureSheafInType R M).obj.obj (op (basicOpen (g x)))))
        s)
n : (i j : ↥U) → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : (↑U : Set (↑(PrimeSpectrum.Top R) : Type u)) ⊆ ⋃ i ∈ t, (↑(basicOpen (g i)) : Set (PrimeSpectrum R))
N : ℕ := (t ×ˢ t).sup fun (x : ↥U × ↥U) ↦ n x.1 x.2 + 1
i : ↥t
h :
  ∀ (x : ↥(unop (op (basicOpen ((fun (i : ↥t) ↦ g (↑i : ↥U) ^ (N + 1)) i))))),
    HSMul.hSMul (α := ↥(↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) 1
        (HSMul.hSMul (α := ↥(↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) (β := M)
          (Subtype.mk (p := fun (x_1 : R) ↦
            Membership.mem (γ := Submonoid R)
              (Ideal.primeCompl
                (PrimeSpectrum.asIdeal
                  (↑((Quiver.Hom.unop (Quiver.Hom.op (homOfLE ⋯)) :
                          (a : ↥(unop (op (basicOpen ((fun (i : ↥t) ↦ g (↑i : ↥U) ^ (N + 1)) i))))) →
                            ↥(unop (op (basicOpen (g (↑i : ↥U))))))
                        x) :
                    (↑(PrimeSpectrum.Top R) : Type u))))
              x_1)
            (g (↑i : ↥U)) ⋯)
          ((fun (i : ↥t) ↦ g (↑i : ↥U) ^ N • f (↑i : ↥U)) i)) =
      HSMul.hSMul (α := ↥(↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) 1
        (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl)
            ((fun (i : ↥t) ↦ g (↑i : ↥U) ^ (N + 1)) i) ⋯ •
          f (↑i : ↥U))
⊢ Eq.{u + 1} (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ) (Sheaf.presheaf (structureSheafInType R M))
        (op (basicOpen ((fun (i : ↥t) ↦ g (↑i : ↥U) ^ (N + 1)) i)))))
    (const ((fun (i : ↥t) ↦ g (↑i : ↥U) ^ N • f (↑i : ↥U)) i) ((fun (i : ↥t) ↦ g (↑i : ↥U) ^ (N + 1)) i)
      (basicOpen ((fun (i : ↥t) ↦ g (↑i : ↥U) ^ (N + 1)) i)) ⋯)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map (Sheaf.presheaf (structureSheafInType R M)) (Quiver.Hom.op (homOfLE ⋯))) :
        (a : (fun (X : Type u) ↦ X) ((structureSheafInType R M).presheaf.obj (op (basicOpen (g (↑i : ↥U)))))) →
          (fun (X : Type u) ↦ X)
            ((structureSheafInType R M).presheaf.obj (op (basicOpen ((fun (i : ↥t) ↦ g (↑i : ↥U) ^ (N + 1)) i)))))
      (const (f (↑i : ↥U)) (g (↑i : ↥U)) (basicOpen (g (↑i : ↥U))) ⋯))

Tactic:
refine Subtype.ext <| funext fun x ↦ LocalizedModule.mk_eq.mpr ⟨1, ?_⟩

Premises used: Iff.mpr, LocalizedModule.mk_eq, funext, Exists.intro, OfNat.ofNat, Subtype.ext