-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M_1 : ModuleCat (↑R : Type u)
M N : (Spec R).Modules
f : Functor.obj modulesSpecToSheaf M ⟶ Functor.obj modulesSpecToSheaf N
U : (Opens ↥(Spec R))ᵒᵖ
t :
  (↑(Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
        U) :
    Type u)
m : (↑(M.val.1 U) : Type u)
x : ↥(Spec R)
hxU : x ∈ unop U
r : (↑R : Type u)
hxr : x ∈ (↑(basicOpen r) : Set (PrimeSpectrum (↑R : Type u)))
hrU : basicOpen r ≤ unop U
this :
  ∀
    (x :
      (↑((Functor.obj modulesSpecToSheaf M).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))).obj
            (op (unop U))) :
        Type u)),
    Eq (α :=
      (↑((Functor.obj modulesSpecToSheaf N).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))).obj
            (op (basicOpen r))) :
        Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑R : Type u)) ↦
              LinearMap (R := (↑R : Type u)) (RingHom.id (↑R : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (X :=
              (Functor.obj modulesSpecToSheaf M).obj (P :=
                    CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))).obj
                (op (basicOpen r)))
              (f.hom.app (op (basicOpen r))) :
            (a : (↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen r))) : Type u)) →
              (↑((modulesSpecToSheaf.obj N).obj.obj (op (basicOpen r))) : Type u))
          ((ConcreteCategory.hom (FC :=
                  fun
                    (x1 x2 :
                      ModuleCat
                        (↑(Functor.obj
                              (ObjectProperty.FullSubcategory.obj (P :=
                                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
                                (Spec R).ringCatSheaf)
                              (op (unop U))) :
                          Type u)) ↦
                  LinearMap (R :=
                    (↑(Functor.obj
                          (ObjectProperty.FullSubcategory.obj (P :=
                            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
                            (Spec R).ringCatSheaf)
                          (op (unop U))) :
                      Type u))
                    (RingHom.id
                      (↑(Functor.obj
                            (ObjectProperty.FullSubcategory.obj (P :=
                              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
                              (Spec R).ringCatSheaf)
                            (op (unop U))) :
                        Type u))
                    (↑x1 : Type u) (↑x2 : Type u))
                  (CC := ModuleCat.carrier) (M.val.map (homOfLE hrU).op) :
                (a : (↑(M.val.obj (op (unop U))) : Type u)) →
                  (↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((Spec R).ringCatSheaf.obj.map (homOfLE hrU).op))).obj
                        (M.val.obj (op (basicOpen r)))) :
                    Type u))
              x :
            (↑(Functor.obj (C :=
                  ModuleCat
                    (↑(Functor.obj (C := (Opens ↥(Spec R))ᵒᵖ)
                          (ObjectProperty.FullSubcategory.obj (P :=
                            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
                            (Spec R).ringCatSheaf)
                          (op (basicOpen r))) :
                      Type u))
                  (ModuleCat.restrictScalars
                    (RingCat.Hom.hom
                      (CategoryTheory.Functor.map
                        (ObjectProperty.FullSubcategory.obj (P :=
                          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                        (homOfLE hrU).op)))
                  (M.val.obj (op (basicOpen r)))) :
              Type u)) :
        (↑((Functor.obj modulesSpecToSheaf N).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))).obj
              (op (basicOpen r))) :
          Type u))
      ((ConcreteCategory.hom (FC :=
              fun
                (x1 x2 :
                  ModuleCat
                    (↑(Functor.obj
                          (ObjectProperty.FullSubcategory.obj (P :=
                            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
                            (Spec R).ringCatSheaf)
                          (op (unop U))) :
                      Type u)) ↦
              LinearMap (R :=
                (↑(Functor.obj
                      (ObjectProperty.FullSubcategory.obj (P :=
                        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                      (op (unop U))) :
                  Type u))
                (RingHom.id
                  (↑(Functor.obj
                        (ObjectProperty.FullSubcategory.obj (P :=
                          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                        (op (unop U))) :
                    Type u))
                (↑x1 : Type u) (↑x2 : Type u))
              (CC := ModuleCat.carrier) (N.val.map (homOfLE hrU).op) :
            (a : (↑(N.val.obj (op (unop U))) : Type u)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((Spec R).ringCatSheaf.obj.map (homOfLE hrU).op))).obj
                    (N.val.obj (op (basicOpen r)))) :
                Type u))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑R : Type u)) ↦
                  LinearMap (R := (↑R : Type u)) (RingHom.id (↑R : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
                  ModuleCat.carrier) (X :=
                  (Functor.obj modulesSpecToSheaf M).obj (P :=
                        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))).obj
                    (op (unop U)))
                  (f.hom.app (op (unop U))) :
                (a : (↑((modulesSpecToSheaf.obj M).obj.obj (op (unop U))) : Type u)) →
                  (↑((modulesSpecToSheaf.obj N).obj.obj (op (unop U))) : Type u))
              x :
            (↑((Functor.obj modulesSpecToSheaf N).obj (P :=
                      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))).obj
                  (op (unop U))) :
              Type u)) :
        (↑(Functor.obj (C :=
              ModuleCat
                (↑(Functor.obj (C := (Opens ↥(Spec R))ᵒᵖ)
                      (ObjectProperty.FullSubcategory.obj (P :=
                        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                      (op (basicOpen r))) :
                  Type u))
              (ModuleCat.restrictScalars
                (RingCat.Hom.hom
                  (CategoryTheory.Functor.map
                    (ObjectProperty.FullSubcategory.obj (P :=
                      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                    (homOfLE hrU).op)))
              (N.val.obj (op (basicOpen r)))) :
          Type u))
generalize :
  ∀
    (t :
      (↑(Functor.obj (C := (Opens ↥(Spec R))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
            (op (basicOpen r))) :
        Type u)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑R : Type u)) ↦
            LinearMap (R := (↑R : Type u)) (RingHom.id (↑R : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
            ModuleCat.carrier) (X :=
            (Functor.obj modulesSpecToSheaf M).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))).obj
              (op (basicOpen r)))
            (f.hom.app (op (basicOpen r))) :
          (a : (↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen r))) : Type u)) →
            (↑((modulesSpecToSheaf.obj N).obj.obj (op (basicOpen r))) : Type u))
        (HSMul.hSMul (β :=
          (↑(Functor.obj (C :=
                ModuleCat
                  (↑(Functor.obj (C := (Opens ↥(Spec R))ᵒᵖ)
                        (ObjectProperty.FullSubcategory.obj (P :=
                          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                        (op (basicOpen r))) :
                    Type u))
                (ModuleCat.restrictScalars
                  (RingCat.Hom.hom
                    (CategoryTheory.Functor.map
                      (ObjectProperty.FullSubcategory.obj (P :=
                        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                      (homOfLE hrU).op)))
                (M.val.obj (op (basicOpen r)))) :
            Type u))
          t
          ((ConcreteCategory.hom (FC :=
                  fun
                    (x1 x2 :
                      ModuleCat
                        (↑(Functor.obj
                              (ObjectProperty.FullSubcategory.obj (P :=
                                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
                                (Spec R).ringCatSheaf)
                              (op (unop U))) :
                          Type u)) ↦
                  LinearMap (R :=
                    (↑(Functor.obj
                          (ObjectProperty.FullSubcategory.obj (P :=
                            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
                            (Spec R).ringCatSheaf)
                          (op (unop U))) :
                      Type u))
                    (RingHom.id
                      (↑(Functor.obj
                            (ObjectProperty.FullSubcategory.obj (P :=
                              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
                              (Spec R).ringCatSheaf)
                            (op (unop U))) :
                        Type u))
                    (↑x1 : Type u) (↑x2 : Type u))
                  (CC := ModuleCat.carrier) (M.val.map (homOfLE hrU).op) :
                (a : (↑(M.val.obj (op (unop U))) : Type u)) →
                  (↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((Spec R).ringCatSheaf.obj.map (homOfLE hrU).op))).obj
                        (M.val.obj (op (basicOpen r)))) :
                    Type u))
              m :
            (↑(Functor.obj (C :=
                  ModuleCat
                    (↑(Functor.obj (C := (Opens ↥(Spec R))ᵒᵖ)
                          (ObjectProperty.FullSubcategory.obj (P :=
                            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
                            (Spec R).ringCatSheaf)
                          (op (basicOpen r))) :
                      Type u))
                  (ModuleCat.restrictScalars
                    (RingCat.Hom.hom
                      (CategoryTheory.Functor.map
                        (ObjectProperty.FullSubcategory.obj (P :=
                          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                        (homOfLE hrU).op)))
                  (M.val.obj (op (basicOpen r)))) :
              Type u))) =
      HSMul.hSMul (β :=
        (↑(Functor.obj (C :=
              ModuleCat
                (↑(Functor.obj (C := (Opens ↥(Spec R))ᵒᵖ)
                      (ObjectProperty.FullSubcategory.obj (P :=
                        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                      (op (basicOpen r))) :
                  Type u))
              (ModuleCat.restrictScalars
                (RingCat.Hom.hom
                  (CategoryTheory.Functor.map
                    (ObjectProperty.FullSubcategory.obj (P :=
                      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                    (homOfLE hrU).op)))
              (N.val.obj (op (basicOpen r)))) :
          Type u))
        t
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑R : Type u)) ↦
                LinearMap (R := (↑R : Type u)) (RingHom.id (↑R : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
                ModuleCat.carrier) (X :=
                (Functor.obj modulesSpecToSheaf M).obj (P :=
                      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))).obj
                  (op (basicOpen r)))
                (f.hom.app (op (basicOpen r))) :
              (a : (↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen r))) : Type u)) →
                (↑((modulesSpecToSheaf.obj N).obj.obj (op (basicOpen r))) : Type u))
            ((ConcreteCategory.hom (FC :=
                    fun
                      (x1 x2 :
                        ModuleCat
                          (↑(Functor.obj
                                (ObjectProperty.FullSubcategory.obj (P :=
                                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
                                  (Spec R).ringCatSheaf)
                                (op (unop U))) :
                            Type u)) ↦
                    LinearMap (R :=
                      (↑(Functor.obj
                            (ObjectProperty.FullSubcategory.obj (P :=
                              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
                              (Spec R).ringCatSheaf)
                            (op (unop U))) :
                        Type u))
                      (RingHom.id
                        (↑(Functor.obj
                              (ObjectProperty.FullSubcategory.obj (P :=
                                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
                                (Spec R).ringCatSheaf)
                              (op (unop U))) :
                          Type u))
                      (↑x1 : Type u) (↑x2 : Type u))
                    (CC := ModuleCat.carrier) (M.val.map (homOfLE hrU).op) :
                  (a : (↑(M.val.obj (op (unop U))) : Type u)) →
                    (↑((ModuleCat.restrictScalars
                              (RingCat.Hom.hom ((Spec R).ringCatSheaf.obj.map (homOfLE hrU).op))).obj
                          (M.val.obj (op (basicOpen r)))) :
                      Type u))
                m :
              (↑(Functor.obj (C :=
                    ModuleCat
                      (↑(Functor.obj (C := (Opens ↥(Spec R))ᵒᵖ)
                            (ObjectProperty.FullSubcategory.obj (P :=
                              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
                              (Spec R).ringCatSheaf)
                            (op (basicOpen r))) :
                        Type u))
                    (ModuleCat.restrictScalars
                      (RingCat.Hom.hom
                        (CategoryTheory.Functor.map
                          (ObjectProperty.FullSubcategory.obj (P :=
                            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
                            (Spec R).ringCatSheaf)
                          (homOfLE hrU).op)))
                    (M.val.obj (op (basicOpen r)))) :
                Type u)) :
          (↑((Functor.obj modulesSpecToSheaf N).obj (P :=
                    CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))).obj
                (op (basicOpen r))) :
            Type u))
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑R : Type u)) ↦
          LinearMap (R := (↑R : Type u)) (RingHom.id (↑R : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
          ModuleCat.carrier) (X :=
          (Functor.obj modulesSpecToSheaf M).obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))).obj
            (op (basicOpen r)))
          (f.hom.app (op (basicOpen r))) :
        (a : (↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen r))) : Type u)) →
          (↑((modulesSpecToSheaf.obj N).obj.obj (op (basicOpen r))) : Type u))
      (HSMul.hSMul (α :=
        (↑(Functor.obj (C := (Opens ↥(Spec R))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
              (op (basicOpen r))) :
          Type u))
        (β :=
        (↑(Functor.obj (C :=
              ModuleCat
                (↑(Functor.obj (C := (Opens ↥(Spec R))ᵒᵖ)
                      (ObjectProperty.FullSubcategory.obj (P :=
                        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                      (op (basicOpen r))) :
                  Type u))
              (ModuleCat.restrictScalars
                (RingCat.Hom.hom
                  (CategoryTheory.Functor.map
                    (ObjectProperty.FullSubcategory.obj (P :=
                      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                    (homOfLE hrU).op)))
              (M.val.obj (op (basicOpen r)))) :
          Type u))
        ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
                (X :=
                Functor.obj
                  (ObjectProperty.FullSubcategory.obj (P :=
                    CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                  (op (unop U)))
                (Y :=
                Functor.obj (C := (Opens ↥(Spec R))ᵒᵖ)
                  (ObjectProperty.FullSubcategory.obj (P :=
                    CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                  (op (basicOpen r)))
                (CategoryTheory.Functor.map
                  (ObjectProperty.FullSubcategory.obj (P :=
                    CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                  (homOfLE hrU).op) :
              (a : (↑((Spec R).ringCatSheaf.obj.obj (op (unop U))) : Type u)) →
                (↑((Spec R).ringCatSheaf.obj.obj (op (basicOpen r))) : Type u))
            t :
          (↑(Functor.obj (C := (Opens ↥(Spec R))ᵒᵖ)
                (ObjectProperty.FullSubcategory.obj (P :=
                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                (op (basicOpen r))) :
            Type u))
        ((ConcreteCategory.hom (FC :=
                fun
                  (x1 x2 :
                    ModuleCat
                      (↑(Functor.obj
                            (ObjectProperty.FullSubcategory.obj (P :=
                              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
                              (Spec R).ringCatSheaf)
                            (op (unop U))) :
                        Type u)) ↦
                LinearMap (R :=
                  (↑(Functor.obj
                        (ObjectProperty.FullSubcategory.obj (P :=
                          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                        (op (unop U))) :
                    Type u))
                  (RingHom.id
                    (↑(Functor.obj
                          (ObjectProperty.FullSubcategory.obj (P :=
                            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
                            (Spec R).ringCatSheaf)
                          (op (unop U))) :
                      Type u))
                  (↑x1 : Type u) (↑x2 : Type u))
                (CC := ModuleCat.carrier) (M.val.map (homOfLE hrU).op) :
              (a : (↑(M.val.obj (op (unop U))) : Type u)) →
                (↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((Spec R).ringCatSheaf.obj.map (homOfLE hrU).op))).obj
                      (M.val.obj (op (basicOpen r)))) :
                  Type u))
            m :
          (↑(Functor.obj (C :=
                ModuleCat
                  (↑(Functor.obj (C := (Opens ↥(Spec R))ᵒᵖ)
                        (ObjectProperty.FullSubcategory.obj (P :=
                          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                        (op (basicOpen r))) :
                    Type u))
                (ModuleCat.restrictScalars
                  (RingCat.Hom.hom
                    (CategoryTheory.Functor.map
                      (ObjectProperty.FullSubcategory.obj (P :=
                        CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                      (homOfLE hrU).op)))
                (M.val.obj (op (basicOpen r)))) :
            Type u))) =
    HSMul.hSMul (α :=
      (↑(Functor.obj (C := (Opens ↥(Spec R))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
            (op (basicOpen r))) :
        Type u))
      (β :=
      (↑(Functor.obj (C :=
            ModuleCat
              (↑(Functor.obj (C := (Opens ↥(Spec R))ᵒᵖ)
                    (ObjectProperty.FullSubcategory.obj (P :=
                      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                    (op (basicOpen r))) :
                Type u))
            (ModuleCat.restrictScalars
              (RingCat.Hom.hom
                (CategoryTheory.Functor.map
                  (ObjectProperty.FullSubcategory.obj (P :=
                    CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                  (homOfLE hrU).op)))
            (N.val.obj (op (basicOpen r)))) :
        Type u))
      ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
              (X :=
              Functor.obj
                (ObjectProperty.FullSubcategory.obj (P :=
                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                (op (unop U)))
              (Y :=
              Functor.obj (C := (Opens ↥(Spec R))ᵒᵖ)
                (ObjectProperty.FullSubcategory.obj (P :=
                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                (op (basicOpen r)))
              (CategoryTheory.Functor.map
                (ObjectProperty.FullSubcategory.obj (P :=
                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                (homOfLE hrU).op) :
            (a : (↑((Spec R).ringCatSheaf.obj.obj (op (unop U))) : Type u)) →
              (↑((Spec R).ringCatSheaf.obj.obj (op (basicOpen r))) : Type u))
          t :
        (↑(Functor.obj (C := (Opens ↥(Spec R))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
              (op (basicOpen r))) :
          Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑R : Type u)) ↦
              LinearMap (R := (↑R : Type u)) (RingHom.id (↑R : Type u)) (↑x1 : Type u) (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (X :=
              (Functor.obj modulesSpecToSheaf M).obj (P :=
                    CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))).obj
                (op (basicOpen r)))
              (f.hom.app (op (basicOpen r))) :
            (a : (↑((modulesSpecToSheaf.obj M).obj.obj (op (basicOpen r))) : Type u)) →
              (↑((modulesSpecToSheaf.obj N).obj.obj (op (basicOpen r))) : Type u))
          ((ConcreteCategory.hom (FC :=
                  fun
                    (x1 x2 :
                      ModuleCat
                        (↑(Functor.obj
                              (ObjectProperty.FullSubcategory.obj (P :=
                                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
                                (Spec R).ringCatSheaf)
                              (op (unop U))) :
                          Type u)) ↦
                  LinearMap (R :=
                    (↑(Functor.obj
                          (ObjectProperty.FullSubcategory.obj (P :=
                            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
                            (Spec R).ringCatSheaf)
                          (op (unop U))) :
                      Type u))
                    (RingHom.id
                      (↑(Functor.obj
                            (ObjectProperty.FullSubcategory.obj (P :=
                              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
                              (Spec R).ringCatSheaf)
                            (op (unop U))) :
                        Type u))
                    (↑x1 : Type u) (↑x2 : Type u))
                  (CC := ModuleCat.carrier) (M.val.map (homOfLE hrU).op) :
                (a : (↑(M.val.obj (op (unop U))) : Type u)) →
                  (↑((ModuleCat.restrictScalars (RingCat.Hom.hom ((Spec R).ringCatSheaf.obj.map (homOfLE hrU).op))).obj
                        (M.val.obj (op (basicOpen r)))) :
                    Type u))
              m :
            (↑(Functor.obj (C :=
                  ModuleCat
                    (↑(Functor.obj (C := (Opens ↥(Spec R))ᵒᵖ)
                          (ObjectProperty.FullSubcategory.obj (P :=
                            CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
                            (Spec R).ringCatSheaf)
                          (op (basicOpen r))) :
                      Type u))
                  (ModuleCat.restrictScalars
                    (RingCat.Hom.hom
                      (CategoryTheory.Functor.map
                        (ObjectProperty.FullSubcategory.obj (P :=
                          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) (Spec R).ringCatSheaf)
                        (homOfLE hrU).op)))
                  (M.val.obj (op (basicOpen r)))) :
              Type u)) :
        (↑((Functor.obj modulesSpecToSheaf N).obj (P :=
                  CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))).obj
              (op (basicOpen r))) :
          Type u))

Tactic:
generalize (Spec R).ringCatSheaf.obj.map (homOfLE hrU).op t = t

Premises used: AlgebraicGeometry.Spec, CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Functor.map, AlgebraicGeometry.Scheme.ringCatSheaf, CategoryTheory.homOfLE, DFunLike.coe