Module: Mathlib.AlgebraicGeometry.Modules.Sheaf

Goal state before:
pp: case 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, ⊤))
⊢ ((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 ≅
    ((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

pp: case refine_2
X Y Z T : Scheme
M N K : X.Modules
φ✝ : M ⟶ N
U V : X.Opens
R S : CommRingCat
φ : R ⟶ S
⊢ ∀ {X Y : Sheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))} (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))).map
          f ≫
        (ObjectProperty.isoMk (Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) ?refine_1).hom =
      (ObjectProperty.isoMk (Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R))) ?refine_1).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 φ))).map
          f

Tactic:
· refine NatIso.ofComponents (fun U ↦ ?_) ?_
    · 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]
    · cat_disch

Goal state after:
case refine_2
X Y Z T : Scheme
M N K : X.Modules
φ✝ : M ⟶ N
U V : X.Opens
R S : CommRingCat
φ : R ⟶ S
⊢ ∀ {X Y : Sheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))} (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))).map
          f ≫
        (ObjectProperty.isoMk (Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
            (NatIso.ofComponents
              (fun U ↦
                (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 Y).obj
                        ((Opens.map (Spec.map φ).base).op.obj U))).symm ≪≫
                  (ModuleCat.restrictScalarsComp (CommRingCat.Hom.hom φ) (CommRingCat.Hom.hom (ΓSpecIso S).inv)).app
                    (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj Y).obj
                      ((Opens.map (Spec.map φ).base).op.obj U)))
              ⋯)).hom =
      (ObjectProperty.isoMk (Presheaf.IsSheaf (Opens.grothendieckTopology ↥(Spec R)))
            (NatIso.ofComponents
              (fun U ↦
                (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 X).obj
                        ((Opens.map (Spec.map φ).base).op.obj U))).symm ≪≫
                  (ModuleCat.restrictScalarsComp (CommRingCat.Hom.hom φ) (CommRingCat.Hom.hom (ΓSpecIso S).inv)).app
                    (((sheafToPresheaf (Opens.grothendieckTopology ↥(Spec S)) (ModuleCat ↑Γ(Spec S, ⊤))).obj X).obj
                      ((Opens.map (Spec.map φ).base).op.obj U)))
              ⋯)).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 φ))).map
          f