awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)
s : (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U)) : Type v)
⊢ IsOpen (imageBasicOpen f g U s).carrier

Tactic:
(imageBasicOpen f g U s).2

Premises used: AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen, TopologicalSpace.Opens.is_open'
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)
s : (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U)) : Type v)
⊢ IsOpen (imageBasicOpen f g U s).carrier

Tactic:
exact (imageBasicOpen f g U s).2

Premises used: AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen, TopologicalSpace.Opens.is_open'
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
x : (↑Y.toTopCat : Type v)
map_nonunit :
  ∀
    (a :
      (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                  TopCat.carrier) (Y := (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
                  (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) :
                (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
                  (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
              x)) :
        Type v)),
    IsUnit (M := (↑(Y.presheaf.stalk x) : Type v))
        ((CommRingCat.Hom.hom
                (PresheafedSpace.Hom.stalkMap (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))
                  x) :
              (a :
                  (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.stalk
                        ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base :
                            (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
                              (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
                          x)) :
                    Type v)) →
                (↑(Y.presheaf.stalk x) : Type v))
            a :
          (↑(Y.presheaf.stalk x) : Type v)) →
      IsUnit a
⊢ IsLocalHom (R :=
    (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                (Y := (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) :
              (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
                (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
            x)) :
      Type v))
    (S := (↑(Y.presheaf.stalk x) : Type v)) (F :=
    (↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                  TopCat.carrier) (Y := (↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
                  (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) :
                (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
                  (↑(↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
              x)) :
        Type v) →+*
      (↑(Y.presheaf.stalk x) : Type v))
    (CommRingCat.Hom.hom
      (PresheafedSpace.Hom.stalkMap (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g))) x))

Tactic:
constructor
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
x : (↑(↑(Limits.coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v)
obtain :
  ∀ (y : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)),
    IsLocalRing.{v}
      (↑((Limits.coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                  TopCat.carrier) (Y :=
                  (↑(Limits.coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
                  (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) :
                (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
                  (↑(↑(Limits.coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
              y)) :
        Type v)
⊢ IsLocalRing.{v} (↑((Limits.coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.stalk x) : Type v)

Tactic:
obtain ⟨y, rfl⟩ :=
      (TopCat.epi_iff_surjective (coequalizer.π f.toShHom g.toShHom).hom.base).mp inferInstance x

Premises used: inferInstance, Iff.mp, TopCat.epi_iff_surjective, AlgebraicGeometry.PresheafedSpace.Hom.base, CategoryTheory.InducedCategory.Hom.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom, CategoryTheory.Limits.coequalizer.π, rfl
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
y : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)
⊢ IsLocalRing.{v}
    (↑((Limits.coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                (Y := (↑(Limits.coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) :
              (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
                (↑(↑(Limits.coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
            y)) :
      Type v)

Tactic:
((coequalizer.π f.toShHom g.toShHom :).hom.stalkMap y).hom.domain_isLocalRing

Premises used: CommRingCat.Hom.hom, AlgebraicGeometry.PresheafedSpace.Hom.stalkMap, RingHom.domain_isLocalRing, CategoryTheory.InducedCategory.Hom.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom, CategoryTheory.Limits.coequalizer.π
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
y : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)
⊢ IsLocalRing.{v}
    (↑((Limits.coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                (Y := (↑(Limits.coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)))) :
              (a : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)) →
                (↑(↑(Limits.coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace : TopCat) : Type v))
            y)) :
      Type v)

Tactic:
exact ((coequalizer.π f.toShHom g.toShHom :).hom.stalkMap y).hom.domain_isLocalRing

Premises used: CommRingCat.Hom.hom, AlgebraicGeometry.PresheafedSpace.Hom.stalkMap, RingHom.domain_isLocalRing, CategoryTheory.InducedCategory.Hom.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom, CategoryTheory.Limits.coequalizer.π
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : RingedSpace
f g : X ⟶ Y
H : f = g
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
h :
  IsLocalHom (R :=
    (↑(Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                TopCat.carrier) f.hom.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
            x)) :
      Type u_1))
    (S := (↑(X.presheaf.stalk x) : Type u_1)) (F :=
    (↑(Y.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  TopCat.carrier) f.hom.base :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
              x)) :
        Type u_1) →+*
      (↑(X.presheaf.stalk x) : Type u_1))
    (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap f.hom x))
rw :
  IsLocalHom (R :=
    (↑(Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                TopCat.carrier) g.hom.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
            x)) :
      Type u_1))
    (S := (↑(X.presheaf.stalk x) : Type u_1)) (F :=
    (↑(Y.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  TopCat.carrier) g.hom.base :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
              x)) :
        Type u_1) →+*
      (↑(X.presheaf.stalk x) : Type u_1))
    (CommRingCat.Hom.hom (eqToHom ⋯ ≫ PresheafedSpace.Hom.stalkMap f.hom x))
⊢ IsLocalHom (R :=
    (↑(Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                TopCat.carrier) g.hom.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
            x)) :
      Type u_1))
    (S := (↑(X.presheaf.stalk x) : Type u_1)) (F :=
    (↑(Y.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  TopCat.carrier) g.hom.base :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
              x)) :
        Type u_1) →+*
      (↑(X.presheaf.stalk x) : Type u_1))
    (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap g.hom x))

Tactic:
rw [PresheafedSpace.stalkMap.congr_hom _ _ (congr_arg InducedCategory.Hom.hom H.symm) x]

Premises used: congr_arg, AlgebraicGeometry.PresheafedSpace.stalkMap.congr_hom, CategoryTheory.InducedCategory.Hom.hom, Eq.symm
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : RingedSpace
f g : X ⟶ Y
H : f = g
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)
h :
  IsLocalHom (R :=
    (↑(Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                TopCat.carrier) f.hom.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
            x)) :
      Type u_1))
    (S := (↑(X.presheaf.stalk x) : Type u_1)) (F :=
    (↑(Y.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  TopCat.carrier) f.hom.base :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
              x)) :
        Type u_1) →+*
      (↑(X.presheaf.stalk x) : Type u_1))
    (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap f.hom x))
⊢ IsLocalHom (R :=
    (↑(Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                TopCat.carrier) g.hom.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
            x)) :
      Type u_1))
    (S := (↑(X.presheaf.stalk x) : Type u_1)) (F :=
    (↑(Y.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  TopCat.carrier) g.hom.base :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u_1)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u_1))
              x)) :
        Type u_1) →+*
      (↑(X.presheaf.stalk x) : Type u_1))
    (CommRingCat.Hom.hom (eqToHom ⋯ ≫ PresheafedSpace.Hom.stalkMap f.hom x))

Tactic:
infer_instance
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
⊢ HasCoequalizer f g

Tactic:
⟨⟨⟨_, coequalizerCoforkIsColimit f g⟩⟩⟩

Premises used: AlgebraicGeometry.LocallyRingedSpace.coequalizerCoforkIsColimit, Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
⊢ HasCoequalizers LocallyRingedSpace

Tactic:
hasCoequalizers_of_hasColimit_parallelPair _

Premises used: CategoryTheory.Limits.hasCoequalizers_of_hasColimit_parallelPair
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
F : WalkingParallelPair ⥤ LocallyRingedSpace
suffices :
  PreservesColimit (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right))
    forgetToSheafedSpace
⊢ PreservesColimit F forgetToSheafedSpace

Tactic:
suffices PreservesColimit (parallelPair (F.map WalkingParallelPairHom.left)
        (F.map WalkingParallelPairHom.right)) forgetToSheafedSpace from
      preservesColimit_of_iso_diagram _ (diagramIsoParallelPair F).symm
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
F : WalkingParallelPair ⥤ LocallyRingedSpace
apply :
  IsColimit (F :=
    parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right) ⋙ forgetToSheafedSpace)
    (forgetToSheafedSpace.mapCocone
      (coequalizerCofork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)))
⊢ PreservesColimit (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right))
    forgetToSheafedSpace

Tactic:
apply preservesColimit_of_preserves_colimit_cocone (coequalizerCoforkIsColimit _ _)

Premises used: AlgebraicGeometry.LocallyRingedSpace.coequalizerCoforkIsColimit, CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
F : WalkingParallelPair ⥤ LocallyRingedSpace
apply : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ IsColimit (F :=
    parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right) ⋙ forgetToSheafedSpace)
    (forgetToSheafedSpace.mapCocone
      (coequalizerCofork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)))

Tactic:
apply (isColimitMapCoconeCoforkEquiv _ _).symm _

Premises used: Equiv.symm, DFunLike.coe, CategoryTheory.Limits.isColimitMapCoconeCoforkEquiv
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
F : WalkingParallelPair ⥤ LocallyRingedSpace
dsimp : 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:
dsimp only [forgetToSheafedSpace]

Premises used: AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
F : WalkingParallelPair ⥤ LocallyRingedSpace
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact coequalizerIsCoequalizer _ _

Premises used: CategoryTheory.Limits.coequalizerIsCoequalizer
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
⊢ HasColimits LocallyRingedSpace

Tactic:
has_colimits_of_hasCoequalizers_and_coproducts

Premises used: CategoryTheory.Limits.has_colimits_of_hasCoequalizers_and_coproducts
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
Goal:
⊢ PreservesColimits forgetToSheafedSpace

Tactic:
preservesColimits_of_preservesCoequalizers_and_coproducts _

Premises used: CategoryTheory.Limits.preservesColimits_of_preservesCoequalizers_and_coproducts
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
Goal:
X : LocallyRingedSpace
U : Opens (↑X.toTopCat : Type u)
x : ↥U
f : (↑(X.presheaf.obj (op U)) : Type u)
rw :
  ¬Eq (α := (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X.evaluation x) :
              (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))
            f :
          (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))
        (0 : (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u)) ↔
    IsUnit (M := (↑(X.toRingedSpace.presheaf.stalk (↑x : (↑X.toTopCat : Type u))) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := X.toRingedSpace.presheaf.stalk (↑x : (↑X.toTopCat : Type u)))
              (X.toRingedSpace.presheaf.germ U (↑x : (↑X.toTopCat : Type u)) ⋯) :
            (a : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u)) →
              (↑(X.toRingedSpace.presheaf.stalk (↑x : (↑X.toTopCat : Type u))) : Type u))
          f :
        (↑(X.toRingedSpace.presheaf.stalk (↑x : (↑X.toTopCat : Type u))) : Type u))
⊢ Eq (α := (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X.evaluation x) :
            (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))
          f :
        (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))
      (0 : (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u)) ↔
    (↑x : (↑X.toTopCat : Type u)) ∉ X.toRingedSpace.basicOpen f

Tactic:
rw [X.toRingedSpace.mem_basicOpen f x.1 x.2, ← not_iff_not, not_not]

Premises used: not_iff_not, Classical.not_not, AlgebraicGeometry.LocallyRingedSpace.toRingedSpace, Subtype.val, AlgebraicGeometry.RingedSpace.mem_basicOpen, Subtype.property
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
Goal:
X : LocallyRingedSpace
U : Opens (↑X.toTopCat : Type u)
x : ↥U
f : (↑(X.presheaf.obj (op U)) : Type u)
⊢ ¬Eq (α := (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X.evaluation x) :
              (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))
            f :
          (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))
        (0 : (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u)) ↔
    IsUnit (M := (↑(X.toRingedSpace.presheaf.stalk (↑x : (↑X.toTopCat : Type u))) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := X.toRingedSpace.presheaf.stalk (↑x : (↑X.toTopCat : Type u)))
              (X.toRingedSpace.presheaf.germ U (↑x : (↑X.toTopCat : Type u)) ⋯) :
            (a : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u)) →
              (↑(X.toRingedSpace.presheaf.stalk (↑x : (↑X.toTopCat : Type u))) : Type u))
          f :
        (↑(X.toRingedSpace.presheaf.stalk (↑x : (↑X.toTopCat : Type u))) : Type u))

Tactic:
(IsLocalRing.residue_ne_zero_iff_isUnit _)

Premises used: Submodule.Quotient.mk, IsLocalRing.residue_ne_zero_iff_isUnit, IsLocalRing.ResidueField
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
Goal:
X : LocallyRingedSpace
U : Opens (↑X.toTopCat : Type u)
x : ↥U
f : (↑(X.presheaf.obj (op U)) : Type u)
⊢ ¬Eq (α := (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X.evaluation x) :
              (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))
            f :
          (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))
        (0 : (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u)) ↔
    IsUnit (M := (↑(X.toRingedSpace.presheaf.stalk (↑x : (↑X.toTopCat : Type u))) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := X.toRingedSpace.presheaf.stalk (↑x : (↑X.toTopCat : Type u)))
              (X.toRingedSpace.presheaf.germ U (↑x : (↑X.toTopCat : Type u)) ⋯) :
            (a : (↑(X.toRingedSpace.presheaf.obj (op U)) : Type u)) →
              (↑(X.toRingedSpace.presheaf.stalk (↑x : (↑X.toTopCat : Type u))) : Type u))
          f :
        (↑(X.toRingedSpace.presheaf.stalk (↑x : (↑X.toTopCat : Type u))) : Type u))

Tactic:
exact (IsLocalRing.residue_ne_zero_iff_isUnit _)

Premises used: IsLocalRing.residue_ne_zero_iff_isUnit
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
Goal:
X : LocallyRingedSpace
U : Opens (↑X.toTopCat : Type u)
x : ↥U
f : (↑(X.presheaf.obj (op U)) : Type u)
⊢ Ne (α := (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X.evaluation x) :
            (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))
          f :
        (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))
      (0 : (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u)) ↔
    (↑x : (↑X.toTopCat : Type u)) ∈ X.toRingedSpace.basicOpen f

Tactic:
simp
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
Goal:
X : LocallyRingedSpace
U : Opens (↑X.toTopCat : Type u)
f : (↑(X.presheaf.obj (op U)) : Type u)
simp : X.toRingedSpace.basicOpen f = ⊥ ↔ ∀ (a : (↑X.toTopCat : Type u)) (b : a ∈ U), a ∉ X.toRingedSpace.basicOpen f
⊢ X.toRingedSpace.basicOpen f = ⊥ ↔
    ∀ (x : ↥U),
      Eq (α := (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X.evaluation x) :
              (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))
            f :
          (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))
        (0 : (↑(X.residueField (↑x : (↑X.toTopCat : Type u))) : Type u))

Tactic:
simp only [evaluation_eq_zero_iff_notMem_basicOpen, Subtype.forall]

Premises used: Subtype.forall, AlgebraicGeometry.LocallyRingedSpace.evaluation_eq_zero_iff_notMem_basicOpen
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
Goal:
X : LocallyRingedSpace
U : Opens (↑X.toTopCat : Type u)
f : (↑(X.presheaf.obj (op U)) : Type u)
⊢ X.toRingedSpace.basicOpen f = ⊥ ↔ ∀ (a : (↑X.toTopCat : Type u)) (b : a ∈ U), a ∉ X.toRingedSpace.basicOpen f

Tactic:
⟨fun h ↦ h ▸ fun a _ hc ↦ hc,
    fun h ↦ eq_bot_iff.mpr <| fun a ha ↦ h a (X.toRingedSpace.basicOpen_le f ha) ha⟩

Premises used: Iff.mpr, AlgebraicGeometry.LocallyRingedSpace.toRingedSpace, Eq.rec, AlgebraicGeometry.RingedSpace.basicOpen_le, Iff.intro, eq_bot_iff, Eq.symm