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

Goal state before:
pp: case 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
⊢ ((pushforward φ ⋙ forgetToSheafModuleCat S X hX).obj M).obj ≅
    ((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

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) ?refine_1).hom =
      (ObjectProperty.isoMk (Presheaf.IsSheaf J) ?refine_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).map
          f

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

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