awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X : Scheme
⊢ (CategoryTheory.conjugateEquiv CategoryTheory.Adjunction.id (pullbackPushforwardAdjunction (𝟙 X)) :
        (a : pullback (𝟙 X) ⟶ 𝟭 X.Modules) → 𝟭 X.Modules ⟶ pushforward (𝟙 X))
      (pullbackId X).hom =
    (pushforwardId X).inv

Tactic:
SheafOfModules.conjugateEquiv_pullbackId_hom _

Premises used: CategoryTheory.Functor.op, AlgebraicGeometry.Scheme.Modules.pullback, AlgebraicGeometry.Scheme.Modules.pushforward, Set.Mem, Quiver.Hom.op, AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom, setOf, CategoryTheory.Functor.comp, CategoryTheory.Functor.id, TopCat.Presheaf, CategoryTheory.Functor.whiskerRight, AlgebraicGeometry.Scheme.Modules.Hom, Set.preimage, TopologicalSpace.Opens.map, SheafOfModules.conjugateEquiv_pullbackId_hom, CategoryTheory.NatTrans.id, AlgebraicGeometry.Scheme.Modules
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y Z : Scheme
M : X.Modules
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
⊢ Hom.app ((pushforwardComp f g).hom.app M) U = 𝟙 Γ((pushforward f ⋙ pushforward g).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 Y Z : Scheme
M : X.Modules
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
⊢ Hom.app ((pushforwardComp f g).inv.app M) U = 𝟙 Γ((pushforward (f ≫ g)).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 Y : Scheme
M : X.Modules
f g : X ⟶ Y
hf : f = g
U : Y.Opens
⊢ Hom.app ((pushforwardCongr hf).hom.app M) U = M.presheaf.map (Quiver.Hom.op (eqToHom ⋯))

Tactic:
rfl

Premises used: Eq.mpr, AlgebraicGeometry.Scheme.Modules.Hom.app, Set.Mem, CategoryTheory.eqToHom, setOf, Set.preimage, AddMonoidHom.mk', rfl
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y : Scheme
M : X.Modules
f g : X ⟶ Y
hf : f = g
U : Y.Opens
⊢ Hom.app ((pushforwardCongr hf).inv.app M) U = M.presheaf.map (Quiver.Hom.op (eqToHom ⋯))

Tactic:
rfl

Premises used: Eq.mpr, AlgebraicGeometry.Scheme.Modules.Hom.app, Set.Mem, CategoryTheory.eqToHom, setOf, Set.preimage, AddMonoidHom.mk', rfl
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (CategoryTheory.conjugateEquiv ((pullbackPushforwardAdjunction g).comp (pullbackPushforwardAdjunction f))
          (pullbackPushforwardAdjunction (f ≫ g)) :
        (a : pullback (f ≫ g) ⟶ pullback g ⋙ pullback f) → pushforward f ⋙ pushforward g ⟶ pushforward (f ≫ g))
      (pullbackComp f g).inv =
    (pushforwardComp f g).hom

Tactic:
SheafOfModules.conjugateEquiv_pullbackComp_inv _ _

Premises used: CategoryTheory.NatTrans.vcomp, AlgebraicGeometry.Scheme.Modules.pullback, AlgebraicGeometry.Scheme.Modules.pushforward, Set.Mem, AlgebraicGeometry.Scheme.Hom.toRingCatSheafHom, setOf, CategoryTheory.Functor.comp, SheafOfModules.conjugateEquiv_pullbackComp_inv, CategoryTheory.Functor.whiskerRight, AlgebraicGeometry.Scheme.Modules.Hom, Set.preimage, TopologicalSpace.Opens.map, AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction, AlgebraicGeometry.Scheme.Modules
-- 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 ≫ g ≫ h) = pullback ((f ≫ g) ≫ h)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y Z T : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
e₁ : pullback (g ≫ h) ⋙ pullback f ≅ pullback (f ≫ g ≫ h) := pullbackComp f (g ≫ h)
e₂ : (pullback h ⋙ pullback g) ⋙ pullback f ≅ pullback (g ≫ h) ⋙ pullback f :=
  Functor.isoWhiskerRight (pullbackComp g h) (pullback f)
e₃ : pullback h ⋙ pullback g ⋙ pullback f ≅ pullback h ⋙ pullback (f ≫ g) :=
  (pullback h).isoWhiskerLeft (pullbackComp f g)
e₄ : pullback h ⋙ pullback (f ≫ g) ≅ pullback ((f ≫ g) ≫ h) := pullbackComp (f ≫ g) h
change : e₁.inv ≫ e₂.inv ≫ ((pullback h).associator (pullback g) (pullback f)).hom ≫ e₃.hom ≫ e₄.hom = eqToHom ⋯
⊢ (pullbackComp f (g ≫ h)).inv ≫
      Functor.whiskerRight (pullbackComp g h).inv (pullback f) ≫
        ((pullback h).associator (pullback g) (pullback f)).hom ≫
          (pullback h).whiskerLeft (pullbackComp f g).hom ≫ (pullbackComp (f ≫ g) h).hom =
    eqToHom ⋯

Tactic:
change e₁.inv ≫ e₂.inv ≫ (Functor.associator _ _ _).hom ≫ e₃.hom ≫ e₄.hom = _

Premises used: CategoryTheory.Functor.associator, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y Z T : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
e₁ : pullback (g ≫ h) ⋙ pullback f ≅ pullback (f ≫ g ≫ h) := pullbackComp f (g ≫ h)
e₂ : (pullback h ⋙ pullback g) ⋙ pullback f ≅ pullback (g ≫ h) ⋙ pullback f :=
  Functor.isoWhiskerRight (pullbackComp g h) (pullback f)
e₃ : pullback h ⋙ pullback g ⋙ pullback f ≅ pullback h ⋙ pullback (f ≫ g) :=
  (pullback h).isoWhiskerLeft (pullbackComp f g)
e₄ : pullback h ⋙ pullback (f ≫ g) ≅ pullback ((f ≫ g) ≫ h) := pullbackComp (f ≫ g) h
⊢ e₃.hom ≫ e₄.hom = ((pullback h).associator (pullback g) (pullback f)).inv ≫ e₂.hom ≫ e₁.hom

Tactic:
have : e₃.hom ≫ e₄.hom = (Functor.associator _ _ _).inv ≫ e₂.hom ≫ e₁.hom :=
    congr_arg Iso.hom (SheafOfModules.pullback_assoc.{u}
      h.toRingCatSheafHom g.toRingCatSheafHom f.toRingCatSheafHom)
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y Z T : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
e₁ : pullback (g ≫ h) ⋙ pullback f ≅ pullback (f ≫ g ≫ h) := pullbackComp f (g ≫ h)
e₂ : (pullback h ⋙ pullback g) ⋙ pullback f ≅ pullback (g ≫ h) ⋙ pullback f :=
  Functor.isoWhiskerRight (pullbackComp g h) (pullback f)
e₃ : pullback h ⋙ pullback g ⋙ pullback f ≅ pullback h ⋙ pullback (f ≫ g) :=
  (pullback h).isoWhiskerLeft (pullbackComp f g)
e₄ : pullback h ⋙ pullback (f ≫ g) ≅ pullback ((f ≫ g) ≫ h) := pullbackComp (f ≫ g) h
this : e₃.hom ≫ e₄.hom = ((pullback h).associator (pullback g) (pullback f)).inv ≫ e₂.hom ≫ e₁.hom
⊢ e₁.inv ≫ e₂.inv ≫ ((pullback h).associator (pullback g) (pullback f)).hom ≫ e₃.hom ≫ e₄.hom = eqToHom ⋯

Tactic:
simp [this]
-- 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 ≫ 𝟙 Y) = pullback f

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y : Scheme
f : X ⟶ Y
e₁ : pullback (𝟙 Y) ⋙ pullback f ≅ pullback (f ≫ 𝟙 Y) := pullbackComp f (𝟙 Y)
e₂ : pullback (𝟙 Y) ⋙ pullback f ≅ 𝟭 Y.Modules ⋙ pullback f := Functor.isoWhiskerRight (pullbackId Y) (pullback f)
e₃ : 𝟭 Y.Modules ⋙ pullback f ≅ pullback f := (pullback f).leftUnitor
change : e₁.inv ≫ e₂.hom ≫ e₃.hom = eqToHom ⋯
⊢ (pullbackComp f (𝟙 Y)).inv ≫ Functor.whiskerRight (pullbackId Y).hom (pullback f) ≫ (pullback f).leftUnitor.hom =
    eqToHom ⋯

Tactic:
change e₁.inv ≫ e₂.hom ≫ e₃.hom = _

Premises used: CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y : Scheme
f : X ⟶ Y
e₁ : pullback (𝟙 Y) ⋙ pullback f ≅ pullback (f ≫ 𝟙 Y) := pullbackComp f (𝟙 Y)
e₂ : pullback (𝟙 Y) ⋙ pullback f ≅ 𝟭 Y.Modules ⋙ pullback f := Functor.isoWhiskerRight (pullbackId Y) (pullback f)
e₃ : 𝟭 Y.Modules ⋙ pullback f ≅ pullback f := (pullback f).leftUnitor
⊢ e₁.hom = e₂.hom ≫ e₃.hom

Tactic:
have : e₁.hom = e₂.hom ≫ e₃.hom :=
    congr_arg Iso.hom (SheafOfModules.pullback_id_comp.{u} f.toRingCatSheafHom)
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y : Scheme
f : X ⟶ Y
e₁ : pullback (𝟙 Y) ⋙ pullback f ≅ pullback (f ≫ 𝟙 Y) := pullbackComp f (𝟙 Y)
e₂ : pullback (𝟙 Y) ⋙ pullback f ≅ 𝟭 Y.Modules ⋙ pullback f := Functor.isoWhiskerRight (pullbackId Y) (pullback f)
e₃ : 𝟭 Y.Modules ⋙ pullback f ≅ pullback f := (pullback f).leftUnitor
this : e₁.hom = e₂.hom ≫ e₃.hom
⊢ e₁.inv ≫ e₂.hom ≫ e₃.hom = eqToHom ⋯

Tactic:
simp [← this]
-- 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 (𝟙 X ≫ f) = pullback f

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y : Scheme
f : X ⟶ Y
e₁ : pullback f ⋙ pullback (𝟙 X) ≅ pullback (𝟙 X ≫ f) := pullbackComp (𝟙 X) f
e₂ : pullback f ⋙ pullback (𝟙 X) ≅ pullback f ⋙ 𝟭 X.Modules := (pullback f).isoWhiskerLeft (pullbackId X)
e₃ : pullback f ⋙ 𝟭 X.Modules ≅ pullback f := (pullback f).rightUnitor
change : e₁.inv ≫ e₂.hom ≫ e₃.hom = eqToHom ⋯
⊢ (pullbackComp (𝟙 X) f).inv ≫ (pullback f).whiskerLeft (pullbackId X).hom ≫ (pullback f).rightUnitor.hom = eqToHom ⋯

Tactic:
change e₁.inv ≫ e₂.hom ≫ e₃.hom = _

Premises used: CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y : Scheme
f : X ⟶ Y
e₁ : pullback f ⋙ pullback (𝟙 X) ≅ pullback (𝟙 X ≫ f) := pullbackComp (𝟙 X) f
e₂ : pullback f ⋙ pullback (𝟙 X) ≅ pullback f ⋙ 𝟭 X.Modules := (pullback f).isoWhiskerLeft (pullbackId X)
e₃ : pullback f ⋙ 𝟭 X.Modules ≅ pullback f := (pullback f).rightUnitor
⊢ e₁.hom = e₂.hom ≫ e₃.hom

Tactic:
have : e₁.hom = e₂.hom ≫ e₃.hom :=
    congr_arg Iso.hom (SheafOfModules.pullback_comp_id.{u} f.toRingCatSheafHom)
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y : Scheme
f : X ⟶ Y
e₁ : pullback f ⋙ pullback (𝟙 X) ≅ pullback (𝟙 X ≫ f) := pullbackComp (𝟙 X) f
e₂ : pullback f ⋙ pullback (𝟙 X) ≅ pullback f ⋙ 𝟭 X.Modules := (pullback f).isoWhiskerLeft (pullbackId X)
e₃ : pullback f ⋙ 𝟭 X.Modules ≅ pullback f := (pullback f).rightUnitor
this : e₁.hom = e₂.hom ≫ e₃.hom
⊢ e₁.inv ≫ e₂.hom ≫ e₃.hom = eqToHom ⋯

Tactic:
simp [← this]
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y : Scheme
M : Y.Modules
f : X ⟶ Y
inst : IsOpenImmersion f
U : TopologicalSpace.Opens ↥X
⊢ Γ(M.restrict f, U) = Γ(M, f ''ᵁ U)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y : Scheme
M : Y.Modules
f : X ⟶ Y
inst : IsOpenImmersion f
U V : TopologicalSpace.Opens ↥X
i : U ⟶ V
⊢ (M.restrict f).presheaf.map i.op = M.presheaf.map ((Hom.opensFunctor f).map i).op

Tactic:
rfl

Premises used: Set.Mem, Quiver.Hom.op, 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
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
⊢ IsIso (X := pushforward f ⋙ restrictFunctor f) (CategoryTheory.Adjunction.counit (restrictAdjunction f))

Tactic:
inferInstanceAs (IsIso <| (restrictFunctorAdjCounitIso f).hom)

Premises used: _private.0.AlgebraicGeometry.Scheme.Modules.instIsIsoFunctorCounitRestrictAdjunction._proof_1
-- 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
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
⊢ (restrictFunctor f).IsLeftAdjoint

Tactic:
(restrictAdjunction f).isLeftAdjoint

Premises used: CategoryTheory.Adjunction.isLeftAdjoint, AlgebraicGeometry.Scheme.Modules.restrictAdjunction
-- 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
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
⊢ (pushforward f).Full

Tactic:
(restrictAdjunction f).fullyFaithfulROfIsIsoCounit.full

Premises used: CategoryTheory.Adjunction.fullyFaithfulROfIsIsoCounit, CategoryTheory.Functor.FullyFaithful.full, AlgebraicGeometry.Scheme.Modules.restrictAdjunction
-- 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
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
⊢ (pushforward f).Faithful

Tactic:
(restrictAdjunction f).fullyFaithfulROfIsIsoCounit.faithful

Premises used: CategoryTheory.Adjunction.fullyFaithfulROfIsIsoCounit, CategoryTheory.Functor.FullyFaithful.faithful, AlgebraicGeometry.Scheme.Modules.restrictAdjunction
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
M : Y.Modules
U : Y.Opens
⊢ Eq (α := Γ(Functor.obj (𝟭 Y.Modules) M, U) ⟶ Γ((restrictFunctor f ⋙ pushforward f).obj M, U))
    (Hom.app (NatTrans.app (CategoryTheory.Adjunction.unit (restrictAdjunction f)) M) U)
    (M.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))

Tactic:
rfl

Premises used: AlgebraicGeometry.Scheme.Modules.Hom.app, Set.Mem, CategoryTheory.homOfLE, AddMonoidHom.mk', rfl
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
M : X.Modules
U : X.Opens
⊢ Eq (α := Γ((pushforward f ⋙ restrictFunctor f).obj M, U) ⟶ Γ(Functor.obj (𝟭 X.Modules) M, U))
    (Hom.app (NatTrans.app (CategoryTheory.Adjunction.counit (restrictAdjunction f)) M) U)
    (M.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))

Tactic:
rfl

Premises used: Eq.mpr, AlgebraicGeometry.Scheme.Modules.Hom.app, Set.Mem, CategoryTheory.eqToHom, setOf, Set.preimage, CategoryTheory.homOfLE, AddMonoidHom.mk', Set.image, 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
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
x : X.Opens
⊢ Functor.obj (𝟭 X.Opens) x = 𝟙 X ''ᵁ x

Tactic:
simp
-- 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
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
h :
  ∀ (x : (TopologicalSpace.Opens ↥X)ᵒᵖ),
    NatTrans.app
        (InducedCategory.Hom.hom
          (CategoryStruct.comp (Y :=
            Functor.obj
              ((Hom.opensFunctor (𝟙 X)).sheafPushforwardContinuous RingCat (Opens.grothendieckTopology ↥X)
                (Opens.grothendieckTopology ↥X))
              X.ringCatSheaf)
            {
              hom :=
                Functor.whiskerRight
                  { app := fun (U : (TopologicalSpace.Opens ↥X)ᵒᵖ) ↦ Iso.inv (Hom.appIso (𝟙 X) (Opposite.unop U)),
                    naturality := ⋯ }
                  (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                    (CD := RingCat.carrier)) }
            (NatTrans.app
              (Functor.sheafPushforwardContinuousNatTrans
                (Iso.hom (NatIso.ofComponents (fun (x : X.Opens) ↦ eqToIso ⋯) ⋯)) RingCat
                (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥X))
              X.ringCatSheaf)))
        x =
      (InducedCategory.Hom.hom (𝟙 X.ringCatSheaf)).app x
⊢ Eq (α :=
    X.ringCatSheaf ⟶
      Functor.obj
        (Functor.sheafPushforwardContinuous (𝟭 X.Opens) RingCat (Opens.grothendieckTopology ↥X)
          (Opens.grothendieckTopology ↥X))
        X.ringCatSheaf)
    (CategoryStruct.comp (Y :=
      Functor.obj
        ((Hom.opensFunctor (𝟙 X)).sheafPushforwardContinuous RingCat (Opens.grothendieckTopology ↥X)
          (Opens.grothendieckTopology ↥X))
        X.ringCatSheaf)
      {
        hom :=
          Functor.whiskerRight
            { app := fun (U : (TopologicalSpace.Opens ↥X)ᵒᵖ) ↦ Iso.inv (Hom.appIso (𝟙 X) (Opposite.unop U)),
              naturality := ⋯ }
            (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
              RingCat.carrier)) }
      (NatTrans.app
        (Functor.sheafPushforwardContinuousNatTrans (Iso.hom (NatIso.ofComponents (fun (x : X.Opens) ↦ eqToIso ⋯) ⋯))
          RingCat (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥X))
        X.ringCatSheaf))
    (𝟙 X.ringCatSheaf)

Tactic:
ext : 3
-- 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
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
x : (TopologicalSpace.Opens ↥X)ᵒᵖ
⊢ NatTrans.app
      (InducedCategory.Hom.hom
        (CategoryStruct.comp (Y :=
          Functor.obj
            ((Hom.opensFunctor (𝟙 X)).sheafPushforwardContinuous RingCat (Opens.grothendieckTopology ↥X)
              (Opens.grothendieckTopology ↥X))
            X.ringCatSheaf)
          {
            hom :=
              Functor.whiskerRight
                { app := fun (U : (TopologicalSpace.Opens ↥X)ᵒᵖ) ↦ Iso.inv (Hom.appIso (𝟙 X) (Opposite.unop U)),
                  naturality := ⋯ }
                (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
                  RingCat.carrier)) }
          (NatTrans.app
            (Functor.sheafPushforwardContinuousNatTrans
              (Iso.hom (NatIso.ofComponents (fun (x : X.Opens) ↦ eqToIso ⋯) ⋯)) RingCat (Opens.grothendieckTopology ↥X)
              (Opens.grothendieckTopology ↥X))
            X.ringCatSheaf)))
      x =
    (InducedCategory.Hom.hom (𝟙 X.ringCatSheaf)).app x

Tactic:
simp [← Functor.map_comp, SheafedSpace.sheaf]

Premises used: CategoryTheory.Functor.map_comp, AlgebraicGeometry.SheafedSpace.sheaf
-- 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
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
⊢ U = 𝟙 X ''ᵁ U

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X : Scheme
M : X.Modules
U : X.Opens
⊢ Hom.app (NatTrans.app (Iso.hom restrictFunctorId) M) U = M.presheaf.map (Quiver.Hom.op (eqToHom ⋯))

Tactic:
rfl

Premises used: Eq.mpr, AlgebraicGeometry.Scheme.Modules.Hom.app, Set.Mem, CategoryTheory.eqToHom, setOf, AddMonoidHom.mk', Set.image, 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
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
⊢ 𝟙 X ''ᵁ U = U

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X : Scheme
M : X.Modules
U : X.Opens
⊢ Hom.app (NatTrans.app (Iso.inv restrictFunctorId) M) U = M.presheaf.map (Quiver.Hom.op (eqToHom ⋯))

Tactic:
rfl

Premises used: Eq.mpr, AlgebraicGeometry.Scheme.Modules.Hom.app, Set.Mem, CategoryTheory.eqToHom, setOf, AddMonoidHom.mk', Set.image, 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
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
this :
  (Hom.opensFunctor f ⋙ Hom.opensFunctor g).IsContinuous (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥Z)
x : X.Opens
⊢ (Hom.opensFunctor f ⋙ Hom.opensFunctor g).obj x = (f ≫ g) ''ᵁ x

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y Z T : Scheme
M_1 N K : X.Modules
φ : M_1 ⟶ N
U V : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
M : Z.Modules
⊢ g ''ᵁ Opposite.unop ((Hom.opensFunctor f).op.obj (Opposite.op U)) = (f ≫ g) ''ᵁ Opposite.unop (Opposite.op U)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y Z : Scheme
U : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
M : Z.Modules
⊢ Eq (α := Γ((restrictFunctor (f ≫ g)).obj M, U) ⟶ Γ((restrictFunctor g ⋙ restrictFunctor f).obj M, U))
    (Hom.app (NatTrans.app (Iso.hom (restrictFunctorComp f g)) M) U) (M.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))

Tactic:
rfl

Premises used: Eq.mpr, AlgebraicGeometry.Scheme.Modules.Hom.app, Set.Mem, CategoryTheory.eqToHom, setOf, AddMonoidHom.mk', Set.image, rfl
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y Z T : Scheme
M_1 N K : X.Modules
φ : M_1 ⟶ N
U V : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
M : Z.Modules
⊢ (f ≫ g) ''ᵁ Opposite.unop (Opposite.op U) = g ''ᵁ Opposite.unop ((Hom.opensFunctor f).op.obj (Opposite.op U))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y Z : Scheme
U : X.Opens
f : X ⟶ Y
g : Y ⟶ Z
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
M : Z.Modules
⊢ Eq (α := Γ((restrictFunctor g ⋙ restrictFunctor f).obj M, U) ⟶ Γ((restrictFunctor (f ≫ g)).obj M, U))
    (Hom.app (NatTrans.app (Iso.inv (restrictFunctorComp f g)) M) U) (M.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))

Tactic:
rfl

Premises used: Eq.mpr, AlgebraicGeometry.Scheme.Modules.Hom.app, Set.Mem, CategoryTheory.eqToHom, setOf, AddMonoidHom.mk', Set.image, rfl
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U V : X.Opens
f_1 : X ⟶ Y
g_1 : Y ⟶ Z
inst : IsOpenImmersion f_1
inst_1 : IsOpenImmersion g_1
f g : X ⟶ Y
hf : f = g
inst_2 : IsOpenImmersion f
inst_3 : IsOpenImmersion g
x : X.Opens
⊢ g ''ᵁ x = f ''ᵁ x

Tactic:
simp [hf]
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y Z T : Scheme
M N K : X.Modules
φ : M ⟶ N
U V : X.Opens
f_1 : X ⟶ Y
g : Y ⟶ Z
inst : IsOpenImmersion f_1
inst_1 : IsOpenImmersion g
f : X ⟶ Y
inst_2 : IsOpenImmersion f
x : (TopologicalSpace.Opens ↥X)ᵒᵖ
inst_3 : IsOpenImmersion f
⊢ Eq (α :=
    X.ringCatSheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X)).obj x ⟶
      (ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology ↥X))
            (Functor.obj
              ((Hom.opensFunctor f).sheafPushforwardContinuous RingCat (Opens.grothendieckTopology ↥X)
                (Opens.grothendieckTopology ↥Y))
              Y.ringCatSheaf)).obj
        x)
    (NatTrans.app
      (InducedCategory.Hom.hom
        (CategoryStruct.comp (Y :=
          Functor.obj
            ((Hom.opensFunctor f).sheafPushforwardContinuous RingCat (Opens.grothendieckTopology ↥X)
              (Opens.grothendieckTopology ↥Y))
            Y.ringCatSheaf)
          {
            hom :=
              Functor.whiskerRight
                { app := fun (U : (TopologicalSpace.Opens ↥X)ᵒᵖ) ↦ Iso.inv (Hom.appIso f (Opposite.unop U)),
                  naturality := ⋯ }
                (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
                  RingCat.carrier)) }
          (NatTrans.app
            (Functor.sheafPushforwardContinuousNatTrans
              (Iso.hom (NatIso.ofComponents (fun (x : X.Opens) ↦ eqToIso ⋯) ⋯)) RingCat (Opens.grothendieckTopology ↥X)
              (Opens.grothendieckTopology ↥Y))
            Y.ringCatSheaf)))
      x)
    (NatTrans.app
      (InducedCategory.Hom.hom
        {
          hom :=
            Functor.whiskerRight
              { app := fun (U : (TopologicalSpace.Opens ↥X)ᵒᵖ) ↦ Iso.inv (Hom.appIso f (Opposite.unop U)),
                naturality := ⋯ }
              (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
                RingCat.carrier)) })
      x)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y Z T : Scheme
M_1 N K : X.Modules
φ : M_1 ⟶ N
U V : X.Opens
f_1 : X ⟶ Y
g_1 : Y ⟶ Z
inst : IsOpenImmersion f_1
inst_1 : IsOpenImmersion g_1
f g : X ⟶ Y
hf : f = g
inst_2 : IsOpenImmersion f
inst_3 : IsOpenImmersion g
M : Y.Modules
⊢ g ''ᵁ Opposite.unop (Opposite.op U) = f ''ᵁ Opposite.unop (Opposite.op U)

Tactic:
simp [hf]
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y : Scheme
U : X.Opens
f g : X ⟶ Y
hf : f = g
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
M : Y.Modules
⊢ Eq (α := Γ((restrictFunctor f).obj M, U) ⟶ Γ((restrictFunctor g).obj M, U))
    (Hom.app (NatTrans.app (Iso.hom (restrictFunctorCongr hf)) M) U) (M.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))

Tactic:
rfl

Premises used: Eq.mpr, AlgebraicGeometry.Scheme.Modules.Hom.app, Set.Mem, CategoryTheory.eqToHom, setOf, AddMonoidHom.mk', Set.image, rfl
-- Module: Mathlib.AlgebraicGeometry.Modules.Sheaf
Goal:
X Y Z T : Scheme
M_1 N K : X.Modules
φ : M_1 ⟶ N
U V : X.Opens
f_1 : X ⟶ Y
g_1 : Y ⟶ Z
inst : IsOpenImmersion f_1
inst_1 : IsOpenImmersion g_1
f g : X ⟶ Y
hf : f = g
inst_2 : IsOpenImmersion f
inst_3 : IsOpenImmersion g
M : Y.Modules
⊢ f ''ᵁ Opposite.unop (Opposite.op U) = g ''ᵁ Opposite.unop (Opposite.op U)

Tactic:
simp [hf]