awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.LimitsOver
Goal:
X : Scheme
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst_1 : Category.{v_1, u_1} J
F : CategoryTheory.Functor.{v_1, u, u_1, u + 1} J (P.Over ⊤ S)
inst_2 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_3 : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst_4 : Quiver.IsThin.{u_1, v_1} J
inst_5 : Small.{u, u_1} J
this : HasColimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)
e : (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).left ≅
  colimit ((F ⋙ MorphismProperty.Over.forget P ⊤ S) ⋙ Over.forget S) :=
  preservesColimitIso (Over.forget S) (F ⋙ MorphismProperty.Over.forget P ⊤ S)
𝒰 : Scheme.OpenCover.{u_1, u} (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).left :=
  Scheme.Cover.pushforwardIso (P := IsOpenImmersion)
    (Scheme.IsLocallyDirected.openCover ((F ⋙ MorphismProperty.Over.forget P ⊤ S) ⋙ Over.forget S)) e.inv
i : 𝒰.I₀
⊢ P (𝒰.f i ≫ (colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S)).hom)

Tactic:
simpa [𝒰, e] using (F.obj i).prop

Premises used: CategoryTheory.MorphismProperty.Comma.prop, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.LimitsOver
Goal:
X : Scheme
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst_1 : Category.{v_1, u_1} J
F : CategoryTheory.Functor.{v_1, u, u_1, u + 1} J (P.Over ⊤ S)
inst_2 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_3 : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst_4 : Quiver.IsThin.{u_1, v_1} J
inst_5 : Small.{u, u_1} J
⊢ HasColimit F

Tactic:
hasColimit_of_created _ (MorphismProperty.Over.forget P ⊤ S)

Premises used: CategoryTheory.MorphismProperty.Over.forget, Top.top, CategoryTheory.hasColimit_of_created
-- Module: Mathlib.AlgebraicGeometry.LimitsOver
Goal:
X : Scheme
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst_1 : Category.{v_1, u_1} J
F : CategoryTheory.Functor.{v_1, u, u_1, u + 1} J (P.Over ⊤ S)
inst_2 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_3 : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst_4 : Quiver.IsThin.{u_1, v_1} J
inst_5 : Small.{u, u_1} J
⊢ PreservesColimit F (MorphismProperty.Over.forget P ⊤ S)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.LimitsOver
Goal:
X : Scheme
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst_1 : Category.{v_1, u_1} J
F : CategoryTheory.Functor.{v_1, u, u_1, u + 1} J (P.Over ⊤ S)
inst_2 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_3 : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst_4 : Quiver.IsThin.{u_1, v_1} J
inst_5 : Small.{u, u_1} J
j : J
e : (colimit F).toComma (P := P) (Q := ⊤) (W := ⊤).left ≅
  colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) :=
  preservesColimitIso (MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) F
rw :
  IsOpenImmersion (X := (F.obj j).toComma (P := P) (Q := ⊤) (W := ⊤).left) (Y :=
    colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S))
    (CategoryTheory.Functor.map (MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) (colimit.ι F j) ≫ e.hom :
      (F.obj j).toComma (P := P) (Q := ⊤) (W := ⊤).left ⟶
        colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S))
⊢ IsOpenImmersion (X := (F.obj j).toComma (P := P) (Q := ⊤) (W := ⊤).left) (Y :=
    (colimit F).toComma (P := P) (Q := ⊤) (W := ⊤).left)
    (CategoryTheory.Functor.map (MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) (colimit.ι F j) :
      Functor.obj (MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) (F.obj j) ⟶
        Functor.obj (MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) (colimit F))

Tactic:
rw [← MorphismProperty.cancel_right_of_respectsIso (P := @IsOpenImmersion) _ e.hom]

Premises used: AlgebraicGeometry.IsOpenImmersion, CategoryTheory.Iso.hom, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.LimitsOver
Goal:
X : Scheme
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst_1 : Category.{v_1, u_1} J
F : CategoryTheory.Functor.{v_1, u, u_1, u + 1} J (P.Over ⊤ S)
inst_2 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_3 : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst_4 : Quiver.IsThin.{u_1, v_1} J
inst_5 : Small.{u, u_1} J
j : J
e : (colimit F).toComma (P := P) (Q := ⊤) (W := ⊤).left ≅
  colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) :=
  preservesColimitIso (MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) F
simp :
  IsOpenImmersion (Y := colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S))
    (colimit.ι (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) j)
⊢ IsOpenImmersion (X := (F.obj j).toComma (P := P) (Q := ⊤) (W := ⊤).left) (Y :=
    colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S))
    (CategoryTheory.Functor.map (MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) (colimit.ι F j) ≫ e.hom :
      (F.obj j).toComma (P := P) (Q := ⊤) (W := ⊤).left ⟶
        colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S))

Tactic:
simp only [e, CategoryTheory.ι_preservesColimitIso_hom]

Premises used: CategoryTheory.ι_preservesColimitIso_hom
-- Module: Mathlib.AlgebraicGeometry.LimitsOver
Goal:
X : Scheme
P : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P
S : Scheme
J : Type u_1
inst_1 : Category.{v_1, u_1} J
F : CategoryTheory.Functor.{v_1, u, u_1, u + 1} J (P.Over ⊤ S)
inst_2 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
inst_3 : (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst_4 : Quiver.IsThin.{u_1, v_1} J
inst_5 : Small.{u, u_1} J
j : J
e : (colimit F).toComma (P := P) (Q := ⊤) (W := ⊤).left ≅
  colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) :=
  preservesColimitIso (MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) F
⊢ IsOpenImmersion (Y := colimit (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S))
    (colimit.ι (F ⋙ MorphismProperty.Over.forget P ⊤ S ⋙ Over.forget S) j)

Tactic:
inferInstanceAs <| IsOpenImmersion
    (colimit.ι ((F ⋙ MorphismProperty.Over.forget P ⊤ S) ⋙ Over.forget S) j)

Premises used: _private.0.AlgebraicGeometry.instIsOpenImmersionLeftSchemeDiscretePUnitιOverTopMorphismProperty._proof_1
-- Module: Mathlib.AlgebraicGeometry.LimitsOver
Goal:
X_1 : Scheme
P_1 : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P_1
S : Scheme
J : Type u_1
inst_1 : Category.{v_1, u_1} J
F : CategoryTheory.Functor.{v_1, u, u_1, u + 1} J (P_1.Over ⊤ S)
inst_2 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).toCommaMorphism (P := P_1) (Q := ⊤) (W := ⊤).left
inst_3 : (F ⋙ MorphismProperty.Over.forget P_1 ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst_4 : Quiver.IsThin.{u_1, v_1} J
inst_5 : Small.{u, u_1} J
P : MorphismProperty Scheme
inst_6 : IsZariskiLocalAtSource P
ι : Type u_2
inst_7 : Small.{u, u_2} ι
C : Type u_3
inst_8 : Category.{v_2, u_3} C
inst_9 : HasColimitsOfShape.{u_2, u_2, v_2, u_3} (Discrete ι) C
L : CategoryTheory.Functor.{v_2, u, u_3, u + 1} C Scheme
inst_10 : PreservesColimitsOfShape.{u_2, u_2, v_2, u, u_3, u + 1} (Discrete ι) L
X : Scheme
⊢ ObjectProperty.IsClosedUnderColimitsOfShape (C := CostructuredArrow L X) (MorphismProperty.costructuredArrowObj L P)
    (Discrete ι)

Tactic:
CostructuredArrow.isClosedUnderColimitsOfShape _ (fun _ ↦ coproductIsCoproduct' _)
    (fun _ _ _ _ h ↦ IsZariskiLocalAtSource.sigmaDesc (h ⟨·⟩)) _

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.sigmaDesc, CategoryTheory.Discrete.mk, CategoryTheory.Limits.coproductIsCoproduct', CategoryTheory.CostructuredArrow.isClosedUnderColimitsOfShape
-- Module: Mathlib.AlgebraicGeometry.LimitsOver
Goal:
X : Scheme
P_1 : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P_1
S : Scheme
J : Type u_1
inst_1 : Category.{v_1, u_1} J
F : CategoryTheory.Functor.{v_1, u, u_1, u + 1} J (P_1.Over ⊤ S)
inst_2 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).toCommaMorphism (P := P_1) (Q := ⊤) (W := ⊤).left
inst_3 : (F ⋙ MorphismProperty.Over.forget P_1 ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst_4 : Quiver.IsThin.{u_1, v_1} J
inst_5 : Small.{u, u_1} J
P : MorphismProperty Scheme
inst_6 : IsZariskiLocalAtSource P
inst_7 : P.IsStableUnderBaseChange
inst_8 : P.HasOfPostcompProperty P
inst_9 : P.IsMultiplicative
n : ℕ
⊢ (MorphismProperty.commaObj Scheme.Spec (Functor.fromPUnit S) P).IsClosedUnderColimitsOfShape (Discrete (Fin n))

Tactic:
have : (MorphismProperty.commaObj Scheme.Spec (.fromPUnit S) P).IsClosedUnderColimitsOfShape
        (Discrete (Fin n)) :=
      IsZariskiLocalAtSource.isClosedUnderColimitsOfShape_discrete _ _
-- Module: Mathlib.AlgebraicGeometry.LimitsOver
Goal:
X : Scheme
P_1 : MorphismProperty Scheme
inst : IsZariskiLocalAtSource P_1
S : Scheme
J : Type u_1
inst_1 : Category.{v_1, u_1} J
F : CategoryTheory.Functor.{v_1, u, u_1, u + 1} J (P_1.Over ⊤ S)
inst_2 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f).toCommaMorphism (P := P_1) (Q := ⊤) (W := ⊤).left
inst_3 : (F ⋙ MorphismProperty.Over.forget P_1 ⊤ S ⋙ Over.forget S ⋙ Scheme.forget).IsLocallyDirected
inst_4 : Quiver.IsThin.{u_1, v_1} J
inst_5 : Small.{u, u_1} J
P : MorphismProperty Scheme
inst_6 : IsZariskiLocalAtSource P
inst_7 : P.IsStableUnderBaseChange
inst_8 : P.HasOfPostcompProperty P
inst_9 : P.IsMultiplicative
n : ℕ
this : (MorphismProperty.commaObj Scheme.Spec (Functor.fromPUnit S) P).IsClosedUnderColimitsOfShape (Discrete (Fin n))
⊢ HasColimitsOfShape.{0, 0, u, u + 1} (Discrete (Fin n)) (P.CostructuredArrow ⊤ Scheme.Spec S)

Tactic:
apply MorphismProperty.Comma.hasColimitsOfShape_of_closedUnderColimitsOfShape

Premises used: CategoryTheory.MorphismProperty.Comma.hasColimitsOfShape_of_closedUnderColimitsOfShape
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y Z T : Scheme
⊢ HasLimits.{u, u + 1} X.Modules

Tactic:
inferInstanceAs (HasLimits (SheafOfModules X.ringCatSheaf))

Premises used: _private.0.AlgebraicGeometry.Scheme.Modules.instHasLimits._proof_1
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y Z T : Scheme
⊢ HasColimits.{u, u + 1} X.Modules

Tactic:
inferInstanceAs (HasColimits (SheafOfModules X.ringCatSheaf))

Premises used: _private.0.AlgebraicGeometry.Scheme.Modules.instHasColimits._proof_1
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y Z T : Scheme
⊢ (toPresheafOfModules X).Full

Tactic:
fullyFaithfulToPresheafOfModules.full

Premises used: CategoryTheory.Functor.FullyFaithful.full, AlgebraicGeometry.Scheme.Modules.fullyFaithfulToPresheafOfModules
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y Z T : Scheme
⊢ (toPresheafOfModules X).Faithful

Tactic:
fullyFaithfulToPresheafOfModules.faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, AlgebraicGeometry.Scheme.Modules.fullyFaithfulToPresheafOfModules
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y Z T : Scheme
⊢ (toPresheafOfModules X).IsRightAdjoint

Tactic:
(PresheafOfModules.sheafificationAdjunction (𝟙 X.ringCatSheaf.obj)).isRightAdjoint

Premises used: CategoryTheory.Functor.comp, CategoryTheory.CategoryStruct.id, CategoryTheory.ObjectProperty.FullSubcategory.obj, AlgebraicGeometry.Scheme.ringCatSheaf, AlgebraicGeometry.Scheme.Modules.Hom, ModuleCat.RestrictScalars.obj', CategoryTheory.Adjunction.isRightAdjoint, ModuleCat.RestrictScalars.map', PresheafOfModules.restrictScalarsObj, PresheafOfModules.sheafificationAdjunction, AlgebraicGeometry.Scheme.Modules, AlgebraicGeometry.Scheme.Modules.toPresheafOfModules, SheafOfModules.forget
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y Z T : Scheme
⊢ (toPresheaf X).Faithful

Tactic:
.comp _ (PresheafOfModules.toPresheaf _)

Premises used: TopCat.Presheaf, CategoryTheory.Functor.Faithful.comp, PresheafOfModules.toPresheaf, AlgebraicGeometry.Scheme.Modules.toPresheaf
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y Z T : Scheme
⊢ PreservesLimits (toPresheaf X)

Tactic:
comp_preservesLimits _ (PresheafOfModules.toPresheaf _)

Premises used: TopCat.Presheaf, PresheafOfModules.toPresheaf, AlgebraicGeometry.Scheme.Modules.toPresheaf, CategoryTheory.Limits.comp_preservesLimits
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y Z T : Scheme
⊢ (toPresheaf X).ReflectsIsomorphisms

Tactic:
reflectsIsomorphisms_comp _ (PresheafOfModules.toPresheaf _)

Premises used: CategoryTheory.reflectsIsomorphisms_comp, TopCat.Presheaf, PresheafOfModules.toPresheaf, AlgebraicGeometry.Scheme.Modules.toPresheaf
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X : Scheme
M : X.Modules
U V : X.Opens
i : U ⟶ V
r : (↑Γ(X, V) : Type u)
x : (↑Γ(M, V) : Type u)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
          AddCommGrpCat.carrier) (M.presheaf.map i.op) :
        (a : (↑(M.presheaf.obj (Opposite.op V)) : Type u)) → (↑(M.presheaf.obj (Opposite.op U)) : Type u))
      (r • x) =
    HSMul.hSMul (α := (↑Γ(X, U) : Type u)) (β := (↑(M.presheaf.obj (Opposite.op U)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X.presheaf.map i.op) :
            (a : (↑Γ(X, V) : Type u)) → (↑Γ(X, U) : Type u))
          r :
        (↑Γ(X, U) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier) (M.presheaf.map i.op) :
            (a : (↑(M.presheaf.obj (Opposite.op V)) : Type u)) → (↑(M.presheaf.obj (Opposite.op U)) : Type u))
          x :
        (↑(M.presheaf.obj (Opposite.op U)) : Type u))

Tactic:
M.val.map_smul _ _ _

Premises used: PresheafOfModules.map_smul, SheafOfModules.val
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X : Scheme
M N : X.Modules
φ : M ⟶ N
U : (TopologicalSpace.Opens ↥X)ᵒᵖ
⊢ (Hom.mapPresheaf φ).app U = Hom.app φ (Opposite.unop U)

Tactic:
rfl

Premises used: LinearMap.toAddMonoidHom, AlgebraicGeometry.Scheme.Modules.Hom.app, rfl
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X : Scheme
M N : X.Modules
U : X.Opens
φ : M ⟶ N
r : (↑Γ(X, U) : Type u)
x : (↑Γ(M, U) : Type u)
⊢ (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
          AddCommGrpCat.carrier) (app φ U) :
        (a : (↑Γ(M, U) : Type u)) → (↑Γ(N, U) : Type u))
      (r • x) =
    HSMul.hSMul (β := (↑Γ(N, U) : Type u)) r
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier) (app φ U) :
            (a : (↑Γ(M, U) : Type u)) → (↑Γ(N, U) : Type u))
          x :
        (↑Γ(N, U) : Type u))

Tactic:
(φ.val.app (.op U)).hom.map_smul r x

Premises used: Opposite.op, SheafOfModules.Hom.val, LinearMap.map_smul, ModuleCat.Hom.hom, PresheafOfModules.Hom.app
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X : Scheme
M N : X.Modules
U : X.Opens
φ ψ : M ⟶ N
⊢ app (φ + ψ) U = app φ U + app ψ U

Tactic:
rfl

Premises used: LinearMap.toAddMonoidHom, AlgebraicGeometry.Scheme.Modules.Hom.app, rfl
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X : Scheme
M N : X.Modules
U : X.Opens
φ ψ : M ⟶ N
⊢ app (φ - ψ) U = app φ U - app ψ U

Tactic:
rfl

Premises used: LinearMap.toAddMonoidHom, AlgebraicGeometry.Scheme.Modules.Hom.app, AddMonoidHom.mk', rfl
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X : Scheme
M N : X.Modules
U : X.Opens
⊢ Eq (α := Γ(M, U) ⟶ Γ(N, U)) (app 0 U) 0

Tactic:
rfl

Premises used: LinearMap.toAddMonoidHom, AlgebraicGeometry.Scheme.Modules.Hom.app, rfl
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X : Scheme
U : X.Opens
M : X.Modules
⊢ app (𝟙 M) U = 𝟙 Γ(M, U)

Tactic:
rfl

Premises used: LinearMap.toAddMonoidHom, AlgebraicGeometry.Scheme.Modules.Hom.app, rfl
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X : Scheme
M N K : X.Modules
U : X.Opens
φ : M ⟶ N
ψ : N ⟶ K
⊢ app (φ ≫ ψ) U = app φ U ≫ app ψ U

Tactic:
rfl

Premises used: AlgebraicGeometry.Scheme.Modules.Hom.app, rfl
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X : Scheme
M N : X.Modules
f g : M ⟶ N
H : ∀ (U : X.Opens), Hom.app f U = Hom.app g U
h : f.val = g.val
⊢ f = g

Tactic:
apply SheafOfModules.hom_ext

Premises used: SheafOfModules.hom_ext
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X : Scheme
M N : X.Modules
f g : M ⟶ N
H : ∀ (U : X.Opens), Hom.app f U = Hom.app g U
h :
  ∀ (U : (TopologicalSpace.Opens ↥X)ᵒᵖ) (x : (↑(M.val.obj U) : Type u)),
    Eq (α := (↑(N.val.obj U) : Type u))
      ((ModuleCat.Hom.hom (f.val.app U) : (a : (↑(M.val.obj U) : Type u)) → (↑(N.val.obj U) : Type u)) x :
        (↑(N.val.obj U) : Type u))
      ((ModuleCat.Hom.hom (g.val.app U) : (a : (↑(M.val.obj U) : Type u)) → (↑(N.val.obj U) : Type u)) x :
        (↑(N.val.obj U) : Type u))
⊢ f.val = g.val

Tactic:
ext U x
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X : Scheme
M N : X.Modules
f g : M ⟶ N
H : ∀ (U : X.Opens), Hom.app f U = Hom.app g U
U : (TopologicalSpace.Opens ↥X)ᵒᵖ
x : (↑(M.val.obj U) : Type u)
⊢ Eq (α := (↑(N.val.obj U) : Type u))
    ((ModuleCat.Hom.hom (f.val.app U) : (a : (↑(M.val.obj U) : Type u)) → (↑(N.val.obj U) : Type u)) x :
      (↑(N.val.obj U) : Type u))
    ((ModuleCat.Hom.hom (g.val.app U) : (a : (↑(M.val.obj U) : Type u)) → (↑(N.val.obj U) : Type u)) x :
      (↑(N.val.obj U) : Type u))

Tactic:
congr($(H U.unop) x)

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, id, DFunLike.coe, Opposite.unop
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X : Scheme
M N : X.Modules
f g : M ⟶ N
H : ∀ (U : X.Opens), Hom.app f U = Hom.app g U
U : (TopologicalSpace.Opens ↥X)ᵒᵖ
x : (↑(M.val.obj U) : Type u)
⊢ Eq (α := (↑(N.val.obj U) : Type u))
    ((ModuleCat.Hom.hom (f.val.app U) : (a : (↑(M.val.obj U) : Type u)) → (↑(N.val.obj U) : Type u)) x :
      (↑(N.val.obj U) : Type u))
    ((ModuleCat.Hom.hom (g.val.app U) : (a : (↑(M.val.obj U) : Type u)) → (↑(N.val.obj U) : Type u)) x :
      (↑(N.val.obj U) : Type u))

Tactic:
exact congr($(H U.unop) x)
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X : Scheme
M : X.Modules
⊢ M.presheaf.IsSheaf

Tactic:
SheafOfModules.isSheaf M

Premises used: SheafOfModules.isSheaf, TopCat.Presheaf.IsSheaf, AlgebraicGeometry.Scheme.Modules.presheaf
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X : Scheme
M : X.Modules
⊢ (toPresheaf X).obj M = M.presheaf

Tactic:
rfl

Premises used: rfl, PresheafOfModules.presheaf, AlgebraicGeometry.Scheme.Modules.presheaf
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X : Scheme
M N : X.Modules
φ : M ⟶ N
⊢ (toPresheaf X).map φ = Hom.mapPresheaf φ

Tactic:
rfl

Premises used: AlgebraicGeometry.Scheme.Modules.Hom.mapPresheaf, rfl
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X : Scheme
M N : X.Modules
φ : M ⟶ N
rw :
  (∀ (X_1 : (TopologicalSpace.Opens ↥X)ᵒᵖ), IsIso (((toPresheaf X).map φ).app X_1)) ↔ ∀ (U : X.Opens), IsIso (app φ U)
⊢ IsIso φ ↔ ∀ (U : X.Opens), IsIso (app φ U)

Tactic:
rw [← isIso_iff_of_reflects_iso _ (toPresheaf X), NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app, CategoryTheory.isIso_iff_of_reflects_iso, AlgebraicGeometry.Scheme.Modules.toPresheaf
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X : Scheme
M N : X.Modules
φ : M ⟶ N
⊢ (∀ (X_1 : (TopologicalSpace.Opens ↥X)ᵒᵖ), IsIso (((toPresheaf X).map φ).app X_1)) ↔ ∀ (U : X.Opens), IsIso (app φ U)

Tactic:
simp [Opposite.op_surjective.forall]

Premises used: Function.Surjective.forall, Opposite.op_surjective
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U V : X.Opens
inst : IsIso φ
⊢ IsIso (Hom.app φ U)

Tactic:
Hom.isIso_iff_isIso_app.mp ‹_› _

Premises used: AlgebraicGeometry.Scheme.Modules.Hom.isIso_iff_isIso_app, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X : Scheme
M N : X.Modules
φ : M ⟶ N
U : X.Opens
inst : IsIso φ
hom_inv_id : Hom.app φ U ≫ Hom.app (inv φ) U = 𝟙 Γ(M, U)
⊢ Hom.app (inv φ) U = inv (Hom.app φ U)

Tactic:
apply IsIso.eq_inv_of_hom_inv_id

Premises used: CategoryTheory.IsIso.eq_inv_of_hom_inv_id
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X : Scheme
M N : X.Modules
φ : M ⟶ N
U : X.Opens
inst : IsIso φ
⊢ Hom.app φ U ≫ Hom.app (inv φ) U = 𝟙 Γ(M, U)

Tactic:
simp [← Hom.comp_app]

Premises used: AlgebraicGeometry.Scheme.Modules.Hom.comp_app
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y : Scheme
f : X ⟶ Y
M : X.Modules
U : Y.Opens
⊢ Γ((pushforward f).obj M, U) = Γ(M, f ⁻¹ᵁ U)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y : Scheme
M : X.Modules
f : X ⟶ Y
U V : Y.Opens
i : U ⟶ V
⊢ ((pushforward f).obj M).presheaf.map i.op = M.presheaf.map ((Opens.map f.base).map i).op

Tactic:
rfl

Premises used: Set.Mem, Quiver.Hom.op, rfl
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y : Scheme
M N : X.Modules
f : X ⟶ Y
φ : M ⟶ N
U : Y.Opens
⊢ Hom.app ((pushforward f).map φ) U = Hom.app φ (f ⁻¹ᵁ U)

Tactic:
rfl

Premises used: LinearMap.toAddMonoidHom, AlgebraicGeometry.Scheme.Modules.Hom.app, CategoryTheory.Functor.comp, AlgebraicGeometry.Scheme.Modules.Hom, AlgebraicGeometry.Scheme.Modules, rfl
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U V : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
⊢ (pullback f).IsLeftAdjoint

Tactic:
(pullbackPushforwardAdjunction f).isLeftAdjoint

Premises used: CategoryTheory.Adjunction.isLeftAdjoint, AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U V : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
⊢ (pushforward f).IsRightAdjoint

Tactic:
(pullbackPushforwardAdjunction f).isRightAdjoint

Premises used: CategoryTheory.Adjunction.isRightAdjoint, AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U V : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
⊢ (pushforward f).Additive

Tactic:
Functor.additive_of_preservesBinaryBiproducts _

Premises used: CategoryTheory.Functor.additive_of_preservesBinaryBiproducts
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U V : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
⊢ (pullback f).Additive

Tactic:
Functor.additive_of_preservesBinaryBiproducts _

Premises used: CategoryTheory.Functor.additive_of_preservesBinaryBiproducts
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X : Scheme
M : X.Modules
U : X.Opens
⊢ Hom.app ((pushforwardId X).hom.app M) U = 𝟙 Γ((pushforward (𝟙 X)).obj M, U)

Tactic:
rfl

Premises used: LinearMap.toAddMonoidHom, AlgebraicGeometry.Scheme.Modules.Hom.app, Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X : Scheme
M : X.Modules
U : X.Opens
⊢ Hom.app ((pushforwardId X).inv.app M) U = 𝟙 Γ(Functor.obj (𝟭 X.Modules) M, U)

Tactic:
rfl

Premises used: LinearMap.toAddMonoidHom, AlgebraicGeometry.Scheme.Modules.Hom.app, Set.Mem, setOf, Set.preimage, rfl