Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: case refine_1.refine_2
X Y Z T : Scheme
M✝ N K : X.Modules
φ✝ : M✝ ⟶ N
U V : X.Opens
R S : CommRingCat
φ : R ⟶ S
M : Sheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))
⊢ ∀ {X Y : (TopologicalSpace.Opens ↥(Spec R))ᵒᵖ} (f : X ⟶ Y),
    ((sheafCompose (Opens.grothendieckTopology ↥(Spec S))
                      (ModuleCat.restrictScalars (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ)))) ⋙
                    TopCat.Sheaf.pushforward (ModuleCat ↑Γ(Spec R, ⊤)) (Spec.map φ).base ⋙
                      sheafCompose (Opens.grothendieckTopology ↥(Spec R))
                        (ModuleCat.restrictScalars (CommRingCat.Hom.hom (ΓSpecIso R).inv))).obj
                M).obj.map
          f ≫
        ((ModuleCat.restrictScalarsComp'App (CommRingCat.Hom.hom (ΓSpecIso R).inv)
                (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ)))
                ((CommRingCat.Hom.hom (ΓSpecIso S).inv).comp (CommRingCat.Hom.hom φ)) ⋯
                (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj M).obj
                  ((Opens.map (Spec.map φ).base).op.obj Y))).symm ≪≫
            (ModuleCat.restrictScalarsComp (CommRingCat.Hom.hom φ) (CommRingCat.Hom.hom (ΓSpecIso S).inv)).app
              (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj M).obj
                ((Opens.map (Spec.map φ).base).op.obj Y))).hom =
      ((ModuleCat.restrictScalarsComp'App (CommRingCat.Hom.hom (ΓSpecIso R).inv)
                (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ)))
                ((CommRingCat.Hom.hom (ΓSpecIso S).inv).comp (CommRingCat.Hom.hom φ)) ⋯
                (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj M).obj
                  ((Opens.map (Spec.map φ).base).op.obj X))).symm ≪≫
            (ModuleCat.restrictScalarsComp (CommRingCat.Hom.hom φ) (CommRingCat.Hom.hom (ΓSpecIso S).inv)).app
              (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj M).obj
                ((Opens.map (Spec.map φ).base).op.obj X))).hom ≫
        ((sheafCompose (Opens.grothendieckTopology ↥(Spec S))
                      (ModuleCat.restrictScalars (CommRingCat.Hom.hom (ΓSpecIso S).inv)) ⋙
                    TopCat.Sheaf.pushforward (ModuleCat ↑S) (Spec.map φ).base ⋙
                      sheafCompose (Opens.grothendieckTopology ↥(Spec R))
                        (ModuleCat.restrictScalars (CommRingCat.Hom.hom φ))).obj
                M).obj.map
          f

Tactic:
·

Goal state after:
case refine_1.refine_2
X Y Z T : Scheme
M✝ N K : X.Modules
φ✝ : M✝ ⟶ N
U V : X.Opens
R S : CommRingCat
φ : R ⟶ S
M : Sheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))
⊢ ∀ {X Y : (TopologicalSpace.Opens ↥(Spec R))ᵒᵖ} (f : X ⟶ Y),
    ((sheafCompose (Opens.grothendieckTopology ↥(Spec S))
                      (ModuleCat.restrictScalars (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ)))) ⋙
                    TopCat.Sheaf.pushforward (ModuleCat ↑Γ(Spec R, ⊤)) (Spec.map φ).base ⋙
                      sheafCompose (Opens.grothendieckTopology ↥(Spec R))
                        (ModuleCat.restrictScalars (CommRingCat.Hom.hom (ΓSpecIso R).inv))).obj
                M).obj.map
          f ≫
        ((ModuleCat.restrictScalarsComp'App (CommRingCat.Hom.hom (ΓSpecIso R).inv)
                (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ)))
                ((CommRingCat.Hom.hom (ΓSpecIso S).inv).comp (CommRingCat.Hom.hom φ)) ⋯
                (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj M).obj
                  ((Opens.map (Spec.map φ).base).op.obj Y))).symm ≪≫
            (ModuleCat.restrictScalarsComp (CommRingCat.Hom.hom φ) (CommRingCat.Hom.hom (ΓSpecIso S).inv)).app
              (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj M).obj
                ((Opens.map (Spec.map φ).base).op.obj Y))).hom =
      ((ModuleCat.restrictScalarsComp'App (CommRingCat.Hom.hom (ΓSpecIso R).inv)
                (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ)))
                ((CommRingCat.Hom.hom (ΓSpecIso S).inv).comp (CommRingCat.Hom.hom φ)) ⋯
                (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj M).obj
                  ((Opens.map (Spec.map φ).base).op.obj X))).symm ≪≫
            (ModuleCat.restrictScalarsComp (CommRingCat.Hom.hom φ) (CommRingCat.Hom.hom (ΓSpecIso S).inv)).app
              (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj M).obj
                ((Opens.map (Spec.map φ).base).op.obj X))).hom ≫
        ((sheafCompose (Opens.grothendieckTopology ↥(Spec S))
                      (ModuleCat.restrictScalars (CommRingCat.Hom.hom (ΓSpecIso S).inv)) ⋙
                    TopCat.Sheaf.pushforward (ModuleCat ↑S) (Spec.map φ).base ⋙
                      sheafCompose (Opens.grothendieckTopology ↥(Spec R))
                        (ModuleCat.restrictScalars (CommRingCat.Hom.hom φ))).obj
                M).obj.map
          f