awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Fiber
Goal:
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : PrimeSpectrum R
refine_1 :
  pullback (X := Spec ((Spec (CommRingCat.of R)).residueField p)) (Y := Spec (CommRingCat.of S))
      ((Spec (CommRingCat.of R)).fromSpecResidueField p) (map (CommRingCat.ofHom (algebraMap R S))) ≅
    pullback (X := Spec (CommRingCat.of p.asIdeal.ResidueField)) (Y := Spec (CommRingCat.of S)) (Z :=
      Spec (CommRingCat.of R)) (map (CommRingCat.ofHom (algebraMap R p.asIdeal.ResidueField)))
      (map (CommRingCat.ofHom (algebraMap R S)))
refine_2 : Spec ((Spec (CommRingCat.of R)).residueField p) ≅ Spec (CommRingCat.of p.asIdeal.ResidueField)
refine_3 :
  Eq (α :=
    Scheme.Hom.fiber (X := Spec (CommRingCat.of S)) (map (CommRingCat.ofHom (algebraMap R S))) p ⟶
      Spec (CommRingCat.of p.asIdeal.ResidueField))
    (Iso.hom
        (pullbackSymmetry (map (CommRingCat.ofHom (algebraMap R S)))
            ((Spec (CommRingCat.of R)).fromSpecResidueField p) ≪≫
          Iso.trans (Y :=
              pullback (X := Spec ((Spec (CommRingCat.of R)).residueField p)) (Y := Spec (CommRingCat.of S)) (Z :=
                Spec (CommRingCat.of R))
                (map (Iso.inv (Scheme.Spec.residueFieldIso (CommRingCat.of R) p)) ≫
                  map (CommRingCat.ofHom (algebraMap (↑(CommRingCat.of R) : Type u) p.asIdeal.ResidueField)))
                (map (CommRingCat.ofHom (algebraMap R S))))
              (pullback.congrHom ⋯ ⋯)
              (asIso
                (pullback.map
                  (map (Iso.inv (Scheme.Spec.residueFieldIso (CommRingCat.of R) p)) ≫
                    map (CommRingCat.ofHom (algebraMap (↑(CommRingCat.of R) : Type u) p.asIdeal.ResidueField)))
                  (map (CommRingCat.ofHom (algebraMap R S)))
                  (map (CommRingCat.ofHom (algebraMap R p.asIdeal.ResidueField)))
                  (map (CommRingCat.ofHom (algebraMap R S)))
                  (map (Iso.inv (Scheme.Spec.residueFieldIso (CommRingCat.of R) p))) (𝟙 (Spec (CommRingCat.of S)))
                  (𝟙 (Spec (CommRingCat.of R))) ⋯ ⋯)) ≪≫
            pullbackSpecIso R p.asIdeal.ResidueField S) ≫
      map (CommRingCat.ofHom (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber S))))
    (Scheme.Hom.fiberToSpecResidueField (map (CommRingCat.ofHom (algebraMap R S))) p ≫
      Iso.hom (Scheme.Spec.mapIso (Iso.op (Iso.symm (Scheme.Spec.residueFieldIso (CommRingCat.of R) p)))))
⊢ Arrow.mk (X := Scheme.Hom.fiber (X := Spec (CommRingCat.of S)) (map (CommRingCat.ofHom (algebraMap R S))) p)
      (Scheme.Hom.fiberToSpecResidueField (map (CommRingCat.ofHom (algebraMap R S))) p) ≅
    Arrow.mk (X := Spec (CommRingCat.of (p.asIdeal.Fiber S))) (Y := Spec (CommRingCat.of p.asIdeal.ResidueField))
      (map (CommRingCat.ofHom (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber S))))

Tactic:
refine Arrow.isoMk' _ _
    (pullbackSymmetry _ _ ≪≫ ?_ ≪≫ pullbackSpecIso R p.asIdeal.ResidueField S) ?_ ?_

Premises used: CategoryTheory.Limits.pullbackSymmetry, AlgebraicGeometry.pullbackSpecIso, Ideal.ResidueField, CategoryTheory.Iso.trans, CategoryTheory.Arrow.isoMk', PrimeSpectrum.asIdeal
-- Module: Mathlib.AlgebraicGeometry.Fiber
Goal:
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : PrimeSpectrum R
refine_1 :
  pullback (X := Spec ((Spec (CommRingCat.of R)).residueField p)) (Y := Spec (CommRingCat.of S)) (Z :=
      Spec (CommRingCat.of R))
      (map (Iso.inv (Scheme.Spec.residueFieldIso (CommRingCat.of R) p)) ≫
        map (CommRingCat.ofHom (algebraMap (↑(CommRingCat.of R) : Type u) p.asIdeal.ResidueField)))
      (map (CommRingCat.ofHom (algebraMap R S))) ≅
    pullback (X := Spec (CommRingCat.of p.asIdeal.ResidueField)) (Y := Spec (CommRingCat.of S)) (Z :=
      Spec (CommRingCat.of R)) (map (CommRingCat.ofHom (algebraMap R p.asIdeal.ResidueField)))
      (map (CommRingCat.ofHom (algebraMap R S)))
⊢ pullback (X := Spec ((Spec (CommRingCat.of R)).residueField p)) (Y := Spec (CommRingCat.of S))
      ((Spec (CommRingCat.of R)).fromSpecResidueField p) (map (CommRingCat.ofHom (algebraMap R S))) ≅
    pullback (X := Spec (CommRingCat.of p.asIdeal.ResidueField)) (Y := Spec (CommRingCat.of S)) (Z :=
      Spec (CommRingCat.of R)) (map (CommRingCat.ofHom (algebraMap R p.asIdeal.ResidueField)))
      (map (CommRingCat.ofHom (algebraMap R S)))

Tactic:
refine pullback.congrHom
      (Scheme.Spec.map_residueFieldIso_inv_eq_fromSpecResidueField (.of R) p).symm rfl ≪≫ ?_

Premises used: AlgebraicGeometry.Scheme.Spec.map_residueFieldIso_inv_eq_fromSpecResidueField, CommRingCat.of, CategoryTheory.Limits.pullback.congrHom, Eq.symm, rfl
-- Module: Mathlib.AlgebraicGeometry.Fiber
Goal:
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : PrimeSpectrum R
⊢ Eq (α := Spec ((Spec (CommRingCat.of R)).residueField p) ⟶ Spec (CommRingCat.of R))
    ((map (Iso.inv (Scheme.Spec.residueFieldIso (CommRingCat.of R) p)) ≫
        map (CommRingCat.ofHom (algebraMap (↑(CommRingCat.of R) : Type u) p.asIdeal.ResidueField))) ≫
      𝟙 (Spec (CommRingCat.of R)))
    (map (Iso.inv (Scheme.Spec.residueFieldIso (CommRingCat.of R) p)) ≫
      map (CommRingCat.ofHom (algebraMap R p.asIdeal.ResidueField)))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Fiber
Goal:
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : PrimeSpectrum R
⊢ map (CommRingCat.ofHom (algebraMap R S)) ≫ 𝟙 (Spec (CommRingCat.of R)) =
    𝟙 (Spec (CommRingCat.of S)) ≫ map (CommRingCat.ofHom (algebraMap R S))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Fiber
Goal:
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : PrimeSpectrum R
⊢ pullback (X := Spec ((Spec (CommRingCat.of R)).residueField p)) (Y := Spec (CommRingCat.of S)) (Z :=
      Spec (CommRingCat.of R))
      (map (Iso.inv (Scheme.Spec.residueFieldIso (CommRingCat.of R) p)) ≫
        map (CommRingCat.ofHom (algebraMap (↑(CommRingCat.of R) : Type u) p.asIdeal.ResidueField)))
      (map (CommRingCat.ofHom (algebraMap R S))) ≅
    pullback (X := Spec (CommRingCat.of p.asIdeal.ResidueField)) (Y := Spec (CommRingCat.of S)) (Z :=
      Spec (CommRingCat.of R)) (map (CommRingCat.ofHom (algebraMap R p.asIdeal.ResidueField)))
      (map (CommRingCat.ofHom (algebraMap R S)))

Tactic:
refine asIso <| pullback.map _ _ _ _ (Spec.map <| (Scheme.Spec.residueFieldIso (.of R) _).inv)
      (𝟙 _) (𝟙 _) (by simp) (by simp)

Premises used: AlgebraicGeometry.Spec.map, CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.pullback.map, AlgebraicGeometry.Scheme.Spec.residueFieldIso, CommRingCat.of, CategoryTheory.Iso.inv, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicGeometry.Fiber
Goal:
X Y : Scheme
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : PrimeSpectrum R
⊢ Spec ((Spec (CommRingCat.of R)).residueField p) ≅ Spec (CommRingCat.of p.asIdeal.ResidueField)

Tactic:
exact Scheme.Spec.mapIso (Scheme.Spec.residueFieldIso (.of R) _).symm.op

Premises used: CategoryTheory.Iso.op, AlgebraicGeometry.Scheme.Spec, AlgebraicGeometry.Scheme.Spec.residueFieldIso, CommRingCat.of, CategoryTheory.Iso.symm, CategoryTheory.Functor.mapIso
-- Module: Mathlib.AlgebraicGeometry.Fiber
Goal:
X Y : Scheme
f : X ⟶ Y
y : ↥Y
⊢ Eq (α := Set ↥X) (Set.range (ι := ↥(fiber f y)) ⇑(fiberι f y)) (Set.preimage (β := ↥Y) ⇑f {y})

Tactic:
simp [fiber, fiberι, Scheme.Pullback.range_fst, Scheme.range_fromSpecResidueField]

Premises used: AlgebraicGeometry.Scheme.Hom.fiberι, AlgebraicGeometry.Scheme.Hom.fiber, AlgebraicGeometry.Scheme.Pullback.range_fst, AlgebraicGeometry.Scheme.range_fromSpecResidueField
-- Module: Mathlib.AlgebraicGeometry.Fiber
Goal:
X Y : Scheme
f : X ⟶ Y
y : ↥Y
⊢ IsPreimmersion (Scheme.Hom.fiberι f y)

Tactic:
MorphismProperty.pullback_fst _ _ inferInstance

Premises used: inferInstance, CategoryTheory.MorphismProperty.pullback_fst, AlgebraicGeometry.Scheme.Hom.fiberι, AlgebraicGeometry.Scheme.Hom.fiber
-- Module: Mathlib.AlgebraicGeometry.Fiber
Goal:
X Y : Scheme
f : X ⟶ Y
y : ↥Y
x : ↥(fiber f y)
⊢ Eq (α := ↥X) ((↑((fiberHomeo f y : (a : ↥(fiber f y)) → (↑(⇑f ⁻¹' {y}) : Type u)) x) : ↥X) : ↥X) ((fiberι f y) x : ↥X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Fiber
Goal:
X Y : Scheme
f : X ⟶ Y
y : ↥Y
x : (↑(Set.preimage (β := ↥Y) ⇑f {y}) : Type u)
⊢ (fiberι f y) (((fiberHomeo f y).symm : (a : (↑(⇑f ⁻¹' {y}) : Type u)) → ↥(fiber f y)) x : ↥(fiber f y)) = (↑x : ↥X)

Tactic:
congr($((f.fiberHomeo y).apply_symm_apply x).1)

Premises used: congrArg, id, AlgebraicGeometry.Scheme.Hom.fiberHomeo, Homeomorph.apply_symm_apply, Subtype.val
-- Module: Mathlib.AlgebraicGeometry.Fiber
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ (fiberι f (f x)) (asFiber f x) = x

Tactic:
f.fiberι_fiberHomeo_symm _ _

Premises used: AlgebraicGeometry.Scheme.Hom.asFiber, AlgebraicGeometry.Scheme.Hom.fiberι_fiberHomeo_symm
-- Module: Mathlib.AlgebraicGeometry.Fiber
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
y : ↥Y
⊢ CompactSpace.{u} ↥(Scheme.Hom.fiber f y)

Tactic:
haveI : QuasiCompact (f.fiberToSpecResidueField y) :=
      MorphismProperty.pullback_snd _ _ inferInstance
  HasAffineProperty.iff_of_isAffine (P := @QuasiCompact)
    (f := f.fiberToSpecResidueField y).mp inferInstance

Premises used: inferInstance, AlgebraicGeometry.HasAffineProperty.iff_of_isAffine, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Fiber
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
y : ↥Y
⊢ IsCompact (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})

Tactic:
f.range_fiberι y ▸ isCompact_range (f.fiberι y).continuous

Premises used: AlgebraicGeometry.Scheme.Hom.range_fiberι, Eq.rec, AlgebraicGeometry.Scheme.Hom.fiberι, isCompact_range, AlgebraicGeometry.Scheme.Hom.continuous
-- Module: Mathlib.AlgebraicGeometry.Fiber
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
y : ↥Y
⊢ IsAffine.{u} (Scheme.Hom.fiber f y)

Tactic:
haveI : IsAffineHom (f.fiberToSpecResidueField y) :=
    MorphismProperty.pullback_snd _ _ inferInstance
  isAffine_of_isAffineHom (f.fiberToSpecResidueField y)

Premises used: AlgebraicGeometry.isAffine_of_isAffineHom, AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField
-- Module: Mathlib.AlgebraicGeometry.Fiber
Goal:
X Y : Scheme
f : X ⟶ Y
y : ↥Y
inst : LocallyOfFiniteType f
⊢ JacobsonSpace.{u} ↥(Scheme.Hom.fiber f y)

Tactic:
have : LocallyOfFiniteType (f.fiberToSpecResidueField y) :=
    MorphismProperty.pullback_snd _ _ inferInstance
  LocallyOfFiniteType.jacobsonSpace (f.fiberToSpecResidueField y)

Premises used: inferInstance, AlgebraicGeometry.Scheme.fromSpecResidueField, CategoryTheory.MorphismProperty.pullback_snd, AlgebraicGeometry.LocallyOfFiniteType.jacobsonSpace, AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField
-- Module: Mathlib.AlgebraicGeometry.Fiber
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ X.fromSpecResidueField x ≫ f = Spec.map (residueFieldMap f x) ≫ Y.fromSpecResidueField (f x)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Fiber
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ asFiberHom f x ≫ fiberι f (f x) = X.fromSpecResidueField x

Tactic:
pullback.lift_fst ..

Premises used: CategoryTheory.Limits.pullback.lift_fst
-- Module: Mathlib.AlgebraicGeometry.Fiber
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
y : ↥(Spec (X.residueField x))
⊢ Eq (α := ↥X) ((fiberι f (f x)) ((asFiberHom f x) y : ↥(fiber f (f x))) : ↥X) ((fiberι f (f x)) (asFiber f x) : ↥X)

Tactic:
simp [← Scheme.Hom.comp_apply]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.Fiber
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ Eq (α := Set ↥(fiber f (f x))) (Set.range (ι := ↥(Spec (X.residueField x))) ⇑(asFiberHom f x)) {asFiber f x}

Tactic:
aesop
-- Module: Mathlib.AlgebraicGeometry.Fiber
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ IsPreimmersion (Scheme.Hom.asFiberHom f x)

Tactic:
have : IsPreimmersion (f.asFiberHom x ≫ f.fiberι _) := f.asFiberHom_fiberι x ▸ inferInstance
  .of_comp _ (f.fiberι _)

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.Hom.asFiberHom, Eq.rec, inferInstance, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.Hom.fiberι, AlgebraicGeometry.Scheme.Hom.asFiberHom_fiberι, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.IsPreimmersion.of_comp, Eq.symm, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
inst : IrreducibleSpace.{u_1} ↥X
U : X.Opens
h : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
⊢ (Set.univ ∩ (↑U : Set ↥X)).Nonempty

Tactic:
simpa using h
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
inst : IsIntegral X
⊢ Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) (closure {genericPoint ↥X})

Tactic:
simp [irreducibleComponents_eq_singleton]

Premises used: irreducibleComponents_eq_singleton
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
x : ↥X
hx : x ∈ U
rw :
  ∀ (a : (↑(X.presheaf.obj (op U)) : Type u_1)),
    Eq (α := (↑(X.presheaf.stalk x) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx) :
              (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
            a :
          (↑(X.presheaf.stalk x) : Type u_1))
        (0 : (↑(X.presheaf.stalk x) : Type u_1)) →
      a = 0
⊢ Function.Injective (α := (↑(X.presheaf.obj (op U)) : Type u_1)) (β := (↑(X.presheaf.stalk x) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx)) :
      (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))

Tactic:
rw [injective_iff_map_eq_zero]

Premises used: injective_iff_map_eq_zero
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
x : ↥X
hx : x ∈ U
y : (↑(X.presheaf.obj (op U)) : Type u_1)
hy :
  Eq (α := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        y :
      (↑(X.presheaf.stalk x) : Type u_1))
    (0 : (↑(X.presheaf.stalk x) : Type u_1))
⊢ Eq (α := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        y :
      (↑(X.presheaf.stalk x) : Type u_1))
    ((CommRingCat.Hom.hom (X.presheaf.germ U x hx) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        0 :
      (↑(X.presheaf.stalk x) : Type u_1))

Tactic:
rw [← (X.presheaf.germ U x hx).hom.map_zero] at hy

Premises used: CommRingCat.Hom.hom, TopCat.Presheaf.germ, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, RingHom.map_zero, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
x : ↥X
hx : x ∈ U
y : (↑(X.presheaf.obj (op U)) : Type u_1)
hy :
  Eq (α := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        y :
      (↑(X.presheaf.stalk x) : Type u_1))
    ((CommRingCat.Hom.hom (X.presheaf.germ U x hx) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        0 :
      (↑(X.presheaf.stalk x) : Type u_1))
obtain :
  ∀ (W : Opens ↥X) (hW : x ∈ W) (iU iV : W ⟶ U)
    (e :
      Eq (α := (↑(X.presheaf.obj (op W)) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (X.presheaf.map iU.op) :
              (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op W)) : Type u_1))
            y :
          (↑(X.presheaf.obj (op W)) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (X.presheaf.map iV.op) :
              (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op W)) : Type u_1))
            0 :
          (↑(X.presheaf.obj (op W)) : Type u_1))),
    y = 0
⊢ y = 0

Tactic:
obtain ⟨W, hW, iU, iV, e⟩ := X.presheaf.germ_eq _ hx hx _ _ hy

Premises used: AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, TopCat.Presheaf.germ_eq, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
x : ↥X
hx : x ∈ U
y : (↑(X.presheaf.obj (op U)) : Type u_1)
hy :
  Eq (α := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        y :
      (↑(X.presheaf.stalk x) : Type u_1))
    ((CommRingCat.Hom.hom (X.presheaf.germ U x hx) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        0 :
      (↑(X.presheaf.stalk x) : Type u_1))
W : Opens ↥X
hW : x ∈ W
iU iV : W ⟶ U
e :
  Eq (α := (↑(X.presheaf.obj (op W)) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map iU.op) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op W)) : Type u_1))
        y :
      (↑(X.presheaf.obj (op W)) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map iV.op) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op W)) : Type u_1))
        0 :
      (↑(X.presheaf.obj (op W)) : Type u_1))
⊢ Eq (α := (↑(X.presheaf.obj (op W)) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map iU.op) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op W)) : Type u_1))
        y :
      (↑(X.presheaf.obj (op W)) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map iU.op) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op W)) : Type u_1))
        0 :
      (↑(X.presheaf.obj (op W)) : Type u_1))

Tactic:
cases Subsingleton.elim iU iV

Premises used: Subsingleton.elim
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
x : ↥X
hx : x ∈ U
y : (↑(X.presheaf.obj (op U)) : Type u_1)
hy :
  Eq (α := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        y :
      (↑(X.presheaf.stalk x) : Type u_1))
    ((CommRingCat.Hom.hom (X.presheaf.germ U x hx) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        0 :
      (↑(X.presheaf.stalk x) : Type u_1))
W : Opens ↥X
hW : x ∈ W
iU : W ⟶ U
e :
  Eq (α := (↑(X.presheaf.obj (op W)) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map iU.op) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op W)) : Type u_1))
        y :
      (↑(X.presheaf.obj (op W)) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map iU.op) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op W)) : Type u_1))
        0 :
      (↑(X.presheaf.obj (op W)) : Type u_1))
⊢ Nonempty.{u_1 + 1} ↥(↑W : Scheme)

Tactic:
haveI : Nonempty W := ⟨⟨_, hW⟩⟩
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
x : ↥X
hx : x ∈ U
y : (↑(X.presheaf.obj (op U)) : Type u_1)
hy :
  Eq (α := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        y :
      (↑(X.presheaf.stalk x) : Type u_1))
    ((CommRingCat.Hom.hom (X.presheaf.germ U x hx) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        0 :
      (↑(X.presheaf.stalk x) : Type u_1))
W : Opens ↥X
hW : x ∈ W
iU : W ⟶ U
e :
  Eq (α := (↑(X.presheaf.obj (op W)) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map iU.op) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op W)) : Type u_1))
        y :
      (↑(X.presheaf.obj (op W)) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map iU.op) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op W)) : Type u_1))
        0 :
      (↑(X.presheaf.obj (op W)) : Type u_1))
this : Nonempty.{u_1 + 1} ↥(↑W : Scheme)
⊢ y = 0

Tactic:
map_injective_of_isIntegral X iU e

Premises used: AlgebraicGeometry.map_injective_of_isIntegral