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:
·

Goal state after:
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