-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R M : Type u
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
s :
  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 f))
ι : Type u
w : Fintype ι
a : ι → M
b : ι → R
ibU : ∀ (i : ι), LE.le (α := Opens (PrimeSpectrum R)) (basicOpen (b i)) (basicOpen f)
iU : LE.le (α := Opens (↑(PrimeSpectrum.Top R) : Type u)) (basicOpen f) (⨆ (i : ι), basicOpen (b i))
hab : ∀ (i j : ι), b j • a i = b i • a j
H :
  ∀ (i : ι),
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ) (Sheaf.presheaf (structureSheafInType R M))
          (op (basicOpen (b i)))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryTheory.Functor.map (Sheaf.presheaf (structureSheafInType R M)) ⋯.hom.op) :
            (a : (fun (X : Type u) ↦ X) ((structureSheafInType R M).presheaf.obj (op (basicOpen f)))) →
              (fun (X : Type u) ↦ X) ((structureSheafInType R M).presheaf.obj (op (basicOpen (b i)))))
          s :
        (fun (X : Type u) ↦ X)
          (Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ) (Sheaf.presheaf (structureSheafInType R M))
            (op (basicOpen (b i)))))
      (const (a i) (b i) (basicOpen (b i)) ⋯ :
        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 (b i))))
n : ℕ
c : ι →₀ R
hc : ∑ i : ι, HSMul.hSMul (α := R) ((c : (a : ι) → R) i : R) (b i) = f ^ (n + 1)
refine :
  ∀ (i : ι) (x : ↥(unop (op ((fun (i : ι) ↦ (basicOpen (b i) : Opens (PrimeSpectrum R))) i)))),
    Eq (α := Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
      ((↑((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))
                      (Quiver.Hom.op ((fun (i : ι) ↦ ⋯.hom) i))) :
                  (a : (structureSheafInType R M).obj.obj (op (basicOpen f))) →
                    (structureSheafInType R M).obj.obj (op ((fun (i : ι) ↦ basicOpen (b i)) i)))
                ((toBasicOpenₗ R M f :
                    (a : LocalizedModule.Away f M) → (structureSheafInType R M).obj.obj (op (basicOpen f)))
                  (LocalizedModule.mk (∑ i : ι, HSMul.hSMul (α := R) ((c : (a : ι) → R) i : R) (a i))
                    (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers f) x)
                      (f ^ (n + 1)) ⋯)))) :
            (x : ↥(unop (op ((fun (i : ι) ↦ basicOpen (b i)) i)))) →
              Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
          x :
        Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
      ((↑(const (a i) (b i) (basicOpen (b i)) ⋯) :
            (x : ↥(unop (op ((fun (i : ι) ↦ basicOpen (b i)) i)))) →
              Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
          x :
        Localizations M (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
⊢ (toBasicOpenₗ R M f : (a : LocalizedModule.Away f M) → (structureSheafInType R M).obj.obj (op (basicOpen f)))
      (LocalizedModule.mk (∑ i : ι, HSMul.hSMul (α := R) ((c : (a : ι) → R) i : R) (a i))
        (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers f) x) (f ^ (n + 1)) ⋯)) =
    s

Tactic:
refine (structureSheafInType R M).eq_of_locally_eq' (fun i ↦ basicOpen (b i)) _
    (fun i ↦ (ibU _).hom) iU _ _ fun i ↦ (Subtype.ext (funext fun x ↦ ?_)).trans (H _).symm

Premises used: PrimeSpectrum.basicOpen, LE.le.hom, TopCat.Sheaf.eq_of_locally_eq', AlgebraicGeometry.structureSheafInType