-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
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)))
⊢ 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))
have simp_rw : HSMul.hSMul (α :=
    ↥(Ideal.primeCompl
        (PrimeSpectrum.asIdeal
          (↑((sorry.hom.op.unop : (a : ↥(basicOpen (b i))) → ↥(basicOpen f)) x) : (↑(PrimeSpectrum.Top R) : Type u)))))
    1
    (HSMul.hSMul (α :=
      ↥(Ideal.primeCompl
          (PrimeSpectrum.asIdeal
            (↑((sorry.hom.op.unop : (a : ↥(basicOpen (b i))) → ↥(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) sorry)
      (∑ i : ι, HSMul.hSMul (α := R) ((c : (a : ι) → R) i : R) (a i))) =
  HSMul.hSMul (α :=
    ↥(Ideal.primeCompl
        (PrimeSpectrum.asIdeal
          (↑((sorry.hom.op.unop : (a : ↥(basicOpen (b i))) → ↥(basicOpen f)) x) : (↑(PrimeSpectrum.Top R) : Type u)))))
    1
    (HSMul.hSMul (α :=
      ↥(Ideal.primeCompl
          (PrimeSpectrum.asIdeal
            (↑((sorry.hom.op.unop : (a : ↥(basicOpen (b i))) → ↥(basicOpen f)) x) : (↑(PrimeSpectrum.Top R) : Type u)))))
      (Subtype.mk (p := fun (x_1 : R) ↦
        Membership.mem (γ := Submonoid R)
          (Ideal.primeCompl
            (PrimeSpectrum.asIdeal
              (↑((sorry.hom.op.unop : (a : ↥(basicOpen (b i))) → ↥(basicOpen f)) x) : (↑(PrimeSpectrum.Top R) : Type u))))
          x_1)
        (f ^ (n + 1)) sorry)
      (a i))
Tactic: simp_rw [one_smul, Finset.smul_sum, Submonoid.smul_def, smul_comm (b i), hab _ i, ← smul_assoc,
    ← Finset.sum_smul, hc]