awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X : Scheme
x y : ↥X
e : x = y
⊢ (residueFieldCongr e).symm = residueFieldCongr ⋯

Tactic:
rfl

Premises used: CategoryTheory.Functor.op, Eq.mpr, AlgebraicGeometry.Scheme.residueFieldCongr, Set.Mem, CategoryTheory.eqToHom, setOf, CategoryTheory.eqToIso, CategoryTheory.Functor.comp, IsLocalRing.maximalIdeal, nonunits, AddOpposite, AlgebraicGeometry.Scheme.residueField, IsLocalRing.ResidueField, Monotone.functor, Quotient, CategoryTheory.Iso.symm, TopologicalSpace.OpenNhds, Submodule.quotientRel, AddAction.orbitRel, TopologicalSpace.OpenNhds.inclusion, rfl
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X : Scheme
x y : ↥X
e : x = y
⊢ (residueFieldCongr e).inv = (residueFieldCongr ⋯).hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X : Scheme
x y z : ↥X
e : x = y
e' : y = z
subst : residueFieldCongr ⋯ ≪≫ residueFieldCongr ⋯ = residueFieldCongr ⋯
⊢ residueFieldCongr e ≪≫ residueFieldCongr e' = residueFieldCongr ⋯

Tactic:
subst e e'
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X : Scheme
x : ↥X
⊢ residueFieldCongr ⋯ ≪≫ residueFieldCongr ⋯ = residueFieldCongr ⋯

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X : Scheme
x y z : ↥X
e : x = y
e' : y = z
subst : (residueFieldCongr ⋯).hom ≫ (residueFieldCongr ⋯).hom = (residueFieldCongr ⋯).hom
⊢ (residueFieldCongr e).hom ≫ (residueFieldCongr e').hom = (residueFieldCongr ⋯).hom

Tactic:
subst e e'
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X : Scheme
x : ↥X
⊢ (residueFieldCongr ⋯).hom ≫ (residueFieldCongr ⋯).hom = (residueFieldCongr ⋯).hom

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X : Scheme
x y : ↥X
h : x = y
subst : X.residue x ≫ (residueFieldCongr ⋯).hom = Iso.hom (X.presheaf.stalkCongr ⋯) ≫ X.residue x
⊢ X.residue x ≫ (residueFieldCongr h).hom = Iso.hom (X.presheaf.stalkCongr ⋯) ≫ X.residue y

Tactic:
subst h
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X : Scheme
x : ↥X
⊢ X.residue x ≫ (residueFieldCongr ⋯).hom = Iso.hom (X.presheaf.stalkCongr ⋯) ≫ X.residue x

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X_1 : Scheme
U : X_1.Opens
X Y : Scheme
f_1 f g : X ⟶ Y
e : f = g
x : ↥X
subst : Eq (α := ↥Y) (f x : ↥Y) (f x : ↥Y)
⊢ Eq (α := ↥Y) (f x : ↥Y) (g x : ↥Y)

Tactic:
subst e
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X_1 : Scheme
U : X_1.Opens
X Y : Scheme
f_1 f : X ⟶ Y
x : ↥X
⊢ Eq (α := ↥Y) (f x : ↥Y) (f x : ↥Y)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X Y : Scheme
f g : X ⟶ Y
e : f = g
x : ↥X
subst : residueFieldMap f x = (residueFieldCongr ⋯).hom ≫ residueFieldMap f x
⊢ residueFieldMap f x = (residueFieldCongr ⋯).hom ≫ residueFieldMap g x

Tactic:
subst e
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ residueFieldMap f x = (residueFieldCongr ⋯).hom ≫ residueFieldMap f x

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X_1 : Scheme
U : X_1.Opens
X_2 Y : Scheme
f : X_2 ⟶ Y
X : Scheme
x : ↥X
rw : IsPreimmersion (Spec.map (X.residue x))
⊢ IsPreimmersion (Spec.map (X.residue x) ≫ X.fromSpecStalk x)

Tactic:
rw [IsPreimmersion.comp_iff]

Premises used: AlgebraicGeometry.IsPreimmersion.comp_iff
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X_1 : Scheme
U : X_1.Opens
X_2 Y : Scheme
f : X_2 ⟶ Y
X : Scheme
x : ↥X
⊢ IsPreimmersion (Spec.map (X.residue x))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X : Scheme
x y : ↥X
h : x = y
subst : Spec.map (residueFieldCongr ⋯).hom ≫ X.fromSpecResidueField x = X.fromSpecResidueField x
⊢ Spec.map (residueFieldCongr h).hom ≫ X.fromSpecResidueField x = X.fromSpecResidueField y

Tactic:
subst h
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X : Scheme
x : ↥X
⊢ Spec.map (residueFieldCongr ⋯).hom ≫ X.fromSpecResidueField x = X.fromSpecResidueField x

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
rw :
  Spec.map (Y.residue (f x) ≫ residueFieldMap f x) ≫ Y.fromSpecStalk (f x) =
    Spec.map (stalkMap f x ≫ X.residue x) ≫ Y.fromSpecStalk (f x)
⊢ Spec.map (residueFieldMap f x) ≫ Spec.map (Y.residue (f x)) ≫ Y.fromSpecStalk (f x) =
    (Spec.map (X.residue x) ≫ X.fromSpecStalk x) ≫ f

Tactic:
rw [Category.assoc, ← SpecMap_stalkMap_fromSpecStalk, ← Spec.map_comp_assoc,
    ← Spec.map_comp_assoc]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Spec.map_comp_assoc, AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ Spec.map (Y.residue (f x) ≫ residueFieldMap f x) ≫ Y.fromSpecStalk (f x) =
    Spec.map (stalkMap f x ≫ X.residue x) ≫ Y.fromSpecStalk (f x)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X : Scheme
x : ↥X
s : ↥(Spec (X.residueField x))
⊢ (X.fromSpecResidueField x) s = x

Tactic:
simp [fromSpecResidueField]

Premises used: AlgebraicGeometry.Scheme.fromSpecResidueField
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
X : Scheme
x : ↥X
⊢ Eq (α := Set ↥X) (Set.range (ι := ↥(Spec (X.residueField x))) ⇑(X.fromSpecResidueField x)) {x}

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
K : Type u_1
inst : Field K
X : Scheme
x : ↥X
f : X.presheaf.stalk x ⟶ CommRingCat.of K
inst_1 :
  IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u_1)) (S := (↑(CommRingCat.of K) : Type u_1)) (CommRingCat.Hom.hom f)
⊢ Spec.map (descResidueField f) ≫ X.fromSpecResidueField x = Spec.map f ≫ X.fromSpecStalk x

Tactic:
simp [fromSpecResidueField, ← Spec.map_comp_assoc]

Premises used: AlgebraicGeometry.Spec.map_comp_assoc, AlgebraicGeometry.Scheme.fromSpecResidueField
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
K : Type u
inst : Field K
X : Scheme
f : Spec (CommRingCat.of K) ⟶ X
rw :
  CategoryStruct.comp (Y := Spec (X.presheaf.stalk (f (closedPoint (↑(CommRingCat.of K) : Type u)))))
      (Spec.map (stalkClosedPointTo f)) (X.fromSpecStalk (f (closedPoint (↑(CommRingCat.of K) : Type u)))) =
    f
rw₁ rw₂ : f = f
⊢ CategoryStruct.comp (Y := Spec (X.residueField (f (closedPoint (↑(CommRingCat.of K) : Type u)))))
      (Spec.map (descResidueField (stalkClosedPointTo f))) (X.fromSpecResidueField (f (closedPoint K))) =
    f

Tactic:
rw [X.descResidueField_fromSpecResidueField, Scheme.Spec_stalkClosedPointTo_fromSpecStalk]

Premises used: AlgebraicGeometry.Scheme.descResidueField_fromSpecResidueField, AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
R : CommRingCat
x : ↥(Spec R)
rw :
  Eq (α := CommRingCat.of (↑R : Type u_1) ⟶ (Spec R).residueField x)
    (CommRingCat.ofHom (algebraMap (↑R : Type u_1) x.asIdeal.ResidueField) ≫ (residueFieldIso R x).inv)
    (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.AtPrime x.asIdeal)) ≫
      (Spec.stalkIso R x).inv ≫ (Spec R).residue x)
⊢ CommRingCat.ofHom (algebraMap (↑R : Type u_1) x.asIdeal.ResidueField) ≫ (residueFieldIso R x).inv =
    (ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial ≫ (Spec R).residue x

Tactic:
rw [← Spec.algebraMap_stalkIso_inv_assoc]

Premises used: AlgebraicGeometry.Spec.algebraMap_stalkIso_inv_assoc
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
R : CommRingCat
x : ↥(Spec R)
⊢ Eq (α := CommRingCat.of (↑R : Type u_1) ⟶ (Spec R).residueField x)
    (CommRingCat.ofHom (algebraMap (↑R : Type u_1) x.asIdeal.ResidueField) ≫ (residueFieldIso R x).inv)
    (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.AtPrime x.asIdeal)) ≫
      (Spec.stalkIso R x).inv ≫ (Spec R).residue x)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
R : CommRingCat
x : ↥(Spec R)
⊢ (Spec R).residue x ≫ (residueFieldIso R x).hom =
    (Spec.stalkIso R x).hom ≫ CommRingCat.ofHom (algebraMap (Localization.AtPrime x.asIdeal) x.asIdeal.ResidueField)

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, AddCon.liftOn, Submodule.Quotient.mk, OreLocalization, MonoidHomClass.toMonoidHom, IsLocalRing.ResidueField, Quotient, RingHomClass.toRingHom, Submodule.quotientRel, AddAction.orbitRel, OreLocalization.liftExpand, rfl
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
R : CommRingCat
x : ↥(Spec R)
simp :
  Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) x.asIdeal.ResidueField) ≫ (residueFieldIso R x).inv) =
    Spec.map (((ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial) ≫ (Spec R).residue x)
⊢ Spec.map (residueFieldIso R x).inv ≫
      Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) x.asIdeal.ResidueField)) =
    (Spec R).fromSpecResidueField x

Tactic:
simp only [Scheme.fromSpecResidueField, Spec.fromSpecStalk_eq, ← Spec.map_comp]

Premises used: AlgebraicGeometry.Scheme.fromSpecResidueField, AlgebraicGeometry.Spec.map_comp, AlgebraicGeometry.Spec.fromSpecStalk_eq
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
R : CommRingCat
x : ↥(Spec R)
rw :
  CommRingCat.ofHom (algebraMap (↑R : Type u_1) x.asIdeal.ResidueField) ≫ (residueFieldIso R x).inv =
    ((ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial) ≫ (Spec R).residue x
⊢ Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) x.asIdeal.ResidueField) ≫ (residueFieldIso R x).inv) =
    Spec.map (((ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial) ≫ (Spec R).residue x)

Tactic:
rw [Spec.map_inj]

Premises used: AlgebraicGeometry.Spec.map_inj
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
R : CommRingCat
x : ↥(Spec R)
⊢ CommRingCat.ofHom (algebraMap (↑R : Type u_1) x.asIdeal.ResidueField) ≫ (residueFieldIso R x).inv =
    ((ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial) ≫ (Spec R).residue x

Tactic:
simp [← Scheme.Spec.algebraMap_residueFieldIso_inv]

Premises used: AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
K : Type u_1
inst : Field K
X : Scheme
f₁ f₂ : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)
mp :
  f₁ = f₂ →
    ∃ (e :
      f₁.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) =
        f₂.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)),
      f₁.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) =
        (residueFieldCongr e).hom ≫ f₂.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
mpr :
  (∃ (e :
      f₁.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) =
        f₂.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)),
      f₁.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) =
        (residueFieldCongr e).hom ≫ f₂.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)) →
    f₁ = f₂
⊢ f₁ = f₂ ↔
    ∃ (e :
      f₁.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) =
        f₂.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)),
      f₁.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) =
        (residueFieldCongr e).hom ≫ f₂.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
K : Type u_1
inst : Field K
X : Scheme
f₁ : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)
⊢ ∃ (e :
    f₁.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) =
      f₁.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)),
    f₁.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) =
      (residueFieldCongr e).hom ≫ f₁.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
K : Type u_1
inst : Field K
X : Scheme
f₁ f₂ : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)
mpr :
  ∀ (f : ↥X) (snd : X.residueField f ⟶ CommRingCat.of K),
    (∃ (e :
        Sigma.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
            (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd) =
          f₂.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)),
        Sigma.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
            (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd) =
          (residueFieldCongr e).hom ≫ f₂.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)) →
      Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd = f₂
⊢ (∃ (e :
      f₁.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) =
        f₂.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)),
      f₁.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) =
        (residueFieldCongr e).hom ≫ f₂.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)) →
    f₁ = f₂

Tactic:
obtain ⟨f, _⟩ := f₁
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
K : Type u_1
inst : Field K
X : Scheme
f₂ : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)
f : ↥X
snd : X.residueField f ⟶ CommRingCat.of K
mpr :
  ∀ (g : ↥X) (snd_1 : X.residueField g ⟶ CommRingCat.of K),
    (∃ (e :
        Sigma.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
            (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd) =
          Sigma.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
            (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) g snd_1)),
        Eq (α :=
          X.residueField
              (Sigma.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
                (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd)) ⟶
            CommRingCat.of K)
          (Sigma.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
              (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd) :
            X.residueField
                (Sigma.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
                  (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd)) ⟶
              CommRingCat.of K)
          ((residueFieldCongr e).hom ≫
              Sigma.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
                (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) g snd_1) :
            X.residueField
                (Sigma.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
                  (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd)) ⟶
              CommRingCat.of K)) →
      Eq (α := (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K))
        (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd)
        (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) g snd_1)
⊢ (∃ (e :
      Sigma.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
          (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd) =
        f₂.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)),
      Sigma.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
          (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd) =
        (residueFieldCongr e).hom ≫ f₂.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)) →
    Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd = f₂

Tactic:
obtain ⟨g, _⟩ := f₂
-- Module: Mathlib.AlgebraicGeometry.ResidueField
Goal:
K : Type u_1
inst : Field K
X : Scheme
f : ↥X
snd snd_1 : X.residueField f ⟶ CommRingCat.of K
h :
  Eq (α :=
    X.residueField
        (Sigma.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
          (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd)) ⟶
      CommRingCat.of K)
    (Sigma.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
        (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd) :
      X.residueField
          (Sigma.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
            (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd)) ⟶
        CommRingCat.of K)
    ((residueFieldCongr ⋯).hom ≫
        Sigma.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
          (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd_1) :
      X.residueField
          (Sigma.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
            (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd)) ⟶
        CommRingCat.of K)
⊢ Eq (α := (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K))
    (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd)
    (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K) f snd_1)

Tactic:
simpa
-- 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 :
  ∃ (e :
    Sigma.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
        ((fun (f : Spec (CommRingCat.of K) ⟶ X) ↦
            (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
                (f (closedPoint (↑(CommRingCat.of K) : Type u))) (descResidueField (stalkClosedPointTo f)) :
              (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)))
          ((fun (xf : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)) ↦
              Spec.map (xf.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)) ≫
                X.fromSpecResidueField (xf.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))
            f)) =
      f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)),
    Sigma.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
        ((fun (f : Spec (CommRingCat.of K) ⟶ X) ↦
            (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
                (f (closedPoint (↑(CommRingCat.of K) : Type u))) (descResidueField (stalkClosedPointTo f)) :
              (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)))
          ((fun (xf : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)) ↦
              Spec.map (xf.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)) ≫
                X.fromSpecResidueField (xf.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))
            f)) =
      (residueFieldCongr e).hom ≫ f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
⊢ (fun (f : Spec (CommRingCat.of K) ⟶ X) ↦
        (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
            (f (closedPoint (↑(CommRingCat.of K) : Type u))) (descResidueField (stalkClosedPointTo f)) :
          (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)))
      ((fun (xf : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)) ↦
          Spec.map (xf.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)) ≫
            X.fromSpecResidueField (xf.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))
        f) =
    f

Tactic:
rw [SpecToEquivOfField_eq_iff]

Premises used: AlgebraicGeometry.Scheme.SpecToEquivOfField_eq_iff
-- 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)
simp :
  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))
⊢ ∃ (e :
    Sigma.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
        ((fun (f : Spec (CommRingCat.of K) ⟶ X) ↦
            (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
                (f (closedPoint (↑(CommRingCat.of K) : Type u))) (descResidueField (stalkClosedPointTo f)) :
              (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)))
          ((fun (xf : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)) ↦
              Spec.map (xf.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)) ≫
                X.fromSpecResidueField (xf.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))
            f)) =
      f.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)),
    Sigma.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
        ((fun (f : Spec (CommRingCat.of K) ⟶ X) ↦
            (Sigma.mk (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)
                (f (closedPoint (↑(CommRingCat.of K) : Type u))) (descResidueField (stalkClosedPointTo f)) :
              (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)))
          ((fun (xf : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)) ↦
              Spec.map (xf.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)) ≫
                X.fromSpecResidueField (xf.fst (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)))
            f)) =
      (residueFieldCongr e).hom ≫ f.snd (β := fun (x : ↥X) ↦ X.residueField x ⟶ CommRingCat.of K)

Tactic:
simp only [CommRingCat.coe_of, Scheme.Hom.comp_base, TopCat.coe_comp, Function.comp_apply,
      Scheme.fromSpecResidueField_apply, exists_true_left]

Premises used: exists_true_left, CommRingCat.coe_of, Function.comp_apply, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.coe_comp, AlgebraicGeometry.Scheme.fromSpecResidueField_apply