awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X_1 : Scheme
U : X_1.Opens
X_2 Y : Scheme
f_1 : X_2 ⟶ Y
K : Type u
inst : Field K
X : Scheme
f : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)
rw :
  CategoryStruct.comp (Y :=
      Spec
        (X.residueField
          ((X.fromSpecResidueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))
            ((Spec.map (f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K))) (closedPoint K) :
              ↥(Spec (X.residueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K))))))))
      (Spec.map
        (descResidueField
          (stalkClosedPointTo
            (Spec.map (f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)) ≫
              X.fromSpecResidueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K))))))
      (X.fromSpecResidueField
        ((X.fromSpecResidueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))
          ((Spec.map (f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K))) (closedPoint K) :
            ↥(Spec (X.residueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K))))))) =
    CategoryStruct.comp (Y :=
      Spec
        (X.residueField
          ((X.fromSpecResidueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))
            ((Spec.map (f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K))) (closedPoint K) :
              ↥(Spec (X.residueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K))))))))
      (Spec.map (f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)) ≫
        Spec.map (Iso.hom (residueFieldCongr ⋯)))
      (X.fromSpecResidueField
        ((X.fromSpecResidueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))
          ((Spec.map (f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K))) (closedPoint K) :
            ↥(Spec (X.residueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))))))
⊢ Eq (α :=
    X.residueField
        ((X.fromSpecResidueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))
          ((Spec.map (f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K))) (closedPoint K) :
            ↥(Spec (X.residueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))))) ⟶
      CommRingCat.of K)
    (descResidueField
      (stalkClosedPointTo
        (Spec.map (f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)) ≫
          X.fromSpecResidueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))))
    (Iso.hom (residueFieldCongr ⋯) ≫ f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K))

Tactic:
rw [← Spec.map_inj, Spec.map_comp, ← cancel_mono (X.fromSpecResidueField _)]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.fromSpecResidueField, AlgebraicGeometry.Spec.map_comp, AlgebraicGeometry.Spec.map_inj
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X_1 : Scheme
U : X_1.Opens
X_2 Y : Scheme
f_1 : X_2 ⟶ Y
K : Type u
inst : Field K
X : Scheme
f : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)
⊢ CategoryStruct.comp (Y :=
      Spec
        (X.residueField
          ((X.fromSpecResidueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))
            ((Spec.map (f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K))) (closedPoint K) :
              ↥(Spec (X.residueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K))))))))
      (Spec.map
        (descResidueField
          (stalkClosedPointTo
            (Spec.map (f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)) ≫
              X.fromSpecResidueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K))))))
      (X.fromSpecResidueField
        ((X.fromSpecResidueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))
          ((Spec.map (f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K))) (closedPoint K) :
            ↥(Spec (X.residueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K))))))) =
    CategoryStruct.comp (Y :=
      Spec
        (X.residueField
          ((X.fromSpecResidueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))
            ((Spec.map (f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K))) (closedPoint K) :
              ↥(Spec (X.residueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K))))))))
      (Spec.map (f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)) ≫
        Spec.map (Iso.hom (residueFieldCongr ⋯)))
      (X.fromSpecResidueField
        ((X.fromSpecResidueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))
          ((Spec.map (f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K))) (closedPoint K) :
            ↥(Spec (X.residueField (f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))))))

Tactic:
grind [Scheme.descResidueField_stalkClosedPointTo_fromSpecResidueField,
      Scheme.fromSpecResidueField_apply,
      Scheme.residueFieldCongr_fromSpecResidueField]

Premises used: AlgebraicGeometry.Scheme.residueFieldCongr_fromSpecResidueField, AlgebraicGeometry.Scheme.descResidueField_stalkClosedPointTo_fromSpecResidueField, AlgebraicGeometry.Scheme.fromSpecResidueField_apply
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
x : ↥U
⊢ U.ι x = (↑x : ↥X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
U : X.Opens
⊢ IsOpenImmersion U.ι

Tactic:
inferInstanceAs (IsOpenImmersion (X.ofRestrict _))

Premises used: _private.0.AlgebraicGeometry.Scheme.Opens.instIsOpenImmersionι._proof_1
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
⊢ ↥(↑U : Scheme) = (↑(↑U : Set ↥X) : Type u)

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
V : (↑U : Scheme).Opens
⊢ Γ((↑U : Scheme), V) = Γ(X, U.ι ''ᵁ V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
P : ↥(↑U : Scheme) → Prop
⊢ (∀ (x : ↥(↑U : Scheme)), P x) ↔ ∀ (x : ↥X) (hx : x ∈ U), P (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx)

Tactic:
Subtype.forall

Premises used: Set.Mem, Subtype.forall
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
P : ↥(↑U : Scheme) → Prop
⊢ (∃ (x : ↥(↑U : Scheme)), P x) ↔ ∃ (x : ↥X) (hx : x ∈ U), P (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hx)

Tactic:
Subtype.exists

Premises used: Set.Mem, Subtype.exists
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
V W : (TopologicalSpace.Opens ↥(↑U : Scheme))ᵒᵖ
i : V ⟶ W
⊢ (↑U : Scheme).presheaf.map i = X.presheaf.map ((Hom.opensFunctor U.ι).map i.unop).op

Tactic:
rfl

Premises used: Set.Mem, Quiver.Hom.op, TopologicalSpace.Opens.inclusion', rfl
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
⊢ Hom.app U.ι V = X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))

Tactic:
rfl

Premises used: Set.Mem, CategoryTheory.homOfLE, rfl
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
⊢ Hom.appTop U.ι = X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))

Tactic:
rfl

Premises used: Set.Mem, Set.univ, setOf, Set.preimage, CategoryTheory.homOfLE, rfl
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
W : (↑U : Scheme).Opens
e : W ≤ U.ι ⁻¹ᵁ V
simp : X.presheaf.map (Quiver.Hom.op (homOfLE ⋯) ≫ Quiver.Hom.op (homOfLE ⋯)) = X.presheaf.map (homOfLE ⋯).op
⊢ Hom.appLE U.ι V W e = X.presheaf.map (homOfLE ⋯).op

Tactic:
simp only [Hom.appLE, ι_app, toScheme_presheaf_map, Quiver.Hom.unop_op,
    Hom.opensFunctor_map_homOfLE, ← Functor.map_comp]

Premises used: AlgebraicGeometry.Scheme.Hom.opensFunctor_map_homOfLE, Quiver.Hom.unop_op, AlgebraicGeometry.Scheme.Hom.appLE, AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_map, CategoryTheory.Functor.map_comp, AlgebraicGeometry.Scheme.Opens.ι_app
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
W : (↑U : Scheme).Opens
e : W ≤ U.ι ⁻¹ᵁ V
⊢ X.presheaf.map (Quiver.Hom.op (homOfLE ⋯) ≫ Quiver.Hom.op (homOfLE ⋯)) = X.presheaf.map (homOfLE ⋯).op

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
V : (↑U : Scheme).Opens
⊢ Hom.appIso U.ι V = Iso.refl Γ(X, U.ι ''ᵁ V)

Tactic:
X.ofRestrict_appIso _ _

Premises used: AlgebraicGeometry.Scheme.ofRestrict_appIso, AlgebraicGeometry.Scheme.Opens.ι, AlgebraicGeometry.Scheme.Opens.toScheme
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
⊢ Hom.opensRange U.ι = U

Tactic:
Opens.ext Subtype.range_val

Premises used: TopologicalSpace.Opens.ext, Subtype.range_val
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
⊢ Set.range (ι := ↥(↑U : Scheme)) ⇑U.ι = (↑U : Set ↥X)

Tactic:
Subtype.range_val

Premises used: Subtype.range_val
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
⊢ U.ι ''ᵁ ⊤ = U

Tactic:
U.isOpenEmbedding_obj_top

Premises used: TopologicalSpace.Opens.isOpenEmbedding_obj_top
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
W : (↑U : Scheme).Opens
simp_rw : U.ι ''ᵁ W ≤ U.ι ''ᵁ ⊤
⊢ U.ι ''ᵁ W ≤ U

Tactic:
simp_rw [← U.ι_image_top]

Premises used: AlgebraicGeometry.Scheme.Opens.ι_image_top
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
W : (↑U : Scheme).Opens
⊢ U.ι ''ᵁ W ≤ U.ι ''ᵁ ⊤

Tactic:
U.ι.image_mono le_top

Premises used: AlgebraicGeometry.Scheme.Hom.image_mono, le_top, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
W : (↑U : Scheme).Opens
⊢ U.ι ''ᵁ W ≤ U.ι ''ᵁ ⊤

Tactic:
exact U.ι.image_mono le_top

Premises used: AlgebraicGeometry.Scheme.Hom.image_mono, le_top, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
⊢ U.ι ⁻¹ᵁ U = ⊤

Tactic:
Opens.inclusion'_map_eq_top _

Premises used: TopologicalSpace.Opens.inclusion'_map_eq_top
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
x : ↥U
V : (↑U : Scheme).Opens
⊢ (↑x : ↥X) ∈ U.ι ''ᵁ V ↔ x ∈ V

Tactic:
U.ι.apply_mem_image_iff

Premises used: Set.Mem, AlgebraicGeometry.Scheme.Hom.apply_mem_image_iff, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
U : X.Opens
simp : IsIso (X := Γ(X, U)) (Y := Γ((↑U : Scheme), ⊤)) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
⊢ IsIso (Hom.appLE U.ι U ⊤ ⋯)

Tactic:
simp only [ι, ofRestrict_appLE]

Premises used: AlgebraicGeometry.Scheme.ofRestrict_appLE, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
U : X.Opens
change : IsIso (X.presheaf.map (Quiver.Hom.op (Iso.hom (eqToIso ⋯))))
⊢ IsIso (X := Γ(X, U)) (Y := Γ((↑U : Scheme), ⊤)) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))

Tactic:
change IsIso (X.presheaf.map (eqToIso U.ι_image_top).hom.op)

Premises used: CategoryTheory.IsIso, Quiver.Hom.op, CategoryTheory.eqToIso, CategoryTheory.Functor.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.Opens.ι_image_top, CategoryTheory.Iso.hom, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
U : X.Opens
⊢ IsIso (X.presheaf.map (Quiver.Hom.op (Iso.hom (eqToIso ⋯))))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
U : X.Opens
⊢ U.ι ''ᵁ unop (op (U.ι ⁻¹ᵁ U)) = U

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
⊢ Hom.app U.ι U = X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))

Tactic:
rfl

Premises used: Eq.mpr, Set.Mem, CategoryTheory.eqToHom, setOf, CategoryTheory.homOfLE, Set.image, rfl
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
V W : (↑U : Scheme).Opens
e : U.ι ''ᵁ V = U.ι ''ᵁ W
⊢ X.presheaf.map (Quiver.Hom.op (eqToHom e)) = (↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom ⋯))

Tactic:
rfl

Premises used: Eq.mpr, IsOpenMap.functorMap, Set.Mem, Quiver.Hom.op, CategoryTheory.eqToHom, setOf, Set.image, rfl
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
simp : (∃ (x : ↥X), x ∈ U) ↔ (↑U : Set ↥X).Nonempty
⊢ Nonempty.{u + 1} ↥(↑U : Scheme) ↔ (↑U : Set ↥X).Nonempty

Tactic:
simp only [toScheme_carrier, SetLike.coe_sort_coe, nonempty_subtype]

Premises used: SetLike.coe_sort_coe, AlgebraicGeometry.Scheme.Opens.toScheme_carrier, nonempty_subtype
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
⊢ (∃ (x : ↥X), x ∈ U) ↔ (↑U : Set ↥X).Nonempty

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
V : (↑U : Scheme).Opens
x : ↥U
hx : x ∈ V
⊢ (↑U : Scheme).presheaf.germ V x hx ≫ (U.stalkIso x).hom = X.presheaf.germ (U.ι ''ᵁ V) (↑x : ↥X) ⋯

Tactic:
PresheafedSpace.restrictStalkIso_hom_eq_germ _ U.isOpenEmbedding _ _ _

Premises used: Set.Mem, AlgebraicGeometry.LocallyRingedSpace.toTopCat, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_hom_eq_germ, TopologicalSpace.Opens.isOpenEmbedding
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
V : (↑U : Scheme).Opens
x : ↥U
hx : x ∈ V
⊢ X.presheaf.germ (U.ι ''ᵁ V) (↑x : ↥X) ⋯ ≫ (U.stalkIso x).inv = (↑U : Scheme).presheaf.germ V x hx

Tactic:
PresheafedSpace.restrictStalkIso_inv_eq_germ X.toPresheafedSpace U.isOpenEmbedding V x hx

Premises used: Set.Mem, AlgebraicGeometry.LocallyRingedSpace.toTopCat, TopologicalSpace.Opens.isOpenEmbedding, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
x : ↥U
rw : 𝟙 ((↑U : Scheme).presheaf.stalk x) = (U.stalkIso x).hom ≫ Hom.stalkMap U.ι x
⊢ (U.stalkIso x).inv = Hom.stalkMap U.ι x

Tactic:
rw [← Category.comp_id (U.stalkIso x).inv, Iso.inv_comp_eq]

Premises used: CategoryTheory.Iso.inv_comp_eq, CategoryTheory.Category.comp_id, AlgebraicGeometry.Scheme.Opens.stalkIso, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
x : ↥U
ih :
  ∀ (U_1 : TopologicalSpace.Opens ↥(↑U : Scheme)) (hxU : x ∈ U_1),
    (↑U : Scheme).presheaf.germ U_1 x hxU ≫ 𝟙 ((↑U : Scheme).presheaf.stalk x) =
      (↑U : Scheme).presheaf.germ U_1 x hxU ≫ (U.stalkIso x).hom ≫ Hom.stalkMap U.ι x
⊢ 𝟙 ((↑U : Scheme).presheaf.stalk x) = (U.stalkIso x).hom ≫ Hom.stalkMap U.ι x

Tactic:
apply TopCat.Presheaf.stalk_hom_ext

Premises used: TopCat.Presheaf.stalk_hom_ext
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
x : ↥U
W : TopologicalSpace.Opens ↥(↑U : Scheme)
hxW : x ∈ W
ih : (↑U : Scheme).presheaf.germ W x hxW = X.presheaf.germ (U.ι ''ᵁ W) (↑x : ↥X) ⋯ ≫ Hom.stalkMap U.ι x
⊢ (↑U : Scheme).presheaf.germ W x hxW ≫ 𝟙 ((↑U : Scheme).presheaf.stalk x) =
    (↑U : Scheme).presheaf.germ W x hxW ≫ (U.stalkIso x).hom ≫ Hom.stalkMap U.ι x

Tactic:
simp only [Category.comp_id, U.germ_stalkIso_hom_assoc]

Premises used: CategoryTheory.Category.comp_id, AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom_assoc
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
x : ↥U
W : TopologicalSpace.Opens ↥(↑U : Scheme)
hxW : x ∈ W
⊢ Eq (α := X.presheaf.obj (op (U.ι ''ᵁ W)) ⟶ (↑U : Scheme).presheaf.stalk x)
    (Hom.app U.ι (U.ι ''ᵁ W) ≫ (↑U : Scheme).presheaf.germ (U.ι ⁻¹ᵁ U.ι ''ᵁ W) x ⋯)
    (X.presheaf.germ (U.ι ''ᵁ W) (U.ι x) ⋯ ≫ Hom.stalkMap U.ι x)

Tactic:
(Scheme.Hom.germ_stalkMap U.ι (U.ι ''ᵁ W) x ⟨_, hxW, rfl⟩).symm

Premises used: AlgebraicGeometry.Scheme.Hom.opensFunctor, AlgebraicGeometry.Scheme.Hom.germ_stalkMap, And.intro, Exists.intro, AlgebraicGeometry.Scheme.Opens.ι, Eq.symm, CategoryTheory.Functor.obj, rfl
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
x : ↥U
W : TopologicalSpace.Opens ↥(↑U : Scheme)
hxW : x ∈ W
h :
  ((↑U : Scheme).presheaf.obj (op W) ⟶ (↑U : Scheme).presheaf.stalk x) =
      (X.presheaf.obj (op (U.ι ''ᵁ W)) ⟶ (↑U : Scheme).presheaf.stalk x) →
    Eq (α := (↑U : Scheme).presheaf.obj (op W) ⟶ (↑U : Scheme).presheaf.stalk x) ((↑U : Scheme).presheaf.germ W x hxW)
      (Hom.app U.ι (U.ι ''ᵁ W) ≫ (↑U : Scheme).presheaf.germ (U.ι ⁻¹ᵁ U.ι ''ᵁ W) x ⋯)
⊢ (↑U : Scheme).presheaf.germ W x hxW = X.presheaf.germ (U.ι ''ᵁ W) (↑x : ↥X) ⋯ ≫ Hom.stalkMap U.ι x

Tactic:
convert! (Scheme.Hom.germ_stalkMap U.ι (U.ι ''ᵁ W) x ⟨_, hxW, rfl⟩).symm

Premises used: AlgebraicGeometry.Scheme.Hom.opensFunctor, AlgebraicGeometry.Scheme.Hom.germ_stalkMap, And.intro, Exists.intro, AlgebraicGeometry.Scheme.Opens.ι, Eq.symm, CategoryTheory.Functor.obj, rfl
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
x : ↥U
W : TopologicalSpace.Opens ↥(↑U : Scheme)
hxW : x ∈ W
e_1 :
  ((↑U : Scheme).presheaf.obj (op W) ⟶ (↑U : Scheme).presheaf.stalk x) =
    (X.presheaf.obj (op (U.ι ''ᵁ W)) ⟶ (↑U : Scheme).presheaf.stalk x)
⊢ Eq (α := (↑U : Scheme).presheaf.obj (op W) ⟶ (↑U : Scheme).presheaf.stalk x) ((↑U : Scheme).presheaf.germ W x hxW)
    (Hom.app U.ι (U.ι ''ᵁ W) ≫ (↑U : Scheme).presheaf.germ (U.ι ⁻¹ᵁ U.ι ''ᵁ W) x ⋯)

Tactic:
(U.toScheme.presheaf.germ_res (homOfLE ?_) _ _).symm

Premises used: IsOpenMap.functorMap, Set.Mem, Quiver.Hom.op, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.Presheaf.germ_res, CategoryTheory.homOfLE, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Eq.symm, AlgebraicGeometry.Scheme.Opens.toScheme, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
x : ↥U
W : TopologicalSpace.Opens ↥(↑U : Scheme)
hxW : x ∈ W
e_1 :
  ((↑U : Scheme).presheaf.obj (op W) ⟶ (↑U : Scheme).presheaf.stalk x) =
    (X.presheaf.obj (op (U.ι ''ᵁ W)) ⟶ (↑U : Scheme).presheaf.stalk x)
h : (Opens.map (Opens.inclusion' U)).1 (unop (op (U.ι ''ᵁ W))) ≤ W
⊢ Eq (α := (↑U : Scheme).presheaf.obj (op W) ⟶ (↑U : Scheme).presheaf.stalk x) ((↑U : Scheme).presheaf.germ W x hxW)
    (Hom.app U.ι (U.ι ''ᵁ W) ≫ (↑U : Scheme).presheaf.germ (U.ι ⁻¹ᵁ U.ι ''ᵁ W) x ⋯)

Tactic:
refine (U.toScheme.presheaf.germ_res (homOfLE ?_) _ _).symm

Premises used: AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.Presheaf.germ_res, CategoryTheory.homOfLE, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Eq.symm, AlgebraicGeometry.Scheme.Opens.toScheme, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
x : ↥U
W : TopologicalSpace.Opens ↥(↑U : Scheme)
hxW : x ∈ W
e_1 :
  ((↑U : Scheme).presheaf.obj (op W) ⟶ (↑U : Scheme).presheaf.stalk x) =
    (X.presheaf.obj (op (U.ι ''ᵁ W)) ⟶ (↑U : Scheme).presheaf.stalk x)
⊢ (Opens.map (Opens.inclusion' U)).1 (unop (op (U.ι ''ᵁ W))) ≤ W

Tactic:
(Set.preimage_image_eq _ Subtype.val_injective).le

Premises used: Set.Mem, Subtype.val_injective, setOf, Eq.le, Set.Subset, Set.preimage, Set.preimage_image_eq, Set.image
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
x : ↥U
W : TopologicalSpace.Opens ↥(↑U : Scheme)
hxW : x ∈ W
e_1 :
  ((↑U : Scheme).presheaf.obj (op W) ⟶ (↑U : Scheme).presheaf.stalk x) =
    (X.presheaf.obj (op (U.ι ''ᵁ W)) ⟶ (↑U : Scheme).presheaf.stalk x)
⊢ (Opens.map (Opens.inclusion' U)).1 (unop (op (U.ι ''ᵁ W))) ≤ W

Tactic:
exact (Set.preimage_image_eq _ Subtype.val_injective).le

Premises used: Subtype.val_injective, Eq.le, Set.preimage_image_eq
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
s : Type u_1
X : Scheme
U : s → X.Opens
hU : IsOpenCover U
rw :
  (∀ (x : ↥X),
      ∃ (i :
        PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := X)
          { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι }),
        Membership.mem (γ := Set ↥X)
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
                  PreZeroHypercover.{u_1, u, u + 1} X }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
                  PreZeroHypercover.{u_1, u, u + 1} X }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := X)
          { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι }),
      IsOpenImmersion
        (PreZeroHypercover.f
          { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
            PreZeroHypercover.{u_1, u, u + 1} X }
          i)
⊢ PreZeroHypercover.presieve₀.{u_1, u, u + 1}
      { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι } ∈
    (precoverage IsOpenImmersion).coverings X

Tactic:
rw [presieve₀_mem_precoverage_iff]

Premises used: AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
s : Type u_1
X : Scheme
U : s → X.Opens
hU : IsOpenCover U
⊢ (∀ (x : ↥X),
      ∃ (i :
        PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := X)
          { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι }),
        Membership.mem (γ := Set ↥X)
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
                  PreZeroHypercover.{u_1, u, u + 1} X }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
                  PreZeroHypercover.{u_1, u, u + 1} X }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀.{u_1, u, u + 1} (C := Scheme) (S := X)
          { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι }),
      IsOpenImmersion
        (PreZeroHypercover.f
          { I₀ := s, X := fun (i : s) ↦ (↑(U i) : Scheme), f := fun (i : s) ↦ (U i).ι :
            PreZeroHypercover.{u_1, u, u + 1} X }
          i)

Tactic:
⟨fun x ↦ ?_, inferInstance⟩

Premises used: inferInstance, And.intro