-- 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)
i : ι
x : ↥(unop (op ((fun (i : ι) ↦ (basicOpen (b i) : Opens (PrimeSpectrum R))) i)))
refine :
  HSMul.hSMul (α :=
      ↥(Ideal.primeCompl
          (PrimeSpectrum.asIdeal
            (↑((Quiver.Hom.unop (Quiver.Hom.op ((fun (i : ι) ↦ ⋯.hom) i)) :
                    (a : ↥(unop (op ((fun (i : ι) ↦ basicOpen (b i)) i)))) → ↥(unop (op (basicOpen f))))
                  x) :
              (↑(PrimeSpectrum.Top R) : Type u)))))
      1
      (HSMul.hSMul (α :=
        ↥(Ideal.primeCompl
            (PrimeSpectrum.asIdeal
              (↑((Quiver.Hom.unop (Quiver.Hom.op ((fun (i : ι) ↦ ⋯.hom) i)) :
                      (a : ↥(unop (op ((fun (i : ι) ↦ basicOpen (b i)) i)))) → ↥(unop (op (basicOpen f))))
                    x) :
                (↑(PrimeSpectrum.Top R) : Type u)))))
        (β := M)
        (Subtype.mk (p := fun (x_1 : R) ↦ x_1 ∈ (↑x : (↑(PrimeSpectrum.Top R) : Type u)).asIdeal.primeCompl) (b i) ⋯)
        (∑ i : ι, HSMul.hSMul (α := R) ((c : (a : ι) → R) i : R) (a i))) =
    HSMul.hSMul (α :=
      ↥(Ideal.primeCompl
          (PrimeSpectrum.asIdeal
            (↑((Quiver.Hom.unop (Quiver.Hom.op ((fun (i : ι) ↦ ⋯.hom) i)) :
                    (a : ↥(unop (op ((fun (i : ι) ↦ basicOpen (b i)) i)))) → ↥(unop (op (basicOpen f))))
                  x) :
              (↑(PrimeSpectrum.Top R) : Type u)))))
      1
      (HSMul.hSMul (α :=
        ↥(Ideal.primeCompl
            (PrimeSpectrum.asIdeal
              (↑((Quiver.Hom.unop (Quiver.Hom.op ((fun (i : ι) ↦ ⋯.hom) i)) :
                      (a : ↥(unop (op ((fun (i : ι) ↦ basicOpen (b i)) i)))) → ↥(unop (op (basicOpen f))))
                    x) :
                (↑(PrimeSpectrum.Top R) : Type u)))))
        (Subtype.mk (p := fun (x_1 : R) ↦
          Membership.mem (γ := Submonoid R)
            (Ideal.primeCompl
              (PrimeSpectrum.asIdeal
                (↑((Quiver.Hom.unop (Quiver.Hom.op ((fun (i : ι) ↦ ⋯.hom) i)) :
                        (a : ↥(unop (op ((fun (i : ι) ↦ basicOpen (b i)) i)))) → ↥(unop (op (basicOpen f))))
                      x) :
                  (↑(PrimeSpectrum.Top R) : Type u))))
            x_1)
          (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers f) x) (f ^ (n + 1)) ⋯) :
            R)
          ⋯)
        (a 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)))
              (const (∑ 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)) ⋯) :
                  R)
                (basicOpen f) ⋯)) :
          (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)))

Tactic:
refine LocalizedModule.mk_eq.mpr ⟨1, ?_⟩

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