awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
e_f :
  Eq (α := Γ(X, U) ⟶ X.presheaf.stalk x)
    (CategoryStruct.comp (Y := (↑U : Scheme).presheaf.stalk (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU))
        (U.topIso.inv ≫ (↑U : Scheme).presheaf.germ ⊤ (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU) trivial)
        (inv (Hom.stalkMap U.ι (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU))) :
      Γ(X, U) ⟶ X.presheaf.stalk x)
    (X.presheaf.germ U x hxU : X.presheaf.obj (op U) ⟶ X.presheaf.stalk x)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
e_f :
  Eq (α :=
    (↑U : Scheme).presheaf.obj (op ⊤) ⟶ (↑U : Scheme).presheaf.stalk (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU))
    ((↑U : Scheme).presheaf.germ ⊤ (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU) trivial)
    (U.topIso.hom ≫
      CategoryStruct.comp (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU)
        (Hom.stalkMap U.ι (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU)))
⊢ Eq (α := Γ(X, U) ⟶ X.presheaf.stalk x)
    (CategoryStruct.comp (Y := (↑U : Scheme).presheaf.stalk (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU))
        (U.topIso.inv ≫ (↑U : Scheme).presheaf.germ ⊤ (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU) trivial)
        (inv (Hom.stalkMap U.ι (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU))) :
      Γ(X, U) ⟶ X.presheaf.stalk x)
    (X.presheaf.germ U x hxU : X.presheaf.obj (op U) ⟶ X.presheaf.stalk x)

Tactic:
rw [IsIso.comp_inv_eq, Iso.inv_comp_eq]

Premises used: CategoryTheory.Iso.inv_comp_eq, CategoryTheory.IsIso.comp_inv_eq
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
e_f :
  Eq (α :=
    (↑U : Scheme).presheaf.obj (op ⊤) ⟶ (↑U : Scheme).presheaf.stalk (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU))
    ((↑U : Scheme).presheaf.germ ⊤ (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU) trivial)
    (U.topIso.hom ≫
      Hom.app U.ι U ≫ (↑U : Scheme).presheaf.germ (U.ι ⁻¹ᵁ U) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU) hxU)
⊢ Eq (α :=
    (↑U : Scheme).presheaf.obj (op ⊤) ⟶ (↑U : Scheme).presheaf.stalk (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU))
    ((↑U : Scheme).presheaf.germ ⊤ (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU) trivial)
    (U.topIso.hom ≫
      CategoryStruct.comp (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU)
        (Hom.stalkMap U.ι (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU)))

Tactic:
erw [Hom.germ_stalkMap U.ι U ⟨x, hxU⟩]

Premises used: Subtype.mk, AlgebraicGeometry.Scheme.Hom.germ_stalkMap, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
e_f :
  Eq (α :=
    (↑U : Scheme).presheaf.obj (op ⊤) ⟶ (↑U : Scheme).presheaf.stalk (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU))
    ((↑U : Scheme).presheaf.germ ⊤ (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU) trivial)
    (CategoryStruct.comp (Y := Γ(X, U.ι ''ᵁ U.ι ⁻¹ᵁ U))
      (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯) ≫ Quiver.Hom.op (homOfLE ⋯)))
      ((↑U : Scheme).presheaf.germ (U.ι ⁻¹ᵁ U) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU) hxU))
⊢ Eq (α :=
    (↑U : Scheme).presheaf.obj (op ⊤) ⟶ (↑U : Scheme).presheaf.stalk (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU))
    ((↑U : Scheme).presheaf.germ ⊤ (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU) trivial)
    (U.topIso.hom ≫
      Hom.app U.ι U ≫ (↑U : Scheme).presheaf.germ (U.ι ⁻¹ᵁ U) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU) hxU)

Tactic:
rw [Opens.ι_app, Opens.topIso_hom, ← Functor.map_comp_assoc]

Premises used: CategoryTheory.Functor.map_comp_assoc, AlgebraicGeometry.Scheme.Opens.ι_app, AlgebraicGeometry.Scheme.Opens.topIso_hom
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
⊢ Eq (α :=
    (↑U : Scheme).presheaf.obj (op ⊤) ⟶ (↑U : Scheme).presheaf.stalk (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU))
    ((↑U : Scheme).presheaf.germ ⊤ (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU) trivial)
    (CategoryStruct.comp (Y := Γ(X, U.ι ''ᵁ U.ι ⁻¹ᵁ U))
      (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯) ≫ Quiver.Hom.op (homOfLE ⋯)))
      ((↑U : Scheme).presheaf.germ (U.ι ⁻¹ᵁ U) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU) hxU))

Tactic:
(U.toScheme.presheaf.germ_res (homOfLE le_top) ⟨x, hxU⟩ (U := U.ι ⁻¹ᵁ U) hxU).symm

Premises used: IsOpenMap.functorMap, Set.Mem, Subtype.mk, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.Presheaf.germ_res, le_top, CategoryTheory.homOfLE, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Eq.symm, AlgebraicGeometry.Scheme.Opens.toScheme, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
U : X.Opens
x : ↥X
hxU : x ∈ U
⊢ Eq (α :=
    (↑U : Scheme).presheaf.obj (op ⊤) ⟶ (↑U : Scheme).presheaf.stalk (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU))
    ((↑U : Scheme).presheaf.germ ⊤ (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU) trivial)
    (CategoryStruct.comp (Y := Γ(X, U.ι ''ᵁ U.ι ⁻¹ᵁ U))
      (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯) ≫ Quiver.Hom.op (homOfLE ⋯)))
      ((↑U : Scheme).presheaf.germ (U.ι ⁻¹ᵁ U) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU) hxU))

Tactic:
exact (U.toScheme.presheaf.germ_res (homOfLE le_top) ⟨x, hxU⟩ (U := U.ι ⁻¹ᵁ U) hxU).symm

Premises used: Subtype.mk, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.Presheaf.germ_res, le_top, CategoryTheory.homOfLE, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Eq.symm, AlgebraicGeometry.Scheme.Opens.toScheme, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
R : CommRingCat
x : ↥(Spec R)
rw : IsAffineOpen.fromSpecStalk ⋯ trivial = map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial)
rw₁ :
  Eq (α := Spec ((Spec R).presheaf.stalk x) ⟶ Spec R)
    (map ((Spec R).presheaf.germ ⊤ x trivial) ≫ IsAffineOpen.fromSpec ⋯)
    (map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial))
rw₂ :
  Eq (α := Spec ((Spec R).presheaf.stalk x) ⟶ Spec R)
    (map ((Spec R).presheaf.germ ⊤ x trivial) ≫ Iso.inv (Spec R).isoSpec)
    (map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial))
rw₃ :
  Eq (α := Spec ((Spec R).presheaf.stalk x) ⟶ Spec R)
    (map ((Spec R).presheaf.germ ⊤ x trivial) ≫ map (Scheme.ΓSpecIso R).inv)
    (map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial))
rw₄ rw₅ :
  Eq (α := Spec ((Spec R).presheaf.stalk x) ⟶ Spec R)
    (map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial))
    (map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial))
⊢ (Spec R).fromSpecStalk x = map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial)

Tactic:
rw [← (isAffineOpen_top (Spec R)).fromSpecStalk_eq_fromSpecStalk (x := x) trivial,
    IsAffineOpen.fromSpecStalk, IsAffineOpen.fromSpec_top, Scheme.isoSpec_Spec_inv,
    ← Spec.map_comp]

Premises used: AlgebraicGeometry.isAffineOpen_top, AlgebraicGeometry.Spec, trivial, AlgebraicGeometry.Spec.map_comp, AlgebraicGeometry.Scheme.isoSpec_Spec_inv, AlgebraicGeometry.IsAffineOpen.fromSpecStalk, AlgebraicGeometry.IsAffineOpen.fromSpec_top, AlgebraicGeometry.IsAffineOpen.fromSpecStalk_eq_fromSpecStalk
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
R : CommRingCat
x : ↥(Spec R)
⊢ (Spec R).fromSpecStalk x = map (StructureSheaf.toStalk (↑R : Type u_1) x)

Tactic:
Spec.fromSpecStalk_eq _ _

Premises used: AlgebraicGeometry.Spec.topObj, Set.Mem, setOf, AlgebraicGeometry.PrimeSpectrum.Top, AlgebraicGeometry.structurePresheafInCommRingCat, AlgebraicGeometry.Spec.fromSpecStalk_eq, AlgebraicGeometry.StructureSheaf.toStalk
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
hf :
  ∀ (x : (↑R : Type u)),
    Eq (α := (↑((Spec R).presheaf.stalk (closedPoint (↑R : Type u))) : Type u))
      ((CommRingCat.Hom.hom (Iso.inv (stalkClosedPointIso R)) :
            (a : (↑R : Type u)) → (↑((Spec R).presheaf.stalk (closedPoint (↑R : Type u))) : Type u))
          x :
        (↑((Spec R).presheaf.stalk (closedPoint (↑R : Type u))) : Type u))
      ((CommRingCat.Hom.hom (StructureSheaf.toStalk (↑R : Type u) (closedPoint (↑R : Type u))) :
            (a : (↑R : Type u)) → (↑((Spec R).presheaf.stalk (closedPoint (↑R : Type u))) : Type u))
          x :
        (↑((Spec R).presheaf.stalk (closedPoint (↑R : Type u))) : Type u))
⊢ Eq (α := R ⟶ (Spec R).presheaf.stalk (closedPoint (↑R : Type u))) (Iso.inv (stalkClosedPointIso R))
    (StructureSheaf.toStalk (↑R : Type u) (closedPoint (↑R : Type u)))

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
x : (↑R : Type u)
⊢ Eq (α := (↑((Spec R).presheaf.stalk (closedPoint (↑R : Type u))) : Type u))
    ((CommRingCat.Hom.hom (Iso.inv (stalkClosedPointIso R)) :
          (a : (↑R : Type u)) → (↑((Spec R).presheaf.stalk (closedPoint (↑R : Type u))) : Type u))
        x :
      (↑((Spec R).presheaf.stalk (closedPoint (↑R : Type u))) : Type u))
    ((CommRingCat.Hom.hom (StructureSheaf.toStalk (↑R : Type u) (closedPoint (↑R : Type u))) :
          (a : (↑R : Type u)) → (↑((Spec R).presheaf.stalk (closedPoint (↑R : Type u))) : Type u))
        x :
      (↑((Spec R).presheaf.stalk (closedPoint (↑R : Type u))) : Type u))

Tactic:
(StructureSheaf.stalkIso _ _).commutes _

Premises used: AlgebraicGeometry.Spec.topObj, Set.Mem, AlgEquiv.commutes, AlgebraicGeometry.StructureSheaf.stalkIso, Quotient.mk', AlgebraicGeometry.PrimeSpectrum.Top, AlgebraicGeometry.structurePresheafInCommRingCat, OreLocalization.oreDiv
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
x : (↑R : Type u)
⊢ Eq (α := (↑((Spec R).presheaf.stalk (closedPoint (↑R : Type u))) : Type u))
    ((CommRingCat.Hom.hom (Iso.inv (stalkClosedPointIso R)) :
          (a : (↑R : Type u)) → (↑((Spec R).presheaf.stalk (closedPoint (↑R : Type u))) : Type u))
        x :
      (↑((Spec R).presheaf.stalk (closedPoint (↑R : Type u))) : Type u))
    ((CommRingCat.Hom.hom (StructureSheaf.toStalk (↑R : Type u) (closedPoint (↑R : Type u))) :
          (a : (↑R : Type u)) → (↑((Spec R).presheaf.stalk (closedPoint (↑R : Type u))) : Type u))
        x :
      (↑((Spec R).presheaf.stalk (closedPoint (↑R : Type u))) : Type u))

Tactic:
exact (StructureSheaf.stalkIso _ _).commutes _

Premises used: AlgEquiv.commutes, AlgebraicGeometry.StructureSheaf.stalkIso
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
rw :
  Eq (α := R ⟶ (Spec R).presheaf.stalk (closedPoint (↑R : Type u)))
    (StructureSheaf.toStalk (↑R : Type u) (closedPoint (↑R : Type u)))
    ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ (closedPoint (↑R : Type u)) trivial)
⊢ Eq (α := Γ(Spec R, ⊤) ⟶ (Spec R).presheaf.stalk (closedPoint (↑R : Type u)))
    ((Scheme.ΓSpecIso R).hom ≫ Iso.inv (stalkClosedPointIso R))
    ((Spec R).presheaf.germ ⊤ (closedPoint (↑R : Type u)) trivial)

Tactic:
rw [stalkClosedPointIso_inv, ← Iso.eq_inv_comp]

Premises used: AlgebraicGeometry.stalkClosedPointIso_inv, CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
⊢ Eq (α := R ⟶ (Spec R).presheaf.stalk (closedPoint (↑R : Type u)))
    (StructureSheaf.toStalk (↑R : Type u) (closedPoint (↑R : Type u)))
    ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ (closedPoint (↑R : Type u)) trivial)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
rw :
  CategoryStruct.comp (Y := (Spec R).presheaf.stalk (closedPoint (↑R : Type u)))
      ((Scheme.ΓSpecIso R).hom ≫ Iso.inv (stalkClosedPointIso R)) (Iso.hom (stalkClosedPointIso R)) =
    (Scheme.ΓSpecIso R).hom
rw₁ :
  (Scheme.ΓSpecIso R).hom ≫
      CategoryStruct.comp (Y := (Spec R).presheaf.stalk (closedPoint (↑R : Type u))) (Iso.inv (stalkClosedPointIso R))
        (Iso.hom (stalkClosedPointIso R)) =
    (Scheme.ΓSpecIso R).hom
rw₂ : (Scheme.ΓSpecIso R).hom ≫ 𝟙 R = (Scheme.ΓSpecIso R).hom
rw₃ rw₄ : (Scheme.ΓSpecIso R).hom = (Scheme.ΓSpecIso R).hom
⊢ CategoryStruct.comp (Y := (Spec R).presheaf.stalk (closedPoint (↑R : Type u)))
      ((Spec R).presheaf.germ ⊤ (closedPoint (↑R : Type u)) trivial) (Iso.hom (stalkClosedPointIso R)) =
    (Scheme.ΓSpecIso R).hom

Tactic:
rw [← ΓSpecIso_hom_stalkClosedPointIso_inv, Category.assoc, Iso.inv_hom_id, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Category.comp_id, AlgebraicGeometry.ΓSpecIso_hom_stalkClosedPointIso_inv
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
rw :
  Eq.{u + 1} (α := Spec ((Spec R).presheaf.stalk (closedPoint (↑R : Type u))) ⟶ Spec R)
    (Spec.map (StructureSheaf.toStalk (↑R : Type u) (closedPoint (↑R : Type u))))
    ((Spec R).fromSpecStalk (closedPoint (↑R : Type u)))
rw₁ rw₂ :
  Eq.{u + 1} (α := Spec ((Spec R).presheaf.stalk (closedPoint (↑R : Type u))) ⟶ Spec R)
    (Spec.map (StructureSheaf.toStalk (↑R : Type u) (closedPoint (↑R : Type u))))
    (Spec.map (StructureSheaf.toStalk (↑R : Type u) (closedPoint (↑R : Type u))))
⊢ Eq (α := Spec ((Spec R).presheaf.stalk (closedPoint (↑R : Type u))) ⟶ Spec R)
    (Spec.map (Iso.inv (stalkClosedPointIso R))) ((Spec R).fromSpecStalk (closedPoint (↑R : Type u)))

Tactic:
rw [stalkClosedPointIso_inv, Spec.fromSpecStalk_eq']

Premises used: AlgebraicGeometry.Spec.fromSpecStalk_eq', AlgebraicGeometry.stalkClosedPointIso_inv
-- 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
⊢ IsLocalHom (R := (↑(X.presheaf.stalk (f (closedPoint (↑R : Type u)))) : Type u)) (S := (↑R : Type u)) (F :=
    (↑(X.presheaf.stalk (f (closedPoint (↑R : Type u)))) : Type u) →+* (↑R : Type u))
    (CommRingCat.Hom.hom (stalkClosedPointTo f))

Tactic:
inferInstanceAs <| IsLocalHom (f.stalkMap (closedPoint R) ≫ (stalkClosedPointIso R).hom).hom

Premises used: _private.0.AlgebraicGeometry.Scheme.isLocalHom_stalkClosedPointTo._proof_1
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X Y : Scheme
f_1 : X ⟶ Y
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
R_1 : CommRingCat
inst : IsLocalRing.{u} (↑R_1 : Type u)
f_2 : Spec R_1 ⟶ X
R : Type u
inst_1 : CommRing R
inst_2 : IsLocalRing R
f : Spec (CommRingCat.of R) ⟶ X
⊢ IsLocalHom (R := (↑(X.presheaf.stalk (f (closedPoint (↑(CommRingCat.of R) : Type u)))) : Type u)) (S :=
    (↑(CommRingCat.of R) : Type u)) (F :=
    (↑(X.presheaf.stalk (f (closedPoint (↑(CommRingCat.of R) : Type u)))) : Type u) →+* (↑(CommRingCat.of R) : Type u))
    (CommRingCat.Hom.hom (stalkClosedPointTo f))

Tactic:
isLocalHom_stalkClosedPointTo f

Premises used: AlgebraicGeometry.Scheme.isLocalHom_stalkClosedPointTo
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
f : Spec R ⟶ X
U : X.Opens
hU : Membership.mem (α := ↥X) U (f (closedPoint (↑R : Type u)) : ↥X)
⊢ f ⁻¹ᵁ U = ⊤

Tactic:
IsLocalRing.closed_point_mem_iff.mp hU

Premises used: IsLocalRing.closed_point_mem_iff, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X Y : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
f : Spec R ⟶ X
g : X ⟶ Y
rw :
  Eq (α := Y.presheaf.stalk ((f ≫ g) (closedPoint (↑R : Type u))) ⟶ R)
    ((Hom.stalkMap g (f (closedPoint (↑R : Type u))) ≫ Hom.stalkMap f (closedPoint (↑R : Type u))) ≫
      Iso.hom (stalkClosedPointIso R))
    (Hom.stalkMap g (f (closedPoint (↑R : Type u))) ≫ stalkClosedPointTo f)
⊢ Eq (α := Y.presheaf.stalk ((f ≫ g) (closedPoint (↑R : Type u))) ⟶ R) (stalkClosedPointTo (f ≫ g))
    (Hom.stalkMap g (f (closedPoint (↑R : Type u))) ≫ stalkClosedPointTo f)

Tactic:
rw [stalkClosedPointTo, Scheme.Hom.stalkMap_comp]

Premises used: AlgebraicGeometry.Scheme.Hom.stalkMap_comp, AlgebraicGeometry.Scheme.stalkClosedPointTo
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X Y : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
f : Spec R ⟶ X
g : X ⟶ Y
⊢ Eq (α := Y.presheaf.stalk ((f ≫ g) (closedPoint (↑R : Type u))) ⟶ R)
    ((Hom.stalkMap g (f (closedPoint (↑R : Type u))) ≫ Hom.stalkMap f (closedPoint (↑R : Type u))) ≫
      Iso.hom (stalkClosedPointIso R))
    (Hom.stalkMap g (f (closedPoint (↑R : Type u))) ≫ stalkClosedPointTo f)

Tactic:
Category.assoc _ _ _

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X Y : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
f : Spec R ⟶ X
g : X ⟶ Y
⊢ Eq (α := Y.presheaf.stalk ((f ≫ g) (closedPoint (↑R : Type u))) ⟶ R)
    ((Hom.stalkMap g (f (closedPoint (↑R : Type u))) ≫ Hom.stalkMap f (closedPoint (↑R : Type u))) ≫
      Iso.hom (stalkClosedPointIso R))
    (Hom.stalkMap g (f (closedPoint (↑R : Type u))) ≫ stalkClosedPointTo f)

Tactic:
exact Category.assoc _ _ _

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
R S : CommRingCat
inst : IsLocalRing.{u_1} (↑S : Type u_1)
φ : R ⟶ S
rw :
  φ ≫
      (ΓSpecIso S).inv ≫
        CategoryStruct.comp (Y := (Spec S).presheaf.stalk (closedPoint (↑S : Type u_1)))
          ((Spec S).presheaf.germ (Spec.map φ ⁻¹ᵁ ⊤) (closedPoint (↑S : Type u_1)) trivial)
          (Iso.hom (stalkClosedPointIso S)) =
    φ
⊢ CategoryStruct.comp (Y := (Spec R).presheaf.stalk ((Spec.map φ) (closedPoint (↑S : Type u_1))))
      ((Spec R).presheaf.germ ⊤ ((Spec.map φ) (closedPoint (↑S : Type u_1))) trivial)
      (stalkClosedPointTo (Spec.map φ)) =
    (ΓSpecIso R).hom ≫ φ

Tactic:
rw [stalkClosedPointTo, Scheme.Hom.germ_stalkMap_assoc, ← Iso.inv_comp_eq,
    ← ΓSpecIso_inv_naturality_assoc]

Premises used: AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality_assoc, AlgebraicGeometry.Scheme.Hom.germ_stalkMap_assoc, CategoryTheory.Iso.inv_comp_eq, AlgebraicGeometry.Scheme.stalkClosedPointTo
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
R S : CommRingCat
inst : IsLocalRing.{u_1} (↑S : Type u_1)
φ : R ⟶ S
rw : φ ≫ (ΓSpecIso S).inv ≫ (ΓSpecIso S).hom = φ
rw₁ : φ ≫ 𝟙 S = φ
rw₂ rw₃ : φ = φ
⊢ φ ≫
      (ΓSpecIso S).inv ≫
        CategoryStruct.comp (Y := (Spec S).presheaf.stalk (closedPoint (↑S : Type u_1)))
          ((Spec S).presheaf.germ ⊤ (closedPoint (↑S : Type u_1)) trivial) (Iso.hom (stalkClosedPointIso S)) =
    φ

Tactic:
rw [germ_stalkClosedPointIso_hom, Iso.inv_hom_id, Category.comp_id]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Category.comp_id, AlgebraicGeometry.germ_stalkClosedPointIso_hom
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
f : Spec R ⟶ X
U : X.Opens
hU : Membership.mem (α := ↥X) U (f (closedPoint (↑R : Type u)) : ↥X)
rw :
  Hom.app f U ≫
      CategoryStruct.comp (Y := (Spec R).presheaf.stalk (closedPoint (↑R : Type u)))
        ((Spec R).presheaf.germ (f ⁻¹ᵁ U) (closedPoint (↑R : Type u)) hU) (Iso.hom (stalkClosedPointIso R)) =
    Hom.app f U ≫ (Functor.mapIso (Spec R).presheaf (Iso.op (eqToIso ⋯))).hom ≫ (ΓSpecIso R).hom
⊢ X.presheaf.germ U (f (closedPoint (↑R : Type u))) hU ≫ stalkClosedPointTo f =
    Hom.app f U ≫ (Functor.mapIso (Spec R).presheaf (Iso.op (eqToIso ⋯)) ≪≫ ΓSpecIso R).hom

Tactic:
rw [stalkClosedPointTo, Scheme.Hom.germ_stalkMap_assoc, Iso.trans_hom]

Premises used: AlgebraicGeometry.Scheme.Hom.germ_stalkMap_assoc, CategoryTheory.Iso.trans_hom, AlgebraicGeometry.Scheme.stalkClosedPointTo
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
f : Spec R ⟶ X
U : X.Opens
hU : Membership.mem (α := ↥X) U (f (closedPoint (↑R : Type u)) : ↥X)
e_a :
  CategoryStruct.comp (Y := (Spec R).presheaf.stalk (closedPoint (↑R : Type u)))
      ((Spec R).presheaf.germ (f ⁻¹ᵁ U) (closedPoint (↑R : Type u)) hU) (Iso.hom (stalkClosedPointIso R)) =
    (Functor.mapIso (Spec R).presheaf (Iso.op (eqToIso ⋯))).hom ≫ (ΓSpecIso R).hom
⊢ Hom.app f U ≫
      CategoryStruct.comp (Y := (Spec R).presheaf.stalk (closedPoint (↑R : Type u)))
        ((Spec R).presheaf.germ (f ⁻¹ᵁ U) (closedPoint (↑R : Type u)) hU) (Iso.hom (stalkClosedPointIso R)) =
    Hom.app f U ≫ (Functor.mapIso (Spec R).presheaf (Iso.op (eqToIso ⋯))).hom ≫ (ΓSpecIso R).hom

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
f : Spec R ⟶ X
U : X.Opens
hU : Membership.mem (α := ↥X) U (f (closedPoint (↑R : Type u)) : ↥X)
e_a :
  Eq (α := Γ(Spec R, f ⁻¹ᵁ U) ⟶ (Spec R).presheaf.stalk (closedPoint (↑R : Type u)))
    ((Spec R).presheaf.germ (f ⁻¹ᵁ U) (closedPoint (↑R : Type u)) hU)
    ((Functor.mapIso (Spec R).presheaf (Iso.op (eqToIso ⋯))).hom ≫
      (Spec R).presheaf.germ ⊤ (closedPoint (↑R : Type u)) trivial)
⊢ CategoryStruct.comp (Y := (Spec R).presheaf.stalk (closedPoint (↑R : Type u)))
      ((Spec R).presheaf.germ (f ⁻¹ᵁ U) (closedPoint (↑R : Type u)) hU) (Iso.hom (stalkClosedPointIso R)) =
    (Functor.mapIso (Spec R).presheaf (Iso.op (eqToIso ⋯))).hom ≫ (ΓSpecIso R).hom

Tactic:
rw [← Iso.eq_comp_inv, Category.assoc, ΓSpecIso_hom_stalkClosedPointIso_inv]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.eq_comp_inv, AlgebraicGeometry.ΓSpecIso_hom_stalkClosedPointIso_inv
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X : Scheme
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
f : Spec R ⟶ X
U : X.Opens
hU : Membership.mem (α := ↥X) U (f (closedPoint (↑R : Type u)) : ↥X)
⊢ Eq (α := Γ(Spec R, f ⁻¹ᵁ U) ⟶ (Spec R).presheaf.stalk (closedPoint (↑R : Type u)))
    ((Spec R).presheaf.germ (f ⁻¹ᵁ U) (closedPoint (↑R : Type u)) hU)
    ((Functor.mapIso (Spec R).presheaf (Iso.op (eqToIso ⋯))).hom ≫
      (Spec R).presheaf.germ ⊤ (closedPoint (↑R : Type u)) trivial)

Tactic:
simp only [Functor.mapIso_hom, Iso.op_hom, eqToIso.hom,
    TopCat.Presheaf.germ_res]

Premises used: CategoryTheory.eqToIso.hom, CategoryTheory.Iso.op_hom, TopCat.Presheaf.germ_res, CategoryTheory.Functor.mapIso_hom
-- Module: Mathlib.AlgebraicGeometry.Stalk
Goal:
X Y : Scheme
f_1 : X ⟶ Y
U_1 V : X.Opens
hU_1 : IsAffineOpen U_1
hV : IsAffineOpen V
R : CommRingCat
inst : IsLocalRing.{u} (↑R : Type u)
f_2 : Spec R ⟶ X
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)
⊢ x ∈ U

Tactic:
simpa using 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)
rw : (X.fromSpecStalk x) ((Spec.map f) (closedPoint (↑R : Type u)) : ↥(Spec (X.presheaf.stalk x))) = x
rw₁ : (X.fromSpecStalk x) (closedPoint (↑(X.presheaf.stalk x) : Type u)) = x
rw₂ rw₃ : x = x
⊢ (Spec.map f ≫ X.fromSpecStalk x) (closedPoint (↑R : Type u)) = x

Tactic:
rw [Hom.comp_apply, Spec_closedPoint, fromSpecStalk_closedPoint]

Premises used: AlgebraicGeometry.Scheme.fromSpecStalk_closedPoint, AlgebraicGeometry.Scheme.Hom.comp_apply, AlgebraicGeometry.Spec_closedPoint
-- 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)
⊢ (Spec.map f ≫ X.fromSpecStalk x) (closedPoint (↑R : Type u)) = x

Tactic:
have : (Spec.map f ≫ X.fromSpecStalk x) (closedPoint R) = x := by
    rw [Hom.comp_apply, Spec_closedPoint, fromSpecStalk_closedPoint]