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

Goal state before:
pp: case 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)
⊢ ∀ {X_1 Y : SheafOfModules R} (f : X_1 ⟶ Y),
    (pushforward φ ⋙ forgetToSheafModuleCat S X hX).map f ≫
        (ObjectProperty.isoMk (Presheaf.IsSheaf J)
            (NatIso.ofComponents
              (fun U ↦
                (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (S.obj.map (hX.to U)))
                      (RingCat.Hom.hom (φ.hom.app U))
                      ((RingCat.Hom.hom (R.obj.map (hX'.to (F.op.obj U)))).comp (RingCat.Hom.hom (φ.hom.app X))) ⋯
                      (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj Y.val).obj
                        U)).symm ≪≫
                  (ModuleCat.restrictScalarsComp (RingCat.Hom.hom (φ.hom.app X))
                        (RingCat.Hom.hom (R.obj.map (hX'.to (F.op.obj U))))).app
                    (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj Y.val).obj U))
              ⋯)).hom =
      (ObjectProperty.isoMk (Presheaf.IsSheaf J)
            (NatIso.ofComponents
              (fun U ↦
                (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (S.obj.map (hX.to U)))
                      (RingCat.Hom.hom (φ.hom.app U))
                      ((RingCat.Hom.hom (R.obj.map (hX'.to (F.op.obj U)))).comp (RingCat.Hom.hom (φ.hom.app X))) ⋯
                      (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj X_1.val).obj
                        U)).symm ≪≫
                  (ModuleCat.restrictScalarsComp (RingCat.Hom.hom (φ.hom.app X))
                        (RingCat.Hom.hom (R.obj.map (hX'.to (F.op.obj U))))).app
                    (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj X_1.val).obj U))
              ⋯)).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).map
          f

Tactic:
·

Goal state after:
case 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)
⊢ ∀ {X_1 Y : SheafOfModules R} (f : X_1 ⟶ Y),
    (pushforward φ ⋙ forgetToSheafModuleCat S X hX).map f ≫
        (ObjectProperty.isoMk (Presheaf.IsSheaf J)
            (NatIso.ofComponents
              (fun U ↦
                (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (S.obj.map (hX.to U)))
                      (RingCat.Hom.hom (φ.hom.app U))
                      ((RingCat.Hom.hom (R.obj.map (hX'.to (F.op.obj U)))).comp (RingCat.Hom.hom (φ.hom.app X))) ⋯
                      (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj Y.val).obj
                        U)).symm ≪≫
                  (ModuleCat.restrictScalarsComp (RingCat.Hom.hom (φ.hom.app X))
                        (RingCat.Hom.hom (R.obj.map (hX'.to (F.op.obj U))))).app
                    (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj Y.val).obj U))
              ⋯)).hom =
      (ObjectProperty.isoMk (Presheaf.IsSheaf J)
            (NatIso.ofComponents
              (fun U ↦
                (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (S.obj.map (hX.to U)))
                      (RingCat.Hom.hom (φ.hom.app U))
                      ((RingCat.Hom.hom (R.obj.map (hX'.to (F.op.obj U)))).comp (RingCat.Hom.hom (φ.hom.app X))) ⋯
                      (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj X_1.val).obj
                        U)).symm ≪≫
                  (ModuleCat.restrictScalarsComp (RingCat.Hom.hom (φ.hom.app X))
                        (RingCat.Hom.hom (R.obj.map (hX'.to (F.op.obj U))))).app
                    (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj X_1.val).obj U))
              ⋯)).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).map
          f