-- 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
x : (↑(PrimeSpectrum.Top R) : Type u)
f : R
hf : Membership.mem (γ := Opens (PrimeSpectrum R)) (basicOpen f) x
this :
  Function.Bijective (α := (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)) (β :=
    (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u))
    (⇑((algebraMap (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u)
                (Module.End (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u)
                  (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)) :
              (a : (↑((structurePresheafInCommRingCat R).stalk x) : Type u)) →
                Module.End (↑((structurePresheafInCommRingCat R).stalk x) : Type u)
                  (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (toStalk R x) :
                (a : (↑(CommRingCat.of R) : Type u)) → (↑((structurePresheafInCommRingCat R).stalk x) : Type u))
              f) :
          Module.End (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u)
            (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)) :
      (a : (↑((structurePresheafInModuleCat R M).stalk x) : Type u)) →
        (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
a : (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)
⊢ Eq (α := (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u))
    ((((algebraMap R (Module.End R (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)) :
                (a : R) → Module.End R (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
              f :
            Module.End R (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)) :
          (a : (↑((structurePresheafInModuleCat R M).stalk x) : Type u)) →
            (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
        a :
      (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u))
    ((((algebraMap (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u)
                  (Module.End (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u)
                    (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)) :
                (a : (↑((structurePresheafInCommRingCat R).stalk x) : Type u)) →
                  Module.End (↑((structurePresheafInCommRingCat R).stalk x) : Type u)
                    (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (toStalk R x) :
                  (a : (↑(CommRingCat.of R) : Type u)) → (↑((structurePresheafInCommRingCat R).stalk x) : Type u))
                f) :
            Module.End (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u)
              (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)) :
          (a : (↑((structurePresheafInModuleCat R M).stalk x) : Type u)) →
            (↑((structurePresheafInModuleCat R M).stalk x) : Type u))
        a :
      (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u))
have h : f • a =
  HSMul.hSMul (α := (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (toStalk R x) :
          (a : R) → (↑((structurePresheafInCommRingCat R).stalk x) : Type u))
        f :
      (↑(Presheaf.stalk (structurePresheafInCommRingCat R) x) : Type u))
    a
Tactic: simp only [Module.algebraMap_end_apply]