-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
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 :
  IsUnit (M :=
    Module.End (↑(Presheaf.stalk (structurePresheafInCommRingCat R) 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))
rw :
  ∀
    (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))),
    Function.Bijective (α := (↑(Presheaf.stalk (structurePresheafInModuleCat R M) x) : Type u)) (β :=
      (↑(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))
⊢ IsUnit (M := Module.End R (↑(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))

Tactic:
rw [Module.End.isUnit_iff] at this ⊢

Premises used: Module.End.isUnit_iff