awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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_2 : F.IsContinuous J K
φ ψ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J K) R
e : φ = ψ
M : SheafOfModules.{u_1, v₂, u₂, u} R
U : Cᵒᵖ
x : (↑(((pushforward φ).obj M).val.obj U) : Type u_1)
⊢ (@ConcreteCategory.hom _ (ModuleCat.moduleCategory (↑(S.obj (P := Presheaf.IsSheaf J).obj U) : Type u))
          (fun (x1 x2 : ModuleCat.{u_1, u} (↑(S.obj (P := Presheaf.IsSheaf J).obj U) : Type u)) ↦
            LinearMap.{u, u, u_1, u_1} (R := (↑(S.obj (P := Presheaf.IsSheaf J).obj U) : Type u))
              (RingHom.id (↑(S.obj (P := Presheaf.IsSheaf J).obj U) : Type u)) (↑x1 : Type u_1) (↑x2 : Type u_1))
          ModuleCat.carrier
          (fun (X Y : ModuleCat.{u_1, u} (↑(S.obj (P := Presheaf.IsSheaf J).obj U) : Type u)) ↦
            (LinearMap.instFunLike :
              FunLike
                (LinearMap.{u, u, u_1, u_1} (R := (↑(S.obj (P := Presheaf.IsSheaf J).obj U) : Type u))
                  (RingHom.id (↑(S.obj (P := Presheaf.IsSheaf J).obj U) : Type u)) (↑X : Type u_1) (↑Y : Type u_1))
                (↑X : Type u_1) (↑Y : Type u_1)))
          _ _ _ (((pushforwardCongr e).hom.app M).val.app U) :
        (a : (↑(((pushforward φ).obj M).val.obj U) : Type u_1)) → (↑(((pushforward ψ).obj M).val.obj U) : Type u_1))
      x =
    x

Tactic:
rfl

Premises used: rfl
-- 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
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_2 : F.IsContinuous J K
φ ψ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J K) R
e : φ = ψ
M : SheafOfModules.{u_1, v₂, u₂, u} R
U : Cᵒᵖ
x : (↑(((pushforward ψ).obj M).val.obj U) : Type u_1)
⊢ (@ConcreteCategory.hom _ (ModuleCat.moduleCategory (↑(S.obj (P := Presheaf.IsSheaf J).obj U) : Type u))
          (fun (x1 x2 : ModuleCat.{u_1, u} (↑(S.obj (P := Presheaf.IsSheaf J).obj U) : Type u)) ↦
            LinearMap.{u, u, u_1, u_1} (R := (↑(S.obj (P := Presheaf.IsSheaf J).obj U) : Type u))
              (RingHom.id (↑(S.obj (P := Presheaf.IsSheaf J).obj U) : Type u)) (↑x1 : Type u_1) (↑x2 : Type u_1))
          ModuleCat.carrier
          (fun (X Y : ModuleCat.{u_1, u} (↑(S.obj (P := Presheaf.IsSheaf J).obj U) : Type u)) ↦
            (LinearMap.instFunLike :
              FunLike
                (LinearMap.{u, u, u_1, u_1} (R := (↑(S.obj (P := Presheaf.IsSheaf J).obj U) : Type u))
                  (RingHom.id (↑(S.obj (P := Presheaf.IsSheaf J).obj U) : Type u)) (↑X : Type u_1) (↑Y : Type u_1))
                (↑X : Type u_1) (↑Y : Type u_1)))
          _ _ _ (((pushforwardCongr e).inv.app M).val.app U) :
        (a : (↑(((pushforward ψ).obj M).val.obj U) : Type u_1)) → (↑(((pushforward φ).obj M).val.obj U) : Type u_1))
      x =
    x

Tactic:
rfl

Premises used: rfl
-- 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'
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_3 : F.IsContinuous J K
φ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J K) R
K' : GrothendieckTopology.{v₃, u₃} D'
G : CategoryTheory.Functor.{v₂, v₃, u₂, u₃} D D'
R' : Sheaf K' RingCat
inst_4 : G.IsContinuous K K'
inst_5 : (F ⋙ G).IsContinuous J K'
ψ : R ⟶ obj (G.sheafPushforwardContinuous RingCat K K') R'
M : SheafOfModules.{u_1, v₃, u₃, u} R'
U : Cᵒᵖ
x : (↑(((pushforward ψ ⋙ pushforward φ).obj M).val.obj U) : Type u_1)
⊢ (@ConcreteCategory.hom _ (ModuleCat.moduleCategory (↑(S.obj (P := Presheaf.IsSheaf J).obj U) : Type u))
          (fun (x1 x2 : ModuleCat.{u_1, u} (↑(S.obj (P := Presheaf.IsSheaf J).obj U) : Type u)) ↦
            LinearMap.{u, u, u_1, u_1} (R := (↑(S.obj (P := Presheaf.IsSheaf J).obj U) : Type u))
              (RingHom.id (↑(S.obj (P := Presheaf.IsSheaf J).obj U) : Type u)) (↑x1 : Type u_1) (↑x2 : Type u_1))
          ModuleCat.carrier
          (fun (X Y : ModuleCat.{u_1, u} (↑(S.obj (P := Presheaf.IsSheaf J).obj U) : Type u)) ↦
            (LinearMap.instFunLike :
              FunLike
                (LinearMap.{u, u, u_1, u_1} (R := (↑(S.obj (P := Presheaf.IsSheaf J).obj U) : Type u))
                  (RingHom.id (↑(S.obj (P := Presheaf.IsSheaf J).obj U) : Type u)) (↑X : Type u_1) (↑Y : Type u_1))
                (↑X : Type u_1) (↑Y : Type u_1)))
          _ _ _
          (PresheafOfModules.Hom.app (Hom.val (NatTrans.app (Iso.hom (pushforwardComp φ ψ)) M)) U :
            ((pushforward ψ ⋙ pushforward φ).obj M).val.obj U ⟶
              ((pushforward (φ ≫ CategoryTheory.Functor.map (F.sheafPushforwardContinuous RingCat J K) ψ)).obj
                      M).val.obj
                U) :
        (a : (↑(((pushforward ψ ⋙ pushforward φ).obj M).val.obj U) : Type u_1)) →
          (↑(((pushforward (φ ≫ (F.sheafPushforwardContinuous RingCat J K).map ψ)).obj M).val.obj U) : Type u_1))
      x =
    x

Tactic:
rfl

Premises used: rfl
-- 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'
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_3 : F.IsContinuous J K
φ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J K) R
K' : GrothendieckTopology.{v₃, u₃} D'
G : CategoryTheory.Functor.{v₂, v₃, u₂, u₃} D D'
R' : Sheaf K' RingCat
inst_4 : G.IsContinuous K K'
inst_5 : (F ⋙ G).IsContinuous J K'
ψ : R ⟶ obj (G.sheafPushforwardContinuous RingCat K K') R'
M : SheafOfModules.{u_1, v₃, u₃, u} R'
U : Cᵒᵖ
x :
  (↑(((pushforward (φ ≫ CategoryTheory.Functor.map (F.sheafPushforwardContinuous RingCat J K) ψ)).obj M).val.obj U) :
    Type u_1)
⊢ (@ConcreteCategory.hom _ (ModuleCat.moduleCategory (↑(S.obj (P := Presheaf.IsSheaf J).obj U) : Type u))
          (fun (x1 x2 : ModuleCat.{u_1, u} (↑(S.obj (P := Presheaf.IsSheaf J).obj U) : Type u)) ↦
            LinearMap.{u, u, u_1, u_1} (R := (↑(S.obj (P := Presheaf.IsSheaf J).obj U) : Type u))
              (RingHom.id (↑(S.obj (P := Presheaf.IsSheaf J).obj U) : Type u)) (↑x1 : Type u_1) (↑x2 : Type u_1))
          ModuleCat.carrier
          (fun (X Y : ModuleCat.{u_1, u} (↑(S.obj (P := Presheaf.IsSheaf J).obj U) : Type u)) ↦
            (LinearMap.instFunLike :
              FunLike
                (LinearMap.{u, u, u_1, u_1} (R := (↑(S.obj (P := Presheaf.IsSheaf J).obj U) : Type u))
                  (RingHom.id (↑(S.obj (P := Presheaf.IsSheaf J).obj U) : Type u)) (↑X : Type u_1) (↑Y : Type u_1))
                (↑X : Type u_1) (↑Y : Type u_1)))
          _ _ _
          (PresheafOfModules.Hom.app (Hom.val (NatTrans.app (Iso.inv (pushforwardComp φ ψ)) M)) U :
            ((pushforward (φ ≫ CategoryTheory.Functor.map (F.sheafPushforwardContinuous RingCat J K) ψ)).obj M).val.obj
                U ⟶
              ((pushforward ψ ⋙ pushforward φ).obj M).val.obj U) :
        (a : (↑(((pushforward (φ ≫ (F.sheafPushforwardContinuous RingCat J K).map ψ)).obj M).val.obj U) : Type u_1)) →
          (↑(((pushforward ψ ⋙ pushforward φ).obj M).val.obj U) : Type u_1))
      x =
    x

Tactic:
rfl

Premises used: rfl
-- 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
φ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J K) R
K' : GrothendieckTopology.{v₃, u₃} D'
K'' : GrothendieckTopology.{v₄, u₄} D''
G : CategoryTheory.Functor.{v₂, v₃, u₂, u₃} D D'
R' : Sheaf K' RingCat
inst_5 : G.IsContinuous K K'
inst_6 : (F ⋙ G).IsContinuous J K'
ψ : R ⟶ obj (G.sheafPushforwardContinuous RingCat K K') R'
G' : CategoryTheory.Functor.{v₃, v₄, u₃, u₄} D' D''
R'' : Sheaf K'' RingCat
inst_7 : G'.IsContinuous K' K''
inst_8 : (G ⋙ G').IsContinuous K K''
inst_9 : ((F ⋙ G) ⋙ G').IsContinuous J K''
inst_10 : (F ⋙ G ⋙ G').IsContinuous J K''
ψ' : R' ⟶ obj (G'.sheafPushforwardContinuous RingCat K' K'') R''
w : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext
-- 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
φ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J K) R
K' : GrothendieckTopology.{v₃, u₃} D'
K'' : GrothendieckTopology.{v₄, u₄} D''
G : CategoryTheory.Functor.{v₂, v₃, u₂, u₃} D D'
R' : Sheaf K' RingCat
inst_5 : G.IsContinuous K K'
inst_6 : (F ⋙ G).IsContinuous J K'
ψ : R ⟶ obj (G.sheafPushforwardContinuous RingCat K K') R'
G' : CategoryTheory.Functor.{v₃, v₄, u₃, u₄} D' D''
R'' : Sheaf K'' RingCat
inst_7 : G'.IsContinuous K' K''
inst_8 : (G ⋙ G').IsContinuous K K''
inst_9 : ((F ⋙ G) ⋙ G').IsContinuous J K''
inst_10 : (F ⋙ G ⋙ G').IsContinuous J K''
ψ' : R' ⟶ obj (G'.sheafPushforwardContinuous RingCat K' K'') R''
x : SheafOfModules.{u_1, v₄, u₄, u} R''
X : Cᵒᵖ
x_1 : (↑(((pushforward ψ' ⋙ pushforward ψ ⋙ pushforward φ).obj x).val.obj X) : Type u_1)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rfl
-- 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
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_2 : F.IsContinuous J K
φ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J K) R
w :
  ∀ (x : SheafOfModules.{v, v₂, u₂, u} R) (X : Cᵒᵖ)
    (x_1 : (↑(PresheafOfModules.obj (val (obj (pushforward φ ⋙ pushforward (F := 𝟭 C) (𝟙 S)) x)) X) : Type v)),
    Eq (α :=
      (↑((obj
                  (pushforward (F := 𝟭 C ⋙ F)
                    (𝟙 S ≫ CategoryTheory.Functor.map (sheafPushforwardContinuous (𝟭 C) RingCat J J) φ))
                  x).val.obj
            X) :
        Type v))
      ((ModuleCat.Hom.hom (PresheafOfModules.Hom.app (Hom.val (NatTrans.app (Iso.hom (pushforwardComp (𝟙 S) φ)) x)) X) :
            (a : (↑(((pushforward φ ⋙ pushforward (𝟙 S)).obj x).val.obj X) : Type v)) →
              (↑(((pushforward (𝟙 S ≫ ((𝟭 C).sheafPushforwardContinuous RingCat J J).map φ)).obj x).val.obj X) :
                Type v))
          x_1 :
        (↑((obj
                    (pushforward (F := 𝟭 C ⋙ F)
                      (𝟙 S ≫ CategoryTheory.Functor.map (sheafPushforwardContinuous (𝟭 C) RingCat J J) φ))
                    x).val.obj
              X) :
          Type v))
      ((ModuleCat.Hom.hom
              ((((pushforward φ).isoWhiskerLeft (pushforwardId S) ≪≫ (pushforward φ).rightUnitor).hom.app x).val.app
                X) :
            (a : (↑(((pushforward φ ⋙ pushforward (𝟙 S)).obj x).val.obj X) : Type v)) →
              (↑(((pushforward (𝟙 S ≫ ((𝟭 C).sheafPushforwardContinuous RingCat J J).map φ)).obj x).val.obj X) :
                Type v))
          x_1 :
        (↑((obj
                    (pushforward (F := 𝟭 C ⋙ F)
                      (𝟙 S ≫ CategoryTheory.Functor.map (sheafPushforwardContinuous (𝟭 C) RingCat J J) φ))
                    x).val.obj
              X) :
          Type v))
⊢ pushforwardComp (𝟙 S) φ = (pushforward φ).isoWhiskerLeft (pushforwardId S) ≪≫ (pushforward φ).rightUnitor

Tactic:
ext
-- 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
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_2 : F.IsContinuous J K
φ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J K) R
x : SheafOfModules.{v, v₂, u₂, u} R
X : Cᵒᵖ
x_1 : (↑(PresheafOfModules.obj (val (obj (pushforward φ ⋙ pushforward (F := 𝟭 C) (𝟙 S)) x)) X) : Type v)
⊢ Eq (α :=
    (↑((obj
                (pushforward (F := 𝟭 C ⋙ F)
                  (𝟙 S ≫ CategoryTheory.Functor.map (sheafPushforwardContinuous (𝟭 C) RingCat J J) φ))
                x).val.obj
          X) :
      Type v))
    ((ModuleCat.Hom.hom (PresheafOfModules.Hom.app (Hom.val (NatTrans.app (Iso.hom (pushforwardComp (𝟙 S) φ)) x)) X) :
          (a : (↑(((pushforward φ ⋙ pushforward (𝟙 S)).obj x).val.obj X) : Type v)) →
            (↑(((pushforward (𝟙 S ≫ ((𝟭 C).sheafPushforwardContinuous RingCat J J).map φ)).obj x).val.obj X) : Type v))
        x_1 :
      (↑((obj
                  (pushforward (F := 𝟭 C ⋙ F)
                    (𝟙 S ≫ CategoryTheory.Functor.map (sheafPushforwardContinuous (𝟭 C) RingCat J J) φ))
                  x).val.obj
            X) :
        Type v))
    ((ModuleCat.Hom.hom
            ((((pushforward φ).isoWhiskerLeft (pushforwardId S) ≪≫ (pushforward φ).rightUnitor).hom.app x).val.app X) :
          (a : (↑(((pushforward φ ⋙ pushforward (𝟙 S)).obj x).val.obj X) : Type v)) →
            (↑(((pushforward (𝟙 S ≫ ((𝟭 C).sheafPushforwardContinuous RingCat J J).map φ)).obj x).val.obj X) : Type v))
        x_1 :
      (↑((obj
                  (pushforward (F := 𝟭 C ⋙ F)
                    (𝟙 S ≫ CategoryTheory.Functor.map (sheafPushforwardContinuous (𝟭 C) RingCat J J) φ))
                  x).val.obj
            X) :
        Type v))

Tactic:
rfl
-- 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
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_2 : F.IsContinuous J K
φ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J K) R
w :
  ∀ (x : SheafOfModules.{v, v₂, u₂, u} R) (X : Cᵒᵖ)
    (x_1 : (↑((obj (pushforward (F := 𝟭 D) (𝟙 R) ⋙ pushforward φ) x).val.obj X) : Type v)),
    Eq (α :=
      (↑(((pushforward (φ ≫ CategoryTheory.Functor.map (F.sheafPushforwardContinuous RingCat J K) (𝟙 R))).obj x).val.obj
            X) :
        Type v))
      ((ModuleCat.Hom.hom (PresheafOfModules.Hom.app (Hom.val (NatTrans.app (Iso.hom (pushforwardComp φ (𝟙 R))) x)) X) :
            (a : (↑(((pushforward (𝟙 R) ⋙ pushforward φ).obj x).val.obj X) : Type v)) →
              (↑(((pushforward (φ ≫ (F.sheafPushforwardContinuous RingCat J K).map (𝟙 R))).obj x).val.obj X) : Type v))
          x_1 :
        (↑(((pushforward (φ ≫ CategoryTheory.Functor.map (F.sheafPushforwardContinuous RingCat J K) (𝟙 R))).obj
                    x).val.obj
              X) :
          Type v))
      ((ModuleCat.Hom.hom
              (((isoWhiskerRight (pushforwardId R) (pushforward φ) ≪≫ (pushforward φ).leftUnitor).hom.app x).val.app
                X) :
            (a : (↑(((pushforward (𝟙 R) ⋙ pushforward φ).obj x).val.obj X) : Type v)) →
              (↑(((pushforward (φ ≫ (F.sheafPushforwardContinuous RingCat J K).map (𝟙 R))).obj x).val.obj X) : Type v))
          x_1 :
        (↑(((pushforward (φ ≫ CategoryTheory.Functor.map (F.sheafPushforwardContinuous RingCat J K) (𝟙 R))).obj
                    x).val.obj
              X) :
          Type v))
⊢ pushforwardComp φ (𝟙 R) = isoWhiskerRight (pushforwardId R) (pushforward φ) ≪≫ (pushforward φ).leftUnitor

Tactic:
ext
-- 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
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_2 : F.IsContinuous J K
φ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J K) R
x : SheafOfModules.{v, v₂, u₂, u} R
X : Cᵒᵖ
x_1 : (↑((obj (pushforward (F := 𝟭 D) (𝟙 R) ⋙ pushforward φ) x).val.obj X) : Type v)
⊢ Eq (α :=
    (↑(((pushforward (φ ≫ CategoryTheory.Functor.map (F.sheafPushforwardContinuous RingCat J K) (𝟙 R))).obj x).val.obj
          X) :
      Type v))
    ((ModuleCat.Hom.hom (PresheafOfModules.Hom.app (Hom.val (NatTrans.app (Iso.hom (pushforwardComp φ (𝟙 R))) x)) X) :
          (a : (↑(((pushforward (𝟙 R) ⋙ pushforward φ).obj x).val.obj X) : Type v)) →
            (↑(((pushforward (φ ≫ (F.sheafPushforwardContinuous RingCat J K).map (𝟙 R))).obj x).val.obj X) : Type v))
        x_1 :
      (↑(((pushforward (φ ≫ CategoryTheory.Functor.map (F.sheafPushforwardContinuous RingCat J K) (𝟙 R))).obj x).val.obj
            X) :
        Type v))
    ((ModuleCat.Hom.hom
            (((isoWhiskerRight (pushforwardId R) (pushforward φ) ≪≫ (pushforward φ).leftUnitor).hom.app x).val.app X) :
          (a : (↑(((pushforward (𝟙 R) ⋙ pushforward φ).obj x).val.obj X) : Type v)) →
            (↑(((pushforward (φ ≫ (F.sheafPushforwardContinuous RingCat J K).map (𝟙 R))).obj x).val.obj X) : Type v))
        x_1 :
      (↑(((pushforward (φ ≫ CategoryTheory.Functor.map (F.sheafPushforwardContinuous RingCat J K) (𝟙 R))).obj x).val.obj
            X) :
        Type v))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
D' : Type u₃
inst_2 : Category.{v₃, u₃} D'
D'' : Type u₄
inst_3 : Category.{v₄, u₄} D''
J_1 : GrothendieckTopology.{v₁, u₁} C_1
K_1 : GrothendieckTopology.{v₂, u₂} D_1
F_1 : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C_1 D_1
S_1 : Sheaf J_1 RingCat
R : Sheaf K_1 RingCat
inst_4 : F_1.IsContinuous J_1 K_1
φ_1 : S_1 ⟶ obj (F_1.sheafPushforwardContinuous RingCat J_1 K_1) R
C : Type u₁
inst_5 : Category.{v₁, u₁} C
D : Type u₂
inst_6 : Category.{v₂, u₂} D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
F G H : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
T : Sheaf J RingCat
S : Sheaf K RingCat
inst_7 : F.IsContinuous J K
inst_8 : G.IsContinuous J K
inst_9 : H.IsContinuous J K
φ : T ⟶ obj (G.sheafPushforwardContinuous RingCat J K) S
α : F ⟶ G
X : SheafOfModules.{v, v₂, u₂, u} S
U V : Cᵒᵖ
i : U ⟶ V
x : (↑(((pushforward φ).obj X).val.obj U) : Type v)
⊢ Eq (α := (↑(X.val.presheaf.obj (Opposite.op (F.obj (Opposite.unop V)))) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier)
            (X.val.presheaf.map (G.map i.unop).op ≫ X.val.presheaf.map (Quiver.Hom.op (α.app (Opposite.unop V)))) :
          (a : (↑(X.val.presheaf.obj (Opposite.op (G.obj (Opposite.unop U)))) : Type v)) →
            (↑(X.val.presheaf.obj (Opposite.op (F.obj (Opposite.unop V)))) : Type v))
        x :
      (↑(X.val.presheaf.obj (Opposite.op (F.obj (Opposite.unop V)))) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier)
            (X.val.presheaf.map (Quiver.Hom.op (α.app (Opposite.unop U))) ≫ X.val.presheaf.map (F.map i.unop).op) :
          (a : (↑(X.val.presheaf.obj (Opposite.op (G.obj (Opposite.unop U)))) : Type v)) →
            (↑(X.val.presheaf.obj (Opposite.op (F.obj (Opposite.unop V)))) : Type v))
        x :
      (↑(X.val.presheaf.obj (Opposite.op (F.obj (Opposite.unop V)))) : Type v))

Tactic:
simp only [← CategoryTheory.Functor.map_comp, ← op_comp, α.naturality]

Premises used: CategoryTheory.op_comp, CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
D_1 : Type u₂
inst_1 : Category.{v₂, u₂} D_1
D' : Type u₃
inst_2 : Category.{v₃, u₃} D'
D'' : Type u₄
inst_3 : Category.{v₄, u₄} D''
J_1 : GrothendieckTopology.{v₁, u₁} C_1
K_1 : GrothendieckTopology.{v₂, u₂} D_1
F_1 : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C_1 D_1
S_1 : Sheaf J_1 RingCat
R : Sheaf K_1 RingCat
inst_4 : F_1.IsContinuous J_1 K_1
φ_1 : S_1 ⟶ obj (F_1.sheafPushforwardContinuous RingCat J_1 K_1) R
C : Type u₁
inst_5 : Category.{v₁, u₁} C
D : Type u₂
inst_6 : Category.{v₂, u₂} D
J : GrothendieckTopology.{v₁, u₁} C
K : GrothendieckTopology.{v₂, u₂} D
F G H : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
T : Sheaf J RingCat
S : Sheaf K RingCat
inst_7 : F.IsContinuous J K
inst_8 : G.IsContinuous J K
inst_9 : H.IsContinuous J K
φ : T ⟶ obj (G.sheafPushforwardContinuous RingCat J K) S
α : F ⟶ G
X Y : SheafOfModules.{v, v₂, u₂, u} S
f : X ⟶ Y
U : Cᵒᵖ
x : (↑(((pushforward φ).obj X).val.obj U) : Type v)
⊢ Eq (α :=
    (↑(((pushforward (φ ≫ NatTrans.app (sheafPushforwardContinuousNatTrans α RingCat J K) S)).obj Y).val.obj U) :
      Type v))
    ((ModuleCat.Hom.hom
            (PresheafOfModules.Hom.app
              (Hom.val
                ((pushforward φ).map f ≫
                  {
                    val :=
                      {
                        app := fun (U : Cᵒᵖ) ↦
                          (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app U))).map
                            (Y.val.map (Quiver.Hom.op (α.app (Opposite.unop U)))),
                        naturality := ⋯ } }))
              U) :
          (a : (↑(((pushforward φ).obj X).val.obj U) : Type v)) →
            (↑(((pushforward (φ ≫ (sheafPushforwardContinuousNatTrans α RingCat J K).app S)).obj Y).val.obj U) :
              Type v))
        x :
      (↑(((pushforward (φ ≫ NatTrans.app (sheafPushforwardContinuousNatTrans α RingCat J K) S)).obj Y).val.obj U) :
        Type v))
    ((ModuleCat.Hom.hom
            (PresheafOfModules.Hom.app
              (Hom.val
                ({
                    val :=
                      {
                        app := fun (U : Cᵒᵖ) ↦
                          (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app U))).map
                            (X.val.map (Quiver.Hom.op (α.app (Opposite.unop U)))),
                        naturality := ⋯ } } ≫
                  (pushforward (φ ≫ NatTrans.app (sheafPushforwardContinuousNatTrans α RingCat J K) S)).map f))
              U) :
          (a : (↑(((pushforward φ).obj X).val.obj U) : Type v)) →
            (↑(((pushforward (φ ≫ (sheafPushforwardContinuousNatTrans α RingCat J K).app S)).obj Y).val.obj U) :
              Type v))
        x :
      (↑(((pushforward (φ ≫ NatTrans.app (sheafPushforwardContinuousNatTrans α RingCat J K) S)).obj Y).val.obj U) :
        Type v))

Tactic:
congr($(f.val.naturality (α.app U.unop).op) x).symm

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, id, SheafOfModules.Hom.val, PresheafOfModules.Hom.naturality, Eq.symm, DFunLike.coe, Opposite.unop, CategoryTheory.NatTrans.app