Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: case refine_1.refine_1
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, ⊤))
U : (TopologicalSpace.Opens ↥(Spec R))ᵒᵖ
⊢ ((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.obj
      U ≅
    ((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.obj
      U

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 ≫
        Iso.hom ?refine_1.refine_1 =
      Iso.hom ?refine_1.refine_1 ≫
        ((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:
· refine (ModuleCat.restrictScalarsComp'App _ _ _ ?_ _).symm ≪≫
        (ModuleCat.restrictScalarsComp φ.hom ((Scheme.ΓSpecIso S).inv).hom).app _
      rw [← CommRingCat.hom_comp, Scheme.ΓSpecIso_inv_naturality, CommRingCat.hom_comp]

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