awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact ⟨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⟩
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
Goal:
X : LocallyRingedSpace
x : (↑X.toTopCat : Type u)
f : (↑(X.presheaf.obj (op ⊤)) : Type u)
⊢ Membership.mem (γ := Opens (↑X.toTopCat : Type u)) ⊤ x

Tactic:
trivial
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : (↑X.toTopCat : Type u)
⊢ Eq (α :=
    CommRingCat.of
        (↑(Y.presheaf.stalk
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) f.base :
                  (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                x)) :
          Type u) ⟶
      X.residueField x)
    (CategoryStruct.comp (Y :=
      CommRingCat.of
        (IsLocalRing.ResidueField
          (↑(Y.presheaf.stalk
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                      TopCat.carrier) f.base :
                    (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                  x)) :
            Type u)))
      (CommRingCat.ofHom
        (IsLocalRing.residue
          (↑(Y.presheaf.stalk
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                      TopCat.carrier) f.base :
                    (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                  x)) :
            Type u)))
      (CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap f x)))))
    (Hom.stalkMap f x ≫ CommRingCat.ofHom (IsLocalRing.residue (↑(X.presheaf.stalk x) : Type u)))

Tactic:
rfl
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
Goal:
X : LocallyRingedSpace
x : (↑X.toTopCat : Type u)
hf : CommRingCat.Hom.hom (residueFieldMap (𝟙 X) x) = CommRingCat.Hom.hom (𝟙 (X.residueField x))
⊢ residueFieldMap (𝟙 X) x = 𝟙 (X.residueField x)

Tactic:
ext : 1
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
Goal:
X : LocallyRingedSpace
x : (↑X.toTopCat : Type u)
hf :
  CommRingCat.Hom.hom
      (CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (𝟙 (X.presheaf.stalk x))))) =
    CommRingCat.Hom.hom (𝟙 (X.residueField x))
⊢ CommRingCat.Hom.hom (residueFieldMap (𝟙 X) x) = CommRingCat.Hom.hom (𝟙 (X.residueField x))

Tactic:
simp only [residueFieldMap, stalkMap_id]

Premises used: AlgebraicGeometry.LocallyRingedSpace.stalkMap_id, AlgebraicGeometry.LocallyRingedSpace.residueFieldMap
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
Goal:
X : LocallyRingedSpace
x : (↑X.toTopCat : Type u)
⊢ CommRingCat.Hom.hom
      (CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (𝟙 (X.presheaf.stalk x))))) =
    CommRingCat.Hom.hom (𝟙 (X.residueField x))

Tactic:
apply IsLocalRing.ResidueField.map_id

Premises used: IsLocalRing.ResidueField.map_id
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
Z : LocallyRingedSpace
g : Y ⟶ Z
x : (↑X.toTopCat : Type u)
hf :
  CommRingCat.Hom.hom (residueFieldMap (f ≫ g) x) =
    CommRingCat.Hom.hom
      (residueFieldMap g
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                f.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
            x) ≫
        residueFieldMap f x)
⊢ residueFieldMap (f ≫ g) x =
    residueFieldMap g
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              f.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
          x) ≫
      residueFieldMap f x

Tactic:
ext : 1
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
Z : LocallyRingedSpace
g : Y ⟶ Z
x : (↑X.toTopCat : Type u)
hf :
  Eq (α :=
    (↑(Z.residueField
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                  TopCat.carrier) (f ≫ g).base :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u))
              x)) :
        Type u) →+*
      (↑(X.residueField x) : Type u))
    (CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (IsLocalRing.ResidueField.map
          (CommRingCat.Hom.hom
            (Hom.stalkMap g
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                      TopCat.carrier) f.base :
                    (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                  x) ≫
              Hom.stalkMap f x)))))
    (CommRingCat.Hom.hom
      (CategoryStruct.comp (Y :=
        Y.residueField
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                f.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
            x))
        (CommRingCat.ofHom
          (IsLocalRing.ResidueField.map
            (CommRingCat.Hom.hom
              (Hom.stalkMap g
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                      TopCat.carrier) f.base :
                    (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                  x)))))
        (CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap f x))))))
⊢ CommRingCat.Hom.hom (residueFieldMap (f ≫ g) x) =
    CommRingCat.Hom.hom
      (residueFieldMap g
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                f.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
            x) ≫
        residueFieldMap f x)

Tactic:
simp only [residueFieldMap, stalkMap_comp]

Premises used: AlgebraicGeometry.LocallyRingedSpace.residueFieldMap, AlgebraicGeometry.LocallyRingedSpace.stalkMap_comp
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
Z : LocallyRingedSpace
g : Y ⟶ Z
x : (↑X.toTopCat : Type u)
⊢ Eq (α :=
    (↑(Z.residueField
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                  TopCat.carrier) (f ≫ g).base :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u))
              x)) :
        Type u) →+*
      (↑(X.residueField x) : Type u))
    (CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (IsLocalRing.ResidueField.map
          (CommRingCat.Hom.hom
            (Hom.stalkMap g
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                      TopCat.carrier) f.base :
                    (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                  x) ≫
              Hom.stalkMap f x)))))
    (CommRingCat.Hom.hom
      (CategoryStruct.comp (Y :=
        Y.residueField
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                f.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
            x))
        (CommRingCat.ofHom
          (IsLocalRing.ResidueField.map
            (CommRingCat.Hom.hom
              (Hom.stalkMap g
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                      TopCat.carrier) f.base :
                    (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                  x)))))
        (CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap f x))))))

Tactic:
apply IsLocalRing.ResidueField.map_comp (Hom.stalkMap g (f.base x)).hom (Hom.stalkMap f x).hom

Premises used: CommRingCat.Hom.hom, IsLocalRing.ResidueField.map_comp, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe, AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : (↑X.toTopCat : Type u)
⊢ Membership.mem (γ := Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u)) ⊤ x

Tactic:
trivial
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : (↑X.toTopCat : Type u)
a : (↑(Y.presheaf.obj (op ⊤)) : Type u)
⊢ Membership.mem (γ := Opens (↑(↑X.toPresheafedSpace : TopCat) : Type u)) ⊤ x

Tactic:
trivial
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X : LocallyRingedSpace
x : (↑X.toTopCat : Type u)
⊢ IsLocalRing.{u} (↑(X.presheaf.stalk x) : Type u)

Tactic:
X.isLocalRing x

Premises used: AlgebraicGeometry.LocallyRingedSpace.isLocalRing
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y : LocallyRingedSpace
f : X.Hom Y.toPresheafedSpace
hf :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)),
    IsLocalHom (R :=
      (↑(Y.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  f.base :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
              x)) :
        Type u))
      (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
      (↑(Y.presheaf.stalk
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    f.base :
                  (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                x)) :
          Type u) →+*
        (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (f.stalkMap x))
⊢ { toHom := f, prop := hf : X.Hom Y }.toShHom = InducedCategory.homMk f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y : LocallyRingedSpace
f g : X ⟶ Y
h : f.toHom = g.toHom
mk :
  ∀ (toHom : X.Hom Y.toPresheafedSpace)
    (prop :
      ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)),
        IsLocalHom (R :=
          (↑(Y.presheaf.stalk
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      toHom.base :
                    (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                  x)) :
            Type u))
          (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
          (↑(Y.presheaf.stalk
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        carrier) toHom.base :
                      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                    x)) :
              Type u) →+*
            (↑(X.presheaf.stalk x) : Type u))
          (CommRingCat.Hom.hom (toHom.stalkMap x)))
    (h : { toHom := toHom, prop := prop : X.Hom Y }.toHom = g.toHom), { toHom := toHom, prop := prop : X.Hom Y } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y : LocallyRingedSpace
g : X ⟶ Y
toHom : X.Hom Y.toPresheafedSpace
prop :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)),
    IsLocalHom (R :=
      (↑(Y.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  toHom.base :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
              x)) :
        Type u))
      (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
      (↑(Y.presheaf.stalk
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    toHom.base :
                  (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                x)) :
          Type u) →+*
        (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (toHom.stalkMap x))
h : { toHom := toHom, prop := prop : X.Hom Y }.toHom = g.toHom
mk :
  ∀ (toHom_1 : X.Hom Y.toPresheafedSpace)
    (prop_1 :
      ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)),
        IsLocalHom (R :=
          (↑(Y.presheaf.stalk
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      toHom_1.base :
                    (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                  x)) :
            Type u))
          (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
          (↑(Y.presheaf.stalk
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        carrier) toHom_1.base :
                      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                    x)) :
              Type u) →+*
            (↑(X.presheaf.stalk x) : Type u))
          (CommRingCat.Hom.hom (toHom_1.stalkMap x)))
    (h : { toHom := toHom, prop := prop : X.Hom Y }.toHom = { toHom := toHom_1, prop := prop_1 }.toHom),
    { toHom := toHom, prop := prop : X.Hom Y } = { toHom := toHom_1, prop := prop_1 }
⊢ { toHom := toHom, prop := prop : X.Hom Y } = g

Tactic:
cases g
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y : LocallyRingedSpace
toHom : X.Hom Y.toPresheafedSpace
prop :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)),
    IsLocalHom (R :=
      (↑(Y.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  toHom.base :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
              x)) :
        Type u))
      (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
      (↑(Y.presheaf.stalk
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    toHom.base :
                  (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                x)) :
          Type u) →+*
        (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (toHom.stalkMap x))
toHom_1 : X.Hom Y.toPresheafedSpace
prop_1 :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)),
    IsLocalHom (R :=
      (↑(Y.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  toHom_1.base :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
              x)) :
        Type u))
      (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
      (↑(Y.presheaf.stalk
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    toHom_1.base :
                  (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
                x)) :
          Type u) →+*
        (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (toHom_1.stalkMap x))
h : { toHom := toHom, prop := prop : X.Hom Y }.toHom = { toHom := toHom_1, prop := prop_1 }.toHom
⊢ { toHom := toHom, prop := prop : X.Hom Y } = { toHom := toHom_1, prop := prop_1 }

Tactic:
congr
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : (↑X.toTopCat : Type u)
⊢ IsLocalHom (R :=
    (↑(Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                f.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
            x)) :
      Type u))
    (S := (↑(X.presheaf.stalk x) : Type u)) (CommRingCat.Hom.hom (Hom.stalkMap f x))

Tactic:
f.2 x

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.prop
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X_1 X Y : LocallyRingedSpace
f : X ⟶ Y
x : (↑X.toTopCat : Type u)
⊢ IsLocalHom (R :=
    (↑(Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                f.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
            x)) :
      Type u))
    (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
    (↑(Y.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  f.base :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
              x)) :
        Type u) →+*
      (↑(X.presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom (f.stalkMap x))

Tactic:
isLocalHomStalkMap f x

Premises used: AlgebraicGeometry.LocallyRingedSpace.isLocalHomStalkMap
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X Y : LocallyRingedSpace
f : X.Hom Y
x : (↑X.toTopCat : Type u)
⊢ IsLocalHom (R :=
    (↑(Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                f.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
            x)) :
      Type u))
    (S := (↑(X.presheaf.stalk x) : Type u)) (CommRingCat.Hom.hom (f.stalkMap x))

Tactic:
f.2 x

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.prop
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X_1 X : LocallyRingedSpace
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)
dsimp :
  IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
    (↑(X.presheaf.stalk x) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (𝟙 X.toPresheafedSpace) x))
⊢ IsLocalHom (R :=
    (↑(X.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (PresheafedSpace.Hom.base (𝟙 X.toPresheafedSpace)) :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑X.toPresheafedSpace : TopCat) : Type u))
            x)) :
      Type u))
    (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
    (↑(X.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (PresheafedSpace.Hom.base (𝟙 X.toPresheafedSpace)) :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑X.toPresheafedSpace : TopCat) : Type u))
              x)) :
        Type u) →+*
      (↑(X.presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (𝟙 X.toPresheafedSpace) x))

Tactic:
dsimp
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X_1 X : LocallyRingedSpace
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)
erw :
  IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑(X.presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom (𝟙 (X.presheaf.stalk x)))
⊢ IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
    (↑(X.presheaf.stalk x) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (𝟙 X.toPresheafedSpace) x))

Tactic:
erw [PresheafedSpace.stalkMap.id]

Premises used: AlgebraicGeometry.PresheafedSpace.stalkMap.id
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X_1 X : LocallyRingedSpace
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)
⊢ IsLocalHom (R := (↑(X.presheaf.stalk x) : Type u)) (S := (↑(X.presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom (𝟙 (X.presheaf.stalk x)))

Tactic:
infer_instance
-- Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace
Goal:
X_1 X Y Z : LocallyRingedSpace
f : X.Hom Y
g : Y.Hom Z
x : (↑(↑X.toPresheafedSpace : TopCat) : Type u)
rw :
  IsLocalHom (R :=
    (↑(Z.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                (↑X.toPresheafedSpace : TopCat)) (Y := (↑Z.toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base (f.toHom ≫ g.toHom)) :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u))
            x)) :
      Type u))
    (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
    (↑(Z.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (X := (↑X.toPresheafedSpace : TopCat)) (Y := (↑Z.toPresheafedSpace : TopCat))
                  (PresheafedSpace.Hom.base (f.toHom ≫ g.toHom)) :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u))
              x)) :
        Type u) →+*
      (↑(X.presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom
      (g.stalkMap
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                f.base :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type u))
            x) ≫
        f.stalkMap x))
⊢ IsLocalHom (R :=
    (↑(Z.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                (↑X.toPresheafedSpace : TopCat)) (Y := (↑Z.toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base (f.toHom ≫ g.toHom)) :
              (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u))
            x)) :
      Type u))
    (S := (↑(X.presheaf.stalk x) : Type u)) (F :=
    (↑(Z.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (X := (↑X.toPresheafedSpace : TopCat)) (Y := (↑Z.toPresheafedSpace : TopCat))
                  (PresheafedSpace.Hom.base (f.toHom ≫ g.toHom)) :
                (a : (↑(↑X.toPresheafedSpace : TopCat) : Type u)) → (↑(↑Z.toPresheafedSpace : TopCat) : Type u))
              x)) :
        Type u) →+*
      (↑(X.presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (f.toHom ≫ g.toHom) x))

Tactic:
rw [PresheafedSpace.stalkMap.comp]

Premises used: AlgebraicGeometry.PresheafedSpace.stalkMap.comp