awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous (goal)
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
⊢ 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) =
    φ
have 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
Tactic: ext : 3
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous (goal)
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
⊢ 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 φ)
have 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 sorry))).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: ext X U x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous (goal)
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)
⊢ 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))
have 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))))
Tactic: suffices X.val.presheaf.map (α.hom.app U.unop).op ≫
      X.val.presheaf.map (α.inv.app U.unop).op = 𝟙 _ from congr($this x)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous (goal)
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
⊢ (pushforwardNatTrans (φ ≫ NatTrans.app (sheafPushforwardContinuousNatTrans α.hom RingCat J K) S) α.inv ≫
        Iso.hom (pushforwardCongr ⋯)) ≫
      pushforwardNatTrans φ α.hom =
    𝟙 (pushforward (φ ≫ NatTrans.app (sheafPushforwardContinuousNatTrans α.hom RingCat J K) S))
have 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 sorry)) ≫
                    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))
Tactic: ext X U x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous (goal)
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 (φ ≫ 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))
have w : X.val.presheaf.map (Quiver.Hom.op (α.inv.app (Opposite.unop U))) ≫
    X.val.presheaf.map (Quiver.Hom.op (α.hom.app (Opposite.unop U))) =
  𝟙 (X.val.presheaf.obj (Opposite.op (F.obj (Opposite.unop U))))
Tactic: suffices X.val.presheaf.map (α.inv.app U.unop).op ≫
      X.val.presheaf.map (α.hom.app U.unop).op = 𝟙 _ from congr($this x)
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous (goal)
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_1 : 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_1
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 : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
G : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} D C
S : Sheaf J RingCat
R : Sheaf K RingCat
inst_7 : F.IsContinuous J K
inst_8 : G.IsContinuous K J
adj : F ⊣ G
φ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J K) R
ψ : R ⟶ obj (G.sheafPushforwardContinuous RingCat K J) S
H₁ : whiskerRight (NatTrans.op adj.counit) (R.obj (P := Presheaf.IsSheaf K)) = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ :
  φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) (S.obj (P := Presheaf.IsSheaf J)) =
    𝟙 (S.obj (P := Presheaf.IsSheaf J))
this : (G ⋙ F).IsContinuous K K := ⋯
⊢ 𝟙 (obj (sheafPushforwardContinuous (𝟭 D) RingCat K K) R) ≫
      NatTrans.app (sheafPushforwardContinuousNatTrans adj.counit RingCat K K) R =
    ψ ≫ CategoryTheory.Functor.map (G.sheafPushforwardContinuous RingCat K J) φ
have h : InducedCategory.Hom.hom
    (𝟙 (obj (sheafPushforwardContinuous (𝟭 D) RingCat K K) R) ≫
      NatTrans.app (sheafPushforwardContinuousNatTrans adj.counit RingCat K K) R) =
  (ψ ≫ CategoryTheory.Functor.map (G.sheafPushforwardContinuous RingCat K J) φ).hom
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous (goal)
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_1 : 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_1
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 : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
G : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} D C
S : Sheaf J RingCat
R : Sheaf K RingCat
inst_7 : F.IsContinuous J K
inst_8 : G.IsContinuous K J
adj : F ⊣ G
φ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J K) R
ψ : R ⟶ obj (G.sheafPushforwardContinuous RingCat K J) S
H₁ : whiskerRight (NatTrans.op adj.counit) (R.obj (P := Presheaf.IsSheaf K)) = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ :
  φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) (S.obj (P := Presheaf.IsSheaf J)) =
    𝟙 (S.obj (P := Presheaf.IsSheaf J))
this : (F ⋙ G).IsContinuous J J := ⋯
⊢ Eq (α := S ⟶ obj (sheafPushforwardContinuous (𝟭 C) RingCat J J) S)
    ((φ ≫ CategoryTheory.Functor.map (F.sheafPushforwardContinuous RingCat J K) ψ) ≫
      NatTrans.app (sheafPushforwardContinuousNatTrans adj.unit RingCat J J) S)
    (𝟙 S)
have h : InducedCategory.Hom.hom
    ((φ ≫ CategoryTheory.Functor.map (F.sheafPushforwardContinuous RingCat J K) ψ) ≫
      NatTrans.app (sheafPushforwardContinuousNatTrans adj.unit RingCat J J) S) =
  InducedCategory.Hom.hom (𝟙 S)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous (goal)
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_1 : 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_1
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 : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
G : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} D C
S : Sheaf J RingCat
R : Sheaf K RingCat
inst_7 : F.IsContinuous J K
inst_8 : G.IsContinuous K J
adj : F ⊣ G
φ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J K) R
ψ : R ⟶ obj (G.sheafPushforwardContinuous RingCat K J) S
H₁ : whiskerRight (NatTrans.op adj.counit) (R.obj (P := Presheaf.IsSheaf K)) = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ :
  φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) (S.obj (P := Presheaf.IsSheaf J)) =
    𝟙 (S.obj (P := Presheaf.IsSheaf J))
X : SheafOfModules.{v, v₂, u₂, u} R
⊢ (pushforward φ).map
        (((pushforwardId R).inv ≫
              pushforwardNatTrans (𝟙 (obj (sheafPushforwardContinuous (𝟭 D) RingCat K K) R)) adj.counit ≫
                (pushforwardCongr ⋯).hom ≫ Iso.inv (pushforwardComp ψ φ)).app
          X) ≫
      (Iso.hom (pushforwardComp φ ψ) ≫
            pushforwardNatTrans (φ ≫ CategoryTheory.Functor.map (F.sheafPushforwardContinuous RingCat J K) ψ) adj.unit ≫
              (pushforwardCongr ⋯).hom ≫ (pushforwardId S).hom).app
        ((pushforward φ).obj X) =
    𝟙 ((pushforward φ).obj X)
have h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: ext U x
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous (goal)
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_1 : 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_1
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 : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
G : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} D C
S : Sheaf J RingCat
R : Sheaf K RingCat
inst_7 : F.IsContinuous J K
inst_8 : G.IsContinuous K J
adj : F ⊣ G
φ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J K) R
ψ : R ⟶ obj (G.sheafPushforwardContinuous RingCat K J) S
H₁ : whiskerRight (NatTrans.op adj.counit) (R.obj (P := Presheaf.IsSheaf K)) = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ :
  φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) (S.obj (P := Presheaf.IsSheaf J)) =
    𝟙 (S.obj (P := Presheaf.IsSheaf J))
X : SheafOfModules.{v, v₂, u₂, u} R
U : Cᵒᵖ
x : (↑(((pushforward φ).obj X).val.obj U) : Type v)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h : Eq (α := (↑(X.val.presheaf.obj (Opposite.op (F.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) (Opposite.unop U))))) : Type v))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
          AddCommGrpCat.carrier) (X :=
          X.val.presheaf.obj (Opposite.op (obj.{v₂, v₂, u₂, u₂} (𝟭 D) (F.obj (Opposite.unop U)))))
          (X.val.presheaf.map (Quiver.Hom.op (adj.counit.app (F.obj (Opposite.unop U)))) ≫
            X.val.presheaf.map (Quiver.Hom.op (F.map (adj.unit.app (Opposite.unop U))))) :
        (a : (↑(X.val.presheaf.obj (Opposite.op ((𝟭 D).obj (F.obj (Opposite.unop U))))) : Type v)) →
          (↑(X.val.presheaf.obj (Opposite.op (F.obj ((𝟭 C).obj (Opposite.unop U))))) : Type v))
      x :
    (↑(X.val.presheaf.obj (Opposite.op (F.obj (obj.{v₁, v₁, u₁, u₁} (𝟭 C) (Opposite.unop U))))) : Type v))
  ((ModuleCat.Hom.hom ((Hom.val (𝟙 ((pushforward φ).obj X))).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: change (X.val.presheaf.map (adj.counit.app (F.obj U.unop)).op ≫
      X.val.presheaf.map (F.map (adj.unit.app U.unop)).op) _ = _
-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous (goal)
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_1 : 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_1
C_2 : Type u₁
inst_5 : Category.{v₁, u₁} C_2
D : Type u₂
inst_6 : Category.{v₂, u₂} D
J_2 : GrothendieckTopology.{v₁, u₁} C_2
K : GrothendieckTopology.{v₂, u₂} D
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C_2 D
G : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} D C_2
S : Sheaf J_2 RingCat
R_2 : Sheaf K RingCat
inst_7 : F.IsContinuous J_2 K
inst_8 : G.IsContinuous K J_2
adj : F ⊣ G
φ : S ⟶ obj (F.sheafPushforwardContinuous RingCat J_2 K) R_2
ψ : R_2 ⟶ obj (G.sheafPushforwardContinuous RingCat K J_2) S
H₁ : whiskerRight (NatTrans.op adj.counit) (R_2.obj (P := Presheaf.IsSheaf K)) = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ :
  φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) (S.obj (P := Presheaf.IsSheaf J_2)) =
    𝟙 (S.obj (P := Presheaf.IsSheaf J_2))
C : Type u'
inst_9 : Category.{v', u'} C
inst_10 : HasBinaryProducts.{v', u'} C
J : GrothendieckTopology.{v', u'} C
R : Sheaf J RingCat
x : C
U V : Cᵒᵖ
f : U ⟶ V
⊢ R.obj (P := Presheaf.IsSheaf J).map f ≫ R.obj (P := Presheaf.IsSheaf J).map (Quiver.Hom.op prod.snd) =
    R.obj (P := Presheaf.IsSheaf J).map (Quiver.Hom.op prod.snd) ≫
      (obj (sheafPushforwardContinuous (Over.star x) RingCat J (J.over x)) (R.over x)).obj (P := Presheaf.IsSheaf J).map
        f
have simp : Eq (α :=
  R.obj (P := Presheaf.IsSheaf J).obj U ⟶
    R.obj (P := Presheaf.IsSheaf J).obj (Opposite.op (Limits.prod.{v', u'} x (Opposite.unop V))))
  (R.obj (P := Presheaf.IsSheaf J).map (f ≫ Quiver.Hom.op prod.snd))
  (R.obj (P := Presheaf.IsSheaf J).map (Quiver.Hom.op (prod.snd ≫ f.unop)))
Tactic: simp [← Functor.map_comp, ← op_comp]