-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
D' : Type u₃
inst_2 : Category.{v₃, u₃} D'
D'' : Type u₄
inst_3 : Category.{v₄, u₄} D''
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst_4 : F.IsContinuous J K
φ_1 φ ψ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J K) R
e : φ = ψ
X : SheafOfModules.{v, v₂, u₂, u} R
x x_1 : Cᵒᵖ
x_2 : x ⟶ x_1
subst :
  ((forget S).obj ((pushforward φ).obj X)).map x_2 ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (S.obj (P := Presheaf.IsSheaf J).map x_2))).map
        (Iso.hom
          ((fun (U : Cᵒᵖ) ↦
              ((ModuleCat.restrictScalarsCongr ⋯).app
                  ((obj (PresheafOfModules.pushforward₀ F (obj (sheafToPresheaf K RingCat) R)) X.val).obj U) :
                (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app U))).obj
                    ((obj (PresheafOfModules.pushforward₀ F (obj (sheafToPresheaf K RingCat) R)) X.val).obj U) ≅
                  (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app U))).obj
                    ((obj (PresheafOfModules.pushforward₀ F (obj (sheafToPresheaf K RingCat) R)) X.val).obj U)))
            x_1)) =
    Iso.hom
        ((fun (U : Cᵒᵖ) ↦
            ((ModuleCat.restrictScalarsCongr ⋯).app
                ((obj (PresheafOfModules.pushforward₀ F (obj (sheafToPresheaf K RingCat) R)) X.val).obj U) :
              (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app U))).obj
                  ((obj (PresheafOfModules.pushforward₀ F (obj (sheafToPresheaf K RingCat) R)) X.val).obj U) ≅
                (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app U))).obj
                  ((obj (PresheafOfModules.pushforward₀ F (obj (sheafToPresheaf K RingCat) R)) X.val).obj U)))
          x) ≫
      ((forget S).obj ((pushforward φ).obj X)).map x_2
⊢ ((forget S).obj ((pushforward φ).obj X)).map x_2 ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (S.obj (P := Presheaf.IsSheaf J).map x_2))).map
        (Iso.hom
          ((fun (U : Cᵒᵖ) ↦
              ((ModuleCat.restrictScalarsCongr ⋯).app
                  ((obj (PresheafOfModules.pushforward₀ F (obj (sheafToPresheaf K RingCat) R)) X.val).obj U) :
                (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app U))).obj
                    ((obj (PresheafOfModules.pushforward₀ F (obj (sheafToPresheaf K RingCat) R)) X.val).obj U) ≅
                  (ModuleCat.restrictScalars (RingCat.Hom.hom (ψ.hom.app U))).obj
                    ((obj (PresheafOfModules.pushforward₀ F (obj (sheafToPresheaf K RingCat) R)) X.val).obj U)))
            x_1)) =
    Iso.hom
        ((fun (U : Cᵒᵖ) ↦
            ((ModuleCat.restrictScalarsCongr ⋯).app
                ((obj (PresheafOfModules.pushforward₀ F (obj (sheafToPresheaf K RingCat) R)) X.val).obj U) :
              (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app U))).obj
                  ((obj (PresheafOfModules.pushforward₀ F (obj (sheafToPresheaf K RingCat) R)) X.val).obj U) ≅
                (ModuleCat.restrictScalars (RingCat.Hom.hom (ψ.hom.app U))).obj
                  ((obj (PresheafOfModules.pushforward₀ F (obj (sheafToPresheaf K RingCat) R)) X.val).obj U)))
          x) ≫
      ((forget S).obj ((pushforward ψ).obj X)).map x_2

Tactic:
subst e