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_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
⊢ 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:
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_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
refine_1 :
  Eq (α :=
    Functor.op (𝟭 C) ⋙ R.obj (P := Presheaf.IsSheaf J) ⟶
      Functor.op (Over.star x ⋙ Over.forget x) ⋙ R.obj (P := Presheaf.IsSheaf J))
    (whiskerRight (NatTrans.op (Adjunction.counit (Over.forgetAdjStar x))) (R.obj (P := Presheaf.IsSheaf J)))
    (InducedCategory.Hom.hom (pushforwardOver x) ≫
      whiskerLeft (Functor.op (Over.star x)) (InducedCategory.Hom.hom (𝟙 (R.over x))))
refine_2 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ pushforward (𝟙 (R.over x)) ⊣ pushforward (F := Over.star x) (pushforwardOver x)

Tactic:
refine pushforwardPushforwardAdj (Over.forgetAdjStar x) (𝟙 (R.over x)) _ ?_ ?_

Premises used: CategoryTheory.Sheaf.over, CategoryTheory.CategoryStruct.id, SheafOfModules.pushforwardPushforwardAdj, CategoryTheory.Over.forgetAdjStar
-- 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_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
refine_1 :
  ∀ (y : Cᵒᵖ),
    Eq (α :=
      (Functor.op (𝟭 C) ⋙ R.obj (P := Presheaf.IsSheaf J)).obj y ⟶
        (Functor.op (Over.star x ⋙ Over.forget x) ⋙ R.obj (P := Presheaf.IsSheaf J)).obj y)
      (NatTrans.app
        (whiskerRight (NatTrans.op (Adjunction.counit (Over.forgetAdjStar x))) (R.obj (P := Presheaf.IsSheaf J))) y)
      (NatTrans.app
        (InducedCategory.Hom.hom (pushforwardOver x) ≫
          whiskerLeft (Functor.op (Over.star x)) (InducedCategory.Hom.hom (𝟙 (R.over x))))
        y)
⊢ Eq (α :=
    Functor.op (𝟭 C) ⋙ R.obj (P := Presheaf.IsSheaf J) ⟶
      Functor.op (Over.star x ⋙ Over.forget x) ⋙ R.obj (P := Presheaf.IsSheaf J))
    (whiskerRight (NatTrans.op (Adjunction.counit (Over.forgetAdjStar x))) (R.obj (P := Presheaf.IsSheaf J)))
    (InducedCategory.Hom.hom (pushforwardOver x) ≫
      whiskerLeft (Functor.op (Over.star x)) (InducedCategory.Hom.hom (𝟙 (R.over x))))

Tactic:
ext y : 2
-- 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_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
y : Cᵒᵖ
⊢ Eq (α :=
    (Functor.op (𝟭 C) ⋙ R.obj (P := Presheaf.IsSheaf J)).obj y ⟶
      (Functor.op (Over.star x ⋙ Over.forget x) ⋙ R.obj (P := Presheaf.IsSheaf J)).obj y)
    (NatTrans.app
      (whiskerRight (NatTrans.op (Adjunction.counit (Over.forgetAdjStar x))) (R.obj (P := Presheaf.IsSheaf J))) y)
    (NatTrans.app
      (InducedCategory.Hom.hom (pushforwardOver x) ≫
        whiskerLeft (Functor.op (Over.star x)) (InducedCategory.Hom.hom (𝟙 (R.over x))))
      y)

Tactic:
simp [pushforwardOver]

Premises used: SheafOfModules.pushforwardOver
-- 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_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
refine_2 : 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 y : 2
-- 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_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
y : (Over.{v', u'} x)ᵒᵖ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

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

Premises used: CategoryTheory.op_comp, SheafOfModules.pushforwardOver, 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 : 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.IsContinuous J_1 K_1
φ_1 : S_1 ⟶ obj (F.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
eqv : CategoryTheory.Equivalence.{v₁, v₂, u₁, u₂} C D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst_7 : eqv.functor.IsContinuous J K
inst_8 : eqv.inverse.IsContinuous K J
φ : S ⟶ obj (eqv.functor.sheafPushforwardContinuous RingCat J K) R
ψ : R ⟶ obj (eqv.inverse.sheafPushforwardContinuous RingCat K J) S
H₁ : whiskerRight (NatTrans.op eqv.counit) (R.obj (P := Presheaf.IsSheaf K)) = ψ.hom ≫ eqv.inverse.op.whiskerLeft φ.hom
H₂ :
  φ.hom ≫ eqv.functor.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op eqv.unit) (S.obj (P := Presheaf.IsSheaf J)) =
    𝟙 (S.obj (P := Presheaf.IsSheaf J))
this : (eqv.inverse ⋙ eqv.functor).IsContinuous K K := ⋯
h :
  InducedCategory.Hom.hom (𝟙 R ≫ NatTrans.app (sheafPushforwardContinuousNatTrans eqv.counitIso.hom RingCat K K) R) =
    (ψ ≫ CategoryTheory.Functor.map (eqv.inverse.sheafPushforwardContinuous RingCat K J) φ).hom
⊢ 𝟙 R ≫ NatTrans.app (sheafPushforwardContinuousNatTrans eqv.counitIso.hom RingCat K K) R =
    ψ ≫ CategoryTheory.Functor.map (eqv.inverse.sheafPushforwardContinuous RingCat K J) φ

Tactic:
ext1
-- 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 : 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.IsContinuous J_1 K_1
φ_1 : S_1 ⟶ obj (F.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
eqv : CategoryTheory.Equivalence.{v₁, v₂, u₁, u₂} C D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst_7 : eqv.functor.IsContinuous J K
inst_8 : eqv.inverse.IsContinuous K J
φ : S ⟶ obj (eqv.functor.sheafPushforwardContinuous RingCat J K) R
ψ : R ⟶ obj (eqv.inverse.sheafPushforwardContinuous RingCat K J) S
H₁ : whiskerRight (NatTrans.op eqv.counit) (R.obj (P := Presheaf.IsSheaf K)) = ψ.hom ≫ eqv.inverse.op.whiskerLeft φ.hom
H₂ :
  φ.hom ≫ eqv.functor.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op eqv.unit) (S.obj (P := Presheaf.IsSheaf J)) =
    𝟙 (S.obj (P := Presheaf.IsSheaf J))
this : (eqv.inverse ⋙ eqv.functor).IsContinuous K K := ⋯
⊢ InducedCategory.Hom.hom (𝟙 R ≫ NatTrans.app (sheafPushforwardContinuousNatTrans eqv.counitIso.hom RingCat K K) R) =
    (ψ ≫ CategoryTheory.Functor.map (eqv.inverse.sheafPushforwardContinuous RingCat K J) φ).hom

Tactic:
simpa
-- 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 : 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.IsContinuous J_1 K_1
φ_1 : S_1 ⟶ obj (F.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
eqv : CategoryTheory.Equivalence.{v₁, v₂, u₁, u₂} C D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst_7 : eqv.functor.IsContinuous J K
inst_8 : eqv.inverse.IsContinuous K J
φ : S ⟶ obj (eqv.functor.sheafPushforwardContinuous RingCat J K) R
ψ : R ⟶ obj (eqv.inverse.sheafPushforwardContinuous RingCat K J) S
H₁ : whiskerRight (NatTrans.op eqv.counit) (R.obj (P := Presheaf.IsSheaf K)) = ψ.hom ≫ eqv.inverse.op.whiskerLeft φ.hom
H₂ :
  φ.hom ≫ eqv.functor.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op eqv.unit) (S.obj (P := Presheaf.IsSheaf J)) =
    𝟙 (S.obj (P := Presheaf.IsSheaf J))
this : (eqv.functor ⋙ eqv.inverse).IsContinuous J J := ⋯
h :
  InducedCategory.Hom.hom
      ((φ ≫ CategoryTheory.Functor.map (eqv.functor.sheafPushforwardContinuous RingCat J K) ψ) ≫
        NatTrans.app (sheafPushforwardContinuousNatTrans eqv.unitIso.hom RingCat J J) S) =
    InducedCategory.Hom.hom (𝟙 S)
⊢ Eq (α := S ⟶ obj (sheafPushforwardContinuous (𝟭 C) RingCat J J) S)
    ((φ ≫ CategoryTheory.Functor.map (eqv.functor.sheafPushforwardContinuous RingCat J K) ψ) ≫
      NatTrans.app (sheafPushforwardContinuousNatTrans eqv.unitIso.hom RingCat J J) S)
    (𝟙 S)

Tactic:
ext1
-- 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 : 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.IsContinuous J_1 K_1
φ_1 : S_1 ⟶ obj (F.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
eqv : CategoryTheory.Equivalence.{v₁, v₂, u₁, u₂} C D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst_7 : eqv.functor.IsContinuous J K
inst_8 : eqv.inverse.IsContinuous K J
φ : S ⟶ obj (eqv.functor.sheafPushforwardContinuous RingCat J K) R
ψ : R ⟶ obj (eqv.inverse.sheafPushforwardContinuous RingCat K J) S
H₁ : whiskerRight (NatTrans.op eqv.counit) (R.obj (P := Presheaf.IsSheaf K)) = ψ.hom ≫ eqv.inverse.op.whiskerLeft φ.hom
H₂ :
  φ.hom ≫ eqv.functor.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op eqv.unit) (S.obj (P := Presheaf.IsSheaf J)) =
    𝟙 (S.obj (P := Presheaf.IsSheaf J))
this : (eqv.functor ⋙ eqv.inverse).IsContinuous J J := ⋯
⊢ InducedCategory.Hom.hom
      ((φ ≫ CategoryTheory.Functor.map (eqv.functor.sheafPushforwardContinuous RingCat J K) ψ) ≫
        NatTrans.app (sheafPushforwardContinuousNatTrans eqv.unitIso.hom RingCat J J) S) =
    InducedCategory.Hom.hom (𝟙 S)

Tactic:
simpa
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_1 : HasWeakSheafify J AddCommGrpCat
inst_2 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_3 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
M : SheafOfModules R
p : M.Presentation
inst_4 : p.IsFinite
⊢ Finite.{u + 1} p.relations.I

Tactic:
GeneratingSections.IsFiniteType.finite

Premises used: SheafOfModules.GeneratingSections.IsFiniteType.finite
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
J_1 : GrothendieckTopology.{v₁, u₁} C_1
R_1 : Sheaf J_1 RingCat
C : Type u₁
inst_1 : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_2 : HasSheafify J AddCommGrpCat
inst_3 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_4 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
ι σ : Type u
M : SheafOfModules R
f : Quiver.Hom (V := SheafOfModules R) (free ι) (free σ)
g : free σ ⟶ M
H : f ≫ g = 0
H' : IsColimit (CokernelCofork.ofπ g H)
⊢ Epi (C := SheafOfModules R) (X := (free σ : SheafOfModules R)) (Y := M)
    ((Equiv.symm M.freeHomEquiv : (a : σ → M.sections) → free σ ⟶ M)
        ((M.freeHomEquiv : (a : free σ ⟶ M) → σ → M.sections) g) :
      free σ ⟶ M)

Tactic:
simpa using epi_of_isColimit_cofork H'

Premises used: CategoryTheory.Limits.epi_of_isColimit_cofork
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_1 : HasSheafify J AddCommGrpCat
inst_2 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_3 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
ι σ : Type u
M : SheafOfModules R
f : Quiver.Hom (V := SheafOfModules R) (free ι) (free σ)
g : free σ ⟶ M
H : f ≫ g = 0
H' : IsColimit (CokernelCofork.ofπ g H)
⊢ GeneratingSections.π (generatorsOfIsCokernelFree f g H H') = g

Tactic:
M.freeHomEquiv.symm_apply_apply g

Premises used: Equiv.symm_apply_apply, SheafOfModules.freeHomEquiv
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
J_1 : GrothendieckTopology.{v₁, u₁} C_1
R_1 : Sheaf J_1 RingCat
C : Type u₁
inst_1 : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_2 : HasSheafify J AddCommGrpCat
inst_3 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_4 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
ι σ : Type u
M : SheafOfModules R
f : Quiver.Hom (V := SheafOfModules R) (free ι) (free σ)
g : free σ ⟶ M
H : f ≫ g = 0
H' : IsColimit (CokernelCofork.ofπ g H)
⊢ Eq (α := free ι ⟶ M) (f ≫ GeneratingSections.π (generatorsOfIsCokernelFree f g H H')) 0

Tactic:
simp [H]
-- Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
J_1 : GrothendieckTopology.{v₁, u₁} C_1
R_1 : Sheaf J_1 RingCat
C : Type u₁
inst_1 : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
R : Sheaf J RingCat
inst_2 : HasSheafify J AddCommGrpCat
inst_3 :
  J.WEqualsLocallyBijective AddCommGrpCat (FA := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u))
    (CA := AddCommGrpCat.carrier)
inst_4 :
  J.HasSheafCompose
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := RingCat.carrier)
      AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommGrpCat.carrier))
ι σ : Type u
M : SheafOfModules R
f : Quiver.Hom (V := SheafOfModules R) (free ι) (free σ)
g : free σ ⟶ M
H : f ≫ g = 0
H' : IsColimit (CokernelCofork.ofπ g H)
h : cokernel f ≅ M := Iso.symm (H'.coconePointUniqueUpToIso (colimit.isColimit (parallelPair f 0)))
⊢ cokernel.π f ≫ h.hom = Iso.hom (Iso.refl (free σ)) ≫ GeneratingSections.π (generatorsOfIsCokernelFree f g H H')

Tactic:
simp [h]