Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Goal state before:
pp: case refine_1.refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
D' : Type u₃
inst✝² : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝¹ : Category.{v₄, u₄} D''
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝ : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
X : Cᵒᵖ
hX : IsInitial X
hX' : IsInitial (F.op.obj X)
M : SheafOfModules R
U : Cᵒᵖ
⊢ ((pushforward φ ⋙ forgetToSheafModuleCat S X hX).obj M).obj.obj U ≅
    ((forgetToSheafModuleCat R (F.op.obj X) hX' ⋙
                sheafCompose K (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app X))) ⋙
                  F.sheafPushforwardContinuous (ModuleCat ↑(S.obj.obj X)) J K).obj
            M).obj.obj
      U

pp: case refine_1.refine_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
D' : Type u₃
inst✝² : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝¹ : Category.{v₄, u₄} D''
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝ : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
X : Cᵒᵖ
hX : IsInitial X
hX' : IsInitial (F.op.obj X)
M : SheafOfModules R
⊢ ∀ {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y),
    ((pushforward φ ⋙ forgetToSheafModuleCat S X hX).obj M).obj.map f ≫ Iso.hom ?refine_1.refine_1 =
      Iso.hom ?refine_1.refine_1 ≫
        ((forgetToSheafModuleCat R (F.op.obj X) hX' ⋙
                    sheafCompose K (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app X))) ⋙
                      F.sheafPushforwardContinuous (ModuleCat ↑(S.obj.obj X)) J K).obj
                M).obj.map
          f

Tactic:
· refine (ModuleCat.restrictScalarsComp'App _ _ _ ?_ _).symm ≪≫
        (ModuleCat.restrictScalarsComp _ _).app _
      rw [← RingCat.hom_comp, ← RingCat.hom_comp, φ.hom.naturality]
      dsimp
      rw [hX'.hom_ext (hX'.to (Opposite.op (F.obj (Opposite.unop U)))) _]

Goal state after:
case refine_1.refine_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
D' : Type u₃
inst✝² : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝¹ : Category.{v₄, u₄} D''
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝ : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
X : Cᵒᵖ
hX : IsInitial X
hX' : IsInitial (F.op.obj X)
M : SheafOfModules R
⊢ ∀ {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y),
    ((pushforward φ ⋙ forgetToSheafModuleCat S X hX).obj M).obj.map f ≫
        ((ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (S.obj.map (hX.to Y))) (RingCat.Hom.hom (φ.hom.app Y))
                ((RingCat.Hom.hom (R.obj.map (hX'.to (F.op.obj Y)))).comp (RingCat.Hom.hom (φ.hom.app X))) ⋯
                (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj M.val).obj Y)).symm ≪≫
            (ModuleCat.restrictScalarsComp (RingCat.Hom.hom (φ.hom.app X))
                  (RingCat.Hom.hom (R.obj.map (hX'.to (F.op.obj Y))))).app
              (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj M.val).obj Y)).hom =
      ((ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (S.obj.map (hX.to X_1))) (RingCat.Hom.hom (φ.hom.app X_1))
                ((RingCat.Hom.hom (R.obj.map (hX'.to (F.op.obj X_1)))).comp (RingCat.Hom.hom (φ.hom.app X))) ⋯
                (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj M.val).obj X_1)).symm ≪≫
            (ModuleCat.restrictScalarsComp (RingCat.Hom.hom (φ.hom.app X))
                  (RingCat.Hom.hom (R.obj.map (hX'.to (F.op.obj X_1))))).app
              (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj M.val).obj X_1)).hom ≫
        ((forgetToSheafModuleCat R (F.op.obj X) hX' ⋙
                    sheafCompose K (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app X))) ⋙
                      F.sheafPushforwardContinuous (ModuleCat ↑(S.obj.obj X)) J K).obj
                M).obj.map
          f