awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact 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
-- 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 G : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
T : Sheaf J RingCat
S : Sheaf K RingCat
inst_2 : F.IsContinuous J K
inst_3 : G.IsContinuous J K
φ : T ⟶ obj (G.sheafPushforwardContinuous RingCat J K) S
α : F ⟶ G
M : SheafOfModules.{u_1, v₂, u₂, u} S
U : Cᵒᵖ
x : (↑(((pushforward φ).obj M).val.obj U) : Type u_1)
⊢ Eq (α :=
    (↑(((pushforward (φ ≫ NatTrans.app (sheafPushforwardContinuousNatTrans α RingCat J K) S)).obj M).val.obj U) :
      Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_1, u} (↑(T.obj (P := Presheaf.IsSheaf J).obj U) : Type u)) ↦
            LinearMap.{u, u, u_1, u_1} (R := (↑(T.obj (P := Presheaf.IsSheaf J).obj U) : Type u))
              (RingHom.id (↑(T.obj (P := Presheaf.IsSheaf J).obj U) : Type u)) (↑x1 : Type u_1) (↑x2 : Type u_1))
            (CC := ModuleCat.carrier) (Y :=
            ((pushforward (φ ≫ NatTrans.app (sheafPushforwardContinuousNatTrans α RingCat J K) S)).obj M).val.obj U)
            (PresheafOfModules.Hom.app (Hom.val (NatTrans.app (pushforwardNatTrans φ α) M)) U) :
          (a : (↑(((pushforward φ).obj M).val.obj U) : Type u_1)) →
            (↑(((pushforward (φ ≫ (sheafPushforwardContinuousNatTrans α RingCat J K).app S)).obj M).val.obj U) :
              Type u_1))
        x :
      (↑(((pushforward (φ ≫ NatTrans.app (sheafPushforwardContinuousNatTrans α RingCat J K) S)).obj M).val.obj U) :
        Type u_1))
    ((ConcreteCategory.hom (FC :=
            fun
              (x1 x2 :
                ModuleCat.{u_1, u}
                  (↑(S.obj (P := Presheaf.IsSheaf K).obj (Opposite.op (G.obj (Opposite.unop U)))) : Type u)) ↦
            LinearMap.{u, u, u_1, u_1} (R :=
              (↑(S.obj (P := Presheaf.IsSheaf K).obj (Opposite.op (G.obj (Opposite.unop U)))) : Type u))
              (RingHom.id (↑(S.obj (P := Presheaf.IsSheaf K).obj (Opposite.op (G.obj (Opposite.unop U)))) : Type u))
              (↑x1 : Type u_1) (↑x2 : Type u_1))
            (CC := ModuleCat.carrier) (Y :=
            obj
              (ModuleCat.restrictScalars
                (RingCat.Hom.hom (S.obj (P := Presheaf.IsSheaf K).map (Quiver.Hom.op (α.app (Opposite.unop U))))))
              (M.val.obj (Opposite.op (F.obj (Opposite.unop U)))))
            (M.val.map (Quiver.Hom.op (α.app (Opposite.unop U)))) :
          (a : (↑(M.val.obj (Opposite.op (G.obj (Opposite.unop U)))) : Type u_1)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (S.obj.map (α.app (Opposite.unop U)).op))).obj
                  (M.val.obj (Opposite.op (F.obj (Opposite.unop U))))) :
              Type u_1))
        x :
      (↑(obj
            (ModuleCat.restrictScalars
              (RingCat.Hom.hom (S.obj (P := Presheaf.IsSheaf K).map (Quiver.Hom.op (α.app (Opposite.unop U))))))
            (M.val.obj (Opposite.op (F.obj (Opposite.unop U))))) :
        Type u_1))

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 G : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
T : Sheaf J RingCat
S : Sheaf K RingCat
inst_2 : F.IsContinuous J K
inst_3 : G.IsContinuous J K
φ : T ⟶ obj (G.sheafPushforwardContinuous RingCat J K) S
α : F ⟶ G
X : SheafOfModules.{u_1, v₂, u₂, u} S
U : Cᵒᵖ
x : (↑(((pushforward φ).obj X).val.obj U) : Type u_1)
⊢ Eq (α :=
    (↑(((pushforward (φ ≫ NatTrans.app (sheafPushforwardContinuousNatTrans α RingCat J K) S)).obj X).val.obj U) :
      Type u_1))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{u_1, u} (↑(T.obj (P := Presheaf.IsSheaf J).obj U) : Type u)) ↦
            LinearMap.{u, u, u_1, u_1} (R := (↑(T.obj (P := Presheaf.IsSheaf J).obj U) : Type u))
              (RingHom.id (↑(T.obj (P := Presheaf.IsSheaf J).obj U) : Type u)) (↑x1 : Type u_1) (↑x2 : Type u_1))
            (CC := ModuleCat.carrier) (Y :=
            ((pushforward (φ ≫ NatTrans.app (sheafPushforwardContinuousNatTrans α RingCat J K) S)).obj X).val.obj U)
            (PresheafOfModules.Hom.app (Hom.val (NatTrans.app (pushforwardNatTrans φ α) X)) U) :
          (a : (↑(((pushforward φ).obj X).val.obj U) : Type u_1)) →
            (↑(((pushforward (φ ≫ (sheafPushforwardContinuousNatTrans α RingCat J K).app S)).obj X).val.obj U) :
              Type u_1))
        x :
      (↑(((pushforward (φ ≫ NatTrans.app (sheafPushforwardContinuousNatTrans α RingCat J K) S)).obj X).val.obj U) :
        Type u_1))
    ((ConcreteCategory.hom (FC :=
            fun
              (x1 x2 :
                ModuleCat.{u_1, u}
                  (↑(S.obj (P := Presheaf.IsSheaf K).obj (Opposite.op (G.obj (Opposite.unop U)))) : Type u)) ↦
            LinearMap.{u, u, u_1, u_1} (R :=
              (↑(S.obj (P := Presheaf.IsSheaf K).obj (Opposite.op (G.obj (Opposite.unop U)))) : Type u))
              (RingHom.id (↑(S.obj (P := Presheaf.IsSheaf K).obj (Opposite.op (G.obj (Opposite.unop U)))) : Type u))
              (↑x1 : Type u_1) (↑x2 : Type u_1))
            (CC := ModuleCat.carrier) (Y :=
            obj
              (ModuleCat.restrictScalars
                (RingCat.Hom.hom (S.obj (P := Presheaf.IsSheaf K).map (Quiver.Hom.op (α.app (Opposite.unop U))))))
              (X.val.obj (Opposite.op (F.obj (Opposite.unop U)))))
            (X.val.map (Quiver.Hom.op (α.app (Opposite.unop U)))) :
          (a : (↑(X.val.obj (Opposite.op (G.obj (Opposite.unop U)))) : Type u_1)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (S.obj.map (α.app (Opposite.unop U)).op))).obj
                  (X.val.obj (Opposite.op (F.obj (Opposite.unop U))))) :
              Type u_1))
        x :
      (↑(obj
            (ModuleCat.restrictScalars
              (RingCat.Hom.hom (S.obj (P := Presheaf.IsSheaf K).map (Quiver.Hom.op (α.app (Opposite.unop U))))))
            (X.val.obj (Opposite.op (F.obj (Opposite.unop U))))) :
        Type u_1))

Tactic:
rfl

Premises used: 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
h :
  ∀ (x : Cᵒᵖ),
    NatTrans.app
        (InducedCategory.Hom.hom
          (CategoryStruct.comp (Y := obj (F.sheafPushforwardContinuous RingCat J K) S)
            (φ ≫ NatTrans.app (sheafPushforwardContinuousNatTrans α.hom RingCat J K) S)
            (NatTrans.app (sheafPushforwardContinuousNatTrans α.inv RingCat J K) S)))
        x =
      φ.hom.app x
⊢ CategoryStruct.comp (Y := obj (F.sheafPushforwardContinuous RingCat J K) S)
      (φ ≫ NatTrans.app (sheafPushforwardContinuousNatTrans α.hom RingCat J K) S)
      (NatTrans.app (sheafPushforwardContinuousNatTrans α.inv RingCat J K) S) =
    φ

Tactic:
ext : 3
-- 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 : Cᵒᵖ
⊢ NatTrans.app
      (InducedCategory.Hom.hom
        (CategoryStruct.comp (Y := obj (F.sheafPushforwardContinuous RingCat J K) S)
          (φ ≫ NatTrans.app (sheafPushforwardContinuousNatTrans α.hom RingCat J K) S)
          (NatTrans.app (sheafPushforwardContinuousNatTrans α.inv RingCat J K) S)))
      x =
    φ.hom.app x

Tactic:
simp [← Functor.map_comp, ← op_comp]

Premises used: CategoryTheory.op_comp, 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
w :
  ∀ (X : SheafOfModules.{v, v₂, u₂, u} S) (U : Cᵒᵖ) (x : (↑(((pushforward φ).obj X).val.obj U) : Type v)),
    Eq (α := (↑(((pushforward φ).obj X).val.obj U) : Type v))
      ((ModuleCat.Hom.hom
              (((CategoryStruct.comp (Y :=
                          pushforward (φ ≫ NatTrans.app (sheafPushforwardContinuousNatTrans α.hom RingCat J K) S))
                          (pushforwardNatTrans φ α.hom)
                          (pushforwardNatTrans
                              (φ ≫ NatTrans.app (sheafPushforwardContinuousNatTrans α.hom RingCat J K) S) α.inv ≫
                            Iso.hom (pushforwardCongr ⋯))).app
                      X).val.app
                U) :
            (a : (↑(((pushforward φ).obj X).val.obj U) : Type v)) → (↑(((pushforward φ).obj X).val.obj U) : Type v))
          x :
        (↑(((pushforward φ).obj X).val.obj U) : Type v))
      ((ModuleCat.Hom.hom ((NatTrans.app (𝟙 (pushforward φ)) X).val.app U) :
            (a : (↑(((pushforward φ).obj X).val.obj U) : Type v)) → (↑(((pushforward φ).obj X).val.obj U) : Type v))
          x :
        (↑(((pushforward φ).obj X).val.obj U) : Type v))
⊢ CategoryStruct.comp (Y := pushforward (φ ≫ NatTrans.app (sheafPushforwardContinuousNatTrans α.hom RingCat J K) S))
      (pushforwardNatTrans φ α.hom)
      (pushforwardNatTrans (φ ≫ NatTrans.app (sheafPushforwardContinuousNatTrans α.hom RingCat J K) S) α.inv ≫
        Iso.hom (pushforwardCongr ⋯)) =
    𝟙 (pushforward φ)

Tactic:
ext X U x
-- 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 : Cᵒᵖ
x : (↑(((pushforward φ).obj X).val.obj U) : Type v)
w :
  X.val.presheaf.map (Quiver.Hom.op (α.hom.app (Opposite.unop U))) ≫
      X.val.presheaf.map (Quiver.Hom.op (α.inv.app (Opposite.unop U))) =
    𝟙 (X.val.presheaf.obj (Opposite.op (G.obj (Opposite.unop U))))
⊢ Eq (α := (↑(((pushforward φ).obj X).val.obj U) : Type v))
    ((ModuleCat.Hom.hom
            (((CategoryStruct.comp (Y :=
                        pushforward (φ ≫ NatTrans.app (sheafPushforwardContinuousNatTrans α.hom RingCat J K) S))
                        (pushforwardNatTrans φ α.hom)
                        (pushforwardNatTrans (φ ≫ NatTrans.app (sheafPushforwardContinuousNatTrans α.hom RingCat J K) S)
                            α.inv ≫
                          Iso.hom (pushforwardCongr ⋯))).app
                    X).val.app
              U) :
          (a : (↑(((pushforward φ).obj X).val.obj U) : Type v)) → (↑(((pushforward φ).obj X).val.obj U) : Type v))
        x :
      (↑(((pushforward φ).obj X).val.obj U) : Type v))
    ((ModuleCat.Hom.hom ((NatTrans.app (𝟙 (pushforward φ)) X).val.app U) :
          (a : (↑(((pushforward φ).obj X).val.obj U) : Type v)) → (↑(((pushforward φ).obj X).val.obj U) : Type v))
        x :
      (↑(((pushforward φ).obj X).val.obj U) : Type v))

Tactic:
suffices X.val.presheaf.map (α.hom.app U.unop).op ≫
      X.val.presheaf.map (α.inv.app U.unop).op = 𝟙 _ from congr($this x)
-- 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 : Cᵒᵖ
x : (↑(((pushforward φ).obj X).val.obj U) : Type v)
⊢ X.val.presheaf.map (Quiver.Hom.op (α.hom.app (Opposite.unop U))) ≫
      X.val.presheaf.map (Quiver.Hom.op (α.inv.app (Opposite.unop U))) =
    𝟙 (X.val.presheaf.obj (Opposite.op (G.obj (Opposite.unop U))))

Tactic:
simp only [← Functor.map_comp, ← op_comp,
      Iso.inv_hom_id_app, op_id, CategoryTheory.Functor.map_id]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.op_id
-- 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
w :
  ∀ (X : SheafOfModules.{v, v₂, u₂, u} S) (U : Cᵒᵖ)
    (x :
      (↑(((pushforward (φ ≫ NatTrans.app (sheafPushforwardContinuousNatTrans α.hom RingCat J K) S)).obj X).val.obj U) :
        Type v)),
    Eq (α :=
      (↑(((pushforward (φ ≫ NatTrans.app (sheafPushforwardContinuousNatTrans α.hom RingCat J K) S)).obj X).val.obj U) :
        Type v))
      ((ModuleCat.Hom.hom
              (PresheafOfModules.Hom.app
                (Hom.val
                  (NatTrans.app
                    ((pushforwardNatTrans (φ ≫ NatTrans.app (sheafPushforwardContinuousNatTrans α.hom RingCat J K) S)
                          α.inv ≫
                        Iso.hom (pushforwardCongr ⋯)) ≫
                      pushforwardNatTrans φ α.hom)
                    X))
                U) :
            (a :
                (↑(((pushforward (φ ≫ (sheafPushforwardContinuousNatTrans α.hom RingCat J K).app S)).obj X).val.obj U) :
                  Type v)) →
              (↑(((pushforward (φ ≫ (sheafPushforwardContinuousNatTrans α.hom RingCat J K).app S)).obj X).val.obj U) :
                Type v))
          x :
        (↑(((pushforward (φ ≫ NatTrans.app (sheafPushforwardContinuousNatTrans α.hom RingCat J K) S)).obj X).val.obj
              U) :
          Type v))
      ((ModuleCat.Hom.hom
              ((NatTrans.app
                      (𝟙 (pushforward (φ ≫ NatTrans.app (sheafPushforwardContinuousNatTrans α.hom RingCat J K) S)))
                      X).val.app
                U) :
            (a :
                (↑(((pushforward (φ ≫ (sheafPushforwardContinuousNatTrans α.hom RingCat J K).app S)).obj X).val.obj U) :
                  Type v)) →
              (↑(((pushforward (φ ≫ (sheafPushforwardContinuousNatTrans α.hom RingCat J K).app S)).obj X).val.obj U) :
                Type v))
          x :
        (↑(((pushforward (φ ≫ NatTrans.app (sheafPushforwardContinuousNatTrans α.hom RingCat J K) S)).obj X).val.obj
              U) :
          Type v))
⊢ (pushforwardNatTrans (φ ≫ NatTrans.app (sheafPushforwardContinuousNatTrans α.hom RingCat J K) S) α.inv ≫
        Iso.hom (pushforwardCongr ⋯)) ≫
      pushforwardNatTrans φ α.hom =
    𝟙 (pushforward (φ ≫ NatTrans.app (sheafPushforwardContinuousNatTrans α.hom RingCat J K) S))

Tactic:
ext X U x