awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
x : ↥X
f : X.presheaf.stalk x ⟶ R
inst_1 : IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)
U : X.Opens
hU : Membership.mem (α := ↥X) U ((Spec.map f ≫ X.fromSpecStalk x) (closedPoint (↑R : Type u)) : ↥X)
this : (Spec.map f ≫ X.fromSpecStalk x) (closedPoint (↑R : Type u)) = x
⊢ x ∈ U

Tactic:
have : x ∈ U := this ▸ hU
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
x : ↥X
f : X.presheaf.stalk x ⟶ R
inst_1 : IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)
U : X.Opens
hU : Membership.mem (α := ↥X) U ((Spec.map f ≫ X.fromSpecStalk x) (closedPoint (↑R : Type u)) : ↥X)
this_1 : (Spec.map f ≫ X.fromSpecStalk x) (closedPoint (↑R : Type u)) = x
this : x ∈ U
simp :
  X.presheaf.germ U x this ≫ Iso.inv (ΓSpecIso (X.presheaf.stalk x)) ≫ Hom.appLE (Spec.map f) ⊤ ⊤ ⋯ ≫ (ΓSpecIso R).hom =
    X.presheaf.germ U x ⋯ ≫ f
⊢ X.presheaf.germ U ((Spec.map f ≫ X.fromSpecStalk x) (closedPoint (↑R : Type u))) hU ≫
      stalkClosedPointTo (Spec.map f ≫ X.fromSpecStalk x) =
    X.presheaf.germ U x ⋯ ≫ f

Tactic:
simp only [germ_stalkClosedPointTo, Hom.comp_app,
    fromSpecStalk_app (X := X) (x := x) this, Category.assoc, Iso.trans_hom, Functor.mapIso_hom,
      (Spec.map f).app_eq_appLE, Hom.appLE_map_assoc, Hom.map_appLE_assoc]

Premises used: AlgebraicGeometry.Scheme.germ_stalkClosedPointTo, CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Hom.comp_app, AlgebraicGeometry.Spec.map, AlgebraicGeometry.Scheme.Hom.map_appLE_assoc, AlgebraicGeometry.Scheme.Hom.appLE_map_assoc, CategoryTheory.Iso.trans_hom, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, AlgebraicGeometry.Scheme.fromSpecStalk_app, CategoryTheory.Functor.mapIso_hom
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
x : ↥X
f : X.presheaf.stalk x ⟶ R
inst_1 : IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)
U : X.Opens
hU : Membership.mem (α := ↥X) U ((Spec.map f ≫ X.fromSpecStalk x) (closedPoint (↑R : Type u)) : ↥X)
this_1 : (Spec.map f ≫ X.fromSpecStalk x) (closedPoint (↑R : Type u)) = x
this : x ∈ U
rw :
  X.presheaf.germ U x this ≫ Iso.inv (ΓSpecIso (X.presheaf.stalk x)) ≫ Hom.app (Spec.map f) ⊤ ≫ (ΓSpecIso R).hom =
    X.presheaf.germ U x ⋯ ≫ f
rw₁ :
  X.presheaf.germ U x this ≫ Iso.inv (ΓSpecIso (X.presheaf.stalk x)) ≫ Iso.hom (ΓSpecIso (X.presheaf.stalk x)) ≫ f =
    X.presheaf.germ U x ⋯ ≫ f
rw₂ rw₃ : X.presheaf.germ U x this ≫ f = X.presheaf.germ U x ⋯ ≫ f
⊢ X.presheaf.germ U x this ≫
      Iso.inv (ΓSpecIso (X.presheaf.stalk x)) ≫
        Hom.appLE (Spec.map f) ⊤ ((Opens.map (Spec.map f).base).obj ⊤) ⋯ ≫ (ΓSpecIso R).hom =
    X.presheaf.germ U x ⋯ ≫ f

Tactic:
rw [← (Spec.map f).app_eq_appLE, ΓSpecIso_naturality, Iso.inv_hom_id_assoc]

Premises used: AlgebraicGeometry.Spec.map, CategoryTheory.Iso.inv_hom_id_assoc, AlgebraicGeometry.Scheme.ΓSpecIso_naturality, AlgebraicGeometry.Scheme.Hom.app_eq_appLE
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X Y : Scheme
f_1 : X ⟶ Y
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
f : Spec R ⟶ X
x : ↥X
rw : Inseparable x x
⊢ Inseparable ((X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk x) : Type u))) x

Tactic:
rw [fromSpecStalk_closedPoint]

Premises used: AlgebraicGeometry.Scheme.fromSpecStalk_closedPoint
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X Y : Scheme
f_1 : X ⟶ Y
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
f : Spec R ⟶ X
x : ↥X
⊢ Inseparable x x

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
x : ↥X
⊢ stalkClosedPointTo (X.fromSpecStalk x) = Iso.hom (X.presheaf.stalkCongr ⋯)

Tactic:
TopCat.Presheaf.stalk_hom_ext _ fun U hxU ↦ ?_

Premises used: TopCat.Presheaf.stalk_hom_ext
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
x : ↥X
refine :
  ∀ (U : TopologicalSpace.Opens ↥X)
    (hxU : Membership.mem (α := ↥X) U ((X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥X)),
    X.presheaf.germ U ((X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk x) : Type u))) hxU ≫
        stalkClosedPointTo (X.fromSpecStalk x) =
      X.presheaf.germ U ((X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk x) : Type u))) hxU ≫
        Iso.hom (X.presheaf.stalkCongr ⋯)
⊢ stalkClosedPointTo (X.fromSpecStalk x) = Iso.hom (X.presheaf.stalkCongr ⋯)

Tactic:
refine TopCat.Presheaf.stalk_hom_ext _ fun U hxU ↦ ?_

Premises used: TopCat.Presheaf.stalk_hom_ext
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
x : ↥X
U : TopologicalSpace.Opens ↥X
hxU : Membership.mem (α := ↥X) U ((X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥X)
simp :
  X.presheaf.germ U ((X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk x) : Type u))) hxU ≫
      stalkClosedPointTo (X.fromSpecStalk x) =
    X.presheaf.germ U x ⋯
⊢ X.presheaf.germ U ((X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk x) : Type u))) hxU ≫
      stalkClosedPointTo (X.fromSpecStalk x) =
    X.presheaf.germ U ((X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk x) : Type u))) hxU ≫
      Iso.hom (X.presheaf.stalkCongr ⋯)

Tactic:
simp only [TopCat.Presheaf.stalkCongr_hom, TopCat.Presheaf.germ_stalkSpecializes]

Premises used: TopCat.Presheaf.stalkCongr_hom, TopCat.Presheaf.germ_stalkSpecializes
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
x : ↥X
U : TopologicalSpace.Opens ↥X
hxU : Membership.mem (α := ↥X) U ((X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥X)
⊢ X.fromSpecStalk x = Spec.map (𝟙 (X.presheaf.stalk x)) ≫ X.fromSpecStalk x

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
x : ↥X
U : TopologicalSpace.Opens ↥X
hxU : Membership.mem (α := ↥X) U ((X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥X)
⊢ X.fromSpecStalk x = Spec.map (𝟙 (X.presheaf.stalk x)) ≫ X.fromSpecStalk x

Tactic:
have : X.fromSpecStalk x = Spec.map (𝟙 (X.presheaf.stalk x)) ≫ X.fromSpecStalk x := by simp
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
x : ↥X
U : TopologicalSpace.Opens ↥X
hxU : Membership.mem (α := ↥X) U ((X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥X)
this : X.fromSpecStalk x = Spec.map (𝟙 (X.presheaf.stalk x)) ≫ X.fromSpecStalk x
⊢ X.presheaf.germ U
        ((Spec.map (𝟙 (X.presheaf.stalk x)) ≫ X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk x) : Type u))) hxU ≫
      stalkClosedPointTo (Spec.map (𝟙 (X.presheaf.stalk x)) ≫ X.fromSpecStalk x) =
    X.presheaf.germ U x ⋯ ≫ 𝟙 (X.presheaf.stalk x)

Tactic:
germ_stalkClosedPointTo_Spec_fromSpecStalk (𝟙 (X.presheaf.stalk x)) U hxU

Premises used: AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec_fromSpecStalk, CategoryTheory.CategoryStruct.id, TopCat.Presheaf.stalk, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
x : ↥X
U : TopologicalSpace.Opens ↥X
hxU : Membership.mem (α := ↥X) U ((X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥X)
this : X.fromSpecStalk x = Spec.map (𝟙 (X.presheaf.stalk x)) ≫ X.fromSpecStalk x
⊢ X.presheaf.germ U ((X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk x) : Type u))) hxU ≫
      stalkClosedPointTo (X.fromSpecStalk x) =
    X.presheaf.germ U x ⋯

Tactic:
convert! germ_stalkClosedPointTo_Spec_fromSpecStalk (𝟙 (X.presheaf.stalk x)) U hxU

Premises used: AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec_fromSpecStalk, CategoryTheory.CategoryStruct.id, TopCat.Presheaf.stalk, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
f : Spec R ⟶ X
obtain :
  ∀ (U : TopologicalSpace.Opens ↥X) (hU : U ∈ X.affineOpens)
    (hxU : Membership.mem (α := ↥X) (↑U : Set ↥X) (f (closedPoint (↑R : Type u)) : ↥X)),
    CategoryStruct.comp (Y := Spec (X.presheaf.stalk (f (closedPoint (↑R : Type u))))) (Spec.map (stalkClosedPointTo f))
        (X.fromSpecStalk (f (closedPoint (↑R : Type u)))) =
      f
⊢ CategoryStruct.comp (Y := Spec (X.presheaf.stalk (f (closedPoint (↑R : Type u))))) (Spec.map (stalkClosedPointTo f))
      (X.fromSpecStalk (f (closedPoint (↑R : Type u)))) =
    f

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ := X.isBasis_affineOpens.exists_subset_of_mem_open
    (Set.mem_univ (f (closedPoint R))) isOpen_univ

Premises used: CommRingCat.carrier, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', isOpen_univ, IsLocalRing.closedPoint, Set.mem_univ, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.isBasis_affineOpens, DFunLike.coe, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
f : Spec R ⟶ X
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : Membership.mem (α := ↥X) (↑U : Set ↥X) (f (closedPoint (↑R : Type u)) : ↥X)
⊢ Spec.map (Hom.appLE f U ⊤ ⋯) ≫ IsAffineOpen.fromSpec hU = IsAffineOpen.fromSpec ⋯ ≫ f

Tactic:
have := IsAffineOpen.SpecMap_appLE_fromSpec f hU (isAffineOpen_top _)
    (preimage_eq_top_of_closedPoint_mem f hxU).ge
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
f : Spec R ⟶ X
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : Membership.mem (α := ↥X) (↑U : Set ↥X) (f (closedPoint (↑R : Type u)) : ↥X)
this : Spec.map (Hom.appLE f U ⊤ ⋯) ≫ IsAffineOpen.fromSpec hU = IsAffineOpen.fromSpec ⋯ ≫ f
⊢ Spec.map (ΓSpecIso R).hom ≫ Spec.map (Hom.appLE f U ⊤ ⋯) ≫ IsAffineOpen.fromSpec hU = f

Tactic:
rw [IsAffineOpen.fromSpec_top, Iso.eq_inv_comp, isoSpec_Spec_hom] at this

Premises used: AlgebraicGeometry.Scheme.isoSpec_Spec_hom, AlgebraicGeometry.IsAffineOpen.fromSpec_top, CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
f : Spec R ⟶ X
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : Membership.mem (α := ↥X) (↑U : Set ↥X) (f (closedPoint (↑R : Type u)) : ↥X)
this : Spec.map (ΓSpecIso R).hom ≫ Spec.map (Hom.appLE f U ⊤ ⋯) ≫ IsAffineOpen.fromSpec hU = f
rw :
  Spec.map (Hom.app f U ≫ (Functor.mapIso (Spec R).presheaf (Iso.op (eqToIso ⋯)) ≪≫ ΓSpecIso R).hom) ≫
      IsAffineOpen.fromSpec hU =
    f
⊢ CategoryStruct.comp (Y := Spec (X.presheaf.stalk (f (closedPoint (↑R : Type u))))) (Spec.map (stalkClosedPointTo f))
      (X.fromSpecStalk (f (closedPoint (↑R : Type u)))) =
    f

Tactic:
rw [← hU.fromSpecStalk_eq_fromSpecStalk hxU, IsAffineOpen.fromSpecStalk, ← Spec.map_comp_assoc,
    germ_stalkClosedPointTo]

Premises used: AlgebraicGeometry.Scheme.germ_stalkClosedPointTo, AlgebraicGeometry.Spec.map_comp_assoc, AlgebraicGeometry.IsAffineOpen.fromSpecStalk, AlgebraicGeometry.IsAffineOpen.fromSpecStalk_eq_fromSpecStalk
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
f : Spec R ⟶ X
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : Membership.mem (α := ↥X) (↑U : Set ↥X) (f (closedPoint (↑R : Type u)) : ↥X)
this : Spec.map (ΓSpecIso R).hom ≫ Spec.map (Hom.appLE f U ⊤ ⋯) ≫ IsAffineOpen.fromSpec hU = f
⊢ Spec.map (Hom.app f U ≫ (Functor.mapIso (Spec R).presheaf (Iso.op (eqToIso ⋯)) ≪≫ ΓSpecIso R).hom) ≫
      IsAffineOpen.fromSpec hU =
    f

Tactic:
simpa only [Iso.trans_hom, Functor.mapIso_hom, Iso.op_hom, Category.assoc,
    Hom.app_eq_appLE, Hom.appLE_map_assoc, Spec.map_comp_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.op_hom, AlgebraicGeometry.Spec.map_comp_assoc, AlgebraicGeometry.Scheme.Hom.appLE_map_assoc, CategoryTheory.Iso.trans_hom, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, CategoryTheory.Functor.mapIso_hom
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X Y : Scheme
f : X ⟶ Y
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
f₁ f₂ :
  (x : ↥X) ×
    { f : X.presheaf.stalk x ⟶ R //
      IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }
h₁ :
  f₁.fst (β := fun (x : ↥X) ↦
      { f : X.presheaf.stalk x ⟶ R //
        IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }) =
    f₂.fst (β := fun (x : ↥X) ↦
      { f : X.presheaf.stalk x ⟶ R //
        IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
rw :
  Inseparable
    (f₂.fst (β := fun (x : ↥X) ↦
      { f : X.presheaf.stalk x ⟶ R //
        IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }))
    (f₂.fst (β := fun (x : ↥X) ↦
      { f : X.presheaf.stalk x ⟶ R //
        IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }))
⊢ Inseparable
    (f₁.fst (β := fun (x : ↥X) ↦
      { f : X.presheaf.stalk x ⟶ R //
        IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }))
    (f₂.fst (β := fun (x : ↥X) ↦
      { f : X.presheaf.stalk x ⟶ R //
        IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }))

Tactic:
rw [h₁]
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X Y : Scheme
f : X ⟶ Y
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
f₁ f₂ :
  (x : ↥X) ×
    { f : X.presheaf.stalk x ⟶ R //
      IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }
h₁ :
  f₁.fst (β := fun (x : ↥X) ↦
      { f : X.presheaf.stalk x ⟶ R //
        IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }) =
    f₂.fst (β := fun (x : ↥X) ↦
      { f : X.presheaf.stalk x ⟶ R //
        IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
⊢ Inseparable
    (f₂.fst (β := fun (x : ↥X) ↦
      { f : X.presheaf.stalk x ⟶ R //
        IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }))
    (f₂.fst (β := fun (x : ↥X) ↦
      { f : X.presheaf.stalk x ⟶ R //
        IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
R : CommRingCat
f₁ f₂ :
  (x : ↥X) ×
    { f : X.presheaf.stalk x ⟶ R //
      IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }
mp :
  f₁ = f₂ →
    ∃ (h₁ :
      f₁.fst (β := fun (x : ↥X) ↦
          { f : X.presheaf.stalk x ⟶ R //
            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }) =
        f₂.fst (β := fun (x : ↥X) ↦
          { f : X.presheaf.stalk x ⟶ R //
            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })),
      (↑(f₁.snd (β := fun (x : ↥X) ↦
              { f : X.presheaf.stalk x ⟶ R //
                IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })) :
          X.presheaf.stalk f₁.fst ⟶ R) =
        Iso.hom (X.presheaf.stalkCongr ⋯) ≫
          (↑(f₂.snd (β := fun (x : ↥X) ↦
                { f : X.presheaf.stalk x ⟶ R //
                  IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })) :
            X.presheaf.stalk f₂.fst ⟶ R)
mpr :
  (∃ (h₁ :
      f₁.fst (β := fun (x : ↥X) ↦
          { f : X.presheaf.stalk x ⟶ R //
            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }) =
        f₂.fst (β := fun (x : ↥X) ↦
          { f : X.presheaf.stalk x ⟶ R //
            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })),
      (↑(f₁.snd (β := fun (x : ↥X) ↦
              { f : X.presheaf.stalk x ⟶ R //
                IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })) :
          X.presheaf.stalk f₁.fst ⟶ R) =
        Iso.hom (X.presheaf.stalkCongr ⋯) ≫
          (↑(f₂.snd (β := fun (x : ↥X) ↦
                { f : X.presheaf.stalk x ⟶ R //
                  IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })) :
            X.presheaf.stalk f₂.fst ⟶ R)) →
    f₁ = f₂
⊢ f₁ = f₂ ↔
    ∃ (h₁ :
      f₁.fst (β := fun (x : ↥X) ↦
          { f : X.presheaf.stalk x ⟶ R //
            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }) =
        f₂.fst (β := fun (x : ↥X) ↦
          { f : X.presheaf.stalk x ⟶ R //
            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })),
      (↑(f₁.snd (β := fun (x : ↥X) ↦
              { f : X.presheaf.stalk x ⟶ R //
                IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })) :
          X.presheaf.stalk f₁.fst ⟶ R) =
        Iso.hom (X.presheaf.stalkCongr ⋯) ≫
          (↑(f₂.snd (β := fun (x : ↥X) ↦
                { f : X.presheaf.stalk x ⟶ R //
                  IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })) :
            X.presheaf.stalk f₂.fst ⟶ R)

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
R : CommRingCat
f₁ :
  (x : ↥X) ×
    { f : X.presheaf.stalk x ⟶ R //
      IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }
⊢ ∃ (h₁ :
    f₁.fst (β := fun (x : ↥X) ↦
        { f : X.presheaf.stalk x ⟶ R //
          IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) }) =
      f₁.fst (β := fun (x : ↥X) ↦
        { f : X.presheaf.stalk x ⟶ R //
          IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })),
    (↑(f₁.snd (β := fun (x : ↥X) ↦
            { f : X.presheaf.stalk x ⟶ R //
              IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })) :
        X.presheaf.stalk f₁.fst ⟶ R) =
      Iso.hom (X.presheaf.stalkCongr ⋯) ≫
        (↑(f₁.snd (β := fun (x : ↥X) ↦
              { f : X.presheaf.stalk x ⟶ R //
                IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })) :
          X.presheaf.stalk f₁.fst ⟶ R)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
R : CommRingCat
x₁ : ↥X
f₁ : X.presheaf.stalk x₁ ⟶ R
h₁ : IsLocalHom (R := (↑(X.presheaf.stalk x₁) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f₁)
f₂ : X.presheaf.stalk x₁ ⟶ R
h₂ : IsLocalHom (R := (↑(X.presheaf.stalk x₁) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f₂)
e :
  f₁ =
    CategoryStruct.comp (Y :=
      X.presheaf.stalk
        (Sigma.fst (β := fun (x : ↥X) ↦
          { f : X.presheaf.stalk x ⟶ R //
            IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
          (Sigma.mk (β := fun (x : ↥X) ↦
            { f : X.presheaf.stalk x ⟶ R //
              IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
            x₁
            (Subtype.mk (p := fun (f : X.presheaf.stalk x₁ ⟶ R) ↦
              IsLocalHom (R := (↑(X.presheaf.stalk x₁) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)) f₂
              h₂))))
      (Iso.hom (X.presheaf.stalkCongr ⋯))
      (↑(Sigma.snd (β := fun (x : ↥X) ↦
            { f : X.presheaf.stalk x ⟶ R //
              IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
            (Sigma.mk (β := fun (x : ↥X) ↦
              { f : X.presheaf.stalk x ⟶ R //
                IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
              x₁
              (Subtype.mk (p := fun (f : X.presheaf.stalk x₁ ⟶ R) ↦
                IsLocalHom (R := (↑(X.presheaf.stalk x₁) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)) f₂
                h₂))) :
        X.presheaf.stalk ⟨x₁, ⟨f₂, h₂⟩⟩.fst ⟶ R)
⊢ Eq (α :=
    (x : ↥X) ×
      { f : X.presheaf.stalk x ⟶ R //
        IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
    (Sigma.mk (β := fun (x : ↥X) ↦
      { f : X.presheaf.stalk x ⟶ R //
        IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
      x₁
      (Subtype.mk (p := fun (f : X.presheaf.stalk x₁ ⟶ R) ↦
        IsLocalHom (R := (↑(X.presheaf.stalk x₁) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)) f₁ h₁))
    (Sigma.mk (β := fun (x : ↥X) ↦
      { f : X.presheaf.stalk x ⟶ R //
        IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f) })
      x₁
      (Subtype.mk (p := fun (f : X.presheaf.stalk x₁ ⟶ R) ↦
        IsLocalHom (R := (↑(X.presheaf.stalk x₁) : Type u)) (S := (↑R : Type u)) (CommRingCat.Hom.hom f)) f₂ h₂))

Tactic:
simp [e]